pith. sign in
module module high

IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation

show as:
view Lean formalization →

The FractionalStepDerivation module computes solid angle fractions and edge counts that fix the generation step for leptons from the cubic ledger geometry. Researchers working on Recognition Science particle spectra would cite these to link D=3 geometry to the alpha band and phi-ladder masses. The module proceeds by direct definitions of total and fractional solid angles together with passive and active edge counts, instantiated from the upstream 4π result.

claimIn $D=3$ the total solid angle is $\Omega=4\pi$ steradians. The fractional solid angle $\Omega_{frac}$, passive edge count $n_{passive}$, active edge count $n_{active}$, alpha seed $\alpha_{seed}$, and derived generation step $\Delta_{gen}$ satisfy the listed equalities.

background

The module sits inside the Recognition Science derivation of physics from the single functional equation, where T7 forces the eight-tick octave and T8 forces $D=3$. It imports the RS time quantum $\tau_0=1$ tick and the AlphaDerivation module whose doc-comment states: 'This module provides a complete, constructive derivation of the fine-structure constant $\alpha^{-1}$ from the geometry of the cubic ledger' together with the clause '4π from Gauss-Bonnet: Structural derivation via vertex deficits of Q₃'. Definitions introduced cover totalSolidAngle as the sphere surface measure, fractionalSolidAngle as its portion, passiveEdgeCount and activeEdgeCount for ledger edges, alphaSeed, and generationStepDerived.

proof idea

This is a definition module, no proofs. The structure consists of successive definitions for the solid angle quantities and edge counts, followed by equality lemmas that verify the relations to the alpha seed and generation step.

why it matters in Recognition Science

This module supplies the fractional step derivation that feeds the lepton generations structure. It connects the geometric 4π result to the alpha seed and the generationStepDerived quantity on the phi-ladder, supporting the T8 forcing of D=3 and the alpha band (137.030, 137.039). No downstream theorems are listed, indicating it is a foundational block for higher-level particle derivations.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)