IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuum
IndisputableMonolith/Gravity/SevenGaps/DiracAlgebraContinuum.lean · 756 lines · 25 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.QuadratureLimit
3import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket
4import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureContinuumSmearing
5import IndisputableMonolith.Gravity.SevenGaps.WeightedHypersurfaceBracket
6
7/-!
8# Wave C2 R4: dynamic bracket shape continuum (rate-h) + ledger name held free
9
10Lands the sampled-lapse Wronskian rate-`h` residual named as OPEN in
11`weightedStructureSum_tendsto`, packaged with the R2 lattice RHS *shape* and
12the R3 dynamic structure profile as
13`dynamic_bracket_shape_continuum_limit`.
14
15## Honesty / demotion (2026-07-22 Codex critic)
16
17The freestanding Riemann object `sampledDynamicBracketSum` is **not**
18provably equal to `bracket (HamDyn N) (HamDyn M)` at sampled phase points:
19`HamDyn` / `bracket_HamDyn_HamDyn` exist only at `n = 2`, and the
20non-periodic mesh leaves a ZMod wraparound term undischarged. The ledger
21name `dirac_algebra_continuum_limit` is therefore **held free** pending an
22honest general-`n` `HamDynN` binding + periodic wrap treatment. The
23rate-`h` analysis (`wronskian_rate_h_tendsto`, forward-density control)
24remains real and is consumed by the renamed shape theorem.
25
26## Scaling (derived before stating)
27
28Lattice summand shape of `bracket_HamDyn_HamDyn`:
29`W_k * G_k * (π_{k+1} Δq_k)` with
30* discrete Wronskian `W_k = O(1/n)` for C¹ lapses,
31* structure `G_k = 1 + q(k/n)² = O(1)`,
32* raw momentum-flux `π_{k+1} Δq_k = O(1/n)` for C¹ fields.
33Product per site `O(1/n²)`; `n` sites give raw sum `O(1/n)`. The honest
34scaled object is therefore **`n · Σ`**, converging to
35`∫ (N M' - M N') · G · (p · q')`. (An `n²` prefactor would diverge; a bare
36unscaled sum vanishes.)
37
38## Further honesty
39
40* Does **not** flip `gap5_constraint_recovery` (needs R6 as well).
41* Decoy: frozen-1 continuum integrand differs from the dynamic `G = 1+q²`
42 integrand for `q = id`.
43* R3 smearing-shape reach alone does not contain this Wronskian rate content;
44 the new content is `wronskian_rate_h_tendsto`.
45-/
46
47namespace IndisputableMonolith
48namespace Gravity
49namespace SevenGaps
50namespace DiracAlgebraContinuum
51
52open HypersurfaceDeformation WeightedHypersurfaceBracket
53open DynamicStructureFunctionBlocker
54open DynamicStructureBracket DynamicStructureContinuumSmearing
55open Filter Topology Set
56
57noncomputable section
58
59open Finset
60
61/-! ## Continuum profiles -/
62
63/-- Continuum momentum-flux density `D(t) = p(t) · q'(t)`. -/
64def continuumMomentumFlux (p q : ℝ → ℝ) : ℝ → ℝ :=
65 fun t => p t * deriv q t
66
67/-- Continuum Dirac structure density:
68`(N M' - M N') · G · D` with `G = 1 + q²`. -/
69def continuumDiracDensity (N M q p : ℝ → ℝ) : ℝ → ℝ :=
70 fun t =>
71 (N t * deriv M t - M t * deriv N t) *
72 (dynamicStructureProfile q t * continuumMomentumFlux p q t)
73
74/-- Sampled RHS shape of `bracket_HamDyn_HamDyn` on the unit-interval mesh
75`k/n` (non-periodic forward differences). -/
76def sampledDynamicBracketSum (n : ℕ) (N M q p : ℝ → ℝ) : ℝ :=
77 ∑ k ∈ range n,
78 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
79 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) *
80 (dynamicStructureProfile q ((k : ℝ) / n) *
81 (p ((k + 1 : ℕ) / n) * (q ((k + 1 : ℕ) / n) - q ((k : ℝ) / n))))
82
83/-- Continuum Wronskian density `(N M' - M N')`. -/
84def continuumWronskian (N M : ℝ → ℝ) : ℝ → ℝ :=
85 fun t => N t * deriv M t - M t * deriv N t
86
87/-! ## Local mesh facts -/
88
89private lemma mesh_lt (n k : ℕ) (hn : 0 < n) (_hk : k < n) :
90 (k : ℝ) / n < ((k + 1 : ℕ) : ℝ) / n :=
91 div_lt_div_of_pos_right (by exact_mod_cast Nat.lt_succ_self k)
92 (Nat.cast_pos.mpr hn)
93
94private lemma mesh_step (n k : ℕ) :
95 ((k + 1 : ℕ) : ℝ) / n - (k : ℝ) / n = 1 / (n : ℝ) := by
96 rw [Nat.cast_succ, add_div, add_sub_cancel_left]
97
98private lemma mesh_le_one (n k : ℕ) (hk : k < n) :
99 ((k + 1 : ℕ) : ℝ) / n ≤ 1 := by
100 have hn0 : (0 : ℝ) < n := Nat.cast_pos.mpr (Nat.zero_lt_of_lt hk)
101 exact (div_le_one hn0).2 (by exact_mod_cast Nat.succ_le_of_lt hk)
102
103private lemma mesh_nonneg (n k : ℕ) : (0 : ℝ) ≤ (k : ℝ) / n :=
104 div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _)
105
106private lemma sample_mem_Icc (n k : ℕ) (hk : k ≤ n) :
107 (k : ℝ) / n ∈ Icc (0 : ℝ) 1 := by
108 refine ⟨mesh_nonneg n k, ?_⟩
109 rcases Nat.eq_zero_or_pos n with h0 | hn
110 · subst h0; simp
111 · exact (div_le_one (Nat.cast_pos.mpr hn)).2 (by exact_mod_cast hk)
112
113private lemma sample_mem_Icc_lt (n k : ℕ) (hk : k < n) :
114 (k : ℝ) / n ∈ Icc (0 : ℝ) 1 :=
115 sample_mem_Icc n k hk.le
116
117private lemma Ioo_mesh_subset_Icc (n k : ℕ) (_hn : 0 < n) (hk : k < n) :
118 Ioo ((k : ℝ) / n) (((k + 1 : ℕ) : ℝ) / n) ⊆ Icc (0 : ℝ) 1 := by
119 intro x hx
120 exact ⟨le_trans (mesh_nonneg n k) hx.1.le,
121 le_trans hx.2.le (mesh_le_one n k hk)⟩
122
123private lemma exists_norm_bound_on_Icc (f : ℝ → ℝ) (hf : ContinuousOn f (Icc 0 1)) :
124 ∃ C : ℝ, 0 ≤ C ∧ ∀ x ∈ Icc (0 : ℝ) 1, |f x| ≤ C := by
125 obtain ⟨C0, hC0⟩ := isCompact_Icc.exists_bound_of_continuousOn hf
126 refine ⟨max C0 0, le_max_right _ _, fun x hx => ?_⟩
127 have : ‖f x‖ ≤ C0 := hC0 x hx
128 simpa [Real.norm_eq_abs] using le_trans this (le_max_left C0 0)
129
130/-! ## (A) Rate-h Wronskian quadrature -/
131
132/-- Discrete Wronskian via two mean-value applications. -/
133theorem discrete_wronskian_mvt (N M : ℝ → ℝ)
134 (hN : ContDiff ℝ 1 N) (hM : ContDiff ℝ 1 M)
135 (n k : ℕ) (hn : 0 < n) (hk : k < n) :
136 ∃ c ∈ Ioo ((k : ℝ) / n) (((k + 1 : ℕ) : ℝ) / n),
137 ∃ d ∈ Ioo ((k : ℝ) / n) (((k + 1 : ℕ) : ℝ) / n),
138 N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
139 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)
140 = (1 / (n : ℝ)) *
141 (N ((k : ℝ) / n) * deriv M c - M ((k : ℝ) / n) * deriv N d) := by
142 set a : ℝ := (k : ℝ) / n
143 set b : ℝ := ((k + 1 : ℕ) : ℝ) / n
144 have hab : a < b := mesh_lt n k hn hk
145 have hIcc_ab : Icc a b ⊆ Icc (0 : ℝ) 1 := by
146 intro x hx
147 exact ⟨le_trans (mesh_nonneg n k) hx.1, le_trans hx.2 (mesh_le_one n k hk)⟩
148 have hNdiff : Differentiable ℝ N := hN.differentiable (by norm_num)
149 have hMdiff : Differentiable ℝ M := hM.differentiable (by norm_num)
150 have hNc : ContinuousOn N (Icc a b) := hN.continuous.continuousOn.mono hIcc_ab
151 have hMc : ContinuousOn M (Icc a b) := hM.continuous.continuousOn.mono hIcc_ab
152 have hNd : DifferentiableOn ℝ N (Ioo a b) := fun x _ => (hNdiff x).differentiableWithinAt
153 have hMd : DifferentiableOn ℝ M (Ioo a b) := fun x _ => (hMdiff x).differentiableWithinAt
154 obtain ⟨c, hc, hcEq⟩ := exists_deriv_eq_slope M hab hMc hMd
155 obtain ⟨d, hd, hdEq⟩ := exists_deriv_eq_slope N hab hNc hNd
156 refine ⟨c, hc, d, hd, ?_⟩
157 have hden : b - a = 1 / (n : ℝ) := by
158 dsimp [a, b]; exact mesh_step n k
159 have hMdiff' : M b - M a = (1 / (n : ℝ)) * deriv M c := by
160 have : deriv M c = (M b - M a) / (b - a) := hcEq
161 rw [this, hden]; field_simp
162 have hNdiff' : N b - N a = (1 / (n : ℝ)) * deriv N d := by
163 have : deriv N d = (N b - N a) / (b - a) := hdEq
164 rw [this, hden]; field_simp
165 calc
166 N a * M b - M a * N b
167 = N a * (M b - M a) - M a * (N b - N a) := by ring
168 _ = N a * ((1 / (n : ℝ)) * deriv M c) - M a * ((1 / (n : ℝ)) * deriv N d) := by
169 rw [hMdiff', hNdiff']
170 _ = (1 / (n : ℝ)) * (N a * deriv M c - M a * deriv N d) := by ring
171
172private lemma continuous_continuumWronskian (N M : ℝ → ℝ)
173 (hN : ContDiff ℝ 1 N) (hM : ContDiff ℝ 1 M) :
174 Continuous (continuumWronskian N M) :=
175 (hN.continuous.mul hM.continuous_deriv_one).sub
176 (hM.continuous.mul hN.continuous_deriv_one)
177
178private lemma wronskian_cell_error_abs (N M : ℝ → ℝ)
179 (n k : ℕ) (hn : 0 < n)
180 {c d : ℝ}
181 (hEq : N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
182 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)
183 = (1 / (n : ℝ)) *
184 (N ((k : ℝ) / n) * deriv M c - M ((k : ℝ) / n) * deriv N d)) :
185 |(N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
186 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
187 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)|
188 = (1 / (n : ℝ)) *
189 |N ((k : ℝ) / n) * (deriv M c - deriv M ((k : ℝ) / n)) -
190 M ((k : ℝ) / n) * (deriv N d - deriv N ((k : ℝ) / n))| := by
191 have hcell :
192 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
193 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
194 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)
195 = (1 / (n : ℝ)) *
196 (N ((k : ℝ) / n) * (deriv M c - deriv M ((k : ℝ) / n)) -
197 M ((k : ℝ) / n) * (deriv N d - deriv N ((k : ℝ) / n))) := by
198 rw [hEq]; simp only [continuumWronskian]; ring
199 have hnR : (0 : ℝ) < n := Nat.cast_pos.mpr hn
200 rw [hcell, abs_mul, abs_of_pos (div_pos one_pos hnR)]
201
202/-- THEOREM (A). Sampled-lapse Wronskian rate-`h` quadrature limit. -/
203theorem wronskian_rate_h_tendsto (N M F : ℝ → ℝ)
204 (hN : ContDiff ℝ 1 N) (hM : ContDiff ℝ 1 M)
205 (hF : ContinuousOn F (Icc 0 1)) :
206 Tendsto
207 (fun n : ℕ =>
208 ∑ k ∈ range n,
209 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
210 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) *
211 F ((k : ℝ) / n))
212 atTop
213 (nhds (∫ t in (0 : ℝ)..1, continuumWronskian N M t * F t)) := by
214 have hWrCont : ContinuousOn (continuumWronskian N M) (Icc 0 1) :=
215 (continuous_continuumWronskian N M hN hM).continuousOn
216 have hRiemann :
217 Tendsto
218 (fun n : ℕ =>
219 (1 / (n : ℝ)) *
220 ∑ k ∈ range n, continuumWronskian N M ((k : ℝ) / n) * F ((k : ℝ) / n))
221 atTop (nhds (∫ t in (0 : ℝ)..1, continuumWronskian N M t * F t)) :=
222 Analysis.weightedLatticeSum_tendsto (continuumWronskian N M) F hWrCont hF
223 have hErr :
224 Tendsto
225 (fun n : ℕ =>
226 ∑ k ∈ range n,
227 ((N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
228 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
229 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)) *
230 F ((k : ℝ) / n))
231 atTop (nhds 0) := by
232 obtain ⟨BN, hBN0, hBN⟩ :=
233 exists_norm_bound_on_Icc N hN.continuous.continuousOn
234 obtain ⟨BM, hBM0, hBM⟩ :=
235 exists_norm_bound_on_Icc M hM.continuous.continuousOn
236 obtain ⟨BF, hBF0, hBF⟩ := exists_norm_bound_on_Icc F hF
237 have hNdb : ContinuousOn (deriv N) (Icc 0 1) :=
238 hN.continuous_deriv_one.continuousOn
239 have hMdb : ContinuousOn (deriv M) (Icc 0 1) :=
240 hM.continuous_deriv_one.continuousOn
241 rw [Metric.tendsto_atTop]
242 intro ε hε
243 set K : ℝ := BN * BF + BM * BF + 1
244 have hKpos : 0 < K := by
245 have : 0 ≤ BN * BF := mul_nonneg hBN0 hBF0
246 have : 0 ≤ BM * BF := mul_nonneg hBM0 hBF0
247 positivity
248 set ε' : ℝ := ε / (2 * K)
249 have hε' : 0 < ε' := div_pos hε (by positivity)
250 obtain ⟨δN, hδNpos, hδN⟩ :=
251 Metric.uniformContinuousOn_iff_le.1
252 (isCompact_Icc.uniformContinuousOn_of_continuous hNdb) ε' hε'
253 obtain ⟨δM, hδMpos, hδM⟩ :=
254 Metric.uniformContinuousOn_iff_le.1
255 (isCompact_Icc.uniformContinuousOn_of_continuous hMdb) ε' hε'
256 set δ : ℝ := min δN δM
257 have hδpos : 0 < δ := lt_min hδNpos hδMpos
258 obtain ⟨M₀, hM₀⟩ := exists_nat_ge (1 / δ)
259 refine ⟨max M₀ 1, fun n hnAll => ?_⟩
260 have hn1 : 1 ≤ n := le_trans (le_max_right M₀ 1) hnAll
261 have hnM : M₀ ≤ n := le_trans (le_max_left M₀ 1) hnAll
262 have hnpos : 0 < n := lt_of_lt_of_le Nat.zero_lt_one hn1
263 have hnR : (0 : ℝ) < n := Nat.cast_pos.mpr hnpos
264 have hmesh : (1 : ℝ) / n ≤ δ := by
265 have h1 : (1 : ℝ) / δ ≤ n := le_trans hM₀ (by exact_mod_cast hnM)
266 have : δ * ((1 : ℝ) / δ) ≤ δ * n :=
267 mul_le_mul_of_nonneg_left h1 hδpos.le
268 have : (1 : ℝ) ≤ δ * n := by convert this using 1; field_simp
269 exact (div_le_iff₀ hnR).2 (by linarith)
270 have hmeshN : (1 : ℝ) / n ≤ δN := le_trans hmesh (min_le_left _ _)
271 have hmeshM : (1 : ℝ) / n ≤ δM := le_trans hmesh (min_le_right _ _)
272 have hterm : ∀ k ∈ range n,
273 |((N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
274 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
275 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)) *
276 F ((k : ℝ) / n)|
277 ≤ (1 / (n : ℝ)) * ε' * (BN * BF + BM * BF) := by
278 intro k hk
279 have hk' : k < n := mem_range.1 hk
280 obtain ⟨c, hc, d, hd, hEq⟩ := discrete_wronskian_mvt N M hN hM n k hnpos hk'
281 have ha : (k : ℝ) / n ∈ Icc (0 : ℝ) 1 := sample_mem_Icc_lt n k hk'
282 have hb : ((k + 1 : ℕ) : ℝ) / n ∈ Icc (0 : ℝ) 1 :=
283 sample_mem_Icc n (k + 1) (Nat.succ_le_of_lt hk')
284 have hcI : c ∈ Icc (0 : ℝ) 1 := Ioo_mesh_subset_Icc n k hnpos hk' hc
285 have hdI : d ∈ Icc (0 : ℝ) 1 := Ioo_mesh_subset_Icc n k hnpos hk' hd
286 have hdistc : dist c ((k : ℝ) / n) ≤ δM := by
287 rw [Real.dist_eq, abs_of_nonneg (sub_nonneg.2 hc.1.le)]
288 have : c - (k : ℝ) / n ≤ 1 / (n : ℝ) := by
289 have := hc.2.le; have := mesh_step n k; linarith
290 exact le_trans this hmeshM
291 have hdistd : dist d ((k : ℝ) / n) ≤ δN := by
292 rw [Real.dist_eq, abs_of_nonneg (sub_nonneg.2 hd.1.le)]
293 have : d - (k : ℝ) / n ≤ 1 / (n : ℝ) := by
294 have := hd.2.le; have := mesh_step n k; linarith
295 exact le_trans this hmeshN
296 have hdM : |deriv M c - deriv M ((k : ℝ) / n)| ≤ ε' := by
297 simpa [Real.dist_eq] using hδM c hcI ((k : ℝ) / n) ha hdistc
298 have hdN : |deriv N d - deriv N ((k : ℝ) / n)| ≤ ε' := by
299 simpa [Real.dist_eq] using hδN d hdI ((k : ℝ) / n) ha hdistd
300 have hAbs := wronskian_cell_error_abs N M n k hnpos hEq
301 have herr :
302 |N ((k : ℝ) / n) * (deriv M c - deriv M ((k : ℝ) / n)) -
303 M ((k : ℝ) / n) * (deriv N d - deriv N ((k : ℝ) / n))|
304 ≤ BN * ε' + BM * ε' := by
305 calc
306 _ ≤ |N ((k : ℝ) / n)| * |deriv M c - deriv M ((k : ℝ) / n)| +
307 |M ((k : ℝ) / n)| * |deriv N d - deriv N ((k : ℝ) / n)| := by
308 calc
309 _ ≤ |N ((k : ℝ) / n) * (deriv M c - deriv M ((k : ℝ) / n))| +
310 |M ((k : ℝ) / n) * (deriv N d - deriv N ((k : ℝ) / n))| :=
311 abs_sub _ _
312 _ = |N ((k : ℝ) / n)| * |deriv M c - deriv M ((k : ℝ) / n)| +
313 |M ((k : ℝ) / n)| * |deriv N d - deriv N ((k : ℝ) / n)| := by
314 simp [abs_mul]
315 _ ≤ BN * ε' + BM * ε' := by
316 refine add_le_add ?_ ?_
317 · exact mul_le_mul (hBN _ ha) hdM (abs_nonneg _) hBN0
318 · exact mul_le_mul (hBM _ ha) hdN (abs_nonneg _) hBM0
319 calc
320 |((N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
321 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
322 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)) *
323 F ((k : ℝ) / n)|
324 = |(N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
325 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
326 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)| *
327 |F ((k : ℝ) / n)| := abs_mul _ _
328 _ = (1 / (n : ℝ)) *
329 |N ((k : ℝ) / n) * (deriv M c - deriv M ((k : ℝ) / n)) -
330 M ((k : ℝ) / n) * (deriv N d - deriv N ((k : ℝ) / n))| *
331 |F ((k : ℝ) / n)| := by rw [hAbs]
332 _ ≤ (1 / (n : ℝ)) * (BN * ε' + BM * ε') * BF := by
333 refine mul_le_mul ?_ (hBF _ ha) (abs_nonneg _) (by positivity)
334 exact mul_le_mul_of_nonneg_left herr (div_nonneg zero_le_one hnR.le)
335 _ = (1 / (n : ℝ)) * ε' * (BN * BF + BM * BF) := by ring
336 have hsum :
337 |∑ k ∈ range n,
338 ((N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
339 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
340 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)) *
341 F ((k : ℝ) / n)|
342 ≤ ε' * (BN * BF + BM * BF) := by
343 calc
344 _ ≤ ∑ k ∈ range n,
345 |((N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
346 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
347 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)) *
348 F ((k : ℝ) / n)| :=
349 abs_sum_le_sum_abs _ _
350 _ ≤ ∑ _k ∈ range n, (1 / (n : ℝ)) * ε' * (BN * BF + BM * BF) :=
351 sum_le_sum hterm
352 _ = (n : ℝ) * ((1 / (n : ℝ)) * ε' * (BN * BF + BM * BF)) := by
353 rw [sum_const, card_range, nsmul_eq_mul]
354 _ = ε' * (BN * BF + BM * BF) := by field_simp
355 have hfinal : ε' * (BN * BF + BM * BF) < ε := by
356 have hle : BN * BF + BM * BF ≤ K := by simp only [K]; linarith
357 have : ε' * (BN * BF + BM * BF) ≤ ε' * K :=
358 mul_le_mul_of_nonneg_left hle hε'.le
359 have hhalf : ε' * K = ε / 2 := by simp only [ε']; field_simp
360 linarith
361 rw [Real.dist_eq]
362 have hdist : |∑ k ∈ range n,
363 ((N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
364 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
365 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)) *
366 F ((k : ℝ) / n) - 0| =
367 |∑ k ∈ range n,
368 ((N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
369 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
370 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)) *
371 F ((k : ℝ) / n)| := by simp
372 rw [hdist]
373 exact lt_of_le_of_lt hsum hfinal
374 have haddRM := hRiemann.add hErr
375 have hlimRM :
376 (∫ t in (0 : ℝ)..1, continuumWronskian N M t * F t) + 0
377 = ∫ t in (0 : ℝ)..1, continuumWronskian N M t * F t :=
378 add_zero _
379 have hMain' :
380 Tendsto
381 (fun n : ℕ =>
382 (1 / (n : ℝ)) *
383 ∑ k ∈ range n,
384 continuumWronskian N M ((k : ℝ) / n) * F ((k : ℝ) / n) +
385 ∑ k ∈ range n,
386 ((N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
387 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) -
388 (1 / (n : ℝ)) * continuumWronskian N M ((k : ℝ) / n)) *
389 F ((k : ℝ) / n))
390 atTop (nhds (∫ t in (0 : ℝ)..1, continuumWronskian N M t * F t)) := by
391 -- `convert` reduces the `nhds` mismatch to the bare limit equality.
392 convert haddRM
393 exact hlimRM.symm
394 refine hMain'.congr fun n => ?_
395 rw [Finset.mul_sum, ← sum_add_distrib]
396 refine sum_congr rfl fun k _ => ?_
397 ring
398
399/-! ## Forward-difference rate for C¹ profiles -/
400
401theorem forward_diff_mvt (q : ℝ → ℝ) (hq : ContDiff ℝ 1 q)
402 (n k : ℕ) (hn : 0 < n) (hk : k < n) :
403 ∃ c ∈ Ioo ((k : ℝ) / n) (((k + 1 : ℕ) : ℝ) / n),
404 (n : ℝ) * (q ((k + 1 : ℕ) / n) - q ((k : ℝ) / n)) = deriv q c := by
405 set a : ℝ := (k : ℝ) / n
406 set b : ℝ := ((k + 1 : ℕ) : ℝ) / n
407 have hab : a < b := mesh_lt n k hn hk
408 have hIcc_ab : Icc a b ⊆ Icc (0 : ℝ) 1 := by
409 intro x hx
410 exact ⟨le_trans (mesh_nonneg n k) hx.1, le_trans hx.2 (mesh_le_one n k hk)⟩
411 have hqdiff : Differentiable ℝ q := hq.differentiable (by norm_num)
412 have hqc : ContinuousOn q (Icc a b) := hq.continuous.continuousOn.mono hIcc_ab
413 have hqd : DifferentiableOn ℝ q (Ioo a b) := fun x _ => (hqdiff x).differentiableWithinAt
414 obtain ⟨c, hc, hcEq⟩ := exists_deriv_eq_slope q hab hqc hqd
415 refine ⟨c, hc, ?_⟩
416 have hden : b - a = 1 / (n : ℝ) := by
417 dsimp [a, b]; exact mesh_step n k
418 have : deriv q c = (q b - q a) / (b - a) := hcEq
419 rw [this, hden]
420 have hnR : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
421 field_simp
422
423/-- Uniform control: scaled forward density vs `p · q'`. -/
424theorem forward_density_uniform (q p : ℝ → ℝ)
425 (hq : ContDiff ℝ 1 q) (hp : ContinuousOn p (Icc 0 1)) :
426 ∀ ε > 0, ∃ N₀ : ℕ, ∀ n ≥ N₀, ∀ k < n,
427 |p ((k + 1 : ℕ) / n) * ((n : ℝ) * (q ((k + 1 : ℕ) / n) - q ((k : ℝ) / n))) -
428 p ((k : ℝ) / n) * deriv q ((k : ℝ) / n)| < ε := by
429 obtain ⟨BP, hBP0, hBP⟩ := exists_norm_bound_on_Icc p hp
430 obtain ⟨Bq', hBq'0, hBq'⟩ :=
431 exists_norm_bound_on_Icc (deriv q) hq.continuous_deriv_one.continuousOn
432 have hqd := hq.continuous_deriv_one
433 intro ε hε
434 set ε' : ℝ := ε / (2 * (BP + Bq' + 1))
435 have hε' : 0 < ε' := div_pos hε (by positivity)
436 obtain ⟨δp, hδppos, hδp⟩ :=
437 Metric.uniformContinuousOn_iff_le.1
438 (isCompact_Icc.uniformContinuousOn_of_continuous hp) ε' hε'
439 obtain ⟨δq, hδqpos, hδq⟩ :=
440 Metric.uniformContinuousOn_iff_le.1
441 (isCompact_Icc.uniformContinuousOn_of_continuous hqd.continuousOn) ε' hε'
442 set δ : ℝ := min δp δq
443 have hδpos : 0 < δ := lt_min hδppos hδqpos
444 obtain ⟨M₀, hM₀⟩ := exists_nat_ge (1 / δ)
445 refine ⟨max M₀ 1, fun n hnAll k hk => ?_⟩
446 have hn1 : 1 ≤ n := le_trans (le_max_right M₀ 1) hnAll
447 have hnM : M₀ ≤ n := le_trans (le_max_left M₀ 1) hnAll
448 have hnpos : 0 < n := lt_of_lt_of_le Nat.zero_lt_one hn1
449 have hnR : (0 : ℝ) < n := Nat.cast_pos.mpr hnpos
450 have hmesh : (1 : ℝ) / n ≤ δ := by
451 have h1 : (1 : ℝ) / δ ≤ n := le_trans hM₀ (by exact_mod_cast hnM)
452 have : δ * ((1 : ℝ) / δ) ≤ δ * n :=
453 mul_le_mul_of_nonneg_left h1 hδpos.le
454 have : (1 : ℝ) ≤ δ * n := by convert this using 1; field_simp
455 exact (div_le_iff₀ hnR).2 (by linarith)
456 have hmeshp : (1 : ℝ) / n ≤ δp := le_trans hmesh (min_le_left _ _)
457 have hmeshq : (1 : ℝ) / n ≤ δq := le_trans hmesh (min_le_right _ _)
458 obtain ⟨c, hc, hcEq⟩ := forward_diff_mvt q hq n k hnpos hk
459 have ha : (k : ℝ) / n ∈ Icc (0 : ℝ) 1 := sample_mem_Icc_lt n k hk
460 have hb : ((k + 1 : ℕ) : ℝ) / n ∈ Icc (0 : ℝ) 1 :=
461 sample_mem_Icc n (k + 1) (Nat.succ_le_of_lt hk)
462 have hcI : c ∈ Icc (0 : ℝ) 1 := Ioo_mesh_subset_Icc n k hnpos hk hc
463 have hdistc : dist c ((k : ℝ) / n) ≤ δq := by
464 rw [Real.dist_eq, abs_of_nonneg (sub_nonneg.2 hc.1.le)]
465 have : c - (k : ℝ) / n ≤ 1 / (n : ℝ) := by
466 have := hc.2.le; have := mesh_step n k; linarith
467 exact le_trans this hmeshq
468 have hdistp : dist (((k + 1 : ℕ) : ℝ) / n) ((k : ℝ) / n) ≤ δp := by
469 rw [Real.dist_eq, abs_of_nonneg (sub_nonneg.2 (mesh_lt n k hnpos hk).le)]
470 rw [mesh_step]; exact hmeshp
471 have hqerr : |deriv q c - deriv q ((k : ℝ) / n)| ≤ ε' := by
472 simpa [Real.dist_eq] using hδq c hcI ((k : ℝ) / n) ha hdistc
473 have hperr : |p ((k + 1 : ℕ) / n) - p ((k : ℝ) / n)| ≤ ε' := by
474 simpa [Real.dist_eq] using hδp _ hb _ ha hdistp
475 have hrew :
476 p ((k + 1 : ℕ) / n) * ((n : ℝ) * (q ((k + 1 : ℕ) / n) - q ((k : ℝ) / n))) -
477 p ((k : ℝ) / n) * deriv q ((k : ℝ) / n)
478 = (p ((k + 1 : ℕ) / n) - p ((k : ℝ) / n)) * deriv q c +
479 p ((k : ℝ) / n) * (deriv q c - deriv q ((k : ℝ) / n)) := by
480 rw [hcEq]; ring
481 rw [hrew]
482 have h1 : |(p ((k + 1 : ℕ) / n) - p ((k : ℝ) / n)) * deriv q c| ≤ ε' * Bq' := by
483 rw [abs_mul]
484 exact mul_le_mul hperr (hBq' c hcI) (abs_nonneg _) hε'.le
485 have h2 : |p ((k : ℝ) / n) * (deriv q c - deriv q ((k : ℝ) / n))| ≤ BP * ε' := by
486 rw [abs_mul]
487 exact mul_le_mul (hBP _ ha) hqerr (abs_nonneg _) hBP0
488 have hsum :=
489 le_trans (abs_add_le _ _) (add_le_add h1 h2)
490 have hbound : ε' * Bq' + BP * ε' < ε := by
491 have : ε' * (BP + Bq') ≤ ε' * (BP + Bq' + 1) :=
492 mul_le_mul_of_nonneg_left (by linarith) hε'.le
493 have hhalf : ε' * (BP + Bq' + 1) = ε / 2 := by simp only [ε']; field_simp
494 linarith
495 exact lt_of_le_of_lt hsum hbound
496
497/-! ## Binding lemmas (R2 / R3) -/
498
499theorem dynamicStructureProfile_eq_one_add_sq (q : ℝ → ℝ) (t : ℝ) :
500 dynamicStructureProfile q t = 1 + (q t) ^ 2 :=
501 rfl
502
503theorem bracket_HamDyn_shape (N M : ZMod 2 → ℝ) (x : PhaseSpace 2) :
504 bracket (HamDyn N) (HamDyn M) x
505 = ∑ j : ZMod 2, (N j * M (j + 1) - M j * N (j + 1)) *
506 (DynamicStructureFunctionBlocker.concreteDynamicInverseMetric x j *
507 (x.2 (j + 1) * (x.1 (j + 1) - x.1 j))) :=
508 bracket_HamDyn_HamDyn N M x
509
510theorem sampledDynamicBracketSum_scaled_eq (n : ℕ) (N M q p : ℝ → ℝ) :
511 (n : ℝ) * sampledDynamicBracketSum n N M q p
512 = ∑ k ∈ range n,
513 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
514 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) *
515 (dynamicStructureProfile q ((k : ℝ) / n) *
516 (p ((k + 1 : ℕ) / n) *
517 ((n : ℝ) * (q ((k + 1 : ℕ) / n) - q ((k : ℝ) / n))))) := by
518 unfold sampledDynamicBracketSum
519 rw [mul_sum]
520 refine sum_congr rfl fun k _ => ?_
521 ring
522
523/-! ## Wronskian × uniform error → 0 -/
524
525private theorem wronskian_times_uniform_error_tendsto_zero
526 (N M : ℝ → ℝ) (err : ℕ → ℕ → ℝ)
527 (hN : ContDiff ℝ 1 N) (hM : ContDiff ℝ 1 M)
528 (herr : ∀ ε > 0, ∃ N₀ : ℕ, ∀ n ≥ N₀, ∀ k < n, |err n k| < ε) :
529 Tendsto
530 (fun n : ℕ =>
531 ∑ k ∈ range n,
532 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
533 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) * err n k)
534 atTop (nhds 0) := by
535 obtain ⟨BN, hBN0, hBN⟩ :=
536 exists_norm_bound_on_Icc N hN.continuous.continuousOn
537 obtain ⟨BM, hBM0, hBM⟩ :=
538 exists_norm_bound_on_Icc M hM.continuous.continuousOn
539 obtain ⟨BNd, hBNd0, hBNd⟩ :=
540 exists_norm_bound_on_Icc (deriv N) hN.continuous_deriv_one.continuousOn
541 obtain ⟨BMd, hBMd0, hBMd⟩ :=
542 exists_norm_bound_on_Icc (deriv M) hM.continuous_deriv_one.continuousOn
543 have hWbound : ∀ (n k : ℕ), 0 < n → k < n →
544 |N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
545 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)|
546 ≤ (1 / (n : ℝ)) * (BN * BMd + BM * BNd) := by
547 intro n k hn hk
548 obtain ⟨c, hc, d, hd, hEq⟩ := discrete_wronskian_mvt N M hN hM n k hn hk
549 have ha := sample_mem_Icc_lt n k hk
550 have hcI := Ioo_mesh_subset_Icc n k hn hk hc
551 have hdI := Ioo_mesh_subset_Icc n k hn hk hd
552 have hnR : (0 : ℝ) < n := Nat.cast_pos.mpr hn
553 rw [hEq, abs_mul, abs_of_pos (div_pos one_pos hnR)]
554 have :
555 |N ((k : ℝ) / n) * deriv M c - M ((k : ℝ) / n) * deriv N d|
556 ≤ BN * BMd + BM * BNd := by
557 calc
558 _ ≤ |N ((k : ℝ) / n)| * |deriv M c| + |M ((k : ℝ) / n)| * |deriv N d| := by
559 rw [← abs_mul, ← abs_mul]; exact abs_sub _ _
560 _ ≤ BN * BMd + BM * BNd := by
561 refine add_le_add ?_ ?_
562 · exact mul_le_mul (hBN _ ha) (hBMd c hcI) (abs_nonneg _) hBN0
563 · exact mul_le_mul (hBM _ ha) (hBNd d hdI) (abs_nonneg _) hBM0
564 exact mul_le_mul_of_nonneg_left this (div_nonneg zero_le_one hnR.le)
565 rw [Metric.tendsto_atTop]
566 intro ε hε
567 set C : ℝ := BN * BMd + BM * BNd + 1
568 have hCpos : 0 < C := by
569 have : 0 ≤ BN * BMd := mul_nonneg hBN0 hBMd0
570 have : 0 ≤ BM * BNd := mul_nonneg hBM0 hBNd0
571 positivity
572 obtain ⟨N₀, hN₀⟩ := herr (ε / (2 * C)) (by positivity)
573 refine ⟨max N₀ 1, fun n hnAll => ?_⟩
574 have hn1 : 1 ≤ n := le_trans (le_max_right N₀ 1) hnAll
575 have hnN : N₀ ≤ n := le_trans (le_max_left N₀ 1) hnAll
576 have hnpos : 0 < n := lt_of_lt_of_le Nat.zero_lt_one hn1
577 have herr' : ∀ k < n, |err n k| < ε / (2 * C) := hN₀ n hnN
578 set η : ℝ := ε / (2 * C)
579 have hηpos : 0 < η := by positivity
580 have hterm : ∀ k ∈ range n,
581 |(N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
582 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) * err n k|
583 ≤ (1 / (n : ℝ)) * (BN * BMd + BM * BNd) * η := by
584 intro k hk
585 have hk' : k < n := mem_range.1 hk
586 have h1 := hWbound n k hnpos hk'
587 have h2 : |err n k| ≤ η := (herr' k hk').le
588 rw [abs_mul]
589 exact mul_le_mul h1 h2 (abs_nonneg _) (by positivity)
590 have hsum :
591 |∑ k ∈ range n,
592 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
593 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) * err n k|
594 ≤ (BN * BMd + BM * BNd) * η := by
595 calc
596 _ ≤ ∑ k ∈ range n,
597 |(N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
598 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) * err n k| :=
599 abs_sum_le_sum_abs _ _
600 _ ≤ ∑ _k ∈ range n, (1 / (n : ℝ)) * (BN * BMd + BM * BNd) * η :=
601 sum_le_sum hterm
602 _ = (BN * BMd + BM * BNd) * η := by
603 rw [sum_const, card_range, nsmul_eq_mul]; field_simp
604 have hfinal : (BN * BMd + BM * BNd) * η < ε := by
605 have hle : BN * BMd + BM * BNd ≤ C := by simp only [C]; linarith
606 have : (BN * BMd + BM * BNd) * η ≤ C * η :=
607 mul_le_mul_of_nonneg_right hle hηpos.le
608 have : C * η = ε / 2 := by simp only [η]; field_simp
609 linarith
610 rw [Real.dist_eq]
611 have hdist :
612 |∑ k ∈ range n,
613 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
614 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) * err n k - 0| =
615 |∑ k ∈ range n,
616 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
617 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) * err n k| := by
618 simp
619 rw [hdist]
620 exact lt_of_le_of_lt hsum hfinal
621
622/-! ## (B) Shape continuum (not the ledger terminal) -/
623
624/-- THEOREM (B, shape only). Sampled-and-scaled freestanding dynamic-bracket
625*shape* sums converge to the continuum Dirac hypersurface-deformation density
626with phase-space-dependent structure function `G = 1 + q²`.
627
628This is a true Riemann / rate-`h` theorem about `sampledDynamicBracketSum`.
629It is **not** a binding of `bracket (HamDyn ·) (HamDyn ·)` (that object is
630only at `n = 2`), and it does **not** occupy the ledger name
631`dirac_algebra_continuum_limit`.
632
633Scaling: `n · Σ W_k G_k (π_{k+1} Δq_k) → ∫ (N M' - M N') G (p q')`. -/
634theorem dynamic_bracket_shape_continuum_limit (N M q p : ℝ → ℝ)
635 (hN : ContDiff ℝ 1 N) (hM : ContDiff ℝ 1 M) (hq : ContDiff ℝ 1 q)
636 (hp : ContinuousOn p (Icc 0 1)) :
637 Tendsto (fun n : ℕ => (n : ℝ) * sampledDynamicBracketSum n N M q p)
638 atTop
639 (nhds (∫ t in (0 : ℝ)..1, continuumDiracDensity N M q p t)) := by
640 have hG : ContinuousOn (dynamicStructureProfile q) (Icc 0 1) :=
641 continuousOn_dynamicStructureProfile q hq.continuous.continuousOn
642 have hF : ContinuousOn
643 (fun t => dynamicStructureProfile q t * continuumMomentumFlux p q t)
644 (Icc 0 1) :=
645 hG.mul (hp.mul hq.continuous_deriv_one.continuousOn)
646 have hMain :=
647 wronskian_rate_h_tendsto N M
648 (fun t => dynamicStructureProfile q t * continuumMomentumFlux p q t)
649 hN hM hF
650 -- Target integral equality (definitional after unfolding the density abbrevs).
651 have hint :
652 (∫ t in (0 : ℝ)..1,
653 continuumWronskian N M t *
654 (dynamicStructureProfile q t * continuumMomentumFlux p q t))
655 = ∫ t in (0 : ℝ)..1, continuumDiracDensity N M q p t :=
656 intervalIntegral.integral_congr fun t _ => by
657 simp only [continuumDiracDensity, continuumWronskian]
658 let densErr (n k : ℕ) : ℝ :=
659 p ((k + 1 : ℕ) / n) * ((n : ℝ) * (q ((k + 1 : ℕ) / n) - q ((k : ℝ) / n))) -
660 continuumMomentumFlux p q ((k : ℝ) / n)
661 let err (n k : ℕ) : ℝ :=
662 dynamicStructureProfile q ((k : ℝ) / n) * densErr n k
663 obtain ⟨BG, hBG0, hBG⟩ := exists_norm_bound_on_Icc _ hG
664 have herr : ∀ ε > 0, ∃ N₀ : ℕ, ∀ n ≥ N₀, ∀ k < n, |err n k| < ε := by
665 intro ε hε
666 obtain ⟨N₀, hN₀⟩ :=
667 forward_density_uniform q p hq hp (ε / (BG + 1)) (by positivity)
668 refine ⟨N₀, fun n hn k hk => ?_⟩
669 have ha : (k : ℝ) / n ∈ Icc (0 : ℝ) 1 := sample_mem_Icc_lt n k hk
670 have hde : |densErr n k| < ε / (BG + 1) := by
671 simpa [densErr, continuumMomentumFlux] using hN₀ n hn k hk
672 have hbound : |err n k| ≤ (BG + 1) * |densErr n k| := by
673 dsimp [err]
674 rw [abs_mul]
675 have : |dynamicStructureProfile q ((k : ℝ) / n)| ≤ BG + 1 :=
676 le_trans (hBG _ ha) (by linarith)
677 exact mul_le_mul this le_rfl (abs_nonneg _) (by linarith)
678 have hlt : (BG + 1) * |densErr n k| < (BG + 1) * (ε / (BG + 1)) :=
679 mul_lt_mul_of_pos_left hde (by positivity)
680 have hεeq : (BG + 1) * (ε / (BG + 1)) = ε := by field_simp
681 linarith
682 have hErrTend :=
683 wronskian_times_uniform_error_tendsto_zero N M err hN hM herr
684 have hEq : ∀ n : ℕ,
685 (n : ℝ) * sampledDynamicBracketSum n N M q p
686 = (∑ k ∈ range n,
687 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
688 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) *
689 (dynamicStructureProfile q ((k : ℝ) / n) *
690 continuumMomentumFlux p q ((k : ℝ) / n))) +
691 ∑ k ∈ range n,
692 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
693 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) * err n k := by
694 intro n
695 rw [sampledDynamicBracketSum_scaled_eq, ← sum_add_distrib]
696 refine sum_congr rfl fun k _ => ?_
697 dsimp [err, densErr, continuumMomentumFlux]
698 ring
699 have hadd := hMain.add hErrTend
700 have hlimEq :
701 (∫ t in (0 : ℝ)..1,
702 continuumWronskian N M t *
703 (dynamicStructureProfile q t * continuumMomentumFlux p q t)) + 0
704 = ∫ t in (0 : ℝ)..1, continuumDiracDensity N M q p t := by
705 rw [add_zero, hint]
706 have hadd' :
707 Tendsto
708 (fun n : ℕ =>
709 (∑ k ∈ range n,
710 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
711 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) *
712 (dynamicStructureProfile q ((k : ℝ) / n) *
713 continuumMomentumFlux p q ((k : ℝ) / n))) +
714 ∑ k ∈ range n,
715 (N ((k : ℝ) / n) * M ((k + 1 : ℕ) / n) -
716 M ((k : ℝ) / n) * N ((k + 1 : ℕ) / n)) * err n k)
717 atTop
718 (nhds (∫ t in (0 : ℝ)..1, continuumDiracDensity N M q p t)) := by
719 -- `convert` reduces the `nhds` mismatch to the bare limit equality.
720 convert hadd
721 exact hlimEq.symm
722 exact hadd'.congr fun n => (hEq n).symm
723
724/-! ## (C) Decoys -/
725
726/-- DECOY: dynamic `G = 1 + id²` is not the frozen-1 profile. -/
727theorem frozen_structure_differs_from_dynamic_id :
728 dynamicStructureProfile id (1 : ℝ) ≠ (1 : ℝ) := by
729 simp [dynamicStructureProfile]
730
731/-- Explicit continuum-density mismatch at `t = 1` for
732`N ≡ 1`, `M = id`, `p ≡ 1`, `q = id`: dynamic value `2`, frozen value `1`. -/
733theorem frozen_continuum_density_differs_from_dynamic :
734 continuumDiracDensity (fun _ => (1 : ℝ)) id id (fun _ => (1 : ℝ)) (1 : ℝ)
735 ≠
736 ((1 : ℝ) * deriv id (1 : ℝ) - id (1 : ℝ) * deriv (fun _ : ℝ => (1 : ℝ)) (1 : ℝ)) *
737 ((1 : ℝ) * continuumMomentumFlux (fun _ => (1 : ℝ)) id (1 : ℝ)) := by
738 simp [continuumDiracDensity, continuumMomentumFlux, dynamicStructureProfile,
739 deriv_id, deriv_const]
740
741/-! ### Axiom receipts -/
742
743#print axioms discrete_wronskian_mvt
744#print axioms wronskian_rate_h_tendsto
745#print axioms forward_diff_mvt
746#print axioms forward_density_uniform
747#print axioms dynamic_bracket_shape_continuum_limit
748#print axioms frozen_structure_differs_from_dynamic_id
749#print axioms frozen_continuum_density_differs_from_dynamic
750
751end
752end DiracAlgebraContinuum
753end SevenGaps
754end Gravity
755end IndisputableMonolith
756