lepton_baseline
plain-language theorem explainer
The lepton baseline rung is obtained by adding one to the active edge count per atomic tick. Mass ladder derivations in Recognition Science cite this as the minimal rung for the electron. The definition follows directly from the active edge count fixed by T2 atomicity.
Claim. The lepton baseline rung $r$ satisfies $r = A + 1$, where $A$ is the number of active edges per atomic tick.
background
Recognition Science derives baseline rungs from the combinatorics of the 3-cube at spatial dimension D = 3. The active edges per tick equals 1, corresponding to one edge transition per tick under T2 atomicity. The lepton baseline is then the lowest rung for a charged lepton, one step above this active edge count, yielding the minimal stable state at rung 2.
proof idea
One-line definition that adds one to the active edges per tick value supplied by AlphaDerivation.
why it matters
This supplies the starting rung for all lepton mass derivations and is referenced by lepton_baseline_eq, lepton_rungs, and the electron rung theorems in ElectronMass.BaselineDerivation. It realizes item B-11 in the cube-geometry table, upgrading a prior boundary assumption to derived status from D = 3 and T2. The result anchors the lowest charged lepton on the phi-ladder before octave offsets and passive field edges are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.