Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong

show as:
view Lean formalization →

Module defining the strong point-split Hojman–Kuchař–Teitelboim dynamic target on cyclic lattices, with site-to-site Kronecker weights, explicit Hamiltonian advection maps, and a balanced quartic density. Gravity/gap5 workers cite it to inhabit the n=2 strong target and kill the strong rigidity claim. Structure is definitions plus elementary ZMod-2 identities equating computed advection to the abstract fields.

claimOn $\mathbb{Z}/n\mathbb{Z}$, introduce Kronecker site weights $\delta(i,j)$, computed Hamiltonian advection maps (from/to), and the strong point-split HKT dynamic target whose momentum–Hamiltonian coupling is realized by a balanced quartic density rather than an unsplit quadratic form. At $n=2$ the $\mathbb{Z}/2\mathbb{Z}$ successor identities make the computed advection match the abstract fields.

background

Recognition Science gap5 work repairs the continuum Hojman–Kuchař–Teitelboim (HKT) constraint algebra on discrete cyclic lattices. The upstream module HKTPointSplitTarget widens the dynamic target by splitting the momentum–Hamiltonian field: an unsplit mom_ham is uninhabitable for honest nearest-neighbor local momentum against a frozen quadratic Hamiltonian, since at $n=2$ unsplit advection forces $(p_0+p_1)\partial_d f=p_0^2+d^2$, singular on $p_0+p_1=0$.

This module sits one layer stronger. It supplies site Kronecker lapse/shift weights on $\mathbb{Z}/n\mathbb{Z}$, explicit computed advection (from and to), and the strong dynamic target class together with a quartic Hamiltonian density. Elementary $\mathbb{Z}/2\mathbb{Z}$ arithmetic (successor inequalities and $0+1$, $1+1$ reductions) underwrites the $n=2$ specializations used downstream.

proof idea

Definition-heavy module, not a single theorem. It introduces site delta weights and proves reflexivity/inequality lemmas; defines computed Hamiltonian advection maps and equates them to the abstract advection fields of the strong target; records $\mathbb{Z}/2\mathbb{Z}$ successor and addition identities needed at $n=2$; and packages HKTPointSplitTargetDynStrong with the balanced quartic density quarticHamDensity2. No deep analytic argument: the content is interface construction plus short algebraic equalities.

why it matters in Recognition Science

Feeds three gap5 closers. HKTCanonicalMomTarget (Wave C2) inhabits HKTPointSplitTargetDynStrong 2 via the balanced quartic falsifier and proves negation of the strong point-split rigidity statement at $n=2$, per design route D-qg-hkt-rigidity-route-20260722. Gap5ConstraintCloseStatus (Wave C5) binds ledger flags so gap5_constraint_recovery is true and both gap5_continuum_algebra_hkt_open and hktRigidityOpen flip false without import cycles. HKTPointSplitStrongAudit audits the strong target surface. Without this strong split and quartic density, the unsplit frozen-quadratic obstruction blocks honest nearest-neighbor witnesses and leaves gap5 rigidity open.

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)