cellCoords0
plain-language theorem explainer
Extracts the three real coordinates (q at site 0, q at site 1, and conjugate momentum at site 0) from a two-site lattice phase-space point. Downstream smoothness and Fréchet-derivative identities for local Hamiltonian profiles cite this chart map. The body is a pure projection triple, not a proof.
Claim. On the two-site canonical phase space $(q,\pi)$ with $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the cell chart sends $y$ to the triple $\bigl(q(0),\,q(1),\,\pi(0)\bigr)\in\mathbb{R}^3$.
background
The ambient object is the lattice phase space of HypersurfaceDeformation: for $n$ sites, $\mathrm{PhaseSpace},n=(q,\pi)$ with configuration $q:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and conjugate momentum $\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ on the periodic chain. Here $n=2$, so each field is a pair of reals.
The module sits in Wave C4/C5 gap5 work: mod-vacuum kill plus kinetic-normalized rigidity for HKT-style local Hamiltonians. Local Hamiltonian profiles are treated as smooth maps on a three-real chart of the two-site cell; this definition supplies that chart by reading $q_0$, $q_1$, and $\pi_0$.
Coordinate functionals on phase space are already continuous linear maps; the chart is their product packaging into $\mathbb{R}\times\mathbb{R}\times\mathbb{R}$, which is the domain used by profile maps and Fréchet derivatives later in the file.
proof idea
Definition only: project the first factor of $y$ at lattice indices $0$ and $1$, and the second factor at index $0$. No lemmas, tactics, or algebraic rewriting; the right-hand side is the triple of evaluations.
why it matters
The chart is the bridge from abstract two-site phase space to the $\mathbb{R}^3$ coordinates used by local Hamiltonian smoothness. It feeds hasFDerivAt_cellCoords0 (product of coordinate Fréchet derivatives), the identity that the chart of the standard embedding fePhase a b p 0 recovers $(a,b,p)$, and the two theorems equating the profile partials $h_b$ and $h_p$ to Fréchet derivatives of the profile map along $(0,1,0)$ and $(0,0,1)$.
Those derivative identities are part of the kinetic-normalized CanonicalMom intensivity apparatus in the gap5 terminal: FTC recovery is theorem-derived rather than an assumed class field. The definition itself is scaffolding for that rigidity half, not a physics claim about gravity or the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.