electron_rung_derived
plain-language theorem explainer
The electron baseline rung derives as r_e = 2 from the active edge count A = 1 per atomic tick. Researchers modeling particle masses via discrete cube geometry cite this to anchor the electron scale without free parameters. The proof is a term that reduces the conjunction via reflexivity on the first two clauses and direct use of the lepton baseline equality lemma.
Claim. Let $A$ denote the number of active edges per atomic tick. Then $A = 1$ and the lepton baseline rung $r_e$ satisfies $r_e = A + 1 = 2$.
background
The module derives the electron baseline rung from cube geometry under T2 atomicity, which enforces exactly one edge transition per tick in a discrete ledger on Q_3. The active edges per tick is defined as the constant 1. The lepton baseline rung is then defined as one above the active edge count, because the minimal stable charged state must sit above the transition mechanism itself. Upstream results include the lepton_baseline definition and its equality theorem from Masses.BaselineDerivation, which already establishes the value 2 by unfolding and norm_num.
proof idea
The term proof constructs the three-way conjunction by applying reflexivity to the first two equalities and substituting the lepton_baseline_eq lemma for the third clause.
why it matters
This theorem completes the local derivation chain A = 1, r_e = A + 1 = 2, supplying the fixed rung that enters the mass formula yardstick * phi^(rung - 8 + gap(Z)). It directly instantiates the T2 atomicity step of the forcing chain and the cube-geometry baseline in the Recognition framework. No downstream uses are recorded yet, and the result carries no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.