IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2PostingLayerFloor
   2
   3/-!
   4# Gap 2: the non-equivariant posting case, resolved by a witness
   5
   6`Gap2PostingCostDerivation.equivariant_posts_mu_iff_numerator_one` closes the posting-cost route
   7for every *equivariant* letter cost: such a cost posts `mu` exactly when its Boltzmann numerator
   8`exp(-historyCost)` is identically one, so the cost layer contributes no factor to the measure.
   9Its docstring names one case it does not settle, and `Gap2PostingLayerFloor` §4 exhibits the class
  10that case lives in (`vertexIndexCost_not_equivariant`) without deciding it:
  11
  12> whether a **non**-equivariant cost can post `mu` with a numerator that is not identically one,
  13> by having the orbit sum of its Boltzmann factors come out to the orbit count while the
  14> individual terms differ.
  15
  16This module settles it, **in the witness direction**.  It can, and a one-parameter family does.
  17
  18## §1, the sharp condition, and it holds for every cost
  19
  20The first content is not the witness; it is the statement the witness is a witness *to*.  For an
  21arbitrary letter cost, with no equivariance hypothesis anywhere,
  22
  23* `classMass_postedWeight`: the class mass of a posted weight is the Gibbs weight times the total
  24  of the numerator over the class, because the divisor is a function of the three sizes and every
  25  labeled complex presenting the class has those sizes;
  26* `mu_eq_orbitCard_mul_gibbsWeight`: `mu` is the orbit count times that same Gibbs weight;
  27* `posts_mu_iff_numeratorMass_eq_orbitCard`: therefore posting `mu` is **exactly** the condition
  28  that the numerator's total over each gauge class equals that class's orbit count, i.e. that the
  29  numerator has **orbit mean one**.
  30
  31That is a strict weakening of "identically one", and naming it is what makes the open case
  32answerable rather than mysterious.  `orbitMeanOne_forces_one_of_invariant` then shows where
  33equivariance was doing its work: an equivariant cost has a numerator that is *constant* on each
  34orbit, and a constant with mean one is one.  So the equivariant theorem is mean one plus
  35constancy, and only constancy fails below.
  36
  37## §2-§4, the witness: an edge-label transposition and a sign that flips under it
  38
  39Mean one with non-constant terms needs a way to split an orbit into halves that cancel.  The
  40device is an involution of the *labeled* carrier that preserves gauge classes: `twist` relabels a
  41complex by transposing edge letters `0` and `1` (`edgeRelabel`, `swap01`).  Two facts make it
  42work.  It lands in the same class, since it is a relabeling (`twistRel`, `twist_class`), and it is
  43an involution on the nose (`twist_twist`), so it is a permutation of the carrier (`twistEquiv`).
  44
  45`edgeSign` reads the two transposed letters and compares the endpoint keys of their incidence
  46pairs, returning `+1`, `-1` or `0`.  Transposing the letters swaps the two keys, and the
  47comparison is antisymmetric, so `edgeSign_twist`: the sign changes sign under the twist.  A
  48summand the twist negates cancels in pairs along each orbit, which is `classMass_of_twistOdd`,
  49proved by reindexing the class sum along `twistEquiv` and observing that the sum equals its own
  50negation.
  51
  52The cost is then read off the numerator we want rather than guessed: `tiltedNumer t K =
  531 + t * edgeSign K`, which is positive for `|t| < 1` and satisfies `tiltedNumer t (twist K) =
  542 - tiltedNumer t K`, so its excess over one is twist-odd and cancels.  `tiltedCost t` charges
  55every letter of `K` an equal share of `-log (tiltedNumer t K)`, so its history cost is exactly
  56`-log (tiltedNumer t K)` (`historyCost_tiltedCost`) and its numerator is exactly `tiltedNumer t K`
  57(`exp_neg_historyCost_tiltedCost`).  Nothing here is baked: the numerator identity is a theorem
  58about a sum over the alphabet, and neither `gibbsWeight` nor `mu` appears in the definition of the
  59cost, the sign, or the twist.
  60
  61## The result
  62
  63`nonequivariant_cost_posts_mu_with_nonunit_numerator` (at `t = 1/2`) and
  64`nonequivariant_posting_family` (for every `|t| < 1`, `t ≠ 0`):
  65
  66* the cost is not gauge-equivariant (`tiltedCost_not_equivariant`);
  67* its class mass is `mu` at **every** complex at **every** cap (`tiltedCost_posts_mu`);
  68* its numerator is `1 + t` at `loopAndBridge`, hence not identically one
  69  (`numerator_ne_one_at_loopAndBridge`).
  70
  71So the forward direction of `equivariant_posts_mu_iff_numerator_one` **fails without the
  72equivariance hypothesis**, and the hypothesis is load-bearing rather than convenient
  73(`equivariance_is_load_bearing`).  This is a family, not one accident: distinct tilts give
  74distinct numerators at the same complex (`family_injective_at_loopAndBridge`), so a continuum of
  75letter costs posts `mu` exactly.
  76
  77## What this does NOT show, stated before anyone reads it as more
  78
  79**It does not derive the measure, and it does not weaken the uniqueness wall.**  It moves the
  80non-equivariant case from OPEN to underdetermined, which is the *opposite* of progress toward a
  81derivation: where the equivariant class contained exactly one posted numerator compatible with
  82`mu`, the full class contains a continuum.  The narrow true statement about determination: among
  83costs which post `mu`, the cost contributes no factor to the *class* mass; costs that fail to post
  84it exist and do constrain the measure (`Gap2PostingCostDerivation.incidencePosting_classMass_ne_mu`),
  85and the criterion `posts_mu_iff_numeratorMass_eq_orbitCard` discriminates the two.  What changes is
  86that the reason is no longer rigidity, and orbit-mean-one is a strictly weaker, hypothesis-free
  87target for any future premise-level selection principle on letter costs.
  88
  89**It does not contradict `Gap2GaugeVolume.invariant_weight_gives_measure_iff`.**  That theorem
  90quantifies over relabeling-invariant labeled weights, and the witness's posted weight is not one
  91(`postedWeight_tiltedCost_not_invariant`): it is `(1+t)` times the Gibbs weight at `loopAndBridge`
  92and `(1-t)` times it at the twist, which are gauge-equivalent.  The witness escapes the class the
  93wall quantifies over; it does not breach the wall.
  94
  95**It does not put a non-unit numerator anywhere the normalizations look.**  The sign vanishes
  96whenever a complex has fewer than two edge letters (`edgeSign_eq_zero_of_nE_le_one`), so the
  97numerator is one at the empty complex and at all three atoms, and the witness satisfies
  98`NormalizedAtTheAtoms` (`normalizedAtTheAtoms_tiltedCost`).  The non-unit values live only where
  99the sector group moves a complex to a *different* labeled complex in the same class, which is the
 100only place they could live: on a class whose orbit is a single labeled complex, mean one is
 101literally "the one term is one", for any cost whatever.
 102
 103**It says nothing about what a substrate posts.**  `Equivariant` is the posting-layer form of
 104"labels are gauge"; a cost that fails it charges two labelings of one complex differently.
 105Whether the ledger does that is not a question any theorem here answers, and the premise the
 106measure rests on is still the one `Gap2GaugeVolume` named, unit sector fugacity, reducible to the
 107gluing law and not to anything proved here.
 108
 109**It is a witness at one carrier cap for the non-unit half.**  The posting identity
 110`tiltedCost_posts_mu` is proved for every `B` and every complex; the non-unit numerator is
 111exhibited at `B = 3` on `loopAndBridge`.  One complex is all a counterexample needs, and no claim
 112is made that the sign is non-vanishing on most complexes: it is not.
 113
 114## Honest tagging
 115
 116Every declaration below is THEOREM (kernel-checked in this module).  The headline certificates,
 117the criterion, the witness, and the family injectivity are audited by `#print axioms` at the foot,
 118each at the base triple only.  The reading of `LetterCost` as a substrate charging rule, of `historyCost` as
 119ledger additivity over postings, and of the Boltzmann form, are the same three MODEL attachments
 120`Gap2PostingCostDerivation` names in its header; this module inherits them and adds none.
 121
 122**Strength.**  The witness is an exact equality of reals at every complex and every cap, not an
 123agreement to a tolerance, and the family is a continuum rather than a single point.  The non-unit
 124claim is exact: the numerator at `loopAndBridge` is `1 + t`, so `3/2` at the tilt used in the
 125headline, against `1`.
 126-/
 127
 128namespace IndisputableMonolith
 129namespace Gravity
 130namespace SevenGaps
 131namespace Gap2NonEquivariantPosting
 132
 133open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
 134open GaugeHistoryMeasure Gap2SizeBlindnessReach Gap2PostingCostDerivation
 135
 136noncomputable section
 137
 138variable {B : ℕ}
 139
 140/-! ## §0. Two pieces of bookkeeping
 141
 142`sgnLt` is a comparison written as a difference of indicators rather than a nest of branches,
 143which is what makes its antisymmetry a `ring` step instead of a case analysis.  `classMass` is
 144linear, and the four lemmas that say so are used throughout. -/
 145
 146/-- The comparison sign of two naturals, as a difference of indicators: `1` if `x < y`, `-1` if
 147`y < x`, `0` if neither.  Written this way on purpose: `sgnLt_swap` is then `ring`. -/
 148def sgnLt (x y : ℕ) : ℝ := (if x < y then (1 : ℝ) else 0) - (if y < x then (1 : ℝ) else 0)
 149
 150/-- **The antisymmetry.**  Swapping the arguments negates the sign.  This is the whole mechanism
 151of the witness, and it is one `ring` call because the definition is a difference. -/
 152theorem sgnLt_swap (x y : ℕ) : sgnLt y x = -sgnLt x y := by
 153  unfold sgnLt
 154  ring
 155
 156/-- The sign takes only three values, so a tilt of size less than one keeps `1 + t · sign`
 157positive. -/
 158theorem sgnLt_cases (x y : ℕ) : sgnLt x y = 1 ∨ sgnLt x y = -1 ∨ sgnLt x y = 0 := by
 159  unfold sgnLt
 160  split_ifs <;> norm_num
 161
 162theorem classMass_zero (cl : TriangulationClass B) :
 163    classMass (fun _ : BoundedComplex B => (0 : ℝ)) cl = 0 := by
 164  classical
 165  unfold classMass
 166  exact Finset.sum_eq_zero fun K _ => by split_ifs <;> rfl
 167
 168theorem classMass_add (D E : BoundedComplex B → ℝ) (cl : TriangulationClass B) :
 169    classMass (fun K => D K + E K) cl = classMass D cl + classMass E cl := by
 170  classical
 171  unfold classMass
 172  rw [← Finset.sum_add_distrib]
 173  exact Finset.sum_congr rfl fun K _ => by split_ifs <;> simp
 174
 175theorem classMass_neg (D : BoundedComplex B → ℝ) (cl : TriangulationClass B) :
 176    classMass (fun K => -D K) cl = -classMass D cl := by
 177  have h : classMass (fun K => D K + -D K) cl
 178      = classMass D cl + classMass (fun K => -D K) cl :=
 179    classMass_add D (fun K => -D K) cl
 180  have h0 : (fun K : BoundedComplex B => D K + -D K) = fun _ : BoundedComplex B => (0 : ℝ) := by
 181    funext K
 182    ring
 183  rw [h0, classMass_zero] at h
 184  linarith
 185
 186/-- The class mass of the constant weight one is the orbit count. -/
 187theorem classMass_one (K : BoundedComplex B) :
 188    classMass (fun _ : BoundedComplex B => (1 : ℝ)) (Quotient.mk (relabelSetoid B) K)
 189      = (gaugeOrbitCard K : ℝ) := by
 190  have h := classMass_of_invariant (fun _ : BoundedComplex B => (1 : ℝ))
 191    (fun _ _ _ => rfl) (Quotient.mk (relabelSetoid B) K)
 192  simp only [orbitCardClass_mk, mul_one] at h
 193  exact h
 194
 195/-! ## §1. The sharp condition for posting `mu`, with no equivariance hypothesis
 196
 197`equivariant_posts_mu_iff_numerator_one` reads the collapse off
 198`Gap2GaugeVolume.invariant_weight_gives_measure_iff`, which needs invariance.  Underneath that
 199theorem there is an identity needing nothing: the divisor is a class function, so it factors out
 200of the class sum, and what is left is a condition on the numerator's *total* over the class.  That
 201total is the object the open case is about. -/
 202
 203/-- The **numerator mass** of a letter cost: the total of its Boltzmann numerator over the labeled
 204complexes presenting a class.  Written with the module's own `classMass` functional so that no new
 205summation or decidability convention enters. -/
 206def numeratorMass (c : LetterCost) (B : ℕ) : TriangulationClass B → ℝ :=
 207  classMass (fun K' : BoundedComplex B => Real.exp (-(historyCost c B K')))
 208
 209/-- **THEOREM (the divisor factors out of every class sum).**  For an arbitrary letter cost, the
 210class mass of its posted weight is the Gibbs weight of any representative times the numerator
 211mass of the class.  No equivariance and no premise on the cost: the only input is that
 212`gibbsWeight` is a class function (`gibbsWeight_invariant`), which holds because it is a function
 213of the three sizes. -/
 214theorem classMass_postedWeight (c : LetterCost) (B : ℕ) (K : BoundedComplex B) :
 215    classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K)
 216      = gibbsWeight K * numeratorMass c B (Quotient.mk (relabelSetoid B) K) := by
 217  classical
 218  unfold numeratorMass classMass
 219  rw [Finset.mul_sum]
 220  refine Finset.sum_congr rfl fun K' _ => ?_
 221  by_cases hc : Quotient.mk (relabelSetoid B) K' = Quotient.mk (relabelSetoid B) K
 222  · rw [if_pos hc, if_pos hc]
 223    unfold postedWeight
 224    rw [gibbsWeight_invariant (Quotient.exact hc)]
 225    ring
 226  · rw [if_neg hc, if_neg hc, mul_zero]
 227
 228/-- **THEOREM (`mu` is the orbit count times the gauge volume, in posted form).**  Recorded in the
 229shape the criterion below needs.  This is `Gap2GaugeVolume`'s orbit-stabilizer accounting read
 230through `classMass`, not a new fact. -/
 231theorem mu_eq_orbitCard_mul_gibbsWeight (K : BoundedComplex B) :
 232    mu K = (gaugeOrbitCard K : ℝ) * gibbsWeight K := by
 233  have h := classMass_of_invariant (fun K' : BoundedComplex B => gibbsWeight K')
 234    (fun _ _ hh => gibbsWeight_invariant hh) (Quotient.mk (relabelSetoid B) K)
 235  simp only [orbitCardClass_mk] at h
 236  rw [classMass_gibbsWeight_eq_mu K, gibbsWeight_invariant (equivalent_out K)] at h
 237  exact h
 238
 239/-- **THEOREM (the sharp condition: orbit mean one).**  For **every** letter cost, equivariant or
 240not, the posted weight has class mass `mu` at a complex exactly when its Boltzmann numerator
 241totals that complex's orbit count over the class, i.e. exactly when the numerator has mean one on
 242that gauge orbit.
 243
 244This is the statement `equivariant_posts_mu_iff_numerator_one` specializes.  Saying it in this
 245form is what turns the open case into a question with an answer: "identically one" is strictly
 246stronger than "mean one", and the gap between them is exactly the room a non-equivariant cost has
 247to move in. -/
 248theorem posts_mu_iff_numeratorMass_eq_orbitCard (c : LetterCost) (B : ℕ) (K : BoundedComplex B) :
 249    classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K
 250      ↔ numeratorMass c B (Quotient.mk (relabelSetoid B) K) = (gaugeOrbitCard K : ℝ) := by
 251  have hg : (0 : ℝ) < gibbsWeight K := gibbsWeight_positive K
 252  rw [classMass_postedWeight, mu_eq_orbitCard_mul_gibbsWeight]
 253  constructor
 254  · intro h
 255    have h' : gibbsWeight K * numeratorMass c B (Quotient.mk (relabelSetoid B) K)
 256        = gibbsWeight K * (gaugeOrbitCard K : ℝ) := by
 257      rw [h]; ring
 258    exact mul_left_cancel₀ (ne_of_gt hg) h'
 259  · intro h
 260    rw [h]
 261    ring
 262
 263/-- **THEOREM (where equivariance was doing its work).**  If a cost's history cost is a class
 264function, which is what equivariance buys (`historyCost_invariant`), then its numerator is
 265constant on each orbit, and orbit mean one forces the value one.
 266
 267So the equivariant collapse decomposes into two independent halves: mean one, which is forced by
 268`mu` for every cost, and constancy on orbits, which is forced only by invariance.  Everything
 269below attacks the second half. -/
 270theorem orbitMeanOne_forces_one_of_invariant (c : LetterCost) (B : ℕ)
 271    (hinv : ∀ K K' : BoundedComplex B, Equivalent K K' →
 272      historyCost c B K = historyCost c B K') (K : BoundedComplex B)
 273    (h : numeratorMass c B (Quotient.mk (relabelSetoid B) K) = (gaugeOrbitCard K : ℝ)) :
 274    Real.exp (-(historyCost c B K)) = 1 := by
 275  have hnum : ∀ K₁ K₂ : BoundedComplex B, Equivalent K₁ K₂ →
 276      Real.exp (-(historyCost c B K₁)) = Real.exp (-(historyCost c B K₂)) := by
 277    intro K₁ K₂ he
 278    rw [hinv K₁ K₂ he]
 279  have hc := classMass_of_invariant
 280    (fun K' : BoundedComplex B => Real.exp (-(historyCost c B K'))) hnum
 281    (Quotient.mk (relabelSetoid B) K)
 282  simp only [orbitCardClass_mk] at hc
 283  unfold numeratorMass at h
 284  rw [hc, hnum _ K (equivalent_out K)] at h
 285  have horb : (0 : ℝ) < (gaugeOrbitCard K : ℝ) := by
 286    exact_mod_cast gaugeOrbitCard_pos K
 287  have h' : (gaugeOrbitCard K : ℝ) * Real.exp (-(historyCost c B K))
 288      = (gaugeOrbitCard K : ℝ) * 1 := by
 289    rw [mul_one]; exact h
 290  exact mul_left_cancel₀ (ne_of_gt horb) h'
 291
 292/-! ## §2. The twist: transposing two edge letters is a class-preserving involution
 293
 294The carrier permutation the cancellation runs on.  `edgeRelabel` renames the edge index set,
 295which is a gauge motion by construction; `swap01` is the transposition of `0` and `1` in `Fin n`,
 296the identity when `n < 2`; `twist` is their composite.  What has to be true, and is proved rather
 297than assumed, is that the twist stays inside the gauge class and squares to the identity. -/
 298
 299/-- Transpose `0` and `1` in `Fin n`; the identity when there is no `1` to transpose.  Stated for a
 300bare `n` rather than for `K.nE` so that the twist of a twist reduces without dependent friction. -/
 301def swap01 (n : ℕ) : Equiv.Perm (Fin n) :=
 302  if h : 1 < n then Equiv.swap ⟨0, by omega⟩ ⟨1, h⟩ else Equiv.refl _
 303
 304theorem swap01_involutive (n : ℕ) : Function.Involutive (swap01 n) := by
 305  intro e
 306  unfold swap01
 307  by_cases h : 1 < n
 308  · rw [dif_pos h]
 309    exact Equiv.swap_apply_self _ _ _
 310  · rw [dif_neg h]
 311    rfl
 312
 313theorem swap01_trans_self (n : ℕ) : (swap01 n).trans (swap01 n) = Equiv.refl (Fin n) :=
 314  Equiv.ext fun e => swap01_involutive n e
 315
 316theorem swap01_apply_zero {n : ℕ} (h : 1 < n) (h0 : 0 < n) : swap01 n ⟨0, h0⟩ = ⟨1, h⟩ := by
 317  unfold swap01
 318  rw [dif_pos h]
 319  exact Equiv.swap_apply_left _ _
 320
 321theorem swap01_apply_one {n : ℕ} (h : 1 < n) (h0 : 0 < n) : swap01 n ⟨1, h⟩ = ⟨0, h0⟩ := by
 322  unfold swap01
 323  rw [dif_pos h]
 324  exact Equiv.swap_apply_right _ _
 325
 326/-- Rename the edge index set of `K` by a permutation of it, keeping the incidence pairs and
 327everything else.  A gauge motion at the labeled level. -/
 328def edgeRelabel (K : BoundedComplex B) (σ : Equiv.Perm (Fin K.nE)) : BoundedComplex B where
 329  nV := K.nV
 330  nE := K.nE
 331  nT := K.nT
 332  hV := K.hV
 333  hE := K.hE
 334  hT := K.hT
 335  edgeVerts := fun e => K.edgeVerts (σ e)
 336  tetVerts := K.tetVerts
 337
 338/-- **The twist**: the complex with its first two edge letters exchanged. -/
 339def twist (K : BoundedComplex B) : BoundedComplex B := edgeRelabel K (swap01 K.nE)
 340
 341theorem twist_nE (K : BoundedComplex B) : (twist K).nE = K.nE := rfl
 342
 343theorem twist_edgeVerts (K : BoundedComplex B) (e : Fin K.nE) :
 344    (twist K).edgeVerts e = K.edgeVerts (swap01 K.nE e) := rfl
 345
 346/-- **THEOREM (the twist is an involution).**  Twisting twice composes the transposition with
 347itself, which is the identity permutation, and renaming by the identity is the complex itself. -/
 348theorem twist_twist (K : BoundedComplex B) : twist (twist K) = K := by
 349  have h1 : twist (twist K) = edgeRelabel K ((swap01 K.nE).trans (swap01 K.nE)) := rfl
 350  have h2 : edgeRelabel K (Equiv.refl (Fin K.nE)) = K := rfl
 351  rw [h1, swap01_trans_self, h2]
 352
 353/-- The twist as a permutation of the labeled carrier: what the class sums are reindexed along. -/
 354def twistEquiv (B : ℕ) : BoundedComplex B ≃ BoundedComplex B where
 355  toFun := twist
 356  invFun := twist
 357  left_inv := twist_twist
 358  right_inv := twist_twist
 359
 360theorem twistEquiv_apply (B : ℕ) (K : BoundedComplex B) : twistEquiv B K = twist K := rfl
 361
 362/-- **THEOREM (the twist is a relabeling).**  The transposition of edge letters, with the identity
 363on vertices and tetrahedra, satisfies the incidence commutation conditions onto the twisted
 364complex.  This is what keeps the twist inside the gauge class. -/
 365def twistRel (K : BoundedComplex B) : Relabel K (twist K) where
 366  vEquiv := Equiv.refl _
 367  eEquiv := swap01 K.nE
 368  tEquiv := Equiv.refl _
 369  edge_comm := fun e => by
 370    show K.edgeVerts (swap01 K.nE (swap01 K.nE e)) = K.edgeVerts e
 371    rw [swap01_involutive K.nE e]
 372  tet_comm := fun _ _ => rfl
 373
 374theorem twist_equivalent (K : BoundedComplex B) : Equivalent K (twist K) := ⟨twistRel K⟩
 375
 376theorem twist_class (K : BoundedComplex B) :
 377    Quotient.mk (relabelSetoid B) (twist K) = Quotient.mk (relabelSetoid B) K :=
 378  (Quotient.sound (twist_equivalent K)).symm
 379
 380/-! ## §3. Twist-odd functions have zero total on every class
 381
 382The cancellation lemma.  Reindexing a class sum along the twist changes nothing, because the twist
 383preserves classes and permutes the carrier; so a summand the twist negates gives a sum equal to
 384its own negation. -/
 385
 386/-- Reindexing a class sum along the twist leaves it unchanged. -/
 387theorem classMass_comp_twist (D : BoundedComplex B → ℝ) (cl : TriangulationClass B) :
 388    classMass (fun K => D (twist K)) cl = classMass D cl := by
 389  classical
 390  unfold classMass
 391  refine Fintype.sum_equiv (twistEquiv B) _ _ fun K => ?_
 392  rw [twistEquiv_apply, twist_class]
 393
 394/-- **THEOREM (the cancellation lemma).**  A real function on labeled complexes that the twist
 395negates has total zero over every gauge class.  Two lines of content: the class sum is invariant
 396under reindexing by the twist, and the twist negates the summand, so the sum is its own
 397negation. -/
 398theorem classMass_of_twistOdd (D : BoundedComplex B → ℝ)
 399    (hodd : ∀ K : BoundedComplex B, D (twist K) = -D K) (cl : TriangulationClass B) :
 400    classMass D cl = 0 := by
 401  have h1 : classMass (fun K => D (twist K)) cl = classMass D cl := classMass_comp_twist D cl
 402  have h2 : (fun K : BoundedComplex B => D (twist K)) = fun K : BoundedComplex B => -D K :=
 403    funext hodd
 404  rw [h2, classMass_neg] at h1
 405  linarith
 406
 407/-! ## §4. The sign that flips, and the cost built from it
 408
 409The one thing left is a function of the labeled complex that the twist negates.  The twist
 410exchanges edge letters `0` and `1`, so anything that compares those two letters antisymmetrically
 411will do.  `keyAt` is the endpoint pair of a numbered edge letter, packed into one natural number
 412with the size cap as radix.  `edgeSign` compares letters `0` and `1`, and is silent wherever there
 413is no second letter. -/
 414
 415/-- The endpoint pair of edge letter `i`, packed into one natural number; `0` when the complex has
 416no letter `i`.  Total in `i` by design. -/
 417def keyAt (K : BoundedComplex B) (i : ℕ) : ℕ :=
 418  if h : i < K.nE then (K.edgeVerts ⟨i, h⟩).1.val * B + (K.edgeVerts ⟨i, h⟩).2.val else 0
 419
 420theorem keyAt_of_lt {K : BoundedComplex B} {i : ℕ} (h : i < K.nE) :
 421    keyAt K i = (K.edgeVerts ⟨i, h⟩).1.val * B + (K.edgeVerts ⟨i, h⟩).2.val :=
 422  dif_pos h
 423
 424/-- Reading a key through the twist reads the transposed letter.  Stated for whichever pair of
 425letters the transposition exchanges, so the two directions below are one lemma applied twice. -/
 426theorem keyAt_twist {K : BoundedComplex B} {i j : ℕ} (hi : i < K.nE) (hj : j < K.nE)
 427    (hij : swap01 K.nE ⟨i, hi⟩ = ⟨j, hj⟩) : keyAt (twist K) i = keyAt K j := by
 428  have hi' : i < (twist K).nE := hi
 429  have e1 : keyAt (twist K) i
 430      = ((twist K).edgeVerts ⟨i, hi'⟩).1.val * B + ((twist K).edgeVerts ⟨i, hi'⟩).2.val :=
 431    keyAt_of_lt hi'
 432  have e2 : keyAt K j = (K.edgeVerts ⟨j, hj⟩).1.val * B + (K.edgeVerts ⟨j, hj⟩).2.val :=
 433    keyAt_of_lt hj
 434  have e3 : (twist K).edgeVerts ⟨i, hi'⟩ = K.edgeVerts ⟨j, hj⟩ := by
 435    have e4 : (twist K).edgeVerts ⟨i, hi'⟩ = K.edgeVerts (swap01 K.nE ⟨i, hi⟩) := rfl
 436    rw [e4, hij]
 437  rw [e1, e2, e3]
 438
 439theorem keyAt_twist_zero {K : BoundedComplex B} (h : 1 < K.nE) :
 440    keyAt (twist K) 0 = keyAt K 1 := by
 441  have h0 : (0 : ℕ) < K.nE := by omega
 442  exact keyAt_twist h0 h (swap01_apply_zero h h0)
 443
 444theorem keyAt_twist_one {K : BoundedComplex B} (h : 1 < K.nE) :
 445    keyAt (twist K) 1 = keyAt K 0 := by
 446  have h0 : (0 : ℕ) < K.nE := by omega
 447  exact keyAt_twist h h0 (swap01_apply_one h h0)
 448
 449/-- The **sign of a labeled complex**: the comparison of the endpoint keys of its first two edge
 450letters, and `0` when it has fewer than two.  This is the only place the witness reads a label
 451rather than a class invariant, and it is what makes the cost non-equivariant. -/
 452def edgeSign (K : BoundedComplex B) : ℝ :=
 453  if 1 < K.nE then sgnLt (keyAt K 0) (keyAt K 1) else 0
 454
 455theorem edgeSign_cases (K : BoundedComplex B) :
 456    edgeSign K = 1 ∨ edgeSign K = -1 ∨ edgeSign K = 0 := by
 457  unfold edgeSign
 458  by_cases h : 1 < K.nE
 459  · rw [if_pos h]
 460    exact sgnLt_cases _ _
 461  · rw [if_neg h]
 462    exact Or.inr (Or.inr rfl)
 463
 464/-- The sign is silent on every complex with fewer than two edge letters, hence at the empty
 465complex and at all three atoms.  This is the scope clause of the whole construction: the witness
 466puts nothing non-unit where the normalizations look. -/
 467theorem edgeSign_eq_zero_of_nE_le_one (K : BoundedComplex B) (h : K.nE ≤ 1) : edgeSign K = 0 := by
 468  unfold edgeSign
 469  rw [if_neg (by omega : ¬ 1 < K.nE)]
 470
 471/-- **THEOREM (the sign flips under the twist).**  The twist exchanges edge letters `0` and `1`,
 472so it exchanges their keys, and the comparison is antisymmetric.  The vanishing case is stable
 473because the twist preserves the edge count. -/
 474theorem edgeSign_twist (K : BoundedComplex B) : edgeSign (twist K) = -edgeSign K := by
 475  by_cases h : 1 < K.nE
 476  · have hT : 1 < (twist K).nE := h
 477    unfold edgeSign
 478    rw [if_pos hT, if_pos h, keyAt_twist_zero h, keyAt_twist_one h,
 479      sgnLt_swap (keyAt K 0) (keyAt K 1)]
 480  · have hT : (twist K).nE ≤ 1 := by
 481      have hEq : (twist K).nE = K.nE := twist_nE K
 482      omega
 483    rw [edgeSign_eq_zero_of_nE_le_one (twist K) hT,
 484      edgeSign_eq_zero_of_nE_le_one K (by omega), neg_zero]
 485
 486/-! ### The numerator, and the cost that posts it -/
 487
 488/-- The **tilted numerator**: one plus `t` times the sign.  This is the Boltzmann numerator the
 489witness is built to have, and the two facts it needs are that it is positive (so it is an
 490exponential of something real) and that it and its twist average to one. -/
 491def tiltedNumer (t : ℝ) (K : BoundedComplex B) : ℝ := 1 + t * edgeSign K
 492
 493theorem tiltedNumer_pos {t : ℝ} (ht : |t| < 1) (K : BoundedComplex B) : 0 < tiltedNumer t K := by
 494  obtain ⟨h1, h2⟩ := abs_lt.mp ht
 495  unfold tiltedNumer
 496  rcases edgeSign_cases K with h | h | h <;> rw [h] <;> linarith
 497
 498/-- **The cancellation identity.**  A complex and its twist carry numerators averaging to one.
 499Nothing about `mu` or `gibbsWeight` enters: this is `edgeSign_twist` and arithmetic. -/
 500theorem tiltedNumer_twist (t : ℝ) (K : BoundedComplex B) :
 501    tiltedNumer t (twist K) = 2 - tiltedNumer t K := by
 502  unfold tiltedNumer
 503  rw [edgeSign_twist]
 504  ring
 505
 506theorem tiltedNumer_eq_one_of_nE_le_one (t : ℝ) (K : BoundedComplex B) (h : K.nE ≤ 1) :
 507    tiltedNumer t K = 1 := by
 508  unfold tiltedNumer
 509  rw [edgeSign_eq_zero_of_nE_le_one K h, mul_zero, add_zero]
 510
 511/-- The **witness letter cost**: every letter of `K` is charged an equal share of
 512`-log (tiltedNumer t K)`.  The cost reads the labeling through `edgeSign`, which is exactly why it
 513is not equivariant. -/
 514def tiltedCost (t : ℝ) : LetterCost := fun _ K _ =>
 515  -(Real.log (tiltedNumer t K)) / ((K.nV + K.nE + K.nT : ℕ) : ℝ)
 516
 517/-- **THEOREM (the history cost is what it was designed to be).**  Summing the shared charge over
 518the alphabet returns the whole of `-log (tiltedNumer t K)`, at every complex including the empty
 519one, where both sides vanish because a complex with no cells has no edge letters and hence unit
 520numerator.  This is the theorem that keeps the numerator claim from being an assumption. -/
 521theorem historyCost_tiltedCost (t : ℝ) (B : ℕ) (K : BoundedComplex B) :
 522    historyCost (tiltedCost t) B K = -(Real.log (tiltedNumer t K)) := by
 523  have hcard : (Finset.univ : Finset (PostingAlphabet K)).card = K.nV + K.nE + K.nT := by
 524    rw [Finset.card_univ, card_postingAlphabet]
 525  unfold historyCost tiltedCost
 526  rw [Finset.sum_const, hcard, nsmul_eq_mul]
 527  by_cases hN : K.nV + K.nE + K.nT = 0
 528  · have h1 : tiltedNumer t K = 1 := tiltedNumer_eq_one_of_nE_le_one t K (by omega)
 529    rw [h1, Real.log_one, neg_zero, zero_div, mul_zero]
 530  · have hne : ((K.nV + K.nE + K.nT : ℕ) : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hN
 531    field_simp
 532
 533/-- **THEOREM (the Boltzmann numerator of the witness).**  Exactly `tiltedNumer t K`. -/
 534theorem exp_neg_historyCost_tiltedCost {t : ℝ} (ht : |t| < 1) (B : ℕ) (K : BoundedComplex B) :
 535    Real.exp (-(historyCost (tiltedCost t) B K)) = tiltedNumer t K := by
 536  rw [historyCost_tiltedCost, neg_neg, Real.exp_log (tiltedNumer_pos ht K)]
 537
 538theorem postedWeight_tiltedCost {t : ℝ} (ht : |t| < 1) (B : ℕ) (K : BoundedComplex B) :
 539    postedWeight (tiltedCost t) B K = tiltedNumer t K * gibbsWeight K := by
 540  unfold postedWeight
 541  rw [exp_neg_historyCost_tiltedCost ht]
 542
 543/-! ### The witness posts `mu` -/
 544
 545/-- The numerator mass of the witness is the orbit count: the excess over one is twist-odd, so it
 546cancels, and what survives is the constant one summed over the class. -/
 547theorem numeratorMass_tiltedCost {t : ℝ} (ht : |t| < 1) (B : ℕ) (K : BoundedComplex B) :
 548    numeratorMass (tiltedCost t) B (Quotient.mk (relabelSetoid B) K)
 549      = (gaugeOrbitCard K : ℝ) := by
 550  have hodd : ∀ K' : BoundedComplex B,
 551      tiltedNumer t (twist K') - 1 = -(tiltedNumer t K' - 1) := by
 552    intro K'
 553    rw [tiltedNumer_twist]
 554    ring
 555  have hzero : classMass (fun K' : BoundedComplex B => tiltedNumer t K' - 1)
 556      (Quotient.mk (relabelSetoid B) K) = 0 :=
 557    classMass_of_twistOdd (fun K' : BoundedComplex B => tiltedNumer t K' - 1) hodd _
 558  have hsplit := classMass_add (fun _ : BoundedComplex B => (1 : ℝ))
 559    (fun K' : BoundedComplex B => tiltedNumer t K' - 1) (Quotient.mk (relabelSetoid B) K)
 560  have hfun : (fun K' : BoundedComplex B => Real.exp (-(historyCost (tiltedCost t) B K')))
 561      = fun K' : BoundedComplex B => (1 : ℝ) + (tiltedNumer t K' - 1) := by
 562    funext K'
 563    rw [exp_neg_historyCost_tiltedCost ht]
 564    ring
 565  unfold numeratorMass
 566  rw [hfun, hsplit, hzero, add_zero, classMass_one]
 567
 568/-- **THEOREM (the witness posts the measure exactly).**  For every tilt of size less than one, at
 569every cap and every complex, the class mass of the witness's posted weight is `mu`. -/
 570theorem tiltedCost_posts_mu {t : ℝ} (ht : |t| < 1) (B : ℕ) (K : BoundedComplex B) :
 571    classMass (postedWeight (tiltedCost t) B) (Quotient.mk (relabelSetoid B) K) = mu K :=
 572  (posts_mu_iff_numeratorMass_eq_orbitCard (tiltedCost t) B K).mpr
 573    (numeratorMass_tiltedCost ht B K)
 574
 575/-! ### The numerator is not identically one
 576
 577`loopAndBridge` is `Gap2PostingCostDerivation`'s three-vertex complex with one loop `(0,0)` and
 578one proper edge `(1,2)`.  Its two edge letters carry different endpoint keys, `0` against `5`, so
 579the sign is `+1` and the numerator is `1 + t`. -/
 580
 581theorem keyAt_loopAndBridge_zero : keyAt loopAndBridge 0 = 0 := by decide
 582
 583theorem keyAt_loopAndBridge_one : keyAt loopAndBridge 1 = 5 := by decide
 584
 585theorem edgeSign_loopAndBridge : edgeSign loopAndBridge = 1 := by
 586  unfold edgeSign
 587  rw [if_pos (show 1 < loopAndBridge.nE by decide),
 588    keyAt_loopAndBridge_zero, keyAt_loopAndBridge_one]
 589  unfold sgnLt
 590  norm_num
 591
 592theorem tiltedNumer_loopAndBridge (t : ℝ) : tiltedNumer t loopAndBridge = 1 + t := by
 593  unfold tiltedNumer
 594  rw [edgeSign_loopAndBridge, mul_one]
 595
 596/-- **THEOREM (a non-unit numerator).**  At `loopAndBridge` the witness's Boltzmann numerator is
 597`1 + t`, so for any nonzero tilt it is not one. -/
 598theorem numerator_ne_one_at_loopAndBridge {t : ℝ} (ht : |t| < 1) (ht0 : t ≠ 0) :
 599    Real.exp (-(historyCost (tiltedCost t) 3 loopAndBridge)) ≠ 1 := by
 600  rw [exp_neg_historyCost_tiltedCost ht, tiltedNumer_loopAndBridge]
 601  intro h
 602  exact ht0 (by linarith)
 603
 604/-! ### The witness is not equivariant
 605
 606It cannot be, given the two theorems above: an equivariant cost with class mass `mu` has unit
 607numerator.  But the failure is exhibited directly rather than inferred, because the whole point is
 608that this cost lives outside the class the wall quantifies over. -/
 609
 610/-- **THEOREM (the witness is label-asymmetric).**  Its history cost differs between
 611`loopAndBridge` and the twist of it, which are gauge-equivalent, so it is not equivariant. -/
 612theorem tiltedCost_not_equivariant {t : ℝ} (ht : |t| < 1) (ht0 : t ≠ 0) :
 613    ¬ Equivariant (tiltedCost t) := by
 614  intro hc
 615  have h : historyCost (tiltedCost t) 3 loopAndBridge
 616      = historyCost (tiltedCost t) 3 (twist loopAndBridge) :=
 617    historyCost_invariant hc (twistRel loopAndBridge)
 618  have h2 : tiltedNumer t loopAndBridge = tiltedNumer t (twist loopAndBridge) := by
 619    rw [← exp_neg_historyCost_tiltedCost ht 3 loopAndBridge,
 620      ← exp_neg_historyCost_tiltedCost ht 3 (twist loopAndBridge), h]
 621  rw [tiltedNumer_twist, tiltedNumer_loopAndBridge] at h2
 622  exact ht0 (by linarith)
 623
 624/-- **THEOREM (the witness escapes the uniqueness wall rather than breaching it).**  Its posted
 625weight is not a relabeling-invariant labeled weight: `loopAndBridge` and its twist are
 626gauge-equivalent and carry `(1+t)` and `(1-t)` times the same Gibbs weight.  So
 627`Gap2GaugeVolume.invariant_weight_gives_measure_iff`, which quantifies over invariant weights, is
 628untouched, and this module contradicts nothing in the library. -/
 629theorem postedWeight_tiltedCost_not_invariant {t : ℝ} (ht : |t| < 1) (ht0 : t ≠ 0) :
 630    ¬ (∀ K K' : BoundedComplex 3, Equivalent K K' →
 631        postedWeight (tiltedCost t) 3 K = postedWeight (tiltedCost t) 3 K') := by
 632  intro hinv
 633  have hEq := hinv loopAndBridge (twist loopAndBridge) (twist_equivalent loopAndBridge)
 634  rw [postedWeight_tiltedCost ht, postedWeight_tiltedCost ht,
 635    gibbsWeight_invariant (twist_equivalent loopAndBridge)] at hEq
 636  have hg : (0 : ℝ) < gibbsWeight (twist loopAndBridge) := gibbsWeight_positive _
 637  have h2 : tiltedNumer t loopAndBridge = tiltedNumer t (twist loopAndBridge) :=
 638    mul_right_cancel₀ (ne_of_gt hg) hEq
 639  rw [tiltedNumer_twist, tiltedNumer_loopAndBridge] at h2
 640  exact ht0 (by linarith)
 641
 642/-- **THEOREM (the witness meets the normalizations too).**  Its posted weight is one at the empty
 643complex and at all three atoms, because a complex with at most one edge letter has unit numerator
 644and unit gauge volume.  So the witness is not excluded by `NormalizedAtTheAtoms`, and the reason
 645is structural: the sign has nothing to compare there. -/
 646theorem normalizedAtTheAtoms_tiltedCost {t : ℝ} (ht : |t| < 1) :
 647    NormalizedAtTheAtoms (postedWeight (tiltedCost t)) := by
 648  intro B' K hv hi
 649  rw [postedWeight_tiltedCost ht, tiltedNumer_eq_one_of_nE_le_one t K (by omega), one_mul,
 650    gibbsWeight_eq_one_at_atoms K hv hi]
 651
 652/-! ## §5. The open case, resolved -/
 653
 654/-- **THE OPEN CASE, RESOLVED IN THE WITNESS DIRECTION.**  At tilt `1/2`: a letter cost that is
 655not gauge-equivariant, whose posted weight has class mass exactly `mu` at every complex at every
 656cap, and whose Boltzmann numerator at `loopAndBridge` is `3/2` rather than `1`.
 657
 658This is the case `equivariant_posts_mu_iff_numerator_one` left open and `Gap2PostingLayerFloor` §4
 659showed inhabited without deciding.  It is now decided: orbit-sum cancellation is real, and the
 660forward implication of that theorem is false without its equivariance hypothesis. -/
 661theorem nonequivariant_cost_posts_mu_with_nonunit_numerator :
 662    ¬ Equivariant (tiltedCost (1/2))
 663      ∧ (∀ (B : ℕ) (K : BoundedComplex B),
 664          classMass (postedWeight (tiltedCost (1/2)) B) (Quotient.mk (relabelSetoid B) K) = mu K)
 665      ∧ Real.exp (-(historyCost (tiltedCost (1/2)) 3 loopAndBridge)) = 3/2
 666      ∧ NormalizedAtTheAtoms (postedWeight (tiltedCost (1/2))) := by
 667  have ht : |(1/2 : ℝ)| < 1 := by
 668    rw [abs_lt]
 669    constructor <;> norm_num
 670  have ht0 : (1/2 : ℝ) ≠ 0 := by norm_num
 671  refine ⟨tiltedCost_not_equivariant ht ht0, fun B K => tiltedCost_posts_mu ht B K, ?_,
 672    normalizedAtTheAtoms_tiltedCost ht⟩
 673  rw [exp_neg_historyCost_tiltedCost ht, tiltedNumer_loopAndBridge]
 674  norm_num
 675
 676/-- **THEOREM (the equivariance hypothesis is load-bearing).**  The equivalence
 677`equivariant_posts_mu_iff_numerator_one` fails when its hypothesis is dropped: there is a letter
 678cost posting `mu` at every complex of `BoundedComplex 3` whose numerator is not identically one.
 679Stated in exactly the shape of that theorem's two sides so the failure is checkable against it. -/
 680theorem equivariance_is_load_bearing :
 681    ∃ c : LetterCost,
 682      ¬ Equivariant c
 683        ∧ (∀ K : BoundedComplex 3,
 684            classMass (postedWeight c 3) (Quotient.mk (relabelSetoid 3) K) = mu K)
 685        ∧ ¬ (∀ K : BoundedComplex 3, Real.exp (-(historyCost c 3 K)) = 1) := by
 686  have ht : |(1/2 : ℝ)| < 1 := by
 687    rw [abs_lt]
 688    constructor <;> norm_num
 689  have ht0 : (1/2 : ℝ) ≠ 0 := by norm_num
 690  refine ⟨tiltedCost (1/2), tiltedCost_not_equivariant ht ht0,
 691    fun K => tiltedCost_posts_mu ht 3 K, ?_⟩
 692  intro hall
 693  exact numerator_ne_one_at_loopAndBridge ht ht0 (hall loopAndBridge)
 694
 695/-- **THEOREM (a continuum, not an accident).**  Every tilt of size less than one gives a cost
 696posting `mu` exactly, and for nonzero tilt the cost is not equivariant and the numerator is not
 697identically one.  So the non-equivariant class does not contain one exceptional cost compatible
 698with the measure; it contains a one-parameter family. -/
 699theorem nonequivariant_posting_family {t : ℝ} (ht : |t| < 1) (ht0 : t ≠ 0) :
 700    ¬ Equivariant (tiltedCost t)
 701      ∧ (∀ (B : ℕ) (K : BoundedComplex B),
 702          classMass (postedWeight (tiltedCost t) B) (Quotient.mk (relabelSetoid B) K) = mu K)
 703      ∧ Real.exp (-(historyCost (tiltedCost t) 3 loopAndBridge)) = 1 + t :=
 704  ⟨tiltedCost_not_equivariant ht ht0, fun B K => tiltedCost_posts_mu ht B K, by
 705    rw [exp_neg_historyCost_tiltedCost ht, tiltedNumer_loopAndBridge]⟩
 706
 707/-- The family is faithfully parametrized: distinct tilts give distinct numerators at the same
 708complex, so the costs above are genuinely different and the underdetermination is a continuum. -/
 709theorem family_injective_at_loopAndBridge {t s : ℝ}
 710    (h : tiltedNumer t loopAndBridge = tiltedNumer s loopAndBridge) : t = s := by
 711  rw [tiltedNumer_loopAndBridge, tiltedNumer_loopAndBridge] at h
 712  linarith
 713
 714/-- **THEOREM (what the resolution changes, and what it does not).**  The five-part verdict.
 715
 7161.  For every letter cost, equivariant or not, posting `mu` is exactly orbit mean one on the
 717    numerator (`posts_mu_iff_numeratorMass_eq_orbitCard`).
 7182.  Equivariance upgrades mean one to identically one only because it makes the numerator constant
 719    on orbits (`orbitMeanOne_forces_one_of_invariant`).
 7203.  Without it the upgrade fails: a label-reading cost posts `mu` with a non-unit numerator.
 7214.  That cost's posted weight is not relabeling-invariant, so the uniqueness wall is escaped, not
 722    breached.
 7235.  Its numerator is one wherever a complex has at most one edge letter, so the atom
 724    normalizations are met and the non-unit values sit only on classes the sector group moves. -/
 725theorem nonequivariant_case_verdict :
 726    (∀ (c : LetterCost) (B : ℕ) (K : BoundedComplex B),
 727        classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K
 728          ↔ numeratorMass c B (Quotient.mk (relabelSetoid B) K) = (gaugeOrbitCard K : ℝ))
 729      ∧ (∀ (c : LetterCost) (B : ℕ),
 730          (∀ K K' : BoundedComplex B, Equivalent K K' →
 731              historyCost c B K = historyCost c B K') →
 732            ∀ K : BoundedComplex B,
 733              numeratorMass c B (Quotient.mk (relabelSetoid B) K) = (gaugeOrbitCard K : ℝ) →
 734                Real.exp (-(historyCost c B K)) = 1)
 735      ∧ (∃ c : LetterCost, ¬ Equivariant c
 736          ∧ (∀ K : BoundedComplex 3,
 737              classMass (postedWeight c 3) (Quotient.mk (relabelSetoid 3) K) = mu K)
 738          ∧ ¬ (∀ K : BoundedComplex 3, Real.exp (-(historyCost c 3 K)) = 1))
 739      ∧ ¬ (∀ K K' : BoundedComplex 3, Equivalent K K' →
 740            postedWeight (tiltedCost (1/2)) 3 K = postedWeight (tiltedCost (1/2)) 3 K')
 741      ∧ (∀ (t : ℝ) (B : ℕ) (K : BoundedComplex B), K.nE ≤ 1 → tiltedNumer t K = 1) := by
 742  have ht : |(1/2 : ℝ)| < 1 := by
 743    rw [abs_lt]
 744    constructor <;> norm_num
 745  have ht0 : (1/2 : ℝ) ≠ 0 := by norm_num
 746  exact ⟨fun c B K => posts_mu_iff_numeratorMass_eq_orbitCard c B K,
 747    fun c B hinv K h => orbitMeanOne_forces_one_of_invariant c B hinv K h,
 748    equivariance_is_load_bearing,
 749    postedWeight_tiltedCost_not_invariant ht ht0,
 750    fun t _ K h => tiltedNumer_eq_one_of_nE_le_one t K h⟩
 751
 752/-! ## §6. Navigation index
 753
 754One flag flips relative to `Gap2PostingCostDerivation`: the non-equivariant case is settled.  The
 755flag it does **not** flip is the one that matters for the measure: the cost layer still contributes
 756no determination, and now for a second reason. -/
 757
 758structure Index : Type where
 759  /-- Posting `mu` is orbit mean one on the numerator, for every letter cost. -/
 760  posting_mu_is_orbit_mean_one : Bool
 761  /-- Equivariance is exactly what turns mean one into identically one. -/
 762  equivariance_supplies_constancy : Bool
 763  /-- SETTLED (this module): a non-equivariant cost can post `mu` with a non-unit numerator. -/
 764  nonequivariant_numerator_settled : Bool
 765  /-- The witness is a one-parameter family, not one exceptional cost. -/
 766  witness_is_a_family : Bool
 767  /-- The witness's posted weight is not relabeling-invariant, so the uniqueness wall stands. -/
 768  uniqueness_wall_escaped_not_breached : Bool
 769  /-- NOT proved, and made worse rather than better: that the cost layer determines the measure.
 770  The equivariant class admitted one compatible numerator; the full class admits a continuum. -/
 771  cost_layer_determines_the_measure : Bool
 772  /-- NOT proved: that anything here derives the measure's premise (unit sector fugacity,
 773  reducible to the gluing law).  A witness that the collapse fails is not a derivation. -/
 774  measure_premise_derived : Bool
 775
 776def index : Index where
 777  posting_mu_is_orbit_mean_one := true
 778  equivariance_supplies_constancy := true
 779  nonequivariant_numerator_settled := true
 780  witness_is_a_family := true
 781  uniqueness_wall_escaped_not_breached := true
 782  cost_layer_determines_the_measure := false
 783  measure_premise_derived := false
 784
 785theorem index_nonequivariant_settled : index.nonequivariant_numerator_settled = true := rfl
 786
 787theorem index_cost_layer_does_not_determine :
 788    index.cost_layer_determines_the_measure = false := rfl
 789
 790theorem index_premise_still_open : index.measure_premise_derived = false := rfl
 791
 792end
 793
 794#print axioms classMass_postedWeight
 795#print axioms family_injective_at_loopAndBridge
 796#print axioms mu_eq_orbitCard_mul_gibbsWeight
 797#print axioms posts_mu_iff_numeratorMass_eq_orbitCard
 798#print axioms orbitMeanOne_forces_one_of_invariant
 799#print axioms twist_twist
 800#print axioms twist_class
 801#print axioms classMass_of_twistOdd
 802#print axioms edgeSign_twist
 803#print axioms historyCost_tiltedCost
 804#print axioms exp_neg_historyCost_tiltedCost
 805#print axioms numeratorMass_tiltedCost
 806#print axioms tiltedCost_posts_mu
 807#print axioms numerator_ne_one_at_loopAndBridge
 808#print axioms tiltedCost_not_equivariant
 809#print axioms postedWeight_tiltedCost_not_invariant
 810#print axioms normalizedAtTheAtoms_tiltedCost
 811#print axioms nonequivariant_cost_posts_mu_with_nonunit_numerator
 812#print axioms equivariance_is_load_bearing
 813#print axioms nonequivariant_posting_family
 814#print axioms nonequivariant_case_verdict
 815
 816end Gap2NonEquivariantPosting
 817end SevenGaps
 818end Gravity
 819end IndisputableMonolith
 820