proof-debt: triage matches proven#107 overly-cautious-OWED pattern — 17 Coq axioms + 5 Idris believe_me's discharge candidates

[hyperpolymath]

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_pattern memory + reference_idris2_0_8_0_reduction_map memory

Owner decision: greenlight Phase 1 attempt, or defer?

[hyperpolymath]

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:

Candidate	Original verdict	Closer look
X_gate_not_identity	"Existence proof; exhibit `|0⟩` as witness"	Not tractable. `X_gate` is a Parameter (abstract), and |0⟩ isn't defined in the model. Would need to add a concrete X_gate definition + a basis_state model — architectural changes, not 30-min work.
hom_functor	"Should be a Definition, not an Axiom"	Not tractable. Source comments (CNOCategory.v L313-322) explicitly say "we leave this as an axiom" because the proper definition requires universe polymorphism and a SetCategory instance. The "DISCHARGE" classification was wrong — the axiom is intentional.
global_phase_unitary	"Derivable from gate algebra"	Not a one-liner. Needs full unitarity proof using `Cconj_Cexp` axiom + linearity of inner_product. Real Coq tactic work; tractable but multi-hour.
programStateAlignmentValid (Idris2)	"claim is computationally true; gap is the typechecker's" + literal n=8 mod 4	Genuine blocker. Empirically verified in /tmp/charrefl (per reference_idris2_0_8_0_reduction_map memory): mod on Nat literals does NOT reduce. Same family as proven#117 (closed for same reason). The believe_me here is unavoidable without an Idris2 reflective tactic for mod.

Honest reclassification

This issue's pattern-match-to-proven#107 was too aggressive. The proven-side discharges were genuinely one-liners (literal Refl on public export smart constructors). The absolute-zero candidates here are all real proof work — either:

1. Require model extensions (X_gate, hom_functor)
2. Need standard tactic proofs (global_phase_unitary)
3. Blocked by genuine Idris2 0.8.0 limitations (programStateAlignmentValid)

Recommendation

• Defer all 4 candidates pending either (a) Idris2 0.9.0 release (proven#119 Path A) or (b) a focused multi-hour session for the Coq side.
• Keep this issue open for tracking, but no immediate action items.
• Remaining 13 DISCHARGE-classified Coq axioms should be re-triaged similarly before committing time.

Refs proven#107 proven#119 (sister analysis)