cellCoords0D
plain-language theorem explainer
On the two-site lattice phase space, the continuous linear map that reads out the triple (q_0, q_1, π_0). It is the candidate Fréchet derivative of the nonlinear cell-coordinate chart used in local Hamiltonian smoothness. Downstream rigidity lemmas cite it to identify partials of a local Hamiltonian profile with directional fderivs along the b and p axes.
Claim. Define the continuous linear map $D:\mathrm{PhaseSpace}(2)\to\mathbb{R}\times\mathbb{R}\times\mathbb{R}$ by $D=(q_0,q_1,\pi_0)$, i.e. the product of the configuration functionals at lattice sites $0$ and $1$ with the momentum functional at site $0$.
background
The ambient model is the canonical phase space of a lattice wave field: $\mathrm{PhaseSpace}(n)=(Z/n\mathbb{Z}\to\mathbb{R})\times(Z/n\mathbb{Z}\to\mathbb{R})$, pairs of configuration $q$ and conjugate momentum $\pi$ on a periodic $n$-site lattice. Coordinate functionals $q_i$ and $\pi_i$ are continuous linear maps obtained by projecting the first or second factor and then the $i$-th component.
This module closes Wave C4/C5 gap 5 on HKT kinetic-normalized rigidity: after killing the mod-vacuum statement with a variable-kinetic CanonicalMom inhabitant, the remaining work is intensivity of the kinetic-normalized canonical momentum and FTC recovery as a derived theorem rather than an assumed class field.
For $n=2$, local Hamiltonian profiles are functions of a three-real cell $(a,b,p)$. The linear readout $(q_0,q_1,\pi_0)$ is the infinitesimal version of that cell chart, so smoothness and chain-rule identities can be stated in Mathlib's HasFDerivAt/fderiv language.
proof idea
Definitional one-liner: product of three continuous linear maps already on the shelf. Compose coordQ 0, coordQ 1, and coordP 0 via the continuous-linear product constructor. No proof obligations beyond the types of those projections.
why it matters
Supplies the derivative object that hasFDerivAt_cellCoords0 certifies as the Fréchet derivative of the nonlinear cell chart. That identity is the bridge used by LocalHamSmooth_hp_eq_fderiv and LocalHamSmooth_hb_eq_fderiv, which rewrite the local Hamiltonian profile partials $h_p$ and $h_b$ as directional Fréchet derivatives of the profile map along $(0,0,1)$ and $(0,1,0)$.
Those equalities sit inside the kinetic-normalized rigidity terminal for gap 5: once partials are genuine fderivs under a $C^2$ profile hypothesis, FTC recovery of the normalized canonical momentum becomes theorem-derived rather than an axiomatic class field. In the broader SevenGaps gravity stack this is bookkeeping infrastructure, not a new physical law; it lets the HKT kinetic sector speak Mathlib calculus cleanly on the two-site cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.