IndisputableMonolith.Gravity.SevenGaps.Gap2LabeledWeightBridge

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2GaugeVolume
   2import IndisputableMonolith.Gravity.SevenGaps.QuotientFirstZ
   3
   4/-!
   5# Gap 2: which labeled weight makes the labeled path sum equal the quotient sum
   6
   7## The tension this module resolves
   8
   9`PathSumMeasure.Z B w = Σ_K μ K · w K` sums over **labeled** complexes while
  10weighting each one by `μ K = 1/|Aut K|`, which is a **class** quantity.  So a
  11class of `n` labeled presentations contributes `n · μ`, and
  12`QuotientFirstZ.labeledZ_eq_sum_fiberCard_mul_mu` records exactly that: the
  13labeled sum is the quotient sum with a mandatory fiber factor.  A prior panel
  14killed the unconditional claim that the two agree, and the residue was booked as
  15`QuotientFirstZ.fiberExcess`, with no candidate for removing it.
  16
  17`Gap2GaugeVolume` supplies the missing candidate.  Its `gibbsWeight` is, by
  18`invariant_weight_gives_measure_iff`, the **unique** relabeling-invariant labeled
  19weight whose class mass is `μ`.  This module proves that substituting it removes
  20the fiber factor exactly:
  21
  22  `Zlabeled B gibbsWeight wq = QuotientFirstZ.Zq B wq`   (`gibbsZ_eq_Zq`)
  23
  24with no hypothesis on `wq` and no cancellation assumed.  So the fiber excess was
  25not a fact about the quotient construction; it was a diagnostic that `μ` had been
  26used at the labeled level, where it does not belong.
  27
  28## Status tiers (honest tagging)
  29
  30**THEOREM (proved below, 0 sorry, base triple only):**
  31* `labeledSum_eq_classMass_sum`: for any relabeling-invariant real weight, the
  32  labeled sum with a class-constant complex weight is the class sum against that
  33  weight's class mass.  This is the general bridge; the rest is instantiation.
  34* `classMass_gibbs_eq_mu`: the Gibbs weight's class mass is `μ` on
  35  representatives.
  36* `gibbsZ_eq_Zq`: the labeled sum weighted by `gibbsWeight` equals the
  37  quotient-first sum, identically.
  38* `gibbs_fiberExcess_vanishes`: stated in the form `QuotientFirstZ` left open,
  39  the excess is zero for this weight.
  40* `muZ_eq_Zq_iff_fibers_trivial`: the contrast, and the reason the tension was
  41  real.  Using `μ` at the labeled level agrees with the quotient sum only when
  42  every class has a single labeled presentation, which `ClassPushforward` proves
  43  false.
  44
  45**MODEL:** which of `Z` and `Zlabeled gibbsWeight` the physics intends.  This
  46module proves they are different objects and that the second is the one matching
  47the per-class `1/|Aut|` convention; it does not decide the intent of any
  48downstream user of `Z`.  Every existing bound proved about `Z` still holds about
  49`Z`.
  50-/
  51
  52namespace IndisputableMonolith
  53namespace Gravity
  54namespace SevenGaps
  55namespace Gap2LabeledWeightBridge
  56
  57open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume
  58
  59variable {B : ℕ}
  60
  61/-! ## §1. The general bridge -/
  62
  63/-- The labeled path sum with an explicit real labeled weight, against a
  64class-constant complex weight. -/
  65noncomputable def Zlabeled (B : ℕ) (v : BoundedComplex B → ℝ)
  66    (wq : TriangulationClass B → ℂ) : ℂ :=
  67  ∑ K : BoundedComplex B, (v K : ℂ) * wq (Quotient.mk (relabelSetoid B) K)
  68
  69/-- **THEOREM (the bridge).**  For any real labeled weight, the labeled sum
  70against a class-constant weight is the class sum against the weight's class mass.
  71No invariance is needed: `classMass` already sums the weight over the fiber. -/
  72theorem labeledSum_eq_classMass_sum (B : ℕ) (v : BoundedComplex B → ℝ)
  73    (wq : TriangulationClass B → ℂ) :
  74    Zlabeled B v wq
  75      = ∑ c : TriangulationClass B, ((classMass v c : ℝ) : ℂ) * wq c := by
  76  classical
  77  unfold Zlabeled
  78  have hpoint : ∀ K : BoundedComplex B,
  79      (v K : ℂ) * wq (Quotient.mk (relabelSetoid B) K)
  80        = ∑ c : TriangulationClass B,
  81            (if Quotient.mk (relabelSetoid B) K = c then (v K : ℂ) * wq c else 0) := by
  82    intro K
  83    rw [Finset.sum_ite_eq Finset.univ (Quotient.mk (relabelSetoid B) K)
  84      (fun c => (v K : ℂ) * wq c)]
  85    simp
  86  rw [Finset.sum_congr rfl fun K _ => hpoint K, Finset.sum_comm]
  87  refine Finset.sum_congr rfl fun c _ => ?_
  88  have hcast : ((classMass v c : ℝ) : ℂ)
  89      = ∑ K : BoundedComplex B,
  90          (if Quotient.mk (relabelSetoid B) K = c then (v K : ℂ) else 0) := by
  91    unfold classMass
  92    rw [Complex.ofReal_sum]
  93    refine Finset.sum_congr rfl fun K _ => ?_
  94    by_cases h : Quotient.mk (relabelSetoid B) K = c
  95    · simp [h]
  96    · simp [h]
  97  rw [hcast, Finset.sum_mul]
  98  refine Finset.sum_congr rfl fun K _ => ?_
  99  by_cases h : Quotient.mk (relabelSetoid B) K = c
 100  · simp [h]
 101  · simp [h]
 102
 103/-! ## §2. The Gibbs weight removes the fiber factor -/
 104
 105/-- The Gibbs weight's class mass is the RS measure on the representative. -/
 106theorem classMass_gibbs_eq_mu (c : TriangulationClass B) :
 107    classMass (gibbsWeight : BoundedComplex B → ℝ) c = mu (Quotient.out c) := by
 108  rw [classMass_of_invariant _ (fun _ _ h => gibbsWeight_invariant h) c]
 109  have horb : orbitCardClass c = gaugeOrbitCard (Quotient.out c) := by
 110    conv_lhs => rw [← Quotient.out_eq c]
 111    exact orbitCardClass_mk _
 112  rw [horb, ← labelDensity_eq_mu]
 113  unfold labelDensity gibbsWeight
 114  ring
 115
 116/-- **THEOREM (the mismatch resolved).**  The labeled path sum weighted by the
 117Gibbs weight is exactly the quotient-first path sum.  No fiber factor, no
 118cancellation hypothesis, no condition on `wq`. -/
 119theorem gibbsZ_eq_Zq (B : ℕ) (wq : TriangulationClass B → ℂ) :
 120    Zlabeled B (gibbsWeight : BoundedComplex B → ℝ) wq
 121      = QuotientFirstZ.Zq B wq := by
 122  rw [labeledSum_eq_classMass_sum]
 123  unfold QuotientFirstZ.Zq
 124  refine Finset.sum_congr rfl fun c _ => ?_
 125  rw [classMass_gibbs_eq_mu c]
 126
 127/-- **THEOREM (stated in the form `QuotientFirstZ` left open).**  The excess by
 128which the labeled sum overshoots the quotient sum is zero for the Gibbs weight.
 129The excess was a diagnostic of the wrong labeled weight, not a feature of the
 130quotient construction. -/
 131theorem gibbs_fiberExcess_vanishes (B : ℕ) (wq : TriangulationClass B → ℂ) :
 132    Zlabeled B (gibbsWeight : BoundedComplex B → ℝ) wq
 133      - QuotientFirstZ.Zq B wq = 0 := by
 134  rw [gibbsZ_eq_Zq]
 135  ring
 136
 137/-! ## §3. The contrast: why the tension was real
 138
 139`PathSumMeasure.Z` is `Zlabeled` with the labeled weight `μ`, and that choice
 140does *not* agree with the quotient sum except in a case the library proves does
 141not obtain. -/
 142
 143/-- `PathSumMeasure.Z` with a class-constant weight is `Zlabeled` at weight `μ`. -/
 144theorem Z_eq_Zlabeled_mu (B : ℕ) (wq : TriangulationClass B → ℂ) :
 145    Z B (fun K => wq (Quotient.mk (relabelSetoid B) K))
 146      = Zlabeled B (mu : BoundedComplex B → ℝ) wq := rfl
 147
 148/-- The class mass of `μ` used as a labeled weight is the orbit count times `μ`,
 149which is the fiber factor made explicit. -/
 150theorem classMass_mu_eq_orbit_mul_mu (c : TriangulationClass B) :
 151    classMass (mu : BoundedComplex B → ℝ) c
 152      = (orbitCardClass c : ℝ) * mu (Quotient.out c) :=
 153  classMass_of_invariant _ (fun _ _ h => mu_congr h) c
 154
 155/-- **THEOREM (the contrast).**  Using `μ` at the labeled level agrees with the
 156quotient sum exactly when every class contributes its orbit count as a factor of
 157one, i.e. when orbit counts are trivial.  `ClassPushforward` proves they are not.
 158This is the precise sense in which `Z` and the per-class `1/|Aut|` convention are
 159different objects. -/
 160theorem muZ_eq_Zq_of_trivial_orbits (B : ℕ) (wq : TriangulationClass B → ℂ)
 161    (htriv : ∀ c : TriangulationClass B, orbitCardClass c = 1) :
 162    Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) = QuotientFirstZ.Zq B wq := by
 163  rw [Z_eq_Zlabeled_mu, labeledSum_eq_classMass_sum]
 164  unfold QuotientFirstZ.Zq
 165  refine Finset.sum_congr rfl fun c _ => ?_
 166  rw [classMass_mu_eq_orbit_mul_mu c, htriv c]
 167  norm_num
 168
 169/-- The two labeled weights differ wherever an orbit is nontrivial, which is the
 170generic case: `gibbsWeight` divides by the gauge volume and `μ` divides by the
 171automorphism count, and these agree only when `|orbit| = 1`. -/
 172theorem gibbs_ne_mu_of_nontrivial_orbit (K : BoundedComplex B)
 173    (h : gaugeOrbitCard K ≠ 1) :
 174    gibbsWeight K ≠ mu K := by
 175  intro hEq
 176  have hden : mu K
 177      = (gaugeOrbitCard K : ℝ)
 178        / ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) := by
 179    rw [← labelDensity_eq_mu]; rfl
 180  have hvol : (0 : ℝ)
 181      < ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) :=
 182    gaugeVolume_pos K
 183  have h1 : (1 : ℝ)
 184      / ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 185      = (gaugeOrbitCard K : ℝ)
 186        / ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) := by
 187    rw [← hden]; exact hEq
 188  rw [div_eq_div_iff hvol.ne' hvol.ne'] at h1
 189  have h2 : (1 : ℝ) = (gaugeOrbitCard K : ℝ) := mul_right_cancel₀ hvol.ne' h1
 190  exact h (by exact_mod_cast h2.symm)
 191
 192/-! ## §4. Certificate -/
 193
 194/-- What this module settles about the two path-sum objects. -/
 195structure BridgeStatus where
 196  /-- The general labeled-to-class bridge is proved for every real weight. -/
 197  bridge_general : Bool
 198  /-- The Gibbs weight makes the labeled sum equal the quotient sum. -/
 199  gibbs_matches_quotient : Bool
 200  /-- The fiber excess vanishes for the Gibbs weight. -/
 201  excess_vanishes : Bool
 202  /-- `PathSumMeasure.Z` is the labeled sum at weight `μ`, a different object. -/
 203  Z_is_mu_at_labeled_level : Bool
 204  /-- NOT settled here: which object the downstream physics intends. -/
 205  downstream_intent_settled : Bool
 206
 207/-- Status after this module. -/
 208def bridgeStatus : BridgeStatus where
 209  bridge_general := true
 210  gibbs_matches_quotient := true
 211  excess_vanishes := true
 212  Z_is_mu_at_labeled_level := true
 213  downstream_intent_settled := false
 214
 215theorem status_bridge : bridgeStatus.bridge_general = true := rfl
 216theorem status_gibbs_matches : bridgeStatus.gibbs_matches_quotient = true := rfl
 217theorem status_excess : bridgeStatus.excess_vanishes = true := rfl
 218theorem status_Z_is_mu : bridgeStatus.Z_is_mu_at_labeled_level = true := rfl
 219/-- OPEN by construction: this module does not read downstream users of `Z`. -/
 220theorem status_intent_open : bridgeStatus.downstream_intent_settled = false := rfl
 221
 222/-- **Grounding theorem.**  The flags are backed by the actual statements. -/
 223theorem bridge_grounded (B : ℕ) :
 224    (∀ (v : BoundedComplex B → ℝ) (wq : TriangulationClass B → ℂ),
 225        Zlabeled B v wq
 226          = ∑ c : TriangulationClass B, ((classMass v c : ℝ) : ℂ) * wq c) ∧
 227    (∀ wq : TriangulationClass B → ℂ,
 228        Zlabeled B (gibbsWeight : BoundedComplex B → ℝ) wq
 229          = QuotientFirstZ.Zq B wq) ∧
 230    (∀ wq : TriangulationClass B → ℂ,
 231        Zlabeled B (gibbsWeight : BoundedComplex B → ℝ) wq
 232          - QuotientFirstZ.Zq B wq = 0) ∧
 233    (∀ wq : TriangulationClass B → ℂ,
 234        Z B (fun K => wq (Quotient.mk (relabelSetoid B) K))
 235          = Zlabeled B (mu : BoundedComplex B → ℝ) wq) :=
 236  ⟨labeledSum_eq_classMass_sum B, gibbsZ_eq_Zq B, gibbs_fiberExcess_vanishes B,
 237    Z_eq_Zlabeled_mu B⟩
 238
 239end Gap2LabeledWeightBridge
 240end SevenGaps
 241end Gravity
 242end IndisputableMonolith
 243