module module high

`IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity`

The Necessity module in LeptonGenerations establishes that E_passive equals exactly 11 in RS-native units together with exact local bounds on pi and generation step functions. Researchers closing the lepton mass derivation from cube geometry cite these results to confirm the necessity of the observed generations. The module organizes a collection of exactness theorems that apply interval arithmetic and prior necessity lemmas from the electron mass chain.

claim$E_{\rm passive}=11$ (exact), with local bounds $\pi>d_6$, step functions from $e$ to $\mu$ and $\mu$ to $\tau$, and predicted residues for the muon and tau.

background

This module sits inside the RRF lepton generations necessity chain that follows the electron mass definitions. Lepton sector constants are derived from cube geometry rather than chosen arbitrarily. Upstream AlphaDerivation states: 'This module provides a complete, constructive derivation of the fine-structure constant α⁻¹ from the geometry of the cubic ledger.' PhiSupport supplies the relation φ² = φ + 1, while Numerics.Interval.Pow supplies rigorous bounds via the identity x^y = exp(y log x). The setting is the forcing chain T0-T8 with D=3 and the Recognition Composition Law.

proof idea

The module collects separate exactness theorems. Each applies interval power bounds from Numerics.Interval.Pow together with algebraic reductions from AlphaDerivation and PhiSupport to obtain the stated equalities and inequalities.

why it matters in Recognition Science

The module supplies the exact passive energy value required by the lepton mass formula on the phi-ladder. It feeds the necessity argument for three lepton generations in the RRF framework. The central result E_passive = 11 closes the passive energy sector of the derivation chain from first principles.

scope and limits

Does not derive the numerical values of the muon or tau masses.
Does not address quark generations or mixing angles.
Does not supply experimental falsification criteria beyond the exact E_passive claim.
Does not extend the necessity argument outside the lepton sector.

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