IndisputableMonolith.Gravity.SevenGaps.WeightedHypersurfaceBracket

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.HypersurfaceDeformation
   3import IndisputableMonolith.Gravity.Analysis.QuadratureLimit
   4
   5/-!
   6# Background-weighted hypersurface bracket on the periodic lattice
   7
   8QG Seven-Gaps campaign, Pillar 1 (constraint algebra), panel-locked live bet
   9C10: weighted structure function w on the lattice. This module generalizes the
  10frozen-1 hypersurface-deformation theorem `bracket_Ham_Ham` of
  11`HypersurfaceDeformation.lean` to a Hamiltonian generator carrying a fixed
  12background weight `w : ZMod n -> Real` in the stiffness (gradient-squared)
  13slot of the density, and proves the exact lattice bracket: the weight emerges
  14in the closure relation exactly where the Dirac structure function sits.
  15
  16## Panel-lock honesty statement (binding)
  17
  18This is a BACKGROUND-w structure function, not a phase-space-dependent inverse
  19metric; it moves toward but does NOT flip gap5_constraint_recovery; HKT
  20rigidity is untouched and OPEN. The weight `w` is a fixed function of the
  21lattice site, never of the phase-space point `(q, pi)`; the phase-space
  22dependent structure function `g^{ab}[q]` demanded by the full Dirac algebra
  23(and by any honest GR-recovery claim) remains OPEN and is not approximated,
  24inhabited, or claimed here. No `HojmanKucharTeitelboimTarget` instance is
  25provided; `HKTRigidityStatement` is not touched.
  26
  27## What is proved (exact statements, no limits taken)
  28
  29* `HamW w N` is the smeared Hamiltonian with density
  30  `(N_i / 2) * (pi_i^2 + w_i * (q_{i+1} - q_i)^2)`: the weight sits in the
  31  stiffness slot only, the kinetic slot is unweighted. Continuum reading: `w`
  32  is the sampled inverse spatial metric `h^{xx}(x)` (equivalently the local
  33  sound speed squared) of a STATIC background line element; that reading is
  34  interpretive commentary, not a theorem of this file.
  35* `HamW_one`: at `w = 1` the weighted generator IS the frozen-1 generator,
  36  as an equality of functions on phase space.
  37* `bracket_HamW_HamW` (headline): the exact lattice identity
  38  `{H_w[N], H_w[M]} = sum_j (N_j M_{j+1} - M_j N_{j+1}) * w_j *
  39  (pi_{j+1} (q_{j+1} - q_j))`. Two w-weighted Hamiltonian deformations close
  40  on a D-type (shift) generator whose smearing is the discrete lapse
  41  Wronskian multiplied by the background weight: the structure function of
  42  this bracket is `w`, appearing linearly (w-weighted, not w^2-weighted; the
  43  kinetic slot carries no weight, so exactly one factor of `w` survives the
  44  Kronecker collapse).
  45* `bracket_HamW_HamW_one`: substituting `w = 1` literally reproduces the
  46  proved frozen-1 statement `bracket_Ham_Ham`, via `HamW_one`.
  47* `weightedStructureSum_tendsto` (bonus): the h-scaled w-weighted structure
  48  smearing sums converge to the continuum integral, by direct consumption of
  49  `Analysis.weightedLatticeSum_tendsto` from the quadrature toolkit.
  50
  51## Conventions (preregistered by the formulation panel)
  52
  53* Point-split density: the closure density on the right of
  54  `bracket_HamW_HamW` is point-split, momentum at site `j + 1` and field
  55  gradient on the cell `(j, j + 1)`; the weight `w_j` sits at the LEFT point
  56  of the split pair. At `w = 1` the placement is invisible; here it is part
  57  of the exact statement and is disclosed rather than symmetrized.
  58* h-scaling: sites sample the unit interval at spacing `h = 1/N` with `q`,
  59  `pi`, `N`, `M`, `w` all sampled O(1). For C^1 lapse profiles the discrete
  60  lapse Wronskian `N_j M_{j+1} - M_j N_{j+1}` tends to
  61  `h * (N M' - M N')(x_j)`, and for a C^1 field profile the gradient factor
  62  `q_{j+1} - q_j` contributes the second `h`; the normalized closure-density
  63  profile is therefore `pi_{j+1} (q_{j+1} - q_j) / h`, and the bracket sum is
  64  a Riemann sum with one explicit h-factor from the Wronskian, finite and
  65  nonzero in the limit with NO further rescaling of `Dgen` or `Ham`. In
  66  `weightedStructureSum_tendsto` the continuum Wronskian profile is sampled
  67  directly, the `1/N` prefactor is exactly that Wronskian h-factor, and the
  68  density profile `S` is the normalized (per-h) shape, matching its own
  69  docstring.
  70* Positivity of `w` is the physical regime (nondegenerate background metric)
  71  but is NOT needed for any algebraic identity below, so no positivity
  72  hypothesis is imposed anywhere (no unused hypotheses).
  73
  74## Status ledger
  75
  76* MODEL: `HamW`, `HamWD` (definitional lattice discretizations, mirroring
  77  `Ham`, `HamD`).
  78* THEOREM (axiom-clean, no sorry, unconditional): `HamW_one`,
  79  `differentiable_HamW`, `pderivP_HamW`, `pderivQ_HamW`,
  80  `bracket_HamW_HamW`, `bracket_HamW_HamW_one`,
  81  `weightedStructureSum_tendsto` (the last with explicit `ContinuousOn`
  82  hypotheses, exactly as in the toolkit).
  83* OPEN (untouched here): phase-space-dependent structure function
  84  `g^{ab}[q]`; the full Dirac algebra continuum limit; HKT target
  85  inhabitation and `HKTRigidityStatement`; Jacobi for the fderiv bracket.
  86-/
  87
  88namespace IndisputableMonolith
  89namespace Gravity
  90namespace SevenGaps
  91namespace WeightedHypersurfaceBracket
  92
  93open HypersurfaceDeformation
  94
  95noncomputable section
  96
  97open Finset
  98
  99variable {n : ℕ} [NeZero n]
 100
 101/-- MODEL. The background-weighted smeared Hamiltonian
 102`H_w[N] = sum_i (N_i / 2) * (pi_i^2 + w_i * (q_{i+1} - q_i)^2)`.
 103The fixed background weight `w` sits in the stiffness (gradient) slot; the
 104kinetic slot is unweighted. `w` depends on the lattice site only, never on
 105the phase-space point: this is a BACKGROUND-w object. -/
 106def HamW (w N : ZMod n → ℝ) (x : PhaseSpace n) : ℝ :=
 107  ∑ i : ZMod n, (N i / 2) *
 108    (x.2 i * x.2 i + w i * ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)))
 109
 110/-- THEOREM (sanity anchor). At unit weight the weighted generator is the
 111frozen-1 generator of `HypersurfaceDeformation.lean`, as an equality of
 112functions on phase space. -/
 113theorem HamW_one (N : ZMod n → ℝ) : HamW (fun _ => 1) N = Ham N := by
 114  funext x
 115  unfold HamW Ham
 116  refine Finset.sum_congr rfl fun i _ => ?_
 117  show (N i / 2) *
 118      (x.2 i * x.2 i + 1 * ((x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i)))
 119      = (N i / 2) * (x.2 i * x.2 i + (x.1 (i + 1) - x.1 i) * (x.1 (i + 1) - x.1 i))
 120  ring
 121
 122/-! ### Frechet derivative of the weighted generator
 123
 124The fderiv chain of `HypersurfaceDeformation.lean` is fully generic in a
 125site-dependent scalar coefficient: the weight enters through one extra
 126`HasFDerivAt.const_mul`, and every Kronecker-collapse step goes through
 127unchanged. This answers the panel's w-genericity question affirmatively. -/
 128
 129/-- The derivative of `HamW w N` at `x`, as an explicit continuous linear map. -/
 130def HamWD (w N : ZMod n → ℝ) (x : PhaseSpace n) : PhaseSpace n →L[ℝ] ℝ :=
 131  ∑ i : ZMod n,
 132    (N i / 2) • ((x.2 i • coordP i + x.2 i • coordP i)
 133      + w i • ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)
 134          + (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)))
 135
 136lemma hasFDerivAt_HamW (w N : ZMod n → ℝ) (x : PhaseSpace n) :
 137    HasFDerivAt (HamW w N) (HamWD w N x) x := by
 138  unfold HamW HamWD
 139  exact HasFDerivAt.fun_sum fun i _ =>
 140    ((((hasFDerivAt_coord_snd i x).mul (hasFDerivAt_coord_snd i x)).add
 141      ((((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x)).mul
 142        ((hasFDerivAt_coord_fst (i + 1) x).sub (hasFDerivAt_coord_fst i x))).const_mul
 143          (w i))).const_mul (N i / 2))
 144
 145/-- THEOREM. `HamW w N` is (unconditionally) differentiable. -/
 146theorem differentiable_HamW (w N : ZMod n → ℝ) :
 147    Differentiable ℝ (HamW (n := n) w N) :=
 148  fun x => (hasFDerivAt_HamW w N x).differentiableAt
 149
 150/-! ### Partial derivatives (Kronecker collapse) -/
 151
 152/-- THEOREM. The momentum partial of the weighted generator: the kinetic slot
 153is unweighted, so the weight does not appear. -/
 154theorem pderivP_HamW (w N : ZMod n → ℝ) (j : ZMod n) (x : PhaseSpace n) :
 155    pderivP (HamW w N) j x = N j * x.2 j := by
 156  rw [pderivP, (hasFDerivAt_HamW w N x).fderiv, HamWD, ContinuousLinearMap.sum_apply]
 157  have step : ∀ i : ZMod n,
 158      (((N i / 2) • ((x.2 i • coordP i + x.2 i • coordP i)
 159        + w i • ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)
 160            + (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i))) :
 161          PhaseSpace n →L[ℝ] ℝ))
 162        ((0, Pi.single j 1) : PhaseSpace n)
 163      = (N i * x.2 i) * (if i = j then (1 : ℝ) else 0) := by
 164    intro i
 165    simp [Pi.single_apply]
 166    split_ifs <;> ring
 167  rw [Finset.sum_congr rfl fun i _ => step i, sum_mul_ite]
 168
 169/-- THEOREM. The configuration partial of the weighted generator: each
 170gradient term carries its own site weight. -/
 171theorem pderivQ_HamW (w N : ZMod n → ℝ) (j : ZMod n) (x : PhaseSpace n) :
 172    pderivQ (HamW w N) j x
 173      = N (j - 1) * (w (j - 1) * (x.1 j - x.1 (j - 1)))
 174        - N j * (w j * (x.1 (j + 1) - x.1 j)) := by
 175  rw [pderivQ, (hasFDerivAt_HamW w N x).fderiv, HamWD, ContinuousLinearMap.sum_apply]
 176  have step : ∀ i : ZMod n,
 177      (((N i / 2) • ((x.2 i • coordP i + x.2 i • coordP i)
 178        + w i • ((x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i)
 179            + (x.1 (i + 1) - x.1 i) • (coordQ (i + 1) - coordQ i))) :
 180          PhaseSpace n →L[ℝ] ℝ))
 181        ((Pi.single j 1, 0) : PhaseSpace n)
 182      = (N i * (w i * (x.1 (i + 1) - x.1 i))) * (if i + 1 = j then (1 : ℝ) else 0)
 183        - (N i * (w i * (x.1 (i + 1) - x.1 i))) * (if i = j then (1 : ℝ) else 0) := by
 184    intro i
 185    simp [Pi.single_apply, mul_sub]
 186    split_ifs <;> ring
 187  rw [Finset.sum_congr rfl fun i _ => step i, Finset.sum_sub_distrib,
 188    sum_mul_ite_add, sum_mul_ite]
 189  have e : j - 1 + 1 = j := by ring
 190  rw [e]
 191
 192/-! ### The headline: exact weighted hypersurface-deformation relation -/
 193
 194/-- THEOREM (headline; exact discrete weighted hypersurface deformation).
 195`{H_w[N], H_w[M]} = sum_j (N_j M_{j+1} - M_j N_{j+1}) * w_j *
 196(pi_{j+1} (q_{j+1} - q_j))`.
 197
 198The bracket of two w-weighted Hamiltonian deformations is a D-type (shift)
 199generator: the point-split momentum density `pi_{j+1} (q_{j+1} - q_j)` smeared
 200by the discrete lapse Wronskian TIMES the background weight `w_j` at the left
 201split point. The weight appears exactly where the Dirac structure function
 202sits (in the continuum, `{H(N), H(M)} = D(g^{xx} (N M' - M N'))`), and it
 203appears LINEARLY: with the weight in the stiffness slot and the kinetic slot
 204unweighted, exactly one factor of `w` survives the Kronecker collapse, so the
 205answer is w-weighted, not w^2-weighted. Antisymmetric in `N, M` by
 206inspection; vanishes identically for `N = M`.
 207
 208Honesty (panel lock): this is a BACKGROUND-w structure function, not a
 209phase-space-dependent inverse metric; it moves toward but does NOT flip
 210gap5_constraint_recovery; HKT rigidity is untouched and OPEN. -/
 211theorem bracket_HamW_HamW (w N M : ZMod n → ℝ) (x : PhaseSpace n) :
 212    bracket (HamW w N) (HamW w M) x
 213      = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1))
 214          * (w j * (x.2 (j + 1) * (x.1 (j + 1) - x.1 j))) := by
 215  simp only [bracket, pderivQ_HamW, pderivP_HamW]
 216  have step1 : (∑ j : ZMod n,
 217      ((N (j - 1) * (w (j - 1) * (x.1 j - x.1 (j - 1)))
 218          - N j * (w j * (x.1 (j + 1) - x.1 j))) * (M j * x.2 j)
 219        - N j * x.2 j
 220          * (M (j - 1) * (w (j - 1) * (x.1 j - x.1 (j - 1)))
 221              - M j * (w j * (x.1 (j + 1) - x.1 j)))))
 222      = ∑ j : ZMod n,
 223          (N (j - 1) * M j - M (j - 1) * N j)
 224            * (w (j - 1) * (x.2 j * (x.1 j - x.1 (j - 1)))) :=
 225    Finset.sum_congr rfl fun j _ => by ring
 226  rw [step1]
 227  refine sum_reindex 1
 228    (fun k => (N (k - 1) * M k - M (k - 1) * N k)
 229      * (w (k - 1) * (x.2 k * (x.1 k - x.1 (k - 1))))) _ fun j => ?_
 230  have e1 : j + 1 - 1 = j := by ring
 231  simp only [e1]
 232
 233/-- THEOREM (frozen-1 recovery). Substituting the unit weight into the
 234weighted bracket literally reproduces the proved frozen-1 statement
 235`bracket_Ham_Ham`: the weighted theorem is an honest generalization, not a
 236parallel construction. Proof: rewrite by `HamW_one` and apply the existing
 237theorem. -/
 238theorem bracket_HamW_HamW_one (N M : ZMod n → ℝ) (x : PhaseSpace n) :
 239    bracket (HamW (fun _ => 1) N) (HamW (fun _ => 1) M) x
 240      = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1))
 241          * (x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) := by
 242  rw [HamW_one, HamW_one, bracket_Ham_Ham]
 243
 244end
 245
 246/-! ### Bonus: continuum limit of the weighted structure smearing
 247
 248Genuine consumption of the quadrature toolkit
 249(`IndisputableMonolith/Gravity/Analysis/QuadratureLimit.lean`), which was
 250built for exactly this consumer. -/
 251
 252open Filter in
 253/-- THEOREM (weighted structure smearing, continuum limit). Sample a
 254background weight profile `W`, a continuum lapse-Wronskian profile `Wr`
 255(the limit shape of `(N_j M_{j+1} - M_j N_{j+1}) / h`), and a closure-density
 256profile `S` (the limit shape of the point-split density
 257`pi_{j+1} (q_{j+1} - q_j) / h`, one factor of `h` absorbed by the gradient),
 258all continuous on `[0, 1]`. Then the h-scaled w-weighted structure sums of
 259`bracket_HamW_HamW` converge:
 260`(1/N) * sum_{k<N} W(k/N) * (Wr(k/N) * S(k/N)) -> integral_0^1 W * (Wr * S)`.
 261
 262h-scaling convention (stated per panel preregistration): the explicit `1/N`
 263prefactor is the single factor of lattice spacing carried by the discrete
 264lapse Wronskian; the sampled profiles are all O(1). This is a limit of the
 265SMEARING SHAPE with continuum profiles sampled directly; it is not a proof
 266that the discrete Wronskian of sampled lapses converges at rate h (that needs
 267C^1 data and is left OPEN with the full Dirac continuum limit). Direct
 268application of `Analysis.weightedLatticeSum_tendsto`. -/
 269theorem weightedStructureSum_tendsto (W Wr S : ℝ → ℝ)
 270    (hW : ContinuousOn W (Set.Icc 0 1)) (hWr : ContinuousOn Wr (Set.Icc 0 1))
 271    (hS : ContinuousOn S (Set.Icc 0 1)) :
 272    Filter.Tendsto
 273      (fun N : ℕ => (1 / (N : ℝ)) * ∑ k ∈ Finset.range N,
 274        W ((k : ℝ) / (N : ℝ)) * (Wr ((k : ℝ) / (N : ℝ)) * S ((k : ℝ) / (N : ℝ))))
 275      Filter.atTop (nhds (∫ x in (0:ℝ)..1, W x * (Wr x * S x))) := by
 276  have h := Analysis.weightedLatticeSum_tendsto (fun x => Wr x * S x) W
 277    (hWr.mul hS) hW
 278  have hint : (∫ x in (0:ℝ)..1, (Wr x * S x) * W x)
 279      = ∫ x in (0:ℝ)..1, W x * (Wr x * S x) :=
 280    intervalIntegral.integral_congr fun x _ => mul_comm _ _
 281  rw [hint] at h
 282  refine h.congr fun N => ?_
 283  congr 1
 284  refine Finset.sum_congr rfl fun k _ => ?_
 285  show Wr ((k : ℝ) / (N : ℝ)) * S ((k : ℝ) / (N : ℝ)) * W ((k : ℝ) / (N : ℝ))
 286      = W ((k : ℝ) / (N : ℝ)) * (Wr ((k : ℝ) / (N : ℝ)) * S ((k : ℝ) / (N : ℝ)))
 287  ring
 288
 289/-! ### Axiom receipts (expected: [propext, Classical.choice, Quot.sound]) -/
 290
 291#print axioms HamW_one
 292#print axioms differentiable_HamW
 293#print axioms pderivP_HamW
 294#print axioms pderivQ_HamW
 295#print axioms bracket_HamW_HamW
 296#print axioms bracket_HamW_HamW_one
 297#print axioms weightedStructureSum_tendsto
 298
 299end WeightedHypersurfaceBracket
 300end SevenGaps
 301end Gravity
 302end IndisputableMonolith
 303