Repository navigation
proof-debt: triage matches proven#107 overly-cautious-OWED pattern — 17 Coq axioms + 5 Idris believe_me's discharge candidates #70
Description
Context
A 2026-05-30 estate-wide survey for proof-debt patterns found that absolute-zero exhibits the same "overly cautious OWED" pattern as proven (proven#107 catalogues 32+ OWEDs discharged today by reading underlying definitions rather than trusting the OWED narrative).
absolute-zero's own triage
`docs/proof-debt-triage.md` already pre-classifies:
- 52 AXIOM (permanent — external / hardness assumptions)
- 17 DISCHARGE (should be provable)
- 3 PROPERTY-TEST
The 17 DISCHARGE-classified axioms + the 5 `believe_me` sites in `src/abi/` are direct analogues to proven's literal-input OWEDs.
Sampled candidates (per survey)
| File | Line | Site | Disposition | Discharge note |
|---|---|---|---|---|
| proofs/coq/quantum/QuantumCNO.v | 258 | `global_phase_unitary` | DISCHARGE | "Derivable from gate algebra" |
| proofs/coq/quantum/QuantumCNO.v | 283 | `X_gate_not_identity` | DISCHARGE | "Existence proof; exhibit `|0⟩` as witness" |
| proofs/coq/category/CNOCategory.v | 323 | `hom_functor` | DISCHARGE | "Should be a `Definition`, not an `Axiom`" |
| src/abi/Proofs/DivMod.idr | 90 | `alignedSizeCorrect _ _ = believe_me ()` | — | comment lays out full discharge path via `Data.Nat.Division.DivisionTheorem` |
| src/abi/Layout.idr | 268 | `programStateAlignmentValid _ = believe_me ()` | — | notes "claim is computationally true; gap is the typechecker's"; literal `n=8 mod 4` should reduce per the proven#119 empirical map |
Empirical reduction-map applies
The Idris2 0.8.0 reduction map from proven#119 and `feedback_proven_overly_cautious_owed_pattern` memory shows:
- Literal Char/String/Nat/Bits32 reductions DO work
- Smart-constructor unfolding DOES work
- `div`/`mod` on Nat literals does NOT (one tried + closed at proven#117)
The `programStateAlignmentValid` (literal n=8 mod 4) and the 4 sampled DISCHARGE Coq axioms look directly analogous. Caveat: Coq's reduction is different (no `Refl` per se; uses `reflexivity`/`simpl`/`vm_compute`), but the principle "the OWED comment overstates the blocker" likely carries over.
Recommended next steps
- Phase 1 (quick wins): try the 4-5 Coq DISCHARGE axioms first. Estimate: 1-2 hours.
- Phase 2 (`believe_me` removal): tackle the 5 `src/abi/` Idris files using the literal-input pattern. Estimate: 2-4 hours.
- Phase 3: re-triage the remaining 12 DISCHARGE Coq axioms against the empirical map.
Could be a 1-day campaign similar to proven's today (which cleared 32+ OWEDs).
Out of scope
- 52 AXIOM-classified Coq axioms — permanent (external math / hardness assumptions)
- 3 PROPERTY-TEST sites — those need separate test-runner work
Reference
- proven#107 — sister issue documenting the pattern
- proven#119 — paths-forward analysis (Path A/B/C)
- proven
feedback_proven_overly_cautious_owed_patternmemory +reference_idris2_0_8_0_reduction_mapmemory
Owner decision: greenlight Phase 1 attempt, or defer?
Activity
hyperpolymath commentedon May 30, 2026
Empirical update — Phase 1 NOT a quick-win after closer inspection
Spent 30 min probing the 4 candidate quick-wins from this issue's body:
X_gate_not_identityParameter(abstract), and|0⟩isn't defined in the model. Would need to add a concreteX_gatedefinition + abasis_statemodel — architectural changes, not 30-min work.hom_functorglobal_phase_unitaryprogramStateAlignmentValid(Idris2)/tmp/charrefl(perreference_idris2_0_8_0_reduction_mapmemory):modon Nat literals does NOT reduce. Same family as proven#117 (closed for same reason). Thebelieve_mehere is unavoidable without an Idris2 reflective tactic formod.Honest reclassification
This issue's pattern-match-to-proven#107 was too aggressive. The proven-side discharges were genuinely one-liners (literal
Reflonpublic exportsmart constructors). The absolute-zero candidates here are all real proof work — either:Recommendation
Refs proven#107 proven#119 (sister analysis)