fix(coq): L-LEP-FALSIFY — close 8 Admitted in Bounds_LeptonMasses.v

[gHashTag]

L-LEP-FALSIFY — close 8 Admitted in Bounds_LeptonMasses.v

Lane: L-LEP-FALSIFY (#554)
Author: Dmitrii Vasilev admin@t27.ai
Anchor: φ² + φ⁻² = 3 · DOI 10.5281/zenodo.19227877

Summary

Closes 8 Admitted. in docs/phd/theorems/trinity/Bounds_LeptonMasses.v:
6 R8 falsifiers (L01/L02/L03 within-tolerance + monomial-form) + 2 proven identities
(phi_seventh, lepton_mass_chain_relation).

Net Admitted delta on main: −8.

Falsified candidate formulas (R8 witness)

PDG 2024 hard targets, tolerance_V = 0.01 (0.1% mass-ratio tolerance):

Lemma	Candidate	Numeric	PDG	Rel err
L01_falsified_by_PDG	4·φ³/e²	2.2932	206.7682830	0.989
L02_falsified_by_PDG	2·φ⁴·π/e	15.8429	16.8167	0.0570
L03_falsified_by_PDG	8·φ⁷·π/e³	36.3304	3477.23	0.9896

Each falsifier discharged by interval with (i_bisect, i_bits) after unfolding phi.

The corresponding *_within_tolerance and *_monomial_form theorems are then
the negation of those bounds, discharged by lra from the falsifier hypothesis.

These three candidate monomials are NOT correct lepton-mass formulas. They
remain in the file as historical record + machine-checked falsification witness
(R8: every formula in trinity must either be proven within tolerance OR carry a
formal falsification certificate).

Proven identities (Qed)

• phi_seventh : phi^7 = (29 + 13 * sqrt 5) / 2
  Queen ruling issuecomment-4406570574: the
  earlier claim phi^7 = 13 * sqrt 5 + 29 was off by factor 2. Corrected via
  Binet phi^7 = phi^4 * phi^3 chain, reduced by field_simplify +
  Rsqr_pow2 + the helper Hsq5 : sqrt 5 * sqrt 5 = 5 (from sqrt_def).
• lepton_mass_chain_relation : L01_theoretical * L02_theoretical = L03_theoretical
  Exact algebra independent of any candidate-formula match to experiment;
  field after assert (He : exp 1 <> 0) by (apply Rgt_not_eq, exp_pos).

File-level verification

$ wc -l docs/phd/theorems/trinity/Bounds_LeptonMasses.v
209
$ grep -nE '^\s*Admitted\.' docs/phd/theorems/trinity/Bounds_LeptonMasses.v
(0 matches)

R-rule compliance

• R1 (Coq-only): every Qed is checked by Coq, no informal arguments.
• R3 (PR-only): no force-push, no --admin, awaiting queen-merge.
• R5 (honest): all 8 closures are Qed — none is paper-over. Falsifiers are
  honest negative results, not converted to fake proofs.
• R7 (witness): every theorem has an explicit closing tactic chain.
• R8 (falsification witness): the three within-tolerance theorems carry
  numeric falsification certificates against PDG 2024 reference values.
• R10 (atomic): single-file commit, no incidental changes.

DoD checklist

• 0 Admitted. in Bounds_LeptonMasses.v
• All theorems Qed (no Abort., no Admitted.)
• phi_seventh corrected per queen ruling 4406570574
• lepton_mass_chain_relation proven by exact algebra
• R8 numeric witnesses (L01/L02/L03 falsifiers) tied to PDG 2024 values
• Author = Dmitrii Vasilev <admin@t27.ai> (verified via git log)
• CPU-only build, no GPU dependency
• Branch off 008cd6a8 (post-Wave-1 main HEAD)

Empire ledger projection

After this PR + Lane B (#559) → canonical Admitted moves toward 0 in
docs/phd/theorems/trinity/. Margin to Rehearsal #2 floor (30) preserved at +29.

Closes #554