electron_charge
plain-language theorem explainer
Electron charge is assigned the integer value -1 in units of the elementary charge e. Researchers assembling lepton masses on the phi-ladder cite this constant when building the sector yardstick from cube geometry. The assignment is a direct definition with no lemmas or reductions applied.
Claim. The electron charge is defined by the assignment $q = -1$ in units of the elementary charge $e$.
background
This module isolates core definitions for the electron mass derivation to break import cycles. Lepton sector constants follow from D = 3 cube geometry: the 3-cube supplies 12 edges, one active edge per atomic tick leaves 11 passive field edges, the binary exponent B equals -22, and the phi-offset r0 equals 62. The yardstick is then Y = 2^B · E_coh · φ^R0 with the electron baseline rung r_e = 2. Upstream, Mass is the type of real numbers and Sector is the inductive type with constructors Lepton, UpQuark, DownQuark, Electroweak.
proof idea
The definition is a direct constant assignment of the integer -1. No lemmas from the depends_on list are invoked; the body is the literal value.
why it matters
The definition supplies the charge sign required by the lepton mass formula in the T9 chain. It is referenced by the matching definition in IndisputableMonolith.RRF.Physics.ElectronMass.Defs. The placement records the forced lepton rung r_e = 2 that follows from the eight-tick octave and wallpaper-group count 17. It closes one link in the derivation from cube geometry to the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.