lepton_baseline
plain-language theorem explainer
The lepton baseline rung fixes the electron starting position on the mass ladder at 2. Recognition Science mass derivations cite this to anchor the charged lepton spectrum from T2 atomicity without free parameters. It is obtained directly as one plus the active edge count per tick, which is set to 1.
Claim. The lepton baseline rung satisfies $r_e = A + 1$, where $A$ is the number of active edges per atomic tick from T2 atomicity.
background
Recognition Science derives the electron baseline from cube geometry on Q3. T2 atomicity requires exactly one edge transition per tick, so active edges per tick equals 1. The minimal stable charged state therefore sits one rung above the active edge itself, yielding rung 2. This definition in ElectronMass.BaselineDerivation matches the electron baseline rung in Defs and aligns with the general lepton baseline in Masses.BaselineDerivation.
proof idea
One-line definition that adds one to the value of active_edges_per_tick.
why it matters
This supplies the starting rung for all lepton mass calculations and feeds lepton_baseline_eq (which confirms the value 2), lepton_rungs (which relates it to passive edges and wallpaper groups), and electron_rung_derived. It realizes the B-11 derived baseline from cube geometry, consistent with the eight-tick octave and D=3 in the forcing chain. It closes the electron rung derivation without external parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.