L-COQ-SWEEP-CLARA-4: close 4 Admitted in trinity-clara proofs/igla/

[gHashTag]

Mission

Sibling lane to gHashTag/trios#586 (L-COQ-SWEEP-13). This lane closes the 4 Admitted lemmas attributed to trinity-clara in the live Coq dashboard inventory:

File	Admitted (per dashboard)	Notes
proofs/igla/lr_convergence.v	1	uncovered_gap
proofs/igla/lucas_closure_gf16.v	1	uncovered_gap (already PROVEN per in-file header — verify)
proofs/igla/rainbow_bridge_consistency.v	2	covered as at_least_once_delivery_probabilistic + no_split_brain_probabilistic (probabilistic Admitted, see file lines 261, 280) — needs Pmf / Coquelicot infrastructure

Honesty rules

• This lane is scope-only — opened by the L-COQ-SWEEP-13 lane (trios#586) for traceability. Implementation deferred to a contributor with a working coqc + Coquelicot environment.
• If any of the 4 lemmas are already discovered to be Qed-closed on main (analogous to the trios audit drift in #586), close this lane with an audit comment instead of attempting fake closure.
• Placeholder Rust witness tests are NOT in trinity-clara's scope (no Rust workspace there). Documentation-only placeholders allowed.

Acceptance (R7-honest)

• L1 — audit each of the 4 files on trinity-clara main and report actual Admitted. count vs dashboard's claim
• L2 — for each truly-Admitted lemma, attempt real proof; if blocked on infrastructure (e.g. Coquelicot probability), document blocker and defer
• L3 — open follow-up trinity-clara issues for any deferred lemma with concrete blocker
• L4 — update trios dashboard inventory in a separate PR once trinity-clara closures land

Cross-references

• L-COQ-SWEEP-13: close 13 trios Admitted (Rehearsal #2 gate, placeholders allowed) trios#586 — sibling sweep lane
• L-COQ-WITNESS-TODO: runtime-witness implementation tracking trios#587 — runtime-witness umbrella tracker

Anchor

phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877