IndisputableMonolith.Gravity.SevenGaps.DynamicStructureFunctionBlocker

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.WeightedHypersurfaceBracket
   3
   4/-!
   5# Dynamic structure-function blocker for the background-weighted bracket
   6
   7The exact theorem `bracket_HamW_HamW` puts a site-dependent weight in the
   8Dirac structure-function slot, and `weightedStructureSum_tendsto` carries its
   9smearing shape to the continuum.  Both results keep the weight fixed as the
  10phase-space point varies.  Full ADM gravity instead requires the inverse
  11spatial metric in that slot to vary with the canonical metric data.
  12
  13This file certifies that distinction.  A fixed background weight represents a
  14phase-space-dependent inverse metric at every phase point only if that metric
  15is phase-space constant.  The positive two-site example
  16`concreteDynamicInverseMetric` is not constant, so no background weight can
  17represent it.  Thus the existing background-weighted bracket, despite its
  18exact lattice identity and continuum smearing reach, cannot by itself be the
  19full dynamic Dirac structure function.
  20
  21No closure flag is changed.  `PhaseSpaceDependentHamiltonianConstruction`
  22names the missing Hamiltonian construction, and
  23`Gap5DynamicDiracAndHKTRigidityTarget` records that this construction and the
  24existing HKT rigidity statement are separate remaining obligations.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Gravity
  29namespace SevenGaps
  30namespace DynamicStructureFunctionBlocker
  31
  32open HypersurfaceDeformation WeightedHypersurfaceBracket
  33
  34noncomputable section
  35
  36open Finset
  37
  38variable {n : ℕ} [NeZero n]
  39
  40/-! ## Exact fixed-background underdetermination -/
  41
  42/-- A lattice inverse metric is phase-space constant when changing the
  43canonical data cannot change its value at any site. -/
  44def PhaseSpaceConstant (g : PhaseSpace n → ZMod n → ℝ) : Prop :=
  45  ∀ x y : PhaseSpace n, ∀ j : ZMod n, g x j = g y j
  46
  47/-- A fixed site weight represents a candidate inverse metric at every
  48phase-space point when their values agree at every point and site. -/
  49def FixedBackgroundRepresents (w : ZMod n → ℝ)
  50    (g : PhaseSpace n → ZMod n → ℝ) : Prop :=
  51  ∀ x : PhaseSpace n, ∀ j : ZMod n, w j = g x j
  52
  53/-- THEOREM. If one fixed background weight represents `g` at every
  54phase-space point, then `g` is phase-space constant. -/
  55theorem fixed_background_represents_only_constant
  56    (w : ZMod n → ℝ) (g : PhaseSpace n → ZMod n → ℝ)
  57    (h : FixedBackgroundRepresents w g) :
  58    PhaseSpaceConstant g := by
  59  intro x y j
  60  rw [← h x j, ← h y j]
  61
  62/-- THEOREM (exact characterization). A candidate inverse metric admits one
  63fixed background representation at all phase points exactly when it is
  64phase-space constant. -/
  65theorem exists_fixed_background_iff_phaseSpaceConstant
  66    (g : PhaseSpace n → ZMod n → ℝ) :
  67    (∃ w : ZMod n → ℝ, FixedBackgroundRepresents w g) ↔
  68      PhaseSpaceConstant g := by
  69  constructor
  70  · rintro ⟨w, hw⟩
  71    exact fixed_background_represents_only_constant w g hw
  72  · intro hg
  73    let x₀ : PhaseSpace n := (fun _ => 0, fun _ => 0)
  74    refine ⟨g x₀, ?_⟩
  75    intro x j
  76    exact hg x₀ x j
  77
  78/-! ## A concrete positive dynamic inverse metric on two sites -/
  79
  80/-- MODEL. A positive inverse-metric candidate on the two-site phase space.
  81It depends on the configuration coordinate at each site. -/
  82def concreteDynamicInverseMetric (x : PhaseSpace 2) (j : ZMod 2) : ℝ :=
  83  1 + (x.1 j) ^ 2
  84
  85/-- The zero canonical point used to witness metric variation. -/
  86def zeroPhasePoint : PhaseSpace 2 :=
  87  (fun _ => 0, fun _ => 0)
  88
  89/-- A canonical point with unit configuration and zero momentum. -/
  90def unitConfigurationPoint : PhaseSpace 2 :=
  91  (fun _ => 1, fun _ => 0)
  92
  93/-- THEOREM. The concrete inverse-metric candidate is everywhere positive. -/
  94theorem concreteDynamicInverseMetric_pos
  95    (x : PhaseSpace 2) (j : ZMod 2) :
  96    0 < concreteDynamicInverseMetric x j := by
  97  unfold concreteDynamicInverseMetric
  98  positivity
  99
 100/-- THEOREM. The concrete metric takes different values at two explicit
 101phase-space points on the two-site lattice. -/
 102theorem concreteDynamicInverseMetric_witness :
 103    concreteDynamicInverseMetric zeroPhasePoint (0 : ZMod 2) = 1 ∧
 104      concreteDynamicInverseMetric unitConfigurationPoint (0 : ZMod 2) = 2 := by
 105  norm_num [concreteDynamicInverseMetric, zeroPhasePoint, unitConfigurationPoint]
 106
 107/-- THEOREM. The positive two-site metric candidate is genuinely
 108phase-space-dependent. -/
 109theorem concreteDynamicInverseMetric_not_constant :
 110    ¬ PhaseSpaceConstant concreteDynamicInverseMetric := by
 111  intro h
 112  have hEq := h zeroPhasePoint unitConfigurationPoint (0 : ZMod 2)
 113  have hw := concreteDynamicInverseMetric_witness
 114  rw [hw.1, hw.2] at hEq
 115  norm_num at hEq
 116
 117/-- THEOREM (concrete no-go). No fixed two-site background weight represents
 118the concrete dynamic inverse metric at every phase-space point. -/
 119theorem no_fixed_background_represents_concrete
 120    (w : ZMod 2 → ℝ) :
 121    ¬ FixedBackgroundRepresents w concreteDynamicInverseMetric := by
 122  intro h
 123  exact concreteDynamicInverseMetric_not_constant
 124    (fixed_background_represents_only_constant w concreteDynamicInverseMetric h)
 125
 126/-! ## What the current weighted bracket reaches -/
 127
 128/-- The exact proposition proved by `bracket_HamW_HamW`: `HamW w` has fixed
 129background structure function `w` in its Hamiltonian-Hamiltonian bracket. -/
 130def HamWHasBackgroundStructureFunction (w : ZMod n → ℝ) : Prop :=
 131  ∀ (N M : ZMod n → ℝ) (x : PhaseSpace n),
 132    bracket (HamW w N) (HamW w M) x
 133      = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1))
 134          * (w j * (x.2 (j + 1) * (x.1 (j + 1) - x.1 j)))
 135
 136/-- THEOREM. The existing exact bracket theorem supplies the fixed-background
 137structure-function proposition. -/
 138theorem HamW_has_background_structure_function (w : ZMod n → ℝ) :
 139    HamWHasBackgroundStructureFunction w :=
 140  bracket_HamW_HamW w
 141
 142/-- The continuum smearing reach of a fixed background profile `W`. -/
 143def BackgroundWeightedContinuumReach (W : ℝ → ℝ) : Prop :=
 144  ∀ (Wr S : ℝ → ℝ),
 145    ContinuousOn Wr (Set.Icc 0 1) →
 146    ContinuousOn S (Set.Icc 0 1) →
 147    Filter.Tendsto
 148      (fun N : ℕ => (1 / (N : ℝ)) * ∑ k ∈ Finset.range N,
 149        W ((k : ℝ) / (N : ℝ)) *
 150          (Wr ((k : ℝ) / (N : ℝ)) * S ((k : ℝ) / (N : ℝ))))
 151      Filter.atTop (nhds (∫ x in (0 : ℝ)..1, W x * (Wr x * S x)))
 152
 153/-- THEOREM. The existing quadrature theorem gives the full continuum
 154smearing reach for every continuous fixed background profile. -/
 155theorem background_weighted_continuum_reach
 156    (W : ℝ → ℝ) (hW : ContinuousOn W (Set.Icc 0 1)) :
 157    BackgroundWeightedContinuumReach W := by
 158  intro Wr S hWr hS
 159  exact weightedStructureSum_tendsto W Wr S hW hWr hS
 160
 161/-! ## The missing dynamic Hamiltonian and HKT obligations -/
 162
 163/-- OPEN TARGET. A Hamiltonian family whose exact Hamiltonian-Hamiltonian
 164bracket carries a genuinely phase-space-dependent inverse metric `g`.
 165
 166The right side uses the same point-split momentum density as the current
 167background theorem, isolating the missing ingredient: constructing a
 168differentiable Hamiltonian whose bracket produces `g x j`, including all
 169derivative terms caused by the dependence of `g` on the canonical data. -/
 170structure PhaseSpaceDependentHamiltonianConstruction
 171    (g : PhaseSpace n → ZMod n → ℝ) where
 172  ham : (ZMod n → ℝ) → PhaseSpace n → ℝ
 173  ham_differentiable :
 174    ∀ N : ZMod n → ℝ, Differentiable ℝ (ham N)
 175  ham_ham :
 176    ∀ (N M : ZMod n → ℝ) (x : PhaseSpace n),
 177      bracket (ham N) (ham M) x
 178        = ∑ j : ZMod n, (N j * M (j + 1) - M j * N (j + 1))
 179            * (g x j * (x.2 (j + 1) * (x.1 (j + 1) - x.1 j)))
 180
 181/-- THEOREM. Every fixed `HamW` construction inhabits the dynamic target only
 182with the phase-space-constant metric `g x = w`.  This packages the exact
 183bracket theorem without promoting the background weight to a dynamic metric. -/
 184def backgroundHamiltonianConstruction (w : ZMod n → ℝ) :
 185    PhaseSpaceDependentHamiltonianConstruction
 186      (fun _ : PhaseSpace n => w) where
 187  ham := HamW w
 188  ham_differentiable := differentiable_HamW w
 189  ham_ham := by
 190    intro N M x
 191    exact bracket_HamW_HamW w N M x
 192
 193/-- OPEN. The missing dynamic Dirac premise: a nonconstant inverse metric
 194together with a Hamiltonian construction whose exact bracket produces it. -/
 195def PhaseSpaceDependentDiracPremise (n : ℕ) [NeZero n] : Prop :=
 196  ∃ g : PhaseSpace n → ZMod n → ℝ,
 197    ¬ PhaseSpaceConstant g ∧
 198      Nonempty (PhaseSpaceDependentHamiltonianConstruction g)
 199
 200/-- OPEN. Gap 5 requires both the phase-space-dependent Dirac construction
 201and an HKT rigidity theorem.  The current `HamW` theorem and its continuum
 202smearing result supply neither conjunct. -/
 203def Gap5DynamicDiracAndHKTRigidityTarget (n : ℕ) [NeZero n] : Prop :=
 204  PhaseSpaceDependentDiracPremise n ∧ HKTRigidityStatement n
 205
 206/-- THEOREM (certified blocker). The present background-weighted family has
 207its exact bracket and continuum reach, but no choice of its fixed two-site
 208weight can represent the explicit positive dynamic metric at all phase
 209points. -/
 210theorem gap5_background_weight_blocker :
 211    (∀ w : ZMod 2 → ℝ, HamWHasBackgroundStructureFunction w) ∧
 212      (∀ W : ℝ → ℝ, ContinuousOn W (Set.Icc 0 1) →
 213        BackgroundWeightedContinuumReach W) ∧
 214      (∀ w : ZMod 2 → ℝ,
 215        ¬ FixedBackgroundRepresents w concreteDynamicInverseMetric) := by
 216  exact ⟨HamW_has_background_structure_function,
 217    background_weighted_continuum_reach,
 218    no_fixed_background_represents_concrete⟩
 219
 220/-! ### Axiom receipts (expected: standard Mathlib basis only) -/
 221
 222#print axioms fixed_background_represents_only_constant
 223#print axioms exists_fixed_background_iff_phaseSpaceConstant
 224#print axioms concreteDynamicInverseMetric_pos
 225#print axioms concreteDynamicInverseMetric_witness
 226#print axioms concreteDynamicInverseMetric_not_constant
 227#print axioms no_fixed_background_represents_concrete
 228#print axioms HamW_has_background_structure_function
 229#print axioms background_weighted_continuum_reach
 230#print axioms gap5_background_weight_blocker
 231
 232end
 233end DynamicStructureFunctionBlocker
 234end SevenGaps
 235end Gravity
 236end IndisputableMonolith
 237