hktDynamicTargetStatus_flags
plain-language theorem explainer
Status snapshot for the widened Hojman–Kuchař–Teitelboim dynamic target: the dynamic target and rigidity statement are defined, and the frozen unit-structure decoy is excluded, while no dynamic inhabitant is banked and gap-5 constraint recovery remains open. Gravity auditors cite it to read the Wave C2 ledger without inspecting structure fields. Proof is a single decidability check on the concrete boolean record.
Claim. The HKT dynamic-target status record satisfies: dynamic target defined $=\mathrm{true}$, dynamic rigidity defined $=\mathrm{true}$, unit-structure decoy excluded $=\mathrm{true}$, dynamic inhabitant banked $=\mathrm{false}$, and gap-5 constraint recovery $=\mathrm{false}$.
background
This module is Wave C2 R5/R6 groundwork for a widened Hojman–Kuchař–Teitelboim (HKT) target in the Seven Gaps gravity stack. Codex adjudication rejected folding the structure factor $g$ into momentum density and treating frozen unit structure as GR. The widened target therefore carries an explicit structure-function slot with a non-constant structure condition.
The dynamic rigidity statement is only defined here, neither proved nor assumed. The original (non-dynamic) rigidity claim is already false at one site. Unsplit momentum–Hamiltonian advection is recorded as falsification-adjacent: no smooth nearest-neighbor local profile satisfies it against the frozen quadratic Hamiltonian at $n=2$.
The upstream status definition hard-codes the five boolean ledger flags that this theorem re-exports as a proved conjunction.
proof idea
One-line wrapper: decide on the concrete five-field boolean record from the status definition. Each field is a literal true or false, so propositional equality is decidable and closes immediately. No lemmas beyond the definition itself.
why it matters
Serves as the machine-checked ledger line for HKT dynamic-target progress inside Gravity/SevenGaps. It records what Wave C2 has actually closed (target and rigidity schemas defined; unit-structure decoy excluded) versus what remains open (no banked dynamic inhabitant; gap-5 constraint recovery still false).
Downstream use is empty so far; the value is auditability: a referee can cite the flags without re-reading the structure-function and point-split modules. It sits beside the unsplit momentum–Hamiltonian no-go and the strong point-split target class, marking that dynamic structure is on the books while GR-level constraint recovery is not yet claimed.
No forcing-chain (T0–T8) landmark is discharged here; this is scaffolding status for the gravity gap track, not a constants or dimension result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.