lepton_rungs
plain-language theorem explainer
The theorem fixes the lepton baseline rung at 2 and shows that this value plus the count of passive field edges at D=3 equals 13 while the same baseline plus the number of wallpaper groups equals 19. Mass derivations in the Recognition framework cite these integers to locate the electron, muon, and tau on the phi-ladder. The proof unfolds the baseline definition once and dispatches the three arithmetic checks by native decision.
Claim. Let $r$ be the lepton baseline rung. Then $r=2$, $r + p=13$ where $p$ is the number of passive field edges in three dimensions, and $r + w=19$ where $w$ is the number of wallpaper groups.
background
The module derives rung integers directly from the combinatorics of the 3-cube once D=3 is fixed. lepton_baseline is defined as active_edges_per_tick plus one, which evaluates to 2. passive_field_edges(d) subtracts the active edges per tick from the total cube edges; its value at D=3 is 11. wallpaper_groups is the crystallographic constant 17. These three quantities appear in the table of derived items B-11, B-13, and B-14. The upstream passive_field_edges definition states that these edges dress the interaction, while the wallpaper_groups definition records the Fedorov count used for curvature normalization.
proof idea
The term proof unfolds the definition of lepton_baseline, then applies constructor to split the conjunction into three goals. Each goal is discharged by a single native_decide tactic that evaluates the concrete natural-number arithmetic.
why it matters
This result supplies the three lepton rung values that feed the derived_parameters record and the SMDerivation structure in ParticleSummary. It closes the B-11 entry in the cube-geometry derivation table, replacing a former boundary assumption with a direct consequence of D=3. The same D=3 input also fixes the octave offset at -8 and the neutrino baseline at -54, completing the rung ladder used for mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.