IndisputableMonolith.Gravity.SevenGaps.RegulatorRemovalNoGo
IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean · 558 lines · 29 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugeUV
3
4/-!
5# Seven Gaps: regulator removal FAILS at zero phase (kernel no-go)
6
7## What this module proves (and what it does NOT)
8
9**Status: THEOREM (kernel no-go at zero phase).** This module proves that
10the Gaussian-regulated quotient path sum `Z_RS_uv` of
11`ExactShellGaugeUV` has NO `ρ → 0⁺` limit at zero phase
12(`not_hasZRSRegulatorRemoval_zeroPhase`): the named OPEN
13`HasZRSRegulatorRemoval zeroPhase` is refuted, not merely left open.
14The mechanism is quantitative and fully kernel-checked:
15
16* **Shell-mass identity (Burnside / orbit-stabilizer route).** For every
17 exact signature `(v, e, t)`, the sum of the per-class measures
18 `1/|Aut|` over the quotient equals the labeled count divided by the
19 full relabeling gauge volume `v!·e!·t!`
20 (`sum_classMuOn_eq_card_div_factorials`). The proof realizes the
21 relabeling-triple group as a torsor over the sigma of all relabelings
22 out of a fixed base complex (`relabelSigmaEquiv`), splits it fiberwise
23 by orbit-stabilizer (`orbitCard_mul_autCard`), and sums fibers over the
24 quotient (`sum_orbitCard`).
25* **Shell-mass divergence.** `shellMass n = ∑_classes 1/|Aut|` grows
26 without bound (`shellMass_unbounded`): restricting to the single
27 signature `(n, n, n)` gives `shellMass n ≥ n^(6n)/(n!)³ ≥ n^(3n)`
28 (`shellMass_lower`) since `n! ≤ n^n`. Labeled entropy beats the
29 factorial gauge volume, so the absolute/positive-term route to
30 regulator removal is dead.
31* **The headline no-go.** At zero phase every regulated term is real and
32 nonnegative, so a single shell bounds the regulated sum from below
33 (`single_shell_re_lower_bound`); as `ρ → 0⁺` the regulator on any fixed
34 shell tends to 1, so any putative limit `L` is exceeded by a shell of
35 mass `> L.re + 2`. Contradiction: `¬ HasZRSRegulatorRemoval zeroPhase`.
36
37**What is NOT proved (binding honesty disclosures):**
38* NOTHING about oscillatory phases: regulator removal for a genuine
39 action phase would require proved cancellation between unit phases and
40 remains OPEN (`OscillatoryRemovalOpen` is a definition-level Prop
41 below, never claimed, and `regulatorRemovalNoGoStatus` records it
42 `open`). The zero-phase refutation does NOT transport to nonzero
43 phases: the lower-bound argument uses positivity, which oscillation
44 destroys.
45* NOTHING about the physical continuum limit: the complexity cutoff is
46 NOT mesh refinement (standing constraint); no `FullTheoryLedger` or
47 `CampaignLedger` flag is flipped by this module.
48* `Z_RS_uv` is the QUOTIENT-sum convention (per-class measure `1/|Aut|`);
49 it must never be silently equated with the labeled-sum convention of
50 `PathSumMeasure.Z` (standing constraint, respected here: only
51 `ExactShellGaugeUV` definitions are used).
52
53## Status tiers (honest tagging)
54
55**THEOREM (proved below, 0 sorry, 0 new axioms, no `native_decide`):**
56`sum_classMuOn_eq_card_div_factorials`, `orbitCard_mul_autCard`,
57`shellMass_lower`, `shellMass_unbounded`,
58`single_shell_re_lower_bound`, `not_hasZRSRegulatorRemoval_zeroPhase`.
59
60**MODEL (definitional, inherited):** the `1/|Aut|` symmetry-factor
61measure and the Gaussian regulator shape, both from `ExactShellGaugeUV`.
62
63**OPEN (named, never claimed):** `OscillatoryRemovalOpen` (regulator
64removal for some nonzero phase); the physical continuum limit.
65
66Expected axiom footprint: standard trio
67`[propext, Classical.choice, Quot.sound]`.
68-/
69
70namespace IndisputableMonolith
71namespace Gravity
72namespace SevenGaps
73namespace RegulatorRemovalNoGo
74
75open ExactShellGaugeUV
76
77/-! ## §1. The relabeling triple group and its pushforward action -/
78
79variable {v e t : ℕ}
80
81/-- The full relabeling gauge group at signature `(v, e, t)`: independent
82permutations of the vertex, edge, and tetrahedron index sets. -/
83abbrev RelabelTriple (v e t : ℕ) : Type :=
84 (Fin v ≃ Fin v) × (Fin e ≃ Fin e) × (Fin t ≃ Fin t)
85
86/-- **Gauge volume.** The relabeling triple group has cardinality
87`v!·e!·t!`. -/
88theorem relabelTriple_card (v e t : ℕ) :
89 Fintype.card (RelabelTriple v e t)
90 = v.factorial * e.factorial * t.factorial := by
91 have hv : Fintype.card (Fin v ≃ Fin v) = v.factorial := by
92 rw [Fintype.card_equiv (Equiv.refl (Fin v)), Fintype.card_fin]
93 have he : Fintype.card (Fin e ≃ Fin e) = e.factorial := by
94 rw [Fintype.card_equiv (Equiv.refl (Fin e)), Fintype.card_fin]
95 have ht : Fintype.card (Fin t ≃ Fin t) = t.factorial := by
96 rw [Fintype.card_equiv (Equiv.refl (Fin t)), Fintype.card_fin]
97 rw [Fintype.card_prod, Fintype.card_prod, hv, he, ht]
98 ring
99
100/-- Pushforward action of a relabeling triple on a labeled complex:
101transport the incidence data along the three index bijections. -/
102def act (σ : RelabelTriple v e t) (K : ExactComplex v e t) :
103 ExactComplex v e t where
104 edgeVerts i := Prod.map σ.1 σ.1 (K.edgeVerts (σ.2.1.symm i))
105 tetVerts i j := σ.1 (K.tetVerts (σ.2.2.symm i) j)
106
107/-- The tautological relabeling witness from `K` to `act σ K`. -/
108def actRelabel (σ : RelabelTriple v e t) (K : ExactComplex v e t) :
109 ExactRelabel K (act σ K) where
110 vEquiv := σ.1
111 eEquiv := σ.2.1
112 tEquiv := σ.2.2
113 edge_comm := fun i => by
114 show Prod.map σ.1 σ.1 (K.edgeVerts (σ.2.1.symm (σ.2.1 i)))
115 = Prod.map σ.1 σ.1 (K.edgeVerts i)
116 rw [Equiv.symm_apply_apply]
117 tet_comm := fun i j => by
118 show σ.1 (K.tetVerts (σ.2.2.symm (σ.2.2 i)) j) = σ.1 (K.tetVerts i j)
119 rw [Equiv.symm_apply_apply]
120
121/-- Extensionality for exact complexes (incidence data determines the
122complex). -/
123theorem exactComplex_ext {K K' : ExactComplex v e t}
124 (he : K.edgeVerts = K'.edgeVerts) (ht : K.tetVerts = K'.tetVerts) :
125 K = K' := by
126 cases K with
127 | mk ev tv =>
128 cases K' with
129 | mk ev' tv' =>
130 simp only [ExactComplex.mk.injEq]
131 exact ⟨he, ht⟩
132
133/-- A pair `(target, witness)` in the total relabeling sigma is determined
134by the witness's index bijections (the target is forced by the
135commutation equations). -/
136theorem sigma_relabel_ext {K : ExactComplex v e t}
137 (p q : Σ K' : ExactComplex v e t, ExactRelabel K K')
138 (hv : p.2.vEquiv = q.2.vEquiv) (he : p.2.eEquiv = q.2.eEquiv)
139 (ht : p.2.tEquiv = q.2.tEquiv) : p = q := by
140 obtain ⟨K₁, r₁⟩ := p
141 obtain ⟨K₂, r₂⟩ := q
142 replace hv : r₁.vEquiv = r₂.vEquiv := hv
143 replace he : r₁.eEquiv = r₂.eEquiv := he
144 replace ht : r₁.tEquiv = r₂.tEquiv := ht
145 have hK : K₁ = K₂ := by
146 refine exactComplex_ext ?_ ?_
147 · funext i
148 have h₁ := r₁.edge_comm (r₁.eEquiv.symm i)
149 rw [Equiv.apply_symm_apply] at h₁
150 have h₂ := r₂.edge_comm (r₂.eEquiv.symm i)
151 rw [Equiv.apply_symm_apply] at h₂
152 rw [h₁, h₂, hv, he]
153 · funext i j
154 have h₁ := r₁.tet_comm (r₁.tEquiv.symm i) j
155 rw [Equiv.apply_symm_apply] at h₁
156 have h₂ := r₂.tet_comm (r₂.tEquiv.symm i) j
157 rw [Equiv.apply_symm_apply] at h₂
158 rw [h₁, h₂, hv, ht]
159 subst hK
160 exact congrArg (Sigma.mk K₁) (ExactRelabel.ext hv he ht)
161
162/-- **THEOREM (the total torsor).** The sigma of ALL relabelings out of a
163fixed base complex `K` is in bijection with the full relabeling triple
164group: every triple acts (pushforward), and every pair `(target, witness)`
165comes from exactly one triple. -/
166def relabelSigmaEquiv (K : ExactComplex v e t) :
167 RelabelTriple v e t ≃ Σ K' : ExactComplex v e t, ExactRelabel K K' where
168 toFun σ := ⟨act σ K, actRelabel σ K⟩
169 invFun p := p.2.toEquivTriple
170 left_inv _ := rfl
171 right_inv p := sigma_relabel_ext _ _ rfl rfl rfl
172
173/-! ## §2. Orbit-stabilizer on exact complexes -/
174
175/-- Relabeling witnesses between any two exact complexes form a finite
176type (inject into the finite triple of index bijections; generalizes
177`instFiniteExactAut` beyond the diagonal). -/
178instance instFiniteExactRelabel (K K' : ExactComplex v e t) :
179 Finite (ExactRelabel K K') :=
180 Finite.of_injective _
181 (ExactRelabel.toEquivTriple_injective (K := K) (K' := K'))
182
183/-- **THEOREM (torsor over the automorphism group).** Fixing one witness
184`r0 : ExactRelabel K K'`, composition `a ↦ a.trans r0` is a bijection
185`ExactAut K ≃ ExactRelabel K K'` (mirrors
186`ExactShellGaugePreflight.torsorEquiv` on the cap-free class). -/
187def torsorEquiv {K K' : ExactComplex v e t} (r0 : ExactRelabel K K') :
188 ExactAut K ≃ ExactRelabel K K' where
189 toFun a := a.trans r0
190 invFun r := r.trans r0.symm
191 left_inv a := by
192 apply ExactRelabel.ext <;>
193 · apply Equiv.ext
194 intro x
195 simp only [ExactRelabel.trans_vEquiv, ExactRelabel.trans_eEquiv,
196 ExactRelabel.trans_tEquiv, ExactRelabel.symm_vEquiv,
197 ExactRelabel.symm_eEquiv, ExactRelabel.symm_tEquiv,
198 Equiv.trans_apply, Equiv.symm_apply_apply]
199 right_inv r := by
200 apply ExactRelabel.ext <;>
201 · apply Equiv.ext
202 intro x
203 simp only [ExactRelabel.trans_vEquiv, ExactRelabel.trans_eEquiv,
204 ExactRelabel.trans_tEquiv, ExactRelabel.symm_vEquiv,
205 ExactRelabel.symm_eEquiv, ExactRelabel.symm_tEquiv,
206 Equiv.trans_apply, Equiv.apply_symm_apply]
207
208/-- The relabeling orbit size of `K` inside the exact labeled class. -/
209noncomputable def orbitCard (K : ExactComplex v e t) : ℕ :=
210 Nat.card {K' : ExactComplex v e t // GlobalEquivalent K K'}
211
212/-- Summing witness counts over all targets exhausts the triple group. -/
213theorem sum_card_relabel (K : ExactComplex v e t) :
214 ∑ K' : ExactComplex v e t, Nat.card (ExactRelabel K K')
215 = v.factorial * e.factorial * t.factorial := by
216 calc ∑ K' : ExactComplex v e t, Nat.card (ExactRelabel K K')
217 = Nat.card (Σ K' : ExactComplex v e t, ExactRelabel K K') :=
218 Nat.card_sigma.symm
219 _ = Nat.card (RelabelTriple v e t) :=
220 Nat.card_congr (relabelSigmaEquiv K).symm
221 _ = Fintype.card (RelabelTriple v e t) := Nat.card_eq_fintype_card
222 _ = v.factorial * e.factorial * t.factorial := relabelTriple_card v e t
223
224/-- Summing witness counts over all targets factorizes through the orbit:
225each on-orbit fiber is an `Aut`-torsor, each off-orbit fiber is empty. -/
226theorem sum_card_relabel_eq_orbit (K : ExactComplex v e t) :
227 ∑ K' : ExactComplex v e t, Nat.card (ExactRelabel K K')
228 = orbitCard K * Nat.card (ExactAut K) := by
229 classical
230 calc ∑ K' : ExactComplex v e t, Nat.card (ExactRelabel K K')
231 = ∑ K' : ExactComplex v e t,
232 (if GlobalEquivalent K K' then Nat.card (ExactAut K) else 0) := by
233 refine Finset.sum_congr rfl fun K' _ => ?_
234 by_cases h : GlobalEquivalent K K'
235 · rw [if_pos h]
236 obtain ⟨r0⟩ := h
237 exact (Nat.card_congr (torsorEquiv r0)).symm
238 · rw [if_neg h]
239 haveI : IsEmpty (ExactRelabel K K') := ⟨fun r => h ⟨r⟩⟩
240 exact Nat.card_of_isEmpty
241 _ = ∑ K' ∈ Finset.univ.filter (fun K' => GlobalEquivalent K K'),
242 Nat.card (ExactAut K) := (Finset.sum_filter _ _).symm
243 _ = (Finset.univ.filter (fun K' => GlobalEquivalent K K')).card
244 * Nat.card (ExactAut K) := by
245 rw [Finset.sum_const, smul_eq_mul]
246 _ = orbitCard K * Nat.card (ExactAut K) := by
247 congr 1
248 show (Finset.univ.filter (fun K' => GlobalEquivalent K K')).card
249 = Nat.card {K' : ExactComplex v e t // GlobalEquivalent K K'}
250 rw [Nat.card_eq_fintype_card, Fintype.card_subtype]
251
252/-- **THEOREM (orbit-stabilizer, exact form).** Orbit size times
253automorphism count equals the full gauge volume `v!·e!·t!` for EVERY
254labeled complex. -/
255theorem orbitCard_mul_autCard (K : ExactComplex v e t) :
256 orbitCard K * Nat.card (ExactAut K)
257 = v.factorial * e.factorial * t.factorial := by
258 rw [← sum_card_relabel_eq_orbit K]
259 exact sum_card_relabel K
260
261/-! ## §3. The shell-mass identity (Burnside route) -/
262
263/-- The quotient at a fixed signature is a finite type (noncomputable
264enumeration; `instFiniteExactQuotient` supplies finiteness). -/
265noncomputable instance instFintypeExactQuotient (v e t : ℕ) :
266 Fintype (Quotient (exactSetoid v e t)) :=
267 Fintype.ofFinite _
268
269/-- The per-class measure at a representative: `classMuOn` evaluated on a
270class is `exactMu` of its chosen representative. -/
271theorem classMuOn_out (c : Quotient (exactSetoid v e t)) :
272 classMuOn v e t c = exactMu (Quotient.out c) := by
273 refine Quotient.inductionOn c ?_
274 intro K
275 change exactMu K =
276 exactMu (Quotient.out (Quotient.mk (exactSetoid v e t) K))
277 exact (exactMu_congr
278 (Quotient.exact
279 (Quotient.out_eq (Quotient.mk (exactSetoid v e t) K)))).symm
280
281/-- The fiber of the quotient map over a class has the orbit cardinality
282of the class representative. -/
283theorem fiber_card (c : Quotient (exactSetoid v e t)) :
284 Nat.card {K : ExactComplex v e t //
285 Quotient.mk (exactSetoid v e t) K = c}
286 = orbitCard (Quotient.out c) := by
287 refine Nat.card_congr (Equiv.subtypeEquivRight fun K => ?_)
288 constructor
289 · intro hK
290 exact Quotient.exact ((Quotient.out_eq c).trans hK.symm)
291 · intro hE
292 exact (Quotient.sound hE).symm.trans (Quotient.out_eq c)
293
294/-- Orbit sizes over the quotient sum to the labeled count (the orbits
295partition the labeled class). -/
296theorem sum_orbitCard (v e t : ℕ) :
297 ∑ c : Quotient (exactSetoid v e t), orbitCard (Quotient.out c)
298 = Fintype.card (ExactComplex v e t) := by
299 classical
300 have h1 : Nat.card (Σ c : Quotient (exactSetoid v e t),
301 {K : ExactComplex v e t // Quotient.mk (exactSetoid v e t) K = c})
302 = Fintype.card (ExactComplex v e t) := by
303 rw [Nat.card_congr
304 (Equiv.sigmaFiberEquiv (Quotient.mk (exactSetoid v e t))),
305 Nat.card_eq_fintype_card]
306 rw [Nat.card_sigma] at h1
307 rw [← h1]
308 exact Finset.sum_congr rfl fun c _ => (fiber_card c).symm
309
310/-- **HEADLINE IDENTITY (Burnside / orbit-stabilizer route).** At every
311exact signature, the total per-class measure equals the labeled count
312divided by the full gauge volume:
313`∑_classes 1/|Aut| = |labeled| / (v!·e!·t!)`. -/
314theorem sum_classMuOn_eq_card_div_factorials (v e t : ℕ) :
315 ∑ c : Quotient (exactSetoid v e t), classMuOn v e t c
316 = (Fintype.card (ExactComplex v e t) : ℝ)
317 / ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ) := by
318 classical
319 have hfactpos : 0 < v.factorial * e.factorial * t.factorial :=
320 Nat.mul_pos (Nat.mul_pos v.factorial_pos e.factorial_pos) t.factorial_pos
321 have hfactR : (0 : ℝ) < ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ) := by
322 exact_mod_cast hfactpos
323 rw [eq_div_iff hfactR.ne', Finset.sum_mul]
324 have hterm : ∀ c : Quotient (exactSetoid v e t),
325 classMuOn v e t c * ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ)
326 = (orbitCard (Quotient.out c) : ℝ) := by
327 intro c
328 have hOS := orbitCard_mul_autCard (Quotient.out c)
329 have hautpos : (0 : ℝ) < (Nat.card (ExactAut (Quotient.out c)) : ℝ) := by
330 exact_mod_cast exactAutCard_pos (Quotient.out c)
331 have hcast : (orbitCard (Quotient.out c) : ℝ)
332 * (Nat.card (ExactAut (Quotient.out c)) : ℝ)
333 = ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ) := by
334 exact_mod_cast congrArg (Nat.cast : ℕ → ℝ) hOS
335 rw [classMuOn_out c]
336 unfold exactMu
337 rw [div_mul_eq_mul_div, one_mul, ← hcast, mul_div_assoc,
338 div_self hautpos.ne', mul_one]
339 rw [Finset.sum_congr rfl fun c _ => hterm c, ← Nat.cast_sum]
340 exact_mod_cast congrArg (Nat.cast : ℕ → ℝ) (sum_orbitCard v e t)
341
342/-! ## §4. Shell-mass divergence -/
343
344/-- The cube signature `(n, n, n)` is a shell signature at level `n`. -/
345def cubeSig (n : ℕ) : ShellSig n :=
346 ⟨(⟨n, Nat.lt_succ_self n⟩, ⟨n, Nat.lt_succ_self n⟩,
347 ⟨n, Nat.lt_succ_self n⟩), by
348 show max n (max n n) = n
349 rw [max_self, max_self]⟩
350
351/-- Restricting the shell mass to the single cube signature `(n, n, n)`
352bounds it from below (all classes carry positive measure). -/
353theorem cube_sum_le_shellMass (n : ℕ) :
354 ∑ q : Quotient (exactSetoid n n n), classMuOn n n n q ≤ shellMass n := by
355 classical
356 have himg : ∑ c ∈ Finset.univ.image
357 (fun q : Quotient (exactSetoid n n n) =>
358 (⟨cubeSig n, q⟩ : ExactPathClass n)),
359 classMu c
360 = ∑ q : Quotient (exactSetoid n n n),
361 classMu (⟨cubeSig n, q⟩ : ExactPathClass n) :=
362 Finset.sum_image
363 (f := fun c : ExactPathClass n => classMu c)
364 (s := (Finset.univ : Finset (Quotient (exactSetoid n n n))))
365 (g := fun q : Quotient (exactSetoid n n n) =>
366 (⟨cubeSig n, q⟩ : ExactPathClass n))
367 (by
368 intro q _ q' _ h
369 cases h
370 rfl)
371 calc ∑ q : Quotient (exactSetoid n n n), classMuOn n n n q
372 = ∑ q : Quotient (exactSetoid n n n),
373 classMu (⟨cubeSig n, q⟩ : ExactPathClass n) :=
374 Finset.sum_congr rfl fun q _ => rfl
375 _ = ∑ c ∈ Finset.univ.image
376 (fun q : Quotient (exactSetoid n n n) =>
377 (⟨cubeSig n, q⟩ : ExactPathClass n)),
378 classMu c := himg.symm
379 _ ≤ ∑ c : ExactPathClass n, classMu c :=
380 Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ _)
381 (fun c _ _ => (classMu_pos c).le)
382 _ = shellMass n := rfl
383
384/-- **Quantitative shell-mass lower bound.**
385`shellMass n ≥ n^(6n)/(n!)³ ≥ n^(3n)`: the labeled entropy of the cube
386signature beats its factorial gauge volume. -/
387theorem shellMass_lower (n : ℕ) :
388 ((n : ℝ)) ^ (3 * n) ≤ shellMass n := by
389 have hfact3 : n.factorial * n.factorial * n.factorial ≤ n ^ (3 * n) := by
390 have h := Nat.factorial_le_pow n
391 calc n.factorial * n.factorial * n.factorial
392 ≤ n ^ n * n ^ n * n ^ n := Nat.mul_le_mul (Nat.mul_le_mul h h) h
393 _ = n ^ (3 * n) := by
394 rw [← pow_add, ← pow_add]
395 congr 1
396 omega
397 have hcard : Fintype.card (ExactComplex n n n) = n ^ (6 * n) := by
398 rw [exactComplex_card_eq, ← pow_two, ← pow_mul, ← pow_mul, ← pow_add]
399 congr 1
400 omega
401 have hfactR : (0 : ℝ) < ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ) := by
402 exact_mod_cast
403 Nat.mul_pos (Nat.mul_pos n.factorial_pos n.factorial_pos) n.factorial_pos
404 have hkey : ((n : ℝ)) ^ (3 * n)
405 ≤ (Fintype.card (ExactComplex n n n) : ℝ)
406 / ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ) := by
407 rw [le_div_iff₀ hfactR]
408 calc ((n : ℝ)) ^ (3 * n)
409 * ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ)
410 ≤ ((n : ℝ)) ^ (3 * n) * ((n : ℝ)) ^ (3 * n) := by
411 refine mul_le_mul_of_nonneg_left ?_ (by positivity)
412 calc ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ)
413 ≤ ((n ^ (3 * n) : ℕ) : ℝ) := by exact_mod_cast hfact3
414 _ = ((n : ℝ)) ^ (3 * n) := Nat.cast_pow n (3 * n)
415 _ = ((n : ℝ)) ^ (6 * n) := by
416 rw [← pow_add]
417 congr 1
418 omega
419 _ = ((n ^ (6 * n) : ℕ) : ℝ) := (Nat.cast_pow n (6 * n)).symm
420 _ = (Fintype.card (ExactComplex n n n) : ℝ) := by rw [hcard]
421 calc ((n : ℝ)) ^ (3 * n)
422 ≤ (Fintype.card (ExactComplex n n n) : ℝ)
423 / ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ) := hkey
424 _ = ∑ q : Quotient (exactSetoid n n n), classMuOn n n n q :=
425 (sum_classMuOn_eq_card_div_factorials n n n).symm
426 _ ≤ shellMass n := cube_sum_le_shellMass n
427
428/-- **HEADLINE DIVERGENCE.** The shell masses are unbounded: for every
429real threshold there is a shell whose total `1/|Aut|` mass exceeds it. -/
430theorem shellMass_unbounded (C : ℝ) : ∃ n : ℕ, C < shellMass n := by
431 obtain ⟨m, hm⟩ := exists_nat_gt C
432 refine ⟨max 1 m, ?_⟩
433 have hle : ((max 1 m : ℕ) : ℝ) ^ (3 * max 1 m) ≤ shellMass (max 1 m) :=
434 shellMass_lower (max 1 m)
435 have hselfN : (max 1 m : ℕ) ≤ (max 1 m) ^ (3 * max 1 m) :=
436 Nat.le_self_pow (by omega) _
437 have hself : ((max 1 m : ℕ) : ℝ) ≤ ((max 1 m : ℕ) : ℝ) ^ (3 * max 1 m) := by
438 calc ((max 1 m : ℕ) : ℝ)
439 ≤ (((max 1 m) ^ (3 * max 1 m) : ℕ) : ℝ) := by exact_mod_cast hselfN
440 _ = ((max 1 m : ℕ) : ℝ) ^ (3 * max 1 m) := Nat.cast_pow _ _
441 have hmR : (m : ℝ) ≤ ((max 1 m : ℕ) : ℝ) := by
442 exact_mod_cast le_max_right 1 m
443 linarith
444
445/-! ## §5. The headline no-go: regulator removal fails at zero phase -/
446
447/-- **Single-shell lower bound.** At zero phase every regulated term is
448real and nonnegative, so any single shell bounds the real part of the
449regulated path sum from below. -/
450theorem single_shell_re_lower_bound (ρ : ℝ) (hρ : 0 < ρ) (n₀ : ℕ) :
451 Real.exp (-ρ * (n₀ : ℝ) ^ 2) * shellMass n₀
452 ≤ (Z_RS_uv ρ zeroPhase).re := by
453 have hsC : Summable
454 (fun n : ℕ => ((Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ)) :=
455 (summable_zRSUVShell ρ hρ zeroPhase).congr
456 (fun n => zRSUVShell_zeroPhase_eq ρ n)
457 have hsR : Summable
458 (fun n : ℕ => Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n) :=
459 Complex.summable_ofReal.mp hsC
460 have hZ : Z_RS_uv ρ zeroPhase =
461 ((∑' n : ℕ, Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ) := by
462 unfold Z_RS_uv
463 rw [tsum_congr (fun n => zRSUVShell_zeroPhase_eq ρ n),
464 ← Complex.ofReal_tsum]
465 rw [hZ, Complex.ofReal_re]
466 exact hsR.le_tsum n₀
467 (fun j _ => (mul_pos (Real.exp_pos _) (shellMass_pos j)).le)
468
469/-- **HEADLINE (kernel no-go).** Regulator removal FAILS at zero phase:
470the Gaussian-regulated quotient path sum `Z_RS_uv ρ zeroPhase` has NO
471limit as `ρ → 0⁺`. Mechanism: any putative limit `L` is beaten by a
472single shell of mass `> L.re + 2` (shell masses diverge), whose regulated
473contribution tends to its full mass as the regulator is removed. -/
474theorem not_hasZRSRegulatorRemoval_zeroPhase :
475 ¬ HasZRSRegulatorRemoval zeroPhase := by
476 rintro ⟨L, hL⟩
477 have hre : Filter.Tendsto (fun ρ : ℝ => (Z_RS_uv ρ zeroPhase).re)
478 (nhdsWithin 0 (Set.Ioi 0)) (nhds L.re) :=
479 (Complex.continuous_re.tendsto L).comp hL
480 obtain ⟨n₀, hn₀⟩ := shellMass_unbounded (L.re + 2)
481 have hexp : Filter.Tendsto
482 (fun ρ : ℝ => Real.exp (-ρ * (n₀ : ℝ) ^ 2) * shellMass n₀)
483 (nhdsWithin 0 (Set.Ioi 0)) (nhds (shellMass n₀)) := by
484 refine Filter.Tendsto.mono_left ?_ nhdsWithin_le_nhds
485 refine Continuous.tendsto' ?_ 0 (shellMass n₀) ?_
486 · exact (Real.continuous_exp.comp
487 (continuous_neg.mul continuous_const)).mul continuous_const
488 · simp only [neg_zero, zero_mul, Real.exp_zero, one_mul]
489 have hev1 : ∀ᶠ ρ in nhdsWithin (0 : ℝ) (Set.Ioi 0),
490 L.re + 1 < Real.exp (-ρ * (n₀ : ℝ) ^ 2) * shellMass n₀ :=
491 hexp.eventually_const_lt (by linarith)
492 have hev2 : ∀ᶠ ρ in nhdsWithin (0 : ℝ) (Set.Ioi 0),
493 (Z_RS_uv ρ zeroPhase).re < L.re + 1 :=
494 hre.eventually_lt_const (by linarith)
495 have hev3 : ∀ᶠ ρ in nhdsWithin (0 : ℝ) (Set.Ioi 0), ρ ∈ Set.Ioi (0 : ℝ) :=
496 eventually_mem_nhdsWithin
497 obtain ⟨ρ, ⟨h1, h2⟩, h3⟩ := ((hev1.and hev2).and hev3).exists
498 have h4 := single_shell_re_lower_bound ρ (Set.mem_Ioi.mp h3) n₀
499 linarith
500
501/-! ## §6. Status record (honest boundary) -/
502
503/-- **NAMED OPEN (definition only, NEVER claimed).** Whether regulator
504removal holds for SOME phase (in particular, for a genuine oscillatory
505action phase whose cancellations could tame the diverging shell masses).
506The zero-phase refutation above does NOT decide this: its lower-bound
507argument uses positivity, which oscillation destroys. No theorem in this
508module asserts or refutes this Prop. -/
509def OscillatoryRemovalOpen : Prop :=
510 ∃ phase : ∀ n : ℕ, ExactPathClass n → ℝ, HasZRSRegulatorRemoval phase
511
512/-- Status of the regulator-removal no-go module. Every `true` flag is
513grounded in its kernel theorem by `regulatorRemovalNoGoStatus_grounded`;
514`oscillatory_removal_open` records the honest OPEN boundary (the nonzero-
515phase question, `OscillatoryRemovalOpen`, is a definition-level Prop with
516no claim). This module flips NO `FullTheoryLedger` or `CampaignLedger`
517flag. -/
518structure RegulatorRemovalNoGoStatus where
519 /-- §3: `sum_classMuOn_eq_card_div_factorials` (Burnside identity). -/
520 shell_mass_identity_proved : Bool
521 /-- §4: `shellMass_unbounded` (via `shellMass_lower`). -/
522 shell_mass_divergence_proved : Bool
523 /-- §5: `not_hasZRSRegulatorRemoval_zeroPhase`. -/
524 zero_phase_removal_refuted : Bool
525 /-- §6: `OscillatoryRemovalOpen` is a NAMED OPEN definition; MUST stay
526 `true` (open) until a kernel proof or refutation for nonzero phases
527 exists. -/
528 oscillatory_removal_open : Bool
529
530/-- The canonical status record. -/
531def regulatorRemovalNoGoStatus : RegulatorRemovalNoGoStatus where
532 shell_mass_identity_proved := true
533 shell_mass_divergence_proved := true
534 zero_phase_removal_refuted := true
535 oscillatory_removal_open := true
536
537/-- **Grounding theorem.** The status flags are not bare Booleans: each
538`true` proof flag is tied to its kernel theorem, and the OPEN flag is
539recorded without any claim on `OscillatoryRemovalOpen`. -/
540theorem regulatorRemovalNoGoStatus_grounded :
541 (regulatorRemovalNoGoStatus.shell_mass_identity_proved = true ∧
542 ∀ v e t : ℕ, ∑ c : Quotient (exactSetoid v e t), classMuOn v e t c
543 = (Fintype.card (ExactComplex v e t) : ℝ)
544 / ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ)) ∧
545 (regulatorRemovalNoGoStatus.shell_mass_divergence_proved = true ∧
546 ∀ C : ℝ, ∃ n : ℕ, C < shellMass n) ∧
547 (regulatorRemovalNoGoStatus.zero_phase_removal_refuted = true ∧
548 ¬ HasZRSRegulatorRemoval zeroPhase) ∧
549 regulatorRemovalNoGoStatus.oscillatory_removal_open = true :=
550 ⟨⟨rfl, sum_classMuOn_eq_card_div_factorials⟩,
551 ⟨rfl, shellMass_unbounded⟩,
552 ⟨rfl, not_hasZRSRegulatorRemoval_zeroPhase⟩, rfl⟩
553
554end RegulatorRemovalNoGo
555end SevenGaps
556end Gravity
557end IndisputableMonolith
558