lepton_baseline_eq
plain-language theorem explainer
The lepton baseline rung equals 2, obtained by adding one to the single active edge per atomic tick. Researchers deriving particle masses on the Recognition Science phi-ladder cite this result to fix the minimal charged lepton position from cube combinatorics at D=3. The proof is a direct unfolding of the definition followed by numerical simplification.
Claim. The lepton baseline rung satisfies $l_{baseline}=2$, where $l_{baseline}$ is the active edge count per tick plus one.
background
This module upgrades boundary assumptions to derived quantities by extracting rung integers from the combinatorics of the 3-cube at spatial dimension D=3. The lepton baseline is defined as active_edges_per_tick + 1, with active_edges_per_tick fixed at 1 as the single edge transition per atomic tick by T2. Upstream, the active_edges_per_tick definition appears in AlphaDerivation and is reused in the ElectronMass sibling module to anchor the minimal stable charged state.
proof idea
One-line wrapper that unfolds lepton_baseline and active_edges_per_tick then applies norm_num to reduce the expression to 1+1=2.
why it matters
This theorem establishes item B-11 as derived rather than assumed, supplying the lepton baseline value to neutrino_rung and electron_rung_derived. It anchors the lepton sector of the mass ladder at the Recognition Science phi-ladder starting point consistent with D=3 cube geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.