IndisputableMonolith.Gravity.SevenGaps.HKTDynamicTarget
Open target module packaging Hojman–Kuchař–Teitelboim hypotheses with an explicit dynamic Dirac structure function. A non-constant structure clause excludes frozen background decoys that would trivialize the algebra. Gap-5 constraint-closure workers cite it when wiring residual DAGs, groundwork audits, and point-split repairs. Deliberately uninhabited: it states the target Prop rather than proving it.
claimThe module declares a dynamic Hojman–Kuchař–Teitelboim target: hypotheses on the discrete ADM constraint algebra in which the Dirac structure function may depend on canonical metric data (not a frozen background weight), plus a rigidity statement and unit-structure lemmas recovering the original Hamiltonian–Hamiltonian right-hand side when the structure is phase-space constant.
background
HypersurfaceDeformation supplies the Lane-5 setting: finite-dimensional canonical phase space on a periodic lattice, an fderiv-based Poisson bracket, and kernel-checked closure for discrete constraint generators in the linearized regime.
DynamicStructureFunctionBlocker records the obstruction this target is meant to face. Existing results place a site-dependent weight in the Dirac structure-function slot, but keep that weight fixed as the phase-space point varies. Full ADM gravity instead needs the inverse spatial metric in that slot to vary with the canonical metric data.
This module therefore opens an HKT hypothesis package whose structure function is explicitly dynamic, with a non-constant clause that rules out the frozen/background decoy.
proof idea
Definition and open-target module, not a proof development. It packages Prop-valued hypotheses (dynamic HKT target and rigidity statement), unit-structure recovery facts showing the constant-structure case recovers the original ham–ham RHS and is phase-space constant, and a status-flag bundle. No inhabiting construction is given; the target is left deliberately uninhabited.
why it matters in Recognition Science
Imported by Gap5ConstraintResidualDAG, which names residuals for dynamic Dirac structure functions and HKT rigidity in the Wave C2/D typed residual DAG for gap5_constraint_recovery. Also feeds HKTDynamicTargetAudit, HKTGroundworkAudit (Wave C2 R5/R6 axiom audit), and HKTPointSplitTarget. The latter notes that the widened dynamic target keeps an unsplit mom_ham field, uninhabitable for honest nearest-neighbor local momentum profiles against a frozen quadratic Hamiltonian, and repairs that scope. The module is the named open target in the discrete ADM/Dirac constraint-closure program.
scope and limits
- Does not inhabit the dynamic HKT target; the Prop is deliberately open.
- Does not prove continuum ADM recovery from the lattice model.
- Does not supply a point-split mom_ham; that repair lives downstream.
- Does not claim structure-function dynamics beyond the discrete periodic setting.
- Does not discharge Gap-5 residual obligations by itself.