concreteDynamicInverseMetric
plain-language theorem explainer
A concrete positive inverse-metric candidate on the two-site lattice phase space: at each site it equals one plus the squared configuration coordinate. Gravity auditors cite it as the explicit dynamic counterexample that fixed background weights cannot represent. The body is a one-line algebraic formula, not a derived identity.
Claim. On the two-site phase space $x=(q,\pi)$ with $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, define the inverse-metric candidate $g^{-1}(x,j):=1+q_j^2$ for each lattice site $j\in\mathbb{Z}/2\mathbb{Z}$.
background
The ambient module separates background-weighted Dirac brackets from a fully dynamic ADM structure function. Exact lattice identities such as the weighted Hamiltonian bracket place a site-dependent weight in the structure-function slot, and continuum smearing carries that weight forward, but the weight is held fixed while the phase-space point varies. Full ADM gravity instead needs the inverse spatial metric in that slot to depend on the canonical metric data.
Phase space on an $n$-site periodic lattice is the product of configuration and conjugate momentum maps $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$, so each point is a pair of two-component real vectors. The present definition supplies an explicit positive function of those data that still varies with the configuration coordinates.
A fixed background weight is said to represent an inverse-metric candidate only when the two agree at every phase point and every site. That forces the candidate to be phase-space constant, which is the hinge of the blocker theorems built on this model.
proof idea
Pure definition: evaluate one plus the square of the configuration coordinate of $x$ at site $j$. No lemmas, no tactics; the formula is the content.
why it matters
This model is the concrete dynamic object that the Gap 5 structure-function blocker turns on. Downstream positivity, two-point witness, and non-constancy theorems establish that it is a genuine phase-space-dependent positive inverse metric. From non-constancy one obtains the concrete no-go: no fixed two-site background weight represents it at every phase point.
Those facts assemble into the certified blocker: every background weight still has an exact bracket and continuum reach, yet none represents this dynamic metric. The full-theory ledger records the same package and keeps the Gap 5 closure flag false, because a genuinely dynamic structure-function substrate (and the separate HKT rigidity obligation) remain open. The definition itself changes no closure flag; it is the witness that makes the background-versus-dynamic distinction sharp.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.