kg_mass_squared
plain-language theorem explainer
The Klein-Gordon mass-squared parameter equals the reciprocal square of the lattice spacing. Continuum-limit work cites it when matching discrete J-cost dynamics on ℤ³ to (∂² − m²)φ = 0. The definition encodes unit curvature at the J-minimum: J''(1) = 1, so m² = 1/a². It is a one-line abbreviation, not a derived identity.
Claim. For a real lattice spacing $a$, the Klein-Gordon mass-squared parameter in the continuum limit is $m^2(a) = 1/a^2$. This records that the second derivative of the J-cost at its minimum is $J''(1) = 1$, so the continuum mass term is $m^2 = J''(1)/a^2 = 1/a^2$.
background
Module F-014 shows how discrete J-cost dynamics on the lattice ℤ³ produce, in the long-wavelength limit, a second-order equation with Klein-Gordon structure. The J-cost is $J(e^t) = \cosh(t) - 1$, with Taylor expansion $t^2/2 + t^4/24 + \cdots$. Small perturbations make the leading quadratic term dominate; quadratic lattice costs yield a discrete Laplacian, which scales to the continuum $\nabla^2$.
The mass term is not inserted by hand. It comes from the curvature of $J$ at its unique minimum $x = 1$. Cost.Convexity proves $J''(1) = 1$. Dividing that curvature by the squared lattice spacing $a^2$ supplies the continuum coefficient $m^2$ in $(\partial^2 - m^2)\varphi = 0$.
Sibling material in the module develops the quadratic leading term, the lattice Laplacian, and the scaling limit that recovers continuous $\nabla^2$. This definition isolates the mass parameter that those steps feed into the Klein-Gordon form.
proof idea
Pure definition: the body is the term $1/a^2$. No tactics or lemmas are applied. The mathematical justification sits in the doc-comment and upstream convexity: $J''(1) = 1$ (Cost.Convexity.deriv2_Jcost_one), so the continuum mass-squared is exactly the reciprocal square of the lattice spacing. Treat it as a named constant in later continuum-limit statements.
why it matters
F-014 asks how continuous field equations emerge from the discrete ledger, ticks, and voxels. The chain is J-cost on ℤ³ → lattice Laplacian → continuum $\nabla^2$ → Klein-Gordon (mass from curvature at the J-minimum) → Dirac (spinor structure in $D = 3$) → Einstein (defect-field curvature). This definition pins the mass coefficient in that Klein-Gordon step: $m^2 = J''(1)/a^2 = 1/a^2$.
It sits next to the module's main results on quadratic leading behavior, lattice-Laplacian equivalence, and the Gaussian universality class. No downstream Lean uses are wired yet; the object is infrastructure for klein_gordon_structure and related continuum statements. It does not replace the RS mass ladder (yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$); it only names the continuum KG parameter from local J-curvature and lattice scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.