Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintCloseStatus

show as:
view Lean formalization →

Status ledger for Gap 5 constraint recovery in the seven-gaps quantum-gravity campaign. It records the HKT half as kinetic-normalized ADM shape rigidity on an n=2 lattice point-split target, and keeps continuum GR unpinned. Campaign auditors and the full-theory ledger cite the flag bundle. The module wires named terminals and boolean holds lemmas to upstream rigidity and residual-DAG results rather than proving new continuum physics.

claimGap-5 constraint-close status packages both recovery halves: dynamic Dirac structure functions and HKT rigidity. The HKT half is bound to kinetic-normalized ADM shape rigidity for ContDiff-2 CanonicalMom data on an $n=2$ point-split lattice target (intensivity disclosed; FTC recovery derived). Continuum general relativity is not claimed; the continuum Dirac-algebra limit remains an open terminal.

background

Gap 5 in the seven-gaps QG campaign concerns constraint recovery: dynamic Dirac structure functions together with Hojman–Kuchař–Teitelboim (HKT) rigidity of the ADM generator shape. The residual DAG names those two halves and tracks what is kernel-checked versus open. The campaign ledger records scoped increments only; it does not flip full-strength QGScopeAudit closures.

Upstream work kills over-strong rigidity (point-split strong and mod-vacuum variants) and isolates a kinetic-normalized CanonicalMom class. On that class, rigidity of the ADM shape at lattice size $n=2$ is proved, with FTC recovery of the normalized kinetic term derived rather than assumed. Separately, sampled Hamiltonian dynamics is bound toward a continuum Dirac-algebra terminal, which stays open.

This module sits between those terminals and the audit layer. Historical ledger names such as "Hojman pins GR" are retained as compatibility aliases; the accurate reading is ADM-shape rigidity at $n=2$, not continuum GR.

proof idea

Definition and status module, not a new continuum proof. It aliases the HKT/GR-pin ledger name to the kinetic-normalized $n=2$ ADM-shape rigidity terminal, exposes boolean holds wrappers, and bundles both constraint-recovery halves into a close-status record and flag list. Bindings point at upstream kill-tower and CanonicalMom rigidity theorems; continuum Dirac-algebra limit is referenced as still open. Downstream audit only checks axiom surface and sorry-freedom of these status objects.

why it matters in Recognition Science

Gives the campaign a single honest close-status object for Gap 5 so the full-theory and campaign ledgers can cite scoped progress without overclaiming continuum GR. Feeds Gap5ConstraintCloseStatusAudit, which requires headline status theorems to print in {propext, Classical.choice, Quot.sound} with zero sorryAx. Ties the residual-DAG recovery story to the kinetic-normalized HKT terminal (Wave C4/C5) while leaving the Dirac continuum-limit terminal explicitly open. Landmark contact is classical constraint algebra / ADM hypersurface deformation, not the T0–T8 forcing chain.

scope and limits

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.

declarations in this module (10)