concreteDynamicInverseMetric_witness
plain-language theorem explainer
On the two-site lattice, the model inverse metric 1+(q_j)^2 equals 1 at the zero canonical point and 2 at the unit-configuration point (site 0). Anyone proving that this candidate is phase-space-dependent cites this evaluation pair. The proof is a one-shot numerical unfolding of the three definitions.
Claim. Let $g(x,j)=1+(q_j(x))^2$ be the positive two-site inverse-metric candidate. Then $g(x_0,0)=1$ and $g(x_1,0)=2$, where $x_0$ is the zero canonical point and $x_1$ is the point with unit configuration and vanishing momentum.
background
This module separates fixed background weights in the Dirac structure-function slot from a genuinely dynamic inverse spatial metric. The exact lattice identity bracket_HamW_HamW and the continuum smearing limit keep the weight fixed while the phase-space point varies; full ADM gravity needs the inverse metric to move with the canonical data.
The model candidate is $g(x,j)=1+(q_j)^2$ on PhaseSpace 2. The zero canonical point has vanishing configuration and momentum; the unit-configuration point has $q\equiv 1$ and $p\equiv 0$. Both are ordinary points in the two-site phase space used as evaluation sites.
The surrounding development shows that a fixed background weight can represent a phase-space-dependent inverse metric at every point only if that metric is phase-space constant. Explicit unequal values at two points are therefore the first step toward blocking background representation.
proof idea
Term-mode proof by norm_num after unfolding the three definitions. Substituting the zero point into $1+(q_j)^2$ yields $1+0=1$; substituting the unit-configuration point yields $1+1^2=2$. No lemmas beyond definitional reduction are required.
why it matters
Feeds directly into concreteDynamicInverseMetric_not_constant, which assumes constancy, applies it at the two witness points, and rewrites with this equality pair to obtain $1=2$. That non-constancy theorem is then used by the certified blocker gap5_background_weight_blocker: no fixed two-site weight represents this positive dynamic metric at all phase points, even though the background-weighted family still has its exact bracket and continuum reach.
In the Seven Gaps gravity program this is the concrete counterexample that forces Gap 5 to demand a phase-space-dependent Hamiltonian construction rather than a fixed background weight. It does not close the gap; PhaseSpaceDependentHamiltonianConstruction and the HKT rigidity target remain separate obligations. No T0–T8 landmark is altered; the result is local to the Dirac structure-function analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.