lepton_baseline_eq
plain-language theorem explainer
Lepton baseline rung equals 2 because it is defined as one plus the single active edge per atomic tick. Researchers deriving lepton masses from Recognition Science geometry cite this to eliminate free parameters in the rung ladder. The proof unfolds the recursive definition and normalizes the resulting integer arithmetic.
Claim. $r_e = 2$ where the lepton baseline rung $r_e$ is defined by $r_e := A + 1$ and $A = 1$ is the number of active edges per atomic tick.
background
In the Recognition Science framework, active edges per atomic tick is defined as 1, reflecting exactly one edge transition per tick in the discrete ledger on the three-dimensional cube by T2 atomicity. The lepton baseline is then the active edge count plus one, positioning the minimal stable charged lepton one rung above the transition edge itself. This derivation module shows that the electron baseline rung follows directly from cube geometry without additional assumptions, as stated in the module documentation: 'The electron baseline rung is not a free parameter. It is derived from r_e = A + 1 = active_edges_per_tick + 1 = 1 + 1 = 2'. Upstream, the definition lepton_baseline := active_edges_per_tick + 1 is established in both the Masses and Physics.ElectronMass modules.
proof idea
This is a one-line wrapper proof. It unfolds the definitions of lepton_baseline and active_edges_per_tick to expose the expression 1 + 1, then applies norm_num to reduce it to the equality with 2.
why it matters
This theorem closes the baseline derivation for the electron in the Recognition Science mass ladder, feeding into the electron rung derived theorem and the neutrino baseline in the Masses module. It implements the T2 atomicity step from the forcing chain, fixing the starting point for the phi-ladder mass formula where masses scale as yardstick times phi to the power of (rung - 8 + gap). No open questions remain here as the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.