IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityEliminationHostileProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityElimination
   2import IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
   3
   4/-!
   5# Hostile probe for Gap2FugacityElimination (A19 / C17)
   6
   7Uncommitted. Rebuilds from source on the bigbird tree; re-checks axioms,
   8inhabits the A1.4 class, re-verifies the three widening witnesses, and
   9exposes the theorem-3 dependency / vacuity shape for attack B.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Gravity
  14namespace SevenGaps
  15namespace Gap2FugacityEliminationHostileProbe
  16
  17open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume
  18open Gap2GluingDerivation Gap2PostingCostDerivation Gap2NonEquivariantPosting
  19open Gap2SizeBlindnessReach Gap2FugacityPostingGluing Gap2LabelErasure
  20open Gap2LetterCostDichotomy Gap2FugacityElimination FullTheoryLedger
  21
  22noncomputable section
  23
  24/-! ## F. Class of theorem 1 is inhabited (gibbsSize / characterCost 1 1 1) -/
  25
  26theorem a14_class_inhabited_by_unit_character :
  27    (∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
  28        classMass (postedWeight (characterCost 1 1 1) B')
  29          (Quotient.mk (relabelSetoid B') K) = mu K)
  30      ∧ (∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
  31          classMass (postedWeight (characterCost 1 1 1) B')
  32            (Quotient.mk (relabelSetoid B') K)
  33          = classMass (sizeWeight (characterSize 1 1 1))
  34            (Quotient.mk (relabelSetoid B') K))
  35      ∧ UnitFugacity (characterSize 1 1 1) := by
  36  have hz : (0 : ℝ) < 1 := by norm_num
  37  have hposts := (characterCost_posts_mu_iff hz hz hz).mpr ⟨rfl, rfl, rfl⟩
  38  refine ⟨fun B' K _ _ => hposts B' K,
  39    fun B' K _ _ => by rw [postedWeight_characterCost_eq hz hz hz B'],
  40    ?_⟩
  41  exact unit_fugacity_forced_after_erasure (characterCost 1 1 1) (characterSize 1 1 1)
  42    (fun B' K _ _ => hposts B' K)
  43    (fun B' K _ _ => by rw [postedWeight_characterCost_eq hz hz hz B'])
  44
  45theorem gibbsSize_witnesses_unit_fugacity : UnitFugacity gibbsSize :=
  46  gibbsSize_unitFugacity
  47
  48/-! ## C. Witness recomputation -/
  49
  50theorem witness_tilted_posts_mu_and_not_sizeWeight :
  51    (∀ (B' : ℕ) (K : BoundedComplex B'),
  52        classMass (postedWeight (tiltedCost (1 / 2)) B')
  53          (Quotient.mk (relabelSetoid B') K) = mu K)
  54      ∧ (¬ ∃ f : ℕ → ℕ → ℕ → ℝ,
  55            ∀ K : BoundedComplex 3,
  56              postedWeight (tiltedCost (1 / 2)) 3 K = sizeWeight f K) := by
  57  have ht : |(1 / 2 : ℝ)| < 1 := by
  58    rw [abs_lt]
  59    constructor <;> norm_num
  60  have ht0 : (1 / 2 : ℝ) ≠ 0 := by norm_num
  61  exact ⟨fun B' K => tiltedCost_posts_mu ht B' K,
  62    postedWeight_tiltedCost_not_sizeWeight ht ht0⟩
  63
  64theorem witness_characterCost_continuum (zV zE zT : ℝ)
  65    (hzV : 0 < zV) (hzE : 0 < zE) (hzT : 0 < zT)
  66    (hne : ¬ (zV = 1 ∧ zE = 1 ∧ zT = 1)) :
  67    KindOnly (characterCost zV zE zT)
  68      ∧ Equivariant (characterCost zV zE zT)
  69      ∧ SizeBlind (postedWeight (characterCost zV zE zT))
  70      ∧ CarrierShuffle (characterSize zV zE zT)
  71      ∧ ¬ UnitFugacity (characterSize zV zE zT) := by
  72  refine ⟨characterCost_kindOnly zV zE zT, characterCost_equivariant zV zE zT,
  73    postedWeight_characterCost_sizeBlind zV zE zT,
  74    characterSize_carrierShuffle hzV hzE hzT, ?_⟩
  75  intro hUF
  76  exact hne (unitFugacity_characterSize_iff.mp hUF)
  77
  78theorem witness_surfaceCost_escapes_kindTotals (F : CensusDilateFamily) :
  79    Equivariant (surfaceCost (1 : ℝ))
  80      ∧ SurfaceTotal F (surfaceCost (1 : ℝ)) 1 0
  81      ∧ ¬ FixedKindTotals (surfaceCost (1 : ℝ))
  82      ∧ historyCost (surfaceCost (1 : ℝ)) 16 (dust 16) ≠ 0 :=
  83  widening_blocked_without_kindTotals F (by norm_num : (1 : ℝ) ≠ 0)
  84
  85/-! ## B. Theorem-3 dependency trace
  86
  87`unit_fugacity_forced_by_surface_and_kindTotals` binders name only
  88`FixedKindTotals` and `SurfaceTotal`.  Its proof cites
  89`the_measure_is_exactly_the_gauge_divisor`, whose *conclusion* names `mu`
  90(and equals the gauge divisor).  The first conjunct `UnitFugacity gibbsSize`
  91is discharged by `gibbsSize_unitFugacity` and does not use those binders.
  92The load-bearing content is the posted-weight and class-mass conjuncts,
  93which are A1.7's content re-exported.
  94-/
  95
  96theorem thm3_first_conjunct_is_hypothesis_free :
  97    UnitFugacity gibbsSize :=
  98  gibbsSize_unitFugacity
  99
 100theorem thm3_load_bearing_is_a17
 101    (F : CensusDilateFamily) {c : LetterCost} {a e : ℝ}
 102    (h : FixedKindTotals c) (hs : SurfaceTotal F c a e)
 103    (B' : ℕ) (K : BoundedComplex B') :
 104    postedWeight c B' K = sizeWeight gibbsSize K
 105      ∧ classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K := by
 106  have hdiv := the_measure_is_exactly_the_gauge_divisor F h hs B' K
 107  refine ⟨?_, hdiv.2.2.2⟩
 108  rw [hdiv.2.1, gibbsWeight_eq_gibbsSize]
 109  rfl
 110
 111/-- `a17_lands_in_a14_elimination` concludes a hypothesis-free fact. -/
 112theorem a17_lands_ignores_binders
 113    (F : CensusDilateFamily) {c : LetterCost} {a e : ℝ}
 114    (_h : FixedKindTotals c) (_hs : SurfaceTotal F c a e) :
 115    a17_lands_in_a14_elimination F _h _hs = gibbsSize_unitFugacity := by
 116  rfl
 117
 118/-! ## D. Full-posting force is pointwise on realized triples, hypotheses on face -/
 119
 120theorem full_posting_force_is_pointwise
 121    {c : LetterCost} (hc : Equivariant c) (f : ℕ → ℕ → ℕ → ℝ)
 122    (hpost : ∀ (B' : ℕ) (K : BoundedComplex B'),
 123      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K)
 124    (hrep : ∀ (B' : ℕ) (K : BoundedComplex B'),
 125      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K)
 126        = classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K))
 127    (B : ℕ) (K : BoundedComplex B) :
 128    f K.nV K.nE K.nT = gibbsSize K.nV K.nE K.nT :=
 129  (erasure_and_full_posting_force_gibbsSize hc f hpost hrep K).1
 130
 131/-! ## A / alias check: theorem 1 is definitionally A1.4 -/
 132
 133theorem thm1_is_a14_alias (c : LetterCost) (f : ℕ → ℕ → ℕ → ℝ)
 134    (hpost : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 135      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K)
 136    (hrep : ∀ (B' : ℕ) (K : BoundedComplex B'), K.nV = 1 → K.nE + K.nT ≤ 1 →
 137      classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K)
 138        = classMass (sizeWeight f) (Quotient.mk (relabelSetoid B') K)) :
 139    unit_fugacity_forced_after_erasure c f hpost hrep
 140      = no_posting_countermodel_with_nonunit_fugacity c f hpost hrep :=
 141  rfl
 142
 143/-! ## E / G. Flag and ledger -/
 144
 145theorem flag_unmoved_rfl :
 146    Gap2FugacityElimination.fugacityEliminationIndex.measure_flag_moved = false :=
 147  Gap2FugacityElimination.index_flag_unmoved
 148
 149theorem ledger_gap2_now_true :
 150    fullTheoryBenchmarks.gap2_measure_derived = true := by
 151  simp [fullTheoryBenchmarks]
 152
 153/-! ## Axiom audit (every named C17 theorem + probe locals) -/
 154
 155#print axioms unit_fugacity_forced_after_erasure
 156#print axioms three_fugacities_collapse_on_posting_mu
 157#print axioms three_fugacities_collapse_via_characterCost
 158#print axioms unit_fugacity_forced_by_surface_and_kindTotals
 159#print axioms a17_lands_in_a14_elimination
 160#print axioms erasure_and_unit_fugacity_compose_to_mu
 161#print axioms erasure_and_full_posting_force_gibbsSize
 162#print axioms erasure_and_a17_compose_to_mu_no_fugacity
 163#print axioms widening_blocked_by_non_sizeWeight_posting
 164#print axioms widening_blocked_without_naming_mu
 165#print axioms widening_blocked_without_kindTotals
 166#print axioms fugacity_elimination_verdict
 167#print axioms a14_class_inhabited_by_unit_character
 168#print axioms witness_tilted_posts_mu_and_not_sizeWeight
 169#print axioms witness_characterCost_continuum
 170#print axioms witness_surfaceCost_escapes_kindTotals
 171#print axioms thm1_is_a14_alias
 172#print axioms thm3_load_bearing_is_a17
 173#print axioms full_posting_force_is_pointwise
 174#print axioms ledger_gap2_now_true
 175#print axioms flag_unmoved_rfl
 176
 177end
 178
 179end Gap2FugacityEliminationHostileProbe
 180end SevenGaps
 181end Gravity
 182end IndisputableMonolith
 183