module module moderate

`IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity`

The TauStepExclusivity module presents D/2 as the leading candidate formula for the tau lepton step correction within Recognition Science. Physicists deriving lepton masses from cube geometry would cite it when tracing dimension-dependent adjustments. The module organizes definitions for fractional corrections such as D/2, F/4 and E/8 drawn from the imported cubic ledger structure.

claimCandidate formula $\Delta(D) = D/2$ for the tau step correction, with related definitions for corrections at $D/2$, $F/4$, $E/8$ and their evaluations at dimension 3.

background

The module sits inside the lepton generations development and imports the RS time quantum $\tau_0 = 1$ tick together with the AlphaDerivation module that obtains $\alpha^{-1}$ from vertex deficits of the cubic ledger $Q_3$ via Gauss-Bonnet. Sibling definitions correction_D_half, correction_F_quarter, D_half_at_3 and F_quarter_eq_D_half supply the concrete correction terms and their dimension-3 specializations. The local setting is therefore the geometry of the cubic ledger before any mass calibration occurs.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the candidate formula that feeds directly into TauStepDeltaDerivation, whose goal is to show $\Delta(3) = 3/2$ is forced by cube geometry without empirical fitting. It therefore occupies the position of Candidate 1 inside the first-principles derivation of the dimension-dependent correction $\Delta(D) = D/2$.

scope and limits

Does not derive any correction formula from first principles.
Does not compare candidate values to measured tau mass.
Does not treat electron or muon generations.
Does not invoke the Recognition Composition Law or phi-ladder.

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