IndisputableMonolith.Gravity.SevenGaps.Gap2LetterCostDichotomy

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2OrientedFaceSpan
   2
   3/-!
   4# Gap 2 / A1.7: the letter-cost dichotomy, decided
   5
   6`Gap2JEhrhartSpan` (A1.5) and `Gap2OrientedFaceSpan` (A1.6) each built a gauge-equivariant
   7recognition cost out of an imbalance referent on the Freudenthal carrier, each cost had
   8bulk cancellation, and each died on the same clause: no fixed kind totals, because the
   9surviving total is a *surface* and a surface is not a fixed multiple of a volume.  Two
  10kills with one cause invite the obvious question, and this module answers it: is that
  11failure an accident of the two referents, or is it a theorem about the carrier?
  12
  13It is a theorem about the carrier.
  14
  15## STRENGTH, in one sentence
  16
  17The impossibility is exactly this conditional and nothing wider: **for any family of
  18bounded complexes whose three counts are the MEASURED four-dimensional Freudenthal cube
  19census at every dilate (the proof samples five, `0` through `4`, and the robustness
  20variant `surface_at_positive_dilates_forces_zero` works from the five positive dilates
  21alone), a letter cost with fixed kind totals whose history over those dilates equals
  22`a * N^3 + e` has `a = e = 0` and all three rates zero, so its
  23history cost is identically zero at every complex and every cap** (`surface_and_kindTotals_force_zero`,
  24`surface_and_fixedKindTotals_force_zero_historyCost`).  Four things are worth reading off
  25that sentence before anything else.
  26
  27* **Gauge equivariance is not used.**  It appears in neither the statement nor the proof,
  28  so the theorem holds on the strictly wider class of costs that are not equivariant
  29  (`equivariance_is_not_load_bearing`, with a non-equivariant witness inside the
  30  hypothesis class).  Hypothesis (i) of the question as posed is free.
  31* **The three atom normalizations are not assumed, they are derived**
  32  (`atom_normalizations_are_derived`).  That is the sharpening over the kernel theorem
  33  `Gap2PostingCostDerivation.fixedKindTotals_and_atoms_force_zero_historyCost`, which
  34  needs `NormalizedAtTheAtoms` in its binders.  Bulk cancellation on the dilate family
  35  replaces it, and does so without leaning on the family's degenerate member
  36  (`surface_at_positive_dilates_forces_zero` uses only `N` in `1..5`).
  37* **The letter cost is NOT forced to zero, and saying otherwise would be false.**  The
  38  fibre over the zero history cost is infinite: `centeredIncidenceCost t` is equivariant,
  39  has fixed kind totals, is bulk-cancelling in the sharp sense, and is a nonzero letter
  40  cost for every nonzero `t` (`the_letter_level_fibre_is_not_a_point`).  What is forced
  41  is everything the weight can see.
  42* **What the impossibility buys is the measure.**  Under (ii) and (iii) the Boltzmann
  43  numerator is identically one, so the posted weight is exactly the reciprocal order of
  44  the alphabet's sort-respecting gauge group and the class measure is exactly `mu`
  45  (`the_measure_is_exactly_the_gauge_divisor`).  The cost layer contributes no factor, and
  46  the rate-derivation route through this class of costs is closed.
  47
  48## Which hypothesis does the work, measured
  49
  50Three load-bearing checks, each a kernel-checked countermodel where one exists.
  51
  52* **(iii) fixed kind totals is load-bearing.**  `surfaceCost t` is equivariant, its history
  53  on every census family is exactly `t * N^3` (a pure surface term, `a = t`), it is not
  54  zero, and it has no fixed kind totals (`fixed_kind_totals_is_load_bearing`).  Its
  55  physical counterpart is A1.6's oriented-face cost, whose MEASURED total on the real
  56  carrier is exactly `48 N^3`; `surfaceCost` is the synthetic member of the same hypothesis
  57  class that makes the check kernel-checked rather than measured.
  58* **(ii) bulk cancellation is load-bearing.**  `kindRateCost 1 0 0`, which charges every
  59  vertex letter one unit, is equivariant, has fixed kind totals, has nonzero history cost,
  60  and by the headline itself cannot be bulk-cancelling on any census family
  61  (`bulk_cancellation_is_load_bearing`).
  62* **(i) gauge equivariance is NOT load-bearing.**  There is no countermodel to exhibit,
  63  because the theorem is proved without the hypothesis.  What is exhibited instead is that
  64  dropping it genuinely widens the class rather than being vacuous: `indexTiltCost t` has
  65  fixed kind totals, is bulk-cancelling, is a nonzero letter cost, and is not equivariant.
  66
  67## Where the boundary of (ii) actually sits, and it is sharp
  68
  69Bulk cancellation in the loose sense, "the leading term vanishes", does **not** force the
  70cost to zero.  `kindRateCost 1 0 (-(1/24))` charges each vertex one unit and each Kuhn
  714-simplex `-1/24`, its total on the census family is `4N^3 + 6N^2 + 4N + 1`, and its
  72leading coefficient is exactly zero (`purity_of_the_surface_term_is_load_bearing`).  So it
  73is not the absence of a bulk term that kills, it is the *purity* of what is left.
  74
  75Purity has an exact width, and the module measures both sides of it.  A surface term plus
  76an additive corner constant dies (`surface_and_kindTotals_force_zero`).  A surface term
  77plus an area term with no constant dies too (`surfaceArea_and_kindTotals_force_zero`).
  78Their union does not: rates `(1, -1, 7/12)` give the total `-24N^3 - 12N^2 + 1`, which is
  79bulk-free and linear-term-free and still nonzero (`the_two_relaxations_cannot_be_combined`).
  80So "surface plus constant" and "surface plus area" are each maximal, and no wider form of
  81(ii) supports the theorem.
  82
  83## Why the census does it, in A1.6's own language
  84
  85The finite-complex argument above is a linear system at five dilates, and the reason it is
  86nonsingular is the geometry A1.6 already computed.  `surface_moment_forces_zero_rates`
  87states the same fact in moment coordinates: a rational triple of kind rates whose census
  88combination is the pure surface moment vector `(0, a, 0, 0, 0)` has `a = 0` and all three
  89rates zero.  Its `a = 0` half is exactly
  90`Gap2OrientedFaceSpan.no_pure_surface_term_in_census_span`, the corollary A1.6 drew from
  91computing the census span as a hyperplane; the remaining half is that the three census
  92columns are linearly independent (`census4_columns_independent`), which is why zero
  93moments force zero rates rather than leaving a kernel.
  94
  95## Scope
  96
  97The verdict is about letter costs on the Freudenthal carrier, over families realizing the
  98four-dimensional Kuhn cube census, with bulk cancellation read in A1.6's sharp
  99quantitative form.  It does not say a substrate must charge this way, and it does not
 100touch flag 8 or any other flag.  The census counts are imported from A1.5's MEASURED
 101moment vectors and tied to them by theorem (`censusV_eq_moments` and its two siblings), so
 102no number is re-entered by hand.
 103
 104Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
 105-/
 106
 107namespace IndisputableMonolith
 108namespace Gravity
 109namespace SevenGaps
 110namespace Gap2LetterCostDichotomy
 111
 112open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
 113open GaugeHistoryMeasure Gap2SizeBlindnessReach Gap2PostingCostDerivation
 114open Gap2JEhrhartSpan Gap2OrientedFaceSpan
 115
 116variable {B : ℕ}
 117
 118/-! ## §1. The census of the four-dimensional Freudenthal cube dilate
 119
 120The three counts of the dilate at side `N`, as integers, together with the theorems tying
 121them to A1.5's MEASURED moment vectors.  Nothing here is a new measurement: `mV4`, `mE4`
 122and `mT4` are imported, and the three lemmas below are the only place the closed forms
 123appear. -/
 124
 125/-- Vertex census of the four-dimensional cube dilate, `(N+1)^4`. -/
 126def censusV (N : ℕ) : ℕ := (N + 1) ^ 4
 127
 128/-- Edge census of the four-dimensional cube dilate over the fifteen displacement classes,
 129`(2N+1)^4 - (N+1)^4`. -/
 130def censusE (N : ℕ) : ℕ := 15 * N ^ 4 + 28 * N ^ 3 + 18 * N ^ 2 + 4 * N
 131
 132/-- Kuhn 4-simplex census of the four-dimensional cube dilate, `24 N^4`. -/
 133def censusT (N : ℕ) : ℕ := 24 * N ^ 4
 134
 135/-- Evaluate a moment vector in the basis `(N^4, N^3, N^2, N, 1)`. -/
 136def evalMoments (m : Fin 5 → ℚ) (N : ℕ) : ℚ :=
 137  m 0 * (N : ℚ) ^ 4 + m 1 * (N : ℚ) ^ 3 + m 2 * (N : ℚ) ^ 2 + m 3 * (N : ℚ) + m 4
 138
 139theorem censusV_eq_moments (N : ℕ) : (censusV N : ℚ) = evalMoments mV4 N := by
 140  simp only [censusV, evalMoments, mV4, Matrix.cons_val_zero, Matrix.cons_val_one,
 141    Matrix.head_cons, Matrix.cons_val_two, Matrix.tail_cons, Matrix.cons_val_three,
 142    Matrix.cons_val_four]
 143  push_cast
 144  ring
 145
 146theorem censusE_eq_moments (N : ℕ) : (censusE N : ℚ) = evalMoments mE4 N := by
 147  simp only [censusE, evalMoments, mE4, Matrix.cons_val_zero, Matrix.cons_val_one,
 148    Matrix.head_cons, Matrix.cons_val_two, Matrix.tail_cons, Matrix.cons_val_three,
 149    Matrix.cons_val_four]
 150  push_cast
 151  ring
 152
 153theorem censusT_eq_moments (N : ℕ) : (censusT N : ℚ) = evalMoments mT4 N := by
 154  simp only [censusT, evalMoments, mT4, Matrix.cons_val_zero, Matrix.cons_val_one,
 155    Matrix.head_cons, Matrix.cons_val_two, Matrix.tail_cons, Matrix.cons_val_three,
 156    Matrix.cons_val_four]
 157  push_cast
 158  ring
 159
 160theorem censusV_pos (N : ℕ) : 0 < censusV N := by
 161  unfold censusV
 162  exact pow_pos (Nat.succ_pos N) 4
 163
 164/-! ## §2. A dilate family, and the fact that there is one
 165
 166A `CensusDilateFamily` is a family of bounded complexes whose three counts follow the
 167census.  The impossibility below quantifies over every such family, so it is stronger the
 168larger that class is, and `flatFamily` records that the class is not empty.  The
 169incidence data of `flatFamily` is deliberately trivial: what the theorem reads off a
 170family is its census, and nothing else. -/
 171
 172/-- A family of bounded complexes realizing the four-dimensional Freudenthal cube census
 173at every dilate. -/
 174structure CensusDilateFamily where
 175  cap : ℕ → ℕ
 176  K : ∀ N : ℕ, BoundedComplex (cap N)
 177  nV_eq : ∀ N : ℕ, (K N).nV = censusV N
 178  nE_eq : ∀ N : ℕ, (K N).nE = censusE N
 179  nT_eq : ∀ N : ℕ, (K N).nT = censusT N
 180
 181/-- A cap large enough for all three census counts at side `N`. -/
 182def flatCap (N : ℕ) : ℕ := censusV N + censusE N + censusT N
 183
 184/-- A complex with the census counts and no incidence content. -/
 185def flatComplex (N : ℕ) : BoundedComplex (flatCap N) where
 186  nV := censusV N
 187  nE := censusE N
 188  nT := censusT N
 189  hV := by unfold flatCap; omega
 190  hE := by unfold flatCap; omega
 191  hT := by unfold flatCap; omega
 192  edgeVerts := fun _ => (⟨0, censusV_pos N⟩, ⟨0, censusV_pos N⟩)
 193  tetVerts := fun _ _ => ⟨0, censusV_pos N⟩
 194
 195/-- **Non-vacuity of the hypothesis class.**  A census dilate family exists. -/
 196def flatFamily : CensusDilateFamily where
 197  cap := flatCap
 198  K := flatComplex
 199  nV_eq := fun _ => rfl
 200  nE_eq := fun _ => rfl
 201  nT_eq := fun _ => rfl
 202
 203/-! ## §3. Bulk cancellation, in A1.6's sharp quantitative form
 204
 205A1.6 measured that the oriented-face cost on the four-dimensional cube dilate is exactly
 206`48 N^3`, and called that bulk cancellation in its sharpest quantitative form: the total
 207is a pure surface functional of the side.  `SurfaceTotal` states that condition, with an
 208additive corner constant allowed, since forbidding one would be a hypothesis nobody has a
 209reason to impose.  `SurfaceAreaTotal` is the other maximal relaxation, an area term
 210allowed and no constant. -/
 211
 212/-- **Bulk cancellation, sharp form.**  The history cost over the dilate at side `N` is a
 213pure surface term plus at most an additive corner constant. -/
 214def SurfaceTotal (F : CensusDilateFamily) (c : LetterCost) (a e : ℝ) : Prop :=
 215  ∀ N : ℕ, historyCost c (F.cap N) (F.K N) = a * (N : ℝ) ^ 3 + e
 216
 217/-- **Bulk cancellation, the other maximal relaxation.**  Surface plus area, no constant. -/
 218def SurfaceAreaTotal (F : CensusDilateFamily) (c : LetterCost) (a b : ℝ) : Prop :=
 219  ∀ N : ℕ, historyCost c (F.cap N) (F.K N) = a * (N : ℝ) ^ 3 + b * (N : ℝ) ^ 2
 220
 221/-- The history cost of a cost with fixed kind totals, on a census family, in the census
 222counts.  This is the only bridge between the cost layer and the carrier. -/
 223theorem historyCost_on_family {c : LetterCost} {cV cE cT : ℝ}
 224    (h : KindTotalRates c cV cE cT) (F : CensusDilateFamily) (N : ℕ) :
 225    historyCost c (F.cap N) (F.K N)
 226      = cV * (censusV N : ℝ) + cE * (censusE N : ℝ) + cT * (censusT N : ℝ) := by
 227  rw [historyCost_of_kindTotalRates h (F.cap N) (F.K N), F.nV_eq, F.nE_eq, F.nT_eq]
 228
 229/-! ## §4. The headline: the three conditions force the history cost to zero -/
 230
 231/-- **THE IMPOSSIBILITY.**  On any family realizing the four-dimensional Freudenthal cube
 232census, a letter cost with fixed kind totals whose history over the dilates is a pure
 233surface term plus a constant has all three rates zero, zero surface coefficient, and zero
 234constant.
 235
 236Gauge equivariance is absent from the statement and from the proof.  The three atom
 237normalizations are absent too: `e = 0` is a conclusion, not a binder. -/
 238theorem surface_and_kindTotals_force_zero (F : CensusDilateFamily) {c : LetterCost}
 239    {cV cE cT a e : ℝ} (hk : KindTotalRates c cV cE cT) (hs : SurfaceTotal F c a e) :
 240    cV = 0 ∧ cE = 0 ∧ cT = 0 ∧ a = 0 ∧ e = 0 := by
 241  have key : ∀ N : ℕ,
 242      cV * (censusV N : ℝ) + cE * (censusE N : ℝ) + cT * (censusT N : ℝ)
 243        = a * (N : ℝ) ^ 3 + e := by
 244    intro N
 245    rw [← historyCost_on_family hk F N]
 246    exact hs N
 247  have h0 := key 0
 248  have h1 := key 1
 249  have h2 := key 2
 250  have h3 := key 3
 251  have h4 := key 4
 252  norm_num [censusV, censusE, censusT] at h0 h1 h2 h3 h4
 253  exact ⟨by linarith, by linarith, by linarith, by linarith, by linarith⟩
 254
 255/-- **The degenerate member of the family is not doing the work.**  The same conclusion
 256follows from the surface form at the five positive dilates `1..5` alone, so nobody can read
 257the theorem as the atom normalizations smuggled in through `N = 0`, whose complex is the
 258vertex atom. -/
 259theorem surface_at_positive_dilates_forces_zero (F : CensusDilateFamily) {c : LetterCost}
 260    {cV cE cT a e : ℝ} (hk : KindTotalRates c cV cE cT)
 261    (hs : ∀ N : ℕ, 1 ≤ N → historyCost c (F.cap N) (F.K N) = a * (N : ℝ) ^ 3 + e) :
 262    cV = 0 ∧ cE = 0 ∧ cT = 0 ∧ a = 0 ∧ e = 0 := by
 263  have key : ∀ N : ℕ, 1 ≤ N →
 264      cV * (censusV N : ℝ) + cE * (censusE N : ℝ) + cT * (censusT N : ℝ)
 265        = a * (N : ℝ) ^ 3 + e := by
 266    intro N hN
 267    rw [← historyCost_on_family hk F N]
 268    exact hs N hN
 269  have h1 := key 1 (by norm_num)
 270  have h2 := key 2 (by norm_num)
 271  have h3 := key 3 (by norm_num)
 272  have h4 := key 4 (by norm_num)
 273  have h5 := key 5 (by norm_num)
 274  norm_num [censusV, censusE, censusT] at h1 h2 h3 h4 h5
 275  exact ⟨by linarith, by linarith, by linarith, by linarith, by linarith⟩
 276
 277/-- **The other maximal relaxation dies too.**  Surface plus area, with no constant
 278allowed, forces every coefficient to zero. -/
 279theorem surfaceArea_and_kindTotals_force_zero (F : CensusDilateFamily) {c : LetterCost}
 280    {cV cE cT a b : ℝ} (hk : KindTotalRates c cV cE cT) (hs : SurfaceAreaTotal F c a b) :
 281    cV = 0 ∧ cE = 0 ∧ cT = 0 ∧ a = 0 ∧ b = 0 := by
 282  have key : ∀ N : ℕ,
 283      cV * (censusV N : ℝ) + cE * (censusE N : ℝ) + cT * (censusT N : ℝ)
 284        = a * (N : ℝ) ^ 3 + b * (N : ℝ) ^ 2 := by
 285    intro N
 286    rw [← historyCost_on_family hk F N]
 287    exact hs N
 288  have h0 := key 0
 289  have h1 := key 1
 290  have h2 := key 2
 291  have h3 := key 3
 292  have h4 := key 4
 293  norm_num [censusV, censusE, censusT] at h0 h1 h2 h3 h4
 294  exact ⟨by linarith, by linarith, by linarith, by linarith, by linarith⟩
 295
 296/-- **The history cost is identically zero, at every complex and every cap.**  Not only on
 297the family: three rates pinned to zero pin the whole linear functional. -/
 298theorem surface_and_fixedKindTotals_force_zero_historyCost (F : CensusDilateFamily)
 299    {c : LetterCost} {a e : ℝ} (h : FixedKindTotals c) (hs : SurfaceTotal F c a e)
 300    (B : ℕ) (K : BoundedComplex B) : historyCost c B K = 0 := by
 301  obtain ⟨cV, cE, cT, hk⟩ := h
 302  obtain ⟨hV, hE, hT, _, _⟩ := surface_and_kindTotals_force_zero F hk hs
 303  rw [historyCost_of_kindTotalRates hk B K, hV, hE, hT]
 304  ring
 305
 306/-- **The content of the impossibility: the measure is exactly the gauge divisor.**  The
 307Boltzmann numerator is identically one, the posted weight is the reciprocal order of the
 308alphabet's sort-respecting gauge group, and the class measure is `mu`.  The cost layer
 309contributes no factor, so no rate can be read off it. -/
 310theorem the_measure_is_exactly_the_gauge_divisor (F : CensusDilateFamily) {c : LetterCost}
 311    {a e : ℝ} (h : FixedKindTotals c) (hs : SurfaceTotal F c a e)
 312    (B : ℕ) (K : BoundedComplex B) :
 313    Real.exp (-(historyCost c B K)) = 1
 314      ∧ postedWeight c B K = gibbsWeight K
 315      ∧ postedWeight c B K = 1 / (Nat.card (AlphabetGauge K) : ℝ)
 316      ∧ classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K := by
 317  have hz : ∀ (B' : ℕ) (K' : BoundedComplex B'), historyCost c B' K' = 0 :=
 318    fun B' K' => surface_and_fixedKindTotals_force_zero_historyCost F h hs B' K'
 319  have hgib : ∀ (B' : ℕ) (K' : BoundedComplex B'), postedWeight c B' K' = gibbsWeight K' := by
 320    intro B' K'
 321    unfold postedWeight
 322    rw [hz B' K', neg_zero, Real.exp_zero, one_mul]
 323  refine ⟨by rw [hz B K, neg_zero, Real.exp_zero], hgib B K, ?_, ?_⟩
 324  · rw [hgib B K, gibbsWeight_eq_inv_card_alphabetGauge]
 325  · have hfun : postedWeight c B = fun K' : BoundedComplex B => gibbsWeight K' := by
 326      funext K'
 327      exact hgib B K'
 328    rw [hfun]
 329    exact classMass_gibbsWeight_eq_mu K
 330
 331/-- **The atom normalizations are derived, not assumed.**  This is the sharpening over
 332`Gap2PostingCostDerivation.fixedKindTotals_and_atoms_force_zero_historyCost`, which needs
 333`NormalizedAtTheAtoms` in its binders and gets the same conclusion.  Bulk cancellation on
 334the dilate family does that job instead. -/
 335theorem atom_normalizations_are_derived (F : CensusDilateFamily) {c : LetterCost}
 336    {a e : ℝ} (h : FixedKindTotals c) (hs : SurfaceTotal F c a e) :
 337    NormalizedAtTheAtoms (postedWeight c) := by
 338  intro B' K' hv hi
 339  rw [(the_measure_is_exactly_the_gauge_divisor F h hs B' K').2.1]
 340  exact gibbsWeight_eq_one_at_atoms K' hv hi
 341
 342/-! ## §5. The same fact in A1.6's moment coordinates
 343
 344The linear system at five dilates is nonsingular for a reason A1.6 computed: the census
 345span is the hyperplane the obstruction functional annihilates, so no pure surface term is
 346in it, and the three census columns are independent, so zero moments force zero rates. -/
 347
 348/-- The three census columns are linearly independent over the rationals.  Read off the
 349constant, linear and leading strata in that order. -/
 350theorem census4_columns_independent {cV cE cT : ℚ}
 351    (h : ∀ i : Fin 5, cV * mV4 i + cE * mE4 i + cT * mT4 i = 0) :
 352    cV = 0 ∧ cE = 0 ∧ cT = 0 := by
 353  have h4 := h 4
 354  have h3 := h 3
 355  have h0 := h 0
 356  simp [mV4, mE4, mT4] at h0 h3 h4
 357  refine ⟨h4, ?_, ?_⟩ <;> linarith
 358
 359/-- **THE IMPOSSIBILITY, in moment coordinates.**  A rational triple of kind rates whose
 360census combination is a pure surface moment vector has zero surface coefficient and zero
 361rates.  The first half is exactly A1.6's `no_pure_surface_term_in_census_span`; the second
 362is column independence. -/
 363theorem surface_moment_forces_zero_rates {cV cE cT a : ℚ}
 364    (h : ∀ i : Fin 5,
 365      cV * mV4 i + cE * mE4 i + cT * mT4 i = (![0, a, 0, 0, 0] : Fin 5 → ℚ) i) :
 366    cV = 0 ∧ cE = 0 ∧ cT = 0 ∧ a = 0 := by
 367  have ha : a = 0 := by
 368    by_contra hne
 369    refine no_pure_surface_term_in_census_span a hne ⟨cV, cE, cT, 0, ?_⟩
 370    intro i
 371    rw [zero_mul, add_zero]
 372    exact h i
 373  subst ha
 374  have hz : ∀ i : Fin 5, cV * mV4 i + cE * mE4 i + cT * mT4 i = 0 := by
 375    intro i
 376    rw [h i]
 377    fin_cases i <;> simp
 378  obtain ⟨hV, hE, hT⟩ := census4_columns_independent hz
 379  exact ⟨hV, hE, hT, rfl⟩
 380
 381/-! ## §6. The load-bearing checks
 382
 383One countermodel per hypothesis that has one, and for the hypothesis that has none, the
 384measurement that its absence widens the class rather than emptying it. -/
 385
 386/-- The letter cost charging the three fixed rates, one per kind. -/
 387def kindRateCost (cV cE cT : ℝ) : LetterCost := fun _ _ a =>
 388  match a with
 389  | Sum.inl _ => cV
 390  | Sum.inr (Sum.inl _) => cE
 391  | Sum.inr (Sum.inr _) => cT
 392
 393theorem kindRateCost_kindRates (cV cE cT : ℝ) :
 394    KindRates (kindRateCost cV cE cT) cV cE cT :=
 395  fun _ _ => ⟨fun _ => rfl, fun _ => rfl, fun _ => rfl⟩
 396
 397theorem kindRateCost_kindOnly (cV cE cT : ℝ) : KindOnly (kindRateCost cV cE cT) :=
 398  ⟨cV, cE, cT, kindRateCost_kindRates cV cE cT⟩
 399
 400theorem kindRateCost_equivariant (cV cE cT : ℝ) : Equivariant (kindRateCost cV cE cT) :=
 401  kindOnly_equivariant (kindRateCost_kindOnly cV cE cT)
 402
 403theorem kindRateCost_fixedKindTotals (cV cE cT : ℝ) :
 404    FixedKindTotals (kindRateCost cV cE cT) :=
 405  kindOnly_fixedKindTotals (kindRateCost_kindOnly cV cE cT)
 406
 407theorem historyCost_kindRateCost_on_family (cV cE cT : ℝ) (F : CensusDilateFamily)
 408    (N : ℕ) :
 409    historyCost (kindRateCost cV cE cT) (F.cap N) (F.K N)
 410      = cV * (censusV N : ℝ) + cE * (censusE N : ℝ) + cT * (censusT N : ℝ) :=
 411  historyCost_on_family (kindRates_kindTotalRates (kindRateCost_kindRates cV cE cT)) F N
 412
 413theorem historyCost_kindRateCost_dust_one (cV cE cT : ℝ) :
 414    historyCost (kindRateCost cV cE cT) 1 (dust 1) = cV := by
 415  rw [historyCost_of_kindRates (kindRateCost_kindRates cV cE cT) 1 (dust 1)]
 416  simp
 417
 418/-- **(ii) is load-bearing.**  The cost charging one unit per vertex letter is equivariant,
 419has fixed kind totals, and has nonzero history cost, so it satisfies (i) and (iii) and
 420fails only (ii).  That it fails (ii) on every census family is the headline read
 421backwards: were it bulk-cancelling, its vertex rate would be zero. -/
 422theorem bulk_cancellation_is_load_bearing (F : CensusDilateFamily) :
 423    Equivariant (kindRateCost 1 0 0)
 424      ∧ FixedKindTotals (kindRateCost 1 0 0)
 425      ∧ historyCost (kindRateCost 1 0 0) 1 (dust 1) ≠ 0
 426      ∧ ¬ ∃ a e : ℝ, SurfaceTotal F (kindRateCost 1 0 0) a e := by
 427  refine ⟨kindRateCost_equivariant 1 0 0, kindRateCost_fixedKindTotals 1 0 0, ?_, ?_⟩
 428  · rw [historyCost_kindRateCost_dust_one]
 429    norm_num
 430  · rintro ⟨a, e, hs⟩
 431    obtain ⟨hV, _, _, _, _⟩ :=
 432      surface_and_kindTotals_force_zero F (kindRates_kindTotalRates
 433        (kindRateCost_kindRates 1 0 0)) hs
 434    norm_num at hV
 435
 436/-- **The purity of the surface term is load-bearing, not the absence of a bulk term.**
 437Charging each vertex one unit and each Kuhn 4-simplex `-1/24` gives a total whose leading
 438coefficient is exactly zero, and the cost is equivariant, has fixed kind totals, and is
 439nonzero.  So (ii) read loosely as "the bulk cancels" does not decide the question; only the
 440sharp form does. -/
 441theorem purity_of_the_surface_term_is_load_bearing (F : CensusDilateFamily) :
 442    Equivariant (kindRateCost 1 0 (-(1/24)))
 443      ∧ FixedKindTotals (kindRateCost 1 0 (-(1/24)))
 444      ∧ historyCost (kindRateCost 1 0 (-(1/24))) 1 (dust 1) ≠ 0
 445      ∧ ∀ N : ℕ, historyCost (kindRateCost 1 0 (-(1/24))) (F.cap N) (F.K N)
 446          = 4 * (N : ℝ) ^ 3 + 6 * (N : ℝ) ^ 2 + 4 * (N : ℝ) + 1 := by
 447  refine ⟨kindRateCost_equivariant _ _ _, kindRateCost_fixedKindTotals _ _ _, ?_, ?_⟩
 448  · rw [historyCost_kindRateCost_dust_one]
 449    norm_num
 450  · intro N
 451    rw [historyCost_kindRateCost_on_family]
 452    simp only [censusV, censusE, censusT]
 453    push_cast
 454    ring
 455
 456/-- **The two relaxations of (ii) cannot be combined.**  Rates `(1, -1, 7/12)` give the
 457total `-24N^3 - 12N^2 + 1`: no bulk term, no linear term, a surface term, an area term and
 458a constant, and the rates are not zero.  So "surface plus constant" and "surface plus
 459area" are each maximal, and their union supports no theorem. -/
 460theorem the_two_relaxations_cannot_be_combined (F : CensusDilateFamily) :
 461    Equivariant (kindRateCost 1 (-1) (7/12))
 462      ∧ FixedKindTotals (kindRateCost 1 (-1) (7/12))
 463      ∧ historyCost (kindRateCost 1 (-1) (7/12)) 1 (dust 1) ≠ 0
 464      ∧ ∀ N : ℕ, historyCost (kindRateCost 1 (-1) (7/12)) (F.cap N) (F.K N)
 465          = (-24) * (N : ℝ) ^ 3 + (-12) * (N : ℝ) ^ 2 + 1 := by
 466  refine ⟨kindRateCost_equivariant _ _ _, kindRateCost_fixedKindTotals _ _ _, ?_, ?_⟩
 467  · rw [historyCost_kindRateCost_dust_one]
 468    norm_num
 469  · intro N
 470    rw [historyCost_kindRateCost_on_family]
 471    simp only [censusV, censusE, censusT]
 472    push_cast
 473    ring
 474
 475/-! ### (iii): a nonzero equivariant cost whose total is a pure surface term
 476
 477The physical witness for this slot is A1.6's oriented-face cost, whose total on the real
 478carrier is MEASURED to be exactly `48 N^3`.  A measurement is not a kernel check, so what
 479stands here is a synthetic member of the same hypothesis class: a cost that reads the side
 480of the region off the vertex census and charges the surface it implies. -/
 481
 482/-- The side of a cube dilate, recovered from its vertex census. -/
 483def sideOf (n : ℕ) : ℕ := Nat.sqrt (Nat.sqrt n) - 1
 484
 485theorem sideOf_censusV (N : ℕ) : sideOf (censusV N) = N := by
 486  have h : censusV N = ((N + 1) ^ 2) ^ 2 := by
 487    unfold censusV
 488    ring
 489  unfold sideOf
 490  rw [h, Nat.sqrt_eq', Nat.sqrt_eq']
 491  omega
 492
 493theorem sideOf_one : sideOf 1 = 0 := by
 494  have h : censusV 0 = 1 := by norm_num [censusV]
 495  have hs := sideOf_censusV 0
 496  rw [h] at hs
 497  exact hs
 498
 499theorem sideOf_sixteen : sideOf 16 = 1 := by
 500  have h : censusV 1 = 16 := by norm_num [censusV]
 501  have hs := sideOf_censusV 1
 502  rw [h] at hs
 503  exact hs
 504
 505noncomputable section
 506
 507/-- The **surface cost**: every vertex letter carries an equal share of a charge that is
 508the cube of the region's side.  Equivariant, since it reads only the vertex count. -/
 509def surfaceCost (t : ℝ) : LetterCost := fun _ K a =>
 510  match a with
 511  | Sum.inl _ => t * (sideOf K.nV : ℝ) ^ 3 / (K.nV : ℝ)
 512  | Sum.inr _ => 0
 513
 514@[simp] theorem surfaceCost_inl (t : ℝ) (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV) :
 515    surfaceCost t B K (Sum.inl v) = t * (sideOf K.nV : ℝ) ^ 3 / (K.nV : ℝ) := rfl
 516
 517@[simp] theorem surfaceCost_edge (t : ℝ) (B : ℕ) (K : BoundedComplex B) (e : Fin K.nE) :
 518    surfaceCost t B K (Sum.inr (Sum.inl e)) = 0 := rfl
 519
 520@[simp] theorem surfaceCost_tet (t : ℝ) (B : ℕ) (K : BoundedComplex B) (τ : Fin K.nT) :
 521    surfaceCost t B K (Sum.inr (Sum.inr τ)) = 0 := rfl
 522
 523theorem vertexBlockSum_surfaceCost (t : ℝ) (B : ℕ) (K : BoundedComplex B)
 524    (h : K.nV ≠ 0) :
 525    (∑ v : Fin K.nV, surfaceCost t B K (Sum.inl v)) = t * (sideOf K.nV : ℝ) ^ 3 := by
 526  classical
 527  have hne : (K.nV : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr h
 528  simp only [surfaceCost_inl, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
 529    nsmul_eq_mul]
 530  field_simp
 531
 532theorem historyCost_surfaceCost (t : ℝ) (B : ℕ) (K : BoundedComplex B) (h : K.nV ≠ 0) :
 533    historyCost (surfaceCost t) B K = t * (sideOf K.nV : ℝ) ^ 3 := by
 534  classical
 535  unfold historyCost
 536  rw [Fintype.sum_sum_type, Fintype.sum_sum_type]
 537  simp only [surfaceCost_edge, surfaceCost_tet, Finset.sum_const_zero, add_zero]
 538  exact vertexBlockSum_surfaceCost t B K h
 539
 540/-- The surface cost is gauge equivariant: it reads only the vertex count, which a
 541relabeling preserves. -/
 542theorem surfaceCost_equivariant (t : ℝ) : Equivariant (surfaceCost t) := by
 543  intro B K K' r a
 544  rcases a with v | (e | τ)
 545  · show surfaceCost t B K' (Sum.inl (r.vEquiv v)) = surfaceCost t B K (Sum.inl v)
 546    rw [surfaceCost_inl, surfaceCost_inl, size_v r]
 547  · rfl
 548  · rfl
 549
 550/-- **The surface cost is bulk-cancelling in the sharp sense, with coefficient `t`.** -/
 551theorem surfaceCost_surfaceTotal (F : CensusDilateFamily) (t : ℝ) :
 552    SurfaceTotal F (surfaceCost t) t 0 := by
 553  intro N
 554  have hne : (F.K N).nV ≠ 0 := by
 555    rw [F.nV_eq N]
 556    exact (censusV_pos N).ne'
 557  rw [historyCost_surfaceCost t (F.cap N) (F.K N) hne, F.nV_eq N, sideOf_censusV N]
 558  ring
 559
 560/-- **The surface cost has no fixed kind totals.**  A single vertex has side zero and
 561costs nothing, which forces the vertex rate to zero; sixteen vertices have side one and
 562cost `t`, which then demands `t = 0`. -/
 563theorem surfaceCost_not_fixedKindTotals {t : ℝ} (ht : t ≠ 0) :
 564    ¬ FixedKindTotals (surfaceCost t) := by
 565  rintro ⟨cV, cE, cT, h⟩
 566  have h1 := (h 1 (dust 1)).1
 567  have h2 := (h 16 (dust 16)).1
 568  rw [vertexBlockSum_surfaceCost t 1 (dust 1) (by simp)] at h1
 569  rw [vertexBlockSum_surfaceCost t 16 (dust 16) (by simp)] at h2
 570  simp only [dust_nV, sideOf_one, sideOf_sixteen, Nat.cast_zero, Nat.cast_one,
 571    Nat.cast_ofNat] at h1 h2
 572  norm_num at h1 h2
 573  exact ht (by linarith)
 574
 575/-- **(iii) is load-bearing.**  A nonzero gauge-equivariant cost whose total on every
 576census family is exactly the pure surface term `t N^3`, and which has no fixed kind
 577totals.  Drop (iii) and the impossibility is false. -/
 578theorem fixed_kind_totals_is_load_bearing (F : CensusDilateFamily) {t : ℝ} (ht : t ≠ 0) :
 579    Equivariant (surfaceCost t)
 580      ∧ SurfaceTotal F (surfaceCost t) t 0
 581      ∧ ¬ FixedKindTotals (surfaceCost t)
 582      ∧ historyCost (surfaceCost t) 16 (dust 16) ≠ 0 := by
 583  refine ⟨surfaceCost_equivariant t, surfaceCost_surfaceTotal F t,
 584    surfaceCost_not_fixedKindTotals ht, ?_⟩
 585  rw [historyCost_surfaceCost t 16 (dust 16) (by simp)]
 586  simp only [dust_nV, sideOf_sixteen, Nat.cast_one, one_pow, mul_one]
 587  exact ht
 588
 589/-! ### (i): equivariance is not load-bearing, and dropping it widens the class
 590
 591There is no countermodel to exhibit here, because the theorem never used the hypothesis.
 592What is worth measuring is that its absence widens the class rather than emptying it: a
 593cost outside it that satisfies (ii) and (iii) and is not zero. -/
 594
 595/-- A cost that charges the first vertex letter the whole of a debt the remaining vertex
 596letters each pay back one unit of.  Every block sum is zero, and the letter it charges
 597depends on the letter's index, so labels are not gauge for it. -/
 598def indexTiltCost (t : ℝ) : LetterCost := fun _ K a =>
 599  match a with
 600  | Sum.inl v => if (v : ℕ) = 0 then t * ((K.nV : ℝ) - 1) else -t
 601  | Sum.inr _ => 0
 602
 603@[simp] theorem indexTiltCost_inl (t : ℝ) (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV) :
 604    indexTiltCost t B K (Sum.inl v)
 605      = if (v : ℕ) = 0 then t * ((K.nV : ℝ) - 1) else -t := rfl
 606
 607@[simp] theorem indexTiltCost_edge (t : ℝ) (B : ℕ) (K : BoundedComplex B) (e : Fin K.nE) :
 608    indexTiltCost t B K (Sum.inr (Sum.inl e)) = 0 := rfl
 609
 610@[simp] theorem indexTiltCost_tet (t : ℝ) (B : ℕ) (K : BoundedComplex B) (τ : Fin K.nT) :
 611    indexTiltCost t B K (Sum.inr (Sum.inr τ)) = 0 := rfl
 612
 613theorem vertexSum_indexTilt (t : ℝ) (n : ℕ) :
 614    (∑ v : Fin n, (if (v : ℕ) = 0 then t * ((n : ℝ) - 1) else -t)) = 0 := by
 615  classical
 616  cases n with
 617  | zero => simp
 618  | succ m =>
 619    rw [Fin.sum_univ_succ]
 620    have hz : ((0 : Fin (m + 1)) : ℕ) = 0 := rfl
 621    have hs : ∀ i : Fin m, ((i.succ : Fin (m + 1)) : ℕ) ≠ 0 := by
 622      intro i
 623      rw [Fin.val_succ]
 624      omega
 625    rw [Finset.sum_congr rfl (fun i (_ : i ∈ Finset.univ) => if_neg (hs i)),
 626      Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
 627    rw [if_pos hz]
 628    push_cast
 629    ring
 630
 631theorem indexTiltCost_kindTotalRates (t : ℝ) : KindTotalRates (indexTiltCost t) 0 0 0 := by
 632  classical
 633  intro B K
 634  refine ⟨?_, ?_, ?_⟩
 635  · simp only [indexTiltCost_inl]
 636    rw [vertexSum_indexTilt t K.nV]
 637    ring
 638  · simp
 639  · simp
 640
 641theorem indexTiltCost_fixedKindTotals (t : ℝ) : FixedKindTotals (indexTiltCost t) :=
 642  ⟨0, 0, 0, indexTiltCost_kindTotalRates t⟩
 643
 644theorem historyCost_indexTiltCost (t : ℝ) (B : ℕ) (K : BoundedComplex B) :
 645    historyCost (indexTiltCost t) B K = 0 := by
 646  rw [historyCost_of_kindTotalRates (indexTiltCost_kindTotalRates t) B K]
 647  ring
 648
 649theorem indexTiltCost_surfaceTotal (F : CensusDilateFamily) (t : ℝ) :
 650    SurfaceTotal F (indexTiltCost t) 0 0 := by
 651  intro N
 652  rw [historyCost_indexTiltCost]
 653  ring
 654
 655/-- The first vertex of the two-point dust. -/
 656def v0Dust2 : Fin (dust 2).nV := ⟨0, by decide⟩
 657
 658/-- The second vertex of the two-point dust. -/
 659def v1Dust2 : Fin (dust 2).nV := ⟨1, by decide⟩
 660
 661/-- Swap the two vertices of the two-point dust.  With no incidence data both commutation
 662conditions are vacuous, so this is a relabeling. -/
 663def swapDust2 : Relabel (dust 2) (dust 2) where
 664  vEquiv := Equiv.swap v0Dust2 v1Dust2
 665  eEquiv := Equiv.refl _
 666  tEquiv := Equiv.refl _
 667  edge_comm := fun e => e.elim0
 668  tet_comm := fun t _ => t.elim0
 669
 670theorem swapDust2_v0 : swapDust2.vEquiv v0Dust2 = v1Dust2 :=
 671  Equiv.swap_apply_left _ _
 672
 673/-- The first vertex letter of the two-point dust is charged `t`. -/
 674theorem indexTiltCost_at_v0 (t : ℝ) :
 675    indexTiltCost t 2 (dust 2) (Sum.inl v0Dust2) = t := by
 676  rw [indexTiltCost_inl]
 677  norm_num [v0Dust2]
 678
 679/-- The second vertex letter of the two-point dust is charged `-t`. -/
 680theorem indexTiltCost_at_v1 (t : ℝ) :
 681    indexTiltCost t 2 (dust 2) (Sum.inl v1Dust2) = -t := by
 682  rw [indexTiltCost_inl]
 683  norm_num [v1Dust2]
 684
 685/-- **The tilt cost is not gauge equivariant.**  Swapping the two vertices of the two-point
 686dust carries a letter charged `t` to a letter charged `-t`. -/
 687theorem indexTiltCost_not_equivariant {t : ℝ} (ht : t ≠ 0) :
 688    ¬ Equivariant (indexTiltCost t) := by
 689  intro h
 690  have hEq := h 2 (dust 2) (dust 2) swapDust2 (Sum.inl v0Dust2)
 691  rw [show postingAlphEquiv swapDust2.vEquiv swapDust2.eEquiv swapDust2.tEquiv
 692      (Sum.inl v0Dust2) = Sum.inl (swapDust2.vEquiv v0Dust2) from rfl, swapDust2_v0,
 693    indexTiltCost_at_v1, indexTiltCost_at_v0] at hEq
 694  exact ht (by linarith)
 695
 696/-- **(i) is not load-bearing, and its absence widens the class.**  The tilt cost has fixed
 697kind totals, is bulk-cancelling in the sharp sense, is a nonzero letter cost, and is not
 698equivariant.  The impossibility applies to it unchanged, which is the point: no
 699countermodel exists for (i) because (i) was never used. -/
 700theorem equivariance_is_not_load_bearing (F : CensusDilateFamily) {t : ℝ} (ht : t ≠ 0) :
 701    FixedKindTotals (indexTiltCost t)
 702      ∧ SurfaceTotal F (indexTiltCost t) 0 0
 703      ∧ ¬ Equivariant (indexTiltCost t)
 704      ∧ indexTiltCost t 2 (dust 2) (Sum.inl v0Dust2) ≠ 0
 705      ∧ ∀ (B : ℕ) (K : BoundedComplex B), historyCost (indexTiltCost t) B K = 0 := by
 706  refine ⟨indexTiltCost_fixedKindTotals t, indexTiltCost_surfaceTotal F t,
 707    indexTiltCost_not_equivariant ht, ?_, historyCost_indexTiltCost t⟩
 708  rw [indexTiltCost_at_v0]
 709  exact ht
 710
 711/-! ## §7. What is NOT forced: the letter-level fibre
 712
 713The question as posed asks for a nonzero letter cost.  Read at the letter, the answer is
 714that one exists and the library already had it, which is why the impossibility above is
 715stated at the history cost and not at the letter.  The centered incidence cost reads
 716incidence at every edge letter, is equivariant, has fixed kind totals, is bulk-cancelling
 717with coefficient zero, and is nonzero.  What it is not is visible to the weight. -/
 718
 719/-- **The fibre over the zero history cost is not a point.**  For every nonzero `t` the
 720centered incidence cost satisfies all three conditions and is a nonzero letter cost, while
 721its history cost is identically zero.  So "no nonzero cost" is false at the letter and true
 722at everything the posted weight can see, and the impossibility must be stated at the
 723history cost. -/
 724theorem the_letter_level_fibre_is_not_a_point (F : CensusDilateFamily) {t : ℝ} (ht : t ≠ 0) :
 725    Equivariant (centeredIncidenceCost t)
 726      ∧ FixedKindTotals (centeredIncidenceCost t)
 727      ∧ SurfaceTotal F (centeredIncidenceCost t) 0 0
 728      ∧ centeredIncidenceCost t 3 loopAndBridge (Sum.inr (Sum.inl ⟨1, by decide⟩)) ≠ 0
 729      ∧ ∀ (B : ℕ) (K : BoundedComplex B), historyCost (centeredIncidenceCost t) B K = 0 := by
 730  refine ⟨centeredIncidenceCost_equivariant t, fixedKindTotals_centeredIncidenceCost t,
 731    ?_, ?_, fun B K => historyCost_centeredIncidenceCost t B K⟩
 732  · intro N
 733    rw [historyCost_centeredIncidenceCost]
 734    ring
 735  · rw [(centeredIncidence_charges_on_loopAndBridge t).2]
 736    exact ht
 737
 738/-! ## §8. Certificate -/
 739
 740/-- **The A1.7 dichotomy verdict.**  The impossibility horn landed, at the history cost and
 741not at the letter.  Every clause below is a theorem of this module or of one it imports. -/
 742structure LetterCostDichotomyVerdict : Prop where
 743  family_exists : True
 744  impossibility : ∀ (F : CensusDilateFamily) (c : LetterCost) (cV cE cT a e : ℝ),
 745    KindTotalRates c cV cE cT → SurfaceTotal F c a e →
 746      cV = 0 ∧ cE = 0 ∧ cT = 0 ∧ a = 0 ∧ e = 0
 747  history_cost_is_zero : ∀ (F : CensusDilateFamily) (c : LetterCost) (a e : ℝ),
 748    FixedKindTotals c → SurfaceTotal F c a e →
 749      ∀ (B : ℕ) (K : BoundedComplex B), historyCost c B K = 0
 750  measure_is_the_divisor : ∀ (F : CensusDilateFamily) (c : LetterCost) (a e : ℝ),
 751    FixedKindTotals c → SurfaceTotal F c a e →
 752      ∀ (B : ℕ) (K : BoundedComplex B),
 753        postedWeight c B K = 1 / (Nat.card (AlphabetGauge K) : ℝ)
 754          ∧ classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K
 755  atoms_derived : ∀ (F : CensusDilateFamily) (c : LetterCost) (a e : ℝ),
 756    FixedKindTotals c → SurfaceTotal F c a e → NormalizedAtTheAtoms (postedWeight c)
 757  positive_dilates_suffice : ∀ (F : CensusDilateFamily) (c : LetterCost) (cV cE cT a e : ℝ),
 758    KindTotalRates c cV cE cT →
 759      (∀ N : ℕ, 1 ≤ N → historyCost c (F.cap N) (F.K N) = a * (N : ℝ) ^ 3 + e) →
 760        cV = 0 ∧ cE = 0 ∧ cT = 0 ∧ a = 0 ∧ e = 0
 761  surface_plus_area_also_dies : ∀ (F : CensusDilateFamily) (c : LetterCost)
 762      (cV cE cT a b : ℝ), KindTotalRates c cV cE cT → SurfaceAreaTotal F c a b →
 763        cV = 0 ∧ cE = 0 ∧ cT = 0 ∧ a = 0 ∧ b = 0
 764  moment_form : ∀ cV cE cT a : ℚ,
 765    (∀ i : Fin 5, cV * mV4 i + cE * mE4 i + cT * mT4 i
 766        = (![0, a, 0, 0, 0] : Fin 5 → ℚ) i) → cV = 0 ∧ cE = 0 ∧ cT = 0 ∧ a = 0
 767  kind_totals_load_bearing : ∀ (F : CensusDilateFamily) (t : ℝ), t ≠ 0 →
 768    Equivariant (surfaceCost t) ∧ SurfaceTotal F (surfaceCost t) t 0
 769      ∧ ¬ FixedKindTotals (surfaceCost t)
 770  bulk_cancellation_load_bearing : ∀ F : CensusDilateFamily,
 771    ¬ ∃ a e : ℝ, SurfaceTotal F (kindRateCost 1 0 0) a e
 772  equivariance_not_load_bearing : ∀ (F : CensusDilateFamily) (t : ℝ), t ≠ 0 →
 773    FixedKindTotals (indexTiltCost t) ∧ SurfaceTotal F (indexTiltCost t) 0 0
 774      ∧ ¬ Equivariant (indexTiltCost t)
 775  purity_is_the_boundary : ∀ F : CensusDilateFamily,
 776    ∀ N : ℕ, historyCost (kindRateCost 1 0 (-(1/24))) (F.cap N) (F.K N)
 777      = 4 * (N : ℝ) ^ 3 + 6 * (N : ℝ) ^ 2 + 4 * (N : ℝ) + 1
 778  relaxations_incompatible : ∀ F : CensusDilateFamily,
 779    ∀ N : ℕ, historyCost (kindRateCost 1 (-1) (7/12)) (F.cap N) (F.K N)
 780      = (-24) * (N : ℝ) ^ 3 + (-12) * (N : ℝ) ^ 2 + 1
 781  letter_fibre_not_a_point : ∀ (F : CensusDilateFamily) (t : ℝ), t ≠ 0 →
 782    Equivariant (centeredIncidenceCost t) ∧ FixedKindTotals (centeredIncidenceCost t)
 783      ∧ SurfaceTotal F (centeredIncidenceCost t) 0 0
 784      ∧ centeredIncidenceCost t 3 loopAndBridge (Sum.inr (Sum.inl ⟨1, by decide⟩)) ≠ 0
 785
 786theorem letterCostDichotomyVerdict : LetterCostDichotomyVerdict where
 787  family_exists := trivial
 788  impossibility := fun F c _ _ _ _ _ hk hs => surface_and_kindTotals_force_zero F hk hs
 789  history_cost_is_zero := fun F c _ _ h hs B K =>
 790    surface_and_fixedKindTotals_force_zero_historyCost F h hs B K
 791  measure_is_the_divisor := fun F c _ _ h hs B K =>
 792    ⟨(the_measure_is_exactly_the_gauge_divisor F h hs B K).2.2.1,
 793      (the_measure_is_exactly_the_gauge_divisor F h hs B K).2.2.2⟩
 794  atoms_derived := fun F c _ _ h hs => atom_normalizations_are_derived F h hs
 795  positive_dilates_suffice := fun F c _ _ _ _ _ hk hs =>
 796    surface_at_positive_dilates_forces_zero F hk hs
 797  surface_plus_area_also_dies := fun F c _ _ _ _ _ hk hs =>
 798    surfaceArea_and_kindTotals_force_zero F hk hs
 799  moment_form := fun _ _ _ _ h => surface_moment_forces_zero_rates h
 800  kind_totals_load_bearing := fun F t ht =>
 801    ⟨(fixed_kind_totals_is_load_bearing F ht).1,
 802      (fixed_kind_totals_is_load_bearing F ht).2.1,
 803      (fixed_kind_totals_is_load_bearing F ht).2.2.1⟩
 804  bulk_cancellation_load_bearing := fun F => (bulk_cancellation_is_load_bearing F).2.2.2
 805  equivariance_not_load_bearing := fun F t ht =>
 806    ⟨(equivariance_is_not_load_bearing F ht).1,
 807      (equivariance_is_not_load_bearing F ht).2.1,
 808      (equivariance_is_not_load_bearing F ht).2.2.1⟩
 809  purity_is_the_boundary := fun F => (purity_of_the_surface_term_is_load_bearing F).2.2.2
 810  relaxations_incompatible := fun F => (the_two_relaxations_cannot_be_combined F).2.2.2
 811  letter_fibre_not_a_point := fun F t ht =>
 812    ⟨(the_letter_level_fibre_is_not_a_point F ht).1,
 813      (the_letter_level_fibre_is_not_a_point F ht).2.1,
 814      (the_letter_level_fibre_is_not_a_point F ht).2.2.1,
 815      (the_letter_level_fibre_is_not_a_point F ht).2.2.2.1⟩
 816
 817/-! ## §9. Flag status
 818
 819Nothing moves.  The impossibility closes a route to a triple of chemical potentials rather
 820than producing one, so there is still nothing to compare against unit fugacity and
 821`gap2_measure_derived` stays exactly as it was.  What the module changes is the frontier:
 822the open question is no longer whether some other imbalance referent escapes, it is whether
 823the substrate forces aggregate linearity by kind at all. -/
 824
 825structure DichotomyIndex : Type where
 826  /-- The dichotomy is decided, and the impossibility horn landed. -/
 827  dichotomy_decided : Bool
 828  /-- The forcing is at the history cost, and the letter cost is NOT forced to zero. -/
 829  forced_at_history_not_at_letter : Bool
 830  /-- Gauge equivariance is absent from the statement and the proof. -/
 831  equivariance_used : Bool
 832  /-- The three atom normalizations are derived rather than assumed. -/
 833  atom_normalizations_derived : Bool
 834  /-- The sharp form of bulk cancellation is exactly maximal: two relaxations, each
 835  maximal, incompatible with each other. -/
 836  boundary_of_bulk_cancellation_measured : Bool
 837  /-- NOT produced: a triple of chemical potentials.  The impossibility closes the route
 838  rather than deriving a rate. -/
 839  triple_derived : Bool
 840  /-- NOT moved. -/
 841  measure_flag_moved : Bool
 842
 843def dichotomyIndex : DichotomyIndex where
 844  dichotomy_decided := true
 845  forced_at_history_not_at_letter := true
 846  equivariance_used := false
 847  atom_normalizations_derived := true
 848  boundary_of_bulk_cancellation_measured := true
 849  triple_derived := false
 850  measure_flag_moved := false
 851
 852theorem index_no_triple : dichotomyIndex.triple_derived = false := rfl
 853
 854theorem index_flag_unmoved : dichotomyIndex.measure_flag_moved = false := rfl
 855
 856theorem index_equivariance_unused : dichotomyIndex.equivariance_used = false := rfl
 857
 858end
 859
 860/-! ## Axiom audit -/
 861
 862#print axioms censusV_eq_moments
 863#print axioms censusE_eq_moments
 864#print axioms censusT_eq_moments
 865#print axioms historyCost_on_family
 866#print axioms surface_and_kindTotals_force_zero
 867#print axioms surface_at_positive_dilates_forces_zero
 868#print axioms surfaceArea_and_kindTotals_force_zero
 869#print axioms surface_and_fixedKindTotals_force_zero_historyCost
 870#print axioms the_measure_is_exactly_the_gauge_divisor
 871#print axioms atom_normalizations_are_derived
 872#print axioms census4_columns_independent
 873#print axioms surface_moment_forces_zero_rates
 874#print axioms bulk_cancellation_is_load_bearing
 875#print axioms purity_of_the_surface_term_is_load_bearing
 876#print axioms the_two_relaxations_cannot_be_combined
 877#print axioms sideOf_censusV
 878#print axioms historyCost_surfaceCost
 879#print axioms surfaceCost_equivariant
 880#print axioms surfaceCost_surfaceTotal
 881#print axioms surfaceCost_not_fixedKindTotals
 882#print axioms fixed_kind_totals_is_load_bearing
 883#print axioms vertexSum_indexTilt
 884#print axioms indexTiltCost_kindTotalRates
 885#print axioms indexTiltCost_not_equivariant
 886#print axioms equivariance_is_not_load_bearing
 887#print axioms the_letter_level_fibre_is_not_a_point
 888#print axioms letterCostDichotomyVerdict
 889
 890end Gap2LetterCostDichotomy
 891end SevenGaps
 892end Gravity
 893end IndisputableMonolith
 894