IndisputableMonolith.Gravity.SevenGaps.QuotientFirstZ

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.ClassPushforward
   3
   4/-!
   5# Seven Gaps, Pillar 2: quotient-first path-sum object
   6
   7## What is proved here
   8
   9This module constructs the quotient-first path-sum object promoted by the
  10P2c panel lock:
  11
  12* `Zq B wq = Σ q : TriangulationClass B, (1 / |Aut(out q)|) · wq q`.
  13  The quotient is finite by the scoped `FiniteQuotient` instances imported
  14  from `ClassPushforward`; those classical instances are opened locally.
  15* `labeledZ_eq_sum_fiberCard_mul_mu`: the standing LABELED path sum
  16  `PathSumMeasure.Z` with a class-constant weight is exactly the quotient
  17  sum with the mandatory labeled-fiber factor:
  18  `Σ q, |fiber q| · μ(out q) · wq q`.
  19* `labeledZ_eq_Zq_plus_fiberExcess` and
  20  `Zq_eq_labeledZ_iff_fiberExcess_vanishes`: the exact relation between
  21  `Zq` and the labeled `Z` is not an unconditional equality.  Their
  22  difference is the explicit excess
  23  `Σ q, (|fiber q| - 1) · μ(out q) · wq q`.
  24
  25## Honesty boundary
  26
  27The P2c panel killed the unconditional claim that the standing labeled
  28`PathSumMeasure.Z` equals the per-class `1/|Aut|` quotient sum.  This file
  29does not resurrect it by convention.  The non-singleton fiber fact is
  30inherited from `ClassPushforward` (`PathSum.one_lt_fiberCard_edgeClass`),
  31so the fiber factor remains part of the bridge.
  32
  33No orbit-stabilizer theorem for the full bounded `TriangulationClass B`
  34setoid is derived here.  Unlike the fixed-signature exact-shell machinery,
  35the scoped bounded carrier ranges over varying signatures, so a single
  36global relabeling group action is not supplied in this wave.  Any future
  37orbit-stabilizer statement must be a theorem with its signature/gauge
  38volume hypotheses explicit.
  39
  40Expected axiom footprint: standard trio
  41`[propext, Classical.choice, Quot.sound]`.
  42-/
  43
  44namespace IndisputableMonolith
  45namespace Gravity
  46namespace SevenGaps
  47namespace QuotientFirstZ
  48
  49open PathSumMeasure
  50open FiniteQuotient
  51
  52/-- The quotient-first path sum over triangulation classes, with the
  53per-class symmetry-factor measure evaluated on the chosen representative.
  54This is the quotient convention, not the standing labeled `PathSumMeasure.Z`.
  55-/
  56noncomputable def Zq (B : ℕ) (wq : TriangulationClass B → ℂ) : ℂ :=
  57  ∑ q : TriangulationClass B, (mu (Quotient.out q) : ℂ) * wq q
  58
  59/-- The representative symmetry factor is independent of the chosen
  60representative of a triangulation class. -/
  61theorem mu_out_eq_of_mk_eq {B : ℕ} {K : BoundedComplex B}
  62    (q : TriangulationClass B) (hK : Quotient.mk (relabelSetoid B) K = q) :
  63    mu (Quotient.out q) = mu K := by
  64  exact mu_congr (PathSum.equivalent_of_mk_eq ((Quotient.out_eq q).trans hK.symm))
  65
  66/-- **Bridge to the labeled sum, with the mandatory fiber factor.**  For a
  67class weight `wq`, the standing labeled path sum with pulled-back weight is
  68the quotient sum weighted by the pushforward class mass
  69`|fiber q| · μ(out q)`. -/
  70theorem labeledZ_eq_sum_fiberCard_mul_mu (B : ℕ)
  71    (wq : TriangulationClass B → ℂ) :
  72    Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) =
  73      ∑ q : TriangulationClass B,
  74        (((fiberCard (relabelSetoid B) q : ℂ) * (mu (Quotient.out q) : ℂ))
  75          * wq q) := by
  76  classical
  77  have hw : ∀ K K' : BoundedComplex B, Equivalent K K' →
  78      wq (Quotient.mk (relabelSetoid B) K) =
  79        wq (Quotient.mk (relabelSetoid B) K') := by
  80    intro K K' h
  81    exact congrArg wq (Quotient.sound h)
  82  calc
  83    Z B (fun K => wq (Quotient.mk (relabelSetoid B) K))
  84        = ∑ q : TriangulationClass B,
  85            (PathSum.classMass q : ℂ) *
  86              wq (Quotient.mk (relabelSetoid B) (Quotient.out q)) := by
  87          simpa using PathSum.Z_eq_classPushforward B
  88            (fun K => wq (Quotient.mk (relabelSetoid B) K)) hw
  89    _ = ∑ q : TriangulationClass B,
  90        (((fiberCard (relabelSetoid B) q : ℂ) * (mu (Quotient.out q) : ℂ))
  91          * wq q) := by
  92          refine Finset.sum_congr rfl fun q _ => ?_
  93          rw [PathSum.classMass_eq_fiberCard_mul_mu]
  94          rw [show wq (Quotient.mk (relabelSetoid B) (Quotient.out q)) = wq q
  95            from congrArg wq (Quotient.out_eq q)]
  96          simp only [Complex.ofReal_mul]
  97          norm_num
  98
  99/-- The explicit excess by which the labeled class pushforward differs
 100from the quotient-first object.  It is zero only under additional
 101fiber/weight cancellation hypotheses; no such cancellation is assumed. -/
 102noncomputable def fiberExcess (B : ℕ) (wq : TriangulationClass B → ℂ) : ℂ :=
 103  ∑ q : TriangulationClass B,
 104    ((((fiberCard (relabelSetoid B) q : ℂ) - 1) * (mu (Quotient.out q) : ℂ))
 105      * wq q)
 106
 107/-- **Exact relation.**  The labeled class-constant path sum is the
 108quotient-first path sum plus the labeled-fiber excess.  This is the honest
 109replacement for the killed unconditional claim `Z = Σ_q wq/|Aut q|`. -/
 110theorem labeledZ_eq_Zq_plus_fiberExcess (B : ℕ)
 111    (wq : TriangulationClass B → ℂ) :
 112    Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) =
 113      Zq B wq + fiberExcess B wq := by
 114  classical
 115  rw [labeledZ_eq_sum_fiberCard_mul_mu, Zq, fiberExcess, ← Finset.sum_add_distrib]
 116  refine Finset.sum_congr rfl fun q _ => ?_
 117  let f : ℂ := fiberCard (relabelSetoid B) q
 118  let m : ℂ := mu (Quotient.out q)
 119  let z : ℂ := wq q
 120  calc
 121    (((fiberCard (relabelSetoid B) q : ℂ) * (mu (Quotient.out q) : ℂ)) * wq q)
 122        = (f * m) * z := rfl
 123    _ = m * z + ((f - 1) * m) * z := by ring
 124    _ = (mu (Quotient.out q) : ℂ) * wq q +
 125        ((((fiberCard (relabelSetoid B) q : ℂ) - 1) *
 126          (mu (Quotient.out q) : ℂ)) * wq q) := rfl
 127
 128/-- **IFF form of the exact relation.**  The quotient-first object equals
 129the standing labeled sum for a pulled-back class weight exactly when the
 130explicit fiber excess vanishes. -/
 131theorem Zq_eq_labeledZ_iff_fiberExcess_vanishes (B : ℕ)
 132    (wq : TriangulationClass B → ℂ) :
 133    Zq B wq = Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) ↔
 134      fiberExcess B wq = 0 := by
 135  rw [labeledZ_eq_Zq_plus_fiberExcess]
 136  constructor
 137  · intro h
 138    have h' : Zq B wq + fiberExcess B wq = Zq B wq + 0 := by
 139      simpa using h.symm
 140    exact add_left_cancel h'
 141  · intro h
 142    rw [h, add_zero]
 143
 144/-- A sufficient singleton-fiber condition under which the quotient-first
 145object agrees with the labeled sum.  `ClassPushforward` proves this
 146condition is false in general (`PathSum.one_lt_fiberCard_edgeClass`). -/
 147theorem Zq_eq_labeledZ_of_singleton_fibers (B : ℕ)
 148    (wq : TriangulationClass B → ℂ)
 149    (hfiber : ∀ q : TriangulationClass B,
 150      fiberCard (relabelSetoid B) q = 1) :
 151    Zq B wq = Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) := by
 152  rw [Zq_eq_labeledZ_iff_fiberExcess_vanishes]
 153  unfold fiberExcess
 154  refine Finset.sum_eq_zero fun q _ => ?_
 155  rw [hfiber q]
 156  norm_num
 157
 158/-! ## Status record (honest boundary; RED flags stay RED) -/
 159
 160/-- Status record for the quotient-first path-sum wave.  No `True` shells:
 161the grounding theorem below ties the green flags to kernel statements and
 162keeps the requested RED flags false. -/
 163structure QuotientFirstStatus where
 164  quotient_first_object_constructed : Bool
 165  labeled_bridge_has_fiber_factor : Bool
 166  exact_excess_relation_proved : Bool
 167  nonSingleton_fiber_inherited : Bool
 168  /-- FALSE in this wave: no full bounded-setoid orbit-stabilizer theorem
 169  is derived here. -/
 170  bounded_orbit_stabilizer_derived : Bool
 171  /-- RED. -/
 172  Z_RS_continuum_limit : Bool
 173  /-- RED: the `1/|Aut|` measure remains a MODEL input. -/
 174  substrate_measure_derived : Bool
 175  /-- RED. -/
 176  gap1_bridge_derived : Bool
 177
 178/-- The canonical status record for this quotient-first module. -/
 179def quotientFirstStatus : QuotientFirstStatus where
 180  quotient_first_object_constructed := true
 181  labeled_bridge_has_fiber_factor := true
 182  exact_excess_relation_proved := true
 183  nonSingleton_fiber_inherited := true
 184  bounded_orbit_stabilizer_derived := false
 185  Z_RS_continuum_limit := false
 186  substrate_measure_derived := false
 187  gap1_bridge_derived := false
 188
 189/-- **Grounding theorem.**  The status flags are tied to the constructed
 190object and kernel bridges.  The RED flags remain false, and the inherited
 191non-singleton fiber theorem records why the unconditional labeled/quotient
 192equality is not available. -/
 193theorem quotientFirstStatus_grounded :
 194    (quotientFirstStatus.quotient_first_object_constructed = true ∧
 195      ∀ B : ℕ, ∀ wq : TriangulationClass B → ℂ,
 196        Zq B wq = ∑ q : TriangulationClass B,
 197          (mu (Quotient.out q) : ℂ) * wq q) ∧
 198    (quotientFirstStatus.labeled_bridge_has_fiber_factor = true ∧
 199      ∀ B : ℕ, ∀ wq : TriangulationClass B → ℂ,
 200        Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) =
 201          ∑ q : TriangulationClass B,
 202            (((fiberCard (relabelSetoid B) q : ℂ) * (mu (Quotient.out q) : ℂ))
 203              * wq q)) ∧
 204    (quotientFirstStatus.exact_excess_relation_proved = true ∧
 205      ∀ B : ℕ, ∀ wq : TriangulationClass B → ℂ,
 206        Zq B wq = Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) ↔
 207          fiberExcess B wq = 0) ∧
 208    (quotientFirstStatus.nonSingleton_fiber_inherited = true ∧
 209      1 < fiberCard (relabelSetoid 2)
 210        (Quotient.mk (relabelSetoid 2) PathSum.edgeAB)) ∧
 211    quotientFirstStatus.bounded_orbit_stabilizer_derived = false ∧
 212    quotientFirstStatus.Z_RS_continuum_limit = false ∧
 213    quotientFirstStatus.substrate_measure_derived = false ∧
 214    quotientFirstStatus.gap1_bridge_derived = false :=
 215  ⟨⟨rfl, fun _ _ => rfl⟩,
 216    ⟨rfl, labeledZ_eq_sum_fiberCard_mul_mu⟩,
 217    ⟨rfl, Zq_eq_labeledZ_iff_fiberExcess_vanishes⟩,
 218    ⟨rfl, PathSum.one_lt_fiberCard_edgeClass⟩,
 219    rfl, rfl, rfl, rfl⟩
 220
 221end QuotientFirstZ
 222end SevenGaps
 223end Gravity
 224end IndisputableMonolith
 225