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 extending T9 electron mass results to T10 muon and tau masses cite this when constructing the full fermion spectrum from cube geometry. The argument assembles the base rung from electron linking, adds the E_p=11 and cube-face=6 increments, then verifies uniqueness through residue classes modulo 8.

claimThe lepton ladder rungs $r_1=2$, $r_2=13=2+11$, $r_3=19=13+6$ are the unique stable solutions for the three-generation torsion constraint in $D=3$, with residues classes modulo 8 given by the set {2,5,3} that label the three distinct directions of the cubic voxel.

background

This module belongs to the lepton sector of Recognition Science and sits downstream of the T9 electron mass definitions. It imports the core constants, the golden-ratio relation φ²=φ+1, interval arithmetic for power bounds, and the electron-mass necessity results that derive lepton constants from cube geometry. The AlphaDerivation module supplies the 4π term obtained from Gauss-Bonnet on vertex deficits of the cubic ledger Q₃.

proof idea

The module organises its argument into sibling theorems. lepton_rungs_forced assembles the base rung from T9 linking and applies the fixed increments E_p and cube faces. lepton_residues_distinct and lepton_rungs_unique establish that the resulting positions occupy distinct classes modulo 8. is_stable_lepton_ladder and torsion_minimality_forced close the torsion constraint using the eight-tick octave and D=3. The remaining lemmas verify exact equalities for E, cube faces, W and local bounds on π.

why it matters in Recognition Science

The module supplies the forced rung positions required by the T10 lepton-generations derivation and by the unified hierarchy module. It thereby completes the necessity half of the three-generation model inside the Recognition forcing chain, directly using T7 (eight-tick octave) and T8 (D=3) together with the cubic-voxel geometry. The result is imported by ParticleSummary and the RRF lepton module.

scope and limits

Does not derive numerical mass ratios for the muon or tau.
Does not treat quark sectors or quarter-ladder coordinates.
Does not address dynamical stability or decay widths.
Does not incorporate higher-order radiative corrections.

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