IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
This module derives the leading coefficient for the tau step in the lepton mass ladder of Recognition Science. It supplies explicit definitions and equality checks for the third-generation transition coefficient using the imported RS constants and alpha geometry. The structure consists of named definitions followed by direct equality lemmas that match external paper values.
claimThe derived coefficient for the tau step on the phi-ladder together with its equality to the explicit algebraic form and the matching statement for the muon-tau step transition.
background
The module sits inside the lepton-generations development and imports the base RS time quantum τ₀ = 1 tick together with the alpha derivation that obtains 4π from vertex deficits of the cubic ledger. Sibling definitions introduce F, W, dim and the explicit tauStepCoefficientDerived object whose value is fixed by the phi-ladder rung arithmetic. The local setting is the mass formula yardstick · phi^(rung - 8 + gap(Z)) applied to the third lepton generation.
proof idea
This is a definition module whose argument consists of direct definitions of the coefficient and the step transition followed by equality lemmas that reduce to the imported constants; no complex tactic chains are required.
why it matters in Recognition Science
The module supplies the concrete tau coefficient required by any parent derivation of the full lepton mass spectrum. It closes the third-generation case in the chain that begins from the J-uniqueness fixed point and the eight-tick octave, feeding forward to higher-level statements on generational mass ratios.
scope and limits
- Does not derive the electron or muon coefficients.
- Does not contain the full three-generation mass spectrum theorem.
- Does not address mixing angles or decay widths.