IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure
IndisputableMonolith/Gravity/SevenGaps/PathSumMeasure.lean · 530 lines · 56 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.PathSumUVBound
3
4/-!
5# Seven Gaps, Lane 2: A Proved Path-Sum Measure for Z_RS
6
7## Status tiers (honest tagging)
8
9**THEOREM (proved below, 0 sorry, 0 new axioms):**
10* The scoped configuration class `BoundedComplex B` is a `Fintype`
11 (`instFintypeBoundedComplex`, via the explicit equivalence `codeEquiv`).
12 Scope honesty: `BoundedComplex` carries arbitrary bounded incidence data
13 (it does not enforce simplicial constraints, so it CONTAINS all bounded
14 triangulations but also non-simplicial configurations); finiteness of the
15 superclass gives finiteness of every subclass. This DISCHARGES the
16 count-finiteness content of the assumed `growthBase` field of
17 `PathSumUVBound.AdmissibleTriangulationFamily` (a proved finite cardinal
18 where a bound was postulated); the sharper exponential-growth semantics
19 of that field for exact simplicial classes remains OPEN.
20* Relabeling isomorphism is a genuine equivalence relation
21 (`relabelSetoid`; refl/symm/trans proved, not asserted), and the quotient
22 `TriangulationClass B` is finite (`triangulationClass_finite`).
23* The automorphism group `Aut K` of a labeled complex is finite and nonempty,
24 so the symmetry-factor measure `mu K = 1 / |Aut K|` satisfies
25 `0 < mu K ≤ 1` (`mu_pos`, `mu_le_one`) and is a relabeling invariant
26 (`mu_congr`).
27* The path sum `Z B w = Σ_K mu(K) · w(K)` over the labeled class is a finite
28 sum with the modulus bounds `‖Z‖ ≤ Σ mu` (`Z_norm_le_muSum`) and
29 `‖Z‖ ≤ card (BoundedComplex B)` (`Z_norm_le_card`), and it is invariant
30 under any equivalence-preserving bijection of configurations
31 (`Z_relabel_invariant`): the measure respects the equivalence.
32* The unitary instance `w K = exp(i·S K)` for a real action `S` has
33 `‖w K‖ = 1`, so all bounds apply (`zRS_scoped_wellDefined`). This is the
34 honest Z_RS statement for the scoped class.
35
36**MODEL (definitional assumptions, stated, not derived):**
37* Scoped class: bounded combinatorial triangulations at a fixed lattice
38 scale. The recognition substrate fixes the edge length at the minimum
39 mesh ℓ_sub, so path-sum configurations are combinatorial and equilateral;
40 all geometric data is carried by the incidence maps. This is the standard
41 CDT-style measure class. `BoundedComplex` mirrors the incidence shape of
42 `IndisputableMonolith.Geometry.ReggeTriangulation3D.Triangulation3D`
43 (fields `nV nE nT`, `edgeVerts : Fin nE → Fin nV × Fin nV`,
44 `tetVerts : Fin nT → Fin 4 → Fin nV`), with the metric field dropped
45 (equilateral at fixed scale) and the size capped by `B`.
46* Measure convention: the LABELED sum with the `1/|Aut|` symmetry factor
47 (the standard discrete-gravity convention), not the bare quotient sum.
48 `mu_congr` + `Z_relabel_invariant` give compatibility EVIDENCE (measure
49 and summand are class functions); the orbit-counting identity equating
50 the weighted labeled sum with a quotient sum is not proved here.
51* The intended action `S` is the sinh recognition action of
52 `PathSumUVBound.recognitionAction` evaluated on the deficit data of the
53 complex; here `S` is an arbitrary real action parameter with an explicit
54 relabeling-invariance hypothesis where needed.
55
56**OPEN (recorded in `pathSumMeasureStatus`, not claimed):**
57* The continuum limit of `Z B` as `B → ∞`.
58* A substrate-DERIVED nonuniform measure (beyond the uniform `1/|Aut|`
59 convention).
60
61## Proof notes
62* No `decide` / `native_decide` anywhere; cardinalities are never computed
63 numerically, only bounded.
64* All undischarged premises are explicit hypothesis parameters
65 (`hw`, `hσ`, `hS`).
66-/
67
68namespace IndisputableMonolith
69namespace Gravity
70namespace SevenGaps
71namespace PathSumMeasure
72
73/-! ## §1. The scoped configuration class -/
74
75/-- A bounded combinatorial triangulation at fixed lattice scale: at most `B`
76vertices, edges, and tetrahedra, with abstract incidence data. MODEL: the
77substrate fixes the edge length at the minimum mesh, so configurations are
78combinatorial and equilateral (CDT-style); this mirrors the shape of
79`Geometry.ReggeTriangulation3D.Triangulation3D` with the metric field
80dropped and an explicit size cap. -/
81structure BoundedComplex (B : ℕ) where
82 nV : ℕ
83 nE : ℕ
84 nT : ℕ
85 hV : nV ≤ B
86 hE : nE ≤ B
87 hT : nT ≤ B
88 edgeVerts : Fin nE → Fin nV × Fin nV
89 tetVerts : Fin nT → Fin 4 → Fin nV
90
91/-- The empty complex: a concrete inhabitant of every `BoundedComplex B`. -/
92def emptyComplex (B : ℕ) : BoundedComplex B where
93 nV := 0
94 nE := 0
95 nT := 0
96 hV := Nat.zero_le B
97 hE := Nat.zero_le B
98 hT := Nat.zero_le B
99 edgeVerts := fun e => e.elim0
100 tetVerts := fun t => t.elim0
101
102instance (B : ℕ) : Nonempty (BoundedComplex B) := ⟨emptyComplex B⟩
103
104/-! ## §2. THEOREM: count-finiteness of the scoped class
105
106We exhibit an explicit equivalence with a finite code type (sizes packaged
107as `Fin (B+1)`, incidence maps as functions between explicit finite types)
108and transfer the `Fintype` instance. This replaces the ASSUMED `growthBase`
109count bound of `PathSumUVBound.AdmissibleTriangulationFamily` with a proved
110finite cardinal. -/
111
112/-- Finite code type for `BoundedComplex B`: sizes in `Fin (B+1)`, incidence
113data as functions between explicit finite types. `Fintype` is automatic
114from the sigma/pi/prod instances. -/
115abbrev CodeType (B : ℕ) : Type :=
116 Σ (v : Fin (B + 1)) (e : Fin (B + 1)) (t : Fin (B + 1)),
117 (Fin (e : ℕ) → Fin (v : ℕ) × Fin (v : ℕ)) × (Fin (t : ℕ) → Fin 4 → Fin (v : ℕ))
118
119/-- Encode a bounded complex into the finite code type. -/
120def toCode {B : ℕ} (K : BoundedComplex B) : CodeType B :=
121 ⟨⟨K.nV, Nat.lt_succ_of_le K.hV⟩, ⟨K.nE, Nat.lt_succ_of_le K.hE⟩,
122 ⟨K.nT, Nat.lt_succ_of_le K.hT⟩, (K.edgeVerts, K.tetVerts)⟩
123
124/-- Decode: inverse of `toCode`. -/
125def ofCode {B : ℕ} (c : CodeType B) : BoundedComplex B where
126 nV := c.1
127 nE := c.2.1
128 nT := c.2.2.1
129 hV := Nat.lt_succ_iff.mp c.1.isLt
130 hE := Nat.lt_succ_iff.mp c.2.1.isLt
131 hT := Nat.lt_succ_iff.mp c.2.2.1.isLt
132 edgeVerts := c.2.2.2.1
133 tetVerts := c.2.2.2.2
134
135/-- The scoped class is EQUIVALENT to the finite code type (both inverses
136are definitional, using structure eta and proof irrelevance). -/
137def codeEquiv (B : ℕ) : BoundedComplex B ≃ CodeType B where
138 toFun := toCode
139 invFun := ofCode
140 left_inv _ := rfl
141 right_inv _ := rfl
142
143/-- **THEOREM (count-finiteness).** The scoped class of bounded
144combinatorial triangulations is a finite type. This is the proved
145replacement for the assumed `growthBase` field. -/
146instance instFintypeBoundedComplex (B : ℕ) : Fintype (BoundedComplex B) :=
147 Fintype.ofEquiv (CodeType B) (codeEquiv B).symm
148
149/-- The scoped class has at least one element (the empty complex). -/
150theorem boundedComplex_card_pos (B : ℕ) : 0 < Fintype.card (BoundedComplex B) :=
151 Fintype.card_pos
152
153/-! ## §3. Relabeling isomorphism: a genuine Setoid -/
154
155/-- A relabeling isomorphism between two bounded complexes: bijections of
156the vertex/edge/tet index sets commuting with the incidence maps. -/
157structure Relabel {B : ℕ} (K K' : BoundedComplex B) where
158 vEquiv : Fin K.nV ≃ Fin K'.nV
159 eEquiv : Fin K.nE ≃ Fin K'.nE
160 tEquiv : Fin K.nT ≃ Fin K'.nT
161 edge_comm : ∀ e : Fin K.nE,
162 K'.edgeVerts (eEquiv e) = Prod.map vEquiv vEquiv (K.edgeVerts e)
163 tet_comm : ∀ (t : Fin K.nT) (i : Fin 4),
164 K'.tetVerts (tEquiv t) i = vEquiv (K.tetVerts t i)
165
166namespace Relabel
167
168variable {B : ℕ}
169
170/-- Identity relabeling. -/
171def refl (K : BoundedComplex B) : Relabel K K where
172 vEquiv := Equiv.refl _
173 eEquiv := Equiv.refl _
174 tEquiv := Equiv.refl _
175 edge_comm := fun _ => rfl
176 tet_comm := fun _ _ => rfl
177
178/-- Inverse relabeling. -/
179def symm {K K' : BoundedComplex B} (r : Relabel K K') : Relabel K' K where
180 vEquiv := r.vEquiv.symm
181 eEquiv := r.eEquiv.symm
182 tEquiv := r.tEquiv.symm
183 edge_comm := fun e => by
184 have h := r.edge_comm (r.eEquiv.symm e)
185 rw [Equiv.apply_symm_apply] at h
186 rw [h, Prod.map_map, Equiv.symm_comp_self, Prod.map_id, id_eq]
187 tet_comm := fun t i => by
188 have h := r.tet_comm (r.tEquiv.symm t) i
189 rw [Equiv.apply_symm_apply] at h
190 rw [h, Equiv.symm_apply_apply]
191
192/-- Composite relabeling. -/
193def trans {K₁ K₂ K₃ : BoundedComplex B} (r : Relabel K₁ K₂) (s : Relabel K₂ K₃) :
194 Relabel K₁ K₃ where
195 vEquiv := r.vEquiv.trans s.vEquiv
196 eEquiv := r.eEquiv.trans s.eEquiv
197 tEquiv := r.tEquiv.trans s.tEquiv
198 edge_comm := fun e => by
199 rw [Equiv.trans_apply, s.edge_comm, r.edge_comm, Prod.map_map, Equiv.coe_trans]
200 tet_comm := fun t i => by
201 rw [Equiv.trans_apply, s.tet_comm, r.tet_comm, Equiv.trans_apply]
202
203@[simp] theorem refl_vEquiv (K : BoundedComplex B) : (refl K).vEquiv = Equiv.refl _ := rfl
204
205@[simp] theorem symm_vEquiv {K K' : BoundedComplex B} (r : Relabel K K') :
206 r.symm.vEquiv = r.vEquiv.symm := rfl
207@[simp] theorem symm_eEquiv {K K' : BoundedComplex B} (r : Relabel K K') :
208 r.symm.eEquiv = r.eEquiv.symm := rfl
209@[simp] theorem symm_tEquiv {K K' : BoundedComplex B} (r : Relabel K K') :
210 r.symm.tEquiv = r.tEquiv.symm := rfl
211
212@[simp] theorem trans_vEquiv {K₁ K₂ K₃ : BoundedComplex B}
213 (r : Relabel K₁ K₂) (s : Relabel K₂ K₃) :
214 (r.trans s).vEquiv = r.vEquiv.trans s.vEquiv := rfl
215@[simp] theorem trans_eEquiv {K₁ K₂ K₃ : BoundedComplex B}
216 (r : Relabel K₁ K₂) (s : Relabel K₂ K₃) :
217 (r.trans s).eEquiv = r.eEquiv.trans s.eEquiv := rfl
218@[simp] theorem trans_tEquiv {K₁ K₂ K₃ : BoundedComplex B}
219 (r : Relabel K₁ K₂) (s : Relabel K₂ K₃) :
220 (r.trans s).tEquiv = r.tEquiv.trans s.tEquiv := rfl
221
222/-- Forget the commutation proofs: the underlying triple of index bijections. -/
223def toEquivTriple {K K' : BoundedComplex B} (r : Relabel K K') :
224 (Fin K.nV ≃ Fin K'.nV) × (Fin K.nE ≃ Fin K'.nE) × (Fin K.nT ≃ Fin K'.nT) :=
225 (r.vEquiv, r.eEquiv, r.tEquiv)
226
227/-- A relabeling is determined by its index bijections (the commutation
228fields are propositions). -/
229theorem toEquivTriple_injective {K K' : BoundedComplex B} :
230 Function.Injective (toEquivTriple (K := K) (K' := K')) := by
231 rintro ⟨v₁, e₁, t₁, p₁, q₁⟩ ⟨v₂, e₂, t₂, p₂, q₂⟩ h
232 simp only [toEquivTriple, Prod.mk.injEq] at h
233 obtain ⟨h1, h2, h3⟩ := h
234 subst h1
235 subst h2
236 subst h3
237 rfl
238
239/-- Extensionality for relabelings. -/
240theorem ext {K K' : BoundedComplex B} {r s : Relabel K K'}
241 (hv : r.vEquiv = s.vEquiv) (he : r.eEquiv = s.eEquiv)
242 (ht : r.tEquiv = s.tEquiv) : r = s := by
243 apply toEquivTriple_injective
244 unfold toEquivTriple
245 rw [hv, he, ht]
246
247end Relabel
248
249/-- Two bounded complexes are EQUIVALENT iff a relabeling isomorphism
250exists between them. -/
251def Equivalent {B : ℕ} (K K' : BoundedComplex B) : Prop :=
252 Nonempty (Relabel K K')
253
254/-- **THEOREM (genuine equivalence relation).** Relabeling isomorphism is a
255Setoid on the scoped class: refl/symm/trans are proved via the explicit
256identity/inverse/composite relabelings above. -/
257def relabelSetoid (B : ℕ) : Setoid (BoundedComplex B) where
258 r := Equivalent
259 iseqv :=
260 ⟨fun K => ⟨Relabel.refl K⟩,
261 fun h => h.elim fun r => ⟨r.symm⟩,
262 fun h₁ h₂ => h₁.elim fun r => h₂.elim fun s => ⟨r.trans s⟩⟩
263
264/-- Combinatorially distinct triangulations: the quotient of the labeled
265scoped class by relabeling isomorphism. -/
266abbrev TriangulationClass (B : ℕ) := Quotient (relabelSetoid B)
267
268/-- **THEOREM (quotient finiteness).** The set of combinatorially distinct
269bounded triangulations is finite. -/
270theorem triangulationClass_finite (B : ℕ) : Finite (TriangulationClass B) :=
271 Quotient.finite _
272
273instance (B : ℕ) : Finite (TriangulationClass B) := triangulationClass_finite B
274
275/-- The number of distinct classes is bounded by the labeled count. -/
276theorem classCount_le_labeledCount (B : ℕ) :
277 Nat.card (TriangulationClass B) ≤ Nat.card (BoundedComplex B) :=
278 Nat.card_le_card_of_surjective (Quotient.mk (relabelSetoid B))
279 (fun q => Quotient.exists_rep q)
280
281/-- The labeled count agrees with the `Fintype` cardinal. -/
282theorem labeledCount_eq_card (B : ℕ) :
283 Nat.card (BoundedComplex B) = Fintype.card (BoundedComplex B) :=
284 Nat.card_eq_fintype_card
285
286/-! ## §4. The automorphism group and the measure μ -/
287
288/-- The automorphism group of a labeled complex: relabelings of `K` onto
289itself. -/
290abbrev Aut {B : ℕ} (K : BoundedComplex B) := Relabel K K
291
292instance {B : ℕ} (K : BoundedComplex B) : Nonempty (Aut K) :=
293 ⟨Relabel.refl K⟩
294
295/-- **THEOREM.** The automorphism group is finite (inject into the finite
296triple of index permutations). -/
297instance instFiniteAut {B : ℕ} (K : BoundedComplex B) : Finite (Aut K) :=
298 Finite.of_injective _ (Relabel.toEquivTriple_injective (K := K) (K' := K))
299
300/-- The automorphism count is positive (the identity is an automorphism). -/
301theorem autCard_pos {B : ℕ} (K : BoundedComplex B) : 0 < Nat.card (Aut K) :=
302 Nat.card_pos
303
304/-- The path-sum measure: the standard `1/|Aut|` symmetry factor of each
305labeled configuration. (MODEL: uniform convention; a substrate-derived
306nonuniform measure is OPEN, see `pathSumMeasureStatus`.) -/
307noncomputable def mu {B : ℕ} (K : BoundedComplex B) : ℝ :=
308 1 / (Nat.card (Aut K) : ℝ)
309
310/-- **THEOREM.** 0 < μ(K). -/
311theorem mu_pos {B : ℕ} (K : BoundedComplex B) : 0 < mu K := by
312 unfold mu
313 have h : (0 : ℝ) < (Nat.card (Aut K) : ℝ) := by
314 exact_mod_cast autCard_pos K
315 exact div_pos one_pos h
316
317/-- **THEOREM.** μ(K) ≤ 1 (since |Aut K| ≥ 1). -/
318theorem mu_le_one {B : ℕ} (K : BoundedComplex B) : mu K ≤ 1 := by
319 unfold mu
320 have h : (0 : ℝ) < (Nat.card (Aut K) : ℝ) := by
321 exact_mod_cast autCard_pos K
322 rw [div_le_one h]
323 exact_mod_cast autCard_pos K
324
325/-- Conjugation by a relabeling: automorphism groups of equivalent complexes
326are in bijection. -/
327def Relabel.autCongr {B : ℕ} {K K' : BoundedComplex B} (r : Relabel K K') :
328 Aut K ≃ Aut K' where
329 toFun a := (r.symm.trans a).trans r
330 invFun b := (r.trans b).trans r.symm
331 left_inv a := by
332 apply Relabel.ext <;>
333 · apply Equiv.ext
334 intro x
335 simp only [Relabel.trans_vEquiv, Relabel.trans_eEquiv, Relabel.trans_tEquiv,
336 Relabel.symm_vEquiv, Relabel.symm_eEquiv, Relabel.symm_tEquiv,
337 Equiv.trans_apply, Equiv.symm_apply_apply]
338 right_inv b := by
339 apply Relabel.ext <;>
340 · apply Equiv.ext
341 intro x
342 simp only [Relabel.trans_vEquiv, Relabel.trans_eEquiv, Relabel.trans_tEquiv,
343 Relabel.symm_vEquiv, Relabel.symm_eEquiv, Relabel.symm_tEquiv,
344 Equiv.trans_apply, Equiv.apply_symm_apply]
345
346/-- **THEOREM (measure respects the equivalence).** μ is a relabeling
347invariant: equivalent complexes have equal measure. -/
348theorem mu_congr {B : ℕ} {K K' : BoundedComplex B} (h : Equivalent K K') :
349 mu K = mu K' := by
350 obtain ⟨r⟩ := h
351 unfold mu
352 rw [Nat.card_congr r.autCongr]
353
354/-! ## §5. The path sum Z and its bounds
355
356CONVENTION: `Z` is the sum over the LABELED scoped class with the `1/|Aut|`
357symmetry factor (the standard discrete-gravity convention); `mu_congr` and
358`Z_relabel_invariant` establish compatibility with the quotient view. -/
359
360/-- The recognition path sum over the scoped class: a finite sum, hence
361well-defined with no convergence hypothesis. -/
362noncomputable def Z (B : ℕ) (w : BoundedComplex B → ℂ) : ℂ :=
363 ∑ K : BoundedComplex B, (mu K : ℂ) * w K
364
365/-- **THEOREM (μ-weighted modulus bound).** For any weight of modulus at
366most 1, `‖Z‖` is bounded by the total measure. -/
367theorem Z_norm_le_muSum (B : ℕ) (w : BoundedComplex B → ℂ)
368 (hw : ∀ K, ‖w K‖ ≤ 1) :
369 ‖Z B w‖ ≤ ∑ K : BoundedComplex B, mu K := by
370 unfold Z
371 calc ‖∑ K : BoundedComplex B, (mu K : ℂ) * w K‖
372 ≤ ∑ K : BoundedComplex B, ‖(mu K : ℂ) * w K‖ := norm_sum_le _ _
373 _ ≤ ∑ K : BoundedComplex B, mu K := by
374 refine Finset.sum_le_sum fun K _ => ?_
375 rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (mu_pos K)]
376 exact mul_le_of_le_one_right (le_of_lt (mu_pos K)) (hw K)
377
378/-- **THEOREM (UV-finiteness bound).** For any weight of modulus at most 1,
379`‖Z‖ ≤ card (BoundedComplex B)`: the path sum is finite with an explicit
380proved bound, replacing the assumed `growthBase^N` count. -/
381theorem Z_norm_le_card (B : ℕ) (w : BoundedComplex B → ℂ)
382 (hw : ∀ K, ‖w K‖ ≤ 1) :
383 ‖Z B w‖ ≤ (Fintype.card (BoundedComplex B) : ℝ) := by
384 unfold Z
385 calc ‖∑ K : BoundedComplex B, (mu K : ℂ) * w K‖
386 ≤ ∑ K : BoundedComplex B, ‖(mu K : ℂ) * w K‖ := norm_sum_le _ _
387 _ ≤ ∑ _K : BoundedComplex B, (1 : ℝ) := by
388 refine Finset.sum_le_sum fun K _ => ?_
389 rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (mu_pos K)]
390 calc mu K * ‖w K‖
391 ≤ 1 * 1 := mul_le_mul (mu_le_one K) (hw K) (norm_nonneg _) zero_le_one
392 _ = 1 := one_mul 1
393 _ = (Fintype.card (BoundedComplex B) : ℝ) := by
394 rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one]
395
396/-- **THEOREM (invariance).** For ANY weight `w` and any bijection `σ` of
397configurations that maps each complex to an equivalent one, replacing `w`
398by `w ∘ σ` leaves `Z` unchanged: the `1/|Aut|` measure respects the
399relabeling equivalence. (Uses `mu_congr`; no invariance of `w` needed.) -/
400theorem Z_relabel_invariant (B : ℕ) (w : BoundedComplex B → ℂ)
401 (σ : BoundedComplex B ≃ BoundedComplex B)
402 (hσ : ∀ K, Equivalent K (σ K)) :
403 Z B (fun K => w (σ K)) = Z B w := by
404 unfold Z
405 calc ∑ K : BoundedComplex B, (mu K : ℂ) * w (σ K)
406 = ∑ K : BoundedComplex B, (mu (σ K) : ℂ) * w (σ K) := by
407 refine Finset.sum_congr rfl fun K _ => ?_
408 rw [mu_congr (hσ K)]
409 _ = ∑ K : BoundedComplex B, (mu K : ℂ) * w K :=
410 Fintype.sum_equiv σ _ _ (fun _ => rfl)
411
412/-- **THEOREM (class functions).** If the weight is relabeling-invariant,
413the summand μ·w is constant on equivalence classes, so `Z` descends to the
414finite quotient `TriangulationClass B`. -/
415theorem summand_class_constant (B : ℕ) (w : BoundedComplex B → ℂ)
416 (hinv : ∀ K K', Equivalent K K' → w K = w K')
417 {K K' : BoundedComplex B} (h : Equivalent K K') :
418 (mu K : ℂ) * w K = (mu K' : ℂ) * w K' := by
419 rw [mu_congr h, hinv K K' h]
420
421/-! ## §6. The unitary instance: the honest Z_RS statement -/
422
423/-- The unitary path-sum weight `exp(i·S)` for a real action `S`. The
424intended `S` for Z_RS is the sinh recognition action
425(`PathSumUVBound.recognitionAction`) evaluated on the deficit data of the
426complex. -/
427noncomputable def unitaryWeight {B : ℕ} (S : BoundedComplex B → ℝ) :
428 BoundedComplex B → ℂ :=
429 fun K => Complex.exp (Complex.I * (S K : ℂ))
430
431/-- **THEOREM.** The unitary weight has modulus exactly 1. -/
432theorem unitaryWeight_norm {B : ℕ} (S : BoundedComplex B → ℝ)
433 (K : BoundedComplex B) : ‖unitaryWeight S K‖ = 1 :=
434 Complex.norm_exp_I_mul_ofReal (S K)
435
436/-- **THEOREM (Z_RS on the scoped class).** For an arbitrary real action
437`S` with an explicit relabeling-invariance hypothesis `hS`, the unitary
438path sum `Z_RS = Σ_K (1/|Aut K|)·exp(i·S K)`:
4391. has unit-modulus weights,
4402. is relabeling-invariant as a weight,
4413. satisfies the proved UV-finiteness bound `‖Z_RS‖ ≤ card`,
4424. is unchanged under any equivalence-preserving reindexing of the
443 configuration class. -/
444theorem zRS_scoped_wellDefined (B : ℕ) (S : BoundedComplex B → ℝ)
445 (hS : ∀ K K', Equivalent K K' → S K = S K') :
446 (∀ K, ‖unitaryWeight S K‖ = 1) ∧
447 (∀ K K', Equivalent K K' → unitaryWeight S K = unitaryWeight S K') ∧
448 ‖Z B (unitaryWeight S)‖ ≤ (Fintype.card (BoundedComplex B) : ℝ) ∧
449 (∀ σ : BoundedComplex B ≃ BoundedComplex B, (∀ K, Equivalent K (σ K)) →
450 Z B (fun K => unitaryWeight S (σ K)) = Z B (unitaryWeight S)) := by
451 refine ⟨unitaryWeight_norm S, ?_, ?_, ?_⟩
452 · intro K K' h
453 unfold unitaryWeight
454 rw [hS K K' h]
455 · exact Z_norm_le_card B _ (fun K => le_of_eq (unitaryWeight_norm S K))
456 · exact fun σ hσ => Z_relabel_invariant B (unitaryWeight S) σ hσ
457
458/-! ## §7. Replacing the assumed growthBase field -/
459
460/-- The admissible family whose count data is now PROVED: `growthBase` is
461the actual `Fintype` cardinal of the scoped class (a derived quantity), not
462an assumed exponential base. `minMesh := 1` is the fixed lattice unit of
463the scoped class. -/
464noncomputable def provedFamily (B : ℕ) : PathSumUVBound.AdmissibleTriangulationFamily where
465 maxSimplexCount := B + 1
466 maxSimplexCount_pos := Nat.succ_pos B
467 growthBase := (Fintype.card (BoundedComplex B) : ℝ)
468 growthBase_pos := by exact_mod_cast boundedComplex_card_pos B
469 minMesh := 1
470 minMesh_pos := one_pos
471
472/-- The growth base of the proved family is the derived cardinal. -/
473theorem provedFamily_growthBase_derived (B : ℕ) :
474 (provedFamily B).growthBase = (Fintype.card (BoundedComplex B) : ℝ) := rfl
475
476/-- **THEOREM (bridge).** The proved count is within the structural bound
477of `PathSumUVBound.triangulationCountBound` for the proved family: the
478assumed-count interface is satisfiable with derived data. -/
479theorem proved_count_le_structural_bound (B : ℕ) :
480 (Fintype.card (BoundedComplex B) : ℝ) ≤
481 PathSumUVBound.triangulationCountBound (provedFamily B) := by
482 unfold PathSumUVBound.triangulationCountBound
483 show (Fintype.card (BoundedComplex B) : ℝ) ≤
484 (Fintype.card (BoundedComplex B) : ℝ) ^ (B + 1)
485 have h1 : (1 : ℝ) ≤ (Fintype.card (BoundedComplex B) : ℝ) := by
486 exact_mod_cast boundedComplex_card_pos B
487 exact le_self_pow₀ h1 (Nat.succ_ne_zero B)
488
489/-! ## §8. Status ledger -/
490
491/-- What is proved and what remains open in this gap. All flags are
492rfl-forced below; no `: True` fields. -/
493structure GapStatus where
494 count_finite_proved : Bool
495 quotient_finite_proved : Bool
496 measure_defined : Bool
497 measure_positive_proved : Bool
498 modulus_bound_proved : Bool
499 relabel_invariance_proved : Bool
500 continuum_limit_derived : Bool
501 substrate_measure_derived : Bool
502
503/-- Status of the path-sum-measure gap after this module. -/
504def pathSumMeasureStatus : GapStatus where
505 count_finite_proved := true
506 quotient_finite_proved := true
507 measure_defined := true
508 measure_positive_proved := true
509 modulus_bound_proved := true
510 relabel_invariance_proved := true
511 continuum_limit_derived := false
512 substrate_measure_derived := false
513
514theorem status_count_finite : pathSumMeasureStatus.count_finite_proved = true := rfl
515theorem status_quotient_finite : pathSumMeasureStatus.quotient_finite_proved = true := rfl
516theorem status_measure_defined : pathSumMeasureStatus.measure_defined = true := rfl
517theorem status_measure_positive : pathSumMeasureStatus.measure_positive_proved = true := rfl
518theorem status_modulus_bound : pathSumMeasureStatus.modulus_bound_proved = true := rfl
519theorem status_relabel_invariance : pathSumMeasureStatus.relabel_invariance_proved = true := rfl
520/-- OPEN: the continuum limit of `Z B` as `B → ∞` is not derived here. -/
521theorem status_continuum_open : pathSumMeasureStatus.continuum_limit_derived = false := rfl
522/-- OPEN: a substrate-derived nonuniform measure is not derived here. -/
523theorem status_substrate_measure_open :
524 pathSumMeasureStatus.substrate_measure_derived = false := rfl
525
526end PathSumMeasure
527end SevenGaps
528end Gravity
529end IndisputableMonolith
530