concreteDynamicInverseMetric_pos
plain-language theorem explainer
On the two-site phase space, the model inverse metric 1 + q_j^2 is strictly positive at every phase point and every site. Gravity auditors cite it when showing that a genuinely dynamic spatial inverse metric cannot be absorbed into a fixed background weight. The proof unfolds the definition and applies Mathlib positivity to 1 plus a square.
Claim. For every phase-space point $x$ on the two-site lattice and every site $j \in \mathbb{Z}/2\mathbb{Z}$, the concrete inverse-metric candidate satisfies $0 < 1 + (q_j(x))^2$, where $q_j(x)$ is the configuration coordinate of $x$ at site $j$.
background
This module separates background-weighted Dirac structure functions from the fully dynamic ADM inverse metric. The exact lattice identity bracket_HamW_HamW and the continuum smearing limit keep a site-dependent weight fixed while the phase point varies. Full ADM gravity instead needs the inverse spatial metric in that slot to depend on the canonical metric data.
PhaseSpace 2 is the two-site canonical phase space (configuration plus momentum data per site). The model inverse metric is defined pointwise by $g^{jj}(x) := 1 + (q_j(x))^2$: it is positive by construction and varies with the configuration coordinate at each site. The surrounding blocker argument shows that a fixed background weight can match a phase-space-dependent inverse metric at every phase point only if that metric is actually constant on phase space.
proof idea
Term-mode proof in two steps. Unfold concreteDynamicInverseMetric to expose the expression $1 + (x.1, j)^2$. Then invoke Mathlib's positivity tactic, which discharges $0 < 1 + t^2$ for any real $t$ from the sum of a positive constant and a square. No intermediate lemmas are required.
why it matters
Positivity is a prerequisite for treating the two-site example as a legitimate inverse-metric candidate inside the Gap-5 blocker. Downstream, gap5_background_weight_blocker packages three facts: the background-weighted family still has its exact bracket and continuum reach, yet no fixed two-site weight represents this concrete dynamic metric at all phase points.
Together with the non-constancy and non-representability lemmas in the same file, this pins the distinction the module advertises: existing background-weighted brackets cannot by themselves be the full dynamic Dirac structure function. No closure flag moves; the missing piece remains the phase-space-dependent Hamiltonian construction named by PhaseSpaceDependentHamiltonianConstruction, recorded separately from HKT rigidity in Gap5DynamicDiracAndHKTRigidityTarget.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.