Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexampleAudit

show as:
view Lean formalization →

Audit layer for the one-site counterexample that falsifies HKT rigidity as stated. On the degenerate lattice $\mathbb{Z}/1\mathbb{Z}$, discrete differences and Wronskians vanish, so a quartic kinetic density with zero momentum density meets every field of the Hojman–Kuchař–Teitelboim target at $n=1$ while escaping the quadratic pin. Gravity workers closing SevenGaps Wave C2 R5/R6 cite this to record the adjudication. Structure is documentary: it imports and frames the counterexample module rather than reproving it.

claimOn the one-site lattice $\mathbb{Z}/1\mathbb{Z}$, the Hojman–Kuchař–Teitelboim rigidity claim (that admissible kinetic densities are forced to the quadratic pin) fails: there exist field configurations with vanishing discrete differences and Wronskians for which a quartic kinetic density and zero momentum density satisfy every component of the HKT target at $n=1$ without being quadratic.

background

Recognition Science gravity work packages the classical Hojman–Kuchař–Teitelboim (HKT) analysis as a discrete rigidity statement: admissible kinetic densities on a lattice of $n$ sites should be forced to a quadratic pin once the discrete difference structure and Wronskian constraints are imposed. The SevenGaps track isolates gaps in that transfer from continuum GR to the RS discrete setting.

The upstream counterexample module records a Codex adjudication (D-gap5-hkt-design-20260722): HKTRigidityStatement is false as stated when $n=1$. On $\mathbb{Z}/1\mathbb{Z}$ every discrete difference and Wronskian is identically zero, so the algebraic constraints that were meant to pin the kinetic density become vacuous. A quartic kinetic density with vanishing momentum density then satisfies every field of the HKT target at $n=1$ while escaping the quadratic pin.

This audit module sits one layer above that counterexample. It does not redefine the HKT target; it frames the degenerate one-site case as groundwork for Wave C2 R5/R6 so that later rigidity repairs can cite a named falsification rather than an informal remark.

proof idea

Definition and documentation module, not a proof development. It imports the HKT one-site counterexample module and exposes the adjudication that rigidity fails at $n=1$ because discrete differences and Wronskians vanish on $\mathbb{Z}/1\mathbb{Z}$. No independent lemmas are proved here; the logical content is the upstream existence of a quartic, zero-momentum configuration that meets the full HKT target while missing the quadratic pin. Readers should treat this as an audit wrapper that freezes the counterexample for SevenGaps bookkeeping.

why it matters in Recognition Science

SevenGaps Wave C2 needs a clean status on whether HKT-style rigidity survives discretization. The upstream counterexample shows the original statement is false at $n=1$; this audit module is the named place that records that falsification for R5/R6 groundwork. Downstream gravity developments that repair or re-scope HKT rigidity (non-degenerate $n$, strengthened difference hypotheses, or an explicit quadratic-pin axiom) depend on having the degenerate case sealed rather than rediscovered. In the broader RS gravity stack, the episode warns that continuum GR identities do not automatically force the discrete kinetic sector when the lattice collapses to a single site. No parent theorem currently lists this audit as a hard dependency (used_by is empty); its role is bookkeeping and design closure for the gap track.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.