pith. sign in
module module high

IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation

show as:
view Lean formalization →

This module derives fractional steps for lepton generations by partitioning the 4π steradian solid angle into active and passive edge counts on the cubic lattice. Physicists constructing the phi-ladder mass formula for the electron-muon-tau sequence would cite these equalities when fixing the generation gap term. The module is a chain of definitions and direct equality lemmas that reduce solid-angle fractions to an alpha seed and a derived step value.

claimThe module establishes the total solid angle $4π$ steradians in $D=3$, defines the fractional solid angle, passive and active edge counts on the lattice, the alpha seed, and the derived generation step for leptons.

background

Recognition Science fixes $D=3$ spatial dimensions and obtains the total solid angle of $4π$ steradians directly from the geometry of the cubic ledger $Q_3$. The module imports the RS time quantum $τ_0=1$ tick from Constants and the alpha derivation that extracts $4π$ via Gauss-Bonnet vertex deficits on $Q_3$ (AlphaDerivation doc-comment). Sibling declarations introduce totalSolidAngle as the sphere surface measure, fractionalSolidAngle as its normalized portion, passiveEdgeCount and activeEdgeCount as the lattice edge partition, alphaSeed as the initial fine-structure seed, and generationStepDerived as the computed step separating lepton families.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the geometric fractions that close the lepton-generation derivation inside the Recognition framework, feeding the mass formula yardstick * phi^(rung - 8 + gap(Z)) and the Berry creation threshold phi^-1. It extends the upstream alpha derivation (4π from Gauss-Bonnet on Q_3) by converting solid-angle fractions into the generation step that distinguishes the three charged leptons. No downstream theorems are listed, indicating this block is an intermediate scaffold for the full lepton mass ladder.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)