module module high

`IndisputableMonolith.Physics.LeptonGenerations.Necessity`

Lepton rungs at positions 2, 13 and 19 solve the three-generation torsion constraint uniquely in three dimensions. A physicist building discrete mass spectra from cube geometry would cite the result to anchor the muon and tau on the phi-ladder. The argument links the electron base rung via T9, then adds the passive E increment of 11 and the six face steps of the cubic voxel.

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$, with residues $\{2,5,3\}$ modulo 8 that label the three directions of the cubic voxel.

background

Recognition Science fixes $D=3$ via the eight-tick octave and derives masses from the phi-ladder whose rung positions are set by geometric increments in the cubic ledger. Electron mass definitions fix the base rung at 2; lepton generation definitions introduce the torsion constraint. Upstream results include the alpha derivation from vertex deficits of the cubic ledger and the identity $\phi^2=\phi+1$.

proof idea

The module chains the electron mass necessity result with the distinct residue classes and the unique ladder property. It invokes the torsion minimality lemma together with the exact relations for passive E, cube faces and W. Sibling results on the stable lepton ladder and torsion verification close the forcing argument.

why it matters in Recognition Science

The module feeds the rung positions into the unified generation hierarchy and the T10 lepton generations derivation. It supplies the structural input required by the particle summary for matching the three lepton masses. The doc comment identifies the result as the theorem that lepton rungs are forced by the cubic voxel geometry in $D=3$.

scope and limits

Does not extend the rung construction to quarks or other sectors.
Does not compute explicit mass ratios beyond rung positions.
Does not relax the $D=3$ assumption or the torsion constraint.
Does not address numerical stability outside the phi-ladder.

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