module module high

`IndisputableMonolith.Physics.LeptonGenerations.Necessity`

The Necessity module proves the lepton ladder rungs at 2, 13 and 19 are the unique stable solutions to the three-generation torsion constraint in D=3. Researchers deriving Standard Model spectra from first principles cite it to extend the T9 electron mass to muon and tau via the phi-ladder. The argument composes the base rung with the E-passive increment of 11 and the cube-face increment of 6, confirming uniqueness through residue classes modulo 8.

claimThe unique stable solutions to the three-generation torsion constraint in $D=3$ are the lepton rungs $r_1=2$, $r_2=13$, $r_3=19$, corresponding to the residue classes $\{2,5,3\} \pmod{8}$ that label the three distinct directions of the cubic voxel.

background

This module belongs to the lepton sector of Recognition Science, which derives all constants from the J-functional equation and the phi-ladder after the T0-T8 forcing chain fixes $D=3$ and the eight-tick octave. It imports the electron mass definitions (T9) that place the base rung at 2 and the lepton generation definitions that encode the torsion constraint. Upstream, AlphaDerivation supplies the 4π factor from Gauss-Bonnet on the cubic vertex deficits, while PhiSupport encodes the relation $\phi^2=\phi+1$.

proof idea

The module organises its argument by first fixing the electron base rung from ElectronMass.Necessity, then applying the forced E-passive step of 11 and the cube-face step of 6 derived from cubic geometry. Uniqueness follows from verifying that the resulting residues modulo 8 are distinct and exhaust the three independent directions of the voxel; torsion minimality is checked via the sibling declarations lepton_rungs_unique and torsion_minimality_forced.

why it matters in Recognition Science

The module supplies the rung positions required by the T10 lepton generations module and the unified hierarchy in Physics.Hierarchy. It closes the parameter-free chain from the cubic ledger to the three lepton masses, consistent with the alpha band and the RS-native constants $c=1$, $\hbar=\phi^{-5}$. Downstream ParticleSummary and RRF.Physics.LeptonGenerations import these rungs to assemble the full fermion spectrum.

scope and limits

Does not derive numerical mass values or decay rates.
Does not address the quark sector or mixing angles.
Does not incorporate neutrino masses or oscillations.
Does not relax the integer-rung restriction of the core model.
Does not treat experimental inputs or fitting procedures.

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.Hierarchy module_import
IndisputableMonolith.Physics.LeptonGenerations module_import
IndisputableMonolith.Physics.ParticleSummary module_import
IndisputableMonolith.RRF.Physics.LeptonGenerations module_import

depends on (9)

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
IndisputableMonolith.RSBridge.GapProperties module_import

declarations in this module (110)

theorem lepton_rungs_forced L59
theorem lepton_residues_distinct L71
def is_stable_lepton_ladder L89
theorem lepton_rungs_unique L101
structure LeptonTorsionCert L130
theorem lepton_torsion_verified L138
theorem torsion_minimality_forced L152
lemma E_passive_exact L165
lemma cube_faces_exact L170
lemma W_exact L175
lemma pi_gt_d6_local L180
lemma pi_lt_d6_local L183
lemma inv_4pi_lower L186
lemma inv_4pi_upper L198
lemma inv_4pi_bounds L209
lemma step_e_mu_bounds L214
lemma step_mu_tau_bounds L223
lemma gap_minus_shift_bounds_proven L236
lemma predicted_residue_mu_bounds L244
lemma predicted_residue_tau_bounds L257
def phi_pow_neg963_lower_hypothesis L276
def phi_pow_neg962_upper_hypothesis L280
lemma exp_four_upper L285
lemma exp_four_lower L296
def exp_taylor_10_at_081416924 L309
def exp_error_10_at_081416924 L313
lemma exp_081416924_upper_q L317
lemma exp_081416924_upper L321
def exp_taylor_10_at_080454125 L343
def exp_error_10_at_080454125 L347
lemma exp_080454125_lower_q L351
lemma exp_080454125_lower L355
def exp_taylor_10_at_063407156 L380
def exp_error_10_at_063407156 L384
lemma exp_063407156_upper_q L388
lemma exp_063407156_upper L392
def exp_taylor_10_at_062924882 L414
def exp_error_10_at_062924882 L418
lemma exp_062924882_lower_q L422
lemma exp_062924882_lower L426
lemma exp_181416924_upper L451
lemma exp_180454125_lower L464
lemma exp_463407156_upper L477
lemma exp_462924882_lower L490
theorem phi_pow_neg963_lower_proved L503
theorem phi_pow_neg962_upper_proved L529
theorem phi_pow_residue_mu_lower L555
theorem phi_pow_residue_mu_upper L570
lemma phi_pow_residue_mu_bounds L583
def phi_pow_neg377_lower_hypothesis L594
def phi_pow_neg375_upper_hypothesis L598
theorem phi_pow_neg377_lower_proved L601
theorem phi_pow_neg375_upper_proved L627
theorem phi_pow_residue_tau_lower L653
theorem phi_pow_residue_tau_upper L665
lemma phi_pow_residue_tau_bounds L678
theorem predicted_mass_mu_lower L690
theorem predicted_mass_mu_upper L698
theorem muon_mass_pred_bounds_proven L710
theorem predicted_mass_mu_lower_tight L716
theorem predicted_mass_mu_upper_tight L725
theorem muon_mass_pred_bounds_tight L735
theorem predicted_mass_tau_lower L746
theorem predicted_mass_tau_upper L754
theorem tau_mass_pred_bounds_proven L766
theorem predicted_mass_tau_lower_tight L772
theorem predicted_mass_tau_upper_tight L781
theorem tau_mass_pred_bounds_tight L791
theorem lepton_ladder_forced_from_T9 L812
lemma inv_4pi_lower_v2 L863
lemma inv_4pi_upper_v2 L871
lemma step_e_mu_bounds_v2 L879
lemma step_mu_tau_bounds_v2 L886
lemma predicted_residue_mu_bounds_v2 L891
lemma predicted_residue_tau_bounds_v2 L898
def exp_taylor_v2_1 L915
def exp_error_v2_1 L918
lemma exp_v2_1_q L921
lemma exp_06327_upper L922
def exp_taylor_v2_2 L944

… and 30 more