active_edges_eq_one
plain-language theorem explainer
The theorem fixes the active edge count per atomic tick at exactly one, following from T2 atomicity in the discrete ledger on Q3. Researchers deriving the electron baseline rung or the phi-ladder mass formula would cite this to set r_e = 2 without free parameters. The proof is a direct reflexivity step on the definition of active_edges_per_tick.
Claim. The active edge count per fundamental tick satisfies $A = 1$, where $A$ counts the number of active edge transitions per atomic tick in the discrete ledger.
background
The Baseline Rung Derivation module obtains the electron baseline rung from the relation r_e = A + 1. Here A is the active edge count per tick, fixed at 1 by T2 atomicity: exactly one edge transition per tick in the discrete ledger on Q3. This value originates in the definition active_edges_per_tick := 1 from Constants.AlphaDerivation and is aliased as A in IntegrationGap and Masses.Anchor.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity to the definition of active_edges_per_tick as 1.
why it matters
This anchors the electron mass derivation by fixing the baseline rung at 2, which then supports sibling results such as baseline_matches_electron_rung and lepton_baseline_eq. It implements the T2 atomicity step from the forcing chain, ensuring the mass formula starts from a parameter-free rung for the electron. The result closes the atomicity interface without scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.