unitConfigurationPoint
plain-language theorem explainer
Canonical two-site phase-space point with unit configuration and vanishing momentum. Downstream proofs evaluate the concrete dynamic inverse metric here and at the zero phase point to exhibit two distinct values. The body is the pair of constant maps (site ↦ 1, site ↦ 0) on ℤ/2ℤ.
Claim. The point $(q,\pi)$ in the two-site lattice phase space with $q_i=1$ and $\pi_i=0$ for every site $i\in\mathbb{Z}/2\mathbb{Z}$.
background
The ambient phase space on an $n$-site periodic lattice is the product of configuration and conjugate momentum: pairs $(q,\pi)$ with $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$, so each field is a pair of real values on the two sites.
This module separates fixed background weights in the Dirac structure-function slot from genuinely phase-space-dependent inverse metrics required by full ADM gravity. The exact lattice identity bracket_HamW_HamW and its continuum smearing keep the weight fixed while the phase point varies; the file shows that such a fixed weight can represent a phase-space-dependent inverse metric everywhere only if that metric is constant on phase space.
The companion point with vanishing configuration and momentum is the other evaluation site used in the same comparison.
proof idea
Definitional constructor, not a proof. The value is the pair of constant functions on $\mathbb{Z}/2\mathbb{Z}$: configuration identically $1$, momentum identically $0$. No lemmas are applied.
why it matters
Supplies one of the two explicit phase points that make the concrete two-site inverse-metric candidate non-constant. The witness theorem evaluates that candidate at the zero phase point and at this unit-configuration point, obtaining $1$ and $2$ respectively at site $0$. The non-constancy theorem then feeds those unequal values into the fixed-background representation criterion, concluding that no background weight represents the candidate. That is the dynamic structure-function blocker: the existing background-weighted bracket cannot by itself be the full dynamic Dirac structure function. The module leaves the missing phase-space-dependent Hamiltonian construction and the separate HKT rigidity obligation open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.