module module high

`IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity`

This module defines the tau step correction candidates in the Recognition Science lepton model, centering on the D/2 formula as the exclusive choice. It supplies half, quarter, and eighth order corrections derived from cubic ledger geometry and evaluates them at D=3. Physicists constructing first-principles lepton mass hierarchies cite it to fix the dimension-dependent adjustment without empirical fitting. The module consists of sequential correction definitions that establish exclusivity by direct comparison.

claim$Delta(D) = D/2$ is the exclusive tau-step correction, with auxiliary terms $D/2$, $F/4$, $E/8$ and their evaluations at $D=3$.

background

The Recognition Science framework sets the fundamental time quantum as $tau_0 = 1$ tick. The fine-structure constant $alpha^{-1}$ is derived from the geometry of the cubic ledger, with $4pi$ obtained via the Gauss-Bonnet theorem on vertex deficits. This module resides in the lepton generations section and introduces the correction functions for the tau step that depend on spatial dimension $D$.

proof idea

This is a definition module, no proofs. It declares the correction candidates and their specific values at three dimensions, establishing the formulas that support the subsequent delta derivation.

why it matters in Recognition Science

This module supplies the correction definitions that feed the TauStepDeltaDerivation. The downstream module derives $Delta(D) = D/2$ from cube geometry without calibration to observed masses and shows that $Delta(3) = 3/2$ is forced by the framework. It advances the first-principles lepton mass chain in Recognition Science.

scope and limits

Does not calibrate any correction to experimental mass values.
Does not address electron or muon generation steps.
Does not incorporate electromagnetic or quantum corrections beyond the cubic ledger.
Does not derive the complete lepton mass spectrum.

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