Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong

show as:
view Lean formalization →

Defines the strong point-split Hojman–Kuchař–Teitelboim dynamic target on a discrete circle, with Kronecker site weights and explicit Hamiltonian advection maps. Gravity gap-5 workers cite it to inhabit the n=2 strong target via a balanced quartic density and to refute strong rigidity. The module is mostly definitions plus elementary ZMod-2 arithmetic identities that pin the advection equalities.

claimOn $\mathbb{Z}/n\mathbb{Z}$, introduce the Kronecker site weight $\delta_i(j)$ (1 at $i$, 0 elsewhere), the computed Hamiltonian advection maps from/to a site, and the strong point-split HKT dynamic target structure. At $n=2$ these specialize with $\mathbb{Z}/2\mathbb{Z}$ successor identities and a balanced quartic Hamiltonian density used to inhabit the strong target.

background

Recognition Science gap-5 work reconstructs continuum constraint algebra in a discrete Hojman–Kuchař–Teitelboim (HKT) setting. The upstream point-split target module widens the dynamic HKT interface so momentum–Hamiltonian coupling is split across neighboring sites: an unsplit mom_ham field is uninhabitable for honest nearest-neighbor momentum against a frozen quadratic Hamiltonian, because at $n=2$ unsplit advection forces a singular identity when $p_0+p_1=0$.

This module supplies the strong variant of that point-split interface. The Kronecker lapse/shift weight on $\mathbb{Z}/n\mathbb{Z}$ marks a single site; computed advection maps package the discrete Hamiltonian flux from and to a site. Sibling lemmas record that the weight is 1 on the diagonal and 0 off it, and that the named advection fields equal those computed maps. At $n=2$, elementary $\mathbb{Z}/2\mathbb{Z}$ facts (successor never equals the base point; $0+1=1$, $1+1=0$) close the arithmetic.

proof idea

Definition-heavy module, not a single theorem campaign. Site weights are introduced as Kronecker indicators on $\mathbb{Z}/n\mathbb{Z}$, with immediate self/off-diagonal evaluations. Advection-from and advection-to are defined by explicit formulas and then identified with the structure fields of the strong target by rewriting. The $n=2$ layer is pure finite-ring arithmetic: successor inequalities and the two addition tables for $\mathbb{Z}/2\mathbb{Z}$. The strong target structure and the balanced quartic Hamiltonian density are packaged as named definitions for downstream inhabitation, not proved as existence theorems here.

why it matters in Recognition Science

Feeds the gap-5 rigidity kill and the constraint-recovery close path. Downstream HKTCanonicalMomTarget states the binding design: Session A inhabits the strong point-split target at $n=2$ by the balanced quartic falsifier and proves negation of the strong point-split rigidity statement; Session B then installs the repaired canonical-momentum class. Gap5ConstraintCloseStatus binds ledger flags so gap-5 constraint recovery reads closed and the continuum-algebra/HKT-open bits flip false, without import cycles through the full theory ledger. The audit module re-exports this surface for campaign checks. In the Seven Gaps gravity stack this is the strong-target carrier that lets the point-split repair actually host a smooth nearest-neighbor witness the unsplit frozen quadratic could not.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (38)