function
plain-language theorem explainer
On the linearized 1D lattice rung of the discrete ADM program, the Dirac algebra structure function is frozen to the constant 1 (the inverse spatial metric of full gravity is absent). Constraint-closure and Poisson-bracket identities in the Seven-Gaps gravity lane cite this as the fixed spatial factor. It is a pure structure definition: fields are real propositions, with no proof body and no instances supplied in-file.
Claim. In the discrete ADM setting on a periodic 1D lattice, the continuum Dirac structure function equals $1$ on this flat scalar rung; in full gravity the same object is the inverse spatial metric $g^{ab}$. Each field of the structure is a genuine mathematical proposition (none is the trivial true proposition), and no instance is provided in the module.
background
The module is the first theorem-grade layer of the ADM/Dirac constraint-algebra program in the QG Seven-Gaps campaign (constraint-closure lane). It equips a finite-dimensional canonical phase space on a periodic 1D lattice with an fderiv-based Poisson bracket and kernel-checked closure relations for discrete constraint generators in the linearized regime.
The $(q,\pi)$ system is one polarization of a linearized TT-gauge lattice wave field. There is no metric degree of freedom on this rung, so the continuum structure function $g^{ab}$ of the Dirac algebra cannot vary: it is frozen to 1. Momentum and Hamiltonian constraint generators are definitional lattice discretizations; bracket identities (antisymmetry, bilinearity, Leibniz, canonical pairs, and $D$–$H$ closure) are the theorems built on top of that phase space.
Upstream lattice and continuum-smearing work in the Seven-Gaps stack treats analogous structure-function and profile objects; here the object is specialized to the flat scalar rung where the spatial factor is identically one.
proof idea
No proof. The declaration is a structure (definitional packaging) whose fields are proposition-valued mathematical statements about the frozen structure function. The module explicitly records that none of those fields is the trivial true proposition and that no instance is constructed anywhere in the file. Downstream bracket and closure theorems simply read the constant-$1$ convention from this packaging rather than deriving a dynamical $g^{ab}$.
why it matters
Without a fixed structure function, the discrete Dirac algebra on this rung is not even well-typed: continuum identities involve $g^{ab}$ as the spatial factor in ${H[N],H[M]}$ and related brackets. Freezing it to 1 is the honest scope cut that lets the module prove sharp momentum-sector closure and the exact forward-difference $D$–$H$ anomaly without pretending to full $3{+}1$ gravity.
It sits in the Seven-Gaps constraint-closure ladder toward a discrete ADM program. Parent consumers in the wider tree include Hamiltonian energy bookkeeping and cost-algebra windowing only at the level of shared real-analytic vocabulary; the scientifically primary dependents are the in-module bracket closure theorems (bracket_Dgen_Dgen, bracket_Dgen_Ham, and the constant-lapse anomaly). Framework-wise this is scaffolding for later unfreezing toward a true inverse-metric structure function once metric degrees of freedom enter, not a claim that $D=3$ gravity is already present (T8 is upstream geometry, not this rung).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.