IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCostDerivation

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2SizeBlindnessReach
   2
   3/-!
   4# Gap 2: premise (i) derived from a posting cost, and the premise that derivation needs
   5
   6`Gap2GluingDerivation` assumes premise (i), size-blindness of the labeled weight, and
   7`Gap2SizeBlindnessReach` shows that no premise of the form *the weight cannot distinguish
   8complexes that agree on `X`* supplies it while being weaker than it: blindness to `X` forces
   9size-blindness for every weight exactly when `X` resolves no more than the three counts.  What
  10that rules out is a *weaker* sufficient premise of this shape; it does not say the two conditions
  11are interchangeable, and they are not, since the coarse class also contains conditions strictly
  12stronger than premise (i) (`unsorted_is_strictly_stronger`).  That dichotomy quantifies over
  13**indistinguishability** premises, and this module goes at premise (i) with a premise of a
  14different kind, one that assigns the weight instead of failing to separate it.
  15
  16## The layer this module works at
  17
  18`GaugeHistoryMeasure` presents a complex as a posted history, and the reading of that
  19presentation is MODEL: `PostingAlphabet K = Fin K.nV ⊕ Fin K.nE ⊕ Fin K.nT` is a three-block
  20index type with canonical injections, and nothing in the library defines an emission process or
  21proves that substrate dynamics produces those letters.  "The substrate posts one letter per cell"
  22is how the type is *read*, not something derived, and additivity of a cost over those postings is
  23the unproved physical attachment the whole module rests on.  Two things then have posting-layer
  24readings.
  25
  26The **divisor** does: `gibbsWeight K = 1 / (nV! nE! nT!)` is the reciprocal of the order of
  27the alphabet's sort-respecting gauge group, the three symmetric groups on the three letter
  28blocks (`gibbsWeight_eq_inv_card_alphabetGauge`).  That group is not a new object: it is
  29`Gap2GaugeVolume.SectorGroup` (`alphabetGauge_eq_sectorGroup`), which that module already proved
  30is in bijection with the relabeling witnesses out of `K` (`sectorEquiv`).  So the identification is
  31real rather than a rename, and its content is borrowed rather than added: what §1 contributes is
  32that the same group is what the alphabet's three blocks admit.
  33
  34The **numerator** does too, once a cost is added.  A `LetterCost` assigns a real number to
  35each letter.  The `historyCost` of a complex is the sum of its letters' costs, which is
  36ledger additivity over postings and nothing more.  The `postedWeight` is the Boltzmann factor
  37of that cost over the gauge volume, and **the exponential is a third modeling choice, not a
  38consequence of the first two**: nothing here derives that a charge enters the weight as
  39`exp(-cost)` rather than through some other strictly decreasing map, and the derivation below uses
  40`exp` throughout.  It is named here because §7's inventory of what stands undischarged missed it
  41twice.
  42
  43## §3, the derivation: kind-only letter costs give premise (i), and then the measure
  44
  45A letter cost is **kind-only** when a letter's cost depends on which of the three blocks it
  46came from and on nothing else.  Then:
  47
  48* the history cost is `cV·nV + cE·nE + cT·nT` (`historyCost_of_kindRates`), so the posted
  49  weight is size-blind (`postedWeight_sizeBlind`) and premise (i) holds in exactly the form
  50  the derivation states it (`posting_cost_derives_premise_one`);
  51* the three unit normalizations then force `cV = cE = cT = 0`
  52  (`kindRates_atoms_force_zero`), because the gauge volume is `1` at each atom, so the
  53  Boltzmann factor must be too;
  54* hence the weight is the Gibbs weight (`posting_cost_derives_gibbs`) and the class measure
  55  is `mu` exactly (`posting_cost_derives_mu`).
  56
  57**No gluing premise appears in that chain.**  Premise (ii) is not used, not assumed, and not
  58needed.  Be precise about what replaces it, because the loose version of this sentence is wrong.
  59The deflation theorem needs only premise (i), and what it gives is the *shape* `q(sizes)/|Aut K|`,
  60not `mu`: for a general size-blind weight the class mass is the sector fugacity over the
  61automorphism count, and `mu` requires the fugacity to be one.  So premise (i) supplies the
  62`1/|Aut K|` dependence and the normalizations supply the numerator, which is the job premise (ii)
  63used to do by recursion.  The premise set is satisfied at the intended point
  64(`posting_premises_satisfiable`), so none of this is vacuous.
  65
  66That premise (ii) is gone does not mean it was idle, and the module says what it was for
  67rather than leaving the reader to wonder.  Its job in `Gap2GluingDerivation` is to propagate
  68the three unit normalizations from the atoms out to every size triple, which premise (i) alone
  69cannot do, since three values do not determine a function of the counts.  What replaces it here
  70is **linearity in the counts**, and that is a premise rather than a consequence of the carrier.
  71Summing a per-letter charge over an alphabet with one letter per cell does *not* make the total
  72linear in the counts: `pairCost` charges each vertex letter the vertex count, so its history cost
  73is `nV(nV-1)` (`historyCost_pairCost`).  Linearity arrives only with `KindRates` or
  74`FixedKindTotals`, and once it is assumed, a linear function vanishing at three independent points
  75vanishes everywhere.  That the job is real is measured, not asserted:
  76`costSizeBlind_and_atoms_do_not_give_gibbs` exhibits a cost satisfying premise (i) and all three
  77normalizations whose weight is not the Gibbs weight, so drop linearity and keep everything else and
  78the derivation stops.
  79
  80Three things must be said in the same breath, or the claim is inflated.
  81
  82First, the gauge divisor is a **premise, not a definition**.  Writing it into `postedWeight`
  83would hide it, so `PostedBy` states it as one equation, which packs three things and not two: that
  84the charge of a complex is the sum of its letters' charges, that the charge enters through `exp`,
  85and that the unit of recognition is shared evenly over the alphabet's gauge orbits.
  86`measure_from_posting_premises` is the derivation with that premise, `KindOnly`, and the atom
  87normalizations all three in the binders, and it is the statement to read.  §7 then measures how
  88much `PostedBy` restricts and the answer is almost nothing: every strictly positive weight is posted
  89by some cost at every complex with a cell (`postedBy_constrains_only_the_empty_complex`).  **That
  90measurement is unconditional and therefore does not say `PostedBy` is free given the kind clause**,
  91since the cost it constructs is generally not kind-only.  What it does say is that no
  92restrictiveness can be attributed to the divisor by itself.
  93
  94Second, the premise set is a **single point at the weight**, under §3's premise and under §7's
  95corrected one alike, and the reason is older than either.  Kind-only plus the three normalizations
  96forces the cost to be identically zero (`kindOnly_and_atoms_force_zeroCost`); aggregate linearity
  97plus the same three forces the history cost to be identically zero
  98(`fixedKindTotals_and_atoms_force_zero_historyCost`).  But the general fact is that *any*
  99equivariant cost posts `mu` exactly when its Boltzmann numerator is identically one
 100(`equivariant_posts_mu_iff_numerator_one`), which follows from a uniqueness theorem
 101`Gap2GaugeVolume` proved before this module existed.  So the chain above is rigidity rather than
 102computation, the premises select which cost rather than producing the answer, and the cost layer
 103contributes no factor to the measure.  `mu` itself is the orbit count over the gauge volume, so the
 104divisor is one of its two sources and the cost is neither.
 105
 106Third, these premises are **jointly stronger** than premise (i), not weaker.  What premise (i)
 107amounts to at this layer is exactly that the *total* charge is a function of the three counts
 108(`postedWeight_sizeBlind_iff`), and kind-only is strictly stronger than that
 109(`costSizeBlind_not_kindOnly`: a cost charging each vertex letter the vertex count is
 110size-blind and not kind-only).  So the trade is explicit.  Premise (ii) is gone, and premise
 111(i) is replaced by a statement about single postings, which is a different kind of assumption in a
 112place where the kind of assumption is the whole question.  Not a *locality* statement, and the word
 113is avoided from here on: `KindRates` demands the same three reals at every complex and every cap, so
 114it is a global condition on the charging rule, not constancy within one complex.
 115
 116## §4-§5, the hard stop: the named premise is incidence-silence
 117
 118Kind-only is the only clause of the derivation that constrains the weight away from the empty
 119complex and the three atoms, so the question is what forces it.  Gauge equivariance does not.
 120`incidenceCost t` charges `t` for an edge letter whose two endpoints
 121differ and nothing for any other letter.  It is a well-formed letter cost, it is equivariant
 122under every relabeling (`incidenceCost_equivariant`), because a relabeling carries an edge
 123with distinct endpoints to an edge with distinct endpoints, and it is not kind-only
 124(`incidenceCost_not_kindOnly`).  Its posted weight is exactly the proper-edge escape of
 125`Gap2SizeBlindnessReach` at `lam = exp(-t)` (`postedWeight_incidenceCost`), so it satisfies
 126every hypothesis of the derivation except premise (i)
 127(`incidencePosting_satisfiesTheOtherHypotheses`), is not size-blind, and its class mass at the
 128two-bridge class is `exp(-2t)/|Aut|` against `1/|Aut|`.
 129
 130So the escape is not an artifact of working with abstract weights.  A charging rule of the shape
 131this module formalizes, one letter per cell with a cost per posting, produces it.  Whether a
 132substrate charges this way is not a question any theorem here answers; what is closed is that
 133nothing in the posting layer as formalized rules the rule out.  §5's headline is
 134`incidence_silence_suffices_and_equivariance_does_not`, and its name is deliberately not "needs":
 135kind-only is strictly stronger than premise (i), so what needs it is this route to the measure,
 136and the necessity §5 proves is only that the natural weakening of it fails.
 137
 138**The name of the premise is corrected in §7, and the correction matters.**  Letter-level
 139incidence silence is *not* the boundary.  A cost may read incidence at every letter of a kind and
 140still produce `mu` exactly, provided what it reads cancels when that block is summed
 141(`centeredIncidence_is_the_measure`).  What suffices is **aggregate linearity by kind**: the total
 142charge of each kind is a fixed multiple of that kind's count.  `FixedKindTotals` states it, it is
 143strictly weaker than kind-only, and together with the three normalizations it derives the measure
 144(`measure_from_fixedKindTotals`).  Not on its own: the normalizations are load-bearing there, since
 145they are exactly what kills the three rates, and aggregate linearity by itself gives only premise
 146(i) at the cost layer (`fixedKindTotals_costSizeBlind`).  "Incidence silence" is the right slogan
 147for the block sum and the wrong one for the letter.
 148
 149## §6, what the stronger premise costs, measured
 150
 151Kind-only is strictly stronger than premise (i) as a condition on weights, and saying so is
 152not a hedge; it is the price.  The uniform labeled weight `sizeWeight 1` is size-blind and is
 153not the posted weight of any kind-only cost (`sizeBlind_not_always_posted`), because
 154`f · gaugeVol` would have to be exponential in the counts and a factorial is not.  What that
 155excludes is a wrong answer: `sizeWeight 1` is the decoy whose class mass is `gaugeVol/|Aut|`,
 156and the intended answer is a kind-only posted weight (`postedWeight_zeroCost`).  So the
 157strengthening removes the decoy and keeps the answer, which is what a strengthening should do.
 158
 159## Scope, and what this leaves open
 160
 161This does not prove aggregate linearity, and it does not prove kind-only.  It shows that either
 162one, conjoined with the three normalizations, derives premise (i) and then the measure, that
 163equivariance delivers neither, and that the gap sits at whether the *block sum* of a kind's charges
 164is a fixed multiple of that kind's count.  Whether the substrate forces that, from the definition of
 165`PostingAlphabet` or from anything else in the ledger layer, is open, and it is the residual worth
 166attacking.
 167
 168**It is not the only thing left, and counting the rest correctly took two referees.**  Five
 169assumptions stand behind `measure_from_posting_premises`.  `PostedBy` packs three: that the charge
 170of a complex is the sum of its letters' charges, built into `historyCost` before any premise is
 171stated and which nobody here has attacked; that the charge enters the weight through `exp`, which
 172is a modeling choice no theorem here motivates; and that one unit of recognition is shared evenly
 173over the alphabet's gauge orbits, which restricts nothing but the empty complex.  Then the kind
 174clause, and then `NormalizedAtTheAtoms`, which is fully restrictive rather than cosmetic: it is what
 175kills the three rates, and without it a nonzero triple of rates gives a posted weight that is not
 176the Gibbs weight at all.
 177
 178So the honest ranking is: posting additivity and the Boltzmann form are untouched, gauge sharing is
 179nearly free on its own, and the kind clause and the normalizations are both restrictive.  An earlier
 180version of this section said the kind clause was *the only* restrictive premise, which was wrong on
 181the normalizations and is withdrawn.
 182
 183This also revises the conjecture `Gap2SizeBlindnessReach` left, which guessed that the missing
 184premise would have to come from "structure that is not a function of the complex".  Half of
 185that is wrong: `KindOnly` is a condition on a letter cost, which is a function of the complex.
 186The half that survives is the other one, that it has to be a cost that assigns the weight
 187rather than a symmetry that fails to separate it.
 188-/
 189
 190namespace IndisputableMonolith
 191namespace Gravity
 192namespace SevenGaps
 193namespace Gap2PostingCostDerivation
 194
 195open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
 196open GaugeHistoryMeasure Gap2SizeBlindnessReach
 197
 198noncomputable section
 199
 200variable {B B' : ℕ}
 201
 202/-! ## §1. The alphabet's gauge group, and the Gibbs weight as its inverse order
 203
 204The divisor in `gibbsWeight` remains the imported formula `1/(nV! nE! nT!)`; what this section adds
 205is an identification of it, not a replacement.  The number it is the reciprocal of is the number of
 206ways to hand out the letters of the posting alphabet within their three blocks, which is the order
 207of the sort-respecting gauge group of the alphabet.  `Gap2SizeBlindnessReach.RespectsKinds` is the
 208condition that *names* block-respecting transports among alphabet equivalences; that the
 209block-respecting equivalences are in bijection with `AlphabetGauge` is the natural next lemma and is
 210not proved here, so read `RespectsKinds` as a definition and `card_alphabetGauge` as the count. -/
 211
 212/-- The **sort-respecting gauge group of the posting alphabet**: independent relabelings of
 213the vertex block, the edge block, and the tetrahedron block.
 214
 215**This is `Gap2GaugeVolume.SectorGroup` and not a new object.**  Stating it here under a
 216posting-layer name would be a rename dressed as a discovery, so `alphabetGauge_eq_sectorGroup`
 217records the identity, and the content behind it belongs to `Gap2GaugeVolume`: `sectorEquiv` proves
 218this group is in bijection with the (target, witness) pairs out of `K`, which is what makes it the
 219gauge group of the labeling rather than a product of permutation groups with a convenient order.
 220Everything §1 adds is the observation that the same group is what the posting alphabet's three
 221blocks admit. -/
 222abbrev AlphabetGauge (K : BoundedComplex B) : Type :=
 223  Equiv.Perm (Fin K.nV) × Equiv.Perm (Fin K.nE) × Equiv.Perm (Fin K.nT)
 224
 225/-- The posting alphabet's gauge group is the carrier's sector group, definitionally.  Recorded so
 226no reader takes §1 for an independent derivation of the divisor. -/
 227theorem alphabetGauge_eq_sectorGroup (K : BoundedComplex B) :
 228    AlphabetGauge K = Gap2GaugeVolume.SectorGroup K := rfl
 229
 230theorem card_alphabetGauge (K : BoundedComplex B) :
 231    Nat.card (AlphabetGauge K)
 232      = Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) :=
 233  Gap2GaugeVolume.card_sectorGroup K
 234
 235/-- **The Gibbs weight is one unit of recognition per gauge orbit of the alphabet.**  Its
 236divisor is the order of `AlphabetGauge`, so the weight is stated entirely in posting-layer
 237terms. -/
 238theorem gibbsWeight_eq_inv_card_alphabetGauge (K : BoundedComplex B) :
 239    gibbsWeight K = 1 / (Nat.card (AlphabetGauge K) : ℝ) := by
 240  unfold gibbsWeight
 241  rw [card_alphabetGauge]
 242
 243/-! ## §2. Letter costs, the history cost, and the posted weight -/
 244
 245/-- A **letter cost**: one real number per posting-alphabet letter, for each complex at each
 246size cap.  Nothing more, and in particular nothing about a substrate: this is a function on an index
 247type, and the ledger reading of it, that each posting costs something, is how it is meant rather
 248than anything a declaration here establishes. -/
 249def LetterCost : Type :=
 250  ∀ (B : ℕ) (K : BoundedComplex B), PostingAlphabet K → ℝ
 251
 252/-- The **history cost**: the sum of the costs of a complex's letters.  Additivity of the
 253ledger over postings is the entire content of this definition, and it is the one thing this
 254module assumes about a cost before any premise is stated. -/
 255def historyCost (c : LetterCost) (B : ℕ) (K : BoundedComplex B) : ℝ :=
 256  ∑ a : PostingAlphabet K, c B K a
 257
 258/-- The **posted weight** of a letter cost: the Boltzmann factor of the history cost, divided
 259by the gauge volume of the alphabet (`gibbsWeight_eq_inv_card_alphabetGauge`). -/
 260def postedWeight (c : LetterCost) (B : ℕ) (K : BoundedComplex B) : ℝ :=
 261  Real.exp (-(historyCost c B K)) * gibbsWeight K
 262
 263theorem postedWeight_pos (c : LetterCost) (B : ℕ) (K : BoundedComplex B) :
 264    0 < postedWeight c B K :=
 265  mul_pos (Real.exp_pos _) (gibbsWeight_positive K)
 266
 267/-- **Gauge equivariance of a letter cost.**  The cost of a letter is unchanged by transport
 268along the alphabet equivalence a relabeling induces.  This is the posting-layer form of
 269"labels are gauge", and §4 measures that it is strictly weaker than kind-only. -/
 270def Equivariant (c : LetterCost) : Prop :=
 271  ∀ (B : ℕ) (K K' : BoundedComplex B) (r : Relabel K K') (a : PostingAlphabet K),
 272    c B K' (postingAlphEquiv r.vEquiv r.eEquiv r.tEquiv a) = c B K a
 273
 274/-- An equivariant cost has a relabeling-invariant history cost: the alphabet equivalence
 275re-indexes the sum. -/
 276theorem historyCost_invariant {c : LetterCost} (hc : Equivariant c) {K K' : BoundedComplex B}
 277    (r : Relabel K K') : historyCost c B K = historyCost c B K' := by
 278  unfold historyCost
 279  exact Fintype.sum_equiv (postingAlphEquiv r.vEquiv r.eEquiv r.tEquiv) _ _
 280    (fun a => (hc B K K' r a).symm)
 281
 282theorem postedWeight_invariant {c : LetterCost} (hc : Equivariant c) {K K' : BoundedComplex B}
 283    (h : Equivalent K K') : postedWeight c B K = postedWeight c B K' := by
 284  obtain ⟨r⟩ := h
 285  unfold postedWeight
 286  rw [historyCost_invariant hc r, gibbsWeight_invariant ⟨r⟩]
 287
 288/-! ## §3. Kind-only letter costs derive premise (i), and then the measure -/
 289
 290/-- `c` charges the three **rates** `cV`, `cE`, `cT`: a vertex letter costs `cV` in every
 291complex at every cap, an edge letter `cE`, a tetrahedron letter `cT`. -/
 292def KindRates (c : LetterCost) (cV cE cT : ℝ) : Prop :=
 293  ∀ (B : ℕ) (K : BoundedComplex B),
 294    (∀ v : Fin K.nV, c B K (Sum.inl v) = cV)
 295      ∧ (∀ e : Fin K.nE, c B K (Sum.inr (Sum.inl e)) = cE)
 296      ∧ (∀ τ : Fin K.nT, c B K (Sum.inr (Sum.inr τ)) = cT)
 297
 298/-- **The premise.**  A letter's cost is a function of its kind and of nothing else, with the same
 299three reals at every complex and every cap.  What matters structurally is that this is a condition on
 300a *cost* rather than on what a weight can distinguish, which is what puts it outside the family
 301`Gap2SizeBlindnessReach`'s dichotomy covers.  Whether a substrate charges this way is a separate
 302question and no declaration here touches it. -/
 303def KindOnly (c : LetterCost) : Prop :=
 304  ∃ cV cE cT : ℝ, KindRates c cV cE cT
 305
 306/-- **The history cost of a kind-only cost is linear in the three counts.**  This is the whole
 307mechanism: the alphabet has one letter per cell, so summing a per-kind charge over it counts
 308cells. -/
 309theorem historyCost_of_kindRates {c : LetterCost} {cV cE cT : ℝ} (h : KindRates c cV cE cT)
 310    (B : ℕ) (K : BoundedComplex B) :
 311    historyCost c B K = cV * (K.nV : ℝ) + cE * (K.nE : ℝ) + cT * (K.nT : ℝ) := by
 312  classical
 313  obtain ⟨hV, hE, hT⟩ := h B K
 314  unfold historyCost
 315  rw [Fintype.sum_sum_type, Fintype.sum_sum_type]
 316  have e1 : ∑ v : Fin K.nV, c B K (Sum.inl v) = (K.nV : ℝ) * cV := by
 317    rw [Finset.sum_congr rfl (fun v _ => hV v), Finset.sum_const, Finset.card_univ,
 318      Fintype.card_fin, nsmul_eq_mul]
 319  have e2 : ∑ e : Fin K.nE, c B K (Sum.inr (Sum.inl e)) = (K.nE : ℝ) * cE := by
 320    rw [Finset.sum_congr rfl (fun e _ => hE e), Finset.sum_const, Finset.card_univ,
 321      Fintype.card_fin, nsmul_eq_mul]
 322  have e3 : ∑ τ : Fin K.nT, c B K (Sum.inr (Sum.inr τ)) = (K.nT : ℝ) * cT := by
 323    rw [Finset.sum_congr rfl (fun τ _ => hT τ), Finset.sum_const, Finset.card_univ,
 324      Fintype.card_fin, nsmul_eq_mul]
 325  rw [e1, e2, e3]
 326  ring
 327
 328/-- A kind-only cost is equivariant.  Recorded so that §4's cost cannot be dismissed for
 329being equivariant when the intended one is too. -/
 330theorem kindOnly_equivariant {c : LetterCost} (h : KindOnly c) : Equivariant c := by
 331  obtain ⟨cV, cE, cT, hc⟩ := h
 332  intro B K K' r a
 333  rcases a with x | (y | z)
 334  · rw [show postingAlphEquiv r.vEquiv r.eEquiv r.tEquiv (Sum.inl x)
 335        = Sum.inl (r.vEquiv x) from rfl, (hc B K').1, (hc B K).1]
 336  · rw [show postingAlphEquiv r.vEquiv r.eEquiv r.tEquiv (Sum.inr (Sum.inl y))
 337        = Sum.inr (Sum.inl (r.eEquiv y)) from rfl, (hc B K').2.1, (hc B K).2.1]
 338  · rw [show postingAlphEquiv r.vEquiv r.eEquiv r.tEquiv (Sum.inr (Sum.inr z))
 339        = Sum.inr (Sum.inr (r.tEquiv z)) from rfl, (hc B K').2.2, (hc B K).2.2]
 340
 341/-- **THEOREM (a kind-only posting cost gives premise (i)).**  The posted weight of a
 342kind-only cost is size-blind, in exactly the sense `Gap2SizeBlindnessReach.SizeBlind` states
 343and therefore in exactly the sense premise (i) needs. -/
 344theorem postedWeight_sizeBlind {c : LetterCost} (h : KindOnly c) :
 345    SizeBlind (postedWeight c) := by
 346  obtain ⟨cV, cE, cT, hc⟩ := h
 347  intro B B' K L hv he ht
 348  unfold postedWeight gibbsWeight
 349  rw [historyCost_of_kindRates hc B K, historyCost_of_kindRates hc B' L, hv, he, ht]
 350
 351/-- **THEOREM (premise (i), in the derivation's own words).**  `Gap2GluingDerivation` states
 352premise (i) as "the labeled weight is `sizeWeight f` for some size function `f`".  A kind-only
 353posting cost produces such an `f`. -/
 354theorem posting_cost_derives_premise_one {c : LetterCost} (h : KindOnly c) :
 355    ∃ f : ℕ → ℕ → ℕ → ℝ, ∀ (B : ℕ) (K : BoundedComplex B),
 356      postedWeight c B K = sizeWeight f K :=
 357  (sizeBlind_iff_exists_sizeFun (postedWeight c)).mp (postedWeight_sizeBlind h)
 358
 359/-- **THEOREM (the three normalizations pin all three rates to zero).**  Stated for any cost whose
 360history cost is linear in the three counts, because §7 needs it at a premise strictly weaker than
 361kind-only.  The gauge volume is `1` at each of the three atoms, so a unit weight there forces a
 362unit Boltzmann factor, and a unit Boltzmann factor forces the exponent to vanish.  The three atoms
 363are `bouquet 0 0`, `bouquet 1 0` and `bouquet 0 1`, at sizes `(1,0,0)`, `(1,1,0)` and
 364`(1,0,1)`. -/
 365theorem linearCost_atoms_force_zero {c : LetterCost} {cV cE cT : ℝ}
 366    (hlin : ∀ (B : ℕ) (K : BoundedComplex B),
 367      historyCost c B K = cV * (K.nV : ℝ) + cE * (K.nE : ℝ) + cT * (K.nT : ℝ))
 368    (hn : NormalizedAtTheAtoms (postedWeight c)) : cV = 0 ∧ cE = 0 ∧ cT = 0 := by
 369  have hone : ∀ (B : ℕ) (K : BoundedComplex B), K.nV = 1 → K.nE + K.nT ≤ 1 →
 370      Real.exp (-(cV * (K.nV : ℝ) + cE * (K.nE : ℝ) + cT * (K.nT : ℝ))) = 1 := by
 371    intro B K hv hi
 372    have h1 := hn B K hv hi
 373    unfold postedWeight at h1
 374    rw [hlin B K, gibbsWeight_eq_one_at_atoms K hv hi, mul_one] at h1
 375    exact h1
 376  have hV : cV = 0 := by
 377    have h1 := hone _ (bouquet 0 0) rfl (by norm_num)
 378    simp only [bouquet_nV, bouquet_nE, bouquet_nT, Nat.cast_one, Nat.cast_zero,
 379      mul_one, mul_zero, add_zero] at h1
 380    rw [← Real.exp_zero] at h1
 381    have := Real.exp_eq_exp.mp h1
 382    linarith
 383  have hE : cE = 0 := by
 384    have h1 := hone _ (bouquet 1 0) rfl (by norm_num)
 385    simp only [bouquet_nV, bouquet_nE, bouquet_nT, Nat.cast_one, Nat.cast_zero,
 386      mul_one, mul_zero, add_zero] at h1
 387    rw [← Real.exp_zero] at h1
 388    have := Real.exp_eq_exp.mp h1
 389    linarith
 390  have hT : cT = 0 := by
 391    have h1 := hone _ (bouquet 0 1) rfl (by norm_num)
 392    simp only [bouquet_nV, bouquet_nE, bouquet_nT, Nat.cast_one, Nat.cast_zero,
 393      mul_one, mul_zero, add_zero] at h1
 394    rw [← Real.exp_zero] at h1
 395    have := Real.exp_eq_exp.mp h1
 396    linarith
 397  exact ⟨hV, hE, hT⟩
 398
 399/-- The kind-only case, which is the one §3 uses. -/
 400theorem kindRates_atoms_force_zero {c : LetterCost} {cV cE cT : ℝ} (hc : KindRates c cV cE cT)
 401    (hn : NormalizedAtTheAtoms (postedWeight c)) : cV = 0 ∧ cE = 0 ∧ cT = 0 :=
 402  linearCost_atoms_force_zero (historyCost_of_kindRates hc) hn
 403
 404/-- **THEOREM (the posted weight is forced to be the Gibbs weight).**  A kind-only cost that
 405is unit at the three atoms charges nothing at all, so the weight is one unit of recognition
 406per gauge orbit of the alphabet. -/
 407theorem posting_cost_derives_gibbs {c : LetterCost} (h : KindOnly c)
 408    (hn : NormalizedAtTheAtoms (postedWeight c)) (B : ℕ) (K : BoundedComplex B) :
 409    postedWeight c B K = gibbsWeight K := by
 410  obtain ⟨cV, cE, cT, hc⟩ := h
 411  obtain ⟨hV, hE, hT⟩ := kindRates_atoms_force_zero hc hn
 412  unfold postedWeight
 413  rw [historyCost_of_kindRates hc B K, hV, hE, hT]
 414  simp only [zero_mul, add_zero, neg_zero, Real.exp_zero, one_mul]
 415
 416/-- The class mass of the Gibbs weight is the RS measure.  This is the deflation theorem at
 417unit tilt; no gluing premise is involved. -/
 418theorem classMass_gibbsWeight_eq_mu (K : BoundedComplex B) :
 419    classMass (fun K' : BoundedComplex B => gibbsWeight K')
 420      (Quotient.mk (relabelSetoid B) K) = mu K := by
 421  have h : (fun K' : BoundedComplex B => gibbsWeight K') = statWeight loopStat 1 B := by
 422    funext K'
 423    unfold statWeight
 424    rw [one_pow, one_mul]
 425  rw [h]
 426  exact classMass_statWeight_at_one loopStat K
 427
 428/-- **THE DERIVATION.**  If the ledger cost of a history is the sum of its letters' costs, a
 429letter's cost depends only on its kind, and the three atoms are free, then the class measure
 430is `mu K = 1/|Aut K|` for every complex at every cap.
 431
 432Premise (ii) of `Gap2GluingDerivation`, gluing multiplicativity, is not used anywhere in the
 433chain that proves this, and neither is any restriction on which pairs glue.  The `1/|Aut|`
 434comes from the deflation theorem, which needs only premise (i), and the three rates are pinned
 435by the normalizations directly rather than through a recursion.  So this derivation replaces
 436premise (i) by a posting-layer premise and drops premise (ii) entirely. -/
 437theorem posting_cost_derives_mu {c : LetterCost} (h : KindOnly c)
 438    (hn : NormalizedAtTheAtoms (postedWeight c)) (B : ℕ) (K : BoundedComplex B) :
 439    classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K := by
 440  have hfun : postedWeight c B = fun K' : BoundedComplex B => gibbsWeight K' := by
 441    funext K'
 442    exact posting_cost_derives_gibbs h hn B K'
 443  rw [hfun]
 444  exact classMass_gibbsWeight_eq_mu K
 445
 446/-! ### The two premises, made visible in the statement
 447
 448`postedWeight` bakes the gauge divisor into a definition, and a definition is not a premise a
 449reader can see.  It is one: the claim that a labeled complex carries one unit of recognition
 450divided by the number of ways to hand out its letters.  `PostedBy` says it out loud, and
 451`measure_from_posting_premises` is the derivation with both premises in the binders. -/
 452
 453/-- **`w` is posted by the letter cost `c`.**  Two assumptions in one predicate, and they are
 454the two the derivation runs on: the charge of a complex is the *sum* of its letters' charges
 455(ledger additivity over postings, which is `historyCost`), and the unit of recognition is
 456shared evenly over the alphabet's gauge orbits (the divisor).  Neither mentions what the
 457weight can or cannot distinguish. -/
 458def PostedBy (w : ∀ B : ℕ, BoundedComplex B → ℝ) (c : LetterCost) : Prop :=
 459  ∀ (B : ℕ) (K : BoundedComplex B),
 460    w B K = Real.exp (-(historyCost c B K)) / (Nat.card (AlphabetGauge K) : ℝ)
 461
 462theorem postedBy_postedWeight (c : LetterCost) : PostedBy (postedWeight c) c := by
 463  intro B K
 464  unfold postedWeight
 465  rw [gibbsWeight_eq_inv_card_alphabetGauge]
 466  ring
 467
 468theorem postedBy_eq_postedWeight {w : ∀ B : ℕ, BoundedComplex B → ℝ} {c : LetterCost}
 469    (h : PostedBy w c) (B : ℕ) (K : BoundedComplex B) : w B K = postedWeight c B K := by
 470  rw [h B K]
 471  unfold postedWeight
 472  rw [gibbsWeight_eq_inv_card_alphabetGauge]
 473  ring
 474
 475/-- **THE DERIVATION, with every premise in the binders.**  A weight posted by a kind-only
 476letter cost and unit at the three atoms is the Gibbs weight, and its class measure is
 477`mu K = 1/|Aut K|`, at every complex and every cap.
 478
 479Three binders, packing five assumptions.  `PostedBy` is ledger additivity over postings, plus the
 480charge entering through `exp`, plus even sharing of the unit over the alphabet's gauge orbits.
 481`KindOnly` is that a letter's charge depends on its kind alone, with the same rates everywhere.
 482`NormalizedAtTheAtoms` is the three unit normalizations the derivation module also assumes.
 483**Premise (ii), gluing multiplicativity, appears nowhere.**
 484
 485The honest comparison with `Gap2GluingDerivation`, since these premises are not weaker: the first
 486two jointly imply premise (i) and are not implied by it (`sizeBlind_not_always_posted`).  What the
 487strengthening buys is that premise (ii) is gone and that the surviving premises constrain a *cost*
 488rather than a weight's resolving power, which is the family `Gap2SizeBlindnessReach`'s dichotomy
 489covers.  Say that carefully: the dichotomy does not show resolving-power premises *cannot* supply
 490premise (i), since a coarse one does supply it; what it shows is that none of them supplies it while
 491being strictly weaker than it. -/
 492theorem measure_from_posting_premises {w : ∀ B : ℕ, BoundedComplex B → ℝ} {c : LetterCost}
 493    (hpost : PostedBy w c) (hkind : KindOnly c) (hn : NormalizedAtTheAtoms w) (B : ℕ)
 494    (K : BoundedComplex B) :
 495    w B K = gibbsWeight K
 496      ∧ classMass (w B) (Quotient.mk (relabelSetoid B) K) = mu K := by
 497  have hfun : w = postedWeight c := by
 498    funext B' K'
 499    exact postedBy_eq_postedWeight hpost B' K'
 500  subst hfun
 501  exact ⟨posting_cost_derives_gibbs hkind hn B K, posting_cost_derives_mu hkind hn B K⟩
 502
 503/-! ### What premise (i) is, exactly, at the posting layer
 504
 505Premise (i) is not `KindOnly`.  It is the weaker condition that the *total* charge is a
 506function of the three counts, and the equivalence is exact.  Saying so is what keeps the
 507derivation from claiming more than it does: `KindOnly` fixes each single posting's charge, globally,
 508and premise (i) constrains only the total. -/
 509
 510/-- The total charge is a function of the three counts. -/
 511def CostSizeBlind (c : LetterCost) : Prop :=
 512  ∀ (B B' : ℕ) (K : BoundedComplex B) (L : BoundedComplex B'),
 513    K.nV = L.nV → K.nE = L.nE → K.nT = L.nT → historyCost c B K = historyCost c B' L
 514
 515/-- **THEOREM (premise (i) at the posting layer, exactly).**  A posted weight is size-blind
 516precisely when its total charge is a function of the three counts.  So the posting presentation
 517does not weaken premise (i) by itself; it relocates it to the cost. -/
 518theorem postedWeight_sizeBlind_iff (c : LetterCost) :
 519    SizeBlind (postedWeight c) ↔ CostSizeBlind c := by
 520  constructor
 521  · intro h B B' K L hv he ht
 522    have hEq := h B B' K L hv he ht
 523    unfold postedWeight at hEq
 524    have hgib : gibbsWeight K = gibbsWeight L := by
 525      unfold gibbsWeight
 526      rw [hv, he, ht]
 527    have hpos : (0 : ℝ) < gibbsWeight L := gibbsWeight_positive L
 528    rw [hgib] at hEq
 529    have hexp : Real.exp (-(historyCost c B K)) = Real.exp (-(historyCost c B' L)) :=
 530      mul_right_cancel₀ hpos.ne' hEq
 531    have := Real.exp_eq_exp.mp hexp
 532    linarith
 533  · intro h B B' K L hv he ht
 534    unfold postedWeight
 535    rw [h B B' K L hv he ht]
 536    unfold gibbsWeight
 537    rw [hv, he, ht]
 538
 539theorem kindOnly_costSizeBlind {c : LetterCost} (h : KindOnly c) : CostSizeBlind c := by
 540  obtain ⟨cV, cE, cT, hc⟩ := h
 541  intro B B' K L hv he ht
 542  rw [historyCost_of_kindRates hc B K, historyCost_of_kindRates hc B' L, hv, he, ht]
 543
 544/-- A letter cost that charges each vertex letter the vertex count.  Its total charge is
 545`nV²`, a function of the counts, so it satisfies premise (i); and it is not kind-only, since
 546the rate varies with the complex. -/
 547def squareCost : LetterCost := fun _ K a =>
 548  match a with
 549  | Sum.inl _ => (K.nV : ℝ)
 550  | Sum.inr _ => 0
 551
 552theorem historyCost_squareCost (B : ℕ) (K : BoundedComplex B) :
 553    historyCost squareCost B K = (K.nV : ℝ) * (K.nV : ℝ) := by
 554  classical
 555  unfold historyCost squareCost
 556  rw [Fintype.sum_sum_type]
 557  simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
 558  ring
 559
 560/-- **THEOREM (kind-only is strictly stronger than premise (i) at the cost layer too).**  A
 561cost whose per-letter rate reads the vertex count is size-blind at the level of totals and is
 562not kind-only.  So the derivation's premise is genuinely a locality assumption about single
 563postings, not premise (i) in disguise, and the module says so rather than letting a reader
 564assume the two coincide. -/
 565theorem costSizeBlind_not_kindOnly :
 566    CostSizeBlind squareCost ∧ ¬ KindOnly squareCost := by
 567  refine ⟨?_, ?_⟩
 568  · intro B B' K L hv _ _
 569    rw [historyCost_squareCost, historyCost_squareCost, hv]
 570  · rintro ⟨cV, cE, cT, hc⟩
 571    have h1 : (0 : ℕ) < 1 := by norm_num
 572    have h2 : (0 : ℕ) < 2 := by norm_num
 573    have hd1 : squareCost 1 (dust 1) (Sum.inl ⟨0, h1⟩) = cV := (hc 1 (dust 1)).1 ⟨0, h1⟩
 574    have hd2 : squareCost 2 (dust 2) (Sum.inl ⟨0, h2⟩) = cV := (hc 2 (dust 2)).1 ⟨0, h2⟩
 575    have e1 : squareCost 1 (dust 1) (Sum.inl ⟨0, h1⟩) = ((dust 1).nV : ℝ) := rfl
 576    have e2 : squareCost 2 (dust 2) (Sum.inl ⟨0, h2⟩) = ((dust 2).nV : ℝ) := rfl
 577    rw [e1, dust_nV] at hd1
 578    rw [e2, dust_nV] at hd2
 579    rw [← hd1] at hd2
 580    norm_num at hd2
 581
 582/-! ### What premise (ii) was doing, and what replaced it
 583
 584"Gluing multiplicativity is gone" invites the reading that it was doing nothing.  It was.  In
 585`Gap2GluingDerivation` premise (ii) drives a recursion that propagates the three unit
 586normalizations from the atoms out to every size triple.  Premise (i) alone does not do that: the
 587atoms are three points and a function of the counts is not determined by three of its values.
 588
 589What replaces it here is not nothing, it is **linearity**.  A per-letter charge summed over an
 590alphabet with one letter per cell is linear in the counts, and a linear function that vanishes
 591at those three points vanishes everywhere.  So the trade is precise: premise (ii)'s propagation
 592job is done by the linearity that per-letter charging supplies for free, and the theorem below
 593measures that the job is real, by exhibiting a cost that satisfies premise (i) and the three
 594normalizations and still gets the weight wrong. -/
 595
 596/-- A cost charging each vertex letter one unit per *other* vertex.  Its total is the number of
 597ordered pairs of distinct vertices, `nV(nV-1)`, which vanishes on every one-vertex complex. -/
 598def pairCost : LetterCost := fun _ K a =>
 599  match a with
 600  | Sum.inl _ => (K.nV : ℝ) - 1
 601  | Sum.inr _ => 0
 602
 603theorem historyCost_pairCost (B : ℕ) (K : BoundedComplex B) :
 604    historyCost pairCost B K = (K.nV : ℝ) * ((K.nV : ℝ) - 1) := by
 605  classical
 606  unfold historyCost pairCost
 607  rw [Fintype.sum_sum_type]
 608  simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
 609  ring
 610
 611/-- **THEOREM (premise (i) plus the three normalizations do not give the Gibbs weight).**  The
 612pair cost satisfies premise (i), since its total is a function of the vertex count, and it is
 613unit at all three atoms, since its total vanishes whenever `nV = 1`.  Its weight at two isolated
 614vertices is `exp(-2)` times the Gibbs weight, so it is not the Gibbs weight, and the derivation's
 615conclusion fails at the first link of the chain.
 616
 617This is what premise (ii) was for in `Gap2GluingDerivation`, and what the linearity of per-letter
 618charging replaces here.  It also shows the `KindOnly` premise is not decoration on top of premise
 619(i): drop linearity, keep everything else, and the derivation stops. -/
 620theorem costSizeBlind_and_atoms_do_not_give_gibbs :
 621    CostSizeBlind pairCost
 622      ∧ NormalizedAtTheAtoms (postedWeight pairCost)
 623      ∧ ¬ KindOnly pairCost
 624      ∧ postedWeight pairCost 2 (dust 2) ≠ gibbsWeight (dust 2) := by
 625  refine ⟨?_, ?_, ?_, ?_⟩
 626  · intro B B' K L hv _ _
 627    rw [historyCost_pairCost, historyCost_pairCost, hv]
 628  · intro B K hv hi
 629    unfold postedWeight
 630    rw [historyCost_pairCost, hv, gibbsWeight_eq_one_at_atoms K hv hi]
 631    norm_num
 632  · rintro ⟨cV, cE, cT, hc⟩
 633    have h1 : (0 : ℕ) < 1 := by norm_num
 634    have h2 : (0 : ℕ) < 2 := by norm_num
 635    have hd1 : pairCost 1 (dust 1) (Sum.inl ⟨0, h1⟩) = cV := (hc 1 (dust 1)).1 ⟨0, h1⟩
 636    have hd2 : pairCost 2 (dust 2) (Sum.inl ⟨0, h2⟩) = cV := (hc 2 (dust 2)).1 ⟨0, h2⟩
 637    have e1 : pairCost 1 (dust 1) (Sum.inl ⟨0, h1⟩) = ((dust 1).nV : ℝ) - 1 := rfl
 638    have e2 : pairCost 2 (dust 2) (Sum.inl ⟨0, h2⟩) = ((dust 2).nV : ℝ) - 1 := rfl
 639    rw [e1, dust_nV] at hd1
 640    rw [e2, dust_nV] at hd2
 641    rw [← hd1] at hd2
 642    norm_num at hd2
 643  · unfold postedWeight
 644    rw [historyCost_pairCost, dust_nV]
 645    intro hEq
 646    have hpos : (0 : ℝ) < gibbsWeight (dust 2) := gibbsWeight_positive (dust 2)
 647    have hone : Real.exp (-((2 : ℝ) * ((2 : ℝ) - 1))) = 1 := by
 648      have : Real.exp (-((2 : ℝ) * ((2 : ℝ) - 1))) * gibbsWeight (dust 2)
 649          = 1 * gibbsWeight (dust 2) := by rw [one_mul]; exact_mod_cast hEq
 650      exact mul_right_cancel₀ hpos.ne' this
 651    rw [← Real.exp_zero] at hone
 652    have := Real.exp_eq_exp.mp hone
 653    norm_num at this
 654
 655/-! ### The premise set is satisfied, at the intended point -/
 656
 657/-- The letter cost that charges nothing. -/
 658def zeroCost : LetterCost := fun _ _ _ => 0
 659
 660theorem zeroCost_kindRates : KindRates zeroCost 0 0 0 :=
 661  fun _ _ => ⟨fun _ => rfl, fun _ => rfl, fun _ => rfl⟩
 662
 663theorem zeroCost_kindOnly : KindOnly zeroCost :=
 664  ⟨0, 0, 0, zeroCost_kindRates⟩
 665
 666theorem postedWeight_zeroCost (B : ℕ) (K : BoundedComplex B) :
 667    postedWeight zeroCost B K = gibbsWeight K := by
 668  unfold postedWeight historyCost zeroCost
 669  simp
 670
 671theorem zeroCost_normalizedAtTheAtoms : NormalizedAtTheAtoms (postedWeight zeroCost) := by
 672  intro B K hv hi
 673  rw [postedWeight_zeroCost]
 674  exact gibbsWeight_eq_one_at_atoms K hv hi
 675
 676/-- **Non-vacuity.**  The premises of the derivation are satisfiable, and satisfied exactly at
 677the intended answer: a free ledger posts the Gibbs weight and returns `mu`. -/
 678theorem posting_premises_satisfiable :
 679    KindOnly zeroCost ∧ NormalizedAtTheAtoms (postedWeight zeroCost)
 680      ∧ (∀ (B : ℕ) (K : BoundedComplex B), postedWeight zeroCost B K = gibbsWeight K)
 681      ∧ (∀ (B : ℕ) (K : BoundedComplex B),
 682          classMass (postedWeight zeroCost B) (Quotient.mk (relabelSetoid B) K) = mu K) :=
 683  ⟨zeroCost_kindOnly, zeroCost_normalizedAtTheAtoms, postedWeight_zeroCost,
 684    fun B K => posting_cost_derives_mu zeroCost_kindOnly zeroCost_normalizedAtTheAtoms B K⟩
 685
 686/-! ## §4. The cost that reads incidence: equivariant, normalized, and not kind-only -/
 687
 688/-- The **incidence-aware letter cost**: an edge letter whose two endpoints differ costs `t`,
 689every other letter is free.  A perfectly well-formed charging rule at the posting layer. -/
 690def incidenceCost (t : ℝ) : LetterCost := fun _ K a =>
 691  match a with
 692  | Sum.inl _ => 0
 693  | Sum.inr (Sum.inl e) => if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then t else 0
 694  | Sum.inr (Sum.inr _) => 0
 695
 696@[simp] theorem incidenceCost_inl (t : ℝ) (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV) :
 697    incidenceCost t B K (Sum.inl v) = 0 := rfl
 698
 699@[simp] theorem incidenceCost_edge (t : ℝ) (B : ℕ) (K : BoundedComplex B) (e : Fin K.nE) :
 700    incidenceCost t B K (Sum.inr (Sum.inl e))
 701      = if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then t else 0 := rfl
 702
 703@[simp] theorem incidenceCost_tet (t : ℝ) (B : ℕ) (K : BoundedComplex B) (τ : Fin K.nT) :
 704    incidenceCost t B K (Sum.inr (Sum.inr τ)) = 0 := rfl
 705
 706/-- **The history cost of the incidence cost is `t` times the proper-edge count.**  So the
 707statistic `Gap2SizeBlindnessReach` used as an escape is exactly what a posting ledger charges
 708under this rule. -/
 709theorem historyCost_incidenceCost (t : ℝ) (B : ℕ) (K : BoundedComplex B) :
 710    historyCost (incidenceCost t) B K = t * (properEdgeCount K : ℝ) := by
 711  classical
 712  unfold historyCost
 713  rw [Fintype.sum_sum_type, Fintype.sum_sum_type]
 714  simp only [incidenceCost_inl, incidenceCost_edge, incidenceCost_tet,
 715    Finset.sum_const_zero, zero_add, add_zero]
 716  rw [← Finset.sum_filter, Finset.sum_const, nsmul_eq_mul]
 717  unfold properEdgeCount
 718  ring
 719
 720/-- **THEOREM (the incidence cost reproduces the escape).**  Its posted weight is the
 721proper-edge escape weight of `Gap2SizeBlindnessReach` at tilt `exp(-t)`.  Since the two functions are
 722equal, everything the reach bound proved about that weight holds of this posted weight.  What that
 723licenses is that the escape is realizable *inside this formalism*, as the posted weight of a
 724well-formed letter cost; it says nothing about what a substrate posts. -/
 725theorem postedWeight_incidenceCost (t : ℝ) (B : ℕ) (K : BoundedComplex B) :
 726    postedWeight (incidenceCost t) B K = statWeight properStat (Real.exp (-t)) B K := by
 727  have hpow : ∀ n : ℕ, Real.exp (-(t * (n : ℝ))) = Real.exp (-t) ^ n := by
 728    intro n
 729    induction n with
 730    | zero => simp
 731    | succ k ih =>
 732      have hstep : -(t * ((k + 1 : ℕ) : ℝ)) = -(t * (k : ℝ)) + -t := by push_cast; ring
 733      rw [hstep, Real.exp_add, ih, pow_succ]
 734  unfold postedWeight statWeight
 735  rw [historyCost_incidenceCost, hpow]
 736  rfl
 737
 738theorem postedWeight_incidenceCost_eq (t : ℝ) :
 739    postedWeight (incidenceCost t) = statWeight properStat (Real.exp (-t)) := by
 740  funext B K
 741  exact postedWeight_incidenceCost t B K
 742
 743theorem exp_neg_pos (t : ℝ) : 0 < Real.exp (-t) := Real.exp_pos _
 744
 745theorem exp_neg_ne_one {t : ℝ} (ht : t ≠ 0) : Real.exp (-t) ≠ 1 := by
 746  intro h
 747  rw [← Real.exp_zero] at h
 748  have := Real.exp_eq_exp.mp h
 749  exact ht (by linarith)
 750
 751/-- **THEOREM (the incidence cost is gauge-equivariant).**  A relabeling carries an edge with
 752distinct endpoints to an edge with distinct endpoints, so the charge transports.  This is the
 753theorem that closes the obvious escape from §5: one cannot rule the incidence cost out for
 754breaking gauge invariance, because it does not. -/
 755theorem incidenceCost_equivariant (t : ℝ) : Equivariant (incidenceCost t) := by
 756  intro B K K' r a
 757  rcases a with x | (y | z)
 758  · rfl
 759  · rw [show postingAlphEquiv r.vEquiv r.eEquiv r.tEquiv (Sum.inr (Sum.inl y))
 760        = Sum.inr (Sum.inl (r.eEquiv y)) from rfl, incidenceCost_edge, incidenceCost_edge]
 761    exact if_congr (not_congr (loop_iff_of_relabel r y).symm) rfl rfl
 762  · rfl
 763
 764/-- Every edge of `twoBridges` has distinct endpoints. -/
 765theorem twoBridges_edges_proper : ∀ e : Fin twoBridges.nE,
 766    (twoBridges.edgeVerts e).1 ≠ (twoBridges.edgeVerts e).2 := by decide
 767
 768/-- No edge of `twoLoops` has distinct endpoints. -/
 769theorem twoLoops_edges_loop : ∀ e : Fin twoLoops.nE,
 770    ¬ ((twoLoops.edgeVerts e).1 ≠ (twoLoops.edgeVerts e).2) := by decide
 771
 772/-- **THEOREM (the incidence cost is not kind-only).**  Two complexes at the same cap with the
 773same number of edges charge the same edge letter differently: `twoBridges` charges `t` and
 774`twoLoops` charges nothing.  So no triple of rates can reproduce it. -/
 775theorem incidenceCost_not_kindOnly {t : ℝ} (ht : t ≠ 0) : ¬ KindOnly (incidenceCost t) := by
 776  rintro ⟨cV, cE, cT, hc⟩
 777  have h2 : (0 : ℕ) < 2 := by norm_num
 778  have hb : incidenceCost t 2 twoBridges (Sum.inr (Sum.inl ⟨0, h2⟩)) = cE :=
 779    (hc 2 twoBridges).2.1 ⟨0, h2⟩
 780  have hl : incidenceCost t 2 twoLoops (Sum.inr (Sum.inl ⟨0, h2⟩)) = cE :=
 781    (hc 2 twoLoops).2.1 ⟨0, h2⟩
 782  rw [incidenceCost_edge, if_pos (twoBridges_edges_proper ⟨0, h2⟩)] at hb
 783  rw [incidenceCost_edge, if_neg (twoLoops_edges_loop ⟨0, h2⟩)] at hl
 784  exact ht (hb.trans hl.symm)
 785
 786/-- The posted weight of the incidence cost fails premise (i). -/
 787theorem incidencePosting_not_sizeBlind {t : ℝ} (ht : t ≠ 0) :
 788    ¬ SizeBlind (postedWeight (incidenceCost t)) := by
 789  rw [postedWeight_incidenceCost_eq]
 790  exact properEscape_not_sizeBlind (exp_neg_pos t) (exp_neg_ne_one ht)
 791
 792/-- **THEOREM.**  The posted weight of the incidence cost satisfies every hypothesis the
 793derivation places on the weight other than premise (i): relabeling invariance, strict
 794positivity, unit on the empty complex, unit at all three atoms, and gluing multiplicativity at
 795every pair whose automorphism counts multiply. -/
 796theorem incidencePosting_satisfiesTheOtherHypotheses (t : ℝ) :
 797    SatisfiesTheOtherHypotheses (postedWeight (incidenceCost t)) := by
 798  rw [postedWeight_incidenceCost_eq]
 799  exact properEscape_satisfiesTheOtherHypotheses (exp_neg_pos t)
 800
 801/-- **THEOREM.**  The class mass of the incidence-posted weight is not the RS measure. -/
 802theorem incidencePosting_classMass_ne_mu {t : ℝ} (ht : t ≠ 0) :
 803    classMass (postedWeight (incidenceCost t) 2) (Quotient.mk (relabelSetoid 2) twoBridges)
 804      ≠ mu twoBridges := by
 805  rw [postedWeight_incidenceCost_eq]
 806  exact properEscape_classMass_ne_mu (exp_neg_pos t) (exp_neg_ne_one ht)
 807
 808/-! ## §5. The named premise -/
 809
 810/-- **THE NAMED PREMISE, AS A SANDWICH.**  Three conjunct groups: what suffices, what does not
 811suffice from below, and what does not suffice from the side.
 812
 813**Sufficient.**  A ledger cost additive over postings that charges by kind alone, with free
 814atoms, forces the class measure to be `mu` at every complex and every cap, with no gluing
 815premise anywhere in the argument.  That is incidence silence doing the whole job: **a posting's
 816cost is a function of its kind and not of the incidence its letter participates in.**
 817
 818**Not sufficient from below.**  Weakening kind-only to premise (i) itself, which at this layer is
 819exactly `CostSizeBlind` (`postedWeight_sizeBlind_iff`), breaks the derivation: `pairCost` is
 820size-blind at the level of totals, unit at all three atoms, and its weight is not the Gibbs
 821weight.  So the derivation needs strictly more than premise (i) at the cost layer, which is the
 822one direction of necessity this module proves.
 823
 824**Not sufficient from the side.**  Gauge equivariance does not supply it.  For any nonzero charge
 825`t`, the cost that charges an edge letter with distinct endpoints is equivariant under every
 826relabeling, is unit at the three atoms, satisfies every remaining hypothesis of the derivation,
 827is not kind-only, and produces a weight that is not size-blind and whose class mass is not `mu`.
 828
 829**What is left open, and why the name is not "needs".**  Kind-only is strictly stronger than
 830premise (i) (`costSizeBlind_not_kindOnly`), so it would be false to say premise (i) *needs*
 831incidence silence; what needs it is this route to the *measure*, and even there the necessity
 832proved is only that the natural weakening fails.  Incidence silence is not an indistinguishability
 833premise, so `Gap2SizeBlindnessReach`'s dichotomy does not apply to it.
 834
 835**Superseded on the sufficiency side, and by a theorem in this file.**  The open question in the
 836previous paragraph, whether something strictly between `CostSizeBlind` and `KindOnly` suffices, is
 837answered yes in §7: `FixedKindTotals` is strictly between them and derives the measure
 838(`measure_from_fixedKindTotals`, `fixedKindTotals_not_kindOnly`).  So the first conjunct here is
 839true but not sharp, and the sufficient premise to cite is the aggregate one.  What survives
 840unchanged is the third group, that equivariance supplies neither. -/
 841theorem incidence_silence_suffices_and_equivariance_does_not {t : ℝ} (ht : t ≠ 0) :
 842    (∀ c : LetterCost, KindOnly c → NormalizedAtTheAtoms (postedWeight c) →
 843        ∀ (B : ℕ) (K : BoundedComplex B),
 844          classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K)
 845      ∧ (CostSizeBlind pairCost ∧ NormalizedAtTheAtoms (postedWeight pairCost)
 846          ∧ postedWeight pairCost 2 (dust 2) ≠ gibbsWeight (dust 2))
 847      ∧ Equivariant (incidenceCost t)
 848      ∧ NormalizedAtTheAtoms (postedWeight (incidenceCost t))
 849      ∧ SatisfiesTheOtherHypotheses (postedWeight (incidenceCost t))
 850      ∧ ¬ KindOnly (incidenceCost t)
 851      ∧ ¬ SizeBlind (postedWeight (incidenceCost t))
 852      ∧ classMass (postedWeight (incidenceCost t) 2)
 853          (Quotient.mk (relabelSetoid 2) twoBridges) ≠ mu twoBridges :=
 854  ⟨fun _ h hn B K => posting_cost_derives_mu h hn B K,
 855    ⟨costSizeBlind_and_atoms_do_not_give_gibbs.1,
 856      costSizeBlind_and_atoms_do_not_give_gibbs.2.1,
 857      costSizeBlind_and_atoms_do_not_give_gibbs.2.2.2⟩,
 858    incidenceCost_equivariant t,
 859    (incidencePosting_satisfiesTheOtherHypotheses t).2.2.2.1,
 860    incidencePosting_satisfiesTheOtherHypotheses t,
 861    incidenceCost_not_kindOnly ht,
 862    incidencePosting_not_sizeBlind ht,
 863    incidencePosting_classMass_ne_mu ht⟩
 864
 865/-- **THEOREM (equivariance does not separate the two costs).**  Both the intended free ledger
 866and the incidence-aware ledger are gauge-equivariant, and only the first is kind-only.  So the
 867gap between the premise the derivation needs and the gauge principle it might have hoped to
 868get it from is real, not an artifact of how equivariance was stated. -/
 869theorem equivariance_does_not_give_kindOnly {t : ℝ} (ht : t ≠ 0) :
 870    Equivariant zeroCost ∧ Equivariant (incidenceCost t)
 871      ∧ KindOnly zeroCost ∧ ¬ KindOnly (incidenceCost t) :=
 872  ⟨kindOnly_equivariant zeroCost_kindOnly, incidenceCost_equivariant t,
 873    zeroCost_kindOnly, incidenceCost_not_kindOnly ht⟩
 874
 875/-! ## §6. What the stronger premise costs, measured
 876
 877Kind-only implies premise (i) and is not implied by it.  The honest way to record that is to
 878name a size-blind weight the posting layer cannot produce, and then to say which one it is. -/
 879
 880/-- **THEOREM (kind-only is strictly stronger than premise (i)).**  The uniform labeled weight,
 881which is size-blind, is the posted weight of no kind-only cost.  The second conjunct is why that
 882is a feature: the weight so excluded is not the Gibbs weight, `1` against `1/2` at two isolated
 883vertices, so the strengthening removes a wrong answer, and the intended one is still posted
 884(`postedWeight_zeroCost`).
 885
 886The mechanism of the proof is worth stating, since it is the reason no repair rescues the
 887uniform weight: a posted weight is `exp(-linear in the counts) / gaugeVol`, so setting it equal
 888to a constant would make `gaugeVol` exponential in the counts, and a factorial is not.  Two
 889complexes suffice to see it, one vertex and two. -/
 890theorem sizeBlind_not_always_posted :
 891    (¬ ∃ c : LetterCost, KindOnly c
 892        ∧ ∀ (B : ℕ) (K : BoundedComplex B),
 893            sizeWeight (fun _ _ _ => (1 : ℝ)) K = postedWeight c B K)
 894      ∧ sizeWeight (fun _ _ _ => (1 : ℝ)) (dust 2) ≠ gibbsWeight (dust 2) := by
 895  refine ⟨?_, ?_⟩
 896  case refine_2 =>
 897    unfold sizeWeight gibbsWeight
 898    norm_num [Nat.factorial]
 899  rintro ⟨c, ⟨cV, cE, cT, hc⟩, heq⟩
 900  have hg1 : gibbsWeight (dust 1) = 1 := by
 901    unfold gibbsWeight
 902    norm_num [Nat.factorial]
 903  have hg2 : gibbsWeight (dust 2) = 1 / 2 := by
 904    unfold gibbsWeight
 905    norm_num [Nat.factorial]
 906  have h1 := heq 1 (dust 1)
 907  have h2 := heq 2 (dust 2)
 908  unfold sizeWeight postedWeight at h1 h2
 909  rw [historyCost_of_kindRates hc 1 (dust 1), hg1, mul_one] at h1
 910  rw [historyCost_of_kindRates hc 2 (dust 2), hg2] at h2
 911  simp only [dust_nV, dust_nE, dust_nT, Nat.cast_one, Nat.cast_zero, Nat.cast_ofNat,
 912    mul_one, mul_zero, add_zero] at h1 h2
 913  have hcv : cV = 0 := by
 914    rw [← Real.exp_zero] at h1
 915    have := Real.exp_eq_exp.mp h1.symm
 916    linarith
 917  rw [hcv] at h2
 918  norm_num at h2
 919
 920/-! ## §7. Where the content actually sits, measured three ways
 921
 922A cross-family referee read §1-§6 on 2026-07-29 and returned three findings that survive checking.
 923Each is a theorem below, because each one narrows a claim §1-§6 made.
 924
 925**One: the premise set is a single point.**  Kind-only plus the three normalizations force the
 926letter cost to be identically zero (`kindOnly_and_atoms_force_zeroCost`), so the collapse to
 927`gibbsWeight` happens because no nonzero kind-only cost survives normalization, not because a cost
 928was computed.  Legitimate as rigidity, and worth knowing exactly: three normalizations pin three
 929global rates, and after that the cost apparatus has no content left.
 930
 931**Two: `PostedBy` restricts almost nothing.**  Every strictly positive weight is posted by some
 932letter cost at every complex carrying at least one cell
 933(`postedBy_constrains_only_the_empty_complex`), by spreading `-log (w · gaugeVol)` evenly over the
 934letters.  So §3's framing, that naming the gauge divisor as a premise rather than hiding it in a
 935definition keeps the accounting honest, understated the situation: the divisor is not a restrictive
 936premise on its own, it is a change of variables.  The one place `PostedBy` bites is the empty complex,
 937where it forces the weight to be one.
 938
 939Two limits on that, both found later and both real.  The theorem quantifies over unrestricted letter
 940costs, and the cost it constructs is generally not kind-only, so it does **not** say `PostedBy` is
 941free given the kind clause; it says no restrictiveness is attributable to the divisor by itself.  And
 942the restrictive premises are the kind clause *and* `NormalizedAtTheAtoms`: drop the normalizations
 943and a nonzero rate triple gives a posted weight that is not the Gibbs weight, so an earlier sentence
 944here calling the kind clause the only restrictive one was wrong and is withdrawn.
 945
 946**Three, and this changes the headline: per-letter incidence silence is not the boundary.**  A
 947letter cost may read incidence at every letter of a kind and still produce the measure exactly,
 948provided what it reads cancels in that block's sum.  `centeredIncidenceCost t` charges a proper edge
 949letter
 950`t · (nE - properEdgeCount)` and a loop letter `-t · properEdgeCount`.  It is equivariant under
 951every relabeling, it is not kind-only, it reads incidence, and its total charge is zero at every
 952complex, so its posted weight is exactly `gibbsWeight` and its class measure is exactly `mu`
 953(`centeredIncidence_is_the_measure`).
 954
 955What suffices is aggregate linearity by kind: the total charge of each kind is a fixed multiple of
 956that kind's count.  `FixedKindTotals` states it.  It is strictly weaker than kind-only
 957(`fixedKindTotals_not_kindOnly`, witnessed by the centered cost), strictly stronger than premise (i)
 958at the cost layer (`pairCost`, from §3b), and with the three normalizations it derives the measure
 959(`measure_from_fixedKindTotals`; the normalizations are load-bearing there, since aggregate
 960linearity alone gives only `CostSizeBlind`).  That is the corrected named premise, and "incidence
 961silence" is the right slogan only for the aggregate, never for the letter.
 962
 963**Four, and this one is ours rather than the referee's.**  Finding one applies to the corrected
 964premise as well, one level up.  Aggregate linearity plus the three normalizations forces the whole
 965*history cost* to zero, not just three rates
 966(`fixedKindTotals_and_atoms_force_zero_historyCost`), so the Boltzmann numerator is identically
 967one and the posted weight is exactly the reciprocal gauge volume
 968(`the_measure_is_the_gauge_divisor`).  The room the aggregate premise has over kind-only is
 969therefore real at the letters and invisible at the weight: `centeredIncidenceCost` and `zeroCost`
 970are different costs with the same weight.
 971
 972**Five, and it subsumes four.**  The referee's next read found that the collapse in four is not
 973caused by any premise this module names.  `Gap2GaugeVolume.invariant_weight_gives_measure_iff` says
 974the Gibbs weight is the unique *relabeling-invariant* labeled weight whose class mass is `mu`, and
 975an equivariant cost has an invariant posted weight, so an equivariant cost posts `mu` exactly when
 976its numerator is identically one (`equivariant_posts_mu_iff_numerator_one`), with no kind clause and
 977no normalizations in the argument.  That theorem predates this module.  The honest reading is
 978therefore that the premises of §3 and §7 select *which* cost and cannot contribute a factor to the
 979answer, and that no premise on an equivariant cost ever could.
 980
 981**And one thing four got wrong, corrected here rather than left standing.**  "Every factor of `mu`
 982comes from the divisor" is false.  `classMass` sums the weight over the class, so `mu` is the orbit
 983count over the gauge volume by orbit-stabilizer, and the orbit count is a second independent
 984contributor.  What is true is that the *cost* contributes none. -/
 985
 986/-- **THEOREM (the derivation's premise set is a single point).**  A kind-only cost that is unit at
 987the three atoms is the zero cost, letter by letter.  So `posting_cost_derives_gibbs` is a rigidity
 988statement: nothing about the cost was computed, because the premises admit exactly one cost. -/
 989theorem kindOnly_and_atoms_force_zeroCost {c : LetterCost} (h : KindOnly c)
 990    (hn : NormalizedAtTheAtoms (postedWeight c)) (B : ℕ) (K : BoundedComplex B)
 991    (a : PostingAlphabet K) : c B K a = 0 := by
 992  obtain ⟨cV, cE, cT, hc⟩ := h
 993  obtain ⟨hV, hE, hT⟩ := kindRates_atoms_force_zero hc hn
 994  obtain ⟨hv, he, ht⟩ := hc B K
 995  rcases a with x | (y | z)
 996  · rw [hv x, hV]
 997  · rw [he y, hE]
 998  · rw [ht z, hT]
 999
1000/-- The number of letters is the total cell count. -/
1001theorem card_postingAlphabet (K : BoundedComplex B) :
1002    Fintype.card (PostingAlphabet K) = K.nV + K.nE + K.nT := by
1003  simp [PostingAlphabet, add_assoc]
1004
1005theorem card_alphabetGauge_pos (K : BoundedComplex B) :
1006    (0 : ℝ) < (Nat.card (AlphabetGauge K) : ℝ) := by
1007  rw [card_alphabetGauge]
1008  have h : 0 < Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) :=
1009    Nat.mul_pos (Nat.factorial_pos _)
1010      (Nat.mul_pos (Nat.factorial_pos _) (Nat.factorial_pos _))
1011  exact_mod_cast h
1012
1013/-- **THEOREM (`PostedBy` is a change of variables, not a restriction).**  Every strictly positive
1014weight is posted by some letter cost, at every complex with at least one cell: spread
1015`-log (w · gaugeVol)` evenly over the letters and the Boltzmann factor reproduces `w · gaugeVol` by
1016construction.
1017
1018So the honest reading of §3 is that the gauge divisor supplies the symmetry factor outright, and the
1019cost layer contributes only the numerator.  The single place the premise bites is the empty complex,
1020which has no letters, where the history cost is `0` and the gauge volume is `1`, so `PostedBy`
1021forces the weight to be one there. -/
1022theorem postedBy_constrains_only_the_empty_complex
1023    (w : ∀ B : ℕ, BoundedComplex B → ℝ) (hw : ∀ (B : ℕ) (K : BoundedComplex B), 0 < w B K) :
1024    ∃ c : LetterCost, ∀ (B : ℕ) (K : BoundedComplex B), 0 < K.nV + K.nE + K.nT →
1025      w B K = Real.exp (-(historyCost c B K)) / (Nat.card (AlphabetGauge K) : ℝ) := by
1026  classical
1027  refine ⟨fun B K _ => -(Real.log (w B K * (Nat.card (AlphabetGauge K) : ℝ)))
1028      / ((K.nV + K.nE + K.nT : ℕ) : ℝ), ?_⟩
1029  intro B K hN
1030  have hG := card_alphabetGauge_pos K
1031  have hwG : (0 : ℝ) < w B K * (Nat.card (AlphabetGauge K) : ℝ) := mul_pos (hw B K) hG
1032  have hN' : ((K.nV + K.nE + K.nT : ℕ) : ℝ) ≠ 0 := by
1033    have : (0 : ℝ) < ((K.nV + K.nE + K.nT : ℕ) : ℝ) := by exact_mod_cast hN
1034    exact this.ne'
1035  have hH : historyCost (fun B K _ =>
1036      -(Real.log (w B K * (Nat.card (AlphabetGauge K) : ℝ)))
1037        / ((K.nV + K.nE + K.nT : ℕ) : ℝ)) B K
1038      = -(Real.log (w B K * (Nat.card (AlphabetGauge K) : ℝ))) := by
1039    unfold historyCost
1040    rw [Finset.sum_const, Finset.card_univ, card_postingAlphabet, nsmul_eq_mul]
1041    field_simp
1042  rw [hH, neg_neg, Real.exp_log hwG]
1043  field_simp
1044
1045/-! ### The corrected premise: aggregate linearity by kind -/
1046
1047/-- `c` has **kind totals** `cV`, `cE`, `cT`: at every complex, the total charge over the vertex
1048letters is `cV · nV`, over the edge letters `cE · nE`, and over the tetrahedron letters `cT · nT`.
1049Individual letters are unconstrained, so a letter may read whatever it likes provided the block
1050sum comes out right. -/
1051def KindTotalRates (c : LetterCost) (cV cE cT : ℝ) : Prop :=
1052  ∀ (B : ℕ) (K : BoundedComplex B),
1053    (∑ v : Fin K.nV, c B K (Sum.inl v)) = cV * (K.nV : ℝ)
1054      ∧ (∑ e : Fin K.nE, c B K (Sum.inr (Sum.inl e))) = cE * (K.nE : ℝ)
1055      ∧ (∑ τ : Fin K.nT, c B K (Sum.inr (Sum.inr τ))) = cT * (K.nT : ℝ)
1056
1057/-- **The corrected premise.**  Aggregate linearity by kind. -/
1058def FixedKindTotals (c : LetterCost) : Prop := ∃ cV cE cT : ℝ, KindTotalRates c cV cE cT
1059
1060theorem historyCost_of_kindTotalRates {c : LetterCost} {cV cE cT : ℝ}
1061    (h : KindTotalRates c cV cE cT) (B : ℕ) (K : BoundedComplex B) :
1062    historyCost c B K = cV * (K.nV : ℝ) + cE * (K.nE : ℝ) + cT * (K.nT : ℝ) := by
1063  classical
1064  obtain ⟨hV, hE, hT⟩ := h B K
1065  unfold historyCost
1066  rw [Fintype.sum_sum_type, Fintype.sum_sum_type, hV, hE, hT]
1067  ring
1068
1069theorem kindRates_kindTotalRates {c : LetterCost} {cV cE cT : ℝ}
1070    (h : KindRates c cV cE cT) : KindTotalRates c cV cE cT := by
1071  classical
1072  intro B K
1073  obtain ⟨hV, hE, hT⟩ := h B K
1074  refine ⟨?_, ?_, ?_⟩
1075  · rw [Finset.sum_congr rfl (fun v _ => hV v), Finset.sum_const, Finset.card_univ,
1076      Fintype.card_fin, nsmul_eq_mul]
1077    ring
1078  · rw [Finset.sum_congr rfl (fun e _ => hE e), Finset.sum_const, Finset.card_univ,
1079      Fintype.card_fin, nsmul_eq_mul]
1080    ring
1081  · rw [Finset.sum_congr rfl (fun τ _ => hT τ), Finset.sum_const, Finset.card_univ,
1082      Fintype.card_fin, nsmul_eq_mul]
1083    ring
1084
1085theorem kindOnly_fixedKindTotals {c : LetterCost} (h : KindOnly c) : FixedKindTotals c := by
1086  obtain ⟨cV, cE, cT, hc⟩ := h
1087  exact ⟨cV, cE, cT, kindRates_kindTotalRates hc⟩
1088
1089theorem fixedKindTotals_costSizeBlind {c : LetterCost} (h : FixedKindTotals c) :
1090    CostSizeBlind c := by
1091  obtain ⟨cV, cE, cT, hc⟩ := h
1092  intro B B' K L hv he ht
1093  rw [historyCost_of_kindTotalRates hc B K, historyCost_of_kindTotalRates hc B' L, hv, he, ht]
1094
1095/-- **THEOREM (the corrected premise derives the measure).**  Aggregate linearity by kind, plus
1096the three normalizations, gives the Gibbs weight and `mu`, with no gluing premise and no
1097constraint on individual letters. -/
1098theorem measure_from_fixedKindTotals {c : LetterCost} (h : FixedKindTotals c)
1099    (hn : NormalizedAtTheAtoms (postedWeight c)) (B : ℕ) (K : BoundedComplex B) :
1100    postedWeight c B K = gibbsWeight K
1101      ∧ classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K := by
1102  obtain ⟨cV, cE, cT, hc⟩ := h
1103  have hlin := historyCost_of_kindTotalRates hc
1104  obtain ⟨hV, hE, hT⟩ := linearCost_atoms_force_zero hlin hn
1105  have hgib : ∀ (B' : ℕ) (K' : BoundedComplex B'), postedWeight c B' K' = gibbsWeight K' := by
1106    intro B' K'
1107    unfold postedWeight
1108    rw [hlin B' K', hV, hE, hT]
1109    simp only [zero_mul, add_zero, neg_zero, Real.exp_zero, one_mul]
1110  refine ⟨hgib B K, ?_⟩
1111  have hfun : postedWeight c B = fun K' : BoundedComplex B => gibbsWeight K' := by
1112    funext K'
1113    exact hgib B K'
1114  rw [hfun]
1115  exact classMass_gibbsWeight_eq_mu K
1116
1117/-! ### The cost that reads incidence and posts the measure anyway -/
1118
1119/-- The **centered** incidence cost.  A proper edge letter costs `t · (nE - properEdgeCount K)`
1120and a loop letter costs `-t · properEdgeCount K`; vertex and tetrahedron letters cost nothing.  Every
1121*edge* letter reads the incidence structure, and the edge block total is zero at every complex.  The
1122silence on the other two kinds is real and the witness does not need it broken: what it refutes is
1123that silence must hold at every letter, and one kind's letters suffice for that. -/
1124def centeredIncidenceCost (t : ℝ) : LetterCost := fun _ K a =>
1125  match a with
1126  | Sum.inl _ => 0
1127  | Sum.inr (Sum.inl e) =>
1128      t * ((if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then (K.nE : ℝ) else 0)
1129            - (properEdgeCount K : ℝ))
1130  | Sum.inr (Sum.inr _) => 0
1131
1132@[simp] theorem centeredIncidenceCost_inl (t : ℝ) (B : ℕ) (K : BoundedComplex B)
1133    (v : Fin K.nV) : centeredIncidenceCost t B K (Sum.inl v) = 0 := rfl
1134
1135@[simp] theorem centeredIncidenceCost_edge (t : ℝ) (B : ℕ) (K : BoundedComplex B)
1136    (e : Fin K.nE) : centeredIncidenceCost t B K (Sum.inr (Sum.inl e))
1137      = t * ((if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then (K.nE : ℝ) else 0)
1138              - (properEdgeCount K : ℝ)) := rfl
1139
1140@[simp] theorem centeredIncidenceCost_tet (t : ℝ) (B : ℕ) (K : BoundedComplex B)
1141    (τ : Fin K.nT) : centeredIncidenceCost t B K (Sum.inr (Sum.inr τ)) = 0 := rfl
1142
1143/-- **The centering identity.**  The edge letters of the centered cost sum to zero: the proper
1144edges contribute `t · nE · p` and every one of the `nE` edges is debited `t · p`. -/
1145theorem edgeSum_centeredIncidenceCost (t : ℝ) (B : ℕ) (K : BoundedComplex B) :
1146    (∑ e : Fin K.nE, centeredIncidenceCost t B K (Sum.inr (Sum.inl e))) = 0 := by
1147  classical
1148  have hp : (∑ e : Fin K.nE,
1149      (if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then (K.nE : ℝ) else 0))
1150      = (K.nE : ℝ) * (properEdgeCount K : ℝ) := by
1151    rw [← Finset.sum_filter, Finset.sum_const, nsmul_eq_mul]
1152    unfold properEdgeCount
1153    ring
1154  have hc : (∑ _e : Fin K.nE, (properEdgeCount K : ℝ))
1155      = (K.nE : ℝ) * (properEdgeCount K : ℝ) := by
1156    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
1157  simp only [centeredIncidenceCost_edge]
1158  rw [← Finset.mul_sum, Finset.sum_sub_distrib, hp, hc, sub_self, mul_zero]
1159
1160theorem historyCost_centeredIncidenceCost (t : ℝ) (B : ℕ) (K : BoundedComplex B) :
1161    historyCost (centeredIncidenceCost t) B K = 0 := by
1162  classical
1163  unfold historyCost
1164  rw [Fintype.sum_sum_type, Fintype.sum_sum_type]
1165  simp only [centeredIncidenceCost_inl, centeredIncidenceCost_tet, Finset.sum_const_zero,
1166    zero_add, add_zero]
1167  exact edgeSum_centeredIncidenceCost t B K
1168
1169theorem postedWeight_centeredIncidenceCost (t : ℝ) (B : ℕ) (K : BoundedComplex B) :
1170    postedWeight (centeredIncidenceCost t) B K = gibbsWeight K := by
1171  unfold postedWeight
1172  rw [historyCost_centeredIncidenceCost, neg_zero, Real.exp_zero, one_mul]
1173
1174/-- The centered cost is gauge-equivariant: a relabeling preserves the edge count, the
1175proper-edge count, and whether a given edge's endpoints differ. -/
1176theorem centeredIncidenceCost_equivariant (t : ℝ) : Equivariant (centeredIncidenceCost t) := by
1177  intro B K K' r a
1178  rcases a with x | (y | z)
1179  · rfl
1180  · have hE : (K'.nE : ℝ) = (K.nE : ℝ) := by rw [size_e r]
1181    have hP : (properEdgeCount K' : ℝ) = (properEdgeCount K : ℝ) := by
1182      rw [properEdgeCount_congr r]
1183    have hIf : (if (K'.edgeVerts (r.eEquiv y)).1 ≠ (K'.edgeVerts (r.eEquiv y)).2
1184          then (K'.nE : ℝ) else 0)
1185        = (if (K.edgeVerts y).1 ≠ (K.edgeVerts y).2 then (K.nE : ℝ) else 0) := by
1186      rw [hE]
1187      exact if_congr (not_congr (loop_iff_of_relabel r y).symm) rfl rfl
1188    rw [show postingAlphEquiv r.vEquiv r.eEquiv r.tEquiv (Sum.inr (Sum.inl y))
1189        = Sum.inr (Sum.inl (r.eEquiv y)) from rfl, centeredIncidenceCost_edge,
1190      centeredIncidenceCost_edge, hIf, hP]
1191  · rfl
1192
1193/-- Three vertices, one loop and one proper edge: the smallest complex whose two edge letters
1194must be charged differently by the centered cost. -/
1195def loopAndBridge : BoundedComplex 3 where
1196  nV := 3
1197  nE := 2
1198  nT := 0
1199  hV := le_refl 3
1200  hE := by norm_num
1201  hT := Nat.zero_le 3
1202  edgeVerts := fun e => if e = 0 then (0, 0) else (1, 2)
1203  tetVerts := fun t => t.elim0
1204
1205theorem properEdgeCount_loopAndBridge : properEdgeCount loopAndBridge = 1 := by decide
1206
1207theorem loopAndBridge_nE : loopAndBridge.nE = 2 := rfl
1208
1209/-- The loop letter is charged `-t · p` with `p = 1`, and the proper-edge letter `t · (nE - p)`
1210with `nE = 2`, so the two letters of the same kind are charged `-t` and `t`. -/
1211theorem centeredIncidence_charges_on_loopAndBridge (t : ℝ) :
1212    centeredIncidenceCost t 3 loopAndBridge (Sum.inr (Sum.inl ⟨0, by decide⟩)) = -t
1213      ∧ centeredIncidenceCost t 3 loopAndBridge (Sum.inr (Sum.inl ⟨1, by decide⟩)) = t := by
1214  constructor
1215  · rw [centeredIncidenceCost_edge, properEdgeCount_loopAndBridge, if_neg (by decide)]
1216    norm_num
1217  · rw [centeredIncidenceCost_edge, properEdgeCount_loopAndBridge, if_pos (by decide),
1218      loopAndBridge_nE]
1219    norm_num
1220
1221/-- **THEOREM (the centered cost is not kind-only).**  At `loopAndBridge` the loop letter is
1222charged `-t` and the proper-edge letter `t`, so no single edge rate reproduces it. -/
1223theorem centeredIncidenceCost_not_kindOnly {t : ℝ} (ht : t ≠ 0) :
1224    ¬ KindOnly (centeredIncidenceCost t) := by
1225  rintro ⟨cV, cE, cT, hc⟩
1226  obtain ⟨hloop, hprop⟩ := centeredIncidence_charges_on_loopAndBridge t
1227  have h0 : (-t : ℝ) = cE := by rw [← hloop]; exact (hc 3 loopAndBridge).2.1 _
1228  have h1 : (t : ℝ) = cE := by rw [← hprop]; exact (hc 3 loopAndBridge).2.1 _
1229  exact ht (by linarith)
1230
1231/-- **THEOREM (per-letter incidence silence is not the boundary).**  For every nonzero `t` the
1232centered cost reads incidence at every edge letter, is gauge-equivariant, is not kind-only, is
1233unit at the three atoms, and its posted weight is exactly the Gibbs weight with class measure
1234exactly `mu`.
1235
1236So a cost may see incidence and still deliver the intended measure.  What the derivation needs is
1237not silence at the letter but linearity in the aggregate, which the centered cost has: its kind
1238totals are all zero (`fixedKindTotals_centeredIncidenceCost`). -/
1239theorem centeredIncidence_is_the_measure {t : ℝ} (ht : t ≠ 0) (B : ℕ) (K : BoundedComplex B) :
1240    Equivariant (centeredIncidenceCost t)
1241      ∧ ¬ KindOnly (centeredIncidenceCost t)
1242      ∧ NormalizedAtTheAtoms (postedWeight (centeredIncidenceCost t))
1243      ∧ postedWeight (centeredIncidenceCost t) B K = gibbsWeight K
1244      ∧ classMass (postedWeight (centeredIncidenceCost t) B)
1245          (Quotient.mk (relabelSetoid B) K) = mu K := by
1246  have hgib : ∀ (B' : ℕ) (K' : BoundedComplex B'),
1247      postedWeight (centeredIncidenceCost t) B' K' = gibbsWeight K' :=
1248    fun B' K' => postedWeight_centeredIncidenceCost t B' K'
1249  refine ⟨centeredIncidenceCost_equivariant t, centeredIncidenceCost_not_kindOnly ht, ?_,
1250    hgib B K, ?_⟩
1251  · intro B' K' hv hi
1252    rw [hgib B' K']
1253    exact gibbsWeight_eq_one_at_atoms K' hv hi
1254  · have hfun : postedWeight (centeredIncidenceCost t) B
1255        = fun K' : BoundedComplex B => gibbsWeight K' := by
1256      funext K'
1257      exact hgib B K'
1258    rw [hfun]
1259    exact classMass_gibbsWeight_eq_mu K
1260
1261theorem fixedKindTotals_centeredIncidenceCost (t : ℝ) :
1262    FixedKindTotals (centeredIncidenceCost t) := by
1263  classical
1264  refine ⟨0, 0, 0, ?_⟩
1265  intro B K
1266  refine ⟨?_, ?_, ?_⟩
1267  · simp
1268  · rw [edgeSum_centeredIncidenceCost]; ring
1269  · simp
1270
1271/-- **THEOREM (aggregate linearity is strictly weaker than kind-only).**  The centered cost has
1272kind totals and is not kind-only, so the corrected premise is genuinely weaker than the one §3
1273used, and still derives the measure (`measure_from_fixedKindTotals`). -/
1274theorem fixedKindTotals_not_kindOnly {t : ℝ} (ht : t ≠ 0) :
1275    FixedKindTotals (centeredIncidenceCost t) ∧ ¬ KindOnly (centeredIncidenceCost t) :=
1276  ⟨fixedKindTotals_centeredIncidenceCost t, centeredIncidenceCost_not_kindOnly ht⟩
1277
1278/-- **THEOREM (aggregate linearity is strictly stronger than premise (i)).**  `pairCost` is
1279size-blind at the level of totals and does not have kind totals, since its vertex block sums to
1280`nV(nV-1)` rather than to a fixed multiple of `nV`.  That it is also unit at the three atoms is not a
1281conjunct here; it is `costSizeBlind_and_atoms_do_not_give_gibbs`, which is where the pair is used to
1282show the normalizations do not rescue a non-linear cost. -/
1283theorem costSizeBlind_not_fixedKindTotals :
1284    CostSizeBlind pairCost ∧ ¬ FixedKindTotals pairCost := by
1285  refine ⟨costSizeBlind_and_atoms_do_not_give_gibbs.1, ?_⟩
1286  rintro ⟨cV, cE, cT, hc⟩
1287  have h1 := historyCost_of_kindTotalRates hc 1 (dust 1)
1288  have h2 := historyCost_of_kindTotalRates hc 2 (dust 2)
1289  rw [historyCost_pairCost] at h1 h2
1290  simp only [dust_nV, dust_nE, dust_nT, Nat.cast_one, Nat.cast_zero, Nat.cast_ofNat,
1291    mul_zero, add_zero] at h1 h2
1292  norm_num at h1 h2
1293  linarith
1294
1295/-! ### How much room the corrected premise really has
1296
1297§7's third finding says the aggregate premise has room the kind-only one does not, and that is
1298true of the letter costs and false of the weight.  The two theorems below separate those, because
1299the difference is the whole honest reading of this module. -/
1300
1301/-- **THEOREM (the aggregate premise collapses too, one level up).**  Aggregate linearity by kind
1302plus the three normalizations forces the *history cost* to be identically zero, not merely at the
1303atoms.  Three normalizations pin three rates and a linear function of the counts vanishing at three
1304independent points vanishes everywhere, and this argument never looked at a single letter.
1305
1306So `measure_from_fixedKindTotals` is rigidity in exactly the way `posting_cost_derives_gibbs` was:
1307the premises admit one history cost.  What the aggregate premise buys over kind-only is a family of
1308letter costs realizing that one history cost
1309(`centeredIncidence_is_the_measure`), and the weight cannot see which member you picked. -/
1310theorem fixedKindTotals_and_atoms_force_zero_historyCost {c : LetterCost}
1311    (h : FixedKindTotals c) (hn : NormalizedAtTheAtoms (postedWeight c))
1312    (B : ℕ) (K : BoundedComplex B) : historyCost c B K = 0 := by
1313  obtain ⟨cV, cE, cT, hc⟩ := h
1314  have hlin := historyCost_of_kindTotalRates hc
1315  obtain ⟨hV, hE, hT⟩ := linearCost_atoms_force_zero hlin hn
1316  rw [hlin B K, hV, hE, hT]
1317  ring
1318
1319/-- **THEOREM (the cost layer contributes no factor of the weight).**  Under the corrected premise
1320and the three normalizations the Boltzmann numerator is identically `1`, and the posted weight is
1321exactly the reciprocal order of the alphabet's sort-respecting gauge group.
1322
1323**Two corrections to how this was first written.**  It is *not* true that "every factor of `mu`
1324comes from the divisor": `classMass` sums the weight over the class, so
1325`mu K = |orbit K| / |AlphabetGauge K|` by orbit-stabilizer
1326(`Gap2GaugeVolume.orbitCard_mul_autCard`), and the orbit count is independently load-bearing.  What
1327is true is the narrower thing this theorem says, that the *cost* contributes no factor.  And the
1328cause is not the premises named here: `equivariant_posts_mu_iff_numerator_one` gets the same
1329collapse from equivariance alone, so this theorem is a corollary of a fact the library held before
1330the module existed.  Kept because it is the form that mentions the premises a reader arrives
1331holding. -/
1332theorem the_measure_is_the_gauge_divisor {c : LetterCost} (h : FixedKindTotals c)
1333    (hn : NormalizedAtTheAtoms (postedWeight c)) (B : ℕ) (K : BoundedComplex B) :
1334    Real.exp (-(historyCost c B K)) = 1
1335      ∧ postedWeight c B K = 1 / (Nat.card (AlphabetGauge K) : ℝ)
1336      ∧ classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K := by
1337  have hz : ∀ (B' : ℕ) (K' : BoundedComplex B'), historyCost c B' K' = 0 :=
1338    fun B' K' => fixedKindTotals_and_atoms_force_zero_historyCost h hn B' K'
1339  refine ⟨by rw [hz B K, neg_zero, Real.exp_zero], ?_, (measure_from_fixedKindTotals h hn B K).2⟩
1340  unfold postedWeight
1341  rw [hz B K, neg_zero, Real.exp_zero, one_mul, gibbsWeight_eq_inv_card_alphabetGauge]
1342
1343/-! ### The collapse is not this module's premises
1344
1345A cross-family referee read §7 and found the theorem above is not the sharpest form, for a reason
1346that had been sitting in the library since before this module existed.  `Gap2GaugeVolume`'s
1347`invariant_weight_gives_measure_iff` says the Gibbs weight is the *unique* relabeling-invariant
1348labeled weight whose class mass is `mu`.  Every equivariant letter cost has a relabeling-invariant
1349posted weight (`postedWeight_invariant`).  Compose the two and the collapse to a unit numerator
1350follows from equivariance and from wanting `mu`, with no kind clause, no aggregate linearity, and no
1351atom normalizations anywhere in the argument. -/
1352
1353/-- **THEOREM (no equivariant cost contributes a factor to the measure, whatever premise picks
1354it out).**  For an equivariant letter cost, the posted weight's class mass is `mu` at every complex
1355exactly when the Boltzmann numerator is identically one.
1356
1357This subsumes `the_measure_is_the_gauge_divisor` and relocates the finding.  The collapse is not
1358caused by kind-only, by aggregate linearity, or by the three normalizations: it is caused by asking
1359a gauge-invariant cost to reproduce `mu`, and `invariant_weight_gives_measure_iff` had already
1360settled that before this module was written.  What the premises of §3 and §7 do is pick out *which*
1361cost, and the honest reading of the whole module is that they cannot do anything else.
1362
1363**Where equivariance is load-bearing, and where the statement is open.**  The reverse direction
1364needs no invariance: a unit numerator makes the posted weight the Gibbs weight outright.  The
1365forward direction runs through the uniqueness theorem and so needs it.  Whether a *non*-equivariant
1366cost can post `mu` with a numerator that is not identically one, by having the orbit sum of its
1367Boltzmann factors come out to the orbit count while the individual terms differ, is not settled
1368here; the referee's construction for it is not formalized and this docstring does not claim it. -/
1369theorem equivariant_posts_mu_iff_numerator_one {c : LetterCost} (hc : Equivariant c) (B : ℕ) :
1370    (∀ K : BoundedComplex B,
1371        classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K)
1372      ↔ ∀ K : BoundedComplex B, Real.exp (-(historyCost c B K)) = 1 := by
1373  have hinv : ∀ K K' : BoundedComplex B, Equivalent K K' →
1374      postedWeight c B K = postedWeight c B K' :=
1375    fun _ _ h => postedWeight_invariant hc h
1376  have hgibbs : (∀ K : BoundedComplex B, postedWeight c B K = gibbsWeight K)
1377      ↔ ∀ K : BoundedComplex B, Real.exp (-(historyCost c B K)) = 1 := by
1378    constructor
1379    · intro h K
1380      have hg := gibbsWeight_positive K
1381      have hK := h K
1382      unfold postedWeight at hK
1383      have hcancel : Real.exp (-(historyCost c B K)) * gibbsWeight K = 1 * gibbsWeight K := by
1384        rw [one_mul]
1385        exact hK
1386      exact mul_right_cancel₀ hg.ne' hcancel
1387    · intro h K
1388      unfold postedWeight
1389      rw [h K, one_mul]
1390  refine Iff.trans ?_ hgibbs
1391  refine Iff.trans ?_ (Gap2GaugeVolume.invariant_weight_gives_measure_iff (postedWeight c B) hinv)
1392  exact (MeasureSubstrateBlocker.gaugeCountingPrinciple_iff_mu_on_representatives
1393    (classMass (postedWeight c B))).symm
1394
1395/-! ## §8. Navigation index
1396
1397Flags only.  Two are deliberately `false`: the premise this module names is not itself derived,
1398and the cost layer is not shown to contribute any factor of the measure because
1399`equivariant_posts_mu_iff_numerator_one` proves it contributes none.  Those are the frontier
1400Gap 2's measure now sits on.  The non-equivariant case, open when this index was written, is now
1401settled affirmatively downstream: `Gap2NonEquivariantPosting.tiltedCost_posts_mu` with
1402`numerator_ne_one_at_loopAndBridge`.  A fourth flag flipped
1403to `true` in the other direction: the letter cost under §3's premises is not merely unique up to the
1404three rates, it is unique outright and equal to zero. -/
1405
1406structure PostingIndex : Type where
1407  /-- Kind-only posting costs plus free atoms derive `mu`, with no gluing premise. -/
1408  kind_only_derives_mu : Bool
1409  /-- Every premise appears in the binders of the headline, the gauge divisor included.  Three
1410  binders, packing five assumptions. -/
1411  premises_visible_in_statement : Bool
1412  /-- The Gibbs divisor is the order of the alphabet's sort-respecting gauge group. -/
1413  divisor_is_alphabet_gauge_volume : Bool
1414  /-- The incidence-aware cost is gauge-equivariant and not kind-only, so equivariance does
1415  not supply the premise. -/
1416  equivariance_insufficient : Bool
1417  /-- The incidence-aware cost reproduces the reach bound's escape, so the escape is realizable
1418  inside this formalism as the posted weight of a well-formed letter cost.  Not a claim about what a
1419  substrate posts. -/
1420  escape_is_postable : Bool
1421  /-- Kind-only is strictly stronger than premise (i), measured twice: at the uniform weight
1422  and at the cost layer. -/
1423  strictness_measured : Bool
1424  /-- The corrected premise, aggregate linearity by kind, derives `mu` and is strictly between
1425  premise (i) at the cost layer and kind-only. -/
1426  aggregate_premise_derives_mu : Bool
1427  /-- NOT proved: that the substrate forces incidence silence, at the letter or in the aggregate. -/
1428  incidence_silence_derived : Bool
1429  /-- Proved, and stronger than first flagged: under §3's premises the letter cost is unique
1430  outright, being identically zero (`kindOnly_and_atoms_force_zeroCost`).  Under §7's weaker premise
1431  it is not unique, and the history cost is (`fixedKindTotals_and_atoms_force_zero_historyCost`). -/
1432  letter_cost_unique : Bool
1433  /-- NOT proved, and in fact refuted: that the cost layer contributes any factor of the measure.
1434  Every equivariant cost posts `mu` exactly when its numerator is identically one
1435  (`equivariant_posts_mu_iff_numerator_one`), so no premise on an equivariant cost can. -/
1436  cost_layer_contributes_a_factor : Bool
1437  /-- SETTLED affirmatively downstream (`Gap2NonEquivariantPosting`): a non-equivariant cost
1438  CAN post `mu` with a numerator other than one, the orbit sum of its Boltzmann factors matching
1439  the orbit count while the terms differ (`tiltedCost_posts_mu`,
1440  `numerator_ne_one_at_loopAndBridge`, `nonequivariant_posting_family`). -/
1441  nonequivariant_numerator_settled : Bool
1442
1443def postingIndex : PostingIndex where
1444  kind_only_derives_mu := true
1445  premises_visible_in_statement := true
1446  divisor_is_alphabet_gauge_volume := true
1447  equivariance_insufficient := true
1448  escape_is_postable := true
1449  strictness_measured := true
1450  aggregate_premise_derives_mu := true
1451  incidence_silence_derived := false
1452  letter_cost_unique := true
1453  cost_layer_contributes_a_factor := false
1454  nonequivariant_numerator_settled := true
1455
1456theorem index_silence_not_derived : postingIndex.incidence_silence_derived = false := rfl
1457
1458/-- The flag reads `true` and the theorem in the file is stronger than the flag's first wording:
1459under `KindOnly` plus the atom normalizations the cost is not merely pinned up to three rates, it is
1460identically zero. -/
1461theorem index_cost_unique_under_kind_only : postingIndex.letter_cost_unique = true := rfl
1462
1463theorem index_cost_layer_contributes_nothing :
1464    postingIndex.cost_layer_contributes_a_factor = false := rfl
1465
1466/-- Settled downstream in `Gap2NonEquivariantPosting`: the non-equivariant case named in this
1467flag's original docstring is answered affirmatively by an explicit witness family. -/
1468theorem index_nonequivariant_settled : postingIndex.nonequivariant_numerator_settled = true := rfl
1469
1470end
1471
1472end Gap2PostingCostDerivation
1473end SevenGaps
1474end Gravity
1475end IndisputableMonolith
1476