KleinGordonStructure
plain-language theorem explainer
Packages the continuum-limit data of linearized Recognition Science dynamics: a positive mass-squared and a positive propagation speed. Anyone citing the lattice-to-Klein-Gordon bridge (F-014) uses this carrier. It is a plain structure with positivity witnesses, not a proved PDE identity.
Claim. A Klein-Gordon structure is a pair $(m^2, c)$ of real numbers with $m^2 > 0$ and $c > 0$, intended as the mass-squared and light speed of the continuum limit of linearized RS lattice dynamics: $\partial_t^2\phi = c^2\nabla^2\phi - m^2\phi$, where $m^2$ comes from the second derivative of the $J$-cost at equilibrium and $c = a/\tau$ is one voxel per tick.
background
Module F-014 (Continuum Limit) shows how discrete $J$-cost dynamics on $\mathbb{Z}^3$ yield smooth field equations. The cost $J(e^t) = \cosh t - 1$ expands as $t^2/2 + O(t^4)$; small perturbations therefore see a quadratic cost, which on a lattice is equivalent to a discrete Laplacian, and under $a\to 0$, $\tau\to 0$ with $c=a/\tau$ fixed becomes $\nabla^2$.
The module's narrative chain is: $J$-cost on $\mathbb{Z}^3$ $\to$ lattice Laplacian $\to$ continuous $\nabla^2$ $\to$ Klein-Gordon (mass from the $\phi$-ladder) and onward to Dirac and Einstein. Sibling material includes the quadratic leading term of $J$, lattice shift operators, and the lattice Laplacian with its linearity lemmas.
This structure is the data type that records the two continuum coefficients once that limit is taken: mass-squared forced positive by convexity of $J$ at equilibrium, and speed forced positive by the lattice spacing and tick.
proof idea
No proof body: this is a structure definition. Fields are mass_squared and speed (reals) plus two positivity propositions. Instantiation is by supplying concrete positives and discharging the inequalities (as in the canonical unit instance with both coefficients equal to 1 via norm_num).
why it matters
Fills the F-014 registry item: how continuum physics emerges from the discrete ledger. Downstream, rs_klein_gordon builds the canonical RS instance with unit mass-squared and unit speed, the natural normalization when $c=1$ in RS units and the quadratic curvature of $J$ at 1 sets the mass scale.
In the broader forcing chain this sits after discreteness and dimension forcing ($D=3$, eight-tick octave) and before spinor/Dirac and curvature/Einstein steps sketched in the module doc. It does not itself derive $m^2 = J''(1)/a^2$; it only holds the continuum coefficients so later theorems can state that linearized RS dynamics land in the Klein-Gordon universality class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.