pith. sign in
module module high

IndisputableMonolith.Physics.ElectronMass.BaselineDerivation

show as:
view Lean formalization →

This module defines the lepton baseline rung as one above the active edge count, fixing the minimal stable charged state at rung 2. It anchors electron mass derivations from the cubic ledger in Recognition Science. Researchers building the phi-ladder for leptons cite it to set the starting rung before applying the mass formula. The module consists of definitions and equalities that follow directly from the edge traversal requirement for charged states.

claimThe lepton baseline rung is $r = A + 1$, where the active edge count satisfies $A = 1$ for any charged state, placing the minimal stable rung at 2.

background

Recognition Science derives all constants from the geometry of the cubic ledger Q₃. The Constants module supplies the base time quantum τ₀ = 1 tick. AlphaDerivation constructs α⁻¹ from vertex deficits via the Gauss-Bonnet theorem on Q₃. ElectronMass.Defs separates core definitions to break import cycles and states that lepton sector constants arise directly from cube geometry rather than being arbitrary inputs.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the initial rung for the lepton mass ladder and feeds the T9 electron mass derivation chain, including results such as baseline_matches_electron_rung and electron_rung_derived. It anchors the minimal rung to the active edge count, connecting to the forcing chain landmarks T5–T8 and the Recognition Composition Law.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (5)