IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureDerivationHostileProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureDerivation
   2import IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo
   3
   4/-!
   5# Hostile probe: Gap2MeasureDerivation flag-8 synthesis (2026-07-30)
   6
   7Attacks B-iii (wrong labeled weight), D (axiom prints), E (load-bearing
   8premises), F (blocker iff / certificate connection). Verdict MINOR; the one
   9finding (report prose naming C16 as if load-bearing) was repaired in A27 §5
  10and the flip docstring, and the flag then flipped in-session.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Gravity
  15namespace SevenGaps
  16namespace Gap2MeasureDerivationHostileProbe
  17
  18open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume
  19open Gap2LabelErasure Gap2PostingCostDerivation Gap2LetterCostDichotomy
  20open Gap2FugacityPostingGluing Gap2FugacityElimination
  21open Gap2MeasureDerivation MeasureSubstrateBlocker
  22open MeasureInvarianceNoGo
  23open scoped Classical
  24
  25noncomputable section
  26
  27/-! ## A. Type fidelity: conclusion uses library `GaugeCountingPrinciple` -/
  28
  29#check GaugeCountingPrinciple
  30#check MeasureSubstrateBlocker.GaugeCountingPrinciple
  31#check gap2_gauge_counting_gibbsWeight
  32#check gaugeCountingPrinciple_iff_mu_on_representatives
  33#check substrate_measure_blocker_certificate
  34
  35/-- Closing theorem's `GaugeCountingPrinciple` is definitionally the blocker's. -/
  36theorem gcp_closing_is_blocker_gcp (B : ℕ) :
  37    GaugeCountingPrinciple
  38        (classMass (gibbsWeight : BoundedComplex B → ℝ))
  39      = MeasureSubstrateBlocker.GaugeCountingPrinciple
  40        (classMass (gibbsWeight : BoundedComplex B → ℝ)) :=
  41  rfl
  42
  43/-! ## B. Circularity controls
  44
  45(i) `gibbsWeight` is letter-level factorials (definitional).
  46(ii) `classMass gibbsWeight = mu` routes through C4, not `rfl`.
  47(iii) Uniform labeled weight `1` fails the principle (instrument not vacuous).
  48-/
  49
  50theorem gibbsWeight_def_no_aut (K : BoundedComplex 2) :
  51    gibbsWeight K
  52      = 1 / ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) :=
  53  rfl
  54
  55/-- Not definitional: the bridge theorem is a real rewrite through C4. -/
  56theorem classMass_gibbs_eq_mu_is_not_rfl (K : BoundedComplex 2) :
  57    classMass (gibbsWeight : BoundedComplex 2 → ℝ) (erase 2 K) = mu K :=
  58  classMass_gibbs_eq_mu_via_erasure K
  59
  60/-- Fiber sum of the constant labeled weight is the orbit cardinality. -/
  61theorem classMass_one_eq_orbit (c : TriangulationClass 2) :
  62    classMass (fun _ : BoundedComplex 2 => (1 : ℝ)) c = (orbitCardClass c : ℝ) := by
  63  rw [classMass_of_invariant _ (fun _ _ _ => rfl) c, mul_one]
  64
  65/-- two-point orbit card is 1: `|Aut|=2`, factorials `2`, orbit-stabilizer. -/
  66theorem twoPoint_orbitCard : gaugeOrbitCard (twoPointComplex 2 (by decide)) = 1 := by
  67  have hOS := orbitCard_mul_autCard (twoPointComplex 2 (by decide))
  68  rw [autCard_twoPointComplex 2 (by decide)] at hOS
  69  -- abbrev sizes: nV=2, nE=0, nT=0 ⇒ RHS = 2
  70  norm_num [Nat.factorial] at hOS
  71  omega
  72
  73/-- **B-iii control.** The module's target principle fails for the wrong labeled
  74weight `1` (class mass = fibre size = 1 on the two-point class; `mu = 1/2`). -/
  75theorem wrong_labeled_weight_fails_gaugeCounting :
  76    ¬ GaugeCountingPrinciple
  77      (classMass (fun _ : BoundedComplex 2 => (1 : ℝ))) := by
  78  intro h
  79  have hmu :=
  80    (gaugeCountingPrinciple_iff_mu_on_representatives
  81      (classMass (fun _ : BoundedComplex 2 => (1 : ℝ)))).mp h
  82      (twoPointComplex 2 (by decide))
  83  rw [classMass_one_eq_orbit, orbitCardClass_mk, twoPoint_orbitCard,
  84    mu_twoPointComplex 2 (by decide)] at hmu
  85  norm_num at hmu
  86
  87/-- Uniqueness already in the library: only `gibbsWeight` among invariant labeled
  88weights induces the principle. Control that the instrument is selective. -/
  89theorem only_gibbs_among_invariant :
  90    ∀ (w : BoundedComplex 2 → ℝ),
  91      (∀ K K', Equivalent K K' → w K = w K') →
  92        GaugeCountingPrinciple (classMass w) →
  93          ∀ K, w K = gibbsWeight K :=
  94  fun w hinv h => (invariant_weight_gives_measure_iff w hinv).mp h
  95
  96/-! ## E. Load-bearing dependency (proof-term inspection helpers)
  97
  98The closing theorem's proof cites only the blocker iff and the C4 bridge.
  99These theorems exist independently of the premises certificate structure.
 100Cap-3 / cap-4 / C16 fields are not hypotheses of the closing declarations.
 101-/
 102
 103#check classMass_gibbs_eq_mu_via_erasure
 104#check mu_eq_gibbs_mul_erasePush_one
 105#check pushforward_labeledWeight_eq_gauge_divisor
 106#check unit_fugacity_forced_by_surface_and_kindTotals
 107#check measureDerivationPremises
 108#check measureDerivationPremises_inhabited
 109
 110/-- Closing theorem does not take `MeasureDerivationPremises` as an argument. -/
 111theorem closing_has_no_premises_arg (B : ℕ) :
 112    GaugeCountingPrinciple
 113      (classMass (gibbsWeight : BoundedComplex B → ℝ)) :=
 114  gap2_gauge_counting_gibbsWeight B
 115
 116/-- Flag-relevant composition still does not mention cap-3/cap-4. -/
 117theorem composition_load_bearing_shape
 118    (F : CensusDilateFamily) {c : LetterCost} {a e : ℝ}
 119    (hc : Equivariant c) (h : FixedKindTotals c) (hs : SurfaceTotal F c a e)
 120    (B : ℕ) :
 121    GaugeCountingPrinciple (classMass (postedWeight c B))
 122      ∧ GaugeCountingPrinciple
 123          (classMass (gibbsWeight : BoundedComplex B → ℝ)) :=
 124  ⟨(gap2_measure_from_c4_c17 F hc h hs B).1,
 125    (gap2_measure_from_c4_c17 F hc h hs B).2.1⟩
 126
 127/-! ## F. Exactness: blocker certificate connection -/
 128
 129theorem closing_via_blocker_iff (B : ℕ) :
 130    GaugeCountingPrinciple
 131        (classMass (gibbsWeight : BoundedComplex B → ℝ))
 132      ↔ ∀ K : BoundedComplex B,
 133          classMass (gibbsWeight : BoundedComplex B → ℝ)
 134            (Quotient.mk (relabelSetoid B) K) = mu K :=
 135  gaugeCountingPrinciple_iff_mu_on_representatives _
 136
 137theorem closing_lands_on_mu (B : ℕ) (K : BoundedComplex B) :
 138    classMass (gibbsWeight : BoundedComplex B → ℝ)
 139      (Quotient.mk (relabelSetoid B) K) = mu K :=
 140  (closing_via_blocker_iff B).mp (gap2_gauge_counting_gibbsWeight B) K
 141
 142theorem blocker_certificate_available (B : ℕ) (hB : 2 ≤ B) :
 143    GaugeCountingPrinciple
 144        (gaugeOrbitMass : TriangulationClass B → ℝ) ∧
 145      (∀ ν : TriangulationClass B → ℝ,
 146        GaugeCountingPrinciple ν ↔
 147          ∀ K : BoundedComplex B,
 148            ν (Quotient.mk (relabelSetoid B) K) = mu K) ∧
 149      ¬ GaugeCountingPrinciple
 150        (uniformClassMass : TriangulationClass B → ℝ) :=
 151  substrate_measure_blocker_certificate B hB
 152
 153/-! ## Index / flag hygiene
 154
 155The flip landed 2026-07-30 in-session after this probe's verdict (MINOR, prose
 156repaired in A27 §5 and the flip docstring). -/
 157
 158theorem flag_moved :
 159    Gap2MeasureDerivation.measureDerivationIndex.measure_flag_moved = true :=
 160  Gap2MeasureDerivation.index_flag_moved
 161
 162end
 163
 164/-! ## D. Independent axiom audit -/
 165
 166#print axioms gap2_gauge_counting_gibbsWeight
 167#print axioms gap2_gauge_counting_from_surface_and_kindTotals
 168#print axioms gap2_measure_from_c4_c17
 169#print axioms classMass_gibbs_eq_mu_via_erasure
 170#print axioms wrong_labeled_weight_fails_gaugeCounting
 171#print axioms measureDerivationPremises_inhabited
 172#print axioms closing_lands_on_mu
 173#print axioms gcp_closing_is_blocker_gcp
 174#print axioms Gap2MeasureDerivation.index_flag_moved
 175
 176end Gap2MeasureDerivationHostileProbe
 177end SevenGaps
 178end Gravity
 179end IndisputableMonolith
 180