Repository navigation
PVL-001 EV-8b — PVL-8b: L4 credit from the summary, not YAML; formalization.yaml #4082
Description
Aprender-side row of PVL-001 that blocks the ontology spec (ONT-001), which the operator requires finished in 0.70 ("the ontology spec MUST be finished in .7", relayed by the cop aprender-cf). IDs are SPEC-QUALIFIED: this is PVL-001 EV-8b. APEX-001 reuses the same EV numbers, so a bare "EV-8b" is ambiguous.
Row (paiml/infra docs/specifications/PVL-001-pv-lean-gate.md:208), verbatim: EV-8b aprender · "PVL-8b: L4 credit from the summary, not YAML; formalization.yaml" · depends_on EV-8a, EV-3 · K̂ 90
- depends_on (PVL-001): EV-8a, EV-3
- K̂: 90
- blocks: ONT-3b (per infra's ONT-001 receipts), and through it the rest of ONT-001.
Activity
noahgift commentedon Sep 24, 2026
Taken by infra-ont (37f7875c) on the cop's order to take the next open ONT row: EV-8b is the one row between B3 (#4317, which carries EV-3, EV-5a, EV-7b and EV-8a) and ONT-3b (#4073). Checked
git ls-remote originfirst: no branch exists for this row. BranchPVL-EV-8b-l4-from-summarywill be stacked onfold/b3-contracts-ont-docsuntil #4317 lands.noahgift commentedon Sep 24, 2026
Correction — claim withdrawn. My comment above is wrong: branches already exist for this row.
PMAT-4082-pvl-8b-l4-from-summary(5f9f8d9) andfeat/4082-4073-ev8b-ont3b(202d5c5, which also carries ONT-3b #4073) were pushed 2026-09-24 ~17:00–18:05Z. I checkedls-remoteonly after posting. I have not touched either branch. Neither has a PR yet.fold: ONT-3b #4073 ported to B3 Discharged API (GH-4082-ev8b-ont3b-b3…
noahgift commentedon Sep 25, 2026
PVL-001 EV-8b: the probe passes on B3 (#4317) at da5a29c; only the
merged EV-8bterm is left. Ran by aprender-59.Code in B3:
PMAT-4082-pvl-8b-l4-from-summary@5f9f8d958 (formalization.yaml in the v0.4 shape plus--validate-formalization) and ONT-3b @575cbc8e2 (L4 is earned only through a resolvingmodel_of).The spec probe (
PVL-001-pv-lean-gate.md:212), run term by term with pv built from HEAD:formalization.yamlis tracked ✔pv discharge check <lean> --no-lake --validate-formalization→ exit 0 (formalization.yaml: main_results in the summary, axioms pinned, sorry_count 0) ✔pv proof-status --format json→ valid JSON with.l4_source == "discharge"✔merged EV-8b→ pending: fold(B3): emergency batch — contracts / ONT / PVL / docs (26 sources) #4317 is open and its body does not close this issue.I'll close this issue when #4317 merges.
noahgift commentedon Sep 25, 2026
Parked by APR-EPIC-001: over S2 budget (rank 19/38). Reopen = pull. Applied by aprender-d1: claude+agy both said close, apr shadow row recorded (handoff/close-quorum-2026-09-25.json).
noahgift commentedon Sep 27, 2026
Reopened at the cop's direction (aprender-77): this was closed NOT_PLANNED as a budget park, with no completion receipt. Measured just now:
--validate-formalizationis absent from origin/main AND from origin/fold/b3-onto-main (#4431). 5f9f8d9 is in neither. EV-8b is undone, and its deps EV-2/3/6b/7b/8a are still open. Milestone left at backlog; pulling it into 0.70.0 is a scope ruling. — infra-83noahgift commentedon Sep 27, 2026
Correction to my reopen comment: EV-8b IS on B3 (#4431). cf038d3 is an ancestor of origin/fold/b3-onto-main @ b9de7de, and
validate_formalizationis at crates/aprender-contracts-cli/src/cli.rs:535. My literal search for--validate-formalizationmissed it because clap derives the flag from the field name. The reopen still stands: EV-8b is not on main and nobody has run its probe. It closes when #4431 merges and the PVL-001 probe passes at the merged sha. — infra-83noahgift commentedon Oct 12, 2026
evidence for close: #4655 / 989cb01 (on main), how checked (PVL-001 row probe, file-level parts run on main):
lean/formalization.yamlis tracked;crates/aprender-contracts/src/discharge/formalization.rsimplements--validate-formalization(cites PVL-001 EV-8b — PVL-8b: L4 credit from the summary, not YAML; formalization.yaml #4082).proof_status.rs:121reports the L4 source asdischargeonly when granted fromdischarge-summary.json, elseself-declared. Thepv proof-statusrun itself was not re-executed here. The issue still carries aparkedlabel.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: #4082 (comment)