photonMass
plain-language theorem explainer
The definition assigns photon mass the exact value zero in RS-native units, encoding unbroken U(1) electromagnetic symmetry after J-cost symmetry breaking. Particle physicists checking gauge boson consistency in beyond-Standard-Model extensions would cite it when verifying that the photon stays massless while other particles acquire mass from the vev. The assignment is a direct constant definition with no reduction steps.
Claim. The photon mass is defined as $m_γ = 0$ in RS-native units, reflecting the unbroken $U(1)_{em}$ symmetry in the J-cost symmetry-breaking framework.
background
The module derives the Higgs mechanism from the J-cost functional $J(x) = ½(x + 1/x) - 1$, which is symmetric under $x ↔ 1/x$ and minimized at $x=1$. Spontaneous symmetry breaking occurs when the vacuum selects a value such as φ, generating masses proportional to J-cost at that point while preserving some gauge symmetries. Upstream results supply the RS-native units structure U with τ₀ = 1 tick, ℓ₀ = 1 voxel and c = 1, fixing the gauge in which all masses are expressed.
proof idea
Direct definition that assigns the constant 0. It is used verbatim by the one-line wrapper photon_massless : photonMass = 0 := rfl.
why it matters
This definition supplies the massless photon required by the SM-002 derivation of the Higgs mechanism from J-cost. It is the immediate parent of the theorem photon_massless that confirms unbroken U(1) symmetry. In the Recognition Science chain it preserves the gauge structure consistent with T7 eight-tick octave and D = 3 while other particles acquire mass via the phi-ladder; it touches the open question of parameter-free mass generation for all gauge bosons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.