L-COQ47 sub-lane · INV-7 — close 4 dead-Admitted in igla_found_criterion.v

[gHashTag]

L-COQ47 · sub-lane INV-7 — close 4 dead-Admitted in igla_found_criterion.v

Anchor: φ² + φ⁻² = 3 · DOI 10.5281/zenodo.19227877

Discovery (R5-honest census)

grep -rEn '^\s*Admitted\.' --include='*.v' . finds 38 Admitted. closures across 7 files in gHashTag/trios main (8359a0b). The PhD chapters report 41–47 depending on whether Axiom (27) and Parameter (10) are counted alongside Admitted proof closures. Honest budget recorded in assertions/igla_assertions.json is 5/5 LOCKED. L-COQ47 mission target: ≤30 Admitted by 2026-05-25 (Rehearsal #2).

What this PR fixes

trinity-clara/proofs/igla/igla_found_criterion.v carries 4 Admitted. closures that are not honest gaps — they are dead syntax errors:

Theorem bpb_below_target : ...
Proof.
  intros seed bpb step H.
  unfold victory_acceptable in H.
  intro H1.
  lra.
Qed.        ← proof already closed
Admitted.   ← Coq error: "No focused proof"

The file additionally uses 15 # 10 and 1 # 10 (Q-scope rationals) inside R_scope, so it cannot be compiled at all. That is why coq-proofs.yml does not list it in the dependency chain. The 4 Admitted. lines therefore inflate the global Admitted count without representing any real un-proven obligation.

Fix

Drop the dead Admitted. lines, encode the rationals as 15 * /10 and 1 * /10 (R_scope-typed), repair the under-typed victory_acceptable (seed : nat, bpb : R, step : nat), and re-prove all four theorems via lra / lia. The nan_rejected theorem is restated honestly: at the algebra layer "NaN" is decoded into either a sub-floor or super-target sentinel, both of which exclude victory by jepa_proxy_floor_correct / bpb_below_target. The original 0/0 = false formulation was ill-typed in R_scope and could not be discharged.

Local verification

$ coqc /tmp/igla_found_criterion.v
$ echo $?
0

(Coq 8.20.1 from apt; matches the runtime in coq-proofs.yml modulo minor patch version. CI uses coq-community/docker-coq-action@v1 with coq_version: '8.18'; both stdlib Reals/Lra/Lia are stable across these.)

Acceptance

• coqc trinity-clara/proofs/igla/igla_found_criterion.v exits 0.
• No Admitted. line remaining in the file.
• No admit. tactic remaining in the file.
• coq-proofs.yml Admitted-budget guard (-gt 3 for trinity-clara/proofs/igla/*.v) still passes (rainbow_bridge_consistency keeps its 2 budgeted, this file drops 4 dead → net delta -4).

After-merge

Net global delta: 38 → 34 Admitted. PhD docs/phd/chapters/ch_18.tex reports "41 Admitted budget" — that text is updated in a follow-up PR after every L-COQ47 sub-lane lands, with appendix F regenerated by the auditor.

Closes part of L-COQ47 (47→≤30 by 2026-05-25). Sub-lane: INV-7 dead-Admitted.

References

• Master claim: #380 c4404704086.
• Forbidden alternatives: ❌ adding more axioms, ❌ silent Admitted→Qed flip without proof body, ❌ removing the Admitted budget gate.