IndisputableMonolith.Gravity.SevenGaps.Gap2GaugeVolume

   1import IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker
   2
   3/-!
   4# Gap 2: the gauge volume is the order of the sector's relabeling group
   5
   6## What this module does
   7
   8`ExactShellGaugePreflight` derives `mu K = 1/|Aut K|` from a MODEL premise it
   9calls the *pair-counting principle*: the class mass is labeled copies per unit
  10of gauge volume, where the gauge volume `pairCount K` counts pairs
  11`(K', r)` of an orbit member and a relabeling witness.  That premise reads as
  12an invented bookkeeping convention, and `MeasureSubstrateBlocker` records the
  13open task as "derive normalized gauge counting from richer ledger structure".
  14
  15This module identifies the premise by computing the gauge volume:
  16
  17  `pairCount K = (K.nV)! * (K.nE)! * (K.nT)!`
  18
  19The gauge volume carries **no information about the complex**: it is the order of the
  20full relabeling group of `K`'s size sector, `S_nV × S_nE × S_nT`.  So the premise can
  21be restated without the invented quantity, as
  22
  23  class weight  =  (labeled presentations of the class) / (relabelings in the sector)
  24
  25and `labelDensity_eq_mu` proves this ratio is exactly `1/|Aut K|`, the discrete
  26Faddeev-Popov form.
  27
  28## What the premise is NOT (revised 2026-07-28 after adversarial review)
  29
  30An earlier version of this header called the premise **label indifference**, "each
  31labeling counted once and none preferred", and treated a size-only divisor as
  32physically inert.  A four-seat adversarial review at maximum effort returned the same
  33objection from all four seats, and it is correct.  §6c now proves it:
  34
  35* `fugacityWeight_invariant`: for **any** function `a` of the three index sizes, the
  36  weight `a(sizes)/(nV! nE! nT!)` is relabeling-invariant.  So label indifference,
  37  honestly formalized as "the weight is a class function", is satisfied by an entire
  38  family and does not select the Gibbs weight.  The name undershoots the premise.
  39* `gaugeCounting_iff_fugacity_one`: the gauge-counting principle is exactly the member
  40  of that family with `a ≡ 1`.  So the premise is the choice of **unit cross-sector
  41  fugacity**: one positive real per size sector, set to one.
  42* `fugacity_absorbs_into_action`: that factor can be moved between the measure and the
  43  action, `S ↦ S - log a`, without changing any weighted sum.  Only the product is
  44  determined, so "the measure is forced" is relative to a booking convention.
  45
  46The residue is therefore not inert.  A size-only divisor is a reweighting *between*
  47sectors, and in a discrete gravity path sum it competes with the bare cosmological
  48constant.  What genuinely closed is the *localization* of the premise: from an opaque
  49invented quantity to one positive function on the sector lattice, with its group made
  50explicit.
  51
  52## Status tiers (honest tagging)
  53
  54**THEOREM (proved below, 0 sorry, 0 new axioms beyond the base triple):**
  55* `pairCount_eq_factorials`: the gauge volume is `nV! * nE! * nT!`.
  56* `pairCount_congr_sizes`: hence the gauge volume is a function of the index
  57  sizes only, so it cannot distinguish complexes within a size sector.
  58* `orbitCard_mul_autCard`: orbit-stabilizer in sector form,
  59  `|orbit K| * |Aut K| = nV! * nE! * nT!` (the factorization
  60  `pairCount = orbitCard * autCard` is `ExactShellGaugePreflight`'s; the new
  61  content is the closed form of the right-hand side).
  62* `labelDensity_eq_mu`: the count of labeled presentations of `K` per relabeling
  63  in the sector equals `mu K = 1/|Aut K|`.
  64* `gaugeCounting_iff_labelIndifference`: `GaugeCountingPrinciple ν` holds
  65  exactly when `ν` is that label density.  An equivalence, so it restates the
  66  premise without discharging it.
  67* §6c: the residual freedom in closed form, as above.
  68
  69**MODEL:** any reading of the above as licensing the premise.  The equivalences are
  70theorems; the claim that a standard name ("Gibbs", "Faddeev-Popov") supplies a reason
  71is not, and the four-seat review was unanimous on that point.
  72
  73## The premise reduced, not just named (§6d)
  74
  75The review's two strongest seats converged on the same route as the only one that
  76would *close* rather than relocate: the shuffle identity
  77`f(m+n) · C(m+n, m) = f(m) · f(n)`.  §6d proves it.
  78
  79* `gluingLaw_forces_inverse_factorial`: the inverse factorial is the **unique**
  80  size-indexed weight satisfying that identity, given unit weight on the empty and
  81  singleton index sets.
  82* `gluingLaw_gives_gaugeCounting`: therefore the gluing law **implies** the
  83  gauge-counting principle.
  84* `inverseFactorial_gluingLaw`: and the law is satisfiable, so the implication is not
  85  vacuous.
  86
  87So the debt changes shape.  What the theory owes is no longer a normalization ("the
  88sector fugacity is one") but a locality statement: the weight of an assembled
  89configuration times the number of ways to interleave the parts' labels equals the
  90product of the parts' weights.  That is a better place for the debt to sit, because
  91recognition cost is additive over independent parts, which supplies the right-hand
  92side for free; the open question is whether the ledger supplies the interleaving count
  93on the left.
  94
  95**OPEN:** derivation of the gluing law from recognition structure.
  96`Gap2LedgerSiteBlindness` blocks one route, reading the measure off ledger cost values
  97under a free encoding.  Note the scope: that is a proof of *underdetermination* by cost
  98values, not a proof that no cost-based argument exists.  A second route the review
  99named and nobody has attacked: stationarity of the ledger's own *move set* under
 100insertion, which would force `π(N+1)/π(N) = 1/(N+1)` from equirated names rather than
 101from any cost value.
 102
 103**Strength.**  The identification is an equality of natural numbers, not an agreement
 104to a tolerance, and the uniqueness in §6 quantifies over every relabeling-invariant
 105real weight.  But that uniqueness inherits its absolute normalization from the equality
 106form of `GaugeCountingPrinciple`: replace the equality by `∃ λ > 0` and a one-parameter
 107family per sector survives.  The absence of a free scale is bookkeeping, not rigidity.
 108
 109**Refuted objection, recorded for the next reader.**  The review's highest-confidence
 110single claim (0.8) was that `nE!` and `nT!` are artifacts of a carrier without
 111well-formedness conditions, and that imposing injectivity on `edgeVerts` and `tetVerts`
 112would collapse `pairCount` to `nV!`.  The carrier does indeed carry no such conditions,
 113but the inference fails, and `QG/attack_gap2_20260728/rigidity_probe.lean` refutes it
 114with a compiled witness: a complex with injective `edgeVerts` and `tetVerts` whose pair
 115count is `4`, not `nV! = 2`.  The reason is that `pairCount` ranges over *targets*, and
 116permuting cell names produces a different target; injectivity pins `eEquiv` only with
 117the target held fixed, which is `Aut K`, not the pair space.
 118
 119## Proof notes
 120No `decide` / `native_decide`; the bijection to the sector group is explicit.
 121The dependent-size transport is discharged by destructuring the target complex
 122and substituting the three size equalities, after which every cast is `rfl`.
 123-/
 124
 125namespace IndisputableMonolith
 126namespace Gravity
 127namespace SevenGaps
 128namespace Gap2GaugeVolume
 129
 130open PathSumMeasure
 131open ExactShellGaugePreflight
 132
 133variable {B : ℕ}
 134
 135/-! ## §1. Index sizes are relabeling invariants -/
 136
 137/-- A relabeling forces equal vertex counts. -/
 138theorem size_v {K K' : BoundedComplex B} (r : Relabel K K') : K.nV = K'.nV := by
 139  simpa using Fintype.card_congr r.vEquiv
 140
 141/-- A relabeling forces equal edge counts. -/
 142theorem size_e {K K' : BoundedComplex B} (r : Relabel K K') : K.nE = K'.nE := by
 143  simpa using Fintype.card_congr r.eEquiv
 144
 145/-- A relabeling forces equal tetrahedron counts. -/
 146theorem size_t {K K' : BoundedComplex B} (r : Relabel K K') : K.nT = K'.nT := by
 147  simpa using Fintype.card_congr r.tEquiv
 148
 149/-! ## §2. The relabeling group of a size sector, and the pushforward -/
 150
 151/-- The relabeling group of `K`'s size sector: independent permutations of the
 152vertex, edge and tetrahedron index sets.  This is the gauge group of the
 153labeling, and nothing about `K` beyond its three sizes enters. -/
 154abbrev SectorGroup (K : BoundedComplex B) : Type :=
 155  Equiv.Perm (Fin K.nV) × Equiv.Perm (Fin K.nE) × Equiv.Perm (Fin K.nT)
 156
 157/-- Pushforward of `K` along a triple of index permutations: relabel the data,
 158keep the sizes. -/
 159def push (K : BoundedComplex B) (g : SectorGroup K) : BoundedComplex B where
 160  nV := K.nV
 161  nE := K.nE
 162  nT := K.nT
 163  hV := K.hV
 164  hE := K.hE
 165  hT := K.hT
 166  edgeVerts := fun e => Prod.map g.1 g.1 (K.edgeVerts (g.2.1.symm e))
 167  tetVerts := fun t i => g.1 (K.tetVerts (g.2.2.symm t) i)
 168
 169/-- The canonical relabeling witness from `K` onto its pushforward. -/
 170def pushRel (K : BoundedComplex B) (g : SectorGroup K) : Relabel K (push K g) where
 171  vEquiv := g.1
 172  eEquiv := g.2.1
 173  tEquiv := g.2.2
 174  edge_comm := by intro e; simp [push]
 175  tet_comm := by intro t i; simp [push]
 176
 177/-- Every pushforward is gauge-equivalent to the original. -/
 178theorem equivalent_push (K : BoundedComplex B) (g : SectorGroup K) :
 179    Equivalent K (push K g) := ⟨pushRel K g⟩
 180
 181/-! ## §3. The (target, witness) pair space is the sector group
 182
 183The bijection is the mathematical content of this module: a pair
 184`(K', r : Relabel K K')` is *nothing more* than a triple of index
 185permutations, because the commutation conditions pin `K'` to be the
 186pushforward of `K` along that triple. -/
 187
 188/-- The total space of (target, witness) pairs out of `K`. -/
 189abbrev PairSpace (K : BoundedComplex B) : Type := Σ K' : BoundedComplex B, Relabel K K'
 190
 191/-- Restricting the target to the orbit changes nothing: the witness type is
 192empty off the orbit, and on the orbit the subtype proof is irrelevant. -/
 193def pairSpaceEquiv (K : BoundedComplex B) :
 194    (Σ K' : {K' : BoundedComplex B // Equivalent K K'}, Relabel K K'.val) ≃ PairSpace K where
 195  toFun p := ⟨p.1.val, p.2⟩
 196  invFun p := ⟨⟨p.1, ⟨p.2⟩⟩, p.2⟩
 197  left_inv p := by obtain ⟨⟨K', h⟩, r⟩ := p; rfl
 198  right_inv p := by obtain ⟨K', r⟩ := p; rfl
 199
 200/-- A size equality that is reflexive transports trivially. -/
 201theorem finCongr_self {n : ℕ} (h : n = n) : finCongr h = Equiv.refl (Fin n) := by
 202  ext x
 203  simp
 204
 205/-- Read a witness as an element of the sector group: legitimate because the
 206sizes agree (§1). -/
 207def toSector {K : BoundedComplex B} (p : PairSpace K) : SectorGroup K :=
 208  (p.2.vEquiv.trans (finCongr (size_v p.2)).symm,
 209   p.2.eEquiv.trans (finCongr (size_e p.2)).symm,
 210   p.2.tEquiv.trans (finCongr (size_t p.2)).symm)
 211
 212/-- Build a pair from a sector group element by pushing forward. -/
 213def ofSector (K : BoundedComplex B) (g : SectorGroup K) : PairSpace K :=
 214  ⟨push K g, pushRel K g⟩
 215
 216theorem toSector_ofSector (K : BoundedComplex B) (g : SectorGroup K) :
 217    toSector (ofSector K g) = g :=
 218  Prod.ext (Equiv.ext fun _ => Fin.ext rfl)
 219    (Prod.ext (Equiv.ext fun _ => Fin.ext rfl) (Equiv.ext fun _ => Fin.ext rfl))
 220
 221/-- **The pinning lemma.**  A relabeling witness determines its own target: the
 222commutation conditions force `K'` to be the pushforward of `K` along the
 223witness's index permutations.  Stated with value-level hypotheses (`Fin.val`)
 224so that no dependent-size transport appears in the statement. -/
 225theorem target_eq_push {K K' : BoundedComplex B} (r : Relabel K K') (g : SectorGroup K)
 226    (hv : ∀ x : Fin K.nV, (r.vEquiv x).val = (g.1 x).val)
 227    (he : ∀ x : Fin K.nE, (r.eEquiv x).val = (g.2.1 x).val)
 228    (ht : ∀ x : Fin K.nT, (r.tEquiv x).val = (g.2.2 x).val) :
 229    K' = push K g := by
 230  have hnv : K.nV = K'.nV := size_v r
 231  have hne : K.nE = K'.nE := size_e r
 232  have hnt : K.nT = K'.nT := size_t r
 233  obtain ⟨nV', nE', nT', hV', hE', hT', ev', tv'⟩ := K'
 234  subst hnv
 235  subst hne
 236  subst hnt
 237  have hvv : ∀ z, r.vEquiv z = g.1 z := fun z => Fin.ext (hv z)
 238  have hev : ev' = fun x => Prod.map g.1 g.1 (K.edgeVerts (g.2.1.symm x)) := by
 239    funext x
 240    have hx : r.eEquiv (g.2.1.symm x) = x := by
 241      apply Fin.ext
 242      rw [he]
 243      simp
 244    have h : ev' x = Prod.map r.vEquiv r.vEquiv (K.edgeVerts (g.2.1.symm x)) := by
 245      have h0 := r.edge_comm (g.2.1.symm x)
 246      rw [hx] at h0
 247      exact h0
 248    rw [h]
 249    simp [Prod.map, hvv]
 250  have htv : tv' = fun x i => g.1 (K.tetVerts (g.2.2.symm x) i) := by
 251    funext x i
 252    have hx : r.tEquiv (g.2.2.symm x) = x := by
 253      apply Fin.ext
 254      rw [ht]
 255      simp
 256    have h : tv' x i = r.vEquiv (K.tetVerts (g.2.2.symm x) i) := by
 257      have h0 := r.tet_comm (g.2.2.symm x) i
 258      rw [hx] at h0
 259      exact h0
 260    rw [h, hvv]
 261  rw [hev, htv]
 262  rfl
 263
 264theorem ofSector_toSector (K : BoundedComplex B) (p : PairSpace K) :
 265    ofSector K (toSector p) = p := by
 266  obtain ⟨K', r⟩ := p
 267  obtain ⟨g, hg⟩ : ∃ g : SectorGroup K, g = toSector (⟨K', r⟩ : PairSpace K) := ⟨_, rfl⟩
 268  have hv : ∀ x : Fin K.nV, (r.vEquiv x).val = (g.1 x).val := by
 269    intro x; rw [hg]; rfl
 270  have he : ∀ x : Fin K.nE, (r.eEquiv x).val = (g.2.1 x).val := by
 271    intro x; rw [hg]; rfl
 272  have ht : ∀ x : Fin K.nT, (r.tEquiv x).val = (g.2.2 x).val := by
 273    intro x; rw [hg]; rfl
 274  have hK : K' = push K g := target_eq_push r g hv he ht
 275  subst hK
 276  have hrel : pushRel K g = r :=
 277    Relabel.ext (Equiv.ext fun x => (Fin.ext (hv x)).symm)
 278      (Equiv.ext fun x => (Fin.ext (he x)).symm)
 279      (Equiv.ext fun x => (Fin.ext (ht x)).symm)
 280  rw [← hg]
 281  exact congrArg (fun w => (⟨push K g, w⟩ : PairSpace K)) hrel
 282
 283/-- **THEOREM (the pair space is the gauge group).**  The (target, witness)
 284pairs out of `K` are in explicit bijection with the triples of index
 285permutations. -/
 286def sectorEquiv (K : BoundedComplex B) : PairSpace K ≃ SectorGroup K where
 287  toFun := toSector
 288  invFun := ofSector K
 289  left_inv := ofSector_toSector K
 290  right_inv := toSector_ofSector K
 291
 292/-! ## §4. The gauge volume is a factorial -/
 293
 294/-- The order of the sector group. -/
 295theorem card_sectorGroup (K : BoundedComplex B) :
 296    Nat.card (SectorGroup K)
 297      = Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) := by
 298  simp [Nat.card_eq_fintype_card, Fintype.card_perm]
 299
 300/-- **THEOREM (the gauge volume is the sector group order).**  The quantity
 301`ExactShellGaugePreflight` calls the gauge volume of `K`'s orbit is exactly
 302`nV! * nE! * nT!`: the number of ways to label the index sets.  It contains no
 303information about the incidence data of `K`. -/
 304theorem pairCount_eq_factorials (K : BoundedComplex B) :
 305    pairCount K = Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) := by
 306  unfold pairCount
 307  rw [Nat.card_congr (pairSpaceEquiv K), Nat.card_congr (sectorEquiv K), card_sectorGroup]
 308
 309/-- **COROLLARY.**  The gauge volume is a function of the three index sizes
 310alone.  So dividing by it cannot express a physical choice about the complex;
 311it is a normalization of the label count. -/
 312theorem pairCount_congr_sizes {K K' : BoundedComplex B}
 313    (hV : K.nV = K'.nV) (hE : K.nE = K'.nE) (hT : K.nT = K'.nT) :
 314    pairCount K = pairCount K' := by
 315  rw [pairCount_eq_factorials, pairCount_eq_factorials, hV, hE, hT]
 316
 317/-- **THEOREM (orbit-stabilizer, sector form).**  Labeled presentations times
 318automorphisms equals labelings. -/
 319theorem orbitCard_mul_autCard (K : BoundedComplex B) :
 320    gaugeOrbitCard K * Nat.card (Aut K)
 321      = Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) := by
 322  rw [← pairCount_eq_orbitCard_mul_autCard, pairCount_eq_factorials]
 323
 324/-! ## §5. The premise, named: label indifference -/
 325
 326/-- The **label density** of `K`: the number of distinct labeled complexes in `K`'s
 327class, divided by the number of relabelings available in the sector.  Written with no
 328reference to `Aut`, `mu`, or relabeling witnesses: only orbit size and the factorials
 329of the index sizes.
 330
 331**Not a probability.**  Adversarial review (2026-07-28) correctly flagged an earlier
 332gloss here, "the fraction of available labelings that present the class", as false:
 333`equivalent_push` proves every sector permutation sends `K` to a complex in the same
 334class, so that fraction is `1`.  The numerator counts *objects* and the denominator
 335counts *transformations*, which is groupoid cardinality, not a fraction of a sample
 336space. -/
 337noncomputable def labelDensity (K : BoundedComplex B) : ℝ :=
 338  (gaugeOrbitCard K : ℝ)
 339    / ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 340
 341/-- **THEOREM (Gibbs identification).**  The label density is exactly the
 342symmetry-factor measure: `|orbit| / (number of labelings) = 1/|Aut|`. -/
 343theorem labelDensity_eq_mu (K : BoundedComplex B) : labelDensity K = mu K := by
 344  have hpos : (0 : ℝ) < (gaugeOrbitCard K : ℝ) := by
 345    exact_mod_cast gaugeOrbitCard_pos K
 346  unfold labelDensity mu
 347  rw [← orbitCard_mul_autCard K, Nat.cast_mul, div_mul_eq_div_div, div_self hpos.ne']
 348
 349/-- **THEOREM (premise identification).**  The gauge-counting principle, the
 350undischarged MODEL premise of the Gap-2 measure derivation, holds exactly when the
 351class weight is the label density: the orbit's size over the sector's relabeling
 352count, stated without `Aut`, `mu`, or witnesses.
 353
 354This is an equivalence of two ways of writing the same premise, so it identifies the
 355premise without discharging it.  §6c proves that the name "label indifference"
 356undershoots it. -/
 357theorem gaugeCounting_iff_labelIndifference (ν : TriangulationClass B → ℝ) :
 358    MeasureSubstrateBlocker.GaugeCountingPrinciple ν ↔
 359      ∀ K : BoundedComplex B,
 360        ν (Quotient.mk (relabelSetoid B) K) = labelDensity K := by
 361  rw [MeasureSubstrateBlocker.gaugeCountingPrinciple_iff_mu_on_representatives]
 362  constructor
 363  · intro h K
 364    rw [h K, labelDensity_eq_mu]
 365  · intro h K
 366    rw [h K, labelDensity_eq_mu]
 367
 368/-- **THEOREM (the gauge volume carries no incidence information).**  Two complexes
 369with the same index sizes are divided by the same gauge volume, so the divisor cannot
 370express any choice that distinguishes complexes *within* a size sector.
 371
 372**This does not make the divisor inert**, and an earlier docstring here claimed it
 373did.  A size-only divisor is exactly a reweighting *between* sectors, which in a
 374discrete path sum is physically consequential: it competes with the bare cosmological
 375constant.  §6c gives the surviving freedom in closed form. -/
 376theorem gaugeVolume_is_size_data (K K' : BoundedComplex B)
 377    (hV : K.nV = K'.nV) (hE : K.nE = K'.nE) (hT : K.nT = K'.nT) :
 378    pairCount K = pairCount K' ∧
 379      pairCount K = Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) :=
 380  ⟨pairCount_congr_sizes hV hE hT, pairCount_eq_factorials K⟩
 381
 382/-! ## §6. The premise at the substrate level: the Gibbs weight
 383
 384§5 states the premise as a property of the class weight.  The substrate does not
 385work with classes: it works with labeled configurations.  So the question is
 386which *labeled* weight induces the RS measure.  The answer is unique and it is
 387the Gibbs weight: each labeled complex enters with the reciprocal of the number
 388of ways to label it. -/
 389
 390open scoped Classical in
 391/-- The class mass induced by a labeled weight: the total weight of the labeled
 392configurations that present the class. -/
 393noncomputable def classMass (w : BoundedComplex B → ℝ) (c : TriangulationClass B) : ℝ :=
 394  ∑ K : BoundedComplex B, if Quotient.mk (relabelSetoid B) K = c then w K else 0
 395
 396/-- A class representative is equivalent to any complex presenting the class. -/
 397theorem equivalent_out (K : BoundedComplex B) :
 398    Equivalent (Quotient.out (Quotient.mk (relabelSetoid B) K)) K :=
 399  Quotient.exact (Quotient.out_eq (Quotient.mk (relabelSetoid B) K))
 400
 401/-- The number of labeled complexes presenting a class is the orbit count. -/
 402theorem fiber_card (c : TriangulationClass B) :
 403    Nat.card {K : BoundedComplex B // Quotient.mk (relabelSetoid B) K = c}
 404      = orbitCardClass c := by
 405  have hc : Quotient.mk (relabelSetoid B) (Quotient.out c) = c := Quotient.out_eq c
 406  have e : {K : BoundedComplex B // Quotient.mk (relabelSetoid B) K = c}
 407      ≃ {K' : BoundedComplex B // Equivalent (Quotient.out c) K'} :=
 408    Equiv.subtypeEquivRight fun K =>
 409      ⟨fun hK => Quotient.exact (hc.trans hK.symm),
 410       fun hE => (Quotient.sound hE).symm.trans hc⟩
 411  rw [Nat.card_congr e]
 412  conv_rhs => rw [← hc]
 413  rfl
 414
 415/-- **THEOREM.**  A relabeling-invariant labeled weight induces the class mass
 416`orbit size times the common weight of the orbit`. -/
 417theorem classMass_of_invariant (w : BoundedComplex B → ℝ)
 418    (hinv : ∀ K K', Equivalent K K' → w K = w K') (c : TriangulationClass B) :
 419    classMass w c = (orbitCardClass c : ℝ) * w (Quotient.out c) := by
 420  classical
 421  have hc : Quotient.mk (relabelSetoid B) (Quotient.out c) = c := Quotient.out_eq c
 422  have hstep : ∀ K : BoundedComplex B,
 423      (if Quotient.mk (relabelSetoid B) K = c then w K else 0)
 424        = (if Quotient.mk (relabelSetoid B) K = c then (1 : ℝ) else 0)
 425            * w (Quotient.out c) := by
 426    intro K
 427    by_cases h : Quotient.mk (relabelSetoid B) K = c
 428    · simp only [h, if_true, one_mul]
 429      exact hinv K (Quotient.out c) (Quotient.exact (h.trans hc.symm))
 430    · simp only [h, if_false, zero_mul]
 431  have hcount : ∑ K : BoundedComplex B,
 432      (if Quotient.mk (relabelSetoid B) K = c then (1 : ℝ) else 0)
 433        = (orbitCardClass c : ℝ) := by
 434    rw [Finset.sum_boole, ← fiber_card c, Nat.card_eq_fintype_card, Fintype.card_subtype]
 435  unfold classMass
 436  rw [Finset.sum_congr rfl fun K _ => hstep K, ← Finset.sum_mul, hcount]
 437
 438/-- The **Gibbs weight** of a labeled complex: one unit of recognition shared
 439evenly over the ways of labeling it.  This is the premise, stated at the
 440substrate level, with no reference to automorphisms, orbits, or classes. -/
 441noncomputable def gibbsWeight (K : BoundedComplex B) : ℝ :=
 442  1 / ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 443
 444/-- The Gibbs weight is relabeling-invariant, because the index sizes are. -/
 445theorem gibbsWeight_invariant {K K' : BoundedComplex B} (h : Equivalent K K') :
 446    gibbsWeight K = gibbsWeight K' := by
 447  obtain ⟨r⟩ := h
 448  unfold gibbsWeight
 449  rw [size_v r, size_e r, size_t r]
 450
 451theorem gaugeVolume_pos (K : BoundedComplex B) :
 452    (0 : ℝ) < ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) := by
 453  have h : 0 < Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) :=
 454    Nat.mul_pos K.nV.factorial_pos (Nat.mul_pos K.nE.factorial_pos K.nT.factorial_pos)
 455  exact_mod_cast h
 456
 457/-- **THEOREM (substrate premise, sufficiency).**  The Gibbs weight induces
 458exactly the RS path-sum measure: its class mass satisfies the gauge-counting
 459principle, hence equals `1/|Aut|` on every class. -/
 460theorem gibbs_induces_measure (B : ℕ) :
 461    MeasureSubstrateBlocker.GaugeCountingPrinciple
 462      (classMass (gibbsWeight : BoundedComplex B → ℝ)) := by
 463  intro c
 464  rw [classMass_of_invariant _ (fun _ _ h => gibbsWeight_invariant h) c]
 465  have hK := Quotient.out_eq c
 466  have hpc : (pairCountClass c : ℝ)
 467      = ((Nat.factorial (Quotient.out c).nV
 468          * (Nat.factorial (Quotient.out c).nE * Nat.factorial (Quotient.out c).nT) : ℕ) : ℝ) := by
 469    conv_lhs => rw [← hK]
 470    rw [pairCountClass_mk, pairCount_eq_factorials]
 471  rw [hpc]
 472  unfold gibbsWeight
 473  field_simp
 474
 475/-- **THEOREM (substrate premise, uniqueness).**  Among relabeling-invariant
 476labeled weights, the Gibbs weight is the ONLY one whose class mass satisfies the
 477gauge-counting principle.  So the premise behind the Gap-2 measure is exactly:
 478a labeled configuration carries the reciprocal of its label count. -/
 479theorem invariant_weight_gives_measure_iff (w : BoundedComplex B → ℝ)
 480    (hinv : ∀ K K', Equivalent K K' → w K = w K') :
 481    MeasureSubstrateBlocker.GaugeCountingPrinciple (classMass w) ↔
 482      ∀ K : BoundedComplex B, w K = gibbsWeight K := by
 483  constructor
 484  · intro h K
 485    have hc := h (Quotient.mk (relabelSetoid B) K)
 486    rw [classMass_of_invariant w hinv] at hc
 487    have hwout : w (Quotient.out (Quotient.mk (relabelSetoid B) K)) = w K :=
 488      hinv _ _ (equivalent_out K)
 489    rw [hwout, pairCountClass_mk, pairCount_eq_factorials, orbitCardClass_mk] at hc
 490    have horb : (0 : ℝ) < (gaugeOrbitCard K : ℝ) := by
 491      exact_mod_cast gaugeOrbitCard_pos K
 492    have hvol := gaugeVolume_pos K
 493    have h1 : (gaugeOrbitCard K : ℝ)
 494        * (w K * ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ))
 495        = (gaugeOrbitCard K : ℝ) * 1 := by
 496      rw [mul_one, ← mul_assoc]
 497      exact hc
 498    have h2 := mul_left_cancel₀ horb.ne' h1
 499    unfold gibbsWeight
 500    rw [eq_div_iff hvol.ne']
 501    exact h2
 502  · intro h
 503    have hw : w = (gibbsWeight : BoundedComplex B → ℝ) := funext h
 504    rw [hw]
 505    exact gibbs_induces_measure B
 506
 507/-- **THEOREM (the premise in one line).**  The RS path-sum measure is uniform
 508labeled counting divided by the number of labelings.  `classMass (fun _ => 1)` is
 509the count of labeled presentations of the class, and multiplying the Gibbs class
 510mass by the sector's gauge volume returns exactly that count.  This is the
 511discrete Faddeev-Popov statement: sum over labeled configurations, divide once by
 512the gauge volume. -/
 513theorem measure_is_uniform_count_over_gauge_volume (c : TriangulationClass B) :
 514    classMass (gibbsWeight : BoundedComplex B → ℝ) c
 515        * ((Nat.factorial (Quotient.out c).nV
 516            * (Nat.factorial (Quotient.out c).nE
 517              * Nat.factorial (Quotient.out c).nT) : ℕ) : ℝ)
 518      = classMass (fun _ => (1 : ℝ)) c := by
 519  rw [classMass_of_invariant _ (fun _ _ h => gibbsWeight_invariant h) c,
 520    classMass_of_invariant _ (fun _ _ _ => rfl) c]
 521  have hvol := gaugeVolume_pos (Quotient.out c)
 522  unfold gibbsWeight
 523  field_simp
 524
 525/-! ## §6b. Where the premise actually bites: across sectors, not inside one
 526
 527The premise is often read as answering "why `1/|Aut|` and not the uniform class
 528weight".  Inside one size sector it does not have to: the ratio of two class
 529weights is forced to be the ratio of their labeled-presentation counts, which is
 530what one posting per labeled configuration already gives, with no normalization
 531chosen.  What the premise fixes is the RELATIVE normalization of different size
 532sectors, and that factor is the ratio of gauge volumes. -/
 533
 534/-- **THEOREM (inside a sector the measure is uniform labeled counting).**  If `ν`
 535satisfies the gauge-counting principle then for any two complexes with the same
 536index sizes the class weights are in the ratio of the labeled-presentation
 537counts.  No normalization enters: this is exactly what counting labeled
 538configurations equally gives. -/
 539theorem sector_ratio_is_orbit_ratio (ν : TriangulationClass B → ℝ)
 540    (h : MeasureSubstrateBlocker.GaugeCountingPrinciple ν)
 541    (K K' : BoundedComplex B)
 542    (hV : K.nV = K'.nV) (hE : K.nE = K'.nE) (hT : K.nT = K'.nT) :
 543    ν (Quotient.mk (relabelSetoid B) K) * (gaugeOrbitCard K' : ℝ)
 544      = ν (Quotient.mk (relabelSetoid B) K') * (gaugeOrbitCard K : ℝ) := by
 545  have hk := h (Quotient.mk (relabelSetoid B) K)
 546  have hk' := h (Quotient.mk (relabelSetoid B) K')
 547  rw [pairCountClass_mk, orbitCardClass_mk, pairCount_eq_factorials] at hk
 548  rw [pairCountClass_mk, orbitCardClass_mk, pairCount_eq_factorials] at hk'
 549  rw [hV, hE, hT] at hk
 550  have hvol := gaugeVolume_pos K'
 551  have h1 : (ν (Quotient.mk (relabelSetoid B) K) * (gaugeOrbitCard K' : ℝ))
 552      * ((Nat.factorial K'.nV * (Nat.factorial K'.nE * Nat.factorial K'.nT) : ℕ) : ℝ)
 553      = (ν (Quotient.mk (relabelSetoid B) K') * (gaugeOrbitCard K : ℝ))
 554      * ((Nat.factorial K'.nV * (Nat.factorial K'.nE * Nat.factorial K'.nT) : ℕ) : ℝ) := by
 555    calc (ν (Quotient.mk (relabelSetoid B) K) * (gaugeOrbitCard K' : ℝ))
 556          * ((Nat.factorial K'.nV * (Nat.factorial K'.nE * Nat.factorial K'.nT) : ℕ) : ℝ)
 557        = (ν (Quotient.mk (relabelSetoid B) K)
 558            * ((Nat.factorial K'.nV
 559                * (Nat.factorial K'.nE * Nat.factorial K'.nT) : ℕ) : ℝ))
 560          * (gaugeOrbitCard K' : ℝ) := by ring
 561      _ = (gaugeOrbitCard K : ℝ) * (gaugeOrbitCard K' : ℝ) := by rw [hk]
 562      _ = (ν (Quotient.mk (relabelSetoid B) K')
 563            * ((Nat.factorial K'.nV
 564                * (Nat.factorial K'.nE * Nat.factorial K'.nT) : ℕ) : ℝ))
 565          * (gaugeOrbitCard K : ℝ) := by rw [hk']; ring
 566      _ = _ := by ring
 567  exact mul_right_cancel₀ hvol.ne' h1
 568
 569/-- **THEOREM (what the premise adds).**  The class weight given by one posting
 570per labeled configuration is the labeled-presentation count, and it equals the
 571gauge-counting weight multiplied by the sector's gauge volume.  So the entire
 572content of the premise beyond within-sector counting is the cross-sector factor
 573`1/(nV! nE! nT!)`, which is extensive in the index sizes and is therefore the
 574kind of term an action carries, not a statement about the class. -/
 575theorem uniformLabeled_eq_mu_times_gaugeVolume (K : BoundedComplex B) :
 576    (gaugeOrbitCard K : ℝ)
 577      = mu K * ((Nat.factorial K.nV
 578          * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) := by
 579  have haut : (0 : ℝ) < (Nat.card (Aut K) : ℝ) := by exact_mod_cast autCard_pos K
 580  have hfact : ((Nat.factorial K.nV
 581      * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 582      = (gaugeOrbitCard K : ℝ) * (Nat.card (Aut K) : ℝ) := by
 583    rw [← orbitCard_mul_autCard K]
 584    push_cast
 585    ring
 586  rw [hfact]
 587  unfold mu
 588  field_simp
 589
 590/-! ## §6c. The exact residual freedom: one number per size sector
 591
 592An adversarial review of this module (2026-07-28, four independent seats at maximum
 593effort) returned the same objection from all four, and it lands.  `pairCount_congr_sizes`
 594shows the divisor carries no incidence information, but it does **not** follow that
 595dividing by it is physically inert, because a size-dependent normalization reweights
 596whole size sectors against each other, and in a discrete gravity path sum the
 597size-dependence of the measure competes with the bare cosmological constant.
 598
 599Two seats independently prescribed the same repair: formalize the family of weights
 600that label indifference actually permits, and prove that the gauge-counting principle
 601is the single member with unit normalization.  That is what this section does.  The
 602conclusion is that "label indifference" **undershoots** the premise: every member of
 603the family below is relabeling-invariant, so indifference does not select one. -/
 604
 605/-- A **sector fugacity**: any assignment of a real number to the three index sizes.
 606Divided by the gauge volume it gives a labeled weight. -/
 607noncomputable def fugacityWeight (a : ℕ → ℕ → ℕ → ℝ) (K : BoundedComplex B) : ℝ :=
 608  a K.nV K.nE K.nT
 609    / ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 610
 611/-- **THEOREM (indifference does not constrain the fugacity).**  Every sector
 612fugacity gives a relabeling-invariant labeled weight.  So label indifference in the
 613honest sense, that the weight is a class function, is satisfied by the whole family
 614and cannot pick out the Gibbs weight. -/
 615theorem fugacityWeight_invariant (a : ℕ → ℕ → ℕ → ℝ) {K K' : BoundedComplex B}
 616    (h : Equivalent K K') : fugacityWeight a K = fugacityWeight a K' := by
 617  obtain ⟨r⟩ := h
 618  unfold fugacityWeight
 619  rw [size_v r, size_e r, size_t r]
 620
 621/-- The Gibbs weight is the member of the family with fugacity identically one. -/
 622theorem gibbsWeight_eq_fugacity_one (K : BoundedComplex B) :
 623    gibbsWeight K = fugacityWeight (fun _ _ _ => (1 : ℝ)) K := rfl
 624
 625/-- The class mass of a sector-fugacity weight is the fugacity times the RS
 626measure. -/
 627theorem classMass_fugacity_mk (a : ℕ → ℕ → ℕ → ℝ) (K : BoundedComplex B) :
 628    classMass (fugacityWeight a) (Quotient.mk (relabelSetoid B) K)
 629      = a K.nV K.nE K.nT * mu K := by
 630  rw [classMass_of_invariant _ (fun _ _ h => fugacityWeight_invariant a h) _,
 631    fugacityWeight_invariant a (equivalent_out K), orbitCardClass_mk]
 632  unfold fugacityWeight
 633  rw [← labelDensity_eq_mu]
 634  unfold labelDensity
 635  ring
 636
 637/-- The RS measure is strictly positive, so it can be cancelled. -/
 638theorem mu_pos (K : BoundedComplex B) : 0 < mu K := by
 639  unfold mu
 640  have h : (0 : ℝ) < (Nat.card (Aut K) : ℝ) := by exact_mod_cast autCard_pos K
 641  exact one_div_pos.mpr h
 642
 643/-- **THEOREM (the premise, named exactly).**  The gauge-counting principle holds for
 644a sector-fugacity weight exactly when the fugacity is one in every sector that is
 645actually occupied.  Combined with `fugacityWeight_invariant`, this says precisely
 646what the undischarged premise is: not indifference to labels, which the whole family
 647has, but the choice of **unit cross-sector fugacity**.  That is one positive real per
 648size sector, set to one by fiat. -/
 649theorem gaugeCounting_iff_fugacity_one (a : ℕ → ℕ → ℕ → ℝ) :
 650    MeasureSubstrateBlocker.GaugeCountingPrinciple
 651        (classMass (B := B) (fugacityWeight (B := B) a))
 652      ↔ ∀ K : BoundedComplex B, a K.nV K.nE K.nT = 1 := by
 653  rw [gaugeCounting_iff_labelIndifference]
 654  constructor
 655  · intro h K
 656    have hK := h K
 657    rw [classMass_fugacity_mk, labelDensity_eq_mu] at hK
 658    have := mu_pos K
 659    field_simp at hK
 660    exact hK
 661  · intro h K
 662    rw [classMass_fugacity_mk, labelDensity_eq_mu, h K, one_mul]
 663
 664/-- **THEOREM (the freedom is unsplittable).**  A sector fugacity can be moved out of
 665the measure and into the action without changing any weighted sum: reweighting the
 666measure by `a` is the same as shifting the action by `-log a`.  So "the measure is
 667forced" holds only relative to a convention about where the sector factor is booked;
 668only the product of measure and Boltzmann factor is determined. -/
 669theorem fugacity_absorbs_into_action (a : ℕ → ℕ → ℕ → ℝ) (S : BoundedComplex B → ℝ)
 670    (K : BoundedComplex B) (ha : 0 < a K.nV K.nE K.nT) :
 671    fugacityWeight a K * Real.exp (-S K)
 672      = gibbsWeight K
 673        * Real.exp (-(S K - Real.log (a K.nV K.nE K.nT))) := by
 674  have hvol : (0 : ℝ)
 675      < ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) :=
 676    gaugeVolume_pos K
 677  unfold fugacityWeight gibbsWeight
 678  rw [neg_sub, Real.exp_sub, Real.exp_log ha, Real.exp_neg]
 679  ring
 680
 681/-! ## §6d. Reducing the premise: gluing multiplicativity forces the factorial
 682
 683§6c leaves the premise as "the sector fugacity is one", which is a bare choice.  Two
 684seats of the adversarial review converged independently on the one route they judged
 685to *close* rather than relocate: the factorial is the unique solution of a shuffle
 686identity, so the premise can be transmuted into a **locality** axiom about assembling
 687configurations from parts.
 688
 689Read `f n` as the weight carried by one index set of size `n`.  The gluing law says:
 690take a configuration of size `m + n` that is assembled from a part of size `m` and a
 691part of size `n`.  There are `C(m+n, m)` ways to interleave the two blocks of labels
 692into the combined index set.  The law asserts that the assembled weight, multiplied by
 693the number of interleavings, is the product of the parts' weights.  That is
 694multiplicativity of the weight under disjoint union, with the label bookkeeping done
 695honestly, and it is a statement about how independent parts compose rather than a
 696choice of normalization.
 697
 698This is a **reduction, not a discharge**: the gluing law is itself unproved from
 699recognition structure.  What changes is the shape of the debt.  Cost in a recognition
 700ledger is additive over independent parts, so a weight of the form `exp(-cost)` is
 701multiplicative over independent parts, which is the right-hand side of the shuffle
 702identity for free.  The open question becomes whether the ledger supplies the
 703interleaving count on the left, which is a question about how the ledger individuates
 704labels and is the kind of question `Gap2LedgerSiteBlindness` does not block. -/
 705
 706/-- A **gluing law** for a size-indexed weight.  `unit`: the empty index set carries
 707weight one.  `atom`: a single label carries weight one, fixing the scale.  `shuffle`:
 708assembling a size-`m` part and a size-`n` part is multiplicative once the `C(m+n, m)`
 709interleavings of the label blocks are counted. -/
 710structure GluingLaw (f : ℕ → ℝ) : Prop where
 711  unit : f 0 = 1
 712  atom : f 1 = 1
 713  shuffle : ∀ m n : ℕ, f (m + n) * (Nat.choose (m + n) m : ℝ) = f m * f n
 714
 715/-- **THEOREM (the gluing law forces the factorial).**  The inverse factorial is the
 716unique size-indexed weight satisfying the gluing law.  So "divide by the number of
 717labelings" is not an independent convention: it is the only weight that composes
 718multiplicatively under gluing. -/
 719theorem gluingLaw_forces_inverse_factorial {f : ℕ → ℝ} (h : GluingLaw f) :
 720    ∀ n : ℕ, f n = 1 / (Nat.factorial n : ℝ) := by
 721  intro n
 722  induction n with
 723  | zero => simpa using h.unit
 724  | succ k ih =>
 725      have hs := h.shuffle k 1
 726      rw [h.atom, mul_one, Nat.choose_succ_self_right] at hs
 727      have hk1 : (0 : ℝ) < ((k : ℝ) + 1) := by positivity
 728      have hfact : (0 : ℝ) < (Nat.factorial k : ℝ) := by
 729        exact_mod_cast Nat.factorial_pos k
 730      have hcast : ((k + 1 : ℕ) : ℝ) = (k : ℝ) + 1 := by push_cast; ring
 731      rw [hcast] at hs
 732      have hval : f (k + 1) = f k / ((k : ℝ) + 1) :=
 733        eq_div_of_mul_eq hk1.ne' hs
 734      rw [hval, ih, Nat.factorial_succ]
 735      push_cast
 736      field_simp
 737
 738/-- The Gibbs weight is the product of one inverse factorial per index set. -/
 739theorem gibbsWeight_factorizes (K : BoundedComplex B) :
 740    gibbsWeight K
 741      = (1 / (Nat.factorial K.nV : ℝ)) * (1 / (Nat.factorial K.nE : ℝ))
 742        * (1 / (Nat.factorial K.nT : ℝ)) := by
 743  unfold gibbsWeight
 744  push_cast
 745  field_simp
 746
 747/-- **THEOREM (the premise reduces to gluing).**  Any size-indexed weight satisfying
 748the gluing law induces, index set by index set, exactly the Gibbs weight.  Combined
 749with `gibbs_induces_measure` this means the gluing law *implies* the gauge-counting
 750principle, so the unit-fugacity choice of §6c is discharged by a locality axiom rather
 751than asserted. -/
 752theorem gluingLaw_gives_gibbsWeight {f : ℕ → ℝ} (h : GluingLaw f)
 753    (K : BoundedComplex B) :
 754    f K.nV * f K.nE * f K.nT = gibbsWeight K := by
 755  rw [gluingLaw_forces_inverse_factorial h K.nV,
 756    gluingLaw_forces_inverse_factorial h K.nE,
 757    gluingLaw_forces_inverse_factorial h K.nT, gibbsWeight_factorizes]
 758
 759/-- **THEOREM (gluing implies the gauge-counting principle).**  The premise behind the
 760Gap-2 measure follows from the gluing law.  This is the sharpest available statement of
 761what the theory still owes: not a normalization, but multiplicativity under
 762assembly. -/
 763theorem gluingLaw_gives_gaugeCounting (B : ℕ) {f : ℕ → ℝ} (h : GluingLaw f) :
 764    MeasureSubstrateBlocker.GaugeCountingPrinciple
 765      (classMass (B := B) (fun K => f K.nV * f K.nE * f K.nT)) := by
 766  have hfun : (fun K : BoundedComplex B => f K.nV * f K.nE * f K.nT)
 767      = (gibbsWeight : BoundedComplex B → ℝ) := by
 768    funext K
 769    exact gluingLaw_gives_gibbsWeight h K
 770  rw [hfun]
 771  exact gibbs_induces_measure B
 772
 773/-- The gluing law is satisfiable: the inverse factorial is a model, so the reduction
 774is not vacuous.  `Nat.add_choose_le`-style bookkeeping is the whole content. -/
 775theorem inverseFactorial_gluingLaw :
 776    GluingLaw (fun n => 1 / (Nat.factorial n : ℝ)) where
 777  unit := by norm_num
 778  atom := by norm_num
 779  shuffle := by
 780    intro m n
 781    have hkey : (Nat.choose (m + n) m) * (Nat.factorial m * Nat.factorial n)
 782        = Nat.factorial (m + n) := by
 783      have h := Nat.choose_mul_factorial_mul_factorial (Nat.le_add_right m n)
 784      simpa [Nat.add_sub_cancel_left, mul_assoc] using h
 785    have hm : (0 : ℝ) < (Nat.factorial m : ℝ) := by exact_mod_cast Nat.factorial_pos m
 786    have hn : (0 : ℝ) < (Nat.factorial n : ℝ) := by exact_mod_cast Nat.factorial_pos n
 787    have hmn : (0 : ℝ) < (Nat.factorial (m + n) : ℝ) := by
 788      exact_mod_cast Nat.factorial_pos (m + n)
 789    have hcast : ((Nat.choose (m + n) m : ℕ) : ℝ)
 790        * ((Nat.factorial m : ℝ) * (Nat.factorial n : ℝ))
 791        = (Nat.factorial (m + n) : ℝ) := by
 792      exact_mod_cast congrArg (fun k : ℕ => (k : ℝ)) hkey
 793    field_simp
 794    linarith [hcast]
 795
 796/-! ## §7. Certificate -/
 797
 798/-- What this module establishes about the Gap-2 premise. -/
 799structure GaugeVolumeStatus where
 800  /-- The gauge volume is proved equal to the order of the sector group. -/
 801  gauge_volume_is_group_order : Bool
 802  /-- The gauge volume is proved to carry no incidence information. -/
 803  gauge_volume_size_only : Bool
 804  /-- The measure is proved equal to the label density. -/
 805  measure_is_label_density : Bool
 806  /-- The premise is proved equivalent to unit cross-sector fugacity: one positive
 807  real per size sector, set to one.  This is the exact naming of the premise. -/
 808  premise_is_unit_sector_fugacity : Bool
 809  /-- Label indifference alone is proved NOT to select the premise: the whole
 810  sector-fugacity family is relabeling-invariant.  Retired reading, kept false so a
 811  later reader cannot revive it. -/
 812  premise_is_label_indifference : Bool
 813  /-- The residual sector factor is proved absorbable into the action, so the measure
 814  is determined only up to that booking convention. -/
 815  residue_absorbable_into_action : Bool
 816  /-- The premise is proved to follow from a gluing law: multiplicativity of the
 817  weight under assembly, with label interleavings counted.  A reduction of the debt,
 818  not a discharge, since the gluing law is itself not derived from the ledger. -/
 819  premise_reduces_to_gluing : Bool
 820  /-- The Gibbs weight is proved to be the unique relabeling-invariant labeled
 821  weight whose class mass is the RS measure. -/
 822  gibbs_weight_unique : Bool
 823  /-- Label indifference itself is NOT derived from the ledger cost function;
 824  `Gap2LedgerSiteBlindness` proves that route is blocked. -/
 825  indifference_derived_from_cost : Bool
 826
 827/-- Status after this module. -/
 828def gaugeVolumeStatus : GaugeVolumeStatus where
 829  gauge_volume_is_group_order := true
 830  gauge_volume_size_only := true
 831  measure_is_label_density := true
 832  premise_is_unit_sector_fugacity := true
 833  premise_is_label_indifference := false
 834  residue_absorbable_into_action := true
 835  premise_reduces_to_gluing := true
 836  gibbs_weight_unique := true
 837  indifference_derived_from_cost := false
 838
 839theorem status_group_order : gaugeVolumeStatus.gauge_volume_is_group_order = true := rfl
 840theorem status_size_only : gaugeVolumeStatus.gauge_volume_size_only = true := rfl
 841theorem status_label_density : gaugeVolumeStatus.measure_is_label_density = true := rfl
 842theorem status_premise_named : gaugeVolumeStatus.premise_is_unit_sector_fugacity = true := rfl
 843/-- Retired by adversarial review 2026-07-28; `fugacityWeight_invariant` is the proof. -/
 844theorem status_indifference_undershoots :
 845    gaugeVolumeStatus.premise_is_label_indifference = false := rfl
 846theorem status_absorbable : gaugeVolumeStatus.residue_absorbable_into_action = true := rfl
 847theorem status_gluing : gaugeVolumeStatus.premise_reduces_to_gluing = true := rfl
 848theorem status_gibbs_unique : gaugeVolumeStatus.gibbs_weight_unique = true := rfl
 849/-- OPEN by construction: cost cannot supply label indifference. -/
 850theorem status_cost_route_open : gaugeVolumeStatus.indifference_derived_from_cost = false := rfl
 851
 852/-- **Grounding theorem.**  The flags are backed by the actual theorems. -/
 853theorem gaugeVolume_grounded (B : ℕ) :
 854    (∀ K : BoundedComplex B,
 855        pairCount K = Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT)) ∧
 856    (∀ K K' : BoundedComplex B, K.nV = K'.nV → K.nE = K'.nE → K.nT = K'.nT →
 857        pairCount K = pairCount K') ∧
 858    (∀ K : BoundedComplex B, labelDensity K = mu K) ∧
 859    (∀ ν : TriangulationClass B → ℝ,
 860        MeasureSubstrateBlocker.GaugeCountingPrinciple ν ↔
 861          ∀ K : BoundedComplex B,
 862            ν (Quotient.mk (relabelSetoid B) K) = labelDensity K) ∧
 863    MeasureSubstrateBlocker.GaugeCountingPrinciple
 864      (classMass (gibbsWeight : BoundedComplex B → ℝ)) ∧
 865    (∀ w : BoundedComplex B → ℝ, (∀ K K', Equivalent K K' → w K = w K') →
 866        (MeasureSubstrateBlocker.GaugeCountingPrinciple (classMass w) ↔
 867          ∀ K : BoundedComplex B, w K = gibbsWeight K)) :=
 868  ⟨pairCount_eq_factorials,
 869   fun _ _ hV hE hT => pairCount_congr_sizes hV hE hT,
 870   labelDensity_eq_mu,
 871   gaugeCounting_iff_labelIndifference,
 872   gibbs_induces_measure B,
 873   invariant_weight_gives_measure_iff⟩
 874
 875end Gap2GaugeVolume
 876end SevenGaps
 877end Gravity
 878end IndisputableMonolith
 879