continuum_dictionary
plain-language theorem explainer
A fixed lookup table pairing ten Recognition-Science lattice notions with continuum field-theory counterparts (voxel to spacetime point, J-cost to Lagrangian density, eight-tick cycle to Matsubara period, and so on). Anyone reading the F-014 continuum-limit certificate cites it as the conceptual map. The body is a pure list literal of string pairs; there is nothing to prove.
Claim. The continuum dictionary is the finite list of pairs identifying each discrete Recognition concept with its continuum counterpart: lattice site with spacetime point; log-ratio $t(x)$ with scalar field $\varphi(x)$; $J(e^{t})=\cosh t-1$ with Lagrangian density $\tfrac12(\partial\varphi)^2+\tfrac12 m^2\varphi^2+\lambda\varphi^4/24$; total defect $\sum J$ with action $S=\int L\,d^4x$; variational minimization with Euler-Lagrange equations; lattice Laplacian with d'Alembertian $\square$; log-charge conservation with $\partial_\mu j^\mu=0$; 8-tick cycle with Matsubara periodicity; $\varphi$-ladder rungs with the mass spectrum; one voxel per tick ($c=1$) with the speed of light.
background
Module F-014 asks how continuous differential physics emerges from the discrete ledger on $\mathbb{Z}^3$. The J-cost $J(e^t)=\cosh t-1$ expands as $t^2/2+t^4/24+\cdots$. At long wavelength the quadratic piece yields a lattice Laplacian, which scales to $\nabla^2$ and thence to Klein-Gordon structure; higher Taylor terms supply interactions.
LatticeToContDict is a two-field record (lattice string, continuum string). The dictionary is the explicit roster of those pairs. Upstream constants fix the units: one tick $\tau_0=1$, one voxel $\ell_0=1$, so $c=\ell_0/\tau_0=1$. Rung-coarsen cost and spectrum supply the discrete recognition content that the continuum action and mass ladder are meant to match.
The surrounding certificate (F-014) lists seven forced steps: quadratic leading term, Laplacian identification, continuum limit, Klein-Gordon form, Gaussian universality, uniqueness of all Taylor coefficients from $J=\cosh-1$, and CPT from evenness $J(t)=J(-t)$.
proof idea
No proof. The declaration is a definition whose right-hand side is a ten-element list literal of lattice-to-continuum record constructors. Each entry hard-codes one lattice phrase and one continuum phrase. Nothing is computed or discharged.
why it matters
Gives the human-readable bridge for F-014: every discrete object that the continuum-limit theorems manipulate is named beside its continuum image. The module doc traces the chain J-cost to lattice Laplacian to continuous Laplacian to Klein-Gordon to Dirac (via D = 3 spinors) to Einstein (defect curvature). Primer landmarks appear directly: T5 J-uniqueness ($J=\cosh(\log x)-1$), T7 eight-tick octave (here as Matsubara periodicity), T6 phi-ladder as the mass spectrum, and $c=1$ in RS-native units. No downstream Lean users yet; the value is documentary and certificate-facing, not a lemma dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.