Repository navigation
PVL-001 EV-2 — PVL-2: proof-status resolves bindings; ghost binding is a reject #4080
Closed as not planned
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-2. APEX-001 reuses the same EV numbers, so a bare "EV-2" is ambiguous.
Row (paiml/infra docs/specifications/PVL-001-pv-lean-gate.md:115), verbatim: EV-2 aprender · "PVL-2: proof-status resolves bindings; ghost binding is a reject" · depends_on EV-1 · K̂ 80
- depends_on (PVL-001): EV-1
- K̂: 80
- blocks: ONT-3a (per infra's ONT-001 receipts), and through it the rest of ONT-001.
Activity
fix(contracts): regenerate contracts/contracts.nt for PMAT-4080's new…
chore(audit): PMAT-4080 quorum receipt — round 2: 3/3 PASS (gemini, m…
chore(audit): PMAT-4080 — record the cop ruling accepting round 2 as …
KaniStrategyhas no label for symbolic-f32-array harnesses, the dominant DSP verification technique — 7 of rmedia's 8 real Kani proofs are unrepresentable #2530KaniStrategyhas no label for symbolic-f32-array harnesses, the dominant DSP verification technique — 7 of rmedia's 8 real Kani proofs are unrepresentable #2530noahgift commentedon Oct 14, 2026
Folded into #5310 as a checklist row (TRIAGE-100, 2026-10-14): the open-ticket cap is 100, so this ticket is now tracked on that master and closed as not planned. Nothing is lost: reopen it when its work resumes, and an open PR for it reopens it. Pushed branch:
devont/4080-ev2-pub-use-alias.Agent: aprender-clerk