module module high

`IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity`

The TauStepExclusivity module presents D/2 as the candidate formula for the dimension-dependent correction in tau lepton steps. Researchers deriving lepton masses from Recognition Science geometry cite it when selecting among correction variants. The module consists of definitions for half, quarter and eighth corrections together with equality and exclusivity lemmas among them.

claimThe candidate correction is $\Delta(D) = D/2$, supported by auxiliary definitions correction_D_half, correction_F_quarter, correction_E_eighth and lemmas F_quarter_eq_D_half, F_quarter_not_alternative evaluated at dimension 3.

background

Recognition Science fixes the fundamental time quantum at $\tau_0 = 1$ tick. The imported AlphaDerivation module constructs $\alpha^{-1}$ from the geometry of the cubic ledger $Q_3$, including the structural derivation of $4\pi$ via Gauss-Bonnet on vertex deficits. This module introduces correction terms at dimension 3 for D, F and E and the relations that select the D/2 form.

proof idea

This is a definition module, no proofs. It defines the family of correction functions and states the equality and non-alternative lemmas among the listed sibling declarations.

why it matters in Recognition Science

The module supplies the candidate formula and exclusivity arguments that feed into TauStepDeltaDerivation, whose goal is to derive $\Delta(D) = D/2$ from cube geometry without calibration and to show that $\Delta(3) = 3/2$ is forced by the framework.

scope and limits

Does not derive the correction from the forcing chain or RCL.
Does not calibrate any term to observed lepton masses.
Does not compute numerical mass values for any generation.
Does not address electron or muon steps.

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