lepton_baseline_matches_anchor
plain-language theorem explainer
Lepton baseline rung derived from 3-cube face combinatorics equals the anchored electron rung value. Mass ladder calculations cite this equality to fix the lepton starting rung before phi-exponent scaling. The term proof reduces directly by unfolding the baseline definition together with the active-edges constant.
Claim. The lepton baseline rung given by active edges plus one equals the electron rung value $r_ {lepton}(e)$ from the integer anchor.
background
This module upgrades boundary assumptions to derived status by deriving baseline rung integers from the combinatorics of the 3-cube Q₃. Lepton baseline (B-11) is listed as A + 1 with value 2, where A is the active-edges count per tick. The derivation principle states that every integer traces to a single input: D = 3 from the unified forcing chain.
proof idea
One-line wrapper that applies the simp tactic to unfold lepton_baseline, active_edges_per_tick, and the lepton rung function.
why it matters
This theorem completes the B-11 consistency check in the baseline rung derivations, confirming the lepton starting point matches the anchor. It supports the Recognition mass formula by fixing the rung offset for leptons before phi-ladder application. The result relies on D = 3 (T8) and the cube-face edge count 2^(D-1) for related quark and color offsets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.