cellCoords0_fePhase
plain-language theorem explainer
Extracting the triple (q₀, q₁, π₀) from the two-cell phase-space point built by the standard cell embedding with last momentum zero recovers the input (a, b, p). Local smoothness lemmas for the kinetic-normalized Hamiltonian profile cite this to align chart coordinates with Fréchet derivatives. The proof is a one-line simp unfolding of both definitions.
Claim. For all real $a,b,p$, if one embeds the cell $(q_0,q_1,\pi_0,\pi_1)=(a,b,p,0)$ into two-mode phase space and then projects to the first configuration pair and first momentum, the result equals $(a,b,p)$.
background
The ambient module closes Wave C4/C5 gap5: a mod-vacuum kill plus kinetic-normalized rigidity for the HKT (Hamilton–Killing–type) sector. Phase space on two cells is a pair of maps ZMod 2 → ℝ (configurations and momenta). The standard cell embedding sends four reals $(a,b,p,r)$ to the point with $q_0=a$, $q_1=b$, $\pi_0=p$, $\pi_1=r$.
The private chart cellCoords0 reads only the first three slots: $(q_0,q_1,\pi_0)$. That chart is the domain on which local Hamiltonian profiles and their $C^2$ smoothness data are written, so one needs a clean inverse identity when the fourth slot is set to zero.
Upstream, the cell embedding is the configuration/momentum constructor used throughout the CanonicalMom rigidity development; the present identity is the matching left-inverse on the $(a,b,p)$ face.
proof idea
One-line wrapper: simp unfolds the chart and the cell embedding. After reduction, the three components are definitionally $a$, $b$, and $p$ by the if j = 0 branches on ZMod 2.
why it matters
Feeds the two local Fréchet-derivative identities for a smooth local Hamiltonian profile: the $b$-partial and the $p$-partial equal the corresponding directional Fréchet derivatives of the profile map at $(a,b,p)$. Those lemmas sit inside the kinetic-normalized CanonicalMom rigidity terminal of gap5, where FTC recovery is theorem-derived rather than an assumed class field.
In the Recognition gravity stack this is bookkeeping, not a physical law: it locks chart coordinates so the normalized kinetic Hamiltonian can be differentiated without coordinate drift. It supports the C5 upgrade path that flips gap5_constraint_recovery once both ledger halves bind green. No T0–T8 landmark is at stake; the result is internal to the SevenGaps HKT rigidity chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.