IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugeUV
IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean · 871 lines · 75 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure
3import IndisputableMonolith.Gravity.SevenGaps.SimplicialClass
4
5/-!
6# Seven Gaps: exact complexity shells and the Gaussian-UV-regularized path sum
7
8## What this module is (and is NOT)
9
10This module organizes the quotient-class path-sum configuration space into
11EXACT complexity shells (no size caps anywhere in the shell definition) and
12proves that the shell-resummed path sum with an explicit Gaussian UV
13regulator `exp(-ρ·n²)` converges for every regulator strength `ρ > 0`.
14
15**HONESTY DISCLOSURES (binding, per the panel-locked protocol):**
16* The regulator `exp(-ρ·n²)` is a MATHEMATICAL regulator inserted by hand;
17 it is NOT derived physics.
18* The action/phase entering the unitary weight is a PARAMETER (an arbitrary
19 function on equivalence classes, equivalently a `GlobalEquivalent`-invariant
20 function on labeled complexes, exactly as in
21 `PathSumMeasure.zRS_scoped_wellDefined`); no physical action is derived.
22* Regulator removal (the `ρ → 0⁺` limit) is a NAMED OPEN
23 (`HasZRSRegulatorRemoval`, status flag `false`); it is NEVER claimed.
24* NOTHING here is the physical continuum limit: the complexity cutoff is
25 not mesh refinement. `path_sum_continuum_limit` and
26 `gap2_continuum_and_measure` stay RED; this module flips NO
27 `FullTheoryLedger` flag.
28
29## Status tiers (honest tagging)
30
31**THEOREM (proved below, 0 sorry, 0 new axioms, no `native_decide`):**
32* Stage 1 (shell structure): `complexity` is relabeling-invariant
33 (`complexity_congr`); the cap-free exact class `ExactComplex v e t` with
34 its independent relabeling equivalence `GlobalEquivalent` is a genuine
35 setoid (`exactSetoid`); the exact complexity shell `ExactPathClass n` is
36 a `Fintype` (`instFintypeExactPathClass`); the shell entropy bound
37 `card (ExactPathClass n) ≤ (n+1)^(12·(n+1))` (`exactPathClass_card_le`);
38 every shell is inhabited (`exactPathClass_unbounded_support`, witness:
39 `n` isolated vertices — NO simpliciality claim).
40* Stage 2 (regularized limit): the per-class measure `classMu = 1/|Aut|`
41 is well-defined on classes (`exactMu_congr`), positive, and at most 1;
42 the regulated shell term satisfies the modulus bound
43 (`norm_zRSUVShell_le`); the shell series is summable for every `ρ > 0`
44 (`summable_zRSUVShell`); the cutoff partial sums converge to `Z_RS_uv`
45 (`zRSUVCutoff_tendsto`); at zero phase the regulated sum is real and
46 strictly positive (`Z_RS_uv_zeroPhase_re_pos`) — non-vacuity.
47
48**MODEL (definitional):** the `1/|Aut|` symmetry-factor measure convention
49(standard discrete-gravity), the shell coordinate
50`complexity = max(nV, max(nE, nT))`, and the Gaussian regulator shape.
51
52**OPEN (named, recorded in `exactShellGaugeUVStatus`, not claimed):**
53* `HasZRSRegulatorRemoval`: existence of `lim_{ρ→0⁺} Z_RS_uv ρ phase`.
54* The physical continuum limit (complexity cutoff ≠ mesh refinement).
55
56## The cross-cap identification problem (Stage 1 rationale)
57
58The scoped class `PathSumMeasure.BoundedComplex B` carries a size cap `B`,
59so the SAME abstract complex appears as an element of `BoundedComplex B`
60for every `B` above its complexity — a cap-dependent double-counting
61hazard for any sum over caps. The exact class `ExactComplex v e t` has NO
62cap fields: a complex determines its signature `(v, e, t)` and hence
63EXACTLY ONE shell index `max v (max e t)` (`shell_index_unique`), and the
64cap-relaxation map of the bounded class collapses (`toExact_relax` is a
65definitional equality), so no configuration is counted in two shells.
66-/
67
68namespace IndisputableMonolith
69namespace Gravity
70namespace SevenGaps
71namespace ExactShellGaugeUV
72
73open PathSumMeasure
74
75/-! ## §1 (S1a). Complexity of a bounded complex is relabeling-invariant -/
76
77/-- The complexity of a bounded complex: the largest of its vertex, edge,
78and tetrahedron counts. This is the shell coordinate. -/
79def complexity {B : ℕ} (K : BoundedComplex B) : ℕ :=
80 max K.nV (max K.nE K.nT)
81
82/-- A relabeling forces equal vertex counts (`Fin` cardinality through the
83vertex bijection). -/
84theorem relabel_nV_eq {B : ℕ} {K K' : BoundedComplex B} (r : Relabel K K') :
85 K.nV = K'.nV := by
86 have h := Fintype.card_congr r.vEquiv
87 simp only [Fintype.card_fin] at h
88 exact h
89
90/-- A relabeling forces equal edge counts. -/
91theorem relabel_nE_eq {B : ℕ} {K K' : BoundedComplex B} (r : Relabel K K') :
92 K.nE = K'.nE := by
93 have h := Fintype.card_congr r.eEquiv
94 simp only [Fintype.card_fin] at h
95 exact h
96
97/-- A relabeling forces equal tetrahedron counts. -/
98theorem relabel_nT_eq {B : ℕ} {K K' : BoundedComplex B} (r : Relabel K K') :
99 K.nT = K'.nT := by
100 have h := Fintype.card_congr r.tEquiv
101 simp only [Fintype.card_fin] at h
102 exact h
103
104/-- **THEOREM (S1a).** Complexity is a relabeling invariant: equivalent
105bounded complexes have equal complexity. -/
106theorem complexity_congr {B : ℕ} {K K' : BoundedComplex B}
107 (h : Equivalent K K') : complexity K = complexity K' := by
108 obtain ⟨r⟩ := h
109 unfold complexity
110 rw [relabel_nV_eq r, relabel_nE_eq r, relabel_nT_eq r]
111
112/-! ## §2 (S1b). The cap-free exact class and its independent equivalence -/
113
114/-- An EXACT-size combinatorial complex: exactly `v` vertices, `e` edges,
115`t` tetrahedra, with abstract incidence data and NO cap inequalities.
116This is the cap-free configuration type; the cross-cap identification
117problem of `BoundedComplex` cannot arise here because there is no cap. -/
118structure ExactComplex (v e t : ℕ) where
119 edgeVerts : Fin e → Fin v × Fin v
120 tetVerts : Fin t → Fin 4 → Fin v
121
122/-- A relabeling isomorphism between two exact complexes of the same
123signature: bijections of the vertex/edge/tet index sets commuting with the
124incidence maps. Defined INDEPENDENTLY of `PathSumMeasure.Relabel` (no
125embedding into any capped class). -/
126structure ExactRelabel {v e t : ℕ} (K K' : ExactComplex v e t) where
127 vEquiv : Fin v ≃ Fin v
128 eEquiv : Fin e ≃ Fin e
129 tEquiv : Fin t ≃ Fin t
130 edge_comm : ∀ i : Fin e,
131 K'.edgeVerts (eEquiv i) = Prod.map vEquiv vEquiv (K.edgeVerts i)
132 tet_comm : ∀ (i : Fin t) (j : Fin 4),
133 K'.tetVerts (tEquiv i) j = vEquiv (K.tetVerts i j)
134
135namespace ExactRelabel
136
137variable {v e t : ℕ}
138
139/-- Identity relabeling. -/
140def refl (K : ExactComplex v e t) : ExactRelabel K K where
141 vEquiv := Equiv.refl _
142 eEquiv := Equiv.refl _
143 tEquiv := Equiv.refl _
144 edge_comm := fun _ => rfl
145 tet_comm := fun _ _ => rfl
146
147/-- Inverse relabeling. -/
148def symm {K K' : ExactComplex v e t} (r : ExactRelabel K K') :
149 ExactRelabel K' K where
150 vEquiv := r.vEquiv.symm
151 eEquiv := r.eEquiv.symm
152 tEquiv := r.tEquiv.symm
153 edge_comm := fun i => by
154 have h := r.edge_comm (r.eEquiv.symm i)
155 rw [Equiv.apply_symm_apply] at h
156 rw [h, Prod.map_map, Equiv.symm_comp_self, Prod.map_id, id_eq]
157 tet_comm := fun i j => by
158 have h := r.tet_comm (r.tEquiv.symm i) j
159 rw [Equiv.apply_symm_apply] at h
160 rw [h, Equiv.symm_apply_apply]
161
162/-- Composite relabeling. -/
163def trans {K₁ K₂ K₃ : ExactComplex v e t} (r : ExactRelabel K₁ K₂)
164 (s : ExactRelabel K₂ K₃) : ExactRelabel K₁ K₃ where
165 vEquiv := r.vEquiv.trans s.vEquiv
166 eEquiv := r.eEquiv.trans s.eEquiv
167 tEquiv := r.tEquiv.trans s.tEquiv
168 edge_comm := fun i => by
169 rw [Equiv.trans_apply, s.edge_comm, r.edge_comm, Prod.map_map,
170 Equiv.coe_trans]
171 tet_comm := fun i j => by
172 rw [Equiv.trans_apply, s.tet_comm, r.tet_comm, Equiv.trans_apply]
173
174@[simp] theorem trans_vEquiv {K₁ K₂ K₃ : ExactComplex v e t}
175 (r : ExactRelabel K₁ K₂) (s : ExactRelabel K₂ K₃) :
176 (r.trans s).vEquiv = r.vEquiv.trans s.vEquiv := rfl
177@[simp] theorem trans_eEquiv {K₁ K₂ K₃ : ExactComplex v e t}
178 (r : ExactRelabel K₁ K₂) (s : ExactRelabel K₂ K₃) :
179 (r.trans s).eEquiv = r.eEquiv.trans s.eEquiv := rfl
180@[simp] theorem trans_tEquiv {K₁ K₂ K₃ : ExactComplex v e t}
181 (r : ExactRelabel K₁ K₂) (s : ExactRelabel K₂ K₃) :
182 (r.trans s).tEquiv = r.tEquiv.trans s.tEquiv := rfl
183@[simp] theorem symm_vEquiv {K K' : ExactComplex v e t}
184 (r : ExactRelabel K K') : r.symm.vEquiv = r.vEquiv.symm := rfl
185@[simp] theorem symm_eEquiv {K K' : ExactComplex v e t}
186 (r : ExactRelabel K K') : r.symm.eEquiv = r.eEquiv.symm := rfl
187@[simp] theorem symm_tEquiv {K K' : ExactComplex v e t}
188 (r : ExactRelabel K K') : r.symm.tEquiv = r.tEquiv.symm := rfl
189
190/-- Forget the commutation proofs: the underlying triple of index
191bijections. -/
192def toEquivTriple {K K' : ExactComplex v e t} (r : ExactRelabel K K') :
193 (Fin v ≃ Fin v) × (Fin e ≃ Fin e) × (Fin t ≃ Fin t) :=
194 (r.vEquiv, r.eEquiv, r.tEquiv)
195
196/-- A relabeling is determined by its index bijections (the commutation
197fields are propositions). -/
198theorem toEquivTriple_injective {K K' : ExactComplex v e t} :
199 Function.Injective (toEquivTriple (K := K) (K' := K')) := by
200 rintro ⟨v₁, e₁, t₁, p₁, q₁⟩ ⟨v₂, e₂, t₂, p₂, q₂⟩ h
201 simp only [toEquivTriple, Prod.mk.injEq] at h
202 obtain ⟨h1, h2, h3⟩ := h
203 subst h1
204 subst h2
205 subst h3
206 rfl
207
208/-- Extensionality for exact relabelings. -/
209theorem ext {K K' : ExactComplex v e t} {r s : ExactRelabel K K'}
210 (hv : r.vEquiv = s.vEquiv) (he : r.eEquiv = s.eEquiv)
211 (ht : r.tEquiv = s.tEquiv) : r = s := by
212 apply toEquivTriple_injective
213 unfold toEquivTriple
214 rw [hv, he, ht]
215
216end ExactRelabel
217
218/-- Two exact complexes of the same signature are GLOBALLY EQUIVALENT iff
219an exact relabeling exists between them. (A relabeling between different
220signatures is impossible: `vEquiv : Fin v ≃ Fin v'` forces `v = v'` by
221cardinality, so the equivalence lives on each `(v, e, t)` piece.) -/
222def GlobalEquivalent {v e t : ℕ} (K K' : ExactComplex v e t) : Prop :=
223 Nonempty (ExactRelabel K K')
224
225/-- **THEOREM.** Global equivalence is a genuine setoid on each exact
226signature (refl/symm/trans via the explicit relabelings above). -/
227def exactSetoid (v e t : ℕ) : Setoid (ExactComplex v e t) where
228 r := GlobalEquivalent
229 iseqv :=
230 ⟨fun K => ⟨ExactRelabel.refl K⟩,
231 fun h => h.elim fun r => ⟨r.symm⟩,
232 fun h₁ h₂ => h₁.elim fun r => h₂.elim fun s => ⟨r.trans s⟩⟩
233
234/-! ### Finiteness of the exact labeled class -/
235
236/-- Finite code type for `ExactComplex v e t`: the raw incidence data. -/
237def exactCodeEquiv (v e t : ℕ) :
238 ExactComplex v e t ≃
239 ((Fin e → Fin v × Fin v) × (Fin t → Fin 4 → Fin v)) where
240 toFun K := (K.edgeVerts, K.tetVerts)
241 invFun c := ⟨c.1, c.2⟩
242 left_inv _ := rfl
243 right_inv _ := rfl
244
245/-- The exact labeled class at any fixed signature is a finite type. -/
246instance instFintypeExactComplex (v e t : ℕ) : Fintype (ExactComplex v e t) :=
247 Fintype.ofEquiv _ (exactCodeEquiv v e t).symm
248
249/-- The labeled count at signature `(v, e, t)`: `(v·v)^e · (v⁴)^t`
250labelings (one vertex pair per edge, one 4-tuple of vertices per tet). -/
251theorem exactComplex_card_eq (v e t : ℕ) :
252 Fintype.card (ExactComplex v e t) = (v * v) ^ e * (v ^ 4) ^ t := by
253 rw [Fintype.card_congr (exactCodeEquiv v e t)]
254 simp only [Fintype.card_prod, Fintype.card_fun, Fintype.card_fin]
255
256/-- **Labeled entropy bound.** If all three counts are at most `n + 1`,
257the labeled count is at most `(n+1)^(6·(n+1))` (documented counting: at
258most `((n+1)²)^e` edge labelings times `((n+1)⁴)^t` tet labelings, with
259`e, t ≤ n + 1`). -/
260theorem exactComplex_card_le (n v e t : ℕ) (hv : v ≤ n + 1)
261 (he : e ≤ n + 1) (ht : t ≤ n + 1) :
262 Fintype.card (ExactComplex v e t) ≤ (n + 1) ^ (6 * (n + 1)) := by
263 rw [exactComplex_card_eq]
264 have h1 : (v * v) ^ e ≤ (n + 1) ^ (2 * (n + 1)) := by
265 calc (v * v) ^ e
266 ≤ ((n + 1) * (n + 1)) ^ e :=
267 Nat.pow_le_pow_left (Nat.mul_le_mul hv hv) e
268 _ = (n + 1) ^ (2 * e) := by rw [← pow_two, ← pow_mul]
269 _ ≤ (n + 1) ^ (2 * (n + 1)) :=
270 Nat.pow_le_pow_right (Nat.succ_pos n) (by omega)
271 have h2 : (v ^ 4) ^ t ≤ (n + 1) ^ (4 * (n + 1)) := by
272 calc (v ^ 4) ^ t
273 ≤ ((n + 1) ^ 4) ^ t :=
274 Nat.pow_le_pow_left (Nat.pow_le_pow_left hv 4) t
275 _ = (n + 1) ^ (4 * t) := by rw [← pow_mul]
276 _ ≤ (n + 1) ^ (4 * (n + 1)) :=
277 Nat.pow_le_pow_right (Nat.succ_pos n) (by omega)
278 calc (v * v) ^ e * (v ^ 4) ^ t
279 ≤ (n + 1) ^ (2 * (n + 1)) * (n + 1) ^ (4 * (n + 1)) :=
280 Nat.mul_le_mul h1 h2
281 _ = (n + 1) ^ (6 * (n + 1)) := by
282 rw [← pow_add]
283 congr 1
284 omega
285
286/-! ### The exact complexity shell -/
287
288/-- A shell signature at level `n`: a triple `(v, e, t)` with each count
289at most `n` and `max v (max e t) = n`. Packaged in `Fin (n+1)` so the
290signature type is finite. -/
291abbrev ShellSig (n : ℕ) : Type :=
292 { s : Fin (n + 1) × Fin (n + 1) × Fin (n + 1) //
293 max (s.1 : ℕ) (max (s.2.1 : ℕ) (s.2.2 : ℕ)) = n }
294
295/-- Vertex count of a shell signature. -/
296abbrev sigV {n : ℕ} (s : ShellSig n) : ℕ := (s.1.1 : ℕ)
297/-- Edge count of a shell signature. -/
298abbrev sigE {n : ℕ} (s : ShellSig n) : ℕ := (s.1.2.1 : ℕ)
299/-- Tetrahedron count of a shell signature. -/
300abbrev sigT {n : ℕ} (s : ShellSig n) : ℕ := (s.1.2.2 : ℕ)
301
302/-- The number of shell signatures at level `n` is at most `(n+1)³`. -/
303theorem shellSig_card_le (n : ℕ) :
304 Fintype.card (ShellSig n) ≤ (n + 1) ^ 3 := by
305 have h := Fintype.card_subtype_le
306 (fun s : Fin (n + 1) × Fin (n + 1) × Fin (n + 1) =>
307 max (s.1 : ℕ) (max (s.2.1 : ℕ) (s.2.2 : ℕ)) = n)
308 calc Fintype.card (ShellSig n)
309 ≤ Fintype.card (Fin (n + 1) × Fin (n + 1) × Fin (n + 1)) := h
310 _ = (n + 1) ^ 3 := by
311 simp only [Fintype.card_prod, Fintype.card_fin]
312 ring
313
314/-- **THE EXACT COMPLEXITY SHELL (S1b).** The set of combinatorially
315distinct exact complexes of complexity exactly `n`: the disjoint union
316over shell signatures of the quotient of the exact labeled class by
317global equivalence. NO cap type (`BoundedComplex B`) appears anywhere in
318this definition. -/
319abbrev ExactPathClass (n : ℕ) : Type :=
320 Σ s : ShellSig n, Quotient (exactSetoid (sigV s) (sigE s) (sigT s))
321
322instance instFiniteExactQuotient (v e t : ℕ) :
323 Finite (Quotient (exactSetoid v e t)) :=
324 Quotient.finite _
325
326/-- **THEOREM (S1b).** Each exact complexity shell is a finite type. -/
327noncomputable instance instFintypeExactPathClass (n : ℕ) :
328 Fintype (ExactPathClass n) :=
329 Fintype.ofFinite _
330
331/-! ### No cross-shell double counting -/
332
333/-- The complexity of an exact complex: determined by its signature alone. -/
334def exactComplexity {v e t : ℕ} (_ : ExactComplex v e t) : ℕ :=
335 max v (max e t)
336
337/-- **THEOREM (no double counting).** An exact complex can sit in the
338shell at level `n` (i.e. its signature can be a `ShellSig n`) ONLY for
339`n = exactComplexity K`: each configuration has exactly one shell.
340Combined with the fact that `GlobalEquivalent` lives on a fixed signature,
341no abstract complex is counted in two shells. -/
342theorem shell_index_unique {v e t : ℕ} (K : ExactComplex v e t) {n : ℕ}
343 (s : ShellSig n) (hv : sigV s = v) (he : sigE s = e) (ht : sigT s = t) :
344 n = exactComplexity K := by
345 unfold exactComplexity
346 rw [← hv, ← he, ← ht]
347 exact s.2.symm
348
349/-- Forget the cap: every bounded complex yields an exact complex with the
350same incidence data. The TARGET TYPE does not mention the cap `B`. -/
351def toExact {B : ℕ} (K : BoundedComplex B) : ExactComplex K.nV K.nE K.nT where
352 edgeVerts := K.edgeVerts
353 tetVerts := K.tetVerts
354
355/-- **THEOREM (cap-dependence collapses).** Relaxing the cap of a bounded
356complex does not change its exact image: the map to the cap-free class
357identifies all capped copies of the same configuration (definitional
358equality). -/
359theorem toExact_relax {B B' : ℕ} (h : B ≤ B') (K : BoundedComplex B) :
360 toExact (PathSumMeasure.relax h K) = toExact K := rfl
361
362/-- The exact complexity of the image agrees with the capped complexity. -/
363theorem toExact_complexity {B : ℕ} (K : BoundedComplex B) :
364 exactComplexity (toExact K) = complexity K := rfl
365
366/-! ## §3 (S1c). The shell entropy bound -/
367
368/-- **THEOREM (shell entropy bound, S1c).** The number of combinatorially
369distinct exact complexes of complexity `n` is at most `(n+1)^(12·(n+1))`.
370Counting audit: `≤ (n+1)³` signature choices (`shellSig_card_le`), times
371`≤ (n+1)^(6·(n+1))` labeled configurations per signature
372(`exactComplex_card_le`, quotient card ≤ labeled card via the surjection
373`Quotient.mk`), and `3 + 6·(n+1) ≤ 12·(n+1)`. -/
374theorem exactPathClass_card_le (n : ℕ) :
375 Nat.card (ExactPathClass n) ≤ (n + 1) ^ (12 * (n + 1)) := by
376 have hfiber : ∀ s : ShellSig n,
377 Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤
378 (n + 1) ^ (6 * (n + 1)) := by
379 intro s
380 have hsurj : Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤
381 Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) :=
382 Nat.card_le_card_of_surjective
383 (Quotient.mk (exactSetoid (sigV s) (sigE s) (sigT s)))
384 (fun q => Quotient.exists_rep q)
385 have hlab : Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) ≤
386 (n + 1) ^ (6 * (n + 1)) := by
387 rw [Nat.card_eq_fintype_card]
388 exact exactComplex_card_le n _ _ _ (le_of_lt s.1.1.isLt)
389 (le_of_lt s.1.2.1.isLt) (le_of_lt s.1.2.2.isLt)
390 exact le_trans hsurj hlab
391 rw [Nat.card_sigma]
392 calc ∑ s : ShellSig n,
393 Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s)))
394 ≤ ∑ _s : ShellSig n, (n + 1) ^ (6 * (n + 1)) :=
395 Finset.sum_le_sum fun s _ => hfiber s
396 _ = Fintype.card (ShellSig n) * (n + 1) ^ (6 * (n + 1)) := by
397 rw [Finset.sum_const, Finset.card_univ, smul_eq_mul]
398 _ ≤ (n + 1) ^ 3 * (n + 1) ^ (6 * (n + 1)) :=
399 Nat.mul_le_mul_right _ (shellSig_card_le n)
400 _ = (n + 1) ^ (3 + 6 * (n + 1)) := by rw [← pow_add]
401 _ ≤ (n + 1) ^ (12 * (n + 1)) :=
402 Nat.pow_le_pow_right (Nat.succ_pos n) (by omega)
403
404/-! ## §4 (S1d). Every shell is inhabited -/
405
406/-- The `n`-isolated-vertices complex: `n` vertices, no edges, no
407tetrahedra. Complexity exactly `n`. NO simpliciality claim is made or
408needed. -/
409def isolatedVertices (n : ℕ) : ExactComplex n 0 0 where
410 edgeVerts := fun i => i.elim0
411 tetVerts := fun i => i.elim0
412
413/-- The signature `(n, 0, 0)` is a shell signature at level `n`. -/
414def isolatedSig (n : ℕ) : ShellSig n :=
415 ⟨(⟨n, Nat.lt_succ_self n⟩, ⟨0, Nat.succ_pos n⟩, ⟨0, Nat.succ_pos n⟩), by
416 show max n (max 0 0) = n
417 rw [max_self, Nat.max_zero]⟩
418
419/-- The class of the `n`-isolated-vertices complex in the shell at level
420`n`. -/
421def isolatedClass (n : ℕ) : ExactPathClass n :=
422 ⟨isolatedSig n, Quotient.mk _ (isolatedVertices n)⟩
423
424instance instNonemptyExactPathClass (n : ℕ) : Nonempty (ExactPathClass n) :=
425 ⟨isolatedClass n⟩
426
427/-- **THEOREM (S1d, unbounded support).** EVERY shell is inhabited: the
428`n`-isolated-vertices complex has complexity exactly `n`, so no shell is
429eventually empty. -/
430theorem exactPathClass_unbounded_support (n : ℕ) :
431 0 < Nat.card (ExactPathClass n) :=
432 Nat.card_pos
433
434/-! ## §5 (S2a). The per-class measure `1/|Aut|` on exact classes -/
435
436/-- The automorphism group of an exact labeled complex: exact relabelings
437of `K` onto itself. -/
438abbrev ExactAut {v e t : ℕ} (K : ExactComplex v e t) := ExactRelabel K K
439
440instance {v e t : ℕ} (K : ExactComplex v e t) : Nonempty (ExactAut K) :=
441 ⟨ExactRelabel.refl K⟩
442
443/-- The automorphism group is finite (inject into the finite triple of
444index permutations). -/
445instance instFiniteExactAut {v e t : ℕ} (K : ExactComplex v e t) :
446 Finite (ExactAut K) :=
447 Finite.of_injective _
448 (ExactRelabel.toEquivTriple_injective (K := K) (K' := K))
449
450/-- The automorphism count is positive (the identity is an automorphism). -/
451theorem exactAutCard_pos {v e t : ℕ} (K : ExactComplex v e t) :
452 0 < Nat.card (ExactAut K) :=
453 Nat.card_pos
454
455/-- The symmetry-factor measure of an exact labeled complex:
456`μ(K) = 1/|Aut K|` (MODEL: the standard discrete-gravity convention). -/
457noncomputable def exactMu {v e t : ℕ} (K : ExactComplex v e t) : ℝ :=
458 1 / (Nat.card (ExactAut K) : ℝ)
459
460/-- **THEOREM.** `0 < μ(K)`. -/
461theorem exactMu_pos {v e t : ℕ} (K : ExactComplex v e t) : 0 < exactMu K := by
462 unfold exactMu
463 have h : (0 : ℝ) < (Nat.card (ExactAut K) : ℝ) := by
464 exact_mod_cast exactAutCard_pos K
465 exact div_pos one_pos h
466
467/-- **THEOREM.** `μ(K) ≤ 1` (since `|Aut K| ≥ 1`). -/
468theorem exactMu_le_one {v e t : ℕ} (K : ExactComplex v e t) :
469 exactMu K ≤ 1 := by
470 unfold exactMu
471 have h : (0 : ℝ) < (Nat.card (ExactAut K) : ℝ) := by
472 exact_mod_cast exactAutCard_pos K
473 rw [div_le_one h]
474 exact_mod_cast exactAutCard_pos K
475
476/-- Conjugation by an exact relabeling: automorphism groups of globally
477equivalent complexes are in bijection (mirrors
478`PathSumMeasure.Relabel.autCongr`). -/
479def ExactRelabel.autCongr {v e t : ℕ} {K K' : ExactComplex v e t}
480 (r : ExactRelabel K K') : ExactAut K ≃ ExactAut K' where
481 toFun a := (r.symm.trans a).trans r
482 invFun b := (r.trans b).trans r.symm
483 left_inv a := by
484 apply ExactRelabel.ext <;>
485 · apply Equiv.ext
486 intro x
487 simp only [ExactRelabel.trans_vEquiv, ExactRelabel.trans_eEquiv,
488 ExactRelabel.trans_tEquiv, ExactRelabel.symm_vEquiv,
489 ExactRelabel.symm_eEquiv, ExactRelabel.symm_tEquiv,
490 Equiv.trans_apply, Equiv.symm_apply_apply]
491 right_inv b := by
492 apply ExactRelabel.ext <;>
493 · apply Equiv.ext
494 intro x
495 simp only [ExactRelabel.trans_vEquiv, ExactRelabel.trans_eEquiv,
496 ExactRelabel.trans_tEquiv, ExactRelabel.symm_vEquiv,
497 ExactRelabel.symm_eEquiv, ExactRelabel.symm_tEquiv,
498 Equiv.trans_apply, Equiv.apply_symm_apply]
499
500/-- **THEOREM (S2a, class invariance).** `μ` is a global-equivalence
501invariant (mirrors `PathSumMeasure.mu_congr`). -/
502theorem exactMu_congr {v e t : ℕ} {K K' : ExactComplex v e t}
503 (h : GlobalEquivalent K K') : exactMu K = exactMu K' := by
504 obtain ⟨r⟩ := h
505 unfold exactMu
506 rw [Nat.card_congr r.autCongr]
507
508/-- The measure descends to the quotient: the per-class measure. -/
509noncomputable def classMuOn (v e t : ℕ) :
510 Quotient (exactSetoid v e t) → ℝ :=
511 Quotient.lift exactMu (fun _ _ h => exactMu_congr h)
512
513/-- The per-class measure on a shell element. -/
514noncomputable def classMu {n : ℕ} (c : ExactPathClass n) : ℝ :=
515 classMuOn (sigV c.1) (sigE c.1) (sigT c.1) c.2
516
517/-- **THEOREM.** `0 < classMu c` for every class. -/
518theorem classMu_pos {n : ℕ} (c : ExactPathClass n) : 0 < classMu c := by
519 obtain ⟨s, q⟩ := c
520 exact Quotient.inductionOn q (fun K => exactMu_pos K)
521
522/-- **THEOREM.** `classMu c ≤ 1` for every class. -/
523theorem classMu_le_one {n : ℕ} (c : ExactPathClass n) : classMu c ≤ 1 := by
524 obtain ⟨s, q⟩ := c
525 exact Quotient.inductionOn q (fun K => exactMu_le_one K)
526
527/-- A `GlobalEquivalent`-invariant labeled action descends to a class
528function: the honest way a phase parameter enters (mirrors the `hS`
529hypothesis of `PathSumMeasure.zRS_scoped_wellDefined`). The phase used
530below is an arbitrary function on classes, i.e. exactly such a lift. -/
531noncomputable def liftedPhase
532 (S : ∀ v e t : ℕ, ExactComplex v e t → ℝ)
533 (hS : ∀ (v e t : ℕ) (K K' : ExactComplex v e t),
534 GlobalEquivalent K K' → S v e t K = S v e t K') :
535 ∀ n : ℕ, ExactPathClass n → ℝ :=
536 fun _ c => Quotient.lift (S _ _ _) (fun _ _ h => hS _ _ _ _ _ h) c.2
537
538/-! ## §6 (S2b). The regulated shell term and its modulus bound -/
539
540/-- **The Gaussian-regulated shell term (S2b).** At shell level `n`, the
541per-class-weighted unitary sum with the explicit UV regulator
542`exp(-ρ·n²)`. DISCLOSURE: the regulator is mathematical, not derived
543physics; `phase` is a parameter (an arbitrary invariant action on
544classes), not derived physics. -/
545noncomputable def zRSUVShell (ρ : ℝ) (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
546 (n : ℕ) : ℂ :=
547 (Real.exp (-ρ * (n : ℝ) ^ 2) : ℝ) *
548 ∑ c : ExactPathClass n,
549 (classMu c : ℂ) * Complex.exp (Complex.I * (phase n c : ℂ))
550
551/-- **THEOREM (S2b, modulus bound).** The regulated shell term is bounded
552by the regulator times the shell cardinality (`μ ≤ 1`, unit phases). -/
553theorem norm_zRSUVShell_le (ρ : ℝ) (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
554 (n : ℕ) :
555 ‖zRSUVShell ρ phase n‖ ≤
556 Real.exp (-ρ * (n : ℝ) ^ 2) * (Nat.card (ExactPathClass n) : ℝ) := by
557 unfold zRSUVShell
558 rw [norm_mul, Complex.norm_real, Real.norm_eq_abs,
559 abs_of_pos (Real.exp_pos _)]
560 refine mul_le_mul_of_nonneg_left ?_ (Real.exp_pos _).le
561 calc ‖∑ c : ExactPathClass n,
562 (classMu c : ℂ) * Complex.exp (Complex.I * (phase n c : ℂ))‖
563 ≤ ∑ c : ExactPathClass n,
564 ‖(classMu c : ℂ) * Complex.exp (Complex.I * (phase n c : ℂ))‖ :=
565 norm_sum_le _ _
566 _ ≤ ∑ _c : ExactPathClass n, (1 : ℝ) := by
567 refine Finset.sum_le_sum fun c _ => ?_
568 rw [norm_mul, Complex.norm_real, Real.norm_eq_abs,
569 abs_of_pos (classMu_pos c), Complex.norm_exp_I_mul_ofReal, mul_one]
570 exact classMu_le_one c
571 _ = (Fintype.card (ExactPathClass n) : ℝ) := by
572 rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one]
573 _ = (Nat.card (ExactPathClass n) : ℝ) := by
574 rw [Nat.card_eq_fintype_card]
575
576/-- **THEOREM (S2b + S1c composed).** The regulated shell term is bounded
577by the regulator times the proved entropy bound. -/
578theorem norm_zRSUVShell_le_entropy (ρ : ℝ)
579 (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (n : ℕ) :
580 ‖zRSUVShell ρ phase n‖ ≤
581 Real.exp (-ρ * (n : ℝ) ^ 2) * ((n : ℝ) + 1) ^ (12 * (n + 1)) := by
582 refine le_trans (norm_zRSUVShell_le ρ phase n) ?_
583 refine mul_le_mul_of_nonneg_left ?_ (Real.exp_pos _).le
584 have h := exactPathClass_card_le n
585 have hcast : ((Nat.card (ExactPathClass n) : ℕ) : ℝ) ≤
586 (((n + 1) ^ (12 * (n + 1)) : ℕ) : ℝ) := by exact_mod_cast h
587 push_cast at hcast
588 exact hcast
589
590/-! ## §7 (S2c). Summability of the regulated shell series -/
591
592/-- Linear domination of the logarithm with arbitrary slope: for `δ > 0`
593and `x ≥ 1`, `log x ≤ δ·x + (-1 - log δ)`. (Apply `log y ≤ y - 1` at
594`y = δ·x`.) This is the sublinearity input that makes `n·log n = o(n²)`
595quantitative. -/
596theorem log_le_linear {δ : ℝ} (hδ : 0 < δ) {x : ℝ} (hx : 1 ≤ x) :
597 Real.log x ≤ δ * x + (-1 - Real.log δ) := by
598 have hx0 : (0 : ℝ) < x := lt_of_lt_of_le one_pos hx
599 have h1 : Real.log (δ * x) ≤ δ * x - 1 :=
600 Real.log_le_sub_one_of_pos (mul_pos hδ hx0)
601 have h2 : Real.log (δ * x) = Real.log δ + Real.log x :=
602 Real.log_mul (ne_of_gt hδ) (ne_of_gt hx0)
603 linarith
604
605/-- **Eventual Gaussian domination.** For every `ρ > 0` there is a
606threshold `N` beyond which the entropy exponent `12·(n+1)·log(n+1)` is at
607most half the Gaussian exponent `ρ·n²`. -/
608theorem exists_gaussian_domination (ρ : ℝ) (hρ : 0 < ρ) :
609 ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
610 12 * ((n : ℝ) + 1) * Real.log ((n : ℝ) + 1) ≤ ρ / 2 * (n : ℝ) ^ 2 := by
611 set δ : ℝ := ρ / 192 with hδdef
612 have hδ : 0 < δ := by positivity
613 set C : ℝ := |(-1 : ℝ) - Real.log δ| with hCdef
614 have hC0 : (0 : ℝ) ≤ C := abs_nonneg _
615 obtain ⟨N₀, hN₀⟩ := exists_nat_ge (96 * C / ρ)
616 refine ⟨max 1 N₀, fun n hn => ?_⟩
617 have hn1 : 1 ≤ n := le_trans (le_max_left 1 N₀) hn
618 have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn1
619 have hnN₀ : 96 * C / ρ ≤ (n : ℝ) := by
620 have h : (N₀ : ℝ) ≤ (n : ℝ) := by
621 exact_mod_cast le_trans (le_max_right 1 N₀) hn
622 linarith
623 set x : ℝ := (n : ℝ) + 1 with hxdef
624 have hx1 : (1 : ℝ) ≤ x := by simp only [hxdef]; linarith
625 have hx0 : (0 : ℝ) < x := lt_of_lt_of_le one_pos hx1
626 have hx2n : x ≤ 2 * (n : ℝ) := by simp only [hxdef]; linarith
627 have hlx : Real.log x ≤ δ * x + C := by
628 have h := log_le_linear hδ hx1
629 have habs : (-1 : ℝ) - Real.log δ ≤ C := le_abs_self _
630 linarith
631 have hmul : 12 * x * Real.log x ≤ 12 * x * (δ * x + C) := by
632 apply mul_le_mul_of_nonneg_left hlx
633 positivity
634 have hring : 12 * x * (δ * x + C) = 12 * δ * x ^ 2 + 12 * C * x := by ring
635 have hxsq : x ^ 2 ≤ 4 * (n : ℝ) ^ 2 := by
636 have h := pow_le_pow_left₀ hx0.le hx2n 2
637 calc x ^ 2 ≤ (2 * (n : ℝ)) ^ 2 := h
638 _ = 4 * (n : ℝ) ^ 2 := by ring
639 have h1 : 12 * δ * x ^ 2 ≤ ρ / 4 * (n : ℝ) ^ 2 := by
640 have hcoef : 12 * δ = ρ / 16 := by rw [hδdef]; ring
641 rw [hcoef]
642 calc ρ / 16 * x ^ 2 ≤ ρ / 16 * (4 * (n : ℝ) ^ 2) := by
643 apply mul_le_mul_of_nonneg_left hxsq
644 positivity
645 _ = ρ / 4 * (n : ℝ) ^ 2 := by ring
646 have h2 : 12 * C * x ≤ ρ / 4 * (n : ℝ) ^ 2 := by
647 have ha : 12 * C * x ≤ 24 * C * (n : ℝ) := by
648 calc 12 * C * x ≤ 12 * C * (2 * (n : ℝ)) := by
649 apply mul_le_mul_of_nonneg_left hx2n
650 positivity
651 _ = 24 * C * (n : ℝ) := by ring
652 have hρn : 96 * C ≤ ρ * (n : ℝ) := by
653 have h := (div_le_iff₀ hρ).mp hnN₀
654 linarith
655 have hb : 24 * C * (n : ℝ) ≤ ρ / 4 * (n : ℝ) ^ 2 := by
656 nlinarith [mul_nonneg (sub_nonneg.mpr hρn)
657 (le_trans zero_le_one hnR)]
658 linarith
659 linarith
660
661/-- Convert a natural power of `(n+1)` into an exponential of its
662logarithm. -/
663theorem pow_eq_exp_log (n k : ℕ) :
664 ((n : ℝ) + 1) ^ k = Real.exp ((k : ℝ) * Real.log ((n : ℝ) + 1)) := by
665 have hpos : (0 : ℝ) < (n : ℝ) + 1 := by positivity
666 rw [← Real.log_pow, Real.exp_log (pow_pos hpos k)]
667
668/-- **THEOREM (S2c, UV summability).** For every regulator strength
669`ρ > 0` and every phase parameter, the regulated shell series is
670summable. Proof: eventual comparison of
671`exp(-ρn²)·(n+1)^(12(n+1))` with the geometric series `exp(-ρ/2)^n`,
672using `exists_gaussian_domination` (entropy exponent grows like
673`n·log n = o(n²)`). -/
674theorem summable_zRSUVShell (ρ : ℝ) (hρ : 0 < ρ)
675 (phase : ∀ n : ℕ, ExactPathClass n → ℝ) :
676 Summable (fun n => zRSUVShell ρ phase n) := by
677 have hr0 : (0 : ℝ) ≤ Real.exp (-(ρ / 2)) := (Real.exp_pos _).le
678 have hr1 : Real.exp (-(ρ / 2)) < 1 :=
679 Real.exp_lt_one_iff.mpr (by linarith)
680 have hgeo : Summable (fun n : ℕ => Real.exp (-(ρ / 2)) ^ n) :=
681 summable_geometric_of_lt_one hr0 hr1
682 refine Summable.of_norm_bounded_eventually_nat hgeo ?_
683 obtain ⟨N, hN⟩ := exists_gaussian_domination ρ hρ
684 rw [Filter.eventually_atTop]
685 refine ⟨max 1 N, fun n hn => ?_⟩
686 have hn1 : 1 ≤ n := le_trans (le_max_left 1 N) hn
687 have hnN : N ≤ n := le_trans (le_max_right 1 N) hn
688 have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn1
689 have h3 : Real.exp (-ρ * (n : ℝ) ^ 2) * ((n : ℝ) + 1) ^ (12 * (n + 1)) ≤
690 Real.exp (-(ρ / 2) * (n : ℝ) ^ 2) := by
691 rw [pow_eq_exp_log n (12 * (n + 1)), ← Real.exp_add]
692 apply Real.exp_le_exp.mpr
693 have hlog := hN n hnN
694 have hcast : ((12 * (n + 1) : ℕ) : ℝ) = 12 * ((n : ℝ) + 1) := by
695 push_cast
696 ring
697 rw [hcast]
698 linarith
699 have h4 : Real.exp (-(ρ / 2) * (n : ℝ) ^ 2) ≤ Real.exp (-(ρ / 2)) ^ n := by
700 rw [← Real.exp_nat_mul]
701 apply Real.exp_le_exp.mpr
702 have hsq : (n : ℝ) ≤ (n : ℝ) ^ 2 := by nlinarith [hnR]
703 have h := mul_le_mul_of_nonneg_left hsq
704 (by positivity : (0 : ℝ) ≤ ρ / 2)
705 linarith
706 calc ‖zRSUVShell ρ phase n‖
707 ≤ Real.exp (-ρ * (n : ℝ) ^ 2) * ((n : ℝ) + 1) ^ (12 * (n + 1)) :=
708 norm_zRSUVShell_le_entropy ρ phase n
709 _ ≤ Real.exp (-(ρ / 2) * (n : ℝ) ^ 2) := h3
710 _ ≤ Real.exp (-(ρ / 2)) ^ n := h4
711
712/-! ## §8 (S2d). The regulated path sum and the cutoff limit -/
713
714/-- **The Gaussian-UV-regularized recognition path sum (S2d).** The full
715shell series at regulator strength `ρ`. Well-defined as a `tsum`; for
716`ρ > 0` the series is summable (`summable_zRSUVShell`), so this is the
717genuine limit of the cutoff partial sums (`zRSUVCutoff_tendsto`). -/
718noncomputable def Z_RS_uv (ρ : ℝ) (phase : ∀ n : ℕ, ExactPathClass n → ℝ) :
719 ℂ :=
720 ∑' n : ℕ, zRSUVShell ρ phase n
721
722/-- **THEOREM (S2d, cutoff convergence).** The complexity-cutoff partial
723sums converge to the regulated path sum. -/
724theorem zRSUVCutoff_tendsto (ρ : ℝ) (hρ : 0 < ρ)
725 (phase : ∀ n : ℕ, ExactPathClass n → ℝ) :
726 Filter.Tendsto
727 (fun M : ℕ => ∑ n ∈ Finset.range M, zRSUVShell ρ phase n)
728 Filter.atTop (nhds (Z_RS_uv ρ phase)) :=
729 (summable_zRSUVShell ρ hρ phase).hasSum.tendsto_sum_nat
730
731/-! ## §9 (S2e). Non-vacuity at zero phase -/
732
733/-- The zero phase: `S ≡ 0` on every class. -/
734def zeroPhase : ∀ n : ℕ, ExactPathClass n → ℝ := fun _ _ => 0
735
736/-- The total measure of a shell: the sum of the per-class measures. -/
737noncomputable def shellMass (n : ℕ) : ℝ :=
738 ∑ c : ExactPathClass n, classMu c
739
740/-- **THEOREM.** Every shell carries strictly positive measure (the shell
741is inhabited by `isolatedClass n` and each class has `μ > 0`). -/
742theorem shellMass_pos (n : ℕ) : 0 < shellMass n :=
743 Finset.sum_pos (fun c _ => classMu_pos c) Finset.univ_nonempty
744
745/-- At zero phase the shell term is the real number
746`exp(-ρn²) · shellMass n`. -/
747theorem zRSUVShell_zeroPhase_eq (ρ : ℝ) (n : ℕ) :
748 zRSUVShell ρ zeroPhase n =
749 ((Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ) := by
750 unfold zRSUVShell zeroPhase shellMass
751 rw [Complex.ofReal_mul, Complex.ofReal_sum]
752 congr 1
753 refine Finset.sum_congr rfl fun c _ => ?_
754 rw [Complex.ofReal_zero, mul_zero, Complex.exp_zero, mul_one]
755
756/-- **THEOREM.** At zero phase every shell term has strictly positive
757real part (in particular the explicitly constructed inhabited shell
758does). -/
759theorem zRSUVShell_zeroPhase_re_pos (ρ : ℝ) (n : ℕ) :
760 0 < (zRSUVShell ρ zeroPhase n).re := by
761 rw [zRSUVShell_zeroPhase_eq, Complex.ofReal_re]
762 exact mul_pos (Real.exp_pos _) (shellMass_pos n)
763
764/-- **THEOREM (S2e, non-vacuity).** At zero phase the regulated path sum
765has strictly positive real part for every `ρ > 0`: the regulated theory
766is not the zero functional. (All terms are nonnegative real and the
767`n = 0` term is positive; positivity passes to the `tsum`.) -/
768theorem Z_RS_uv_zeroPhase_re_pos (ρ : ℝ) (hρ : 0 < ρ) :
769 0 < (Z_RS_uv ρ zeroPhase).re := by
770 have hsC : Summable
771 (fun n : ℕ => ((Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ)) :=
772 (summable_zRSUVShell ρ hρ zeroPhase).congr
773 (fun n => zRSUVShell_zeroPhase_eq ρ n)
774 have hsR : Summable
775 (fun n : ℕ => Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n) :=
776 Complex.summable_ofReal.mp hsC
777 have hZ : Z_RS_uv ρ zeroPhase =
778 ((∑' n : ℕ, Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ) := by
779 unfold Z_RS_uv
780 rw [tsum_congr (fun n => zRSUVShell_zeroPhase_eq ρ n),
781 ← Complex.ofReal_tsum]
782 rw [hZ, Complex.ofReal_re]
783 exact hsR.tsum_pos
784 (fun n => (mul_pos (Real.exp_pos _) (shellMass_pos n)).le) 0
785 (mul_pos (Real.exp_pos _) (shellMass_pos 0))
786
787/-! ## §10 (S2f). Regulator removal: the NAMED OPEN -/
788
789/-- **NAMED OPEN (S2f, never claimed).** Regulator removal for the
790Gaussian-UV-regularized path sum: existence of the limit of
791`Z_RS_uv ρ phase` as `ρ → 0⁺` (along `nhdsWithin 0 (Ioi 0)`). This is a
792DEFINITION ONLY; no theorem below asserts it, and
793`exactShellGaugeUVStatus.regulator_removal_proved = false` records it as
794OPEN. Even if it were proved, it would NOT be the physical continuum
795limit (complexity cutoff ≠ mesh refinement). -/
796def HasZRSRegulatorRemoval (phase : ∀ n : ℕ, ExactPathClass n → ℝ) : Prop :=
797 ∃ L : ℂ, Filter.Tendsto (fun ρ : ℝ => Z_RS_uv ρ phase)
798 (nhdsWithin 0 (Set.Ioi 0)) (nhds L)
799
800/-! ## §11 (S2g). Status ledger -/
801
802/-- Status of the exact-shell Gaussian-UV module. Every `true` flag is
803grounded in its kernel theorem by `exactShellGaugeUVStatus_grounded`; the
804two `false` flags are the honest OPEN boundary.
805
806`continuum_limit_claimed` is `false` and MUST stay `false` in this
807module: the complexity cutoff is NOT mesh refinement, so nothing here
808touches the physical continuum limit; `path_sum_continuum_limit` and
809`gap2_continuum_and_measure` stay RED and this module flips NO
810`FullTheoryLedger` flag. -/
811structure ExactShellGaugeUVStatus where
812 /-- S1: `complexity_congr`, `exactSetoid`, `instFintypeExactPathClass`,
813 `shell_index_unique`, `toExact_relax`. -/
814 shell_structure_proved : Bool
815 /-- S1c: `exactPathClass_card_le`. -/
816 entropy_bound_proved : Bool
817 /-- S2c: `summable_zRSUVShell`. -/
818 uv_summability_proved : Bool
819 /-- S2d: `zRSUVCutoff_tendsto`. -/
820 cutoff_limit_proved : Bool
821 /-- S2e: `Z_RS_uv_zeroPhase_re_pos`. -/
822 nonvacuity_proved : Bool
823 /-- S2f: `HasZRSRegulatorRemoval` is a NAMED OPEN definition; MUST stay
824 `false` until a kernel proof of the `ρ → 0⁺` limit exists. -/
825 regulator_removal_proved : Bool
826 /-- The physical continuum limit is NOT claimed (complexity cutoff ≠
827 mesh refinement); MUST stay `false` in this module. -/
828 continuum_limit_claimed : Bool
829
830/-- The canonical status record. -/
831def exactShellGaugeUVStatus : ExactShellGaugeUVStatus where
832 shell_structure_proved := true
833 entropy_bound_proved := true
834 uv_summability_proved := true
835 cutoff_limit_proved := true
836 nonvacuity_proved := true
837 regulator_removal_proved := false
838 continuum_limit_claimed := false
839
840/-- **Grounding theorem.** The status flags are not bare Booleans: each
841`true` flag is tied to its kernel theorem, and the two OPEN flags are
842recorded `false`. -/
843theorem exactShellGaugeUVStatus_grounded :
844 (exactShellGaugeUVStatus.shell_structure_proved = true ∧
845 ∀ n : ℕ, 0 < Nat.card (ExactPathClass n)) ∧
846 (exactShellGaugeUVStatus.entropy_bound_proved = true ∧
847 ∀ n : ℕ, Nat.card (ExactPathClass n) ≤ (n + 1) ^ (12 * (n + 1))) ∧
848 (exactShellGaugeUVStatus.uv_summability_proved = true ∧
849 ∀ ρ : ℝ, 0 < ρ → ∀ phase : ∀ n : ℕ, ExactPathClass n → ℝ,
850 Summable (fun n => zRSUVShell ρ phase n)) ∧
851 (exactShellGaugeUVStatus.cutoff_limit_proved = true ∧
852 ∀ ρ : ℝ, 0 < ρ → ∀ phase : ∀ n : ℕ, ExactPathClass n → ℝ,
853 Filter.Tendsto
854 (fun M : ℕ => ∑ n ∈ Finset.range M, zRSUVShell ρ phase n)
855 Filter.atTop (nhds (Z_RS_uv ρ phase))) ∧
856 (exactShellGaugeUVStatus.nonvacuity_proved = true ∧
857 ∀ ρ : ℝ, 0 < ρ → 0 < (Z_RS_uv ρ zeroPhase).re) ∧
858 exactShellGaugeUVStatus.regulator_removal_proved = false ∧
859 exactShellGaugeUVStatus.continuum_limit_claimed = false :=
860 ⟨⟨rfl, exactPathClass_unbounded_support⟩,
861 ⟨rfl, exactPathClass_card_le⟩,
862 ⟨rfl, fun ρ hρ phase => summable_zRSUVShell ρ hρ phase⟩,
863 ⟨rfl, fun ρ hρ phase => zRSUVCutoff_tendsto ρ hρ phase⟩,
864 ⟨rfl, fun ρ hρ => Z_RS_uv_zeroPhase_re_pos ρ hρ⟩,
865 rfl, rfl⟩
866
867end ExactShellGaugeUV
868end SevenGaps
869end Gravity
870end IndisputableMonolith
871