Gap5DynamicDiracAndHKTRigidityTarget
plain-language theorem explainer
Gap 5 of the gravity seven-gaps ledger is packaged as the conjunction of a phase-space-dependent Dirac structure-function premise and an HKT rigidity statement at positive dimension n. Researchers tracking open ADM obligations against the background-weighted bracket cite this target. It is a pure Prop definition: no proof is given, and both conjuncts remain open relative to the existing fixed-weight HamW results.
Claim. For every positive integer $n$, the Gap-5 dynamic target holds precisely when both a phase-space-dependent Dirac premise is available at dimension $n$ and the HKT rigidity statement holds at the same $n$.
background
The module isolates a structural gap between the background-weighted Hamiltonian bracket and full ADM gravity. The exact lattice identity for the weighted bracket and its continuum smearing place a site-dependent weight in the Dirac structure-function slot, but that weight is held fixed as the phase-space point varies. Continuum ADM instead needs the inverse spatial metric in that slot to vary with the canonical metric data.
The file certifies the distinction: a fixed background weight represents a phase-space-dependent inverse metric at every phase point only if that metric is phase-space constant. An explicit positive two-site dynamic inverse metric is not constant, so no fixed background weight represents it. The existing weighted bracket therefore cannot by itself be the full dynamic Dirac structure function.
This definition does not close that gap. It only names the two remaining obligations that Gap 5 still requires beyond the certified blocker.
proof idea
Definitional packaging only. The body is the conjunction of the phase-space-dependent Dirac premise and the HKT rigidity statement at the same positive dimension $n$. No lemmas are applied and no tactic proof runs; both conjuncts are left as open Prop obligations relative to the present fixed-weight HamW theorem and its continuum smearing.
why it matters
In the Recognition Science gravity stack, seven named gaps separate lattice recognition calculus from continuum ADM. Gap 5 is the dynamic Dirac structure function together with HKT rigidity. The surrounding module already proves the blocker: fixed background weights cannot represent a non-constant dynamic inverse metric, so the background-weighted bracket, despite exact lattice identity and continuum reach, is not the full structure function.
This target records what must still be supplied: a Hamiltonian construction whose structure function genuinely depends on phase space, and an HKT rigidity theorem. The module doc states explicitly that no closure flag is changed. Work that closes Gap 5 will discharge both conjuncts (or a stronger package that implies them). Ambient RS landmarks such as the eight-tick octave and Clifford bridge sit in the foundation imports but are not proof steps for this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.