IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugePreflight
IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugePreflight.lean · 400 lines · 34 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure
2
3/-!
4# Seven Gaps, gauge preflight: DERIVING the 1/|Aut| measure from gauge counting
5
6## What this module does
7
8`PathSumMeasure` POSTULATES the symmetry-factor measure `mu K = 1/|Aut K|`
9(standard discrete-gravity convention). This module DERIVES that measure
10from pure gauge counting, with a definition of the gauge mass that never
11mentions `mu` or `Aut`:
12
13* `gaugeOrbitCard K` = number of labeled complexes equivalent to `K`
14 (the size of `K`'s relabeling orbit inside the bounded universe).
15* `pairCount K` = number of pairs `(K', r)` with `K'` in the orbit of
16 `K` and `r : Relabel K K'` a concrete gauge witness (the gauge volume of
17 the orbit). DEFINITION mentions only `Equivalent` and `Relabel`.
18* `gaugeOrbitMass c` = `orbitCard c / pairCount c` on the quotient
19 `TriangulationClass B`: labeled copies per unit of gauge volume.
20 DEFINITION mentions only the two counting quantities above.
21
22## Status tiers (honest tagging)
23
24**THEOREM (proved below, 0 sorry, 0 new axioms):**
25* Torsor/orbit-stabilizer (`torsorEquiv`, `relabelingCount_eq_autCard`):
26 for equivalent `K K'`, the relabeling witnesses `Relabel K K'` are a
27 torsor over `Aut K`, so `|Relabel K K'| = |Aut K|`; hence the total
28 `(copy, witness)` pair count factorizes as
29 `pairCount K = gaugeOrbitCard K * |Aut K|`
30 (`pairCount_eq_orbitCard_mul_autCard`).
31* Representative independence (`gaugeOrbitCard_congr`, `pairCount_congr`,
32 `gaugeMassRep_congr`): the counting quantities are class functions, so
33 the quotient lifts `orbitCardClass`/`pairCountClass`/`gaugeOrbitMass`
34 are well-defined.
35* **The derivation** (`gaugeOrbitMass_eq_mu`): the counting-defined mass
36 of the class of `K` equals `mu K = 1/|Aut K|`. GIVEN the pair-counting
37 principle (the MODEL premise below), the `1/|Aut|` factor follows from
38 orbit-stabilizer; what is put in by hand is the choice that gauge
39 volume equals the `(copy, witness)` pair count (a per-labeled-copy
40 principle would give the quotient-uniform measure instead).
41* Existence + uniqueness (`gaugeOrbitMass_mul_pairCount`,
42 `gaugeCountingMass_unique`): `gaugeOrbitMass` satisfies the counting
43 property `ν c * pairCount c = orbitCard c`, and any class mass `ν`
44 satisfying it equals `gaugeOrbitMass`. The counting principle pins
45 the measure.
46* Path-sum corollary (`labeledZ_eq_orbitWeighted_classSum`): for a
47 relabeling-invariant weight, the labeled path sum `Z` equals the
48 class sum `Σ_c orbitCard c * gaugeOrbitMass c * w(rep c)`.
49
50**MODEL (the named premise, now explicit instead of hidden):**
51* The COUNTING PRINCIPLE itself: uniform gauge density on labeled
52 representatives (each `(copy, witness)` pair carries equal weight, and
53 the physical mass of a class is labeled copies divided by gauge
54 volume). This module derives `1/|Aut|` FROM that principle; it does
55 NOT derive the principle from the ledger. That residue is recorded in
56 `gaugePreflightStatus.counting_principle_derived_from_ledger = false`.
57
58## Kill-condition audit (panel live-bet 1)
59
60The bet survives: `pairCount` and `gaugeOrbitMass` are DEFINED without
61reference to `mu` or `Aut` (only `Equivalent`, `Relabel`, and `Nat.card`);
62`Aut` appears exclusively in THEOREM statements/proofs relating the
63counting quantities to the postulated measure. The pair-count route did
64not collapse to a definitional restatement.
65
66## Ledger note
67
68The decision to flip any `FullTheoryLedger` flag on the strength of this
69derivation belongs to the CONDUCTOR; this module mutates no ledger.
70
71## Proof notes
72* No `decide`/`native_decide`; cardinalities are never computed
73 numerically.
74* Groupoid data (`Relabel.refl/symm/trans`) is REUSED from
75 `PathSumMeasure`, not redefined; the two cancellation laws needed for
76 the torsor are proved pointwise inside `torsorEquiv`.
77-/
78
79namespace IndisputableMonolith
80namespace Gravity
81namespace SevenGaps
82namespace ExactShellGaugePreflight
83
84open PathSumMeasure
85
86variable {B : ℕ}
87
88/-! ## §1. The gauge groupoid (T1)
89
90Identity, inverse, and composition of relabelings already exist in
91`PathSumMeasure` (`Relabel.refl`, `Relabel.symm`, `Relabel.trans`) with the
92setoid `relabelSetoid` proving they implement a genuine equivalence. We
93add only the equivalence-relation restatements used below. -/
94
95/-- Reflexivity of the gauge relation (identity relabeling). -/
96theorem equivalent_refl (K : BoundedComplex B) : Equivalent K K :=
97 ⟨Relabel.refl K⟩
98
99/-- Symmetry of the gauge relation (inverse relabeling). -/
100theorem equivalent_symm {K K' : BoundedComplex B} (h : Equivalent K K') :
101 Equivalent K' K :=
102 h.elim fun r => ⟨r.symm⟩
103
104/-- Transitivity of the gauge relation (composite relabeling). -/
105theorem equivalent_trans {K₁ K₂ K₃ : BoundedComplex B}
106 (h₁ : Equivalent K₁ K₂) (h₂ : Equivalent K₂ K₃) : Equivalent K₁ K₃ :=
107 h₁.elim fun r => h₂.elim fun s => ⟨r.trans s⟩
108
109/-- **THEOREM.** The relabeling witnesses between ANY two bounded complexes
110form a finite type (inject into the finite triple of index bijections;
111generalizes `PathSumMeasure.instFiniteAut` beyond the diagonal). -/
112instance instFiniteRelabel (K K' : BoundedComplex B) : Finite (Relabel K K') :=
113 Finite.of_injective _ (Relabel.toEquivTriple_injective (K := K) (K' := K'))
114
115/-! ## §2. Gauge counting quantities (T2)
116
117Both are pure counts: neither definition mentions `mu` or `Aut`. -/
118
119/-- The size of `K`'s relabeling orbit inside the bounded universe: the
120number of labeled complexes gauge-equivalent to `K`. Finite because the
121universe `BoundedComplex B` is a `Fintype`. -/
122noncomputable def gaugeOrbitCard (K : BoundedComplex B) : ℕ :=
123 Nat.card {K' : BoundedComplex B // Equivalent K K'}
124
125/-- The number of relabeling witnesses from `K` to `K'`. -/
126noncomputable def relabelingCount (K K' : BoundedComplex B) : ℕ :=
127 Nat.card (Relabel K K')
128
129/-- The gauge volume of `K`'s orbit: the total number of pairs `(K', r)`
130where `K'` is a labeled complex in the orbit of `K` and `r` is a concrete
131relabeling witness `K → K'`. DEFINITION mentions only `Equivalent` and
132`Relabel` (pure counting; no `mu`, no `Aut`). -/
133noncomputable def pairCount (K : BoundedComplex B) : ℕ :=
134 Nat.card (Σ K' : {K' : BoundedComplex B // Equivalent K K'}, Relabel K K'.val)
135
136/-- The orbit contains `K` itself, so the orbit count is positive. -/
137theorem gaugeOrbitCard_pos (K : BoundedComplex B) : 0 < gaugeOrbitCard K := by
138 haveI : Nonempty {K' : BoundedComplex B // Equivalent K K'} :=
139 ⟨⟨K, equivalent_refl K⟩⟩
140 exact Nat.card_pos
141
142/-! ## §3. Orbit-stabilizer: the load-bearing torsor theorem (T3) -/
143
144/-- **THEOREM (torsor).** Fixing one witness `r0 : Relabel K K'`, the map
145`a ↦ a.trans r0` is a bijection `Aut K ≃ Relabel K K'`: the witnesses
146between equivalent complexes are a torsor over the automorphism group. -/
147def torsorEquiv {K K' : BoundedComplex B} (r0 : Relabel K K') :
148 Aut K ≃ Relabel K K' where
149 toFun a := a.trans r0
150 invFun r := r.trans r0.symm
151 left_inv a := by
152 apply Relabel.ext <;>
153 · apply Equiv.ext
154 intro x
155 simp only [Relabel.trans_vEquiv, Relabel.trans_eEquiv, Relabel.trans_tEquiv,
156 Relabel.symm_vEquiv, Relabel.symm_eEquiv, Relabel.symm_tEquiv,
157 Equiv.trans_apply, Equiv.symm_apply_apply]
158 right_inv r := by
159 apply Relabel.ext <;>
160 · apply Equiv.ext
161 intro x
162 simp only [Relabel.trans_vEquiv, Relabel.trans_eEquiv, Relabel.trans_tEquiv,
163 Relabel.symm_vEquiv, Relabel.symm_eEquiv, Relabel.symm_tEquiv,
164 Equiv.trans_apply, Equiv.apply_symm_apply]
165
166/-- **THEOREM (orbit-stabilizer, cardinal form).** For equivalent
167complexes, the witness count equals the automorphism count. -/
168theorem relabelingCount_eq_autCard {K K' : BoundedComplex B}
169 (h : Equivalent K K') : relabelingCount K K' = Nat.card (Aut K) := by
170 obtain ⟨r0⟩ := h
171 unfold relabelingCount
172 exact (Nat.card_congr (torsorEquiv r0)).symm
173
174/-- **THEOREM (pair-count factorization).** The gauge volume of the orbit
175is the orbit size times the automorphism count: every fiber of the
176projection `(K', r) ↦ K'` is a torsor over `Aut K`. -/
177theorem pairCount_eq_orbitCard_mul_autCard (K : BoundedComplex B) :
178 pairCount K = gaugeOrbitCard K * Nat.card (Aut K) := by
179 have e : (Σ K' : {K' : BoundedComplex B // Equivalent K K'}, Relabel K K'.val)
180 ≃ {K' : BoundedComplex B // Equivalent K K'} × Aut K :=
181 Equiv.sigmaEquivProdOfEquiv fun K' =>
182 (torsorEquiv (Classical.choice K'.property)).symm
183 unfold pairCount gaugeOrbitCard
184 rw [Nat.card_congr e, Nat.card_prod]
185
186/-- The gauge volume is positive (the orbit is nonempty and `Aut` contains
187the identity). -/
188theorem pairCount_pos (K : BoundedComplex B) : 0 < pairCount K := by
189 rw [pairCount_eq_orbitCard_mul_autCard]
190 exact Nat.mul_pos (gaugeOrbitCard_pos K) (autCard_pos K)
191
192/-! ## §4. Representative independence (well-definedness on classes) -/
193
194/-- The orbit count is a class function. -/
195theorem gaugeOrbitCard_congr {K K' : BoundedComplex B} (h : Equivalent K K') :
196 gaugeOrbitCard K = gaugeOrbitCard K' :=
197 Nat.card_congr (Equiv.subtypeEquivRight fun _L =>
198 ⟨fun hK => equivalent_trans (equivalent_symm h) hK,
199 fun hK' => equivalent_trans h hK'⟩)
200
201/-- The automorphism count is a class function (conjugation bijection,
202reusing `PathSumMeasure.Relabel.autCongr`). -/
203theorem autCard_congr {K K' : BoundedComplex B} (h : Equivalent K K') :
204 Nat.card (Aut K) = Nat.card (Aut K') := by
205 obtain ⟨r⟩ := h
206 exact Nat.card_congr r.autCongr
207
208/-- The gauge volume is a class function: `pairCount` is independent of the
209choice of base representative. -/
210theorem pairCount_congr {K K' : BoundedComplex B} (h : Equivalent K K') :
211 pairCount K = pairCount K' := by
212 rw [pairCount_eq_orbitCard_mul_autCard, pairCount_eq_orbitCard_mul_autCard,
213 gaugeOrbitCard_congr h, autCard_congr h]
214
215/-- **LEMMA (well-definedness).** The representative-level counting ratio
216(labeled copies per unit of gauge volume) is independent of the chosen
217representative. -/
218theorem gaugeMassRep_congr {K K' : BoundedComplex B} (h : Equivalent K K') :
219 (gaugeOrbitCard K : ℝ) / (pairCount K : ℝ) =
220 (gaugeOrbitCard K' : ℝ) / (pairCount K' : ℝ) := by
221 rw [gaugeOrbitCard_congr h, pairCount_congr h]
222
223/-! ## §5. The gauge-counting mass on classes (T4) -/
224
225/-- The orbit count as a function of the class. -/
226noncomputable def orbitCardClass (c : TriangulationClass B) : ℕ :=
227 Quotient.liftOn c gaugeOrbitCard fun _ _ h => gaugeOrbitCard_congr h
228
229@[simp] theorem orbitCardClass_mk (K : BoundedComplex B) :
230 orbitCardClass (Quotient.mk (relabelSetoid B) K) = gaugeOrbitCard K := rfl
231
232/-- The gauge volume as a function of the class. -/
233noncomputable def pairCountClass (c : TriangulationClass B) : ℕ :=
234 Quotient.liftOn c pairCount fun _ _ h => pairCount_congr h
235
236@[simp] theorem pairCountClass_mk (K : BoundedComplex B) :
237 pairCountClass (Quotient.mk (relabelSetoid B) K) = pairCount K := rfl
238
239theorem pairCountClass_pos (c : TriangulationClass B) : 0 < pairCountClass c :=
240 Quotient.inductionOn c fun K => pairCount_pos K
241
242/-- **The gauge-counting mass of a class**: labeled copies per unit of
243gauge volume. DEFINITION mentions only the two counting quantities
244(`orbitCardClass`, `pairCountClass`); no `mu`, no `Aut`. This is the
245explicit counting principle: uniform gauge density on labeled
246representatives. -/
247noncomputable def gaugeOrbitMass (c : TriangulationClass B) : ℝ :=
248 (orbitCardClass c : ℝ) / (pairCountClass c : ℝ)
249
250/-- **THEOREM (the derivation).** The counting-defined class mass equals
251the postulated symmetry-factor measure: GIVEN the pair-counting principle,
252`1/|Aut|` follows from orbit-stabilizer (`pairCount = orbitCard * |Aut|`)
253rather than being written into the definition. -/
254theorem gaugeOrbitMass_eq_mu (K : BoundedComplex B) :
255 gaugeOrbitMass (Quotient.mk (relabelSetoid B) K) = mu K := by
256 have ho : (gaugeOrbitCard K : ℝ) ≠ 0 := by
257 exact_mod_cast (gaugeOrbitCard_pos K).ne'
258 unfold gaugeOrbitMass mu
259 rw [orbitCardClass_mk, pairCountClass_mk, pairCount_eq_orbitCard_mul_autCard,
260 Nat.cast_mul, div_mul_eq_div_div, div_self ho]
261
262/-! ## §6. Existence + uniqueness: the counting principle pins the measure (T5) -/
263
264/-- **THEOREM (existence).** `gaugeOrbitMass` itself satisfies the
265normalized gauge-divided counting property; together with
266`gaugeCountingMass_unique` this pins the measure (existence + uniqueness,
267not uniqueness alone). -/
268theorem gaugeOrbitMass_mul_pairCount (c : TriangulationClass B) :
269 gaugeOrbitMass c * (pairCountClass c : ℝ) = (orbitCardClass c : ℝ) := by
270 have hp : (pairCountClass c : ℝ) ≠ 0 := by
271 exact_mod_cast (pairCountClass_pos c).ne'
272 unfold gaugeOrbitMass
273 rw [div_mul_cancel₀ _ hp]
274
275/-- **THEOREM (uniqueness).** Any class-mass assignment satisfying the
276normalized gauge-divided counting property (`ν c * pairCount c =
277orbitCard c` for every class) equals `gaugeOrbitMass`. Given the counting
278principle (the explicit MODEL premise of this module), the measure is
279unique; combined with `gaugeOrbitMass_eq_mu`, it is forced to be
280`1/|Aut|`. -/
281theorem gaugeCountingMass_unique (ν : TriangulationClass B → ℝ)
282 (hν : ∀ c, ν c * (pairCountClass c : ℝ) = (orbitCardClass c : ℝ))
283 (c : TriangulationClass B) : ν c = gaugeOrbitMass c := by
284 have hp : (pairCountClass c : ℝ) ≠ 0 := by
285 exact_mod_cast (pairCountClass_pos c).ne'
286 unfold gaugeOrbitMass
287 rw [eq_div_iff hp]
288 exact hν c
289
290/-! ## §7. Path-sum corollary: labeled Z as an orbit-weighted class sum (T6) -/
291
292/-- Noncomputable enumeration of the finite class quotient (needed only to
293STATE the class sum; `triangulationClass_finite` supplies finiteness). -/
294noncomputable instance instFintypeTriangulationClass (B : ℕ) :
295 Fintype (TriangulationClass B) :=
296 Fintype.ofFinite _
297
298/-- **THEOREM (diagnostic fragment).** For a relabeling-invariant weight,
299the labeled path sum with the `1/|Aut|` measure equals the class sum
300weighted by orbit size times the COUNTING-DERIVED mass:
301`Z = Σ_c orbitCard c * gaugeOrbitMass c * w(rep c)`.
302The measure in `Z` is now carried entirely by counting data. -/
303theorem labeledZ_eq_orbitWeighted_classSum (B : ℕ) (w : BoundedComplex B → ℂ)
304 (hinv : ∀ K K', Equivalent K K' → w K = w K') :
305 Z B w = ∑ c : TriangulationClass B,
306 (orbitCardClass c : ℂ) * (gaugeOrbitMass c : ℂ) * w (Quotient.out c) := by
307 classical
308 unfold Z
309 rw [← Fintype.sum_fiberwise
310 (fun K : BoundedComplex B => Quotient.mk (relabelSetoid B) K)
311 (fun K : BoundedComplex B => (mu K : ℂ) * w K)]
312 refine Finset.sum_congr rfl fun c _ => ?_
313 have hc : Quotient.mk (relabelSetoid B) (Quotient.out c) = c := Quotient.out_eq c
314 have hmem : ∀ K : {K : BoundedComplex B // Quotient.mk (relabelSetoid B) K = c},
315 Equivalent (Quotient.out c) K.val := fun K =>
316 Quotient.exact (hc.trans K.property.symm)
317 have hmass : gaugeOrbitMass c = mu (Quotient.out c) := by
318 conv_lhs => rw [← hc]
319 exact gaugeOrbitMass_eq_mu (Quotient.out c)
320 have e : {K : BoundedComplex B // Quotient.mk (relabelSetoid B) K = c}
321 ≃ {K' : BoundedComplex B // Equivalent (Quotient.out c) K'} :=
322 Equiv.subtypeEquivRight fun K =>
323 ⟨fun hK => Quotient.exact (hc.trans hK.symm),
324 fun hE => by
325 have h1 : Quotient.mk (relabelSetoid B) (Quotient.out c)
326 = Quotient.mk (relabelSetoid B) K := Quotient.sound hE
327 exact h1.symm.trans hc⟩
328 have hcard : Fintype.card {K : BoundedComplex B // Quotient.mk (relabelSetoid B) K = c}
329 = orbitCardClass c := by
330 rw [Fintype.card_eq_nat_card, Nat.card_congr e]
331 conv_rhs => rw [← hc]
332 rfl
333 calc ∑ K : {K : BoundedComplex B // Quotient.mk (relabelSetoid B) K = c},
334 (mu K.val : ℂ) * w K.val
335 = ∑ _K : {K : BoundedComplex B // Quotient.mk (relabelSetoid B) K = c},
336 (mu (Quotient.out c) : ℂ) * w (Quotient.out c) :=
337 Finset.sum_congr rfl fun K _ =>
338 (summand_class_constant B w hinv (hmem K)).symm
339 _ = (Fintype.card {K : BoundedComplex B // Quotient.mk (relabelSetoid B) K = c} : ℂ) *
340 ((mu (Quotient.out c) : ℂ) * w (Quotient.out c)) := by
341 rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
342 _ = (orbitCardClass c : ℂ) * (gaugeOrbitMass c : ℂ) * w (Quotient.out c) := by
343 rw [hcard, hmass, mul_assoc]
344
345/-! ## §8. Status ledger (T7)
346
347All `true` flags are rfl-forced and grounded by `gaugePreflight_grounded`;
348the `false` flag names the explicit residue. The `FullTheoryLedger` flag
349decision belongs to the conductor; nothing here mutates it. -/
350
351/-- What is proved and what remains the named premise in this module. -/
352structure GaugePreflightStatus where
353 gauge_torsor_proved : Bool
354 measure_derived_from_counting : Bool
355 uniqueness_proved : Bool
356 counting_principle_derived_from_ledger : Bool
357
358/-- Status after this module: the torsor, the derivation, and uniqueness
359are theorems; the uniform-gauge-density counting principle is the explicit
360MODEL premise, not derived from the ledger. -/
361def gaugePreflightStatus : GaugePreflightStatus where
362 gauge_torsor_proved := true
363 measure_derived_from_counting := true
364 uniqueness_proved := true
365 counting_principle_derived_from_ledger := false
366
367theorem status_gauge_torsor :
368 gaugePreflightStatus.gauge_torsor_proved = true := rfl
369theorem status_measure_derived :
370 gaugePreflightStatus.measure_derived_from_counting = true := rfl
371theorem status_uniqueness :
372 gaugePreflightStatus.uniqueness_proved = true := rfl
373/-- OPEN residue: the counting principle itself (uniform gauge density on
374labeled representatives) is the named premise, not a ledger theorem. -/
375theorem status_counting_principle_open :
376 gaugePreflightStatus.counting_principle_derived_from_ledger = false := rfl
377
378/-- **Grounding theorem.** The status flags are backed by the actual
379theorems: orbit-stabilizer, pair-count factorization, the derivation
380`gaugeOrbitMass = mu`, and uniqueness. -/
381theorem gaugePreflight_grounded (B : ℕ) :
382 (∀ K K' : BoundedComplex B, Equivalent K K' →
383 relabelingCount K K' = Nat.card (Aut K)) ∧
384 (∀ K : BoundedComplex B,
385 pairCount K = gaugeOrbitCard K * Nat.card (Aut K)) ∧
386 (∀ K : BoundedComplex B,
387 gaugeOrbitMass (Quotient.mk (relabelSetoid B) K) = mu K) ∧
388 (∀ ν : TriangulationClass B → ℝ,
389 (∀ c, ν c * (pairCountClass c : ℝ) = (orbitCardClass c : ℝ)) →
390 ∀ c, ν c = gaugeOrbitMass c) :=
391 ⟨fun _ _ h => relabelingCount_eq_autCard h,
392 pairCount_eq_orbitCard_mul_autCard,
393 gaugeOrbitMass_eq_mu,
394 gaugeCountingMass_unique⟩
395
396end ExactShellGaugePreflight
397end SevenGaps
398end Gravity
399end IndisputableMonolith
400