electronMassGeV
plain-language theorem explainer
The declaration supplies the accepted numerical value for the electron mass in GeV units inside the tau-gate hypothesis module. Workers checking phi-ladder rung assignments for the three lepton generations cite this constant when populating the LeptonGenerationRungs structure. It enters as a direct constant definition that matches the experimental figure without further computation.
Claim. The electron mass is defined by the constant assignment $m_e = 0.000511$ GeV.
background
The TauGate module states the explicit hypothesis that the tau lepton (rung 19) and molecular gate timescale (also rung 19) occupy the same position on the phi-ladder. The supplied definition furnishes the electron mass value required by the downstream LeptonGenerationRungs structure, which posits a common mass base together with integer rungs for the electron and muon. The local setting is the numerical testing of whether lepton masses align with the phi-ladder mass formula yardstick times phi to an integer power.
proof idea
One-line definition that directly binds the literal 0.000511 to the identifier electronMassGeV.
why it matters
The definition supplies the electron mass input to the LeptonGenerationRungs structure, which tests whether the three lepton generations occupy consistent integer rungs on the same phi-ladder as the tau-gate identity. It therefore participates in the broader check of the mass formula against the eight-tick octave and the phi fixed point. The module doc flags the rung correspondence as the most striking claim in the phi-ladder theory and lists falsification routes that would be triggered if the electron and muon fail to fit integer rungs relative to the same base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.