IndisputableMonolith.Gravity.SevenGaps.Gap2SizeBlindnessReach

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2GluingDerivation
   2import IndisputableMonolith.Gravity.SevenGaps.GaugeHistoryMeasure
   3
   4/-!
   5# Gap 2: how far the gluing premise reaches, and why the posting layer cannot close it
   6
   7`Gap2GluingDerivation` derives the class measure from two premises plus three normalizations.
   8The premises:
   9
  10* **(i) size-blindness**, the labeled weight depends only on the three index sizes;
  11* **(ii) gluing multiplicativity**, class mass multiplies over disjoint unions at pairs
  12  where the automorphism count multiplies.
  13
  14The normalizations, assumed by the final theorem `CarrierShuffle.gibbs_of_unit_fugacities` on
  15top of the premises: the size function is `1` at the three **atoms** `(1,0,0)`, `(1,1,0)` and
  16`(1,0,1)`, the single vertex, the single loop, the single degenerate tetrahedron.  Without them
  17premise (i) and premise (ii) leave three free positive constants
  18(`residue_is_exactly_three_positive_constants`).
  19
  20Its deflation theorem (`classMass_sizeWeight_eq_fugacity_div_autCard`) showed that premise (i)
  21alone already produces the symmetry factor `q(s)/|Aut K|`.  Premise (i) is assumed.  This module
  22attacks it and reports two results, one positive and one negative.
  23
  24## §1-§3, the reach bound: the other five hypotheses do not imply premise (i)
  25
  26An **additive incidence statistic** is a natural-valued function of a complex that is
  27relabeling-invariant, adds over disjoint unions, and vanishes on the empty complex.  The three
  28index sizes qualify.  So do two functions of the incidence data: the **loop count**, the number
  29of edges whose endpoints coincide, and the **proper-edge count**, the number whose endpoints
  30differ.  §1 defines both and §2 proves both additive.
  31
  32For any such statistic and any positive real `lam`, the weight `lam ^ (stat K) / (nV! nE! nT!)`
  33is relabeling-invariant, strictly positive, unit on the empty complex, and satisfies premise (ii)
  34at every pair whose automorphism counts multiply, hence at each of the four families the
  35derivation's `CarrierShuffle` premise is stated at (`all_four_families_available` discharges the
  36hypothesis for all four; `statWeight_glues_at_dust_edge` instantiates the one with no side
  37condition).  No binomial correction appears, because the statistic adds exactly where the
  38automorphism count multiplies.  Its class mass is `lam ^ (stat K) / |Aut K|`, so it leaves the
  39symmetry factor untouched and multiplies it by `lam ^ stat`.
  40
  41The three normalizations then decide *which* statistic survives, and this is the sharpest thing
  42in §3.  They kill the loop-count escape, because the single loop has loop count one, so that
  43escape's weight there is `lam` (`loopEscape_fails_the_atoms`).  They do not touch the proper-edge
  44escape, whose statistic vanishes on every single-vertex complex, atoms included
  45(`properEdgeCount_eq_zero_of_nV_le_one`).  So the normalizations are not idle, and they are also
  46not enough.
  47
  48The proper-edge escape at any positive `lam ≠ 1` therefore satisfies invariance, positivity, unit
  49on the empty complex, unit at all three atoms, and premise (ii) at every eligible pair, is not
  50size-blind, and its class mass at the two-bridge class is `lam²/|Aut|` against the measure's
  51`1/|Aut|` (`size_blindness_not_forced_by_the_other_hypotheses`).  Both witnesses sit at sizes
  52`(2,2,0)`; at `lam = 1` the escape is the Gibbs weight and *is* size-blind
  53(`statWeight_sizeBlind_at_one`, at every statistic, so it controls the proper-edge escape and not
  54only the loop-count one), so the separation is a property of the tilt and not of a malformed
  55construction.
  56
  57**Scope.**  Premise (i) is load-bearing for the conclusion, not merely for the shape of the
  58argument.  This does not say premise (ii) is empty; the sharper statement of that is the
  59derivation module's own `gluing_alone_does_not_force_mu`.  The reach bound is stated against
  60premise (ii) in its restricted form, at eligible pairs; the escape fails the unrestricted
  61predicate `GluesGenerally` (`statWeight_not_gluesGenerally`), and so does the RS measure, which
  62is the same theorem at `lam = 1` and the reason the derivation could not have assumed the
  63unrestricted form.  Unrestricted gluing is not inconsistent on its own, since
  64`uniform_gluesGenerally` satisfies it; what `unrestricted_gluing_inconsistent` refutes is its
  65conjunction with the four restricted equations for a positive size-blind weight.  Nor is "the
  66pairs where automorphism counts multiply" a characterization of eligibility; no such
  67characterization exists in the library.
  68
  69This compiles a refutation carried only in prose since the 2026-07-28 panel killed the
  70cluster-decomposition route: an exponential in an additive incidence statistic escapes the
  71premise-(ii) side of the derivation, for *every* such statistic.  Against the full hypothesis
  72bundle the claim is narrower and the normalizations are why: only statistics vanishing at the
  73three atoms survive, which the loop count does not (`loopEscape_fails_the_atoms`) and the
  74proper-edge count does.
  75
  76## §4-§6, the negative result: no indistinguishability premise is both weaker and sufficient
  77
  78`GaugeHistoryMeasure.PostingAlphabet K` is `Fin K.nV ⊕ Fin K.nE ⊕ Fin K.nT`: the substrate
  79posts one letter per cell, sorted into three kinds, and none per incidence.  It was defined
  80for the posted-history presentation, not for this argument.  The natural hope is that premise
  81(i) is what that alphabet says, so that the premise moves from the measure to the substrate.
  82
  83§4 makes the hope precise, against the library object itself, and §5 proves it in both
  84directions: a weight is `sizeWeight f` for some size function `f` exactly when it is blind to
  85everything but the posting alphabet read with its sorting into cell kinds
  86(`premise_one_iff_alphabetBlind`).
  87
  88§6 kills the hope and then generalizes the reason.  The alphabet is a *function of* the size
  89triple (`postingAlphabet_is_determined_by_the_sizes`): two complexes with the same three
  90counts have sort-respecting equivalent posting alphabets no matter how their cells are wired,
  91the two witnesses of §3 among them.  So the alphabet carries no information about incidence to
  92begin with, and the equivalence of §5 is a reformulation rather than a derivation.
  93
  94The general form is a single equivalence, `blindness_forces_premise_one_iff_coarse`: blindness to an
  95invariant forces premise (i) for every weight **exactly when** that invariant never separates two
  96complexes with the same three counts.  The two directions are the two horns
  97(`coarse_invariant_blindness_implies_sizeBlind`,
  98`fine_invariant_blindness_does_not_imply_sizeBlind`, exhaustive by `invariant_coarse_or_fine`, and
  99available separately as `indistinguishability_premises_never_weaken_premise_one` for the fine
 100witness).  On the coarse side blindness already implies premise (i), so nothing was weakened.  On
 101the fine side it does not, witnessed by a strictly positive two-valued weight that is also
 102relabeling-invariant whenever the invariant is.  Neither horn assumes invariance, so the coverage
 103has no gap at label-sensitive readouts, and both are general rather than instantiated.
 104
 105At one fine invariant the failure survives the whole rest of the hypothesis set: the invariant
 106reading the three counts together with the proper-edge count, where the escape of §3 is blind to
 107it, satisfies all five remaining hypotheses, is not size-blind, and has the wrong class mass
 108(`fine_horn_survives_the_other_hypotheses`).  That is one invariant, chosen to contain the escape's
 109own statistic, and not a statement about the fine side in general.
 110
 111**What this licenses.**  No premise of the form *the weight cannot distinguish complexes that agree
 112on `X`* is both strictly weaker than premise (i) and sufficient for it: if it is sufficient then `X`
 113is coarse, and blindness to a coarse `X` already implies premise (i).  It does not license the
 114converse, so blindness to `X` and premise (i) are not interchangeable; the coarse side contains
 115conditions strictly stronger than premise (i) and `unsorted_is_strictly_stronger` is one.  So the hope
 116this module started from, that the substrate supplies premise (i) by not resolving incidence, is
 117closed.  The posting alphabet lands on the coarse side, which is why pointing at it does not help.
 118The coarse side is not a single point: blindness to the total cell count lands there and is strictly
 119stronger,
 120so much so that it contradicts the derivation's own conclusion
 121(`unsorted_is_strictly_stronger`), which is why "premise (i) renamed" would be the wrong reading of
 122the coarse side.
 123
 124**What it does not license, stated so no reader has to find it.**  Four things.  It does not prove
 125premise (i) needs a premise from outside this family, since the equivalence quantifies over one
 126blindness premise and not over conjunctions or over derivations.  It does not rule out that some
 127fine invariant *other* than the one instantiated might, conjoined with the five remaining
 128hypotheses, force premise (i); that conjunction is restrictive and the question is open.  The fine
 129horn's general witness carries only positivity and invariance, not the normalizations or gluing.
 130And no theorem here is about what a substrate posts or resolves; the substrate language throughout
 131is motivation for which mathematical questions were asked.  The conjecture the module leaves, tagged
 132as conjecture: the premise has to come from structure that is not a function of the complex, a cost
 133or a dynamics that assigns the weight rather than a symmetry that fails to separate it.  §8 of the
 134plan and the companion module `Gap2PostingCostDerivation` act on that conjecture.
 135-/
 136
 137namespace IndisputableMonolith
 138namespace Gravity
 139namespace SevenGaps
 140namespace Gap2SizeBlindnessReach
 141
 142open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
 143
 144/-! ## §1. An incidence statistic on the bounded carrier
 145
 146`Gap2EnrichedCarrierPhase.selfLoopCount` is the same statistic on the exact-signature
 147carrier `ExactComplex v e t`.  The path-sum measure lives on `BoundedComplex B`, so the
 148statistic has to be recreated here; the invariance argument is the same one. -/
 149
 150variable {B B' : ℕ}
 151
 152/-- The number of edges of `K` whose two endpoints coincide.  A function of the incidence
 153data that is *not* a function of the three index sizes. -/
 154def loopCount (K : BoundedComplex B) : ℕ :=
 155  (Finset.univ.filter (fun i : Fin K.nE => (K.edgeVerts i).1 = (K.edgeVerts i).2)).card
 156
 157theorem loopCount_eq_sum (K : BoundedComplex B) :
 158    loopCount K
 159      = ∑ i : Fin K.nE, (if (K.edgeVerts i).1 = (K.edgeVerts i).2 then 1 else 0) := by
 160  unfold loopCount
 161  rw [Finset.card_filter]
 162
 163/-- A relabeling carries loop edges to loop edges, because it acts on endpoints by an
 164injection. -/
 165theorem loop_iff_of_relabel {K K' : BoundedComplex B} (r : Relabel K K') (i : Fin K.nE) :
 166    ((K.edgeVerts i).1 = (K.edgeVerts i).2)
 167      ↔ ((K'.edgeVerts (r.eEquiv i)).1 = (K'.edgeVerts (r.eEquiv i)).2) := by
 168  rw [r.edge_comm i]
 169  simp only [Prod.map_fst, Prod.map_snd]
 170  exact (r.vEquiv.injective.eq_iff).symm
 171
 172/-- **THEOREM (the loop count is a class function).**  Relabeling-invariant, so it descends
 173to relabeling classes, exactly as the three index sizes do. -/
 174theorem loopCount_congr {K K' : BoundedComplex B} (r : Relabel K K') :
 175    loopCount K = loopCount K' := by
 176  classical
 177  unfold loopCount
 178  refine Finset.card_bij (fun i _ => r.eEquiv i) ?_ ?_ ?_
 179  · intro i hi
 180    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi ⊢
 181    exact (loop_iff_of_relabel r i).mp hi
 182  · intro i _ j _ h
 183    exact r.eEquiv.injective h
 184  · intro j hj
 185    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hj
 186    refine ⟨r.eEquiv.symm j, ?_, by simp⟩
 187    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
 188    have := (loop_iff_of_relabel r (r.eEquiv.symm j)).mpr
 189    simpa using this (by simpa using hj)
 190
 191theorem loopCount_invariant {K K' : BoundedComplex B} (h : Equivalent K K') :
 192    loopCount K = loopCount K' := by
 193  obtain ⟨r⟩ := h
 194  exact loopCount_congr r
 195
 196/-! ## §2. The loop count adds over disjoint unions
 197
 198This is what lets the escape weight satisfy premise (ii) with no correction: the statistic
 199is additive exactly where the automorphism count is multiplicative. -/
 200
 201theorem inlV_inj {m n : ℕ} {a b : Fin m} (h : (inlV a : Fin (m + n)) = inlV b) : a = b :=
 202  Sum.inl_injective (finSumFinEquiv.injective h)
 203
 204theorem inrV_inj {m n : ℕ} {a b : Fin n} (h : (inrV a : Fin (m + n)) = inrV b) : a = b :=
 205  Sum.inr_injective (finSumFinEquiv.injective h)
 206
 207@[simp] theorem dunion_edgeVerts_inl (K : BoundedComplex B) (L : BoundedComplex B')
 208    (e : Fin K.nE) :
 209    (dunion K L).edgeVerts (finSumFinEquiv (Sum.inl e))
 210      = (inlV (K.edgeVerts e).1, inlV (K.edgeVerts e).2) := by
 211  simp [dunion]
 212
 213@[simp] theorem dunion_edgeVerts_inr (K : BoundedComplex B) (L : BoundedComplex B')
 214    (e : Fin L.nE) :
 215    (dunion K L).edgeVerts (finSumFinEquiv (Sum.inr e))
 216      = (inrV (L.edgeVerts e).1, inrV (L.edgeVerts e).2) := by
 217  simp [dunion]
 218
 219/-- **THEOREM (the loop count is additive over disjoint unions).** -/
 220theorem loopCount_dunion (K : BoundedComplex B) (L : BoundedComplex B') :
 221    loopCount (dunion K L) = loopCount K + loopCount L := by
 222  classical
 223  rw [loopCount_eq_sum, loopCount_eq_sum, loopCount_eq_sum]
 224  have h1 : (∑ i : Fin (dunion K L).nE,
 225        (if ((dunion K L).edgeVerts i).1 = ((dunion K L).edgeVerts i).2 then 1 else 0))
 226      = ∑ s : Fin K.nE ⊕ Fin L.nE,
 227          (if ((dunion K L).edgeVerts (finSumFinEquiv s)).1
 228              = ((dunion K L).edgeVerts (finSumFinEquiv s)).2 then 1 else 0) :=
 229    (Fintype.sum_equiv finSumFinEquiv _ _ (fun _ => rfl)).symm
 230  rw [h1, Fintype.sum_sum_type]
 231  congr 1
 232  · refine Finset.sum_congr rfl (fun e _ => ?_)
 233    rw [dunion_edgeVerts_inl]
 234    by_cases hc : (K.edgeVerts e).1 = (K.edgeVerts e).2
 235    · simp [hc]
 236    · simp only [if_neg hc]
 237      rw [if_neg (fun h => hc (inlV_inj h))]
 238  · refine Finset.sum_congr rfl (fun e _ => ?_)
 239    rw [dunion_edgeVerts_inr]
 240    by_cases hc : (L.edgeVerts e).1 = (L.edgeVerts e).2
 241    · simp [hc]
 242    · simp only [if_neg hc]
 243      rw [if_neg (fun h => hc (inrV_inj h))]
 244
 245theorem loopCount_emptyComplex (B : ℕ) : loopCount (emptyComplex B) = 0 := by
 246  simp [loopCount, emptyComplex]
 247
 248/-! ### A second statistic, which survives the three unit normalizations
 249
 250The derivation's final step assumes more than the two premises.
 251`Gap2GluingDerivation.CarrierShuffle.gibbs_of_unit_fugacities` also assumes the size function
 252is `1` at the three **atoms** `(1,0,0)`, `(1,1,0)` and `(1,0,1)`: the single vertex, the single
 253loop, the single degenerate tetrahedron.  Translated off the size function and onto a labeled
 254weight, that says the weight is `1` at every complex with one vertex and at most one incidence.
 255
 256Those three normalizations kill the loop-count escape, since the single loop has loop count one
 257(`loopEscape_fails_the_atoms`).  That is a real strength measurement: the normalizations are not
 258idle.  They do not kill the mechanism.  The number of edges whose endpoints *differ* is also an
 259additive incidence statistic, it vanishes at every complex with one vertex, and it still
 260separates the two witnesses of §3, in the other direction. -/
 261
 262/-- The number of edges of `K` whose two endpoints differ.  Like `loopCount` this is a function
 263of the incidence data and not of the three sizes; unlike `loopCount` it vanishes at every
 264complex with a single vertex, which is what the three unit normalizations require. -/
 265def properEdgeCount (K : BoundedComplex B) : ℕ :=
 266  (Finset.univ.filter (fun i : Fin K.nE => (K.edgeVerts i).1 ≠ (K.edgeVerts i).2)).card
 267
 268theorem properEdgeCount_eq_sum (K : BoundedComplex B) :
 269    properEdgeCount K
 270      = ∑ i : Fin K.nE, (if (K.edgeVerts i).1 ≠ (K.edgeVerts i).2 then 1 else 0) := by
 271  unfold properEdgeCount
 272  rw [Finset.card_filter]
 273
 274theorem properEdgeCount_congr {K K' : BoundedComplex B} (r : Relabel K K') :
 275    properEdgeCount K = properEdgeCount K' := by
 276  classical
 277  unfold properEdgeCount
 278  refine Finset.card_bij (fun i _ => r.eEquiv i) ?_ ?_ ?_
 279  · intro i hi
 280    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi ⊢
 281    exact fun hc => hi ((loop_iff_of_relabel r i).mpr hc)
 282  · intro i _ j _ h
 283    exact r.eEquiv.injective h
 284  · intro j hj
 285    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hj
 286    refine ⟨r.eEquiv.symm j, ?_, by simp⟩
 287    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
 288    intro hc
 289    exact hj (by simpa using (loop_iff_of_relabel r (r.eEquiv.symm j)).mp hc)
 290
 291theorem properEdgeCount_invariant {K K' : BoundedComplex B} (h : Equivalent K K') :
 292    properEdgeCount K = properEdgeCount K' := by
 293  obtain ⟨r⟩ := h
 294  exact properEdgeCount_congr r
 295
 296@[simp] theorem inlV_eq_iff {m n : ℕ} {a b : Fin m} :
 297    (inlV a : Fin (m + n)) = inlV b ↔ a = b :=
 298  ⟨inlV_inj, fun h => by rw [h]⟩
 299
 300@[simp] theorem inrV_eq_iff {m n : ℕ} {a b : Fin n} :
 301    (inrV a : Fin (m + n)) = inrV b ↔ a = b :=
 302  ⟨inrV_inj, fun h => by rw [h]⟩
 303
 304/-- **THEOREM (the proper-edge count is additive over disjoint unions).** -/
 305theorem properEdgeCount_dunion (K : BoundedComplex B) (L : BoundedComplex B') :
 306    properEdgeCount (dunion K L) = properEdgeCount K + properEdgeCount L := by
 307  classical
 308  rw [properEdgeCount_eq_sum, properEdgeCount_eq_sum, properEdgeCount_eq_sum]
 309  have h1 : (∑ i : Fin (dunion K L).nE,
 310        (if ((dunion K L).edgeVerts i).1 ≠ ((dunion K L).edgeVerts i).2 then 1 else 0))
 311      = ∑ s : Fin K.nE ⊕ Fin L.nE,
 312          (if ((dunion K L).edgeVerts (finSumFinEquiv s)).1
 313              ≠ ((dunion K L).edgeVerts (finSumFinEquiv s)).2 then 1 else 0) :=
 314    (Fintype.sum_equiv finSumFinEquiv _ _ (fun _ => rfl)).symm
 315  rw [h1, Fintype.sum_sum_type]
 316  congr 1
 317  · refine Finset.sum_congr rfl (fun e _ => ?_)
 318    rw [dunion_edgeVerts_inl]
 319    simp
 320  · refine Finset.sum_congr rfl (fun e _ => ?_)
 321    rw [dunion_edgeVerts_inr]
 322    simp
 323
 324/-- **THEOREM (the proper-edge count vanishes on every single-vertex complex).**  With one
 325vertex there is nothing for an edge's two endpoints to differ between.  This is what makes the
 326escape built from it satisfy the three unit normalizations. -/
 327theorem properEdgeCount_eq_zero_of_nV_le_one (K : BoundedComplex B) (h : K.nV ≤ 1) :
 328    properEdgeCount K = 0 := by
 329  classical
 330  unfold properEdgeCount
 331  rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
 332  intro i _
 333  simp only [ne_eq, not_not]
 334  have h1 : ((K.edgeVerts i).1 : ℕ) < 1 := lt_of_lt_of_le (K.edgeVerts i).1.isLt h
 335  have h2 : ((K.edgeVerts i).2 : ℕ) < 1 := lt_of_lt_of_le (K.edgeVerts i).2.isLt h
 336  exact Fin.ext (by omega)
 337
 338theorem properEdgeCount_emptyComplex (B : ℕ) : properEdgeCount (emptyComplex B) = 0 :=
 339  properEdgeCount_eq_zero_of_nV_le_one _ (by simp [emptyComplex])
 340
 341/-! ## §3. The escape mechanism, and the reach bound -/
 342
 343/-- An **additive incidence statistic**: a natural-valued function of a complex that is
 344relabeling-invariant, adds over disjoint unions, and vanishes on the empty complex.
 345
 346The three index sizes satisfy this, and so does the loop count, which is why this is the
 347exact level of generality at which the restricted gluing premise fails to force premise (i):
 348the premise sees the additivity and cannot see whether the statistic reads incidence. -/
 349structure AdditiveStat where
 350  stat : ∀ B : ℕ, BoundedComplex B → ℕ
 351  invariant : ∀ (B : ℕ) (K K' : BoundedComplex B), Equivalent K K' → stat B K = stat B K'
 352  additive : ∀ (B B' : ℕ) (K : BoundedComplex B) (L : BoundedComplex B'),
 353    stat (B + B') (dunion K L) = stat B K + stat B' L
 354  vanishes : ∀ B : ℕ, stat B (emptyComplex B) = 0
 355
 356/-- The loop count is an additive incidence statistic.  It ignores the cap argument, so the
 357escape built from it is a single function of a complex and not a cap-indexed family. -/
 358def loopStat : AdditiveStat where
 359  stat := fun _ K => loopCount K
 360  invariant := fun _ _ _ h => loopCount_invariant h
 361  additive := fun _ _ K L => loopCount_dunion K L
 362  vanishes := fun B => loopCount_emptyComplex B
 363
 364/-- The proper-edge count is an additive incidence statistic. -/
 365def properStat : AdditiveStat where
 366  stat := fun _ K => properEdgeCount K
 367  invariant := fun _ _ _ h => properEdgeCount_invariant h
 368  additive := fun _ _ K L => properEdgeCount_dunion K L
 369  vanishes := fun B => properEdgeCount_emptyComplex B
 370
 371/-- The **escape weight** of a statistic: the inverse gauge volume tilted by an exponential in that
 372statistic.  At `lam = 1` this is `gibbsWeight` and is size-blind.
 373
 374At other positive `lam` what holds depends on the statistic, and the general facts are only the
 375four proved below: invariance, positivity, unit on the empty complex, and premise (ii) at every
 376eligible pair.  Whether it is size-blind, and whether it is unit at the three atoms, are both
 377properties of the particular statistic.  A statistic that is constant leaves the weight size-blind;
 378`loopStat` fails the atoms (`loopEscape_fails_the_atoms`); `properStat` fails size-blindness while
 379satisfying the atoms, which is the combination the reach bound needs. -/
 380noncomputable def statWeight (φ : AdditiveStat) (lam : ℝ) (B : ℕ) (K : BoundedComplex B) :
 381    ℝ :=
 382  lam ^ (φ.stat B K) * gibbsWeight K
 383
 384theorem gibbsWeight_positive (K : BoundedComplex B) : 0 < gibbsWeight K := by
 385  unfold gibbsWeight
 386  have hGn : 0 < Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) :=
 387    Nat.mul_pos (Nat.factorial_pos _)
 388      (Nat.mul_pos (Nat.factorial_pos _) (Nat.factorial_pos _))
 389  have hG : (0 : ℝ)
 390      < ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) := by
 391    exact_mod_cast hGn
 392  positivity
 393
 394theorem statWeight_invariant (φ : AdditiveStat) (lam : ℝ) {K K' : BoundedComplex B}
 395    (h : Equivalent K K') : statWeight φ lam B K = statWeight φ lam B K' := by
 396  unfold statWeight
 397  rw [φ.invariant B K K' h, gibbsWeight_invariant h]
 398
 399theorem statWeight_pos (φ : AdditiveStat) {lam : ℝ} (hlam : 0 < lam) (B : ℕ)
 400    (K : BoundedComplex B) : 0 < statWeight φ lam B K :=
 401  mul_pos (pow_pos hlam _) (gibbsWeight_positive K)
 402
 403theorem statWeight_emptyComplex (φ : AdditiveStat) (lam : ℝ) (B : ℕ) :
 404    statWeight φ lam B (emptyComplex B) = 1 := by
 405  unfold statWeight gibbsWeight
 406  rw [φ.vanishes B]
 407  norm_num [emptyComplex]
 408
 409/-- **THEOREM (the class mass of an escape weight).**  The symmetry factor survives
 410untouched; the tilt sits beside it as a factor `lam ^ stat`. -/
 411theorem classMass_statWeight (φ : AdditiveStat) (lam : ℝ) (K : BoundedComplex B) :
 412    classMass (statWeight φ lam B) (Quotient.mk (relabelSetoid B) K)
 413      = lam ^ (φ.stat B K) / (Nat.card (Aut K) : ℝ) := by
 414  classical
 415  rw [classMass_of_invariant _ (fun _ _ h => statWeight_invariant φ lam h)]
 416  have hout : statWeight φ lam B (Quotient.out (Quotient.mk (relabelSetoid B) K))
 417      = statWeight φ lam B K :=
 418    statWeight_invariant φ lam (equivalent_out K)
 419  rw [hout, orbitCardClass_mk]
 420  have hA : (0 : ℝ) < (Nat.card (Aut K) : ℝ) := by exact_mod_cast autCard_pos K
 421  have hGn : 0 < Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) :=
 422    Nat.mul_pos (Nat.factorial_pos _)
 423      (Nat.mul_pos (Nat.factorial_pos _) (Nat.factorial_pos _))
 424  have hG : (0 : ℝ)
 425      < ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) := by
 426    exact_mod_cast hGn
 427  have hGc : (gaugeOrbitCard K : ℝ) * (Nat.card (Aut K) : ℝ)
 428      = ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) := by
 429    exact_mod_cast orbitCard_mul_autCard K
 430  unfold statWeight gibbsWeight
 431  rw [eq_div_iff hA.ne']
 432  calc (gaugeOrbitCard K : ℝ)
 433        * (lam ^ (φ.stat B K)
 434            * (1 / ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)))
 435        * (Nat.card (Aut K) : ℝ)
 436      = lam ^ (φ.stat B K)
 437          * (((gaugeOrbitCard K : ℝ) * (Nat.card (Aut K) : ℝ))
 438              / ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)) := by
 439        ring
 440    _ = lam ^ (φ.stat B K) := by rw [hGc, div_self hG.ne', mul_one]
 441
 442/-- **THEOREM (the escape satisfies premise (ii) where the derivation uses it).**  At every
 443pair whose automorphism counts multiply, the class mass of an escape weight multiplies over
 444the disjoint union, with no binomial correction.  `all_four_families_available` discharges
 445this hypothesis at all four families `CarrierShuffle` is stated at.
 446
 447This is the *restricted* premise.  The unrestricted predicate `GluesGenerally` is a different and
 448stronger condition, which the escape fails (`statWeight_not_gluesGenerally`).  It is not
 449inconsistent by itself: `uniform_gluesGenerally` satisfies it.  What
 450`unrestricted_gluing_inconsistent` refutes is the conjunction of unrestricted gluing with the four
 451restricted equations, for a positive weight that is already size-blind. -/
 452theorem statWeight_glues (φ : AdditiveStat) (lam : ℝ) (K : BoundedComplex B)
 453    (L : BoundedComplex B')
 454    (haut : Nat.card (Aut (dunion K L)) = Nat.card (Aut K) * Nat.card (Aut L)) :
 455    classMass (statWeight φ lam (B + B'))
 456        (Quotient.mk (relabelSetoid (B + B')) (dunion K L))
 457      = classMass (statWeight φ lam B) (Quotient.mk (relabelSetoid B) K)
 458        * classMass (statWeight φ lam B') (Quotient.mk (relabelSetoid B') L) := by
 459  rw [classMass_statWeight, classMass_statWeight, classMass_statWeight,
 460    φ.additive B B' K L, haut, pow_add]
 461  push_cast
 462  rw [div_mul_div_comm]
 463
 464/-- Premise (ii) for the escape at one of the four families the derivation's `CarrierShuffle`
 465premise is actually stated at, instantiated to show the hypothesis of `statWeight_glues` is
 466really discharged somewhere and the theorem is not idle. -/
 467theorem statWeight_glues_at_dust_edge (φ : AdditiveStat) (lam : ℝ) (a : ℕ) :
 468    classMass (statWeight φ lam (a + 2))
 469        (Quotient.mk (relabelSetoid (a + 2)) (dunion (dust a) edge))
 470      = classMass (statWeight φ lam a) (Quotient.mk (relabelSetoid a) (dust a))
 471        * classMass (statWeight φ lam 2) (Quotient.mk (relabelSetoid 2) edge) :=
 472  statWeight_glues φ lam (dust a) edge (autMul_dust_edge a)
 473
 474/-- **THEOREM (the escape fails the unrestricted premise, and for the intended measure's own
 475reason).**  No escape weight satisfies `GluesGenerally`, for any additive statistic and any
 476positive `lam`.  The failure is at `dust 1 ⊔ dust 1`, where the automorphism count does *not*
 477multiply: two isolated vertices can be exchanged, so `|Aut (dust 2)| = 2` while each part is
 478rigid.  The statistic contributes nothing to the discrepancy, since it adds on both sides; the
 479whole of it is the symmetry factor.
 480
 481That is what "exactly where the intended measure fails it too" means, and it is not a figure of
 482speech: `lam = 1` is allowed here, and at `lam = 1` the escape *is* the Gibbs weight, so this
 483theorem also proves the RS measure fails unrestricted gluing.  Unrestricted gluing is therefore
 484not a hypothesis the derivation could have used, which is why `Gap2GluingDerivation` states
 485premise (ii) at eligible pairs only. -/
 486theorem statWeight_not_gluesGenerally (φ : AdditiveStat) {lam : ℝ} (hlam : 0 < lam) :
 487    ¬ GluesGenerally (statWeight φ lam) := by
 488  intro h
 489  have hEq := h (dust 1) (dust 1)
 490  rw [classMass_statWeight, classMass_statWeight, φ.additive 1 1 (dust 1) (dust 1)] at hEq
 491  have hA1 : Nat.card (Aut (dust 1)) = 1 := by
 492    rw [autCard_dust]; simp [Nat.factorial]
 493  have hA2 : Nat.card (Aut (dunion (dust 1) (dust 1))) = 2 := by
 494    rw [autCard_congr (dunion_dust_equivalent 1 1), autCard_dust]
 495    norm_num [Nat.factorial]
 496  rw [hA1, hA2, pow_add] at hEq
 497  push_cast at hEq
 498  have hX : (0 : ℝ) < lam ^ (φ.stat 1 (dust 1)) * lam ^ (φ.stat 1 (dust 1)) :=
 499    mul_pos (pow_pos hlam _) (pow_pos hlam _)
 500  linarith
 501
 502/-! ### The two witnesses: same sizes, different loop counts -/
 503
 504/-- Two loops at vertex `0`: sizes `(2,2,0)`. -/
 505def twoLoops : BoundedComplex 2 where
 506  nV := 2
 507  nE := 2
 508  nT := 0
 509  hV := le_refl 2
 510  hE := le_refl 2
 511  hT := Nat.zero_le 2
 512  edgeVerts := fun _ => (0, 0)
 513  tetVerts := fun t => t.elim0
 514
 515/-- Two parallel non-loop edges `(0,1)`: sizes `(2,2,0)`, the same triple. -/
 516def twoBridges : BoundedComplex 2 where
 517  nV := 2
 518  nE := 2
 519  nT := 0
 520  hV := le_refl 2
 521  hE := le_refl 2
 522  hT := Nat.zero_le 2
 523  edgeVerts := fun _ => (0, 1)
 524  tetVerts := fun t => t.elim0
 525
 526@[simp] theorem loopCount_twoLoops : loopCount twoLoops = 2 := by decide
 527
 528@[simp] theorem loopCount_twoBridges : loopCount twoBridges = 0 := by decide
 529
 530@[simp] theorem properEdgeCount_twoLoops : properEdgeCount twoLoops = 0 := by decide
 531
 532@[simp] theorem properEdgeCount_twoBridges : properEdgeCount twoBridges = 2 := by decide
 533
 534theorem twoLoops_sizes : twoLoops.nV = 2 ∧ twoLoops.nE = 2 ∧ twoLoops.nT = 0 :=
 535  ⟨rfl, rfl, rfl⟩
 536
 537theorem twoBridges_sizes : twoBridges.nV = 2 ∧ twoBridges.nE = 2 ∧ twoBridges.nT = 0 :=
 538  ⟨rfl, rfl, rfl⟩
 539
 540/-- The two witnesses have the same three counts, so the loop count is not a function of
 541them.  This is the whole reason the escape exists. -/
 542theorem witnesses_same_sizes_different_loops :
 543    (twoLoops.nV = twoBridges.nV ∧ twoLoops.nE = twoBridges.nE ∧ twoLoops.nT = twoBridges.nT)
 544      ∧ loopCount twoLoops ≠ loopCount twoBridges := by
 545  refine ⟨⟨rfl, rfl, rfl⟩, ?_⟩
 546  rw [loopCount_twoLoops, loopCount_twoBridges]
 547  decide
 548
 549/-! ### Size-blindness, and the reach bound -/
 550
 551/-- **Premise (i), size-blindness, as a relation rather than as a constructor.**  A weight
 552family is size-blind when it agrees on any two complexes, at any two caps, whose three index
 553sizes agree.  §5 proves this equivalent to being `sizeWeight f` for some `f`, which is the
 554constructor form the derivation uses. -/
 555def SizeBlind (w : ∀ B : ℕ, BoundedComplex B → ℝ) : Prop :=
 556  ∀ (B B' : ℕ) (K : BoundedComplex B) (L : BoundedComplex B'),
 557    K.nV = L.nV → K.nE = L.nE → K.nT = L.nT → w B K = w B' L
 558
 559theorem sizeWeight_sizeBlind (f : ℕ → ℕ → ℕ → ℝ) :
 560    SizeBlind (fun _ K => sizeWeight f K) := by
 561  intro _ _ K L hv he ht
 562  simp only [sizeWeight, hv, he, ht]
 563
 564/-- A positive real other than one has square other than one.  The only place the tilt's
 565nontriviality is used, extracted so both escapes share it. -/
 566theorem sq_ne_one_of_pos_ne_one {lam : ℝ} (hlam : 0 < lam) (hne : lam ≠ 1) : lam ^ 2 ≠ 1 := by
 567  intro h2
 568  have hfac : (lam - 1) * (lam + 1) = 0 := by linear_combination h2
 569  rcases mul_eq_zero.mp hfac with hz | hz
 570  · exact hne (by linarith)
 571  · linarith
 572
 573/-- **THEOREM (the loop-count escape is not size-blind).** -/
 574theorem loopEscape_not_sizeBlind {lam : ℝ} (hlam : 0 < lam) (hne : lam ≠ 1) :
 575    ¬ SizeBlind (statWeight loopStat lam) := by
 576  intro h
 577  have hEq := h 2 2 twoLoops twoBridges rfl rfl rfl
 578  have hgib : gibbsWeight twoLoops = gibbsWeight twoBridges := rfl
 579  have hgpos : (0 : ℝ) < gibbsWeight twoBridges := gibbsWeight_positive twoBridges
 580  simp only [statWeight, loopStat, loopCount_twoLoops, loopCount_twoBridges, pow_zero,
 581    one_mul, hgib] at hEq
 582  have h2 : lam ^ 2 = 1 := by
 583    have hcanc : lam ^ 2 * gibbsWeight twoBridges = 1 * gibbsWeight twoBridges := by
 584      rw [one_mul]; exact hEq
 585    exact mul_right_cancel₀ (ne_of_gt hgpos) hcanc
 586  exact sq_ne_one_of_pos_ne_one hlam hne h2
 587
 588/-- **THEOREM (the proper-edge escape is not size-blind).**  Same two witnesses, separated in
 589the other direction: `twoBridges` carries the tilt and `twoLoops` does not. -/
 590theorem properEscape_not_sizeBlind {lam : ℝ} (hlam : 0 < lam) (hne : lam ≠ 1) :
 591    ¬ SizeBlind (statWeight properStat lam) := by
 592  intro h
 593  have hEq := h 2 2 twoBridges twoLoops rfl rfl rfl
 594  have hgib : gibbsWeight twoBridges = gibbsWeight twoLoops := rfl
 595  have hgpos : (0 : ℝ) < gibbsWeight twoLoops := gibbsWeight_positive twoLoops
 596  simp only [statWeight, properStat, properEdgeCount_twoLoops, properEdgeCount_twoBridges,
 597    pow_zero, one_mul, hgib] at hEq
 598  have h2 : lam ^ 2 = 1 := by
 599    have hcanc : lam ^ 2 * gibbsWeight twoLoops = 1 * gibbsWeight twoLoops := by
 600      rw [one_mul]; exact hEq
 601    exact mul_right_cancel₀ (ne_of_gt hgpos) hcanc
 602  exact sq_ne_one_of_pos_ne_one hlam hne h2
 603
 604/-! ### The three unit normalizations, and which escape survives them -/
 605
 606/-- **The three unit normalizations, translated onto the labeled weight.**
 607`gibbs_of_unit_fugacities` assumes `f 1 0 0 = f 1 1 0 = f 1 0 1 = 1`.  Off the size function,
 608that is exactly this: the weight is `1` at every complex with one vertex and at most one
 609incidence, which are the three atoms and nothing else. -/
 610def NormalizedAtTheAtoms (w : ∀ B : ℕ, BoundedComplex B → ℝ) : Prop :=
 611  ∀ (B : ℕ) (K : BoundedComplex B), K.nV = 1 → K.nE + K.nT ≤ 1 → w B K = 1
 612
 613theorem gibbsWeight_eq_one_at_atoms (K : BoundedComplex B) (hv : K.nV = 1)
 614    (hi : K.nE + K.nT ≤ 1) : gibbsWeight K = 1 := by
 615  have hE : K.nE = 0 ∨ K.nE = 1 := by omega
 616  have hT : K.nT = 0 ∨ K.nT = 1 := by omega
 617  unfold gibbsWeight
 618  rcases hE with hE | hE <;> rcases hT with hT | hT <;>
 619    rw [hv, hE, hT] <;> norm_num [Nat.factorial]
 620
 621/-- **THEOREM (the proper-edge escape satisfies the three unit normalizations).**  Its
 622statistic vanishes on every single-vertex complex, and the gauge volume is one there. -/
 623theorem properEscape_normalizedAtTheAtoms (lam : ℝ) :
 624    NormalizedAtTheAtoms (statWeight properStat lam) := by
 625  intro B K hv hi
 626  unfold statWeight
 627  have hs : properStat.stat B K = 0 :=
 628    properEdgeCount_eq_zero_of_nV_le_one K (by omega)
 629  rw [hs, pow_zero, one_mul, gibbsWeight_eq_one_at_atoms K hv hi]
 630
 631/-- **THEOREM (the three normalizations kill the loop-count escape).**  At the single loop the
 632loop count is one, so the loop-count escape's weight there is `lam`.  The normalizations
 633therefore have real discriminating power, and the reach bound has to be carried by a statistic
 634that vanishes at the atoms, which is why `properStat` exists. -/
 635theorem loopEscape_fails_the_atoms {lam : ℝ} (hne : lam ≠ 1) :
 636    ¬ NormalizedAtTheAtoms (statWeight loopStat lam) := by
 637  intro h
 638  have hbad := h 2 (bouquet 1 0) rfl (by norm_num)
 639  have hloop : loopCount (bouquet 1 0) = 1 := by decide
 640  have hgib : gibbsWeight (bouquet 1 0) = 1 := by
 641    unfold gibbsWeight
 642    norm_num [Nat.factorial]
 643  simp only [statWeight, loopStat, hloop, hgib, pow_one, mul_one] at hbad
 644  exact hne hbad
 645
 646/-- **Control for the reach bound, at every statistic.**  At `lam = 1` the escape weight *is* the
 647Gibbs weight and *is* size-blind, whichever statistic it was built from.  So the failure at
 648`lam ≠ 1` is a property of the tilt, not an artifact of the construction, and the two witnesses are
 649separating rather than merely different.  Without this the reach bound would be consistent with the
 650escape being malformed.  Stated for a general statistic so that it controls the proper-edge escape
 651the reach bound actually uses, not only the loop-count one. -/
 652theorem statWeight_sizeBlind_at_one (φ : AdditiveStat) : SizeBlind (statWeight φ 1) := by
 653  have h : ∀ (B : ℕ) (K : BoundedComplex B), statWeight φ 1 B K = gibbsWeight K := by
 654    intro B K
 655    simp [statWeight]
 656  intro B B' K L hv he ht
 657  rw [h, h]
 658  unfold gibbsWeight
 659  rw [hv, he, ht]
 660
 661/-- The control at the loop-count statistic. -/
 662theorem loopEscape_sizeBlind_at_one : SizeBlind (statWeight loopStat 1) :=
 663  statWeight_sizeBlind_at_one loopStat
 664
 665/-- The control at the proper-edge statistic, which is the one the reach bound uses. -/
 666theorem properEscape_sizeBlind_at_one : SizeBlind (statWeight properStat 1) :=
 667  statWeight_sizeBlind_at_one properStat
 668
 669/-- **Every hypothesis the derivation places on the labeled weight except premise (i).**  Five
 670clauses: relabeling invariance, strict positivity, unit on the empty complex, unit at the three
 671atoms, and premise (ii) at every pair whose automorphism counts multiply.
 672
 673The correspondence with `Gap2GluingDerivation`, stated exactly.  Its final theorem is
 674`CarrierShuffle.gibbs_of_unit_fugacities`, whose hypotheses are: the weight is `sizeWeight f`
 675for some `f` (premise (i)); `CarrierShuffle f`, which is `f` positive, `f 0 0 0 = 1`, and four
 676shuffle equations that `gluesAt_of_shuffle` shows are premise (ii) at four eligible families;
 677and `f 1 0 0 = f 1 1 0 = f 1 0 1 = 1`.  Clauses two through five are those, transported off the
 678size function so they can be stated without assuming premise (i).  Clause one is invariance,
 679which the class mass needs to be well defined at all.
 680
 681**One asymmetry, stated rather than hidden.**  Clause five is premise (ii) at *every* eligible
 682pair, which is stronger than the four families the derivation consumes, so a weight satisfying
 683this bundle satisfies more than the derivation asks, not less. -/
 684def SatisfiesTheOtherHypotheses (w : ∀ B : ℕ, BoundedComplex B → ℝ) : Prop :=
 685  (∀ (B : ℕ) (K K' : BoundedComplex B), Equivalent K K' → w B K = w B K')
 686    ∧ (∀ (B : ℕ) (K : BoundedComplex B), 0 < w B K)
 687    ∧ (∀ B : ℕ, w B (emptyComplex B) = 1)
 688    ∧ NormalizedAtTheAtoms w
 689    ∧ (∀ (B B' : ℕ) (K : BoundedComplex B) (L : BoundedComplex B'),
 690        Nat.card (Aut (dunion K L)) = Nat.card (Aut K) * Nat.card (Aut L) →
 691          classMass (w (B + B')) (Quotient.mk (relabelSetoid (B + B')) (dunion K L))
 692            = classMass (w B) (Quotient.mk (relabelSetoid B) K)
 693              * classMass (w B') (Quotient.mk (relabelSetoid B') L))
 694
 695theorem properEscape_satisfiesTheOtherHypotheses {lam : ℝ} (hlam : 0 < lam) :
 696    SatisfiesTheOtherHypotheses (statWeight properStat lam) :=
 697  ⟨fun _ _ _ h => statWeight_invariant properStat lam h,
 698    fun B K => statWeight_pos properStat hlam B K,
 699    fun B => statWeight_emptyComplex properStat lam B,
 700    properEscape_normalizedAtTheAtoms lam,
 701    fun _ _ K L haut => statWeight_glues properStat lam K L haut⟩
 702
 703/-- **Control for the class-mass comparison.**  At `lam = 1` the very same formula returns the
 704RS measure exactly, for every complex.  So the inequality below measures the tilt and not a
 705mismatch of conventions between `classMass` and `mu`. -/
 706theorem classMass_statWeight_at_one (φ : AdditiveStat) (K : BoundedComplex B) :
 707    classMass (statWeight φ 1 B) (Quotient.mk (relabelSetoid B) K) = mu K := by
 708  rw [classMass_statWeight]
 709  simp [mu]
 710
 711/-- **THEOREM (the derivation's conclusion fails for the escape).**  The class mass of the
 712proper-edge escape at the two-bridge class is `lam²/|Aut|`, and the RS measure is `1/|Aut|`, so
 713they differ.  This is what makes the reach bound bite: not merely that the escape misses a
 714premise, but that the thing the derivation concludes is false of it. -/
 715theorem properEscape_classMass_ne_mu {lam : ℝ} (hlam : 0 < lam) (hne : lam ≠ 1) :
 716    classMass (statWeight properStat lam 2) (Quotient.mk (relabelSetoid 2) twoBridges)
 717      ≠ mu twoBridges := by
 718  rw [classMass_statWeight]
 719  unfold mu
 720  intro h
 721  have hA : (0 : ℝ) < (Nat.card (Aut twoBridges) : ℝ) := by
 722    exact_mod_cast autCard_pos twoBridges
 723  rw [div_eq_div_iff hA.ne' hA.ne'] at h
 724  have hkey : lam ^ (properStat.stat 2 twoBridges) = 1 := mul_right_cancel₀ hA.ne' h
 725  have hs : properStat.stat 2 twoBridges = 2 := properEdgeCount_twoBridges
 726  rw [hs] at hkey
 727  exact sq_ne_one_of_pos_ne_one hlam hne hkey
 728
 729/-- **THE REACH BOUND.**  For each positive `lam ≠ 1` there is one fixed labeled weight that
 730satisfies *every* hypothesis the derivation places on the weight except premise (i), is not
 731size-blind, and whose class mass is not the RS measure.  So premise (i) is not redundant: it is
 732load-bearing for the conclusion.
 733
 734The bundle it satisfies is already stronger than the derivation's, since its gluing clause
 735quantifies over every eligible pair rather than the four families `CarrierShuffle` names.  That is
 736the precise sense in which the other hypotheses cannot be blamed for premise (i); it is not a claim
 737about arbitrary strengthenings, some of which would obviously exclude this escape.
 738
 739**Scope, and what this does not say.**  It does not say premise (ii) is empty; the sharper
 740statement of that is `gluing_alone_does_not_force_mu` in the derivation module, which exhibits a
 741weight satisfying gluing at *every* pair whose class mass is not `mu`.  It says premise (ii),
 742even conjoined with positivity, both normalizations and invariance, does not generate the
 743automorphism denominator that premise (i) alone already produces
 744(`classMass_sizeWeight_eq_fugacity_div_autCard`).  It does not characterize eligibility; no such
 745characterization exists in the library.
 746
 747**It does not quantify over derivations.**  The statement is existential: one weight, satisfying
 748that bundle, not size-blind.  A reader may reasonably expect the stronger reading, that every
 749route to premise (i) must import a reason why incidence statistics do not appear, and that reading
 750is *not* proved here and is not provable from an existential.  What supports it, and only as
 751motivation, is that the escape mechanism runs for every additive incidence statistic
 752(`statWeight_glues`, `statWeight_pos`, `statWeight_invariant`) while the normalizations exclude
 753only the statistics that fail to vanish at the atoms (`loopEscape_fails_the_atoms`,
 754`properEdgeCount_eq_zero_of_nV_le_one`).  So the family of escapes is large, which is a fact about
 755the family and not a theorem about derivations. -/
 756theorem size_blindness_not_forced_by_the_other_hypotheses {lam : ℝ} (hlam : 0 < lam)
 757    (hne : lam ≠ 1) :
 758    SatisfiesTheOtherHypotheses (statWeight properStat lam)
 759      ∧ ¬ SizeBlind (statWeight properStat lam)
 760      ∧ classMass (statWeight properStat lam 2) (Quotient.mk (relabelSetoid 2) twoBridges)
 761          ≠ mu twoBridges :=
 762  ⟨properEscape_satisfiesTheOtherHypotheses hlam, properEscape_not_sizeBlind hlam hne,
 763    properEscape_classMass_ne_mu hlam hne⟩
 764
 765/-! ## §4. Blindness to the posting alphabet, stated about the posting alphabet
 766
 767`GaugeHistoryMeasure.PostingAlphabet K = Fin K.nV ⊕ Fin K.nE ⊕ Fin K.nT`, with the three
 768canonical injections `vertexPost`, `edgePost`, `tetPost`.  An equivalence of alphabets is
 769sort-respecting when it carries each kind of letter to the same kind. -/
 770
 771/-- An equivalence of posting alphabets **respects the cell kinds** when it carries vertex
 772letters to vertex letters, edge letters to edge letters, and tetrahedron letters to
 773tetrahedron letters.
 774
 775The condition is one-sided: it constrains the forward map and says nothing about the inverse.
 776That is deliberate and costs nothing, because the totals are already pinned by the equivalence.
 777Each kind injects into its partner, so each count is at most its partner's, and the three counts
 778sum to the same total; `exists_respectsKinds_iff_sizes` turns that into equality on all three.  A
 779two-sided definition would give the same theorem with more hypotheses to discharge. -/
 780def RespectsKinds {K : BoundedComplex B} {L : BoundedComplex B'}
 781    (e : GaugeHistoryMeasure.PostingAlphabet K ≃ GaugeHistoryMeasure.PostingAlphabet L) :
 782    Prop :=
 783  (∀ v : Fin K.nV, ∃ v' : Fin L.nV, e (Sum.inl v) = Sum.inl v')
 784    ∧ (∀ x : Fin K.nE, ∃ x' : Fin L.nE, e (Sum.inr (Sum.inl x)) = Sum.inr (Sum.inl x'))
 785    ∧ (∀ t : Fin K.nT, ∃ t' : Fin L.nT, e (Sum.inr (Sum.inr t)) = Sum.inr (Sum.inr t'))
 786
 787/-- A bare correspondence of posting alphabets exists exactly when the total cell counts
 788agree. -/
 789theorem postingAlphabet_equiv_iff_total (K : BoundedComplex B) (L : BoundedComplex B') :
 790    Nonempty (GaugeHistoryMeasure.PostingAlphabet K ≃ GaugeHistoryMeasure.PostingAlphabet L)
 791      ↔ K.nV + K.nE + K.nT = L.nV + L.nE + L.nT := by
 792  have hK : Fintype.card (GaugeHistoryMeasure.PostingAlphabet K) = K.nV + K.nE + K.nT := by
 793    simp [GaugeHistoryMeasure.PostingAlphabet, Nat.add_assoc]
 794  have hL : Fintype.card (GaugeHistoryMeasure.PostingAlphabet L) = L.nV + L.nE + L.nT := by
 795    simp [GaugeHistoryMeasure.PostingAlphabet, Nat.add_assoc]
 796  constructor
 797  · intro ⟨e⟩
 798    have hc := Fintype.card_congr e
 799    rw [hK, hL] at hc
 800    exact hc
 801  · intro h
 802    exact ⟨Fintype.equivOfCardEq (by rw [hK, hL, h])⟩
 803
 804/-- A sort-respecting correspondence sends each kind into the same kind injectively, so each
 805count is bounded by its partner. -/
 806theorem sizes_le_of_respectsKinds {K : BoundedComplex B} {L : BoundedComplex B'}
 807    {e : GaugeHistoryMeasure.PostingAlphabet K ≃ GaugeHistoryMeasure.PostingAlphabet L}
 808    (h : RespectsKinds e) : K.nV ≤ L.nV ∧ K.nE ≤ L.nE ∧ K.nT ≤ L.nT := by
 809  classical
 810  obtain ⟨hv, he, ht⟩ := h
 811  refine ⟨?_, ?_, ?_⟩
 812  · have hinj : Function.Injective (fun v : Fin K.nV => (hv v).choose) := by
 813      intro a b hab
 814      have hkey : e (Sum.inl a) = e (Sum.inl b) := by
 815        rw [(hv a).choose_spec, (hv b).choose_spec]
 816        exact congrArg Sum.inl hab
 817      exact Sum.inl_injective (e.injective hkey)
 818    simpa using Fintype.card_le_of_injective _ hinj
 819  · have hinj : Function.Injective (fun x : Fin K.nE => (he x).choose) := by
 820      intro a b hab
 821      have hkey : e (Sum.inr (Sum.inl a)) = e (Sum.inr (Sum.inl b)) := by
 822        rw [(he a).choose_spec, (he b).choose_spec]
 823        exact congrArg (fun y => Sum.inr (Sum.inl y)) hab
 824      exact Sum.inl_injective (Sum.inr_injective (e.injective hkey))
 825    simpa using Fintype.card_le_of_injective _ hinj
 826  · have hinj : Function.Injective (fun t : Fin K.nT => (ht t).choose) := by
 827      intro a b hab
 828      have hkey : e (Sum.inr (Sum.inr a)) = e (Sum.inr (Sum.inr b)) := by
 829        rw [(ht a).choose_spec, (ht b).choose_spec]
 830        exact congrArg (fun y => Sum.inr (Sum.inr y)) hab
 831      exact Sum.inr_injective (Sum.inr_injective (e.injective hkey))
 832    simpa using Fintype.card_le_of_injective _ hinj
 833
 834/-- **THEOREM.**  A sort-respecting correspondence of posting alphabets exists exactly when
 835the three cell counts agree.  Each count is bounded by its partner because the letters of
 836each kind inject, and the totals agree because the whole alphabet is in bijection; the two
 837together force equality. -/
 838theorem exists_respectsKinds_iff_sizes (K : BoundedComplex B) (L : BoundedComplex B') :
 839    (∃ e : GaugeHistoryMeasure.PostingAlphabet K ≃ GaugeHistoryMeasure.PostingAlphabet L,
 840        RespectsKinds e)
 841      ↔ (K.nV = L.nV ∧ K.nE = L.nE ∧ K.nT = L.nT) := by
 842  constructor
 843  · intro ⟨e, h⟩
 844    obtain ⟨h1, h2, h3⟩ := sizes_le_of_respectsKinds h
 845    have htot := (postingAlphabet_equiv_iff_total K L).mp ⟨e⟩
 846    exact ⟨by omega, by omega, by omega⟩
 847  · intro ⟨hv, he, ht⟩
 848    refine ⟨Equiv.sumCongr (finCongr hv) (Equiv.sumCongr (finCongr he) (finCongr ht)), ?_, ?_, ?_⟩
 849    · intro v; exact ⟨finCongr hv v, rfl⟩
 850    · intro x; exact ⟨finCongr he x, rfl⟩
 851    · intro t; exact ⟨finCongr ht t, rfl⟩
 852
 853/-- **Blind to everything but the posting alphabet read with its sorting into cell kinds.**
 854Stated against `GaugeHistoryMeasure.PostingAlphabet` itself. -/
 855def AlphabetBlindSorted (w : ∀ B : ℕ, BoundedComplex B → ℝ) : Prop :=
 856  ∀ (B B' : ℕ) (K : BoundedComplex B) (L : BoundedComplex B'),
 857    (∃ e : GaugeHistoryMeasure.PostingAlphabet K ≃ GaugeHistoryMeasure.PostingAlphabet L,
 858        RespectsKinds e) → w B K = w B' L
 859
 860theorem alphabetBlindSorted_iff_sizeBlind (w : ∀ B : ℕ, BoundedComplex B → ℝ) :
 861    AlphabetBlindSorted w ↔ SizeBlind w := by
 862  constructor
 863  · intro h B B' K L hv he ht
 864    exact h B B' K L ((exists_respectsKinds_iff_sizes K L).mpr ⟨hv, he, ht⟩)
 865  · intro h B B' K L hEq
 866    obtain ⟨hv, he, ht⟩ := (exists_respectsKinds_iff_sizes K L).mp hEq
 867    exact h B B' K L hv he ht
 868
 869/-- The escape fails alphabet-blindness too, as it must. -/
 870theorem loopEscape_not_alphabetBlindSorted {lam : ℝ} (hlam : 0 < lam) (hne : lam ≠ 1) :
 871    ¬ AlphabetBlindSorted (statWeight loopStat lam) := by
 872  rw [alphabetBlindSorted_iff_sizeBlind]
 873  exact loopEscape_not_sizeBlind hlam hne
 874
 875/-! ## §5. Against premise (i) exactly as the derivation states it
 876
 877`Gap2GluingDerivation` states premise (i) not as a relation but as a constructor: the weight
 878*is* `sizeWeight f` for some `f` of three naturals.  Closing the equivalence needs a complex
 879at each realizable size triple, and needs the fact that the unrealizable triples are exactly
 880those with no vertex and some incidence, which `vertex_of_incidence` supplies. -/
 881
 882/-- A canonical complex at each realizable size triple with at least one vertex: `a`
 883vertices, `b` loops at the first vertex, `c` tetrahedra degenerate at the first vertex. -/
 884def blob (a b c : ℕ) (h : 0 < a) : BoundedComplex (a + b + c) where
 885  nV := a
 886  nE := b
 887  nT := c
 888  hV := by omega
 889  hE := by omega
 890  hT := by omega
 891  edgeVerts := fun _ => (⟨0, h⟩, ⟨0, h⟩)
 892  tetVerts := fun _ _ => ⟨0, h⟩
 893
 894/-- The size function read off a size-blind weight family.  Its value on the triples no
 895complex realizes, which are exactly those with no vertex and some incidence, is arbitrary
 896and never evaluated. -/
 897noncomputable def canonicalSizeFun (w : ∀ B : ℕ, BoundedComplex B → ℝ) (a b c : ℕ) : ℝ :=
 898  if h : 0 < a then w (a + b + c) (blob a b c h) else w 0 (emptyComplex 0)
 899
 900theorem sizeBlind_eq_sizeWeight {w : ∀ B : ℕ, BoundedComplex B → ℝ} (hw : SizeBlind w)
 901    (B : ℕ) (K : BoundedComplex B) : w B K = sizeWeight (canonicalSizeFun w) K := by
 902  unfold sizeWeight canonicalSizeFun
 903  by_cases h : 0 < K.nV
 904  · rw [dif_pos h]
 905    exact hw B _ K (blob K.nV K.nE K.nT h) rfl rfl rfl
 906  · rw [dif_neg h]
 907    have hv : K.nV = 0 := by omega
 908    have hi : K.nE + K.nT = 0 := by
 909      by_contra hc
 910      have h1 : 1 ≤ K.nE + K.nT := by omega
 911      have := vertex_of_incidence K h1
 912      omega
 913    have hE : K.nE = 0 := by omega
 914    have hT : K.nT = 0 := by omega
 915    exact hw B 0 K (emptyComplex 0) (by simp [emptyComplex, hv])
 916      (by simp [emptyComplex, hE]) (by simp [emptyComplex, hT])
 917
 918/-- Size-blindness as a relation and as a constructor are the same condition. -/
 919theorem sizeBlind_iff_exists_sizeFun (w : ∀ B : ℕ, BoundedComplex B → ℝ) :
 920    SizeBlind w
 921      ↔ ∃ f : ℕ → ℕ → ℕ → ℝ, ∀ (B : ℕ) (K : BoundedComplex B), w B K = sizeWeight f K := by
 922  constructor
 923  · intro hw
 924    exact ⟨canonicalSizeFun w, sizeBlind_eq_sizeWeight hw⟩
 925  · intro ⟨f, hf⟩ B B' K L hv he ht
 926    rw [hf B K, hf B' L]
 927    exact sizeWeight_sizeBlind f B B' K L hv he ht
 928
 929/-- **THEOREM.**  Premise (i) of `Gap2GluingDerivation`, that the labeled weight is
 930`sizeWeight f` for some size function `f`, holds exactly when the weight is blind to
 931everything but the substrate's posting alphabet read with its sorting into cell kinds.
 932
 933**This is an equivalence, not a derivation.**  §6 proves the posting alphabet is itself a
 934function of the three counts, so the right-hand side is the left-hand side in other words.
 935The name says `iff` and means it. -/
 936theorem premise_one_iff_alphabetBlind (w : ∀ B : ℕ, BoundedComplex B → ℝ) :
 937    (∃ f : ℕ → ℕ → ℕ → ℝ, ∀ (B : ℕ) (K : BoundedComplex B), w B K = sizeWeight f K)
 938      ↔ AlphabetBlindSorted w :=
 939  (sizeBlind_iff_exists_sizeFun w).symm.trans (alphabetBlindSorted_iff_sizeBlind w).symm
 940
 941/-! ## §6. The dichotomy: sufficient for premise (i) exactly when not weaker than it
 942
 943§4 and §5 make precise the hope that premise (i) is simply what the posting alphabet says,
 944so that the premise moves off the measure and onto the substrate.  This section kills that
 945hope, and then generalizes the reason into a no-go covering every premise of that shape.
 946
 947An **invariant** of complexes is any function of a complex, valued in any type.  A weight is
 948**blind to** an invariant when it agrees on any two complexes the invariant does not
 949separate.  Premise (i) is itself of this form: it is blindness to the size triple.  The
 950question is whether premise (i) follows from blindness to something *weaker*, and the answer
 951is no, for one of two reasons depending on which side of the dichotomy the invariant falls. -/
 952
 953/-- A readout of a complex, valued in an arbitrary type.
 954
 955**The name overstates the definition, deliberately.**  Nothing here requires relabeling invariance:
 956this is *any* function of a labeled complex, label-sensitive ones included.  The word is kept
 957because these are the objects a substrate would be said to resolve, and the looseness is what makes
 958the dichotomy exhaustive rather than restricted to well-behaved readouts.  Where invariance is
 959needed it is a hypothesis or a conclusion, never packed into the type: see
 960`sizeStatInvariant_invariant` for an instance that has it and the last clause of
 961`fine_invariant_blindness_does_not_imply_sizeBlind` for how the horn handles the case where it is
 962absent. -/
 963def Invariant (α : Type) : Type := ∀ B : ℕ, BoundedComplex B → α
 964
 965/-- An invariant **resolves no more than the sizes** when any two complexes with the same
 966three cell counts receive the same value. -/
 967def ResolvesNoMoreThanSizes {α : Type} (I : Invariant α) : Prop :=
 968  ∀ (B B' : ℕ) (K : BoundedComplex B) (L : BoundedComplex B'),
 969    K.nV = L.nV → K.nE = L.nE → K.nT = L.nT → I B K = I B' L
 970
 971/-- A weight is **blind to** an invariant when the invariant's value decides it. -/
 972def BlindTo {α : Type} (I : Invariant α) (w : ∀ B : ℕ, BoundedComplex B → ℝ) : Prop :=
 973  ∀ (B B' : ℕ) (K : BoundedComplex B) (L : BoundedComplex B'),
 974    I B K = I B' L → w B K = w B' L
 975
 976/-- **Coarse horn.**  If an invariant resolves no more than the three cell counts, blindness
 977to it *implies* premise (i).  So assuming it is assuming premise (i) or more, and a
 978derivation of premise (i) from it is a restatement rather than a discharge. -/
 979theorem coarse_invariant_blindness_implies_sizeBlind {α : Type} (I : Invariant α)
 980    (hI : ResolvesNoMoreThanSizes I) (w : ∀ B : ℕ, BoundedComplex B → ℝ)
 981    (hw : BlindTo I w) : SizeBlind w := by
 982  intro B B' K L hv he ht
 983  exact hw B B' K L (hI B B' K L hv he ht)
 984
 985/-- **Fine horn.**  If an invariant separates even one pair of complexes with the same three cell
 986counts, blindness to it does *not* imply premise (i).  The witness is the two-valued indicator of
 987one invariant value: strictly positive always, and relabeling-invariant whenever the invariant is,
 988which the last clause states as an implication rather than a hypothesis so that the horn applies to
 989**every** invariant, label-sensitive ones included.  That is what makes the dichotomy exhaustive.
 990
 991The witness is not unit on the empty complex and says nothing about gluing;
 992`fine_horn_survives_the_other_hypotheses` supplies a witness that satisfies those too, at one
 993concrete invariant. -/
 994theorem fine_invariant_blindness_does_not_imply_sizeBlind {α : Type} (I : Invariant α)
 995    {B₀ B₀' : ℕ} (K₀ : BoundedComplex B₀) (L₀ : BoundedComplex B₀')
 996    (hv : K₀.nV = L₀.nV) (he : K₀.nE = L₀.nE) (ht : K₀.nT = L₀.nT)
 997    (hsep : I B₀ K₀ ≠ I B₀' L₀) :
 998    ∃ w : ∀ B : ℕ, BoundedComplex B → ℝ,
 999      BlindTo I w
1000        ∧ (∀ (B : ℕ) (K : BoundedComplex B), 0 < w B K)
1001        ∧ ¬ SizeBlind w
1002        ∧ ((∀ (B : ℕ) (K K' : BoundedComplex B), Equivalent K K' → I B K = I B K') →
1003            ∀ (B : ℕ) (K K' : BoundedComplex B), Equivalent K K' → w B K = w B K') := by
1004  classical
1005  refine ⟨fun B K => if I B K = I B₀ K₀ then 1 else 2, ?_, ?_, ?_, ?_⟩
1006  · intro B B' K L h
1007    simp only [h]
1008  · intro B K
1009    show (0 : ℝ) < if I B K = I B₀ K₀ then (1 : ℝ) else 2
1010    by_cases hc : I B K = I B₀ K₀
1011    · rw [if_pos hc]; norm_num
1012    · rw [if_neg hc]; norm_num
1013  · intro hsb
1014    have hbad : (if I B₀ K₀ = I B₀ K₀ then (1 : ℝ) else 2)
1015        = (if I B₀' L₀ = I B₀ K₀ then (1 : ℝ) else 2) := hsb B₀ B₀' K₀ L₀ hv he ht
1016    rw [if_pos (rfl : I B₀ K₀ = I B₀ K₀), if_neg (Ne.symm hsep)] at hbad
1017    norm_num at hbad
1018  · intro hIinv B K K' hEq
1019    simp only [hIinv B K K' hEq]
1020
1021/-- **The two horns are exhaustive.**  By cases on whether the invariant is constant across
1022same-size pairs.
1023
1024**This theorem has no content of its own.**  It is `P ∨ ¬P` with `¬P` unpacked into the witness it
1025asserts, so it excludes nothing and would hold for any predicate whatever.  It is stated because the
1026unpacking is what the horn theorems consume, and because a dichotomy claim should have its
1027exhaustiveness written down rather than assumed.  All the content is in the two horns and in
1028`blindness_forces_premise_one_iff_coarse`, which combines them.  Neither this theorem nor either
1029horn assumes the invariant is relabeling-invariant, so the coverage has no gap at label-sensitive
1030invariants. -/
1031theorem invariant_coarse_or_fine {α : Type} (I : Invariant α) :
1032    ResolvesNoMoreThanSizes I
1033      ∨ ∃ (B₀ B₀' : ℕ) (K₀ : BoundedComplex B₀) (L₀ : BoundedComplex B₀'),
1034          K₀.nV = L₀.nV ∧ K₀.nE = L₀.nE ∧ K₀.nT = L₀.nT ∧ I B₀ K₀ ≠ I B₀' L₀ := by
1035  classical
1036  by_cases h : ResolvesNoMoreThanSizes I
1037  · exact Or.inl h
1038  · right
1039    unfold ResolvesNoMoreThanSizes at h
1040    push_neg at h
1041    obtain ⟨B, B', K, L, hv, he, ht, hne⟩ := h
1042    exact ⟨B, B', K, L, hv, he, ht, hne⟩
1043
1044/-- **THE DICHOTOMY, as one equivalence.**  Blindness to an invariant forces premise (i) **exactly
1045when** that invariant never separates two complexes with the same three counts.  The two horns are
1046the two directions, and this is the statement to cite: it is sharper than their conjunction, because
1047an equivalence cannot be read as leaving a third case open.
1048
1049**What it rules out, stated as the contrapositive it is.**  Take any premise of the form *the weight
1050cannot separate complexes that agree on `X`* and ask it to yield premise (i) for every weight. Then
1051`X` resolves no more than the counts, and blindness to `X` is then sufficient for premise (i)
1052(`coarse_invariant_blindness_implies_sizeBlind`). So no premise of this shape is both strictly weaker
1053than premise (i) and sufficient for it. That is what kills the hope this module started from.
1054
1055**It does not say the two conditions are interchangeable, and they are not.**  Sufficiency runs one
1056way only. A coarse invariant can be so coarse that blindness to it is *strictly stronger* than
1057premise (i), which is exactly what `unsorted_is_strictly_stronger` exhibits: the total cell count
1058resolves no more than the counts, yet a size-blind weight can fail blindness to it, and the Gibbs
1059weight does. So "blindness to `X` and premise (i) imply each other" is false in general, and an
1060earlier version of this docstring asserted it.
1061
1062**Two things this does not say, both of which the word "circular" would wrongly suggest.**  It does
1063not say a coarse premise is premise (i) *renamed*: the coarse class contains conditions strictly
1064stronger than premise (i), and `unsorted_is_strictly_stronger` exhibits one, blindness to the total
1065cell count, which is outright inconsistent with the derivation's conclusion because the Gibbs weight
1066itself fails it. What is equivalent to
1067premise (i) is not the invariant but blindness to it, and only quantified over all weights. And it
1068does not quantify over derivations: a conjunction of several blindness premises, or a premise of
1069some other shape, is outside the statement, so premise (i) is not shown unprovable.
1070
1071The escape's statistic witnesses the fine side (`fine_horn_survives_the_other_hypotheses`), the
1072posting alphabet the coarse side (`postingAlphabet_is_determined_by_the_sizes`), and the total cell
1073count the coarse side strictly (`unsorted_is_strictly_stronger`). -/
1074theorem blindness_forces_premise_one_iff_coarse {α : Type} (I : Invariant α) :
1075    (∀ w : ∀ B : ℕ, BoundedComplex B → ℝ, BlindTo I w → SizeBlind w)
1076      ↔ ResolvesNoMoreThanSizes I := by
1077  classical
1078  refine ⟨fun h => ?_, fun hI w hw => coarse_invariant_blindness_implies_sizeBlind I hI w hw⟩
1079  rcases invariant_coarse_or_fine I with hI | ⟨B₀, B₀', K₀, L₀, hv, he, ht, hsep⟩
1080  · exact hI
1081  · obtain ⟨w, hblind, -, hnsb, -⟩ :=
1082      fine_invariant_blindness_does_not_imply_sizeBlind I K₀ L₀ hv he ht hsep
1083    exact absurd (h w hblind) hnsb
1084
1085/-- The dichotomy in horn form, as the two implications, for readers who want the witness the fine
1086side produces rather than only the equivalence.  Both sides quantify over the invariant's type, so
1087this is one statement covering every invariant of complexes. -/
1088theorem indistinguishability_premises_never_weaken_premise_one :
1089    (∀ (α : Type) (I : Invariant α), ResolvesNoMoreThanSizes I →
1090        ∀ w : ∀ B : ℕ, BoundedComplex B → ℝ, BlindTo I w → SizeBlind w)
1091      ∧ (∀ (α : Type) (I : Invariant α) (B₀ B₀' : ℕ) (K₀ : BoundedComplex B₀)
1092            (L₀ : BoundedComplex B₀'),
1093            K₀.nV = L₀.nV → K₀.nE = L₀.nE → K₀.nT = L₀.nT → I B₀ K₀ ≠ I B₀' L₀ →
1094              ∃ w : ∀ B : ℕ, BoundedComplex B → ℝ,
1095                BlindTo I w
1096                  ∧ (∀ (B : ℕ) (K : BoundedComplex B), 0 < w B K)
1097                  ∧ ¬ SizeBlind w
1098                  ∧ ((∀ (B : ℕ) (K K' : BoundedComplex B), Equivalent K K' → I B K = I B K') →
1099                      ∀ (B : ℕ) (K K' : BoundedComplex B), Equivalent K K' → w B K = w B K')) :=
1100  ⟨fun _ I hI w hw => coarse_invariant_blindness_implies_sizeBlind I hI w hw,
1101    fun _ I _ _ K₀ L₀ hv he ht hsep =>
1102      fine_invariant_blindness_does_not_imply_sizeBlind I K₀ L₀ hv he ht hsep⟩
1103
1104/-! ### The fine horn is not an artifact of a degenerate witness
1105
1106The abstract fine horn is witnessed by a two-valued indicator, which is positive and (when the
1107invariant is) relabeling-invariant, but is not unit on the empty complex and is silent about
1108gluing.  So a reader can still ask whether adding the derivation's remaining hypotheses rescues
1109the implication.  At one invariant it does not, and the escape of §3 is the witness: it is blind
1110to the invariant that reads the three counts together with the proper-edge count, an invariant
1111that separates a same-size pair, and it satisfies all five remaining hypotheses. -/
1112
1113/-- The invariant that reads the three cell counts **and** the value of an additive statistic.
1114At `properStat` it separates the two witnesses of §3, so it is not on the coarse horn. -/
1115def sizeStatInvariant (φ : AdditiveStat) : Invariant (ℕ × ℕ × ℕ × ℕ) :=
1116  fun B K => (K.nV, K.nE, K.nT, φ.stat B K)
1117
1118theorem sizeStatInvariant_invariant (φ : AdditiveStat) (B : ℕ) (K K' : BoundedComplex B)
1119    (h : Equivalent K K') : sizeStatInvariant φ B K = sizeStatInvariant φ B K' := by
1120  obtain ⟨r⟩ := h
1121  unfold sizeStatInvariant
1122  rw [size_v r, size_e r, size_t r, φ.invariant B K K' ⟨r⟩]
1123
1124theorem sizeStatInvariant_separates_witnesses :
1125    sizeStatInvariant properStat 2 twoBridges ≠ sizeStatInvariant properStat 2 twoLoops := by
1126  intro h
1127  have h4 : properEdgeCount twoBridges = properEdgeCount twoLoops :=
1128    congrArg (fun p : ℕ × ℕ × ℕ × ℕ => p.2.2.2) h
1129  rw [properEdgeCount_twoBridges, properEdgeCount_twoLoops] at h4
1130  exact absurd h4 (by decide)
1131
1132/-- An escape weight is a function of the three counts together with its own statistic, so it is
1133blind to that pairing. -/
1134theorem statWeight_blindTo_sizeStat (φ : AdditiveStat) (lam : ℝ) :
1135    BlindTo (sizeStatInvariant φ) (statWeight φ lam) := by
1136  intro B B' K L h
1137  have hv : K.nV = L.nV := congrArg (fun p : ℕ × ℕ × ℕ × ℕ => p.1) h
1138  have he : K.nE = L.nE := congrArg (fun p : ℕ × ℕ × ℕ × ℕ => p.2.1) h
1139  have ht : K.nT = L.nT := congrArg (fun p : ℕ × ℕ × ℕ × ℕ => p.2.2.1) h
1140  have hs : φ.stat B K = φ.stat B' L := congrArg (fun p : ℕ × ℕ × ℕ × ℕ => p.2.2.2) h
1141  unfold statWeight
1142  rw [hs]
1143  unfold gibbsWeight
1144  rw [hv, he, ht]
1145
1146/-- **ONE FINE INVARIANT SURVIVES EVERY OTHER HYPOTHESIS.**  There is a relabeling-invariant
1147invariant that separates a same-size pair, hence is on the fine side, and a weight blind to it that
1148satisfies all five hypotheses the derivation places on the weight except premise (i), is not
1149size-blind, and whose class mass is not the RS measure.
1150
1151**One invariant, and the name says so.**  This does *not* say the fine side in general survives the
1152other hypotheses.  The general fine horn
1153(`fine_invariant_blindness_does_not_imply_sizeBlind`) covers every invariant that separates a
1154same-size pair, but its witness carries only positivity and invariance, not the normalizations or
1155gluing.  What is settled here is: blindness to *this* fine invariant does not force premise (i) even
1156alongside every other hypothesis.  What is **not** settled, and is the open residual this module
1157leaves, is whether some *other* fine invariant might, conjoined with those hypotheses, force
1158premise (i); the conjunction is restrictive and the question is a real one.
1159
1160**And the pair is matched by construction.**  The invariant reads the three counts together with the
1161statistic the weight is built from, so blindness is immediate rather than earned; the work is in the
1162weight satisfying the five hypotheses, not in the blindness clause.  A countermodel is allowed to be
1163constructed this way, and nothing here claims the invariant is one a substrate would supply. The
1164reason it is worth stating at all is that the five hypotheses are a genuine constraint: they already
1165exclude the loop-count version of exactly this construction
1166(`loopEscape_fails_the_atoms`). -/
1167theorem fine_horn_survives_the_other_hypotheses {lam : ℝ} (hlam : 0 < lam) (hne : lam ≠ 1) :
1168    (twoBridges.nV = twoLoops.nV ∧ twoBridges.nE = twoLoops.nE ∧ twoBridges.nT = twoLoops.nT)
1169      ∧ sizeStatInvariant properStat 2 twoBridges ≠ sizeStatInvariant properStat 2 twoLoops
1170      ∧ (∀ (B : ℕ) (K K' : BoundedComplex B), Equivalent K K' →
1171          sizeStatInvariant properStat B K = sizeStatInvariant properStat B K')
1172      ∧ BlindTo (sizeStatInvariant properStat) (statWeight properStat lam)
1173      ∧ SatisfiesTheOtherHypotheses (statWeight properStat lam)
1174      ∧ ¬ SizeBlind (statWeight properStat lam)
1175      ∧ classMass (statWeight properStat lam 2) (Quotient.mk (relabelSetoid 2) twoBridges)
1176          ≠ mu twoBridges :=
1177  ⟨⟨rfl, rfl, rfl⟩, sizeStatInvariant_separates_witnesses,
1178    sizeStatInvariant_invariant properStat, statWeight_blindTo_sizeStat properStat lam,
1179    properEscape_satisfiesTheOtherHypotheses hlam, properEscape_not_sizeBlind hlam hne,
1180    properEscape_classMass_ne_mu hlam hne⟩
1181
1182/-- **Why the posting alphabet lands on the coarse horn.**  The posting alphabet is a
1183*function of* the three cell counts: any two complexes with the same counts have
1184sort-respecting equivalent posting alphabets, no matter how their cells are wired.  In
1185particular the two witnesses of §3, which differ only in incidence, have equivalent
1186alphabets.
1187
1188So the alphabet carries no information about incidence to begin with, and asking a weight to
1189be blind to everything but the alphabet is asking for premise (i) under another name.  The
1190equivalence `premise_one_iff_alphabetBlind` is a reformulation, not a derivation.
1191
1192**Scope.**  This is a statement about the posting *alphabet*, which is the only part of the
1193posting layer it touches.  That the wider posted-history layer adds no selecting information
1194is a separate and earlier result, recorded in the `PathSumMeasure` module header; this
1195theorem neither reproves nor needs it. -/
1196theorem postingAlphabet_is_determined_by_the_sizes :
1197    (∀ (B B' : ℕ) (K : BoundedComplex B) (L : BoundedComplex B'),
1198        K.nV = L.nV → K.nE = L.nE → K.nT = L.nT →
1199          ∃ e : GaugeHistoryMeasure.PostingAlphabet K ≃ GaugeHistoryMeasure.PostingAlphabet L,
1200            RespectsKinds e)
1201      ∧ (∃ e : GaugeHistoryMeasure.PostingAlphabet twoLoops
1202              ≃ GaugeHistoryMeasure.PostingAlphabet twoBridges,
1203          RespectsKinds e)
1204      ∧ loopCount twoLoops ≠ loopCount twoBridges := by
1205  refine ⟨fun _ _ K L hv he ht => (exists_respectsKinds_iff_sizes K L).mpr ⟨hv, he, ht⟩,
1206    (exists_respectsKinds_iff_sizes twoLoops twoBridges).mpr ⟨rfl, rfl, rfl⟩, ?_⟩
1207  rw [loopCount_twoLoops, loopCount_twoBridges]
1208  decide
1209
1210/-! ### The one place the readings differ
1211
1212Forgetting the sorting gives a strictly *stronger* condition, not a weaker one: a bare
1213correspondence of alphabets only forces the total cell count to agree, so unsorted blindness
1214forces the weight to depend on `nV + nE + nT` alone.  This shows the family of readings is
1215non-trivial.  It does not make any of them a derivation. -/
1216
1217/-- **Blind to everything but the posting alphabet as a bare set.** -/
1218def AlphabetBlindUnsorted (w : ∀ B : ℕ, BoundedComplex B → ℝ) : Prop :=
1219  ∀ (B B' : ℕ) (K : BoundedComplex B) (L : BoundedComplex B'),
1220    Nonempty (GaugeHistoryMeasure.PostingAlphabet K ≃ GaugeHistoryMeasure.PostingAlphabet L) →
1221      w B K = w B' L
1222
1223/-- Three vertices and one edge: sizes `(3,1,0)`, total cell count `4`, the same total as
1224`twoBridges` at `(2,2,0)` and a different triple. -/
1225def threeVertsOneEdge : BoundedComplex 3 where
1226  nV := 3
1227  nE := 1
1228  nT := 0
1229  hV := le_refl 3
1230  hE := by norm_num
1231  hT := Nat.zero_le 3
1232  edgeVerts := fun _ => (0, 1)
1233  tetVerts := fun t => t.elim0
1234
1235/-- **THEOREM (the sorting is load-bearing, and the intended measure needs it).**  Three parts.
1236Unsorted blindness implies the sorted form.  A size-blind weight can fail the unsorted form, at
1237the pair `(2,2,0)` and `(3,1,0)` whose totals agree.  And the failing weight is not a contrived
1238one: the Gibbs weight itself, which is what the derivation concludes, fails unsorted blindness at
1239that same pair, `1/4` against `1/6`.
1240
1241**What the third part is for.**  It makes unsorted blindness and the derivation's conclusion jointly
1242unsatisfiable, so the coarse side of the dichotomy contains conditions strictly stronger than
1243premise (i) and not merely restatements of it.  Read as a conditional about substrates it would say:
1244*if* a substrate's posting alphabet were unsorted and *if* blindness to it were the right premise,
1245the two would contradict the conclusion.  Neither antecedent is proved anywhere; nothing here is a
1246theorem about what a substrate posts. -/
1247theorem unsorted_is_strictly_stronger :
1248    (∀ w : ∀ B : ℕ, BoundedComplex B → ℝ, AlphabetBlindUnsorted w → AlphabetBlindSorted w)
1249      ∧ (∃ w : ∀ B : ℕ, BoundedComplex B → ℝ, SizeBlind w ∧ ¬ AlphabetBlindUnsorted w)
1250      ∧ ¬ AlphabetBlindUnsorted (fun _ K => gibbsWeight K) := by
1251  have htot : twoBridges.nV + twoBridges.nE + twoBridges.nT
1252      = threeVertsOneEdge.nV + threeVertsOneEdge.nE + threeVertsOneEdge.nT := by
1253    norm_num [twoBridges, threeVertsOneEdge]
1254  refine ⟨?_, ?_, ?_⟩
1255  · intro w h B B' K L hEq
1256    obtain ⟨hv, he, ht⟩ := (exists_respectsKinds_iff_sizes K L).mp hEq
1257    exact h B B' K L ((postingAlphabet_equiv_iff_total K L).mpr (by rw [hv, he, ht]))
1258  · refine ⟨fun _ K => sizeWeight (fun a _ _ => (a : ℝ)) K, sizeWeight_sizeBlind _, ?_⟩
1259    intro h
1260    have hbad := h 2 3 twoBridges threeVertsOneEdge
1261      ((postingAlphabet_equiv_iff_total twoBridges threeVertsOneEdge).mpr htot)
1262    simp only [sizeWeight] at hbad
1263    norm_num [twoBridges, threeVertsOneEdge] at hbad
1264  · intro h
1265    have hbad := h 2 3 twoBridges threeVertsOneEdge
1266      ((postingAlphabet_equiv_iff_total twoBridges threeVertsOneEdge).mpr htot)
1267    unfold gibbsWeight at hbad
1268    norm_num [twoBridges, threeVertsOneEdge, Nat.factorial] at hbad
1269
1270/-! ## §7. Index
1271
1272The record below is a **navigation index**, not a certificate.  Its fields are assigned by
1273hand and its `rfl` projections prove nothing about the mathematics; the evidence is the named
1274theorems in each field's docstring. -/
1275
1276/-- What this module contains, as a hand-assigned index.  Read the named theorems, not these
1277Booleans. -/
1278structure ReachIndex where
1279  /-- `size_blindness_not_forced_by_the_other_hypotheses`: all five remaining hypotheses hold
1280  of a weight that is not size-blind and whose class mass is not the measure. -/
1281  reachBoundCompiled : Bool
1282  /-- `loopEscape_fails_the_atoms`: the three unit normalizations do exclude something, namely
1283  the loop-count escape.  The reach bound is stated against a statistic that survives them. -/
1284  normalizationsAreNotIdle : Bool
1285  /-- `statWeight_sizeBlind_at_one` and `classMass_statWeight_at_one`: at `lam = 1` every escape,
1286  the proper-edge one included, is size-blind and its class mass is exactly `mu`, so the witness
1287  separates for the right reason. -/
1288  positiveControlCompiled : Bool
1289  /-- `premise_one_iff_alphabetBlind`: premise (i) as written is equivalent to blindness to
1290  the sorted posting alphabet. -/
1291  alphabetEquivalenceCompiled : Bool
1292  /-- `postingAlphabet_is_determined_by_the_sizes`: the alphabet is a function of the size
1293  triple, so the equivalence above is a reformulation. -/
1294  postingAlphabetIsCoarse : Bool
1295  /-- `blindness_forces_premise_one_iff_coarse`: blindness to an invariant forces premise (i)
1296  exactly when the invariant is coarse, so no premise of that shape is both strictly weaker than
1297  premise (i) and sufficient for it. -/
1298  dichotomyCompiled : Bool
1299  /-- `fine_horn_survives_the_other_hypotheses`: the fine side holds against all five remaining
1300  hypotheses together, at one concrete invariant and not in general. -/
1301  fineHornSurvivesOtherHypotheses : Bool
1302  /-- `unsorted_is_strictly_stronger`: the sorting in the alphabet is load-bearing. -/
1303  sortingLoadBearing : Bool
1304  /-- Premise (i) is NOT derived. -/
1305  sizeBlindnessDerived : Bool
1306  /-- NOT proved: that the escape residue is exactly one constant per connected component
1307  class.  That needs connectedness of a complex, which exists nowhere in the library. -/
1308  connectedComponentLawProved : Bool
1309
1310/-- The state of play after this module. -/
1311def reachIndex : ReachIndex where
1312  reachBoundCompiled := true
1313  normalizationsAreNotIdle := true
1314  positiveControlCompiled := true
1315  alphabetEquivalenceCompiled := true
1316  postingAlphabetIsCoarse := true
1317  dichotomyCompiled := true
1318  fineHornSurvivesOtherHypotheses := true
1319  sortingLoadBearing := true
1320  sizeBlindnessDerived := false
1321  connectedComponentLawProved := false
1322
1323theorem index_not_derived : reachIndex.sizeBlindnessDerived = false := rfl
1324theorem index_no_component_law : reachIndex.connectedComponentLawProved = false := rfl
1325
1326end Gap2SizeBlindnessReach
1327end SevenGaps
1328end Gravity
1329end IndisputableMonolith
1330