HKTDynamicTargetStatus
plain-language theorem explainer
Five-flag status record for the widened Hojman–Kuchař–Teitelboim dynamic target in the Seven Gaps gravity program. It tracks whether the dynamic target and rigidity statement are defined, whether the frozen unit-structure decoy is excluded, whether a dynamic inhabitant is banked, and whether gap-5 constraint recovery is done. Downstream code fills the booleans; the first three are presently true and the last two open. Anyone auditing Wave C2 R5/R6 groundwork cites this schema.
Claim. A five-field boolean status record for the dynamic HKT target program: (i) dynamic target defined, (ii) dynamic rigidity statement defined, (iii) unit-structure decoy excluded, (iv) dynamic inhabitant banked, (v) gap-5 constraint recovery complete. Each field is a plain $\mathrm{Bool}$; the structure itself asserts nothing beyond the existence of those flags.
background
The module is definition-only groundwork for Wave C2 (R5/R6): a widened Hojman–Kuchař–Teitelboim (HKT) target that carries an explicit structure-function slot with a non-constant structure condition. Codex adjudication rejected folding the structure function into momentum density and selling a frozen unit structure as GR.
Classical HKT recovers the Einstein constraints from hypersurface deformation algebra. Here the original one-site rigidity claim is already known false (counterexample at $n=1$). The widened dynamic target therefore separates definition of the target and of the rigidity statement from actual inhabitation and from gap-5 constraint recovery.
Related no-go material in the same cluster shows that the classical unsplit momentum–Hamiltonian advection form admits no smooth nearest-neighbor local profile against a frozen quadratic Hamiltonian (singular relation $(\pi_0+\pi_1)\partial_d f=\pi_0^2+d^2$ at $n=2$). The HamDyn-level analogue remains an open proposition.
proof idea
No proof: this is a structure declaration. Five named $\mathrm{Bool}$ fields are introduced with no default values and no theorems. Inhabitation is deferred to the sibling definition that assigns concrete flags.
why it matters
Gives a single machine-readable progress vector for the dynamic HKT target inside Gravity.SevenGaps. The sole downstream consumer is the concrete status value, which presently sets dynamic-target-defined, dynamic-rigidity-defined, and unit-structure-decoy-excluded to true, while dyn-inhabitant-banked and gap-5-constraint-recovery stay false.
That split matches the module brief: HKT rigidity with dynamic structure is defined, neither proved nor assumed; the unit-structure decoy is closed; inhabitation and gap-5 recovery remain open. The record therefore marks exactly where Wave C2 R5/R6 groundwork stops and where later proofs must land, without overclaiming GR recovery from frozen structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.