hktDynamicTargetStatus
plain-language theorem explainer
Status record for the widened Hojman–Kuchař–Teitelboim dynamic target in the Seven Gaps gravity stack. It marks the dynamic target and rigidity proposition as defined, the frozen unit-structure decoy as excluded, and records that no dynamic inhabitant is banked and Gap 5 constraint recovery is still open. Downstream residual DAGs and flag lemmas cite it as the single source of truth for those booleans. The body is a pure structure literal.
Claim. The HKT dynamic-target status is the five-flag record with dynamic target defined $=\mathsf{true}$, dynamic rigidity defined $=\mathsf{true}$, unit-structure decoy excluded $=\mathsf{true}$, dynamic inhabitant banked $=\mathsf{false}$, and Gap 5 constraint recovery $=\mathsf{false}$.
background
This module is Wave C2 R5/R6 groundwork for 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 treating frozen unit structure as GR.
The status structure is a five-boolean ledger: whether the dynamic target and the dynamic rigidity proposition are defined, whether the unit-structure decoy has been excluded, whether a dynamic inhabitant has been banked, and whether Gap 5 constraint recovery is complete. The original one-site rigidity statement is already known false; the dynamic variants are defined here as schema, not as proved theorems.
Related no-gos in the same gravity stack show that unsplit momentum–Hamiltonian advection is uninhabitable for smooth nearest-neighbor profiles against a frozen quadratic Hamiltonian, which is why the ledger keeps inhabitant and recovery flags false.
proof idea
Definitional structure literal. Each field of the status record is assigned a boolean constant (true for the three definitional/exclusion milestones, false for inhabitant banking and Gap 5 recovery). No lemmas or tactics are involved.
why it matters
Serves as the single boolean source for Gap 5 residual tracking. The typed residual TypedResidual_gap5_hkt_dyn_target_defined asserts exactly that the dynamic target and rigidity props are defined while inhabitant banking and Gap 5 recovery remain false, matching the Wave D model note that the widened Dyn HKT target and Dyn rigidity Prop are defined but are neither an inhabitant nor a rigidity proof.
The companion theorem hktDynamicTargetStatus_flags re-exports all five equalities for convenient use in residual DAGs. In the Recognition gravity program this ledger keeps the HKT dynamic widening honest: definitions exist, the unit-structure decoy is closed, and the open work (inhabitant, constraint recovery) stays explicitly unmarked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.