pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation

show as:
view Lean formalization →

The TauStepDerivation module computes the leading face-count term for the tau lepton step coefficient on the Recognition Science phi-ladder. It supplies auxiliary definitions and equality statements that anchor the third-generation rung to the cubic ledger geometry. Lepton mass modelers cite it to fix the tau contribution in the yardstick mass formula. The module structure consists of imports from Constants and AlphaDerivation followed by targeted definitions and direct matching statements.

claimThe leading face-count term yields the tau step coefficient $c_τ$ satisfying the paper value, together with the mu-tau step relation $Δ_{μτ}$ in the lepton mass ladder.

background

The module sits inside the lepton generations sector and imports the RS time quantum τ₀ = 1 tick together with the alpha derivation from the cubic ledger. The upstream alpha module supplies the structural 4π factor obtained from Gauss-Bonnet applied to vertex deficits of the Q₃ lattice. Local definitions introduce the face-count leading term, auxiliary weight and dimension quantities, and the explicit coefficient and step objects used in the phi-ladder mass formula.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the tau rung coefficient required by the Recognition Science mass formula yardstick · ϕ^(rung-8+gap(Z)). It completes the third lepton generation in the eight-tick octave structure and feeds the T8 D=3 spatial dimension and RCL composition law into higher fermion hierarchy results.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)