module module high

`IndisputableMonolith.Gravity.SevenGaps.HypersurfaceDeformation`

Canonical phase space for a lattice wave field on the periodic n-site ring: configuration q and conjugate momentum π as real-valued functions on Z/nZ. Gravity and QG campaign modules import it to define Poisson brackets, partials, and HKT-style hypersurface deformation algebra. The file is a pure model layer: types, coordinate projections, and finite-sum reindexing lemmas, with no dynamical theorems.

claimOn the periodic lattice with $n$ sites, the phase space is the product of configuration and momentum maps $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Coordinate projections, $q$- and $p$-partials, the Poisson bracket, and elementary finite-sum identities (shift, reindex, multiply-by-indicator) are defined on this space.

background

Recognition Science gravity work treats discrete hypersurface deformation on a periodic lattice before continuum GR is recovered. The model object is the phase space of a lattice wave field: configuration $q$ and conjugate momentum $\pi$ as real functions on $\mathbb{Z}/n\mathbb{Z}$.

Sibling definitions supply the working calculus: coordinate maps coordQ/coordP, partials in the $q$ and $p$ directions, and a Poisson bracket built from those partials. Supporting lemmas are pure finite-sum bookkeeping (cyclic shift, reindexing, multiplication by indicators) needed to move discrete derivatives through sums without analysis.

The module sits under the Seven-Gaps gravity campaign. Downstream files use this phase space as the carrier for Hojman–Kuchař–Teitelboim (HKT) targets, local functional equations, and residual DAGs aimed at gap-5 constraint recovery.

proof idea

This is a definition and lemma module, not a theorem package. It introduces the phase-space type, coordinate and partial operators, the bracket, and a short suite of Finset.sum identities (shift, reindex, multiply-by-ite). There is no dynamical claim and no rigidity or continuum limit proved here; later modules import the carrier and the sum lemmas.

why it matters in Recognition Science

Every Wave C2/D attack on gap-5 constraint recovery needs a fixed discrete phase space before structure functions or HKT rigidity can be stated. This module supplies that carrier.

It is imported by HKTDynamicTarget (widened HKT target with dynamic structure function), HKTLocalFunctionalEquation (local-profile reduction at $n=2$), and HKTOneSiteCounterexample (which shows the original rigidity statement fails at $n=1$). Residual and ledger modules (Gap5ConstraintResidualDAG, Gap5ConstraintCloseStatus, CampaignLedger) and WeightedHypersurfaceBracket also import it so bracket and deformation algebra sit on one shared model.

In the campaign ledger sense it is infrastructure: it does not flip any full-strength QGScopeAudit flag, but without it the HKT residual DAG and continuum-algebra open items have no typed home.

scope and limits

Does not prove HKT rigidity, constraint recovery, or any continuum GR limit.
Does not fix a Hamiltonian, structure function, or dynamics on the phase space.
Does not claim the one-site or multi-site rigidity statements; those live downstream.
Does not flip Seven-Gaps or QGScopeAudit closure flags.
Does not address continuum $n\to\infty$ analysis or renormalization.

used by (7)

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

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintCloseStatus module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintResidualDAG module_import
IndisputableMonolith.Gravity.SevenGaps.HKTDynamicTarget module_import
IndisputableMonolith.Gravity.SevenGaps.HKTLocalFunctionalEquation module_import
IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexample module_import
IndisputableMonolith.Gravity.SevenGaps.WeightedHypersurfaceBracket module_import

declarations in this module (65)

abbrev PhaseSpace L106
def coordQ L111
def coordP L115
lemma coordQ_apply L119
lemma coordP_apply L122
def pderivQ L128
def pderivP L133
def bracket L141
lemma sum_shift L147
lemma sum_reindex L152
lemma sum_mul_ite L158
lemma sum_mul_ite_add L168
lemma sum_mul_ite_sub L184
theorem bracket_antisymm L206
theorem bracket_self L214
lemma pderivQ_fun_add L219
lemma pderivP_fun_add L224
lemma pderivQ_const_mul L229
lemma pderivP_const_mul L234
lemma pderivQ_fun_mul L239
lemma pderivP_fun_mul L244
theorem bracket_add_left L251
theorem bracket_add_right L259
theorem bracket_const_mul_left L269
theorem bracket_const_mul_right L276
theorem bracket_mul_left L286
theorem bracket_mul_right L294
def JacobiOn L307
lemma hasFDerivAt_coord_fst L313
lemma hasFDerivAt_coord_snd L317
theorem bracket_coordQ_coordP L322
theorem bracket_coordQ_coordQ L362
theorem bracket_coordP_coordP L376
def Dgen L398
def DgenSym L406
def Ham L411
lemma Ham_eq_sq L415
lemma DgenSym_eq L421
def DgenD L432
lemma hasFDerivAt_Dgen L436
theorem differentiable_Dgen L444
def DgenSymD L448
lemma hasFDerivAt_DgenSym L453
theorem differentiable_DgenSym L462
def HamD L466
lemma hasFDerivAt_Ham L472
theorem differentiable_Ham L482
lemma pderivQ_Dgen L487
lemma pderivP_Dgen L500
lemma pderivQ_DgenSym L511
lemma pderivP_DgenSym L527
lemma pderivP_Ham L540
lemma pderivQ_Ham L555
theorem bracket_Dgen_Dgen L584
theorem bracket_DgenSym_DgenSym L624
theorem bracket_Dgen_Ham L698
theorem bracket_Dgen_Ham_one L732
theorem bracket_DgenSym_Ham L782
theorem bracket_DgenSym_Ham_one L861
theorem bracket_Ham_one_DgenSym L867
theorem bracket_Ham_Ham L883
structure below L911
structure function L925
structure HojmanKucharTeitelboimTarget L928
def HKTRigidityStatement L971