module module high

`IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity`

The TauStepExclusivity module presents D/2 as the candidate formula for the dimension-dependent correction in the tau step of lepton generations. Researchers deriving lepton masses from cube geometry would cite it when selecting among correction candidates. The module structures its case through definitions of multiple correction terms evaluated at D=3 together with equality and exclusion lemmas.

claimThe dimension-dependent correction takes the form $\Delta(D) = D/2$.

background

The module imports Constants, where $\tau_0 = 1$ tick is the fundamental RS time quantum, and AlphaDerivation, which derives $\alpha^{-1}$ from the geometry of the cubic ledger with the main result that $4\pi$ follows from Gauss-Bonnet via vertex deficits of $Q_3$. It introduces correction terms (D/2, F/4, E/8 and quadratic variants) together with their evaluations at $D=3$ and algebraic relations among them.

proof idea

The module is built from a collection of definitions (correction_D_half and siblings) plus lemmas that establish equalities such as F_quarter_eq_D_half and exclusions such as F_quarter_not_alternative. These relations are obtained by direct algebraic comparison of the correction expressions at $D=3$.

why it matters in Recognition Science

This module supplies the D/2 candidate that feeds the downstream TauStepDeltaDerivation, whose stated goal is to derive $\Delta(D) = D/2$ from cube geometry without calibration to observed masses and to show that $\Delta(3) = 3/2$ is forced. It therefore occupies the position of the claimed formula inside the lepton-generation correction chain.

scope and limits

Does not calibrate any correction coefficient to experimental lepton masses.
Does not derive the full three-generation mass spectrum.
Does not incorporate electromagnetic or weak interaction corrections.
Does not address steps beyond the tau generation.

used by (1)

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

IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (22)

def correction_D_half L65
def correction_F_quarter L68
def correction_E_eighth L71
def correction_D_quad1 L74
def correction_D_quad2 L77
theorem D_half_at_3 L81
theorem F_quarter_at_3 L85
theorem E_eighth_at_3 L90
theorem D_quad1_at_3 L95
theorem D_quad2_at_3 L99
theorem F_quarter_eq_D_half L107
theorem F_quarter_not_alternative L115
def AxisAdditive L123
theorem axisAdditive_linear L127
structure AdmissibleCorrection L150
theorem admissible_unique L155
theorem D_half_admissible L180
theorem F_quarter_admissible L188
theorem E_eighth_not_axisAdditive L197
theorem D_quad1_not_axisAdditive L208
theorem D_quad2_not_axisAdditive L216
theorem tau_correction_unique_admissible L226