IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexample

   1import IndisputableMonolith.Gravity.SevenGaps.HypersurfaceDeformation
   2
   3/-!
   4# Wave C2 R5/R6 groundwork: HKT rigidity falsified as stated (n = 1)
   5
   6Codex adjudication (`D-gap5-hkt-design-20260722`) found that
   7`HKTRigidityStatement` is **false as stated**: on the degenerate one-site
   8lattice `ZMod 1`, every discrete difference and Wronskian vanishes, so a
   9quartic kinetic density with zero momentum density satisfies every field of
  10`HojmanKucharTeitelboimTarget 1` while escaping the quadratic pin.
  11
  12This module lands that counterexample against the real fderiv bracket. It does
  13**not** flip `gap5_constraint_recovery` and does **not** prove any rigidity
  14statement.
  15
  16The ledger terminal `hojman_pins_general_relativity` must bind to a repaired
  17statement (`HKTRigidityStatementDyn`, or an n-restricted + nondegenerate form),
  18with this counterexample disclosed.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Gravity
  23namespace SevenGaps
  24namespace HKTOneSiteCounterexample
  25
  26open HypersurfaceDeformation
  27
  28noncomputable section
  29
  30open Finset
  31
  32/-! ## Quartic one-site densities -/
  33
  34/-- MODEL. Quartic kinetic density on one site: `h_j = π_j^4`. -/
  35def quarticHamDensity (x : PhaseSpace 1) (j : ZMod 1) : ℝ :=
  36  (x.2 j) ^ 4
  37
  38/-- MODEL. Vanishing momentum density. -/
  39def zeroMomDensity (_x : PhaseSpace 1) (_j : ZMod 1) : ℝ :=
  40  0
  41
  42/-- Smeared quartic Hamiltonian. -/
  43def quarticHam (N : ZMod 1 → ℝ) (x : PhaseSpace 1) : ℝ :=
  44  ∑ j : ZMod 1, N j * quarticHamDensity x j
  45
  46/-- Frechet derivative matching `HasFDerivAt.pow` then `const_mul`. -/
  47def quarticHamD (N : ZMod 1 → ℝ) (x : PhaseSpace 1) : PhaseSpace 1 →L[ℝ] ℝ :=
  48  ∑ i : ZMod 1, N i • ((4 • (x.2 i) ^ 3) • coordP i)
  49
  50lemma hasFDerivAt_quarticHam (N : ZMod 1 → ℝ) (x : PhaseSpace 1) :
  51    HasFDerivAt (quarticHam N) (quarticHamD N x) x := by
  52  unfold quarticHam quarticHamD quarticHamDensity
  53  exact HasFDerivAt.fun_sum fun i _ =>
  54    ((hasFDerivAt_coord_snd i x).pow 4).const_mul (N i)
  55
  56theorem differentiable_quarticHam (N : ZMod 1 → ℝ) :
  57    Differentiable ℝ (quarticHam N) :=
  58  fun x => (hasFDerivAt_quarticHam N x).differentiableAt
  59
  60lemma pderivQ_quarticHam (N : ZMod 1 → ℝ) (j : ZMod 1) (x : PhaseSpace 1) :
  61    pderivQ (quarticHam N) j x = 0 := by
  62  rw [pderivQ, (hasFDerivAt_quarticHam N x).fderiv, quarticHamD,
  63    ContinuousLinearMap.sum_apply]
  64  refine Finset.sum_eq_zero fun i _ => ?_
  65  simp [coordP]
  66
  67/-- THEOREM. Quartic–quartic bracket vanishes: both generators depend only on
  68momentum, so all configuration partials are zero. -/
  69theorem bracket_quarticHam_quarticHam (N M : ZMod 1 → ℝ) (x : PhaseSpace 1) :
  70    bracket (quarticHam N) (quarticHam M) x = 0 := by
  71  simp only [bracket, pderivQ_quarticHam]
  72  exact Finset.sum_eq_zero fun _ _ => by ring
  73
  74lemma zeroMom_eq_zero (w : ZMod 1 → ℝ) :
  75    (fun x : PhaseSpace 1 => ∑ j : ZMod 1, w j * zeroMomDensity x j)
  76      = fun _ => (0 : ℝ) := by
  77  funext y
  78  simp [zeroMomDensity]
  79
  80lemma differentiable_zeroMom (w : ZMod 1 → ℝ) :
  81    Differentiable ℝ (fun x : PhaseSpace 1 => ∑ j : ZMod 1, w j * zeroMomDensity x j) := by
  82  rw [zeroMom_eq_zero]
  83  exact differentiable_const 0
  84
  85lemma pderivQ_zeroMom (w : ZMod 1 → ℝ) (i : ZMod 1) (x : PhaseSpace 1) :
  86    pderivQ (fun y => ∑ j : ZMod 1, w j * zeroMomDensity y j) i x = 0 := by
  87  unfold pderivQ
  88  rw [zeroMom_eq_zero w]
  89  simp
  90
  91lemma pderivP_zeroMom (w : ZMod 1 → ℝ) (i : ZMod 1) (x : PhaseSpace 1) :
  92    pderivP (fun y => ∑ j : ZMod 1, w j * zeroMomDensity y j) i x = 0 := by
  93  unfold pderivP
  94  rw [zeroMom_eq_zero w]
  95  simp
  96
  97lemma bracket_zeroMom_any (w : ZMod 1 → ℝ) (G : PhaseSpace 1 → ℝ) (x : PhaseSpace 1) :
  98    bracket (fun y => ∑ j : ZMod 1, w j * zeroMomDensity y j) G x = 0 := by
  99  simp only [bracket, pderivQ_zeroMom, pderivP_zeroMom]
 100  exact Finset.sum_eq_zero fun _ _ => by ring
 101
 102lemma zmod1_one_eq_zero : (1 : ZMod 1) = 0 := by decide
 103
 104lemma zmod1_add_self (j : ZMod 1) : j + 1 = j := by
 105  simp [zmod1_one_eq_zero]
 106
 107lemma zmod1_wronskian_zero (N M : ZMod 1 → ℝ) (j : ZMod 1) :
 108    N j * M (j + 1) - M j * N (j + 1) = 0 := by
 109  rw [zmod1_add_self]
 110  ring
 111
 112lemma zmod1_lapse_diff_zero (N : ZMod 1 → ℝ) (j : ZMod 1) :
 113    N (j + 1) - N j = 0 := by
 114  rw [zmod1_add_self]
 115  ring
 116
 117/-- DISCLOSURE. On `ZMod 1` every discrete Wronskian and every discrete lapse
 118difference vanishes identically (`j + 1 = j`). The Dirac `mom_ham` / `ham_ham`
 119right-hand sides are therefore vacuous for every density pair. -/
 120theorem one_site_wronskians_vacuous (N M : ZMod 1 → ℝ) (j : ZMod 1) :
 121    N j * M (j + 1) - M j * N (j + 1) = 0 ∧ N (j + 1) - N j = 0 :=
 122  ⟨zmod1_wronskian_zero N M j, zmod1_lapse_diff_zero N j⟩
 123
 124/-! ## The counterexample inhabitant -/
 125
 126/-- THEOREM (inhabitant). The quartic one-site densities satisfy every real
 127field of `HojmanKucharTeitelboimTarget 1`. On `ZMod 1`, `j + 1 = j`, so
 128Wronskians and discrete lapse derivatives vanish; the Hamiltonian depends only
 129on momentum, so its self-bracket vanishes by vanishing configuration
 130partials; the momentum density is identically zero. -/
 131def quarticOneSiteHKT : HojmanKucharTeitelboimTarget 1 where
 132  hamDensity := quarticHamDensity
 133  momDensity := zeroMomDensity
 134  ham_differentiable := differentiable_quarticHam
 135  mom_differentiable := differentiable_zeroMom
 136  ham_local := by
 137    intro x y j _ _ hp
 138    simp [quarticHamDensity, hp]
 139  ham_covariant := by
 140    intro x a j
 141    simp [quarticHamDensity]
 142  mom_mom := by
 143    intro v w x
 144    exact bracket_zeroMom_any v (fun y => ∑ j : ZMod 1, w j * zeroMomDensity y j) x
 145  mom_ham := by
 146    intro w N x
 147    rw [bracket_zeroMom_any]
 148    refine (Finset.sum_eq_zero fun j _ => ?_).symm
 149    rw [zmod1_lapse_diff_zero]
 150    ring
 151  ham_ham := by
 152    intro N M x
 153    change bracket (quarticHam N) (quarticHam M) x
 154        = ∑ j : ZMod 1, (N j * M (j + 1) - M j * N (j + 1)) * zeroMomDensity x j
 155    rw [bracket_quarticHam_quarticHam]
 156    refine (Finset.sum_eq_zero fun j _ => ?_).symm
 157    simp [zeroMomDensity]
 158
 159/-! ## Falsification of unrestricted rigidity -/
 160
 161/-- Constant-configuration phase point with momentum `p` at the unique site. -/
 162def momPoint (p : ℝ) : PhaseSpace 1 :=
 163  (fun _ => 0, fun _ => p)
 164
 165private lemma momPoint_q (p : ℝ) (j : ZMod 1) : (momPoint p).1 j = 0 := rfl
 166private lemma momPoint_p (p : ℝ) (j : ZMod 1) : (momPoint p).2 j = p := rfl
 167
 168/-- THEOREM (headline falsification). `HKTRigidityStatement 1` is false:
 169`quarticOneSiteHKT` inhabits the target class, but `π^4` is not of the form
 170`cKin π² + cVac` on `ZMod 1` (the gradient slot vanishes by `j + 1 = j`). -/
 171theorem not_HKTRigidityStatement_one : ¬ HKTRigidityStatement 1 := by
 172  intro h
 173  obtain ⟨cKin, cGrad, cVac, hform⟩ := h quarticOneSiteHKT
 174  have form (p : ℝ) : p ^ 4 = cKin * (p * p) + cVac := by
 175    have hj := hform (momPoint p) (0 : ZMod 1)
 176    -- hj : quarticOneSiteHKT.hamDensity _ _ = cKin * .. + cGrad * .. + cVac
 177    change quarticHamDensity (momPoint p) (0 : ZMod 1)
 178        = cKin * ((momPoint p).2 0 * (momPoint p).2 0)
 179          + cGrad *
 180              (((momPoint p).1 ((0 : ZMod 1) + 1) - (momPoint p).1 0) *
 181                ((momPoint p).1 ((0 : ZMod 1) + 1) - (momPoint p).1 0))
 182          + cVac at hj
 183    simp only [quarticHamDensity, momPoint_p, momPoint_q, zmod1_add_self,
 184      sub_self, mul_zero, add_zero] at hj
 185    exact hj
 186  have hVac : cVac = 0 := by
 187    have := form 0
 188    norm_num at this
 189    exact this.symm
 190  have hKin : cKin = 1 := by
 191    have := form 1
 192    rw [hVac] at this
 193    norm_num at this
 194    linarith
 195  have boom := form 2
 196  rw [hVac, hKin] at boom
 197  norm_num at boom
 198
 199end
 200end HKTOneSiteCounterexample
 201end SevenGaps
 202end Gravity
 203end IndisputableMonolith
 204