electron_charge
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the charge value from the Recognition Composition Law.
- Does not specify electromagnetic coupling or fine-structure effects.
- Does not address fractional charges or non-lepton sectors.
- Does not connect to the alpha band or G = φ^5 / π constants.
formal statement (Lean)
38def electron_charge : ℤ := -1
proof body
Definition body.
39
40/-! ## Structural Mass Derivation -/
41
42/-- The Yardstick (Sector Scale): Y = 2^B · E_coh · φ^R0. -/