IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityPostingGluing

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting
   2
   3/-!
   4# Gap 2: can posting plus gluing force unit sector fugacity?  No, and the reason is exact
   5
   6`Gap2GluingDerivation.closedForm` reduces the path-sum measure's residual freedom to three positive
   7constants: a size-blind weight satisfying the four carrier gluing instances is the inverse gauge
   8volume times one fugacity per index type, and `characterSize u v w` realizes every triple
   9(`residue_is_exactly_three_positive_constants`).  `gibbs_of_unit_fugacities` then gets the measure
  10from `f 1 0 0 = f 1 1 0 = f 1 0 1 = 1`.  That last hypothesis is the premise the Gap-2 measure
  11rests on, recorded as unit sector fugacity.
  12
  13`Gap2NonEquivariantPosting` sharpened the posting-layer criterion: for every letter cost, posting
  14`mu` is exactly orbit mean one on the Boltzmann numerator
  15(`posts_mu_iff_numeratorMass_eq_orbitCard`), and a continuum of non-equivariant costs
  16(`tiltedCost t`) meets it.  The open question this module was opened to answer: does the
  17posting layer, together with the gluing law, force the three constants to one?
  18
  19## The answer, in three theorems
  20
  21**No, and the countermodel is the best-behaved cost in the formalism.**  `characterCost u v w`
  22charges every vertex letter `-log u`, every edge letter `-log v`, every tetrahedron letter
  23`-log w`.  It is kind-only and gauge-equivariant, so it satisfies the posting layer's named
  24structural conditions (`KindOnly`, and with it `ChargesCountsOnly`, `FixedKindTotals`, and
  25`CostSizeBlind`), and
  26
  27* `postedWeight_characterCost`: its posted weight is *exactly* `sizeWeight (characterSize u v w)`,
  28  so the kind-rate family and the gluing derivation's three-constant residue are the same family,
  29  under the substitution `u = exp(-cV)`, `v = exp(-cE)`, `w = exp(-cT)`;
  30* `characterSize_carrierShuffle` (imported) and `characterSize_gluesAt`: it satisfies the gluing
  31  law at all four carrier families and in fact at **every** eligible pair, for every positive
  32  triple;
  33* `unitFugacity_characterSize_iff`: its fugacity is unit exactly when `u = v = w = 1`.
  34
  35So `gluing_and_posting_do_not_force_unit_fugacity`: for every non-unit positive triple there is a
  36kind-only equivariant letter cost whose posted weight is size-blind, whose induced size function
  37satisfies the gluing law everywhere, and whose sector fugacity is not unit.  The gluing law
  38constrains the *shape* of the fugacity (it must be a character) and nothing about its value.
  39
  40**What does force it is a restatement of the conclusion.**  `unitFugacity_iff_mu_at_atoms`: for
  41any size function whatever, unit sector fugacity holds **if and only if** the class mass of its
  42size-blind weight equals `mu` at the three atoms.  And `unitFugacity_iff_normalizedAtTheAtoms`:
  43it holds if and only if the labeled weight is `1` there, which is `NormalizedAtTheAtoms`.  Three
  44names, one statement.  So the premise is not a normalization convention sitting beside the
  45conclusion; it is three instances of the conclusion, at the three smallest complexes.
  46
  47**Hence the charged no-go direction is three instances of its own conclusion, and the gluing
  48hypothesis in it is idle.**
  49`posts_mu_at_atoms_forces_unit_fugacity` derives unit fugacity from posting `mu` at three
  50complexes with **no** gluing hypothesis and no positivity.  A conditional whose conclusion follows
  51from one hypothesis alone, where that hypothesis names the target measure, derives nothing.
  52`gluing_hypothesis_is_idle` states both halves side by side so the shape cannot be misread.
  53
  54## The charged first step: does the tilted family's posted weight satisfy the gluing law?
  55
  56Yes at the class-mass level, with unit fugacity, and trivially so.  `CarrierShuffle` is a
  57predicate on size functions, and the tilted posted weight is not one
  58(`postedWeight_tiltedCost_not_sizeWeight`, from the imported non-invariance).  What it does have
  59is a class mass, and because the family posts `mu` that class mass coincides with the size-blind
  60Gibbs one at every complex and every cap
  61(`tiltedCost_classMass_eq_classMass_gibbsSize`), so the size function representing it is
  62`gibbsSize`, which glues and is unit
  63(`tiltedCost_classMass_glues_with_unit_fugacity`).  The tilted family is therefore **not** a
  64non-unit-fugacity countermodel, and `no_posting_countermodel_with_nonunit_fugacity` shows nothing
  65that posts `mu` can be one: posting `mu` and non-unit fugacity are contradictory by construction.
  66That closes the countermodel direction as charged, and relocates the real countermodel to the
  67mu-free question, which is where `characterCost` answers it.
  68
  69## What this does NOT show
  70
  71**It does not show unit fugacity is unreachable.**  It shows it is not reachable from the two
  72inputs named here, the posting layer's structural conditions and the gluing law, in any
  73combination that does not name `mu` or the atom values.  A genuinely new physical input that
  74fixes the weight of a single vertex, a single loop, and a single degenerate tetrahedron would
  75close the premise; this module says exactly what such an input has to do, which is more than
  76"three constants" said before.
  77
  78**It does not weaken anything already proved.**  `posting_cost_derives_mu` still derives the
  79measure from kind-only plus `NormalizedAtTheAtoms`; what this module adds is that its second
  80hypothesis is the premise rather than an extra convenience, so that derivation relocates the
  81premise onto the posting layer without discharging it.  The countermodel is consistent with it:
  82`characterCost u v w` fails `NormalizedAtTheAtoms` for every non-unit triple, which is exactly
  83`characterCost_posts_mu_iff`.
  84
  85**The countermodel family is not new; the identification is.**  A kind-only cost with nonzero
  86rates was already known not to give the Gibbs weight
  87(`Gap2PostingCostDerivation.linearCost_atoms_force_zero` runs on that fact).  What is new here is
  88that the kind-rate family *is* `characterSize`, the exact residue of the gluing derivation, so the
  89two modules' leftover freedoms are one freedom and no gluing family can shrink it.
  90
  91**It says nothing about what a substrate posts.**  Same MODEL attachments as the imported
  92posting modules: `LetterCost` read as a charging rule, `historyCost` as ledger additivity over
  93postings, and the Boltzmann form.  This module adds none.
  94
  95## Honest tagging
  96
  97Every declaration below is THEOREM, kernel-checked in this module, audited by `#print axioms` at
  98the foot at the base triple only.  **Strength.**  All statements are exact equalities and
  99equivalences of reals over unbounded families, not agreements to a tolerance.  The countermodel is
 100a three-parameter continuum, and the three equivalences (`unitFugacity_iff_mu_at_atoms`,
 101`unitFugacity_iff_normalizedAtTheAtoms`, `unitFugacity_characterSize_iff`) are iffs quantified
 102over all size functions, so none of them is a one-witness claim.
 103-/
 104
 105namespace IndisputableMonolith
 106namespace Gravity
 107namespace SevenGaps
 108namespace Gap2FugacityPostingGluing
 109
 110open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
 111open GaugeHistoryMeasure Gap2SizeBlindnessReach Gap2PostingCostDerivation
 112open Gap2NonEquivariantPosting
 113
 114noncomputable section
 115
 116variable {B : ℕ}
 117
 118/-! ## §1. Unit sector fugacity, named, and three ways of saying it
 119
 120The premise of `gibbs_of_unit_fugacities` as a predicate, so it can appear on both sides of an
 121equivalence.  Nothing here mentions the posting layer. -/
 122
 123/-- **Unit sector fugacity**: the size function is one at each of the three atoms.  This is
 124literally the hypothesis triple of `Gap2GluingDerivation.CarrierShuffle.gibbs_of_unit_fugacities`,
 125and it is the premise flag 8 of the full-theory ledger stands on. -/
 126def UnitFugacity (f : ℕ → ℕ → ℕ → ℝ) : Prop :=
 127  f 1 0 0 = 1 ∧ f 1 1 0 = 1 ∧ f 1 0 1 = 1
 128
 129/-- The Gibbs weight of a labeled complex is the Gibbs size function at its three sizes.  A cast
 130identity: both are the reciprocal of the same product of factorials. -/
 131theorem gibbsWeight_eq_gibbsSize (K : BoundedComplex B) :
 132    gibbsWeight K = gibbsSize K.nV K.nE K.nT := by
 133  unfold gibbsWeight gibbsSize
 134  push_cast
 135  ring
 136
 137/-- **THEOREM (the bridge).**  A size-blind weight has class mass `mu` at a complex exactly when
 138its size function agrees with `gibbsSize` at that complex's size triple.  The orbit count cancels;
 139this is `classMass_sizeWeight` against `mu_eq_orbitCard_mul_gibbsWeight`, and it is the only
 140computation the rest of §1 needs. -/
 141theorem classMass_sizeWeight_eq_mu_iff (f : ℕ → ℕ → ℕ → ℝ) (K : BoundedComplex B) :
 142    classMass (sizeWeight f) (Quotient.mk (relabelSetoid B) K) = mu K
 143      ↔ f K.nV K.nE K.nT = gibbsSize K.nV K.nE K.nT := by
 144  have horb : (0 : ℝ) < (gaugeOrbitCard K : ℝ) := by
 145    exact_mod_cast gaugeOrbitCard_pos K
 146  rw [classMass_sizeWeight, mu_eq_orbitCard_mul_gibbsWeight, gibbsWeight_eq_gibbsSize]
 147  constructor
 148  · intro h
 149    exact mul_left_cancel₀ horb.ne' h
 150  · intro h
 151    rw [h]
 152
 153/-- The Gibbs size function is one at every atom size triple, which is why the unit point is the
 154intended one. -/
 155theorem gibbsSize_eq_one_at_atom_sizes {b c : ℕ} (hbc : b + c ≤ 1) : gibbsSize 1 b c = 1 := by
 156  have hb : b = 0 ∨ b = 1 := by omega
 157  have hc : c = 0 ∨ c = 1 := by omega
 158  rcases hb with hb | hb <;> rcases hc with hc | hc
 159  · rw [hb, hc]; norm_num [gibbsSize, Nat.factorial]
 160  · rw [hb, hc]; norm_num [gibbsSize, Nat.factorial]
 161  · rw [hb, hc]; norm_num [gibbsSize, Nat.factorial]
 162  · omega
 163
 164theorem gibbsSize_unitFugacity : UnitFugacity gibbsSize :=
 165  ⟨gibbsSize_eq_one_at_atom_sizes (by norm_num),
 166    gibbsSize_eq_one_at_atom_sizes (by norm_num),
 167    gibbsSize_eq_one_at_atom_sizes (by norm_num)⟩
 168
 169/-- **THEOREM (the premise IS three instances of the conclusion).**  For every size function
 170whatever, positive or not, gluing or not, unit sector fugacity holds if and only if the class mass
 171of its size-blind weight equals `mu` at every complex with one vertex and at most one incidence,
 172i.e. at the three atoms.
 173
 174This is the load-bearing statement of the module and it is an equivalence, not an implication.
 175Read the two directions separately.  Left to right says the premise is enough to get `mu` at the
 176atoms, which nobody doubted.  Right to left says the premise is *no more than* `mu` at the atoms:
 177any principle that yields unit fugacity has already yielded three values of the measure it was
 178supposed to be deriving.  Any condition that forces unit fugacity thereby determines the measure
 179at the three atoms: that is a requirement on such a condition, not a proof that none exists, and
 180it is the precise form of the obstruction the rest of this module measures. -/
 181theorem unitFugacity_iff_mu_at_atoms (f : ℕ → ℕ → ℕ → ℝ) :
 182    UnitFugacity f
 183      ↔ ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 184          classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K) = mu K := by
 185  constructor
 186  · rintro ⟨h1, h2, h3⟩ B' K hv hi
 187    rw [classMass_sizeWeight_eq_mu_iff]
 188    have hgs : gibbsSize K.nV K.nE K.nT = 1 := by
 189      rw [hv]
 190      exact gibbsSize_eq_one_at_atom_sizes hi
 191    rw [hgs]
 192    have hb : K.nE = 0 ∨ K.nE = 1 := by omega
 193    have hc : K.nT = 0 ∨ K.nT = 1 := by omega
 194    rcases hb with hb | hb <;> rcases hc with hc | hc
 195    · rw [hv, hb, hc]; exact h1
 196    · rw [hv, hb, hc]; exact h3
 197    · rw [hv, hb, hc]; exact h2
 198    · omega
 199  · intro h
 200    refine ⟨?_, ?_, ?_⟩
 201    · have hK := h _ (bouquet 0 0) rfl (by norm_num)
 202      rw [classMass_sizeWeight_eq_mu_iff] at hK
 203      simpa [gibbsSize, Nat.factorial] using hK
 204    · have hK := h _ (bouquet 1 0) rfl (by norm_num)
 205      rw [classMass_sizeWeight_eq_mu_iff] at hK
 206      simpa [gibbsSize, Nat.factorial] using hK
 207    · have hK := h _ (bouquet 0 1) rfl (by norm_num)
 208      rw [classMass_sizeWeight_eq_mu_iff] at hK
 209      simpa [gibbsSize, Nat.factorial] using hK
 210
 211/-- **THEOREM (the premise is also exactly the labeled normalization).**  Unit sector fugacity on
 212the size function holds if and only if the labeled size-blind weight is `NormalizedAtTheAtoms`,
 213which is the premise `Gap2PostingCostDerivation` uses in place of gluing.  So the two derivations
 214in the library do not rest on two different premises: they rest on the same one, written once as a
 215condition on a size function and once as a condition on a labeled weight.  The bridge between the
 216two writings is `Gap2PostingCostDerivation.postedWeight_sizeBlind` together with the
 217`SizeBlind`-to-`sizeWeight` equivalence: a size-blind posted weight is a `sizeWeight`, so
 218`NormalizedAtTheAtoms` on it is exactly this theorem's right side. -/
 219theorem unitFugacity_iff_normalizedAtTheAtoms (f : ℕ → ℕ → ℕ → ℝ) :
 220    UnitFugacity f ↔ NormalizedAtTheAtoms (fun _ K => sizeWeight f K) := by
 221  constructor
 222  · rintro ⟨h1, h2, h3⟩ B' K hv hi
 223    show f K.nV K.nE K.nT = 1
 224    have hb : K.nE = 0 ∨ K.nE = 1 := by omega
 225    have hc : K.nT = 0 ∨ K.nT = 1 := by omega
 226    rcases hb with hb | hb <;> rcases hc with hc | hc
 227    · rw [hv, hb, hc]; exact h1
 228    · rw [hv, hb, hc]; exact h3
 229    · rw [hv, hb, hc]; exact h2
 230    · omega
 231  · intro h
 232    exact ⟨by simpa [sizeWeight] using h _ (bouquet 0 0) rfl (by norm_num),
 233      by simpa [sizeWeight] using h _ (bouquet 1 0) rfl (by norm_num),
 234      by simpa [sizeWeight] using h _ (bouquet 0 1) rfl (by norm_num)⟩
 235
 236/-! ## §2. The countermodel cost: one fugacity per index type, charged per letter
 237
 238A letter cost that charges each letter a fixed amount by kind.  Its posted weight is computed
 239exactly, and it turns out to be the gluing derivation's three-constant residue on the nose. -/
 240
 241/-- The **character cost**: every vertex letter costs `-log u`, every edge letter `-log v`, every
 242tetrahedron letter `-log w`.  Kind-only by construction, so the best-behaved shape a letter cost
 243can have; nothing here reads a label, an incidence, or a size. -/
 244def characterCost (u v w : ℝ) : LetterCost := fun _ _ a =>
 245  match a with
 246  | Sum.inl _ => -Real.log u
 247  | Sum.inr (Sum.inl _) => -Real.log v
 248  | Sum.inr (Sum.inr _) => -Real.log w
 249
 250theorem characterCost_kindRates (u v w : ℝ) :
 251    KindRates (characterCost u v w) (-Real.log u) (-Real.log v) (-Real.log w) := by
 252  intro B' K
 253  exact ⟨fun _ => rfl, fun _ => rfl, fun _ => rfl⟩
 254
 255theorem characterCost_kindOnly (u v w : ℝ) : KindOnly (characterCost u v w) :=
 256  ⟨-Real.log u, -Real.log v, -Real.log w, characterCost_kindRates u v w⟩
 257
 258/-- **THEOREM (the character cost is gauge-equivariant).**  A letter's charge depends only on
 259which of the three blocks it lies in, and the alphabet transport a relabeling induces is a
 260block-diagonal sum congruence, so it never moves a letter between blocks. -/
 261theorem characterCost_equivariant (u v w : ℝ) : Equivariant (characterCost u v w) := by
 262  intro B' K K' r a
 263  rcases a with x | (y | z) <;> rfl
 264
 265theorem historyCost_characterCost (u v w : ℝ) (B' : ℕ) (K : BoundedComplex B') :
 266    historyCost (characterCost u v w) B' K
 267      = -Real.log u * (K.nV : ℝ) + -Real.log v * (K.nE : ℝ) + -Real.log w * (K.nT : ℝ) :=
 268  historyCost_of_kindRates (characterCost_kindRates u v w) B' K
 269
 270/-- A positive real raised to a natural power, through the exponential.  Proved by induction
 271rather than cited so no Mathlib naming drift can break the module. -/
 272theorem exp_log_mul_nat {x : ℝ} (hx : 0 < x) (n : ℕ) :
 273    Real.exp (Real.log x * (n : ℝ)) = x ^ n := by
 274  induction n with
 275  | zero => simp
 276  | succ k ih =>
 277      have hstep : Real.log x * ((k + 1 : ℕ) : ℝ) = Real.log x * (k : ℝ) + Real.log x := by
 278        push_cast; ring
 279      rw [hstep, Real.exp_add, ih, Real.exp_log hx, pow_succ]
 280
 281/-- **THEOREM (the Boltzmann numerator of the character cost).**  Exactly one fugacity factor per
 282cell: `u^nV · v^nE · w^nT`.  This is where the name comes from, and it is a computation, not a
 283design choice: the charge is per letter and the alphabet has one letter per cell. -/
 284theorem exp_neg_historyCost_characterCost {u v w : ℝ} (hu : 0 < u) (hv : 0 < v) (hw : 0 < w)
 285    (B' : ℕ) (K : BoundedComplex B') :
 286    Real.exp (-(historyCost (characterCost u v w) B' K))
 287      = u ^ K.nV * v ^ K.nE * w ^ K.nT := by
 288  rw [historyCost_characterCost]
 289  have hneg : -(-Real.log u * (K.nV : ℝ) + -Real.log v * (K.nE : ℝ) + -Real.log w * (K.nT : ℝ))
 290      = Real.log u * (K.nV : ℝ) + (Real.log v * (K.nE : ℝ) + Real.log w * (K.nT : ℝ)) := by
 291    ring
 292  rw [hneg, Real.exp_add, Real.exp_add, exp_log_mul_nat hu, exp_log_mul_nat hv,
 293    exp_log_mul_nat hw]
 294  ring
 295
 296/-- **THEOREM (the identification, and the point of the module).**  The posted weight of the
 297character cost is *exactly* the size-blind weight of `characterSize u v w`, the three-constant
 298residue `Gap2GluingDerivation` was left with.  So the kind-rate family at the posting layer and
 299the residue of the gluing derivation are the same family, under `u = exp(-cV)`, `v = exp(-cE)`,
 300`w = exp(-cT)`.  Everything in §3 is read off this equality. -/
 301theorem postedWeight_characterCost {u v w : ℝ} (hu : 0 < u) (hv : 0 < v) (hw : 0 < w)
 302    (B' : ℕ) (K : BoundedComplex B') :
 303    postedWeight (characterCost u v w) B' K = sizeWeight (characterSize u v w) K := by
 304  unfold postedWeight sizeWeight characterSize gibbsWeight gaugeVol
 305  rw [exp_neg_historyCost_characterCost hu hv hw, mul_one_div]
 306
 307theorem postedWeight_characterCost_eq {u v w : ℝ} (hu : 0 < u) (hv : 0 < v) (hw : 0 < w)
 308    (B' : ℕ) :
 309    postedWeight (characterCost u v w) B'
 310      = fun K : BoundedComplex B' => sizeWeight (characterSize u v w) K := by
 311  funext K
 312  exact postedWeight_characterCost hu hv hw B' K
 313
 314theorem postedWeight_characterCost_sizeBlind (u v w : ℝ) :
 315    SizeBlind (postedWeight (characterCost u v w)) :=
 316  postedWeight_sizeBlind (characterCost_kindOnly u v w)
 317
 318/-! ### The fugacity of the character cost, computed -/
 319
 320theorem characterSize_atom_vertex (u v w : ℝ) : characterSize u v w 1 0 0 = u := by
 321  unfold characterSize gaugeVol
 322  norm_num [Nat.factorial]
 323
 324theorem characterSize_atom_edge (u v w : ℝ) : characterSize u v w 1 1 0 = u * v := by
 325  unfold characterSize gaugeVol
 326  norm_num [Nat.factorial]
 327
 328theorem characterSize_atom_tet (u v w : ℝ) : characterSize u v w 1 0 1 = u * w := by
 329  unfold characterSize gaugeVol
 330  norm_num [Nat.factorial]
 331
 332/-- **THEOREM (the fugacity is unit exactly at the unit triple).**  So the family is faithfully
 333parametrized by its fugacity and the countermodel below is not hiding at the intended point. -/
 334theorem unitFugacity_characterSize_iff {u v w : ℝ} :
 335    UnitFugacity (characterSize u v w) ↔ (u = 1 ∧ v = 1 ∧ w = 1) := by
 336  unfold UnitFugacity
 337  rw [characterSize_atom_vertex, characterSize_atom_edge, characterSize_atom_tet]
 338  constructor
 339  · rintro ⟨h1, h2, h3⟩
 340    rw [h1, one_mul] at h2 h3
 341    exact ⟨h1, h2, h3⟩
 342  · rintro ⟨h1, h2, h3⟩
 343    rw [h1, h2, h3]
 344    norm_num
 345
 346/-- The character cost satisfies the gluing premise at **every** eligible pair, not only at the
 347four carrier families, and for every positive triple.  `characterSize_shuffle` holds
 348unconditionally, and `gluesAt_of_shuffle` transports it wherever the automorphism counts
 349multiply. -/
 350theorem characterSize_gluesAt (u v w : ℝ) {B B' : ℕ} (K : BoundedComplex B)
 351    (L : BoundedComplex B')
 352    (haut : Nat.card (Aut (dunion K L)) = Nat.card (Aut K) * Nat.card (Aut L)) :
 353    GluesAt (characterSize u v w) K L :=
 354  gluesAt_of_shuffle _ K L haut (characterSize_shuffle u v w _ _ _ _ _ _)
 355
 356/-! ## §3. The countermodel: posting structure plus gluing leaves the fugacity free -/
 357
 358/-- **THEOREM (the countermodel, packaged).**  For every positive triple, the character cost is
 359kind-only, gauge-equivariant, has a size-blind posted weight equal to `characterSize u v w`, and
 360that size function satisfies the gluing law at all four carrier families and at every eligible
 361pair, with fugacity `(u, u·v, u·w)`.  Six conjuncts, all exact. -/
 362theorem characterCost_countermodel {u v w : ℝ} (hu : 0 < u) (hv : 0 < v) (hw : 0 < w) :
 363    KindOnly (characterCost u v w)
 364      ∧ Equivariant (characterCost u v w)
 365      ∧ SizeBlind (postedWeight (characterCost u v w))
 366      ∧ (∀ (B' : ℕ) (K : BoundedComplex B'),
 367          postedWeight (characterCost u v w) B' K = sizeWeight (characterSize u v w) K)
 368      ∧ CarrierShuffle (characterSize u v w)
 369      ∧ (characterSize u v w 1 0 0 = u ∧ characterSize u v w 1 1 0 = u * v
 370          ∧ characterSize u v w 1 0 1 = u * w) :=
 371  ⟨characterCost_kindOnly u v w, characterCost_equivariant u v w,
 372    postedWeight_characterCost_sizeBlind u v w,
 373    fun B' K => postedWeight_characterCost hu hv hw B' K,
 374    characterSize_carrierShuffle hu hv hw,
 375    ⟨characterSize_atom_vertex u v w, characterSize_atom_edge u v w,
 376      characterSize_atom_tet u v w⟩⟩
 377
 378/-- **THE HEADLINE.**  The posting layer's structural conditions plus the gluing law do **not**
 379force unit sector fugacity.  For every positive triple other than `(1,1,1)` there is a letter cost
 380which is kind-only and gauge-equivariant, whose posted weight is size-blind and equal to the
 381size-blind weight of a size function satisfying the gluing law, and whose sector fugacity is not
 382unit.
 383
 384This refutes the natural formalization of the no-go direction: "if the posted weight's class mass
 385as a function of sector sizes satisfies `CarrierShuffle`, the fugacity character is trivial".  It
 386is false, and the witness is a continuum of the best-behaved costs in the formalism.  The gluing
 387law does real work, but only on the *shape* of the fugacity: `closedForm` says it must be a
 388character rather than an arbitrary function of the three sizes.  Its value is untouched. -/
 389theorem gluing_and_posting_do_not_force_unit_fugacity {u v w : ℝ} (hu : 0 < u) (hv : 0 < v)
 390    (hw : 0 < w) (hne : ¬ (u = 1 ∧ v = 1 ∧ w = 1)) :
 391    ∃ (c : LetterCost) (f : ℕ → ℕ → ℕ → ℝ),
 392      KindOnly c ∧ Equivariant c ∧ SizeBlind (postedWeight c)
 393        ∧ (∀ (B' : ℕ) (K : BoundedComplex B'), postedWeight c B' K = sizeWeight f K)
 394        ∧ CarrierShuffle f
 395        ∧ ¬ UnitFugacity f := by
 396  refine ⟨characterCost u v w, characterSize u v w, characterCost_kindOnly u v w,
 397    characterCost_equivariant u v w, postedWeight_characterCost_sizeBlind u v w,
 398    fun B' K => postedWeight_characterCost hu hv hw B' K,
 399    characterSize_carrierShuffle hu hv hw, ?_⟩
 400  intro hUF
 401  exact hne (unitFugacity_characterSize_iff.mp hUF)
 402
 403/-- **THEOREM (what separates the countermodel from the intended point, exactly).**  The character
 404cost posts `mu` if and only if its triple is `(1,1,1)`.  So the condition that fails on the
 405countermodel is not any structural condition at the posting layer and not the gluing law; it is
 406posting the measure, which is the conclusion.  This is also the compatibility receipt against
 407`Gap2PostingCostDerivation.posting_cost_derives_mu`: that theorem's second hypothesis,
 408`NormalizedAtTheAtoms`, is what the countermodel violates, and by
 409`unitFugacity_iff_normalizedAtTheAtoms` that hypothesis is unit fugacity itself. -/
 410theorem characterCost_posts_mu_iff {u v w : ℝ} (hu : 0 < u) (hv : 0 < v) (hw : 0 < w) :
 411    (∀ (B' : ℕ) (K : BoundedComplex B'),
 412        classMass (postedWeight (characterCost u v w) B') (Quotient.mk (relabelSetoid B') K)
 413          = mu K)
 414      ↔ (u = 1 ∧ v = 1 ∧ w = 1) := by
 415  have hrw : ∀ (B' : ℕ) (K : BoundedComplex B'),
 416      classMass (postedWeight (characterCost u v w) B') (Quotient.mk (relabelSetoid B') K)
 417        = classMass (sizeWeight (characterSize u v w)) (Quotient.mk (relabelSetoid B') K) := by
 418    intro B' K
 419    rw [postedWeight_characterCost_eq hu hv hw B']
 420  constructor
 421  · intro h
 422    refine unitFugacity_characterSize_iff.mp ((unitFugacity_iff_mu_at_atoms _).mpr ?_)
 423    intro B' K hv' hi
 424    rw [← hrw B' K]
 425    exact h B' K
 426  · rintro ⟨h1, h2, h3⟩ B' K
 427    rw [hrw B' K, h1, h2, h3, ← gibbsSize_eq_characterSize_one]
 428    exact (classMass_sizeWeight_eq_mu_iff gibbsSize K).mpr rfl
 429
 430/-! ## §4. Why the charged no-go direction restates its conclusion: the gluing hypothesis is idle -/
 431
 432/-- **THEOREM (posting `mu` at three complexes forces unit fugacity, with no gluing).**  No
 433positivity, no `CarrierShuffle`, no posting-layer structure: three instances of "the class mass is
 434`mu`" give the premise directly.  This is the backward half of `unitFugacity_iff_mu_at_atoms`,
 435named separately because it is the theorem the charged no-go direction asks for, and because
 436seeing that it needs none of the other hypotheses is the point. -/
 437theorem posts_mu_at_atoms_forces_unit_fugacity (f : ℕ → ℕ → ℕ → ℝ)
 438    (h : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 439      classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K) = mu K) :
 440    UnitFugacity f :=
 441  (unitFugacity_iff_mu_at_atoms f).mpr h
 442
 443/-- **THEOREM (posting `mu` everywhere forces the whole Gibbs size function).**  Same restatement
 444at
 445full strength: if a size-blind weight's class mass is `mu` at every complex, its size function is
 446`gibbsSize` at every size triple any complex realizes.  `closedForm` is not used and no gluing
 447premise appears. -/
 448theorem posts_mu_forces_gibbsSize (f : ℕ → ℕ → ℕ → ℝ)
 449    (h : ∀ (B' : ℕ) (K : BoundedComplex B'),
 450      classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K) = mu K)
 451    (K : BoundedComplex B) : f K.nV K.nE K.nT = gibbsSize K.nV K.nE K.nT :=
 452  (classMass_sizeWeight_eq_mu_iff f K).mp (h B K)
 453
 454/-- **THEOREM (the gluing hypothesis in the no-go is idle, and the no-go is therefore a
 455restatement).**  Two conjuncts, side by side so the shape cannot be misread.
 456
 4571.  Posting `mu` at the three atoms forces unit fugacity **with no gluing hypothesis at all**.
 458    So the charged conditional "posts `mu` and glues, therefore unit fugacity" is true, and its
 459    gluing hypothesis does no work.
 4602.  The gluing law alone, together with every structural condition the posting layer can impose,
 461    is satisfied by size functions with fugacity as far from unit as one likes.  So the work in
 462    the conditional is being done entirely by the hypothesis that names `mu`.
 463
 464A conditional whose only load-bearing hypothesis is three values of its own conclusion does not
 465derive anything.  That is the honest verdict on this route, and it is why the second conjunct is
 466the result worth banking. -/
 467theorem gluing_hypothesis_is_idle :
 468    (∀ f : ℕ → ℕ → ℕ → ℝ,
 469        (∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 470            classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K) = mu K) →
 471          UnitFugacity f)
 472      ∧ (∀ u v w : ℝ, 0 < u → 0 < v → 0 < w → ¬ (u = 1 ∧ v = 1 ∧ w = 1) →
 473          ∃ (c : LetterCost) (f : ℕ → ℕ → ℕ → ℝ),
 474            KindOnly c ∧ Equivariant c ∧ SizeBlind (postedWeight c)
 475              ∧ (∀ (B' : ℕ) (K : BoundedComplex B'), postedWeight c B' K = sizeWeight f K)
 476              ∧ CarrierShuffle f
 477              ∧ ¬ UnitFugacity f) :=
 478  ⟨fun f h => posts_mu_at_atoms_forces_unit_fugacity f h,
 479    fun _ _ _ hu hv hw hne => gluing_and_posting_do_not_force_unit_fugacity hu hv hw hne⟩
 480
 481/-! ## §5. The charged first step: the tilted family, and why no mu-posting countermodel exists -/
 482
 483/-- **THEOREM (the tilted family's posted weight is not size-blind at all).**  There is no size
 484function whose size-blind weight it equals, because a size-blind weight is relabeling-invariant and
 485the tilted posted weight is not (`postedWeight_tiltedCost_not_invariant`).  So `CarrierShuffle`,
 486which is a predicate on size functions, does not apply to it directly; the only object of the
 487tilted family that the gluing law can see is its class mass. -/
 488theorem postedWeight_tiltedCost_not_sizeWeight {t : ℝ} (ht : |t| < 1) (ht0 : t ≠ 0) :
 489    ¬ ∃ f : ℕ → ℕ → ℕ → ℝ,
 490        ∀ K : BoundedComplex 3, postedWeight (tiltedCost t) 3 K = sizeWeight f K := by
 491  rintro ⟨f, hf⟩
 492  refine postedWeight_tiltedCost_not_invariant ht ht0 ?_
 493  intro K K' hEq
 494  rw [hf K, hf K', sizeWeight_invariant f hEq]
 495
 496/-- **THEOREM (the tilted family's class mass IS the Gibbs one).**  At every cap and every
 497complex, because the family posts `mu` and `mu` is the class mass of the size-blind Gibbs weight.
 498The size function representing the tilted class mass is therefore `gibbsSize`. -/
 499theorem tiltedCost_classMass_eq_classMass_gibbsSize {t : ℝ} (ht : |t| < 1) (B' : ℕ)
 500    (K : BoundedComplex B') :
 501    classMass (postedWeight (tiltedCost t) B') (Quotient.mk (relabelSetoid B') K)
 502      = classMass (sizeWeight gibbsSize) (Quotient.mk (relabelSetoid B') K) := by
 503  rw [tiltedCost_posts_mu ht B' K]
 504  exact ((classMass_sizeWeight_eq_mu_iff gibbsSize K).mpr rfl).symm
 505
 506/-- **THEOREM (the charged first step, answered).**  The tilted family's class mass satisfies the
 507gluing law, with unit fugacity, at every cap and every complex.  The answer is yes and it is
 508forced, not accidental: posting `mu` is exactly agreeing with the Gibbs class mass, and the Gibbs
 509size function glues and is unit.
 510
 511So the tilted family is **not** a countermodel to the premise: it exhibits the premise.  The
 512underdetermination it established lives entirely at the labeled level, below the class mass, where
 513`CarrierShuffle` cannot see it. -/
 514theorem tiltedCost_classMass_glues_with_unit_fugacity {t : ℝ} (ht : |t| < 1) :
 515    (∀ (B' : ℕ) (K : BoundedComplex B'),
 516        classMass (postedWeight (tiltedCost t) B') (Quotient.mk (relabelSetoid B') K)
 517          = classMass (sizeWeight gibbsSize) (Quotient.mk (relabelSetoid B') K))
 518      ∧ CarrierShuffle gibbsSize
 519      ∧ UnitFugacity gibbsSize :=
 520  ⟨fun B' K => tiltedCost_classMass_eq_classMass_gibbsSize ht B' K,
 521    gibbsSize_carrierShuffle, gibbsSize_unitFugacity⟩
 522
 523/-- **THEOREM (no mu-posting countermodel can exist).**  If a letter cost posts `mu` at the
 524three atoms, and its class mass there is represented by a size function, that size function has
 525unit fugacity.  Equivariant or not, kind-only or not, gluing or not.  The cost variable is a
 526spectator: the two hypotheses together are exactly `classMass (sizeWeight f) = mu` at the atoms,
 527so the content is the backward half of `unitFugacity_iff_mu_at_atoms` transported across the
 528representation.
 529
 530This closes the countermodel direction as it was charged: "a cost that posts `mu` whose posted
 531weight is gluing-multiplicative with non-unit fugacity" is not merely unfound, it is
 532contradictory.  Which is why the real countermodel had to be sought after dropping the reference
 533to `mu`, and §3 is where it lives. -/
 534theorem no_posting_countermodel_with_nonunit_fugacity (c : LetterCost) (f : ℕ → ℕ → ℕ → ℝ)
 535    (hpost : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 536      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K)
 537    (hrep : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 538      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K)
 539        = classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K)) :
 540    UnitFugacity f := by
 541  refine (unitFugacity_iff_mu_at_atoms f).mpr ?_
 542  intro B' K hv hi
 543  rw [← hrep B' K hv hi]
 544  exact hpost B' K hv hi
 545
 546/-! ## §6. The verdict, and the navigation index -/
 547
 548/-- **THE VERDICT.**  Five parts, and together they settle flag 8's premise question in the
 549negative for this route while saying exactly what remains.
 550
 5511.  Unit sector fugacity is equivalent to `mu` at the three atoms
 552    (`unitFugacity_iff_mu_at_atoms`), and equivalent to `NormalizedAtTheAtoms` on the labeled
 553    weight (`unitFugacity_iff_normalizedAtTheAtoms`).  The premise, the normalization, and three
 554    instances of the conclusion are one statement.
 5552.  Therefore posting `mu` forces the premise with no gluing hypothesis, so the charged no-go is a
 556    restatement rather than a derivation.
 5573.  The gluing law plus the posting layer's named structural conditions leaves the
 558    fugacity entirely free: a kind-only, gauge-equivariant letter cost realizes every positive
 559    triple, with a size-blind posted weight satisfying the gluing law at every eligible pair.
 5604.  No cost that posts `mu` can be a non-unit-fugacity countermodel; the contradiction is
 561    definitional.
 5625.  The tilted family of `Gap2NonEquivariantPosting` exhibits the premise rather than
 563    threatening it: its class mass is the Gibbs one and its underdetermination is invisible below
 564    the class mass. -/
 565theorem fugacity_posting_gluing_verdict :
 566    (∀ f : ℕ → ℕ → ℕ → ℝ, UnitFugacity f
 567        ↔ ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 568            classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K) = mu K)
 569      ∧ (∀ f : ℕ → ℕ → ℕ → ℝ,
 570          UnitFugacity f ↔ NormalizedAtTheAtoms (fun _ K => sizeWeight f K))
 571      ∧ (∀ u v w : ℝ, 0 < u → 0 < v → 0 < w → ¬ (u = 1 ∧ v = 1 ∧ w = 1) →
 572          ∃ (c : LetterCost) (f : ℕ → ℕ → ℕ → ℝ),
 573            KindOnly c ∧ Equivariant c ∧ SizeBlind (postedWeight c)
 574              ∧ (∀ (B' : ℕ) (K : BoundedComplex B'), postedWeight c B' K = sizeWeight f K)
 575              ∧ CarrierShuffle f ∧ ¬ UnitFugacity f)
 576      ∧ (∀ (c : LetterCost) (f : ℕ → ℕ → ℕ → ℝ),
 577          (∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 578              classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K) →
 579            (∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 580                classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K)
 581                  = classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K)) →
 582              UnitFugacity f)
 583      ∧ (CarrierShuffle gibbsSize ∧ UnitFugacity gibbsSize) :=
 584  ⟨unitFugacity_iff_mu_at_atoms, unitFugacity_iff_normalizedAtTheAtoms,
 585    fun _ _ _ hu hv hw hne => gluing_and_posting_do_not_force_unit_fugacity hu hv hw hne,
 586    fun c f hpost hrep => no_posting_countermodel_with_nonunit_fugacity c f hpost hrep,
 587    ⟨gibbsSize_carrierShuffle, gibbsSize_unitFugacity⟩⟩
 588
 589/-- Navigation record.  Fields are assigned by hand; the evidence is the named theorem in each
 590docstring, not the `rfl` projection. -/
 591structure Index : Type where
 592  /-- Unit sector fugacity is exactly `mu` at the three atoms. -/
 593  premise_is_mu_at_the_atoms : Bool
 594  /-- It is also exactly `NormalizedAtTheAtoms`, so the library's two derivations share one
 595  premise. -/
 596  premise_is_the_atom_normalization : Bool
 597  /-- The kind-rate posting family IS the gluing derivation's three-constant residue. -/
 598  kindRates_is_the_residue : Bool
 599  /-- SETTLED (this module): posting structure plus the gluing law does NOT force unit
 600  fugacity, witnessed by a continuum of kind-only equivariant costs. -/
 601  posting_plus_gluing_leaves_fugacity_free : Bool
 602  /-- SETTLED: no cost that posts `mu` can be a non-unit-fugacity countermodel. -/
 603  no_mu_posting_countermodel : Bool
 604  /-- SETTLED: the tilted family exhibits the premise rather than threatening it. -/
 605  tilted_family_glues_with_unit_fugacity : Bool
 606  /-- NOT proved, and refuted for this route: that unit sector fugacity is derivable from
 607  posting-layer structure together with the gluing law. -/
 608  unit_fugacity_derived : Bool
 609  /-- NOT proved: that unit sector fugacity is underivable in general.  What is shown is that it
 610  is not reachable from these two inputs without naming the measure. -/
 611  unit_fugacity_shown_underivable : Bool
 612
 613def index : Index where
 614  premise_is_mu_at_the_atoms := true
 615  premise_is_the_atom_normalization := true
 616  kindRates_is_the_residue := true
 617  posting_plus_gluing_leaves_fugacity_free := true
 618  no_mu_posting_countermodel := true
 619  tilted_family_glues_with_unit_fugacity := true
 620  unit_fugacity_derived := false
 621  unit_fugacity_shown_underivable := false
 622
 623theorem index_premise_is_mu_at_atoms : index.premise_is_mu_at_the_atoms = true := rfl
 624theorem index_fugacity_free : index.posting_plus_gluing_leaves_fugacity_free = true := rfl
 625theorem index_no_countermodel : index.no_mu_posting_countermodel = true := rfl
 626theorem index_premise_not_derived : index.unit_fugacity_derived = false := rfl
 627theorem index_not_shown_underivable : index.unit_fugacity_shown_underivable = false := rfl
 628
 629end
 630
 631#print axioms gibbsWeight_eq_gibbsSize
 632#print axioms classMass_sizeWeight_eq_mu_iff
 633#print axioms unitFugacity_iff_mu_at_atoms
 634#print axioms unitFugacity_iff_normalizedAtTheAtoms
 635#print axioms characterCost_kindOnly
 636#print axioms characterCost_equivariant
 637#print axioms exp_neg_historyCost_characterCost
 638#print axioms postedWeight_characterCost
 639#print axioms unitFugacity_characterSize_iff
 640#print axioms characterSize_gluesAt
 641#print axioms characterCost_countermodel
 642#print axioms gluing_and_posting_do_not_force_unit_fugacity
 643#print axioms characterCost_posts_mu_iff
 644#print axioms posts_mu_at_atoms_forces_unit_fugacity
 645#print axioms posts_mu_forces_gibbsSize
 646#print axioms gluing_hypothesis_is_idle
 647#print axioms postedWeight_tiltedCost_not_sizeWeight
 648#print axioms tiltedCost_classMass_eq_classMass_gibbsSize
 649#print axioms tiltedCost_classMass_glues_with_unit_fugacity
 650#print axioms no_posting_countermodel_with_nonunit_fugacity
 651#print axioms fugacity_posting_gluing_verdict
 652
 653end Gap2FugacityPostingGluing
 654end SevenGaps
 655end Gravity
 656end IndisputableMonolith
 657