IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTarget

   1import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket
   2import IndisputableMonolith.Gravity.SevenGaps.HKTDynamicTarget
   3
   4/-!
   5# Wave C2 R5 repair: point-split HKT dynamic target
   6
   7The widened Dyn target `HojmanKucharTeitelboimTargetDyn` in
   8`HKTDynamicTarget.lean` keeps an **unsplit** `mom_ham` field. That field is
   9uninhabitable for honest nearest-neighbor local momentum profiles against the
  10**frozen** quadratic Hamiltonian: at `n = 2` unsplit advection forces
  11`(p₀ + p₁) · ∂_d f = p₀² + d²`, which is singular on `p₀ + p₁ = 0`
  12(see `unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam`). Scope is
  13honest and narrow (Codex `D-qg-hkt-pointsplit-adjudication-20260722`); the
  14analogous claim against campaign `HamDyn` is the open Prop
  15`UnsplitMomHamNoSmoothNearestNeighborWitnessHamDyn`. The unsplit Dyn target
  16remains as the falsification-adjacent record; this module is the repaired
  17sibling. The weak `HKTPointSplitTargetDyn` is schema-only after that
  18adjudication; the load-bearing class is `HKTPointSplitTargetDynStrong`.
  19
  20**API adaptation (honest, n = 2).** On `ZMod 2` one has `-1 = 1`, so
  21`DgenSym a ≡ 0` as a functional and `{DgenSym a, ·} = 0` vacuously. The
  22adjudicated `mom_ham_split` sketch written with `DgenSym` is therefore
  23definitionally empty at the HamDyn size. The structure below uses the
  24**smeared point-split momentum density** that already appears in
  25`bracket_HamDyn_HamDyn` / `bracket_Ham_Ham`, with source/target advection
  26densities `hamAdvFrom` / `hamAdvTo`. Finding: that momentum sector is
  27**not** abelian (`mom_mom` carries a Wronskian density, not `0`).
  28
  29No rigidity theorem is proved here. No ledger flag is flipped.
  30-/
  31
  32namespace IndisputableMonolith
  33namespace Gravity
  34namespace SevenGaps
  35namespace HKTPointSplitTarget
  36
  37open HypersurfaceDeformation DynamicStructureBracket DynamicStructureFunctionBlocker
  38open HKTDynamicTarget
  39
  40noncomputable section
  41
  42open Finset
  43
  44private lemma zmod2_zero_add_one : (0 : ZMod 2) + 1 = 1 := by decide
  45private lemma zmod2_one_add_one : (1 : ZMod 2) + 1 = 0 := by decide
  46private lemma zmod2_zero_sub_one : (0 : ZMod 2) - 1 = 1 := by decide
  47private lemma zmod2_one_sub_one : (1 : ZMod 2) - 1 = 0 := by decide
  48
  49lemma sum_zmod2 (g : ZMod 2 → ℝ) : (∑ j : ZMod 2, g j) = g 0 + g 1 := by
  50  have huniv : (univ : Finset (ZMod 2)) = {0, 1} := by decide
  51  rw [huniv, Finset.sum_pair (by decide : (0 : ZMod 2) ≠ 1)]
  52
  53/-! ## No-go: unsplit mom_ham has no smooth local witness at n = 2 -/
  54
  55/-- Local momentum profile class: `m_j = f(d_j, π_j, π_{j+1})` with
  56`d_j = q_{j+1} - q_j`. Translation-covariant by construction. -/
  57abbrev LocalMomProfile : Type := ℝ → ℝ → ℝ → ℝ
  58
  59def momFromProfile (f : LocalMomProfile) (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
  60  f (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))
  61
  62def MomFromProfile (f : LocalMomProfile) (w : ZMod 2 → ℝ) (x : PhaseSpace 2) : ℝ :=
  63  ∑ j : ZMod 2, w j * momFromProfile f x j
  64
  65/-- Canonical frozen quadratic Hamiltonian density. -/
  66def quadraticHamDensity (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
  67  (x.2 j * x.2 j + (x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j)) / 2
  68
  69theorem quadraticHamDensity_smear (N : ZMod 2 → ℝ) :
  70    (fun x : PhaseSpace 2 => ∑ j : ZMod 2, N j * quadraticHamDensity x j) = Ham N := by
  71  funext x
  72  unfold quadraticHamDensity Ham
  73  refine Finset.sum_congr rfl fun j _ => ?_
  74  ring
  75
  76/-- Smoothness package for a local momentum profile (Frechet cell data). -/
  77structure LocalMomSmooth (f : LocalMomProfile) where
  78  fd : LocalMomProfile
  79  fp : LocalMomProfile
  80  fr : LocalMomProfile
  81  hasFDerivCell :
  82    ∀ (j : ZMod 2) (x : PhaseSpace 2),
  83      HasFDerivAt (fun y : PhaseSpace 2 =>
  84          f (y.1 (j + 1) - y.1 j) (y.2 j) (y.2 (j + 1)))
  85        ((fd (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) •
  86            (coordQ (j + 1) - coordQ j) +
  87          (fp (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) • coordP j +
  88          (fr (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) • coordP (j + 1))
  89        x
  90
  91def localMomCellD (f : LocalMomProfile) (S : LocalMomSmooth f) (j : ZMod 2)
  92    (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
  93  (S.fd (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) • (coordQ (j + 1) - coordQ j) +
  94    (S.fp (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) • coordP j +
  95    (S.fr (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) • coordP (j + 1)
  96
  97lemma hasFDerivAt_localMomCell (f : LocalMomProfile) (S : LocalMomSmooth f)
  98    (j : ZMod 2) (x : PhaseSpace 2) :
  99    HasFDerivAt (fun y : PhaseSpace 2 =>
 100        f (y.1 (j + 1) - y.1 j) (y.2 j) (y.2 (j + 1)))
 101      (localMomCellD f S j x) x :=
 102  S.hasFDerivCell j x
 103
 104def MomFromProfileD (f : LocalMomProfile) (S : LocalMomSmooth f)
 105    (w : ZMod 2 → ℝ) (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
 106  ∑ j : ZMod 2, (w j) • localMomCellD f S j x
 107
 108lemma hasFDerivAt_MomFromProfile (f : LocalMomProfile) (S : LocalMomSmooth f)
 109    (w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 110    HasFDerivAt (MomFromProfile f w) (MomFromProfileD f S w x) x := by
 111  unfold MomFromProfile MomFromProfileD momFromProfile
 112  exact HasFDerivAt.fun_sum fun j _ =>
 113    (hasFDerivAt_localMomCell f S j x).const_mul (w j)
 114
 115private lemma localMomCellD_pdir (f : LocalMomProfile) (S : LocalMomSmooth f)
 116    (j k : ZMod 2) (x : PhaseSpace 2) :
 117    localMomCellD f S j x (0, Pi.single k 1)
 118      = S.fp (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1)) *
 119          (if j = k then (1 : ℝ) else 0)
 120        + S.fr (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1)) *
 121          (if j + 1 = k then (1 : ℝ) else 0) := by
 122  simp only [localMomCellD, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
 123    coordQ_apply, coordP_apply, Pi.single_apply, smul_eq_mul]
 124  by_cases hjk : j = k <;> by_cases hjp : j + 1 = k <;> simp [hjk, hjp]
 125
 126private lemma localMomCellD_qdir (f : LocalMomProfile) (S : LocalMomSmooth f)
 127    (j k : ZMod 2) (x : PhaseSpace 2) :
 128    localMomCellD f S j x (Pi.single k 1, 0)
 129      = S.fd (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1)) *
 130          ((if j + 1 = k then (1 : ℝ) else 0) - (if j = k then (1 : ℝ) else 0)) := by
 131  simp only [localMomCellD, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
 132    coordQ_apply, coordP_apply, Pi.single_apply, smul_eq_mul]
 133  by_cases hjk : j = k <;> by_cases hjp : j + 1 = k <;> simp [hjk, hjp]
 134
 135theorem pderivP_MomFromProfile (f : LocalMomProfile) (S : LocalMomSmooth f)
 136    (w : ZMod 2 → ℝ) (k : ZMod 2) (x : PhaseSpace 2) :
 137    pderivP (MomFromProfile f w) k x
 138      = w k * S.fp (x.1 (k + 1) - x.1 k) (x.2 k) (x.2 (k + 1))
 139        + w (k - 1) * S.fr (x.1 k - x.1 (k - 1)) (x.2 (k - 1)) (x.2 k) := by
 140  rw [pderivP, (hasFDerivAt_MomFromProfile f S w x).fderiv, MomFromProfileD,
 141    ContinuousLinearMap.sum_apply]
 142  have step : ∀ j : ZMod 2,
 143      (((w j) • localMomCellD f S j x : PhaseSpace 2 →L[ℝ] ℝ)
 144        ((0, Pi.single k 1) : PhaseSpace 2))
 145      = (w j * S.fp (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) *
 146            (if j = k then (1 : ℝ) else 0)
 147        + (w j * S.fr (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) *
 148            (if j + 1 = k then (1 : ℝ) else 0) := by
 149    intro j
 150    simp only [ContinuousLinearMap.smul_apply, localMomCellD_pdir, smul_eq_mul]
 151    ring
 152  rw [Finset.sum_congr rfl fun j _ => step j, Finset.sum_add_distrib,
 153    sum_mul_ite, sum_mul_ite_add]
 154  have e : k - 1 + 1 = k := by ring
 155  simp only [e]
 156
 157theorem pderivQ_MomFromProfile (f : LocalMomProfile) (S : LocalMomSmooth f)
 158    (w : ZMod 2 → ℝ) (k : ZMod 2) (x : PhaseSpace 2) :
 159    pderivQ (MomFromProfile f w) k x
 160      = w (k - 1) * S.fd (x.1 k - x.1 (k - 1)) (x.2 (k - 1)) (x.2 k)
 161        - w k * S.fd (x.1 (k + 1) - x.1 k) (x.2 k) (x.2 (k + 1)) := by
 162  rw [pderivQ, (hasFDerivAt_MomFromProfile f S w x).fderiv, MomFromProfileD,
 163    ContinuousLinearMap.sum_apply]
 164  have step : ∀ j : ZMod 2,
 165      (((w j) • localMomCellD f S j x : PhaseSpace 2 →L[ℝ] ℝ)
 166        ((Pi.single k 1, 0) : PhaseSpace 2))
 167      = (w j * S.fd (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) *
 168          ((if j + 1 = k then (1 : ℝ) else 0) - (if j = k then (1 : ℝ) else 0)) := by
 169    intro j
 170    simp only [ContinuousLinearMap.smul_apply, localMomCellD_qdir, smul_eq_mul]
 171    ring
 172  rw [Finset.sum_congr rfl fun j _ => step j]
 173  simp only [mul_sub, Finset.sum_sub_distrib]
 174  rw [sum_mul_ite_add (fun j => w j * S.fd (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) 1 k,
 175    sum_mul_ite (fun j => w j * S.fd (x.1 (j + 1) - x.1 j) (x.2 j) (x.2 (j + 1))) k]
 176  have e : k - 1 + 1 = k := by ring
 177  simp only [e]
 178
 179/-- Unsplit Dyn-style advection identity for a local momentum profile against
 180the frozen quadratic Hamiltonian. -/
 181def UnsplitMomHamForProfile (f : LocalMomProfile) : Prop :=
 182  ∀ (w N : ZMod 2 → ℝ) (x : PhaseSpace 2),
 183    bracket (MomFromProfile f w) (Ham N) x
 184      = ∑ j : ZMod 2, (w j * (N (j + 1) - N j)) * quadraticHamDensity x j
 185
 186/-- Forced coefficient identity implied by unsplit advection on the class
 187`m_j = f(d_j, π_j, π_{j+1})`: `(p + r) · ∂_d f = p² + d²`. -/
 188def ForcedUnsplitPartialRelation (fd : LocalMomProfile) : Prop :=
 189  ∀ d p r : ℝ, (p + r) * fd d p r = p * p + d * d
 190
 191/-- THEOREM. The forced unsplit partial relation is unsatisfiable: at
 192`(d, p, r) = (1, 1, -1)` the left side vanishes while the right side is `2`. -/
 193theorem forced_unsplit_partial_relation_impossible (fd : LocalMomProfile) :
 194    ¬ ForcedUnsplitPartialRelation fd := by
 195  intro h
 196  have := h (1 : ℝ) 1 (-1)
 197  norm_num at this
 198
 199/-- Witness phase point for the no-go: `d = 1`, `π₀ = 1`, `π₁ = -1`. -/
 200def unsplitNoGoPhase : PhaseSpace 2 :=
 201  (fun j : ZMod 2 => if j = (0 : ZMod 2) then (0 : ℝ) else 1,
 202    fun j : ZMod 2 => if j = (0 : ZMod 2) then (1 : ℝ) else (-1 : ℝ))
 203
 204def delta0 : ZMod 2 → ℝ := fun j => if j = (0 : ZMod 2) then (1 : ℝ) else 0
 205def delta1 : ZMod 2 → ℝ := fun j => if j = (1 : ZMod 2) then (1 : ℝ) else 0
 206
 207private lemma unsplitNoGo_vals :
 208    unsplitNoGoPhase.1 (0 : ZMod 2) = 0 ∧
 209      unsplitNoGoPhase.1 (1 : ZMod 2) = 1 ∧
 210        unsplitNoGoPhase.2 (0 : ZMod 2) = 1 ∧
 211          unsplitNoGoPhase.2 (1 : ZMod 2) = -1 := by
 212  simp [unsplitNoGoPhase]
 213
 214/-- At the no-go witness with `w = δ₀`,
 215`{Mom, Ham N} = (N₀ + N₁) (-∂_d f + ∂_p f - ∂_r f)`. -/
 216theorem bracket_MomFromProfile_delta0_unsplitNoGo (f : LocalMomProfile)
 217    (S : LocalMomSmooth f) (N : ZMod 2 → ℝ) :
 218    bracket (MomFromProfile f delta0) (Ham N) unsplitNoGoPhase
 219      = (N 0 + N 1) *
 220          (- S.fd (1 : ℝ) 1 (-1) + S.fp (1 : ℝ) 1 (-1) - S.fr (1 : ℝ) 1 (-1)) := by
 221  have hv := unsplitNoGo_vals
 222  have hq0 :
 223      pderivQ (MomFromProfile f delta0) (0 : ZMod 2) unsplitNoGoPhase
 224        = -S.fd (1 : ℝ) 1 (-1) := by
 225    rw [pderivQ_MomFromProfile f S]
 226    simp [delta0, zmod2_zero_add_one, zmod2_zero_sub_one, hv.1, hv.2.1, hv.2.2.1, hv.2.2.2]
 227  have hq1 :
 228      pderivQ (MomFromProfile f delta0) (1 : ZMod 2) unsplitNoGoPhase
 229        = S.fd (1 : ℝ) 1 (-1) := by
 230    rw [pderivQ_MomFromProfile f S]
 231    simp [delta0, zmod2_one_add_one, zmod2_one_sub_one, hv.1, hv.2.1, hv.2.2.1, hv.2.2.2]
 232  have hp0 :
 233      pderivP (MomFromProfile f delta0) (0 : ZMod 2) unsplitNoGoPhase
 234        = S.fp (1 : ℝ) 1 (-1) := by
 235    rw [pderivP_MomFromProfile f S]
 236    simp [delta0, zmod2_zero_add_one, zmod2_zero_sub_one, hv.1, hv.2.1, hv.2.2.1, hv.2.2.2]
 237  have hp1 :
 238      pderivP (MomFromProfile f delta0) (1 : ZMod 2) unsplitNoGoPhase
 239        = S.fr (1 : ℝ) 1 (-1) := by
 240    rw [pderivP_MomFromProfile f S]
 241    simp [delta0, zmod2_one_add_one, zmod2_one_sub_one, hv.1, hv.2.1, hv.2.2.1, hv.2.2.2]
 242  have hQP0 : pderivP (Ham N) (0 : ZMod 2) unsplitNoGoPhase = N 0 * (1 : ℝ) := by
 243    rw [pderivP_Ham, hv.2.2.1]
 244  have hQP1 : pderivP (Ham N) (1 : ZMod 2) unsplitNoGoPhase = N 1 * (-1 : ℝ) := by
 245    rw [pderivP_Ham, hv.2.2.2]
 246  have hQQ0 :
 247      pderivQ (Ham N) (0 : ZMod 2) unsplitNoGoPhase = -(N 0 + N 1) := by
 248    rw [pderivQ_Ham, zmod2_zero_add_one, zmod2_zero_sub_one, hv.1, hv.2.1]
 249    ring
 250  have hQQ1 :
 251      pderivQ (Ham N) (1 : ZMod 2) unsplitNoGoPhase = N 0 + N 1 := by
 252    rw [pderivQ_Ham, zmod2_one_add_one, zmod2_one_sub_one, hv.1, hv.2.1]
 253    ring
 254  unfold bracket
 255  rw [sum_zmod2, hq0, hq1, hp0, hp1, hQP0, hQP1, hQQ0, hQQ1]
 256  ring
 257
 258theorem unsplit_RHS_delta0_unsplitNoGo (N : ZMod 2 → ℝ) :
 259    (∑ j : ZMod 2, (delta0 j * (N (j + 1) - N j)) *
 260        quadraticHamDensity unsplitNoGoPhase j)
 261      = N 1 - N 0 := by
 262  have hv := unsplitNoGo_vals
 263  have hδ : delta0 (0 : ZMod 2) = 1 ∧ delta0 (1 : ZMod 2) = 0 := by
 264    simp [delta0]
 265  have hq0 : quadraticHamDensity unsplitNoGoPhase (0 : ZMod 2) = 1 := by
 266    simp [quadraticHamDensity, zmod2_zero_add_one, hv.1, hv.2.1, hv.2.2.1]
 267  rw [sum_zmod2, hδ.1, hδ.2, zmod2_zero_add_one, zmod2_one_add_one, hq0]
 268  ring
 269
 270/-- THEOREM (scoped no-go). No Frechet-smooth **nearest-neighbor** local
 271momentum profile `m_j = f(d_j, π_j, π_{j+1})` satisfies the unsplit Dyn
 272`mom_ham` identity against the **frozen** quadratic Hamiltonian density
 273`quadraticHamDensity` / `Ham` on `PhaseSpace 2`.
 274
 275At the witness `(d, π₀, π₁) = (1, 1, -1)` with `w = δ₀`, unsplit forces
 276`(N₀ + N₁)(-f_d + f_p - f_r) = N₁ - N₀` for all lapses `N`. Taking
 277`N = δ₀` and `N = δ₁` yields `-f_d + f_p - f_r = -1` and
 278`-f_d + f_p - f_r = 1`, contradiction. Equivalent singular form:
 279`(π₀ + π₁) f_d = π₀² + d²` (see `ForcedUnsplitPartialRelation`).
 280
 281**Does NOT establish:** (i) the same no-go against campaign `HamDyn` /
 282`hamDynDensity`; (ii) a no-go for non-nearest-neighbor momentum profiles;
 283(iii) uninhabitability of every unsplit identity in the widened Dyn target.
 284Those are separate claims; see `UnsplitMomHamNoSmoothNearestNeighborWitnessHamDyn`. -/
 285theorem unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam
 286    (f : LocalMomProfile) (S : LocalMomSmooth f) :
 287    ¬ UnsplitMomHamForProfile f := by
 288  intro hUnsplit
 289  have h0 := hUnsplit delta0 delta0 unsplitNoGoPhase
 290  have h1 := hUnsplit delta0 delta1 unsplitNoGoPhase
 291  rw [bracket_MomFromProfile_delta0_unsplitNoGo f S,
 292    unsplit_RHS_delta0_unsplitNoGo] at h0 h1
 293  have hδ0 : (delta0 (0 : ZMod 2) : ℝ) = 1 ∧ delta0 (1 : ZMod 2) = 0 := by
 294    simp [delta0]
 295  have hδ1 : (delta1 (0 : ZMod 2) : ℝ) = 0 ∧ delta1 (1 : ZMod 2) = 1 := by
 296    simp [delta1]
 297  simp only [hδ0.1, hδ0.2, hδ1.1, hδ1.2] at h0 h1
 298  have h0' : -S.fd (1 : ℝ) 1 (-1) + S.fp (1 : ℝ) 1 (-1) - S.fr (1 : ℝ) 1 (-1) = -1 := by
 299    linarith
 300  have h1' : -S.fd (1 : ℝ) 1 (-1) + S.fp (1 : ℝ) 1 (-1) - S.fr (1 : ℝ) 1 (-1) = 1 := by
 301    linarith
 302  linarith
 303
 304/-- Compatibility alias for ledger claim `C-qg-hkt-unsplit-nogo` and older
 305cross-refs. Prefer the scoped name
 306`unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam`. -/
 307theorem unsplit_mom_ham_no_smooth_local_witness (f : LocalMomProfile)
 308    (S : LocalMomSmooth f) : ¬ UnsplitMomHamForProfile f :=
 309  unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam f S
 310
 311/-! ## Point-split dynamic target (SCHEMA-ONLY after critic) -/
 312
 313/-- SCHEMA-ONLY (demoted). HKT hypotheses with dynamic structure function and
 314**point-split** momentum–Hamiltonian advection.
 315
 316Adaptation from the DgenSym-shaped sketch: at `n = 2`, `DgenSym` vanishes, so
 317`mom_ham_split` is stated for the smeared `momDensity` that `ham_ham` already
 318uses, with source/target split densities. The `mom_mom` field records the
 319**true** (non-abelian) bracket of that sector.
 320
 321**Critic demotion** (`D-qg-hkt-pointsplit-adjudication-20260722`):
 322`hamAdvFrom`/`hamAdvTo` are free record slots and `nondegenerate` only requires
 323some nonzero `hamDensity`. The quartic zero-momentum decoy
 324(`hamDensity = π_j^4`, `momDensity = 0`, decorative `structureFunction`, all
 325advection/bracket densities 0) inhabits this structure. Use
 326`HKTPointSplitTargetDynStrong` for any load-bearing claim or rigidity grind. -/
 327structure HKTPointSplitTargetDyn (n : ℕ) [NeZero n] where
 328  hamDensity : PhaseSpace n → ZMod n → ℝ
 329  momDensity : PhaseSpace n → ZMod n → ℝ
 330  structureFunction : PhaseSpace n → ZMod n → ℝ
 331  /-- Source advection density in
 332  `{D[w], H[N]} = Σ_j w_j (N_{j+1} · hamAdvTo_j - N_j · hamAdvFrom_j)`. -/
 333  hamAdvFrom : PhaseSpace n → ZMod n → ℝ
 334  /-- Target advection density (see `hamAdvFrom`). -/
 335  hamAdvTo : PhaseSpace n → ZMod n → ℝ
 336  /-- Structure density for `{D[v], D[w]}` of smeared `momDensity`
 337  (Wronskian form; not identically zero). -/
 338  momBracketDensity : PhaseSpace n → ZMod n → ℝ
 339  ham_differentiable : ∀ N : ZMod n → ℝ,
 340    Differentiable ℝ (fun x : PhaseSpace n => ∑ j : ZMod n, N j * hamDensity x j)
 341  mom_differentiable : ∀ w : ZMod n → ℝ,
 342    Differentiable ℝ (fun x : PhaseSpace n => ∑ j : ZMod n, w j * momDensity x j)
 343  structure_nonconstant : ¬ PhaseSpaceConstant structureFunction
 344  ham_local : ∀ (x y : PhaseSpace n) (j : ZMod n),
 345    x.1 j = y.1 j → x.1 (j + 1) = y.1 (j + 1) → x.2 j = y.2 j →
 346      hamDensity x j = hamDensity y j
 347  ham_covariant : ∀ (x : PhaseSpace n) (a j : ZMod n),
 348    hamDensity (fun i => x.1 (i + a), fun i => x.2 (i + a)) j = hamDensity x (j + a)
 349  structure_local : ∀ (x y : PhaseSpace n) (j : ZMod n),
 350    x.1 j = y.1 j → structureFunction x j = structureFunction y j
 351  /-- Finding: smeared point-split `momDensity` is not abelian. -/
 352  mom_mom : ∀ (v w : ZMod n → ℝ) (x : PhaseSpace n),
 353    bracket (fun y => ∑ j : ZMod n, v j * momDensity y j)
 354      (fun y => ∑ j : ZMod n, w j * momDensity y j) x
 355      = ∑ j : ZMod n,
 356          (v j * w (j + 1) - w j * v (j + 1)) * momBracketDensity x j
 357  /-- Point-split advection (repairs unsplit Dyn `mom_ham`). -/
 358  mom_ham_split : ∀ (w N : ZMod n → ℝ) (x : PhaseSpace n),
 359    bracket (fun y => ∑ j : ZMod n, w j * momDensity y j)
 360      (fun y => ∑ j : ZMod n, N j * hamDensity y j) x
 361      = ∑ j : ZMod n, w j * (N (j + 1) * hamAdvTo x j - N j * hamAdvFrom x j)
 362  ham_ham : ∀ (N M : ZMod n → ℝ) (x : PhaseSpace n),
 363    bracket (fun y => ∑ j : ZMod n, N j * hamDensity y j)
 364      (fun y => ∑ j : ZMod n, M j * hamDensity y j) x
 365      = ∑ j : ZMod n,
 366          (N j * M (j + 1) - M j * N (j + 1)) *
 367            (structureFunction x j * momDensity x j)
 368  /-- Excludes the zero-density junk inhabitant. -/
 369  nondegenerate : ∃ (x : PhaseSpace n) (j : ZMod n), hamDensity x j ≠ 0
 370
 371/-- Convenience: pack source/target densities into a single slot keyed by a
 372shift `a` (DgenSym-shaped packaging). At `n = 2` this is documentary only:
 373`DgenSym` itself vanishes. -/
 374def hamAdvectionSplit {n : ℕ} [NeZero n] (T : HKTPointSplitTargetDyn n)
 375    (x : PhaseSpace n) (a j : ZMod n) : ℝ :=
 376  if a = 1 then (T.hamAdvTo x j + T.hamAdvFrom x j) / 2 else 0
 377
 378/-! ## Honest HamDyn inhabitant at n = 2 -/
 379
 380def hamDynDensity (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
 381  (x.2 j * x.2 j +
 382      (1 + x.1 j * x.1 j) *
 383        ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) / 2
 384
 385/-! ### Open HamDyn-level unsplit no-go (stated, not proved) -/
 386
 387/-- Unsplit Dyn-style advection identity for a local momentum profile against
 388the campaign `HamDyn` density (`hamDynDensity`), not the frozen quadratic. -/
 389def UnsplitMomHamForProfileDyn (f : LocalMomProfile) : Prop :=
 390  ∀ (w N : ZMod 2 → ℝ) (x : PhaseSpace 2),
 391    bracket (MomFromProfile f w) (HamDyn N) x
 392      = ∑ j : ZMod 2, (w j * (N (j + 1) - N j)) * hamDynDensity x j
 393
 394/-- OPEN TARGET (DEFINED only; not proved). The HamDyn-level analogue of
 395`unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam`: no Frechet-smooth
 396nearest-neighbor profile satisfies unsplit advection against `HamDyn`.
 397
 398Honest effort note (Codex repair 2026-07-22): the frozen proof uses that at the
 399witness the LHS factorizes as `(N₀+N₁)·scalar` while the RHS is `N₁-N₀`. Against
 400`HamDyn` the configuration partials break that factorization, so the same
 401two-lapse contradiction does not transport. Do **not** cite this Prop as a
 402theorem until a proof lands. -/
 403def UnsplitMomHamNoSmoothNearestNeighborWitnessHamDyn : Prop :=
 404  ∀ (f : LocalMomProfile) (_S : LocalMomSmooth f), ¬ UnsplitMomHamForProfileDyn f
 405
 406def momDynDensity (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
 407  x.2 (j + 1) * (x.1 (j + 1) - x.1 j)
 408
 409def structureDyn (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
 410  1 + x.1 j * x.1 j
 411
 412/-- TRUE source advection density for `{MomDyn w, HamDyn N}` at `n = 2`. -/
 413def hamDynAdvFrom (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
 414  x.2 j * x.2 (j + 1) +
 415    (1 + x.1 j * x.1 j) * ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))
 416
 417/-- TRUE target advection density for `{MomDyn w, HamDyn N}` at `n = 2`. -/
 418def hamDynAdvTo (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
 419  x.2 (j + 1) * x.2 (j + 1) -
 420    (1 + x.1 (j + 1) * x.1 (j + 1)) *
 421      ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j)) -
 422    x.1 (j + 1) *
 423      ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))
 424
 425/-- TRUE `{Mom, Mom}` Wronskian density at `n = 2`. -/
 426def momDynBracketDensity (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
 427  ((x.1 (j + 1) - x.1 j) * (x.2 j + x.2 (j + 1))) / 2
 428
 429def MomDyn (w : ZMod 2 → ℝ) (x : PhaseSpace 2) : ℝ :=
 430  ∑ j : ZMod 2, w j * momDynDensity x j
 431
 432theorem hamDynDensity_smear (N : ZMod 2 → ℝ) :
 433    (fun x : PhaseSpace 2 => ∑ j : ZMod 2, N j * hamDynDensity x j) = HamDyn N := by
 434  funext x
 435  unfold hamDynDensity HamDyn
 436  refine Finset.sum_congr rfl fun j _ => ?_
 437  ring
 438
 439theorem structureDyn_eq_concrete (x : PhaseSpace 2) (j : ZMod 2) :
 440    structureDyn x j = concreteDynamicInverseMetric x j := by
 441  simp [structureDyn, concreteDynamicInverseMetric, pow_two]
 442
 443theorem MomDyn_closed (w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 444    MomDyn w x = (x.1 1 - x.1 0) * (w 0 * x.2 1 - w 1 * x.2 0) := by
 445  unfold MomDyn momDynDensity
 446  simp only [sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
 447  ring
 448
 449/-- Product-rule order matching `HasFDerivAt.mul`: `f x • g' + g x • f'`. -/
 450def MomDynD (w : ZMod 2 → ℝ) (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
 451  (x.1 1 - x.1 0) • (w 0 • coordP 1 - w 1 • coordP 0) +
 452    (w 0 * x.2 1 - w 1 * x.2 0) • (coordQ 1 - coordQ 0)
 453
 454lemma hasFDerivAt_MomDyn (w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 455    HasFDerivAt (MomDyn w) (MomDynD w x) x := by
 456  -- Match the Pi-sub form produced by `HasFDerivAt.sub` / `.mul`.
 457  have hform :
 458      MomDyn w =
 459        ((fun y : PhaseSpace 2 => y.1 1) - fun y => y.1 0) *
 460          ((fun y => w 0 * y.2 1) - fun y => w 1 * y.2 0) := by
 461    funext y
 462    dsimp [Pi.sub_apply]
 463    exact MomDyn_closed w y
 464  rw [hform]
 465  exact (((hasFDerivAt_coord_fst (1 : ZMod 2) x).sub (hasFDerivAt_coord_fst 0 x)).mul
 466    (((hasFDerivAt_coord_snd (1 : ZMod 2) x).const_mul (w 0)).sub
 467      ((hasFDerivAt_coord_snd (0 : ZMod 2) x).const_mul (w 1))))
 468
 469theorem differentiable_MomDyn (w : ZMod 2 → ℝ) : Differentiable ℝ (MomDyn w) :=
 470  fun x => (hasFDerivAt_MomDyn w x).differentiableAt
 471
 472theorem pderivQ_MomDyn_zero (w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 473    pderivQ (MomDyn w) (0 : ZMod 2) x = -(w 0 * x.2 1 - w 1 * x.2 0) := by
 474  rw [pderivQ, (hasFDerivAt_MomDyn w x).fderiv, MomDynD]
 475  simp [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, coordQ_apply,
 476    coordP_apply]
 477
 478theorem pderivQ_MomDyn_one (w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 479    pderivQ (MomDyn w) (1 : ZMod 2) x = w 0 * x.2 1 - w 1 * x.2 0 := by
 480  rw [pderivQ, (hasFDerivAt_MomDyn w x).fderiv, MomDynD]
 481  simp [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, coordQ_apply,
 482    coordP_apply]
 483
 484theorem pderivP_MomDyn_zero (w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 485    pderivP (MomDyn w) (0 : ZMod 2) x = (x.1 1 - x.1 0) * (-w 1) := by
 486  rw [pderivP, (hasFDerivAt_MomDyn w x).fderiv, MomDynD]
 487  simp [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, coordQ_apply,
 488    coordP_apply]
 489
 490theorem pderivP_MomDyn_one (w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 491    pderivP (MomDyn w) (1 : ZMod 2) x = (x.1 1 - x.1 0) * w 0 := by
 492  rw [pderivP, (hasFDerivAt_MomDyn w x).fderiv, MomDynD]
 493  simp [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, coordQ_apply,
 494    coordP_apply]
 495
 496theorem bracket_MomDyn_MomDyn (v w : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 497    bracket (MomDyn v) (MomDyn w) x
 498      = ∑ j : ZMod 2,
 499          (v j * w (j + 1) - w j * v (j + 1)) * momDynBracketDensity x j := by
 500  have hL :
 501      bracket (MomDyn v) (MomDyn w) x =
 502        (pderivQ (MomDyn v) (0 : ZMod 2) x * pderivP (MomDyn w) (0 : ZMod 2) x -
 503            pderivP (MomDyn v) (0 : ZMod 2) x * pderivQ (MomDyn w) (0 : ZMod 2) x) +
 504          (pderivQ (MomDyn v) (1 : ZMod 2) x * pderivP (MomDyn w) (1 : ZMod 2) x -
 505            pderivP (MomDyn v) (1 : ZMod 2) x * pderivQ (MomDyn w) (1 : ZMod 2) x) := by
 506    unfold bracket
 507    rw [sum_zmod2]
 508  have hR :
 509      (∑ j : ZMod 2,
 510          (v j * w (j + 1) - w j * v (j + 1)) * momDynBracketDensity x j) =
 511        (v 0 * w 1 - w 0 * v 1) * momDynBracketDensity x 0 +
 512          (v 1 * w 0 - w 1 * v 0) * momDynBracketDensity x 1 := by
 513    rw [sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
 514  rw [hL, hR, pderivQ_MomDyn_zero v x, pderivQ_MomDyn_zero w x, pderivQ_MomDyn_one v x,
 515    pderivQ_MomDyn_one w x, pderivP_MomDyn_zero v x, pderivP_MomDyn_zero w x,
 516    pderivP_MomDyn_one v x, pderivP_MomDyn_one w x]
 517  simp only [momDynBracketDensity, zmod2_zero_add_one, zmod2_one_add_one]
 518  ring
 519
 520set_option maxHeartbeats 800000 in
 521theorem bracket_MomDyn_HamDyn (w N : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 522    bracket (MomDyn w) (HamDyn N) x
 523      = ∑ j : ZMod 2, w j * (N (j + 1) * hamDynAdvTo x j - N j * hamDynAdvFrom x j) := by
 524  have hL :
 525      bracket (MomDyn w) (HamDyn N) x =
 526        (pderivQ (MomDyn w) (0 : ZMod 2) x * pderivP (HamDyn N) (0 : ZMod 2) x -
 527            pderivP (MomDyn w) (0 : ZMod 2) x * pderivQ (HamDyn N) (0 : ZMod 2) x) +
 528          (pderivQ (MomDyn w) (1 : ZMod 2) x * pderivP (HamDyn N) (1 : ZMod 2) x -
 529            pderivP (MomDyn w) (1 : ZMod 2) x * pderivQ (HamDyn N) (1 : ZMod 2) x) := by
 530    unfold bracket
 531    rw [sum_zmod2]
 532  have hR :
 533      (∑ j : ZMod 2, w j * (N (j + 1) * hamDynAdvTo x j - N j * hamDynAdvFrom x j)) =
 534        w 0 * (N 1 * hamDynAdvTo x 0 - N 0 * hamDynAdvFrom x 0) +
 535          w 1 * (N 0 * hamDynAdvTo x 1 - N 1 * hamDynAdvFrom x 1) := by
 536    rw [sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
 537  -- Expand every partial, then every Adv density, with ZMod 2 arithmetic frozen.
 538  have hQ0 := pderivQ_HamDyn N (0 : ZMod 2) x
 539  have hQ1 := pderivQ_HamDyn N (1 : ZMod 2) x
 540  have hP0 := pderivP_HamDyn N (0 : ZMod 2) x
 541  have hP1 := pderivP_HamDyn N (1 : ZMod 2) x
 542  rw [hL, hR, pderivQ_MomDyn_zero w x, pderivQ_MomDyn_one w x, pderivP_MomDyn_zero w x,
 543    pderivP_MomDyn_one w x, hP0, hP1, hQ0, hQ1]
 544  -- Rewrite ZMod shifts before unfolding Adv (keeps ring's monomial count down).
 545  simp only [zmod2_zero_add_one, zmod2_one_add_one, zmod2_zero_sub_one, zmod2_one_sub_one]
 546  unfold hamDynAdvFrom hamDynAdvTo
 547  simp only [zmod2_zero_add_one, zmod2_one_add_one]
 548  -- Sympy-checked identity: LHS - RHS = 0 as a polynomial in the 8 scalars.
 549  ring
 550
 551theorem structureDyn_not_constant : ¬ PhaseSpaceConstant structureDyn := by
 552  intro h
 553  have hEq := h zeroPhasePoint unitConfigurationPoint (0 : ZMod 2)
 554  simp only [structureDyn, zeroPhasePoint, unitConfigurationPoint] at hEq
 555  norm_num at hEq
 556
 557def hamDynNondegPhase : PhaseSpace 2 :=
 558  (fun _ => (0 : ℝ), fun j => if j = (0 : ZMod 2) then (1 : ℝ) else 0)
 559
 560theorem hamDynDensity_nondeg :
 561    hamDynDensity hamDynNondegPhase (0 : ZMod 2) ≠ 0 := by
 562  simp only [hamDynDensity, hamDynNondegPhase]
 563  norm_num
 564
 565/-- THEOREM. Honest HamDyn inhabitant of the repaired point-split Dyn target. -/
 566def hamDynPointSplitTarget : HKTPointSplitTargetDyn 2 where
 567  hamDensity := hamDynDensity
 568  momDensity := momDynDensity
 569  structureFunction := structureDyn
 570  hamAdvFrom := hamDynAdvFrom
 571  hamAdvTo := hamDynAdvTo
 572  momBracketDensity := momDynBracketDensity
 573  ham_differentiable := by
 574    intro N
 575    simpa [hamDynDensity_smear] using differentiable_HamDyn N
 576  mom_differentiable := differentiable_MomDyn
 577  structure_nonconstant := structureDyn_not_constant
 578  ham_local := by
 579    intro x y j hx0 hx1 hp
 580    dsimp only [hamDynDensity]
 581    rw [hx0, hx1, hp]
 582  ham_covariant := by
 583    intro x a j
 584    unfold hamDynDensity
 585    have e1 : (j + a + 1 : ZMod 2) = j + 1 + a := by ring
 586    simp only [e1]
 587  structure_local := by
 588    intro x y j hx
 589    dsimp only [structureDyn]
 590    rw [hx]
 591  mom_mom := by
 592    intro v w x
 593    simpa [MomDyn] using bracket_MomDyn_MomDyn v w x
 594  mom_ham_split := by
 595    intro w N x
 596    simpa [MomDyn, hamDynDensity_smear] using bracket_MomDyn_HamDyn w N x
 597  ham_ham := by
 598    intro N M x
 599    have h := bracket_HamDyn_HamDyn N M x
 600    -- Rewrite densities by closed forms; avoid open-ended simp on ZMod.
 601    simp only [hamDynDensity_smear, structureDyn, momDynDensity, concreteDynamicInverseMetric,
 602      pow_two] at h ⊢
 603    exact h
 604  nondegenerate := ⟨hamDynNondegPhase, (0 : ZMod 2), hamDynDensity_nondeg⟩
 605
 606theorem hktPointSplitTargetDyn_two_nonvacuous : Nonempty (HKTPointSplitTargetDyn 2) :=
 607  ⟨hamDynPointSplitTarget⟩
 608
 609/-- Documentary: `DgenSym` vanishes on two sites, so a DgenSym-shaped
 610`mom_ham_split` would be vacuous. -/
 611theorem DgenSym_eq_zero_two (a : ZMod 2) (x : PhaseSpace 2) : DgenSym a x = 0 := by
 612  unfold DgenSym
 613  refine Finset.sum_eq_zero fun i _ => ?_
 614  have h : (i + a : ZMod 2) = i - a := by
 615    -- on ZMod 2, a = -a for all a
 616    have : a + a = (0 : ZMod 2) := by
 617      fin_cases a <;> decide
 618    calc i + a = i + a := rfl
 619      _ = i - a + (a + a) := by ring
 620      _ = i - a + 0 := by rw [this]
 621      _ = i - a := by ring
 622  simp [h]
 623
 624/-- Zero-density junk fails `nondegenerate` by construction. -/
 625theorem zero_density_fails_nondegenerate :
 626    ¬ ∃ (_x : PhaseSpace 2) (_j : ZMod 2), (0 : ℝ) ≠ 0 := by
 627  rintro ⟨_, _, h⟩
 628  exact h rfl
 629
 630/-! ## Binding rigidity Prop (DEMOTED: weak class) -/
 631
 632/-- DEMOTED (likely false). Quantifies over the WEAK schema
 633`HKTPointSplitTargetDyn`, which the quartic zero-momentum decoy inhabits
 634(`quarticZeroMomTarget` in `HKTPointSplitStrong`). Critic finding
 635`D-qg-hkt-pointsplit-adjudication-20260722`: the n=1 quartic disease is
 636reproduced at n=2 over this class. Binding rigidity is
 637`HKTRigidityStatementPointSplitDynN2Strong`. -/
 638def HKTRigidityStatementPointSplitDynN2 : Prop :=
 639  ∀ T : HKTPointSplitTargetDyn 2,
 640    ∃ cKin cGrad cVac : ℝ, ∀ (x : PhaseSpace 2) (j : ZMod 2),
 641      T.hamDensity x j
 642        = cKin * (x.2 j * x.2 j)
 643          + cGrad *
 644              (T.structureFunction x j *
 645                ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j)))
 646          + cVac
 647
 648/-! ### Axiom receipts -/
 649
 650#print axioms forced_unsplit_partial_relation_impossible
 651#print axioms unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam
 652#print axioms unsplit_mom_ham_no_smooth_local_witness
 653#print axioms bracket_MomDyn_MomDyn
 654#print axioms bracket_MomDyn_HamDyn
 655#print axioms hktPointSplitTargetDyn_two_nonvacuous
 656#print axioms DgenSym_eq_zero_two
 657
 658end
 659end HKTPointSplitTarget
 660end SevenGaps
 661end Gravity
 662end IndisputableMonolith
 663