Repository navigation
PVL-001 EV-8a — PVL-8a: pv discharge run — one summary the tree can carry #4202
Description
Aprender-side row of PVL-001 that blocks the ontology spec (ONT-001), which the operator requires finished in 0.70 ("ensure we know that .70 must have FULL ontology spec and all aprender binary working", relayed verbatim by the cop aprender-cf, 2026-09-24). IDs are SPEC-QUALIFIED: this is PVL-001 EV-8a. APEX-001 reuses the same EV numbers, so a bare "EV-8a" is ambiguous.
Row (paiml/infra docs/specifications/PVL-001-pv-lean-gate.md:201), verbatim: EV-8a aprender · "PVL-8a: pv discharge run — one summary the tree can carry" · depends_on EV-5a, EV-6a, EV-6b, EV-7b · K̂ 90
- depends_on (PVL-001): EV-5a, EV-6a, EV-6b, EV-7b
- K̂: 90
- blocks: EV-8b → EV-9 → ONT-5 → ONT-9; EV-12 → ONT-10 (the critical path to ONT-9 ONT-9: the ontology has a contract; checker soundness by Kani and planted-solution generation #4078 / ONT-10 ONT-10: release aprender-contracts-cli with ONT-0..9 (incl. 4d, 4e) — CI tags, operator publishes (RP-001) #4079).
Filed by apex-4c at the cop's instruction (aprender-cf): no aprender issue existed for this row.
Activity
noahgift commentedon Sep 24, 2026
Taken by aprender-98 on the cop's (aprender-cf) assignment, 2026-09-24. Order: EV-7b first, then EV-8a. Checked
git ls-remote originfirst: no branch exists for this row.noahgift commentedon Oct 12, 2026
evidence for close: #4655 / 989cb01 (on main), how checked (PVL-001 row probe, file-level parts run on main):
pv discharge runis incrates/aprender-contracts-cli/src/commands/discharge.rs(cites PVL-001 EV-8a — PVL-8a: pv discharge run — one summary the tree can carry #4202).crates/aprender-contracts-staging/discharge-summary.jsonis tracked; itstree_sha(bed17c8db6) equals the lean tree's object id on main, withlake_exit=0,leanchecker_exit=0,axioms_ok=true, 108 modules;lean/discharge.jsonis gitignored.noahgift commentedon Oct 12, 2026
Cop batch close (FLOW-004 drain, ≤43/d): fix verified on main — merged #4655 ; ancestor of origin/main: 989cb01 . Evidence: #4202 (comment)