concreteDynamicInverseMetric_not_constant
plain-language theorem explainer
The positive two-site inverse-metric candidate g(x,j)=1+(q_j)^2 is genuinely phase-space dependent, not constant under changes of canonical data. Dirac-structure and ADM-gravity workers cite it to separate fixed background weights from full metric dynamics. The proof feeds the zero and unit configuration points into the constancy hypothesis and obtains the numerical contradiction 1=2 from an explicit witness.
Claim. Let $g$ be the two-site inverse-metric candidate $g(x,j)=1+(q_j(x))^2$ on phase space. Then $g$ is not phase-space constant: it is not the case that $g(x,j)=g(y,j)$ for all phase-space points $x,y$ and all sites $j\in\mathbb{Z}/2\mathbb{Z}$.
background
In the background-weighted Dirac bracket program, the exact lattice identity and its continuum smearing keep a site weight fixed while the phase-space point varies. Full ADM gravity instead needs the inverse spatial metric in that structure-function slot to depend on the canonical metric data.
A lattice inverse metric is called phase-space constant when its value at every site is independent of the canonical point: $g(x,j)=g(y,j)$ for all $x,y$ and sites $j$. The model candidate on the two-site lattice is $g(x,j)=1+(q_j)^2$, built from the configuration coordinate at each site. Two explicit points are used as witnesses: the zero canonical point, where $g=1$ at site $0$, and the unit configuration point, where $g=2$ at the same site.
The module's role is to certify that a fixed background weight can represent a candidate inverse metric at every phase point only if that metric is phase-space constant. The present theorem supplies the non-constancy half of that distinction for the concrete positive example.
proof idea
Assume for contradiction that the concrete candidate is phase-space constant. Instantiate the universal quantifiers at the zero phase point, the unit configuration point, and site $0$. The witness lemma rewrites the two sides to the numerals $1$ and $2$. A single norm_num then closes the contradiction $1=2$. The argument is a short tactic proof driven entirely by the explicit two-point witness; no continuum or bracket identities are invoked.
why it matters
This non-constancy is the concrete half of the Gap-5 blocker. Downstream, no_fixed_background_represents_concrete feeds it into the general fact that any fixed background weight representing a metric forces that metric to be phase-space constant, yielding a no-go for every two-site weight against this candidate. That no-go is packaged into gap5_background_weight_blocker, which records that the existing background-weighted family keeps its exact bracket and continuum reach yet cannot represent the explicit positive dynamic metric at all phase points.
In the Recognition gravity stack this separates the already-proved weighted bracket from the still-open dynamic Dirac structure function and the separate HKT rigidity obligation. No closure flag moves; the theorem only certifies that fixed background weights are insufficient for full ADM metric dependence on the two-site model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.