module module high

`IndisputableMonolith.Physics.LeptonGenerations.Necessity`

Module Necessity proves the lepton ladder positions 2, 13 and 19 are the unique stable solutions to the three-generation torsion constraint in D=3. Researchers deriving fermion spectra from Recognition Science cite it to fix the muon and tau rungs after the electron base. The argument chains the base rung from T9 electron necessity, then applies the E_p increment of 11 and the six cube-face steps.

claimThe rung positions $r_1=2$, $r_2=13$, $r_3=19$ are the unique stable solutions of the three-generation torsion constraint in three spatial dimensions, with residues $\{2,5,3\}$ modulo 8.

background

The module extends the T9 electron mass definitions and sits inside the lepton sector of Recognition Science. It imports the RS time quantum, the alpha derivation from cubic ledger geometry via Gauss-Bonnet, phi-support identities, and the electron mass necessity module. The local setting assumes the forcing chain through T8 (D=3) together with the Recognition Composition Law and the phi-ladder mass formula.

Upstream results supply the structural 4π derivation and interval bounds on powers. The doc-comment states the rungs correspond to the three unique directions of the cubic voxel.

proof idea

The module assembles necessity lemmas that first fix the base rung at 2 via the T9 electron link, then add the E_p step of 11 and the six cube-face increments. Uniqueness follows from residue-class distinctness modulo 8 and torsion-minimality constraints already established in the electron mass necessity module.

why it matters in Recognition Science

This module supplies the rung positions required by the unified generation hierarchy and by the T10 lepton generations formalization. It closes the parameter-free derivation of the three lepton masses from cube geometry and feeds directly into the particle summary. The doc-comment identifies the result as the T10 step after T9 electron linking.

scope and limits

Does not derive explicit numerical mass ratios.
Does not treat quark sectors or quarter-ladder steps.
Does not incorporate experimental mass values.
Does not address stability outside the torsion constraint.

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