IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityElimination

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityPostingGluing
   2import IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasure
   3import IndisputableMonolith.Gravity.SevenGaps.Gap2LetterCostDichotomy
   4
   5/-!
   6# Gap 2 / A19 (lane C17): fugacity elimination after the erasure Jacobian
   7
   8## Scoped headline (exact shape; flag 8 unmoved)
   9
  10After the C4 erasure Jacobian, any letter cost whose posted class mass equals `mu`
  11at the three atoms and is representable there by a size-blind weight `sizeWeight f`
  12forces `UnitFugacity f`, so the three sector fugacities collapse.  On the
  13gluing-residue family `characterSize z_V z_E z_T` this is exactly
  14`z_V = z_E = z_T = 1`.  Composed with the erasure Jacobian, the posted class mass
  15equals `mu` with no fugacity freedom on that class.
  16
  17This module does **not** assert flag 8 closed.  Flag 8 still needs numerator
  18triviality for physical costs (the local Boltzmann factor).  `FullTheoryLedger`
  19is not imported.  `measure_flag_moved = false` is rfl-forced below.
  20
  21## What is proved
  22
  23**D1 (elimination, A1.4 class).**  `unit_fugacity_forced_after_erasure`: any letter
  24cost that posts `mu` at the three atoms, with class mass represented there by
  25`sizeWeight f`, forces `UnitFugacity f`.  This is A1.4's
  26`no_posting_countermodel_with_nonunit_fugacity`, named as the mandatory second half
  27after C4's divisor emergence.  Specialization
  28`three_fugacities_collapse_on_posting_mu`: on the gluing closed-form residue
  29`characterSize z_V z_E z_T`, posting `mu` at the atoms forces
  30`z_V = z_E = z_T = 1`.
  31
  32**D2 (widening past atom-named `mu`, A1.7 class).**
  33`unit_fugacity_forced_by_surface_and_kindTotals`: on any census dilate family, a
  34letter cost with fixed kind totals whose dilate history is a pure surface term
  35forces the posted weight to equal `sizeWeight gibbsSize` everywhere, forces
  36`UnitFugacity gibbsSize`, and posts `mu` at every complex.  The atom values of
  37`mu` are derived, not assumed (`atom_normalizations_are_derived`).
  38
  39**D3 (composition).**  `erasure_and_unit_fugacity_compose_to_mu`: for an
  40equivariant letter cost whose posted class mass at the atoms is represented by
  41`sizeWeight f` and equals `mu` there, the erasure Jacobian holds, `UnitFugacity f`
  42holds, and (when the representation extends to every complex and posts `mu`
  43everywhere) the size function is exactly `gibbsSize`, so the posted class mass
  44equals `mu` with no fugacity freedom.
  45
  46## What blocks further widening (deliverable, not a failure)
  47
  481. **Non-`sizeWeight` posting.**  `tiltedCost` posts `mu` everywhere with a
  49   non-unit labeled numerator; its posted weight is not any `sizeWeight`
  50   (`postedWeight_tiltedCost_not_sizeWeight`).  At class-mass level the
  51   representing size function is still `gibbsSize` (unit).  So `UnitFugacity`
  52   as a predicate on a size function does not apply to the labeled weight, and
  53   the local numerator remains free for non-equivariant costs (A1.3).
  542. **Structural conditions without naming `mu`.**  `characterCost` with any
  55   positive non-unit triple is kind-only, equivariant, size-blind, and glues,
  56   yet has non-unit fugacity (`gluing_and_posting_do_not_force_unit_fugacity`).
  57   Posting-layer structure plus gluing cannot supply the elimination; the
  58   load-bearing hypothesis names `mu` at the atoms.
  593. **Costs without fixed kind totals.**  A1.7's escape `surfaceCost t` is
  60   equivariant, bulk-cancelling, and nonzero, with no fixed kind totals.  The
  61   A1.7 widening does not bind that class; the local numerator for physical
  62   costs without kind totals remains open.
  63
  64Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  65-/
  66
  67namespace IndisputableMonolith
  68namespace Gravity
  69namespace SevenGaps
  70namespace Gap2FugacityElimination
  71
  72open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume
  73open Gap2GluingDerivation Gap2PostingCostDerivation Gap2NonEquivariantPosting
  74open Gap2SizeBlindnessReach Gap2FugacityPostingGluing Gap2LabelErasure
  75open Gap2LetterCostDichotomy
  76
  77noncomputable section
  78
  79variable {B : ℕ}
  80
  81/-! ## §1. Elimination on the A1.4 class (after erasure)
  82
  83The panel's locked protocol: once the divisor genuinely emerges (C4), use A1.4
  84to eliminate `z_V, z_E, z_T`.  The content is A1.4's atom-only theorem; the
  85work here is naming it as the second half and specializing to the three-fugacity
  86residue. -/
  87
  88/-- **C17 elimination (A1.4 class).**  After the erasure Jacobian, any letter cost
  89that posts the derived base measure `mu` at the three atoms, and whose posted
  90class mass there is represented by a size-blind weight `sizeWeight f`, forces
  91unit sector fugacity on `f`.  Equivariant or not, kind-only or not, gluing or
  92not.  The class on the theorem's face: atom-only posting of `mu`, plus
  93`sizeWeight`-representability of the class mass at those atoms. -/
  94theorem unit_fugacity_forced_after_erasure (c : LetterCost) (f : ℕ → ℕ → ℕ → ℝ)
  95    (hpost : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
  96      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K)
  97    (hrep : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
  98      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K)
  99        = classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K)) :
 100    UnitFugacity f :=
 101  no_posting_countermodel_with_nonunit_fugacity c f hpost hrep
 102
 103/-- **Specialization to the three fugacities.**  The gluing derivation's closed-form
 104residue is `characterSize z_V z_E z_T`.  Posting `mu` at the three atoms forces
 105`z_V = z_E = z_T = 1`.  This is the literal elimination of the three fugacities
 106named in the C4 surviving-freedom headline. -/
 107theorem three_fugacities_collapse_on_posting_mu {zV zE zT : ℝ}
 108    (_hzV : 0 < zV) (_hzE : 0 < zE) (_hzT : 0 < zT)
 109    (hpost : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 110      classMass (sizeWeight (characterSize zV zE zT))
 111        (Quotient.mk (relabelSetoid B') K) = mu K) :
 112    zV = 1 ∧ zE = 1 ∧ zT = 1 := by
 113  have hUF : UnitFugacity (characterSize zV zE zT) :=
 114    posts_mu_at_atoms_forces_unit_fugacity (characterSize zV zE zT) hpost
 115  exact unitFugacity_characterSize_iff.mp hUF
 116
 117/-- Same elimination, transported through the character cost's posted weight. -/
 118theorem three_fugacities_collapse_via_characterCost {zV zE zT : ℝ}
 119    (hzV : 0 < zV) (hzE : 0 < zE) (hzT : 0 < zT)
 120    (hpost : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 121      classMass (postedWeight (characterCost zV zE zT) B')
 122        (Quotient.mk (relabelSetoid B') K) = mu K) :
 123    zV = 1 ∧ zE = 1 ∧ zT = 1 := by
 124  have hrep : ∀ (B' : ℕ) (K : BoundedComplex B'),
 125      classMass (postedWeight (characterCost zV zE zT) B')
 126          (Quotient.mk (relabelSetoid B') K)
 127        = classMass (sizeWeight (characterSize zV zE zT))
 128          (Quotient.mk (relabelSetoid B') K) := by
 129    intro B' K
 130    rw [postedWeight_characterCost_eq hzV hzE hzT B']
 131  have hUF : UnitFugacity (characterSize zV zE zT) :=
 132    unit_fugacity_forced_after_erasure (characterCost zV zE zT) (characterSize zV zE zT)
 133      (fun B' K hv hi => hpost B' K hv hi)
 134      (fun B' K hv hi => hrep B' K)
 135  exact unitFugacity_characterSize_iff.mp hUF
 136
 137/-! ## §2. Widening: A1.7 forces unit fugacity without naming `mu` at the atoms -/
 138
 139/-- **Widening past A1.4's atom-named `mu` hypothesis.**  On any census dilate
 140family, fixed kind totals plus surface-pure dilate history force the posted weight
 141to equal `sizeWeight gibbsSize` at every complex, force `UnitFugacity gibbsSize`,
 142and post `mu` everywhere.  Strength, exactly: the `UnitFugacity gibbsSize` conjunct
 143is free once the posted weight is forced to `sizeWeight gibbsSize`
 144(`gibbsSize_unitFugacity` uses no binders); what the binders buy is A1.7's
 145posted-weight and class-mass forcing.  The three atom values of `mu` are derived
 146(`atom_normalizations_are_derived`), not assumed.  Class on the face:
 147`FixedKindTotals` + `SurfaceTotal` on a `CensusDilateFamily`. -/
 148theorem unit_fugacity_forced_by_surface_and_kindTotals
 149    (F : CensusDilateFamily) {c : LetterCost} {a e : ℝ}
 150    (h : FixedKindTotals c) (hs : SurfaceTotal F c a e) :
 151    UnitFugacity gibbsSize
 152      ∧ (∀ (B' : ℕ) (K : BoundedComplex B'),
 153          postedWeight c B' K = sizeWeight gibbsSize K)
 154      ∧ (∀ (B' : ℕ) (K : BoundedComplex B'),
 155          classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K) := by
 156  refine ⟨gibbsSize_unitFugacity, ?_, ?_⟩
 157  · intro B' K
 158    have hgib := (the_measure_is_exactly_the_gauge_divisor F h hs B' K).2.1
 159    rw [hgib, gibbsWeight_eq_gibbsSize]
 160    rfl
 161  · intro B' K
 162    exact (the_measure_is_exactly_the_gauge_divisor F h hs B' K).2.2.2
 163
 164/-- Corollary: the A1.7 class lands inside the A1.4 elimination hypothesis, with
 165representing size function `gibbsSize`. -/
 166theorem a17_lands_in_a14_elimination
 167    (F : CensusDilateFamily) {c : LetterCost} {a e : ℝ}
 168    (h : FixedKindTotals c) (hs : SurfaceTotal F c a e) :
 169    UnitFugacity gibbsSize :=
 170  (unit_fugacity_forced_by_surface_and_kindTotals F h hs).1
 171
 172/-! ## §3. Composition: erasure Jacobian + unit fugacity ⇒ `mu` with no fugacity freedom -/
 173
 174/-- **Composition (atom class).**  For an equivariant letter cost that posts `mu`
 175at the three atoms with class mass represented there by `sizeWeight f`:
 176
 1771. the erasure Jacobian holds (C4 / D1);
 1782. `UnitFugacity f` holds (C17 / D1);
 1793. at every atom, the posted class mass equals `mu`.
 180
 181Class on the face: `Equivariant` + atom-only posting of `mu` +
 182`sizeWeight`-representability at the atoms.  This is the full current position of
 183the base/no-tilt split on that class: the divisor is the erasure Jacobian, and the
 184fugacity freedom has collapsed. -/
 185theorem erasure_and_unit_fugacity_compose_to_mu
 186    {c : LetterCost} (hc : Equivariant c) (f : ℕ → ℕ → ℕ → ℝ)
 187    (hpost : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 188      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K)
 189    (hrep : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 190      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K)
 191        = classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K)) :
 192    (∀ (K : BoundedComplex B),
 193        erasePush (fun K' : BoundedComplex B => Real.exp (-(historyCost c B K')))
 194            (erase B K)
 195          = Real.exp (-(historyCost c B K))
 196              * ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 197              / (Nat.card (Aut K) : ℝ)
 198          ∧ postedWeight c B K = Real.exp (-(historyCost c B K)) * gibbsWeight K
 199          ∧ mu K
 200              = gibbsWeight K
 201                  * erasePush (fun _ : BoundedComplex B => (1 : ℝ)) (erase B K))
 202      ∧ UnitFugacity f
 203      ∧ (∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 204          classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K) :=
 205  ⟨fun K => gibbsWeight_is_the_erasure_jacobian hc K,
 206    unit_fugacity_forced_after_erasure c f hpost hrep,
 207    hpost⟩
 208
 209/-- **Composition at full strength on the size-blind class.**  If the
 210`sizeWeight` representation and the posting of `mu` extend to every complex (not
 211only the atoms), the size function is exactly `gibbsSize` at every size triple
 212any complex realizes, so the posted class mass equals `mu` with the fugacity
 213character forced to the unit point. -/
 214theorem erasure_and_full_posting_force_gibbsSize
 215    {c : LetterCost} (hc : Equivariant c) (f : ℕ → ℕ → ℕ → ℝ)
 216    (hpost : ∀ (B' : ℕ) (K : BoundedComplex B'),
 217      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K)
 218    (hrep : ∀ (B' : ℕ) (K : BoundedComplex B'),
 219      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K)
 220        = classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K))
 221    (K : BoundedComplex B) :
 222    f K.nV K.nE K.nT = gibbsSize K.nV K.nE K.nT
 223      ∧ UnitFugacity f
 224      ∧ erasePush (fun K' : BoundedComplex B => Real.exp (-(historyCost c B K')))
 225          (erase B K)
 226        = Real.exp (-(historyCost c B K))
 227            * ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 228            / (Nat.card (Aut K) : ℝ) := by
 229  have hUF : UnitFugacity f :=
 230    unit_fugacity_forced_after_erasure c f
 231      (fun B' K' hv hi => hpost B' K')
 232      (fun B' K' hv hi => hrep B' K')
 233  have hgs : f K.nV K.nE K.nT = gibbsSize K.nV K.nE K.nT := by
 234    have hmu : classMass (sizeWeight f) (Quotient.mk (relabelSetoid B) K) = mu K := by
 235      rw [← hrep B K]
 236      exact hpost B K
 237    exact (classMass_sizeWeight_eq_mu_iff f K).mp hmu
 238  refine ⟨hgs, hUF, ?_⟩
 239  exact (gibbsWeight_is_the_erasure_jacobian hc K).1
 240
 241/-- **Composition on the A1.7 class.**  Erasure Jacobian plus the A1.7 forcing:
 242posted weight equals the Gibbs size-blind weight, unit fugacity holds, class mass
 243equals `mu`, and the three fugacities of the closed-form residue are gone. -/
 244theorem erasure_and_a17_compose_to_mu_no_fugacity
 245    (F : CensusDilateFamily) {c : LetterCost} {a e : ℝ}
 246    (hc : Equivariant c) (h : FixedKindTotals c) (hs : SurfaceTotal F c a e)
 247    (K : BoundedComplex B) :
 248    erasePush (fun K' : BoundedComplex B => Real.exp (-(historyCost c B K')))
 249        (erase B K)
 250      = Real.exp (-(historyCost c B K))
 251          * ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 252          / (Nat.card (Aut K) : ℝ)
 253      ∧ postedWeight c B K = sizeWeight gibbsSize K
 254      ∧ UnitFugacity gibbsSize
 255      ∧ classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K := by
 256  obtain ⟨hUF, hsw, hmu⟩ := unit_fugacity_forced_by_surface_and_kindTotals F h hs
 257  refine ⟨(gibbsWeight_is_the_erasure_jacobian hc K).1, hsw B K, hUF, hmu B K⟩
 258
 259/-! ## §4. Obstruction witnesses: what blocks further widening -/
 260
 261/-- **Obstruction 1 (labeled level).**  There exist costs that post `mu` everywhere
 262whose posted weight is not any `sizeWeight`, so the A1.4 elimination predicate
 263(`UnitFugacity` on a representing size function) does not apply to the labeled
 264weight.  At class-mass level the representing size function is still `gibbsSize`
 265(unit).  Witness: `tiltedCost (1/2)`. -/
 266theorem widening_blocked_by_non_sizeWeight_posting :
 267    ∃ (c : LetterCost),
 268      (∀ (B' : ℕ) (K : BoundedComplex B'),
 269          classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K)
 270        ∧ (¬ ∃ f : ℕ → ℕ → ℕ → ℝ,
 271              ∀ K : BoundedComplex 3, postedWeight c 3 K = sizeWeight f K)
 272        ∧ UnitFugacity gibbsSize := by
 273  have ht : |(1 / 2 : ℝ)| < 1 := by
 274    rw [abs_lt]
 275    constructor <;> norm_num
 276  have ht0 : (1 / 2 : ℝ) ≠ 0 := by norm_num
 277  refine ⟨tiltedCost (1 / 2), fun B' K => tiltedCost_posts_mu ht B' K,
 278    postedWeight_tiltedCost_not_sizeWeight ht ht0, gibbsSize_unitFugacity⟩
 279
 280/-- **Obstruction 2 (no-`mu` structural class).**  Kind-only + equivariant +
 281size-blind + gluing leaves the fugacity free: for every positive non-unit triple
 282there is a countermodel.  So elimination cannot drop the hypothesis that names
 283`mu` at the atoms. -/
 284theorem widening_blocked_without_naming_mu {zV zE zT : ℝ}
 285    (hzV : 0 < zV) (hzE : 0 < zE) (hzT : 0 < zT)
 286    (hne : ¬ (zV = 1 ∧ zE = 1 ∧ zT = 1)) :
 287    ∃ (c : LetterCost) (f : ℕ → ℕ → ℕ → ℝ),
 288      KindOnly c ∧ Equivariant c ∧ SizeBlind (postedWeight c)
 289        ∧ (∀ (B' : ℕ) (K : BoundedComplex B'), postedWeight c B' K = sizeWeight f K)
 290        ∧ CarrierShuffle f
 291        ∧ ¬ UnitFugacity f :=
 292  gluing_and_posting_do_not_force_unit_fugacity hzV hzE hzT hne
 293
 294/-- **Obstruction 3 (A1.7 escape).**  Fixed kind totals is load-bearing for the
 295A1.7 widening: `surfaceCost t` is equivariant, bulk-cancelling, and nonzero, with
 296no fixed kind totals.  Costs without kind totals are outside the widened class. -/
 297theorem widening_blocked_without_kindTotals (F : CensusDilateFamily) {t : ℝ}
 298    (ht : t ≠ 0) :
 299    Equivariant (surfaceCost t)
 300      ∧ SurfaceTotal F (surfaceCost t) t 0
 301      ∧ ¬ FixedKindTotals (surfaceCost t)
 302      ∧ historyCost (surfaceCost t) 16 (dust 16) ≠ 0 :=
 303  fixed_kind_totals_is_load_bearing F ht
 304
 305/-! ## §5. Verdict package and flag certificate -/
 306
 307/-- **THE VERDICT.**  Four parts, composing C4 with C17 on the classes that
 308genuinely reach.
 309
 3101.  Atom-only posting of `mu` plus `sizeWeight` representation forces unit
 311    fugacity (`unit_fugacity_forced_after_erasure`).
 3122.  On the three-fugacity residue, that is exactly `z_V = z_E = z_T = 1`.
 3133.  A1.7 widens past naming `mu`: surface purity plus kind totals derive unit
 314    fugacity and `mu` posting.
 3154.  Composed with the erasure Jacobian, the posted class mass equals `mu` with
 316    no fugacity freedom on those classes.
 317
 318Flag 8 stays false: the local numerator for physical costs remains open, and
 319costs outside the `sizeWeight` / A1.7 classes are not bound. -/
 320theorem fugacity_elimination_verdict :
 321    (∀ (c : LetterCost) (f : ℕ → ℕ → ℕ → ℝ),
 322        (∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 323            classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K) →
 324          (∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 325              classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K)
 326                = classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K)) →
 327            UnitFugacity f)
 328      ∧ (∀ zV zE zT : ℝ, 0 < zV → 0 < zE → 0 < zT →
 329          (∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 330              classMass (sizeWeight (characterSize zV zE zT))
 331                (Quotient.mk (relabelSetoid B') K) = mu K) →
 332            zV = 1 ∧ zE = 1 ∧ zT = 1)
 333      ∧ (∀ (F : CensusDilateFamily) (c : LetterCost) (a e : ℝ),
 334          FixedKindTotals c → SurfaceTotal F c a e → UnitFugacity gibbsSize)
 335      ∧ UnitFugacity gibbsSize :=
 336  ⟨fun c f hpost hrep => unit_fugacity_forced_after_erasure c f hpost hrep,
 337    fun _zV _zE _zT hzV hzE hzT h => three_fugacities_collapse_on_posting_mu hzV hzE hzT h,
 338    fun F _c _ _ h hs => a17_lands_in_a14_elimination F h hs,
 339    gibbsSize_unitFugacity⟩
 340
 341structure FugacityEliminationIndex : Type where
 342  /-- C17 elimination lands on the A1.4 atom/`sizeWeight` class. -/
 343  elimination_on_sizeWeight_atoms : Bool
 344  /-- The three fugacities of `characterSize` collapse on posting `mu`. -/
 345  three_fugacities_collapse : Bool
 346  /-- A1.7 widens past naming `mu` at the atoms. -/
 347  a17_widening : Bool
 348  /-- Composition with the erasure Jacobian is stated. -/
 349  erasure_composition : Bool
 350  /-- NOT claimed: flag 8 / gap2_measure_derived. -/
 351  measure_flag_moved : Bool
 352
 353def fugacityEliminationIndex : FugacityEliminationIndex where
 354  elimination_on_sizeWeight_atoms := true
 355  three_fugacities_collapse := true
 356  a17_widening := true
 357  erasure_composition := true
 358  measure_flag_moved := false
 359
 360theorem index_elimination : fugacityEliminationIndex.elimination_on_sizeWeight_atoms = true := rfl
 361theorem index_three_fugacities : fugacityEliminationIndex.three_fugacities_collapse = true := rfl
 362theorem index_a17_widening : fugacityEliminationIndex.a17_widening = true := rfl
 363theorem index_composition : fugacityEliminationIndex.erasure_composition = true := rfl
 364/-- NOT moved.  Flag 8 stays false; this module eliminates the three fugacities
 365on the named classes, not the local numerator for physical costs. -/
 366theorem index_flag_unmoved : fugacityEliminationIndex.measure_flag_moved = false := rfl
 367
 368/-! ## Axiom audit -/
 369
 370#print axioms unit_fugacity_forced_after_erasure
 371#print axioms three_fugacities_collapse_on_posting_mu
 372#print axioms three_fugacities_collapse_via_characterCost
 373#print axioms unit_fugacity_forced_by_surface_and_kindTotals
 374#print axioms a17_lands_in_a14_elimination
 375#print axioms erasure_and_unit_fugacity_compose_to_mu
 376#print axioms erasure_and_full_posting_force_gibbsSize
 377#print axioms erasure_and_a17_compose_to_mu_no_fugacity
 378#print axioms widening_blocked_by_non_sizeWeight_posting
 379#print axioms widening_blocked_without_naming_mu
 380#print axioms widening_blocked_without_kindTotals
 381#print axioms fugacity_elimination_verdict
 382#print axioms index_flag_unmoved
 383
 384end
 385
 386end Gap2FugacityElimination
 387end SevenGaps
 388end Gravity
 389end IndisputableMonolith
 390