electron_charge
plain-language theorem explainer
Electron charge is assigned the integer value -1 in units of the elementary charge. Researchers deriving lepton structural masses in the RRF sector cite this constant when building the yardstick and rung formulas. The assignment is a direct constant definition introduced to isolate primitives from theorems and break import cycles.
Claim. The electron charge satisfies $q = -1$ in units of the elementary charge $e$.
background
This definition sits in the T9 Electron Mass Definitions module, which isolates core constants from theorems to avoid import cycles. Upstream, Mass is the type of real numbers and Sector is an inductive type with constructors including Lepton. The module imports RSNativeUnits, PhiSupport, and multiple Anchor definitions that map sectors to rung parameters.
proof idea
Direct definition that assigns the integer literal -1 with no lemmas or tactics applied.
why it matters
The constant supplies the charge sign for the lepton sector in the structural mass formula Y = 2^B · E_coh · φ^R0. It feeds the downstream electron_structural_mass and predicted_electron_mass definitions inside the same module. The placement supports the T9 electron mass derivation while keeping the phi-ladder mass formula free of circular imports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.