module module high

`IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity`

The module establishes necessity results for lepton generations in the RRF sector of Recognition Science, with the central claim that E_passive equals 11 exactly. Researchers deriving muon and tau masses from cube geometry and the phi ladder would cite these statements. The module assembles the results by importing alpha derivation, electron mass necessity, and interval power bounds rather than proving new lemmas internally.

claim$E_{\rm passive}=11$ exactly, together with exact statements for cube faces, $W$, and interval bounds on the electron-muon and muon-tau steps.

background

The module sits inside the RRF Physics LeptonGenerations section and imports nine supporting modules. Key upstream results include the derivation of $\alpha^{-1}$ from vertex deficits of the cubic ledger (AlphaDerivation), the relation $\phi^2=\phi+1$ (PhiSupport), the fundamental time quantum $\tau_0=1$ tick (Constants), and the separation of lepton-sector definitions from theorems to avoid import cycles (ElectronMass.Defs). The local theoretical setting treats lepton constants as forced by cube geometry rather than free parameters.

proof idea

This is a definition module with supporting exact statements; the argument assembles E_passive_exact and related bounds from the imported alpha, electron-mass, and interval-arithmetic modules without internal tactic scripts or new reductions.

why it matters in Recognition Science

The module supplies the exact value E_passive=11 required by the phi-ladder mass formula and the Z_cf threshold near phi^5. It feeds the lepton-generation predictions that close the T5-T8 forcing chain and supplies the input needed for residue bounds on the muon and tau. The doc-comment flags the central claim as E_passive=11 (exact).

scope and limits

Does not derive numerical lepton masses.
Does not address neutrino sector.
Does not construct the full RRF action.
Does not prove uniqueness of three generations.

depends on (8)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.Numerics.Interval.Pow module_import
IndisputableMonolith.PhiSupport module_import
IndisputableMonolith.Physics.ElectronMass.Defs module_import
IndisputableMonolith.Physics.ElectronMass.Necessity module_import
IndisputableMonolith.Physics.LeptonGenerations.Defs module_import

declarations in this module (29)

lemma E_passive_exact L51
lemma cube_faces_exact L56
lemma W_exact L61
lemma pi_gt_d6_local L66
lemma pi_lt_d6_local L69
lemma inv_4pi_lower L72
lemma inv_4pi_upper L84
lemma inv_4pi_bounds L95
lemma step_e_mu_bounds L100
lemma step_mu_tau_bounds L109
lemma predicted_residue_mu_bounds L122
lemma predicted_residue_tau_bounds L132
theorem phi_pow_neg963_lower L151
theorem phi_pow_neg962_upper L157
theorem phi_pow_residue_mu_lower L162
theorem phi_pow_residue_mu_upper L175
lemma phi_pow_residue_mu_bounds L186
theorem phi_pow_neg377_lower L196
theorem phi_pow_neg375_upper L202
theorem phi_pow_residue_tau_lower L207
theorem phi_pow_residue_tau_upper L217
lemma phi_pow_residue_tau_bounds L228
theorem predicted_mass_mu_lower L239
theorem predicted_mass_mu_upper L246
theorem muon_mass_pred_bounds_proven L257
theorem predicted_mass_tau_lower L268
theorem predicted_mass_tau_upper L275
theorem tau_mass_pred_bounds_proven L286
theorem lepton_ladder_forced_from_T9 L307