IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPostingHostileProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting
   2
   3/-!
   4# Hostile review probe for `Gap2NonEquivariantPosting` (2026-07-29)
   5
   6Not part of any build target and not imported by anything.  Six adversarial checks that the
   7module under review does not itself make, each written to fail loudly if the module's machinery
   8is vacuous or its hypotheses are decoration:
   9
  101. `probe_criterion_discriminates`: the orbit-mean-one criterion is NOT satisfied by every cost.
  11   A cost the library already proved does not post `mu` (`incidenceCost 1`) must fail it.
  122. `probe_twist_moves_loopAndBridge`: the twist is not the identity at the witness complex, so
  13   the cancelling pair is two distinct labeled complexes.
  143. `probe_orbit_nontrivial`: the gauge orbit of the witness complex has more than one member,
  15   so "orbit mean one" is not secretly "the single term is one".
  164. `probe_witness_not_gibbs`: the witness's labeled weight really differs from `gibbsWeight`.
  175. `probe_family_distinguishable`: distinct tilts give distinct LABELED WEIGHTS, not merely
  18   distinct numerators, so the family does not collapse.
  196. `probe_tilt_one_breaks_the_identity`: the `|t| < 1` hypothesis is load-bearing; at `t = 1`
  20   the numerator identity is false.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Gravity
  25namespace SevenGaps
  26namespace Gap2NonEquivariantPostingHostileProbe
  27
  28open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
  29open GaugeHistoryMeasure Gap2SizeBlindnessReach Gap2PostingCostDerivation
  30open Gap2NonEquivariantPosting
  31
  32noncomputable section
  33
  34/-- **DISCRIMINATION.**  The criterion is not vacuously true.  `incidenceCost 1` is a cost the
  35library already proved does not post `mu` at the two-bridge class, so the criterion must report
  36a numerator mass different from the orbit count there. -/
  37theorem probe_criterion_discriminates :
  38    numeratorMass (incidenceCost 1) 2 (Quotient.mk (relabelSetoid 2) twoBridges)
  39      ≠ (gaugeOrbitCard twoBridges : ℝ) := by
  40  intro h
  41  exact incidencePosting_classMass_ne_mu (one_ne_zero)
  42    ((posts_mu_iff_numeratorMass_eq_orbitCard (incidenceCost 1) 2 twoBridges).mpr h)
  43
  44/-- The twist genuinely moves the witness complex. -/
  45theorem probe_twist_moves_loopAndBridge : twist loopAndBridge ≠ loopAndBridge := by
  46  intro h
  47  have h1 : edgeSign (twist loopAndBridge) = -edgeSign loopAndBridge :=
  48    edgeSign_twist loopAndBridge
  49  rw [h, edgeSign_loopAndBridge] at h1
  50  norm_num at h1
  51
  52/-- The gauge orbit of the witness complex has at least two labeled members. -/
  53theorem probe_orbit_nontrivial : 1 < gaugeOrbitCard loopAndBridge := by
  54  have hne : twist loopAndBridge ≠ loopAndBridge := probe_twist_moves_loopAndBridge
  55  haveI hnt : Nontrivial {K' : BoundedComplex 3 // Equivalent loopAndBridge K'} := by
  56    refine ⟨⟨⟨loopAndBridge, ⟨Relabel.refl _⟩⟩,
  57      ⟨twist loopAndBridge, twist_equivalent loopAndBridge⟩, ?_⟩⟩
  58    intro hEq
  59    exact hne (congrArg Subtype.val hEq).symm
  60  unfold gaugeOrbitCard
  61  first
  62    | exact Finite.one_lt_card_iff_nontrivial.mpr hnt
  63    | exact Nat.one_lt_card_iff_nontrivial.mpr hnt
  64    | exact Nat.one_lt_card_iff_nontrivial.2 hnt
  65
  66/-- The witness's labeled weight is not the Gibbs weight. -/
  67theorem probe_witness_not_gibbs {t : ℝ} (ht : |t| < 1) (ht0 : t ≠ 0) :
  68    postedWeight (tiltedCost t) 3 loopAndBridge ≠ gibbsWeight loopAndBridge := by
  69  intro h
  70  rw [postedWeight_tiltedCost ht, tiltedNumer_loopAndBridge] at h
  71  have hg : (0 : ℝ) < gibbsWeight loopAndBridge := gibbsWeight_positive loopAndBridge
  72  have h1 : (1 + t) * gibbsWeight loopAndBridge = 1 * gibbsWeight loopAndBridge := by
  73    rw [one_mul]; exact h
  74  have h2 : (1 : ℝ) + t = 1 := mul_right_cancel₀ (ne_of_gt hg) h1
  75  exact ht0 (by linarith)
  76
  77/-- Distinct tilts give distinct labeled weights, so the family is not invisible at the weight. -/
  78theorem probe_family_distinguishable {t s : ℝ} (ht : |t| < 1) (hs : |s| < 1) (hts : t ≠ s) :
  79    postedWeight (tiltedCost t) 3 loopAndBridge
  80      ≠ postedWeight (tiltedCost s) 3 loopAndBridge := by
  81  intro h
  82  rw [postedWeight_tiltedCost ht, postedWeight_tiltedCost hs] at h
  83  have hg : (0 : ℝ) < gibbsWeight loopAndBridge := gibbsWeight_positive loopAndBridge
  84  exact hts (family_injective_at_loopAndBridge (mul_right_cancel₀ (ne_of_gt hg) h))
  85
  86/-- The `|t| < 1` hypothesis is load-bearing: at `t = 1` the numerator identity fails, because
  87the twisted witness has numerator `0` and an exponential is never `0`. -/
  88theorem probe_tilt_one_breaks_the_identity :
  89    Real.exp (-(historyCost (tiltedCost 1) 3 (twist loopAndBridge)))
  90      ≠ tiltedNumer 1 (twist loopAndBridge) := by
  91  have hs : edgeSign (twist loopAndBridge) = -1 := by
  92    rw [edgeSign_twist, edgeSign_loopAndBridge]
  93  have hnum : tiltedNumer (1 : ℝ) (twist loopAndBridge) = 0 := by
  94    unfold tiltedNumer
  95    rw [hs]
  96    norm_num
  97  rw [hnum]
  98  exact (Real.exp_pos _).ne'
  99
 100end
 101
 102#print axioms probe_criterion_discriminates
 103#print axioms probe_twist_moves_loopAndBridge
 104#print axioms probe_orbit_nontrivial
 105#print axioms probe_witness_not_gibbs
 106#print axioms probe_family_distinguishable
 107#print axioms probe_tilt_one_breaks_the_identity
 108
 109end Gap2NonEquivariantPostingHostileProbe
 110end SevenGaps
 111end Gravity
 112end IndisputableMonolith
 113