module module high

`IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTarget`

Defines the local momentum profile class for the HKT point-split target: cell momenta of the form m_j = f(d_j, π_j, π_{j+1}) with link differences d_j = q_{j+1} - q_j, translation-covariant by construction. Supplies Z/2 arithmetic lemmas, quadratic Hamiltonian density, and smearing maps used by the strengthened point-split target. Downstream rigidity and audit modules import this class as the admissible momentum ansatz.

claimA local momentum profile is a map $m_j = f(d_j, \pi_j, \pi_{j+1})$ on two-site cells, where $d_j = q_{j+1} - q_j$. The module packages this class together with the induced momentum density, quadratic Hamiltonian density (and its smear), and elementary $\mathbb{Z}/2\mathbb{Z}$ identities used in point-split bookkeeping.

background

Wave C2 of the gravity gap program widens the HKT target so the structure function $g$ is dynamic rather than frozen. The upstream module HKTDynamicTarget records that folding $g$ into a frozen momDensity and claiming GR unit structure was rejected; the widened target carries an explicit structureFunction slot with a nonconstancy hypothesis. DynamicStructureBracket closes the first typed residuals (R0 decoy and R1) for the two-site structure-function bracket: the naive plug-in of $g$ into the frozen HamW slot leaves an uncompensated $\partial g/\partial q$ term.

Against that background this module isolates the admissible local momentum ansatz. Cell momenta depend only on the link difference $d_j$ and the two endpoint momenta $\pi_j,\pi_{j+1}$, so rigid translations of the configuration leave $m$ invariant by construction. Supporting material includes $\mathbb{Z}/2$ sum and shift identities, the map from a profile $f$ to a momentum density, quadratic Hamiltonian density on cells, and a smoothness predicate on local momentum.

proof idea

This is a definition and lemma module, not a rigidity proof. It introduces the LocalMomProfile class and the derived maps momFromProfile, quadraticHamDensity, and quadraticHamDensity_smear, plus small $\mathbb{Z}/2\mathbb{Z}$ arithmetic facts (zero/one add and sub, sum_zmod2) used when indexing point-split cells. No load-bearing HKT identity is proved here; the objects are wired for import by the strengthened target and its audit.

why it matters in Recognition Science

Feeds HKTPointSplitStrong, which replaces the decoy-inhabitable weak point-split target with HKTPointSplitTargetDynStrong (load-bearing momentum, advection tied to the dynamic structure). Also imported by HKTPointSplitTargetAudit. In the Wave C2 residual DAG this sits between the dynamic-structure groundwork (R0/R1 bracket, R5/R6 widened HKT target) and the repaired point-split rigidity goal: without a translation-covariant local momentum class, the strong target has nothing admissible to quantify over. It does not itself discharge HKT rigidity; it supplies the profile language that makes the strong target well-posed.

scope and limits

Does not prove HKT rigidity or any continuum GR limit.
Does not exclude decoy profiles; that is deferred to the strong target module.
Does not fix a unique $f$; only the local functional dependence class.
Does not treat structure-function dynamics beyond importing the widened target.
Does not claim the original frozen HKTRigidityStatement holds at $n=1$.

used by (2)

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

IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong module_import
IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTargetAudit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket module_import
IndisputableMonolith.Gravity.SevenGaps.HKTDynamicTarget module_import

declarations in this module (62)

lemma zmod2_zero_add_one L44
lemma zmod2_one_add_one L45
lemma zmod2_zero_sub_one L46
lemma zmod2_one_sub_one L47
lemma sum_zmod2 L49
abbrev LocalMomProfile L57
def momFromProfile L59
def MomFromProfile L62
def quadraticHamDensity L66
theorem quadraticHamDensity_smear L69
structure LocalMomSmooth L77
def localMomCellD L91
lemma hasFDerivAt_localMomCell L97
def MomFromProfileD L104
lemma hasFDerivAt_MomFromProfile L108
lemma localMomCellD_pdir L115
lemma localMomCellD_qdir L126
theorem pderivP_MomFromProfile L135
theorem pderivQ_MomFromProfile L157
def UnsplitMomHamForProfile L181
def ForcedUnsplitPartialRelation L188
theorem forced_unsplit_partial_relation_impossible L193
def unsplitNoGoPhase L200
def delta0 L204
def delta1 L205
lemma unsplitNoGo_vals L207
theorem bracket_MomFromProfile_delta0_unsplitNoGo L216
theorem unsplit_RHS_delta0_unsplitNoGo L258
theorem unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam L285
theorem unsplit_mom_ham_no_smooth_local_witness L307
structure HKTPointSplitTargetDyn L327
def hamAdvectionSplit L374
def hamDynDensity L380
def UnsplitMomHamForProfileDyn L389
theorem until L402
def UnsplitMomHamNoSmoothNearestNeighborWitnessHamDyn L403
def momDynDensity L406
def structureDyn L409
def hamDynAdvFrom L413
def hamDynAdvTo L418
def momDynBracketDensity L426
def MomDyn L429
theorem hamDynDensity_smear L432
theorem structureDyn_eq_concrete L439
theorem MomDyn_closed L443
def MomDynD L450
lemma hasFDerivAt_MomDyn L454
theorem differentiable_MomDyn L469
theorem pderivQ_MomDyn_zero L472
theorem pderivQ_MomDyn_one L478
theorem pderivP_MomDyn_zero L484
theorem pderivP_MomDyn_one L490
theorem bracket_MomDyn_MomDyn L496
theorem bracket_MomDyn_HamDyn L521
theorem structureDyn_not_constant L551
def hamDynNondegPhase L557
theorem hamDynDensity_nondeg L560
def hamDynPointSplitTarget L566
theorem hktPointSplitTargetDyn_two_nonvacuous L606
theorem DgenSym_eq_zero_two L611
theorem zero_density_fails_nondegenerate L625
def HKTRigidityStatementPointSplitDynN2 L638