match_lepton_e
plain-language theorem explainer
The legacy rung constructor assigns rung value 2 to the electron fermion. Researchers checking lepton mass assignments on the phi-ladder would cite this verification. The proof is immediate reflexivity on the definition of the rung constructor for the electron case.
Claim. The legacy rung constructor applied to the electron fermion yields rung value 2.
background
The legacy rung constructor is defined as a function on particle species that returns an integer rung index. For fermions it extracts the sector and generation index, then applies a universal torsion pattern {0,11,17} for all charged particles. The supplied doc-comment states it is correct for leptons and neutrinos while quarks require a separate constructor. This theorem sits in the Masses.RungConstructor.Proofs module whose purpose is to confirm that the constructor reproduces the charged lepton table.
proof idea
One-line wrapper that applies reflexivity directly to the definition of the legacy rung constructor on the electron fermion case.
why it matters
The result verifies the rung assignment for the electron as part of reproducing the charged lepton table. It supports the Recognition Science mass formula that places particles on the phi-ladder via rung - 8 + gap(Z). No downstream theorems depend on it, so it functions as a table-verification step rather than a lemma for further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.