IndisputableMonolith.Gravity.SevenGaps.ClassPushforward

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure
   3
   4/-!
   5# Seven Gaps, Crux-2 (pillar 2, path-sum): the class pushforward of Z
   6
   7## Protocol: QUOTIENT_BOOKKEEPING (panel-locked).
   8
   9## Status tiers (honest tagging)
  10
  11**THEOREM (proved below, 0 sorry, 0 new axioms):**
  12* `FiniteQuotient.sum_fiberwise_quotient` and
  13  `FiniteQuotient.sum_eq_quotient_sum_classMass`: for a `Fintype α`, a
  14  `Setoid α`, and any `AddCommMonoid`-valued function, the finite sum over
  15  `α` decomposes over the fibers of the quotient map; when the function is
  16  constant on classes the fiber sum collapses to
  17  `fiberCard q • f (rep q)`.  Generic; no group action anywhere.
  18  Decidability of the quotient is supplied classically (this is
  19  noncomputable measure bookkeeping, not computation).
  20* `PathSum.classMass`: for `q : TriangulationClass B`,
  21  `classMass q = Σ_{K : ⟦K⟧ = q} μ(K)`, and
  22  `PathSum.Z_eq_classPushforward`: for any weight `w` constant on classes
  23  (explicit hypothesis `hw`), `Z B w = Σ_q classMass(q) · w(rep q)`.
  24  NOTE (what `classMass` IS and IS NOT): by
  25  `PathSum.classMass_eq_fiberCard_mul_mu`,
  26  `classMass q = |fiber(q)| · (1/|Aut(rep q)|)`.  It is NOT `1/|Aut|` per
  27  class: the labeled fiber cardinality multiplies the symmetry factor.
  28* **FORK VERDICT (C1 landmine DETONATED as a kernel fact):**
  29  `PathSum.exists_nonSingleton_fiber` exhibits, at `B = 2`, two DISTINCT
  30  labeled complexes (`edgeAB` with edge `(0,1)`, `edgeBA` with edge
  31  `(1,0)`) related by an explicit vertex-swap relabeling
  32  (`edgeSwapRelabel`), and `PathSum.one_lt_fiberCard_edgeClass` shows the
  33  corresponding quotient fiber has cardinality `> 1`.  The numeric
  34  separation is itself a THEOREM: `PathSum.mu_lt_classMass_edgeClass`
  35  proves `μ(edgeAB) < classMass(⟦edgeAB⟧)`, so (kernel fact, not prose)
  36  the class decomposition of the standing `Z` of `PathSumMeasure` carries
  37  the weight `|fiber| · (1/|Aut|)` per class and differs from the
  38  inequivalent-class sum with weights `1/|Aut|` already at `B = 2`.
  39  SCOPE OF THE DETONATION: this concerns `PathSum.Z`, the LABELED sum of
  40  `PathSumMeasure`, ONLY.  It does not apply to the exact-shell
  41  `Z_RS_uv` of the `ExactShellGaugeUV` wave, which is defined in the
  42  quotient-sum convention per its own header; the two are different
  43  conventions, not a contradiction.
  44
  45**MODEL / NEXT WAVE (recorded, not claimed):**
  46* The quotient-first object (a path sum defined directly on
  47  `TriangulationClass B` with per-class `1/|Aut|` weights, and its
  48  relation to the labeled `Z` via orbit counting) is PROMOTED to the next
  49  wave; it is not constructed here.
  50
  51**OPEN (flags stay RED; nothing here changes them):**
  52* `Z_RS_continuum_limit` : RED.  No continuum-limit or "prepares
  53  convergence" claim is made anywhere in this module.
  54* `substrate_measure_derived` : RED.  The `1/|Aut|` convention is a MODEL
  55  input; no derivation from invariance + normalization is attempted.
  56* `gap1_bridge_derived` : RED.
  57
  58## Proof notes
  59* Classical decidability instances are used for quotient `Finset`s
  60  (noncomputable, honest); no `decide` / `native_decide` anywhere in this
  61  module; no numerical cardinality evaluation, only structure.
  62* All undischarged premises are explicit hypothesis parameters (`hw`).
  63-/
  64
  65namespace IndisputableMonolith
  66namespace Gravity
  67namespace SevenGaps
  68
  69open PathSumMeasure
  70
  71/-! ## §1. Generic finite-quotient fiber decomposition (T1)
  72
  73No `MulAction`, no group anywhere: a `Fintype`, a `Setoid`, and finite-sum
  74bookkeeping over the fibers of the quotient map. -/
  75
  76namespace FiniteQuotient
  77
  78/-- A quotient of a finite type is a finite type (noncomputable via
  79classical choice; fine for measure bookkeeping).  SCOPED so downstream
  80files do not silently pick it up; activate with `open FiniteQuotient`. -/
  81noncomputable scoped instance instFintypeQuotient {α : Type*} [Fintype α]
  82    (s : Setoid α) : Fintype (Quotient s) :=
  83  Fintype.ofFinite _
  84
  85/-- Classical decidability of quotient equality (low priority so any real
  86decidable instance wins; honest noncomputable bookkeeping, never used for
  87computation).  SCOPED so downstream files do not silently pick it up;
  88activate with `open FiniteQuotient`. -/
  89noncomputable scoped instance (priority := 10) instDecEqQuotient {α : Type*}
  90    (s : Setoid α) : DecidableEq (Quotient s) :=
  91  Classical.decEq _
  92
  93/-- The labeled fiber of a quotient class: all elements of `α` mapping to
  94`q` under the quotient map.  Decidability is classical (noncomputable
  95bookkeeping). -/
  96noncomputable def classFiber {α : Type*} [Fintype α] (s : Setoid α)
  97    (q : Quotient s) : Finset α :=
  98  Finset.univ.filter (fun a => Quotient.mk s a = q)
  99
 100/-- Membership in the fiber is exactly quotient-map equality. -/
 101theorem mem_classFiber {α : Type*} [Fintype α] (s : Setoid α)
 102    (q : Quotient s) (a : α) :
 103    a ∈ classFiber s q ↔ Quotient.mk s a = q := by
 104  unfold classFiber
 105  rw [Finset.mem_filter]
 106  simp only [Finset.mem_univ, true_and]
 107
 108/-- The labeled cardinality of a quotient fiber. -/
 109noncomputable def fiberCard {α : Type*} [Fintype α] (s : Setoid α)
 110    (q : Quotient s) : ℕ :=
 111  (classFiber s q).card
 112
 113/-- **THEOREM (T1, fiber decomposition).**  A finite sum over a `Fintype`
 114decomposes over the fibers of any quotient map:
 115`Σ_{a : α} g a = Σ_{q : Quotient s} Σ_{a ∈ fiber q} g a`.
 116Generic (`AddCommMonoid` values); proved via `Finset.sum_fiberwise`. -/
 117theorem sum_fiberwise_quotient {α : Type*} [Fintype α] (s : Setoid α)
 118    {M : Type*} [AddCommMonoid M] (g : α → M) :
 119    ∑ a : α, g a = ∑ q : Quotient s, ∑ a ∈ classFiber s q, g a := by
 120  classical
 121  rw [← Finset.sum_fiberwise Finset.univ (Quotient.mk s) g]
 122  refine Finset.sum_congr rfl fun q _ => Finset.sum_congr ?_ fun a _ => rfl
 123  ext a
 124  simp only [Finset.mem_filter, Finset.mem_univ, true_and, mem_classFiber]
 125
 126/-- **THEOREM (T1, class-constant collapse).**  If `f` is constant on
 127classes (mk-equality hypothesis), the fiber sum collapses:
 128`Σ_{a : α} f a = Σ_{q} fiberCard(q) • f (rep q)` where `rep q = q.out`. -/
 129theorem sum_eq_quotient_sum_classMass {α : Type*} [Fintype α] (s : Setoid α)
 130    {M : Type*} [AddCommMonoid M] (f : α → M)
 131    (hf : ∀ a b, Quotient.mk s a = Quotient.mk s b → f a = f b) :
 132    ∑ a : α, f a = ∑ q : Quotient s, fiberCard s q • f (Quotient.out q) := by
 133  rw [sum_fiberwise_quotient s f]
 134  refine Finset.sum_congr rfl fun q _ => ?_
 135  have hconst : ∀ a ∈ classFiber s q, f a = f (Quotient.out q) := by
 136    intro a ha
 137    exact hf a (Quotient.out q)
 138      (((mem_classFiber s q a).mp ha).trans (Quotient.out_eq q).symm)
 139  rw [Finset.sum_congr rfl hconst, Finset.sum_const]
 140  rfl
 141
 142end FiniteQuotient
 143
 144/-! ## §2. The class pushforward of the labeled path sum (T2, T3) -/
 145
 146namespace PathSum
 147
 148open FiniteQuotient
 149
 150/-- Bridge: quotient-map equality yields a relabeling equivalence
 151(`Quotient.exact` specialized to `relabelSetoid`). -/
 152theorem equivalent_of_mk_eq {B : ℕ} {K K' : BoundedComplex B}
 153    (h : Quotient.mk (relabelSetoid B) K = Quotient.mk (relabelSetoid B) K') :
 154    Equivalent K K' :=
 155  Quotient.exact h
 156
 157/-- **T2 (definition).**  The pushforward mass of a triangulation class:
 158the sum of the labeled measure `μ` over the labeled fiber of the class.
 159WHAT THIS IS: `classMass q = |fiber(q)| · (1/|Aut(rep q)|)`
 160(`classMass_eq_fiberCard_mul_mu` below).  WHAT THIS IS NOT: it is NOT the
 161per-class weight `1/|Aut|`; the labeled fiber cardinality multiplies in. -/
 162noncomputable def classMass {B : ℕ} (q : TriangulationClass B) : ℝ :=
 163  ∑ K ∈ classFiber (relabelSetoid B) q, mu K
 164
 165/-- **T3 (the fork detector, identity form).**  The pushforward class mass
 166is the labeled fiber cardinality times the symmetry factor of the class
 167representative: `classMass q = |fiber(q)| · μ(rep q)`.  Kernel-checked on
 168the actual carrier; uses `mu_congr` (μ is a class function). -/
 169theorem classMass_eq_fiberCard_mul_mu {B : ℕ} (q : TriangulationClass B) :
 170    classMass q = (fiberCard (relabelSetoid B) q : ℝ) * mu (Quotient.out q) := by
 171  unfold classMass
 172  have hconst : ∀ K ∈ classFiber (relabelSetoid B) q, mu K = mu (Quotient.out q) := by
 173    intro K hK
 174    exact mu_congr (equivalent_of_mk_eq
 175      (((mem_classFiber (relabelSetoid B) q K).mp hK).trans (Quotient.out_eq q).symm))
 176  rw [Finset.sum_congr rfl hconst, Finset.sum_const, nsmul_eq_mul]
 177  rfl
 178
 179/-- **T2 (headline).**  For any weight `w` constant on classes (explicit
 180hypothesis `hw`; note `unitaryWeight S` is class-constant only when `S`
 181is), the labeled path sum `Z` equals its class pushforward:
 182`Z B w = Σ_{q : TriangulationClass B} classMass(q) · w(rep q)`.
 183HONEST SCOPE: `classMass q = |fiber(q)| · (1/|Aut(rep q)|)`
 184(see `classMass_eq_fiberCard_mul_mu`), NOT `1/|Aut|` per class; this
 185theorem does NOT equate `Z` with the inequivalent-class sum with weights
 186`1/|Aut|` (the two weights are separated as a kernel fact by
 187`mu_lt_classMass_edgeClass`, built on `exists_nonSingleton_fiber`). -/
 188theorem Z_eq_classPushforward (B : ℕ) (w : BoundedComplex B → ℂ)
 189    (hw : ∀ K K', Equivalent K K' → w K = w K') :
 190    Z B w = ∑ q : TriangulationClass B,
 191      (classMass q : ℂ) * w (Quotient.out q) := by
 192  unfold Z
 193  rw [FiniteQuotient.sum_fiberwise_quotient (relabelSetoid B)
 194    (fun K => (mu K : ℂ) * w K)]
 195  refine Finset.sum_congr rfl fun q _ => ?_
 196  have hmem : ∀ K ∈ classFiber (relabelSetoid B) q, Equivalent K (Quotient.out q) := by
 197    intro K hK
 198    exact equivalent_of_mk_eq
 199      (((mem_classFiber (relabelSetoid B) q K).mp hK).trans (Quotient.out_eq q).symm)
 200  calc ∑ K ∈ classFiber (relabelSetoid B) q, (mu K : ℂ) * w K
 201      = ∑ K ∈ classFiber (relabelSetoid B) q, (mu K : ℂ) * w (Quotient.out q) := by
 202        refine Finset.sum_congr rfl fun K hK => ?_
 203        rw [hw K (Quotient.out q) (hmem K hK)]
 204    _ = (∑ K ∈ classFiber (relabelSetoid B) q, (mu K : ℂ)) * w (Quotient.out q) := by
 205        rw [← Finset.sum_mul]
 206    _ = (classMass q : ℂ) * w (Quotient.out q) := by
 207        unfold classMass
 208        rw [Complex.ofReal_sum]
 209
 210/-- The unitary instance: for a class-constant action `S`, the unitary
 211path sum equals its class pushforward.  Same honest scope as
 212`Z_eq_classPushforward`. -/
 213theorem zRS_eq_classPushforward (B : ℕ) (S : BoundedComplex B → ℝ)
 214    (hS : ∀ K K', Equivalent K K' → S K = S K') :
 215    Z B (unitaryWeight S) = ∑ q : TriangulationClass B,
 216      (classMass q : ℂ) * unitaryWeight S (Quotient.out q) := by
 217  refine Z_eq_classPushforward B (unitaryWeight S) ?_
 218  intro K K' h
 219  unfold unitaryWeight
 220  rw [hS K K' h]
 221
 222/-! ## §3. T3 fork evaluation: a fiber of cardinality > 1 exists
 223
 224The `edgeVerts` field is an ORDERED pair, so swapping the two vertex
 225labels of a one-edge complex produces a DIFFERENT labeled complex that is
 226`Equivalent` to the original via the explicit vertex-swap relabeling.
 227Witness at `B = 2`: `nV = 2`, `nE = 1`, `nT = 0`. -/
 228
 229/-- Labeled complex at `B = 2`: one edge, ordered `(0, 1)`.  (`abbrev` so
 230the size fields reduce during numeral elaboration.) -/
 231abbrev edgeAB : BoundedComplex 2 where
 232  nV := 2
 233  nE := 1
 234  nT := 0
 235  hV := le_refl 2
 236  hE := one_le_two
 237  hT := Nat.zero_le 2
 238  edgeVerts := fun _ => (0, 1)
 239  tetVerts := fun t => t.elim0
 240
 241/-- Labeled complex at `B = 2`: one edge, ordered `(1, 0)` (the vertex
 242labels of `edgeAB` swapped).  (`abbrev` so the size fields reduce during
 243numeral elaboration.) -/
 244abbrev edgeBA : BoundedComplex 2 where
 245  nV := 2
 246  nE := 1
 247  nT := 0
 248  hV := le_refl 2
 249  hE := one_le_two
 250  hT := Nat.zero_le 2
 251  edgeVerts := fun _ => (1, 0)
 252  tetVerts := fun t => t.elim0
 253
 254/-- The explicit vertex-swap relabeling `edgeAB ≃ edgeBA`. -/
 255def edgeSwapRelabel : Relabel edgeAB edgeBA where
 256  vEquiv := Equiv.swap 0 1
 257  eEquiv := Equiv.refl _
 258  tEquiv := Equiv.refl _
 259  edge_comm := fun _ => by
 260    show ((1 : Fin 2), (0 : Fin 2)) =
 261      (Equiv.swap (0 : Fin 2) 1 (0 : Fin 2), Equiv.swap (0 : Fin 2) 1 (1 : Fin 2))
 262    rw [Equiv.swap_apply_left, Equiv.swap_apply_right]
 263  tet_comm := fun t _ => t.elim0
 264
 265/-- Labeled observable separating the two witnesses: the numeric value of
 266the first endpoint of edge `0` (or `0` if there is no edge). -/
 267def firstEndpointVal {B : ℕ} (K : BoundedComplex B) : ℕ :=
 268  if h : 0 < K.nE then ((K.edgeVerts ⟨0, h⟩).1 : ℕ) else 0
 269
 270theorem firstEndpointVal_edgeAB : firstEndpointVal edgeAB = 0 := rfl
 271
 272theorem firstEndpointVal_edgeBA : firstEndpointVal edgeBA = 1 := rfl
 273
 274/-- The two witnesses are DISTINCT labeled complexes (they differ on the
 275labeled observable `firstEndpointVal`). -/
 276theorem edgeAB_ne_edgeBA : edgeAB ≠ edgeBA := by
 277  intro h
 278  have h0 := congrArg firstEndpointVal h
 279  rw [firstEndpointVal_edgeAB, firstEndpointVal_edgeBA] at h0
 280  exact absurd h0 (by norm_num)
 281
 282/-- **T3 FORK VERDICT (non-singleton fiber; C1 landmine detonated).**
 283There exist two distinct labeled complexes that are equivalent: the
 284quotient fibers of `TriangulationClass` are NOT all singletons, so the
 285labeled pushforward mass `classMass = |fiber| · (1/|Aut|)` genuinely
 286differs from the per-class `1/|Aut|` weight.  Explicit witness at
 287`B = 2`. -/
 288theorem exists_nonSingleton_fiber :
 289    ∃ K K' : BoundedComplex 2, K ≠ K' ∧ Equivalent K K' :=
 290  ⟨edgeAB, edgeBA, edgeAB_ne_edgeBA, ⟨edgeSwapRelabel⟩⟩
 291
 292/-- **T3 FORK VERDICT (count form).**  The fiber of the one-edge class at
 293`B = 2` has labeled cardinality strictly greater than 1: both `edgeAB`
 294and `edgeBA` lie in it. -/
 295theorem one_lt_fiberCard_edgeClass :
 296    1 < fiberCard (relabelSetoid 2) (Quotient.mk (relabelSetoid 2) edgeAB) := by
 297  have hmemAB : edgeAB ∈ classFiber (relabelSetoid 2)
 298      (Quotient.mk (relabelSetoid 2) edgeAB) :=
 299    (mem_classFiber (relabelSetoid 2) _ edgeAB).mpr rfl
 300  have hmemBA : edgeBA ∈ classFiber (relabelSetoid 2)
 301      (Quotient.mk (relabelSetoid 2) edgeAB) :=
 302    (mem_classFiber (relabelSetoid 2) _ edgeBA).mpr
 303      (Quotient.sound ⟨edgeSwapRelabel.symm⟩)
 304  exact Finset.one_lt_card.mpr
 305    ⟨edgeBA, hmemBA, edgeAB, hmemAB, fun h => edgeAB_ne_edgeBA h.symm⟩
 306
 307/-- **T3 FORK VERDICT (numeric witness; the formalized detonation).**
 308At the `B = 2` edge class the labeled measure of a single representative
 309is STRICTLY BELOW the pushforward class mass:
 310`μ(edgeAB) < classMass(⟦edgeAB⟧)`.  Hence a path sum carrying weight
 311`classMass` per class is NOT the per-class `1/|Aut|` sum, as a kernel
 312fact (via `classMass_eq_fiberCard_mul_mu`, `one_lt_fiberCard_edgeClass`,
 313`mu_congr`, and `mu_pos`).  This concerns the LABELED `PathSum.Z` object
 314only. -/
 315theorem mu_lt_classMass_edgeClass :
 316    mu edgeAB < classMass (Quotient.mk (relabelSetoid 2) edgeAB) := by
 317  have hrep : mu (Quotient.out (Quotient.mk (relabelSetoid 2) edgeAB)) =
 318      mu edgeAB :=
 319    mu_congr (equivalent_of_mk_eq (Quotient.out_eq _))
 320  rw [classMass_eq_fiberCard_mul_mu, hrep]
 321  have hcard : (1 : ℝ) < (fiberCard (relabelSetoid 2)
 322      (Quotient.mk (relabelSetoid 2) edgeAB) : ℝ) := by
 323    exact_mod_cast one_lt_fiberCard_edgeClass
 324  calc mu edgeAB = 1 * mu edgeAB := (one_mul _).symm
 325    _ < _ * mu edgeAB := mul_lt_mul_of_pos_right hcard (mu_pos edgeAB)
 326
 327end PathSum
 328
 329/-! ## §4. Status ledger (rfl-forced; RED flags stay RED) -/
 330
 331/-- Status record for the class-pushforward wave.  No `True` shells; every
 332flag is forced by `rfl` below. -/
 333structure ClassPushforwardStatus where
 334  generic_fiber_decomposition_proved : Bool
 335  classMass_defined : Bool
 336  Z_eq_classPushforward_proved : Bool
 337  classMass_is_fiberCard_mul_mu : Bool
 338  nonSingleton_fiber_exhibited : Bool
 339  /-- FALSE (C1 detonated): the standing labeled `PathSum.Z` is NOT the
 340  inequivalent-class sum with per-class `1/|Aut|` weights; the kernel
 341  witness is `PathSum.mu_lt_classMass_edgeClass`.  (Says nothing about
 342  the separate quotient-sum convention of the exact-shell `Z_RS_uv`.) -/
 343  Z_is_invAut_class_sum : Bool
 344  /-- FALSE: the quotient-first path-sum object is promoted to the next
 345  wave, not constructed here. -/
 346  quotient_first_object_constructed : Bool
 347  /-- RED. -/
 348  Z_RS_continuum_limit : Bool
 349  /-- RED. -/
 350  substrate_measure_derived : Bool
 351  /-- RED. -/
 352  gap1_bridge_derived : Bool
 353
 354/-- The class-pushforward status after this module. -/
 355def classPushforwardStatus : ClassPushforwardStatus where
 356  generic_fiber_decomposition_proved := true
 357  classMass_defined := true
 358  Z_eq_classPushforward_proved := true
 359  classMass_is_fiberCard_mul_mu := true
 360  nonSingleton_fiber_exhibited := true
 361  Z_is_invAut_class_sum := false
 362  quotient_first_object_constructed := false
 363  Z_RS_continuum_limit := false
 364  substrate_measure_derived := false
 365  gap1_bridge_derived := false
 366
 367theorem classPushforwardStatus_flags :
 368    classPushforwardStatus.generic_fiber_decomposition_proved = true ∧
 369    classPushforwardStatus.classMass_defined = true ∧
 370    classPushforwardStatus.Z_eq_classPushforward_proved = true ∧
 371    classPushforwardStatus.classMass_is_fiberCard_mul_mu = true ∧
 372    classPushforwardStatus.nonSingleton_fiber_exhibited = true ∧
 373    classPushforwardStatus.Z_is_invAut_class_sum = false ∧
 374    classPushforwardStatus.quotient_first_object_constructed = false ∧
 375    classPushforwardStatus.Z_RS_continuum_limit = false ∧
 376    classPushforwardStatus.substrate_measure_derived = false ∧
 377    classPushforwardStatus.gap1_bridge_derived = false :=
 378  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
 379
 380end SevenGaps
 381end Gravity
 382end IndisputableMonolith
 383