IndisputableMonolith.Gravity.SevenGaps.DynamicStructureContinuumSmearing

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket
   3import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureFunctionBlocker
   4import IndisputableMonolith.Gravity.SevenGaps.WeightedHypersurfaceBracket
   5
   6/-!
   7# Wave C2 R3: dynamic structure-function continuum smearing
   8
   9Extends the banked fixed-background continuum reach
  10`BackgroundWeightedContinuumReach` / `weightedStructureSum_tendsto` so that
  11the structure-function profile is induced by a continuum field profile `q`
  12through the same law that inhabits the dynamic lattice bracket:
  13
  14    G(x) = 1 + (q x)^2
  15
  16i.e. the continuum shape of `concreteDynamicInverseMetric` along `q`.
  17The package is witnessed by the HamDyn family
  18(`PhaseSpaceDependentHamiltonianConstruction concreteDynamicInverseMetric`).
  19
  20## Honesty
  21
  22* This rung is the **smearing half** of the continuum story. The sampled-lapse
  23  Wronskian rate-`h` limit remains OPEN inside the ledger terminal R4
  24  (`dirac_algebra_continuum_limit`); this module does **not** introduce or
  25  claim that name.
  26* Does **not** flip `gap5_constraint_recovery`.
  27* Admissible class: `ContinuousOn q (Icc 0 1)` (no narrowing to global
  28  `Continuous` was required).
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Gravity
  33namespace SevenGaps
  34namespace DynamicStructureContinuumSmearing
  35
  36open HypersurfaceDeformation WeightedHypersurfaceBracket
  37open DynamicStructureFunctionBlocker DynamicStructureBracket
  38
  39noncomputable section
  40
  41open Filter Topology
  42
  43/-! ## Continuum structure profile induced by a field -/
  44
  45/-- MODEL. Continuum shape of `concreteDynamicInverseMetric` along a field
  46profile: `G(x) = 1 + (q x)^2`. -/
  47def dynamicStructureProfile (q : ℝ → ℝ) : ℝ → ℝ :=
  48  fun x => 1 + (q x) ^ 2
  49
  50/-- Continuity of the induced structure profile on the unit interval. -/
  51theorem continuousOn_dynamicStructureProfile
  52    (q : ℝ → ℝ) (hq : ContinuousOn q (Set.Icc 0 1)) :
  53    ContinuousOn (dynamicStructureProfile q) (Set.Icc 0 1) := by
  54  unfold dynamicStructureProfile
  55  exact continuousOn_const.add (hq.pow 2)
  56
  57/-- THEOREM (binding lemma). On any phase point whose configuration sample
  58at site `j` equals the field profile at sample location `t`, the lattice
  59structure function equals the continuum profile value. -/
  60theorem concreteDynamicInverseMetric_eq_dynamicStructureProfile
  61    (q : ℝ → ℝ) (x : PhaseSpace 2) (j : ZMod 2) (t : ℝ)
  62    (hx : x.1 j = q t) :
  63    concreteDynamicInverseMetric x j = dynamicStructureProfile q t := by
  64  simp [concreteDynamicInverseMetric, dynamicStructureProfile, hx]
  65
  66/-- Specialization to the Riemann-sum sample points `k/N`. -/
  67theorem concreteDynamicInverseMetric_eq_sample
  68    (q : ℝ → ℝ) (N k : ℕ) (x : PhaseSpace 2) (j : ZMod 2)
  69    (hx : x.1 j = q ((k : ℝ) / (N : ℝ))) :
  70    concreteDynamicInverseMetric x j =
  71      1 + (q ((k : ℝ) / (N : ℝ))) ^ 2 := by
  72  simpa [dynamicStructureProfile] using
  73    concreteDynamicInverseMetric_eq_dynamicStructureProfile q x j
  74      ((k : ℝ) / (N : ℝ)) hx
  75
  76/-! ## Dynamic continuum reach -/
  77
  78/-- Continuum smearing reach for a field-induced structure profile:
  79h-scaled lattice sums of `G * (Wr * S)` tend to the integral on `[0,1]`,
  80with `G = dynamicStructureProfile q`. Unlike
  81`BackgroundWeightedContinuumReach`, the structure profile is a named
  82function of the field data through `1 + q^2`. -/
  83def DynamicWeightedContinuumReach (q : ℝ → ℝ) : Prop :=
  84  ∀ (Wr S : ℝ → ℝ),
  85    ContinuousOn Wr (Set.Icc 0 1) →
  86    ContinuousOn S (Set.Icc 0 1) →
  87    Tendsto
  88      (fun N : ℕ => (1 / (N : ℝ)) * ∑ k ∈ Finset.range N,
  89        dynamicStructureProfile q ((k : ℝ) / (N : ℝ)) *
  90          (Wr ((k : ℝ) / (N : ℝ)) * S ((k : ℝ) / (N : ℝ))))
  91      atTop (nhds (∫ x in (0 : ℝ)..1,
  92        dynamicStructureProfile q x * (Wr x * S x)))
  93
  94/-- THEOREM. Every continuous-on-`[0,1]` field profile induces a dynamic
  95continuum reach via composition through `1 + q^2` and the banked
  96fixed-background quadrature. -/
  97theorem dynamic_weighted_continuum_reach
  98    (q : ℝ → ℝ) (hq : ContinuousOn q (Set.Icc 0 1)) :
  99    DynamicWeightedContinuumReach q := by
 100  intro Wr S hWr hS
 101  exact background_weighted_continuum_reach
 102      (dynamicStructureProfile q)
 103      (continuousOn_dynamicStructureProfile q hq) Wr S hWr hS
 104
 105/-! ## Decoy: fixed-background reach alone does not discharge R3 -/
 106
 107/-- DECOY certificate. The constant field profiles `q₁ ≡ 0` and `q₂ ≡ 1`
 108induce distinct structure profiles (`G ≡ 1` vs `G ≡ 2` at `x = 0`), so no
 109single fixed background weight covers the dynamic family. Re-exporting
 110`weightedStructureSum_tendsto` under a new name with a phase-independent
 111`W` would therefore miss this rung. -/
 112theorem background_weighted_reach_misses_dynamic_family :
 113    dynamicStructureProfile (fun _ => (0 : ℝ)) (0 : ℝ) ≠
 114      dynamicStructureProfile (fun _ => (1 : ℝ)) (0 : ℝ) := by
 115  simp [dynamicStructureProfile]
 116
 117/-- Stronger decoy: there is no single fixed profile `W` that equals
 118`dynamicStructureProfile q` for every continuous field profile `q`. -/
 119theorem no_fixed_profile_equals_all_dynamic_profiles :
 120    ¬ ∃ W : ℝ → ℝ,
 121      ∀ q : ℝ → ℝ, ContinuousOn q (Set.Icc 0 1) →
 122        W = dynamicStructureProfile q := by
 123  intro ⟨W, hW⟩
 124  have h0 := hW (fun _ => (0 : ℝ)) continuousOn_const
 125  have h1 := hW (fun _ => (1 : ℝ)) continuousOn_const
 126  have hEq :
 127      dynamicStructureProfile (fun _ => (0 : ℝ)) =
 128        dynamicStructureProfile (fun _ => (1 : ℝ)) := by
 129    rw [← h0, ← h1]
 130  exact background_weighted_reach_misses_dynamic_family (congrFun hEq 0)
 131
 132/-! ## Packaged residual (Wave C2 R3) -/
 133
 134/-- Typed residual: dynamic continuum smearing witnessed by the HamDyn
 135family. Conjoins (1) reach for every admissible field profile, (2) binding
 136of the continuum law to `concreteDynamicInverseMetric` on sampled phase
 137points, (3) the already-banked Hamiltonian inhabitant. -/
 138def TypedResidual_gap5_dynamic_continuum_smearing : Prop :=
 139  (∀ q : ℝ → ℝ, ContinuousOn q (Set.Icc 0 1) →
 140      DynamicWeightedContinuumReach q) ∧
 141    (∀ (q : ℝ → ℝ) (x : PhaseSpace 2) (j : ZMod 2) (t : ℝ),
 142      x.1 j = q t →
 143        concreteDynamicInverseMetric x j = dynamicStructureProfile q t) ∧
 144      Nonempty
 145        (PhaseSpaceDependentHamiltonianConstruction concreteDynamicInverseMetric)
 146
 147/-- THEOREM (R3 headline). The dynamic continuum-smearing residual holds. -/
 148theorem typedResidual_gap5_dynamic_continuum_smearing :
 149    TypedResidual_gap5_dynamic_continuum_smearing :=
 150  ⟨fun q hq => dynamic_weighted_continuum_reach q hq,
 151    fun q x j t hx =>
 152      concreteDynamicInverseMetric_eq_dynamicStructureProfile q x j t hx,
 153    typedResidual_dynamic_bracket_concrete_two_site⟩
 154
 155/-! ### Axiom receipts -/
 156
 157#print axioms continuousOn_dynamicStructureProfile
 158#print axioms concreteDynamicInverseMetric_eq_dynamicStructureProfile
 159#print axioms dynamic_weighted_continuum_reach
 160#print axioms background_weighted_reach_misses_dynamic_family
 161#print axioms no_fixed_profile_equals_all_dynamic_profiles
 162#print axioms typedResidual_gap5_dynamic_continuum_smearing
 163
 164end
 165end DynamicStructureContinuumSmearing
 166end SevenGaps
 167end Gravity
 168end IndisputableMonolith
 169