IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureFunctionBlocker
   3
   4/-!
   5# Wave C2 R0+R1: dynamic structure-function bracket on two sites
   6
   7Closes the first two typed residuals of
   8`plans/QG_WaveC2_Gap5_Residual_DAG_Draft_20260722.txt`:
   9
  10* **R0 (decoy).** The naive lookalike that plugs `g x` into the frozen
  11  `HamW` slot and reuses the frozen partials (`pderivQ_HamW`) fails: the
  12  configuration partial picks up an uncompensated `∂g/∂q` term.
  13* **R1.** The same candidate Hamiltonian, once its Frechet derivative is
  14  computed honestly (including `∂g/∂q`), inhabits
  15  `PhaseSpaceDependentHamiltonianConstruction concreteDynamicInverseMetric`
  16  at `n = 2`. The extra derivative terms cancel in the Hamiltonian–Hamiltonian
  17  bracket, so `ham_ham` recovers the target dynamic structure function.
  18
  19Does **not** flip `gap5_constraint_recovery`. Continuum and HKT residuals
  20remain OPEN.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Gravity
  25namespace SevenGaps
  26namespace DynamicStructureBracket
  27
  28open HypersurfaceDeformation WeightedHypersurfaceBracket DynamicStructureFunctionBlocker
  29
  30noncomputable section
  31
  32open Finset
  33
  34/-! ## Candidate: naive dynamic HamW lookalike -/
  35
  36/-- MODEL. The lookalike that substitutes the phase-space-dependent inverse
  37metric into the `HamW` density pointwise:
  38`ham N x := HamW (concreteDynamicInverseMetric x) N x`. -/
  39def naiveDynamicHamW (N : ZMod 2 → ℝ) (x : PhaseSpace 2) : ℝ :=
  40  HamW (concreteDynamicInverseMetric x) N x
  41
  42/-- Unfolded form used for Frechet calculus. -/
  43def HamDyn (N : ZMod 2 → ℝ) (x : PhaseSpace 2) : ℝ :=
  44  ∑ i : ZMod 2, (N i / 2) *
  45    (x.2 i * x.2 i +
  46      (1 + x.1 i * x.1 i) *
  47        ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)))
  48
  49theorem HamDyn_eq_naive (N : ZMod 2 → ℝ) :
  50    HamDyn N = naiveDynamicHamW N := by
  51  funext x
  52  unfold HamDyn naiveDynamicHamW HamW concreteDynamicInverseMetric
  53  refine Finset.sum_congr rfl fun i _ => ?_
  54  ring
  55
  56/-! ## R0 witness data -/
  57
  58/-- Explicit witness phase point: unit configuration and unit momentum at
  59site `0`, zero at site `1`. Gradient and `∂g/∂q` are both nonzero at site
  60`0`. -/
  61def decoyPhasePoint : PhaseSpace 2 :=
  62  (fun j : ZMod 2 => if j = (0 : ZMod 2) then (1 : ℝ) else 0,
  63    fun j : ZMod 2 => if j = (0 : ZMod 2) then (1 : ℝ) else 0)
  64
  65/-- Lapse supported at site `0`. -/
  66def decoyLapse : ZMod 2 → ℝ :=
  67  fun j => if j = (0 : ZMod 2) then (1 : ℝ) else 0
  68
  69private lemma decoyLapse_zero : decoyLapse (0 : ZMod 2) = 1 := by
  70  simp [decoyLapse]
  71
  72private lemma decoyLapse_one : decoyLapse (1 : ZMod 2) = 0 := by
  73  simp [decoyLapse]
  74
  75private lemma decoy_q_zero : decoyPhasePoint.1 (0 : ZMod 2) = 1 := by
  76  simp [decoyPhasePoint]
  77
  78private lemma decoy_q_one : decoyPhasePoint.1 (1 : ZMod 2) = 0 := by
  79  simp [decoyPhasePoint]
  80
  81private lemma zmod2_zero_sub_one : (0 : ZMod 2) - 1 = 1 := by
  82  decide
  83
  84private lemma zmod2_zero_add_one : (0 : ZMod 2) + 1 = 1 := by
  85  decide
  86
  87/-! ## Frechet derivative (honest; includes ∂g/∂q) -/
  88
  89/-- Frechet derivative of `HamDyn N`. The final summand carries `0 + …`
  90so that it matches `HasFDerivAt.const.add` from the metric factor. -/
  91def HamDynD (N : ZMod 2 → ℝ) (x : PhaseSpace 2) : PhaseSpace 2 →L[ℝ] ℝ :=
  92  ∑ i : ZMod 2,
  93    (N i / 2) •
  94      ((x.2 i • coordP i + x.2 i • coordP i) +
  95        ((1 + x.1 i * x.1 i) •
  96            ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i) +
  97              (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)) +
  98          ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)) •
  99            (0 + (x.1 i • coordQ i + x.1 i • coordQ i))))
 100
 101lemma hasFDerivAt_HamDyn (N : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 102    HasFDerivAt (HamDyn N) (HamDynD N x) x := by
 103  unfold HamDyn HamDynD
 104  exact HasFDerivAt.fun_sum fun i _ =>
 105    ((((hasFDerivAt_coord_snd i x).mul (hasFDerivAt_coord_snd i x)).add
 106      (((hasFDerivAt_const (1 : ℝ) x).add
 107          ((hasFDerivAt_coord_fst i x).mul (hasFDerivAt_coord_fst i x))).mul
 108        (((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x)).mul
 109          ((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x))))).const_mul
 110      (N i / 2))
 111
 112/-- THEOREM. Momentum partial: kinetic slot unchanged by `g`. -/
 113theorem pderivP_HamDyn (N : ZMod 2 → ℝ) (j : ZMod 2) (x : PhaseSpace 2) :
 114    pderivP (HamDyn N) j x = N j * x.2 j := by
 115  rw [pderivP, (hasFDerivAt_HamDyn N x).fderiv, HamDynD, ContinuousLinearMap.sum_apply]
 116  have step : ∀ i : ZMod 2,
 117      (((N i / 2) •
 118          ((x.2 i • coordP i + x.2 i • coordP i) +
 119            ((1 + x.1 i * x.1 i) •
 120                ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i) +
 121                  (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)) +
 122              ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)) •
 123                (0 + (x.1 i • coordQ i + x.1 i • coordQ i)))) :
 124            PhaseSpace 2 →L[ℝ] ℝ))
 125        ((0, Pi.single j 1) : PhaseSpace 2)
 126      = (N i * x.2 i) * (if i = j then (1 : ℝ) else 0) := by
 127    intro i
 128    simp [Pi.single_apply]
 129    split_ifs <;> ring
 130  rw [Finset.sum_congr rfl fun i _ => step i, sum_mul_ite]
 131
 132/-- THEOREM. Honest configuration partial: frozen `HamW` contribution plus
 133the `∂g/∂q` correction `N_j q_j (Δq_j)²`. -/
 134theorem pderivQ_HamDyn (N : ZMod 2 → ℝ) (j : ZMod 2) (x : PhaseSpace 2) :
 135    pderivQ (HamDyn N) j x
 136      = N (j - 1) * ((1 + x.1 (j - 1) * x.1 (j - 1)) * (x.1 j - x.1 (j - 1)))
 137        - N j * ((1 + x.1 j * x.1 j) * (x.1 (j + 1) - x.1 j))
 138        + N j * (x.1 j * ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) := by
 139  rw [pderivQ, (hasFDerivAt_HamDyn N x).fderiv, HamDynD, ContinuousLinearMap.sum_apply]
 140  have step : ∀ i : ZMod 2,
 141      (((N i / 2) •
 142          ((x.2 i • coordP i + x.2 i • coordP i) +
 143            ((1 + x.1 i * x.1 i) •
 144                ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i) +
 145                  (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)) +
 146              ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)) •
 147                (0 + (x.1 i • coordQ i + x.1 i • coordQ i)))) :
 148            PhaseSpace 2 →L[ℝ] ℝ))
 149        ((Pi.single j 1, 0) : PhaseSpace 2)
 150      = (N i * ((1 + x.1 i * x.1 i) * (x.1 (i + 1) - x.1 i))) *
 151            (if i + 1 = j then (1 : ℝ) else 0)
 152        - (N i * ((1 + x.1 i * x.1 i) * (x.1 (i + 1) - x.1 i))) *
 153            (if i = j then (1 : ℝ) else 0)
 154        + (N i * (x.1 i * ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)))) *
 155            (if i = j then (1 : ℝ) else 0) := by
 156    intro i
 157    simp [Pi.single_apply, mul_sub]
 158    split_ifs <;> ring
 159  rw [Finset.sum_congr rfl fun i _ => step i]
 160  simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib]
 161  rw [sum_mul_ite_add
 162      (fun i => N i * ((1 + x.1 i * x.1 i) * (x.1 (i + 1) - x.1 i))) 1 j,
 163    sum_mul_ite
 164      (fun i => N i * ((1 + x.1 i * x.1 i) * (x.1 (i + 1) - x.1 i))) j,
 165    sum_mul_ite
 166      (fun i => N i * (x.1 i * ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)))) j]
 167  have e : j - 1 + 1 = j := by ring
 168  simp only [e]
 169
 170/-- THEOREM (R0 decoy). The naive lookalike fails the frozen-partial
 171construction reading: at `decoyPhasePoint`, with lapse `decoyLapse` and site
 172`0`, the honest `pderivQ` differs from the frozen `pderivQ_HamW` evaluation
 173at `w := g x` by the uncompensated `∂g/∂q` term. -/
 174theorem TypedResidual_naive_dynamic_HamW_decoy_fails :
 175    pderivQ (HamDyn decoyLapse) (0 : ZMod 2) decoyPhasePoint
 176      ≠ pderivQ (HamW (concreteDynamicInverseMetric decoyPhasePoint) decoyLapse)
 177          (0 : ZMod 2) decoyPhasePoint := by
 178  have hHonest :
 179      pderivQ (HamDyn decoyLapse) (0 : ZMod 2) decoyPhasePoint = (3 : ℝ) := by
 180    rw [pderivQ_HamDyn, zmod2_zero_sub_one, zmod2_zero_add_one,
 181      decoyLapse_zero, decoyLapse_one, decoy_q_zero, decoy_q_one]
 182    norm_num
 183  have hFrozen :
 184      pderivQ (HamW (concreteDynamicInverseMetric decoyPhasePoint) decoyLapse)
 185          (0 : ZMod 2) decoyPhasePoint = (2 : ℝ) := by
 186    rw [pderivQ_HamW]
 187    rw [zmod2_zero_sub_one, zmod2_zero_add_one, decoyLapse_zero, decoyLapse_one,
 188      decoy_q_zero, decoy_q_one]
 189    simp only [concreteDynamicInverseMetric, decoy_q_zero, pow_two]
 190    norm_num
 191  rw [hHonest, hFrozen]
 192  norm_num
 193
 194theorem differentiable_HamDyn (N : ZMod 2 → ℝ) :
 195    Differentiable ℝ (HamDyn N) :=
 196  fun x => (hasFDerivAt_HamDyn N x).differentiableAt
 197
 198/-- THEOREM (R1 headline). Exact dynamic structure-function identity for the
 199two-site concrete inverse metric. -/
 200theorem bracket_HamDyn_HamDyn (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
 201    bracket (HamDyn N) (HamDyn M) x
 202      = ∑ j : ZMod 2, (N j * M (j + 1) - M j * N (j + 1)) *
 203          (concreteDynamicInverseMetric x j *
 204            (x.2 (j + 1) * (x.1 (j + 1) - x.1 j))) := by
 205  simp only [bracket, pderivQ_HamDyn, pderivP_HamDyn, concreteDynamicInverseMetric]
 206  have step1 :
 207      (∑ j : ZMod 2,
 208          ((N (j - 1) * ((1 + x.1 (j - 1) * x.1 (j - 1)) * (x.1 j - x.1 (j - 1)))
 209              - N j * ((1 + x.1 j * x.1 j) * (x.1 (j + 1) - x.1 j))
 210              + N j * (x.1 j * ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j)))) *
 211            (M j * x.2 j)
 212            - (N j * x.2 j) *
 213              (M (j - 1) * ((1 + x.1 (j - 1) * x.1 (j - 1)) * (x.1 j - x.1 (j - 1)))
 214                - M j * ((1 + x.1 j * x.1 j) * (x.1 (j + 1) - x.1 j))
 215                + M j * (x.1 j * ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))))))
 216        = ∑ j : ZMod 2,
 217            (N (j - 1) * M j - M (j - 1) * N j) *
 218              ((1 + x.1 (j - 1) * x.1 (j - 1)) *
 219                (x.2 j * (x.1 j - x.1 (j - 1)))) :=
 220    Finset.sum_congr rfl fun j _ => by ring
 221  rw [step1]
 222  refine sum_reindex 1
 223    (fun k =>
 224      (N (k - 1) * M k - M (k - 1) * N k) *
 225        ((1 + x.1 (k - 1) * x.1 (k - 1)) *
 226          (x.2 k * (x.1 k - x.1 (k - 1))))) _
 227    fun j => ?_
 228  have e1 : j + 1 - 1 = j := by ring
 229  simp only [e1]
 230  ring
 231
 232/-- THEOREM (R1). Inhabitant of the phase-space-dependent Hamiltonian
 233construction for `concreteDynamicInverseMetric` at `n = 2`. -/
 234def concreteDynamicHamiltonianConstruction :
 235    PhaseSpaceDependentHamiltonianConstruction concreteDynamicInverseMetric where
 236  ham := HamDyn
 237  ham_differentiable := differentiable_HamDyn
 238  ham_ham := bracket_HamDyn_HamDyn
 239
 240/-- Equivalent residual Prop named in the Wave C2 DAG. -/
 241def TypedResidual_dynamic_bracket_concrete_two_site : Prop :=
 242  Nonempty (PhaseSpaceDependentHamiltonianConstruction concreteDynamicInverseMetric)
 243
 244theorem typedResidual_dynamic_bracket_concrete_two_site :
 245    TypedResidual_dynamic_bracket_concrete_two_site :=
 246  ⟨concreteDynamicHamiltonianConstruction⟩
 247
 248/-- Immediate hard-core corollary (DAG R2, folded into R1 for `n = 2`). -/
 249theorem phaseSpaceDependentDiracPremise_two_site :
 250    PhaseSpaceDependentDiracPremise 2 :=
 251  ⟨concreteDynamicInverseMetric,
 252    concreteDynamicInverseMetric_not_constant,
 253    ⟨concreteDynamicHamiltonianConstruction⟩⟩
 254
 255/-! ### Axiom receipts -/
 256
 257#print axioms TypedResidual_naive_dynamic_HamW_decoy_fails
 258#print axioms bracket_HamDyn_HamDyn
 259#print axioms typedResidual_dynamic_bracket_concrete_two_site
 260#print axioms phaseSpaceDependentDiracPremise_two_site
 261
 262end
 263end DynamicStructureBracket
 264end SevenGaps
 265end Gravity
 266end IndisputableMonolith
 267