Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.HKTGroundworkAudit

show as:
view Lean formalization →

Audit barrel for Wave C2 R5/R6 HKT groundwork in the Seven Gaps gravity stack. It re-exports the one-site counterexample that kills the original rigidity claim at n=1, the widened dynamic target with an explicit nonconstant structure function, and the n=2 local-profile functional equation. Anyone tracking whether Hojman–Kuchař–Teitelboim-style rigidity can be restated after the Codex adjudication would land here. No new proofs: pure import aggregation.

claimModule collecting three HKT groundwork pieces: (i) falsity of the original rigidity statement on the one-site lattice $\mathbb{Z}/1\mathbb{Z}$; (ii) a widened dynamic target carrying an explicit structure function $g$ with $g$ nonconstant; (iii) the $n=2$ local-profile reduction of the dynamic Hamiltonian constraint to $\mathrm{momDensity}_j = h_b(j)\, h_p(j+1)$.

background

Hojman–Kuchař–Teitelboim (HKT) rigidity is the classical claim that the Hamiltonian and momentum constraints of geometrodynamics force the kinetic term to be the DeWitt supermetric (quadratic in momenta). In the Seven Gaps program this is formalized as a discrete lattice target HojmanKucharTeitelboimTarget n on $\mathbb{Z}/n\mathbb{Z}$.

Codex adjudication D-gap5-hkt-design-20260722 found the original statement false as written: on the degenerate one-site lattice every discrete difference and Wronskian vanishes, so a quartic kinetic density with zero momentum density meets every field of the $n=1$ target while escaping the quadratic pin. The response is a widened dynamic target that carries an explicit structureFunction slot with a structure_nonconstant side condition, rather than folding $g$ into momentum density and treating frozen unit structure as GR.

At $n=2$ the dynamic Hamiltonian–Hamiltonian identity for local profiles reduces to the pointwise factorization $\mathrm{momDensity}_j = h_b(j), h_p(j+1)$. That identity is the R6 attack surface; it does not by itself prove rigidity.

proof idea

This is a definition and audit module, not a proof module. It imports three sibling groundwork files and adds no theorems of its own: the $n=1$ counterexample that falsifies the original rigidity statement; the definition-only widened dynamic target (HKTRigidityStatementDyn is defined, neither proved nor assumed); and the $n=2$ local-profile functional equation that reduces the dynamic constraint to a momentum-density factorization. Argument structure is aggregation and status bookkeeping after the Codex rejection of the frozen-unit formulation.

why it matters in Recognition Science

Sits in the Gravity / Seven Gaps lane as the Wave C2 R5/R6 groundwork audit. Downstream consumers (none linked yet in the graph) would cite it when restating or attacking HKT-style rigidity after the original claim was shown false at $n=1$. It records three hard facts the rest of the chain must respect: original HKTRigidityStatement is false as stated; any repaired target must expose a nonconstant structure function rather than smuggle $g$ into momentum density; the $n=2$ local equation is an attack surface, not a rigidity proof. No parent theorem is wired in used_by yet; the module exists to keep the adjudication trail and the repaired definitions in one import path.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.