IndisputableMonolith.Gravity.SevenGaps.Gap2OrientedFaceSpanHostileProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2OrientedFaceSpan
   2
   3/-!
   4# Hostile-review probe for `Gap2OrientedFaceSpan` (A16 review, 2026-07-30)
   5
   6Independent checks, written by the reviewer rather than the worker:
   7
   8* §1 re-pins every measured-value definition against the literals the claim
   9  advertises, so a drifted definition cannot hide behind the worker's theorems.
  10* §2 recomputes the certificate arithmetic from the definitions.
  11* §3 instantiates the sharp iff on a concrete vector in both directions, so a
  12  vacuous or one-sided formulation cannot pass silently.
  13* §4 specializes `no_pure_surface_term_in_census_span` at `a = 48` and checks
  14  that the headline span exclusion really is that corollary.
  15* §5 shows the negated premise of the kernel gate is inhabited, so the gate is
  16  not vacuous.
  17* §6/§7 recompute the witness-complex facts by `decide`, independently of the
  18  worker's proofs.
  19* §8 re-audits the axioms of every theorem the module prints.
  20
  21This file is review scaffolding and is removed after the run.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Gravity
  26namespace SevenGaps
  27namespace Gap2OrientedFaceSpanHostileProbe
  28
  29open PathSumMeasure GaugeHistoryMeasure Gap2PostingCostDerivation Gap2JEhrhartSpan
  30  Gap2OrientedFaceSpan
  31
  32/-! ## §1. The definitions carry the advertised values -/
  33
  34example : mV4 = ![1, 4, 6, 4, 1] := rfl
  35example : mE4 = ![15, 28, 18, 4, 0] := rfl
  36example : mT4 = ![24, 0, 0, 0, 0] := rfl
  37example : mC4 = ![0, 0, 0, 0, 1] := rfl
  38example : cert4 = ![0, 1, -2, 2, 0] := rfl
  39example : mFor4 = ![0, 48, 0, 0, 0] := rfl
  40example : mForRaw4 = ![240, -48, 0, 0, 0] := rfl
  41example : mCurl4 = ![50, 48, 12, 0, 0] := rfl
  42example : oV4e = ![1/4, 3/2, 13/4, 3, 1] := rfl
  43example : oE4e = ![15/4, 17/2, 31/4, 5/2, 0] := rfl
  44example : oT4 = ![6, -6, 0, 0, 0] := rfl
  45example : oFor4e = ![0, 21, -18, 0, 0] := rfl
  46example : ocert4e = ![121, 121, -259, 210, 0] := rfl
  47example : oV4o = ![1/4, 3/2, 3, 5/2, 3/4] := rfl
  48example : oE4o = ![15/4, 17/2, 6, 1, -1/4] := rfl
  49example : oFor4o = ![0, 21, -21, 0, 0] := rfl
  50example : ocert4o = ![32, 32, -77, 70, 0] := rfl
  51example : mFor3 = ![0, 12, 0, 0] := rfl
  52
  53/-! ## §2. Certificate arithmetic, recomputed from definitions -/
  54
  55example : dot4 cert4 mFor4 = 48 := by
  56  simp [dot4, cert4, mFor4, Fin.sum_univ_five]
  57
  58example : dot4 cert4 mV4 = 0 ∧ dot4 cert4 mE4 = 0 ∧ dot4 cert4 mT4 = 0
  59    ∧ dot4 cert4 mC4 = 0 := by
  60  refine ⟨?_, ?_, ?_, ?_⟩ <;>
  61    simp [dot4, cert4, mV4, mE4, mT4, mC4, Fin.sum_univ_five] <;> norm_num
  62
  63example : dot4 ocert4e oFor4e = 7203 := by
  64  simp [dot4, ocert4e, oFor4e, Fin.sum_univ_five]
  65  norm_num
  66
  67example : dot4 ocert4o oFor4o = 2289 := by
  68  simp [dot4, ocert4o, oFor4o, Fin.sum_univ_five]
  69  norm_num
  70
  71/-! ## §3. The sharp form is not vacuous in either direction -/
  72
  73/-- Forward direction inhabited: a census column itself lies in the span, and
  74the certificate annihilates it. -/
  75example : (∃ a b c e : ℚ, ∀ i : Fin 5,
  76    a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = mV4 i)
  77    ∧ dot4 cert4 mV4 = 0 :=
  78  ⟨⟨1, 0, 0, 0, fun i => by simp⟩, by
  79    simp [dot4, cert4, mV4, Fin.sum_univ_five] <;> norm_num⟩
  80
  81/-- Reverse direction instantiated on a concrete annihilated vector:
  82`cert4 · (3, 6, 4, 1, 5) = 6 - 8 + 2 = 0`, so the exhibited inverse must
  83produce a representation. -/
  84example : ∃ a b c e : ℚ, ∀ i : Fin 5,
  85    a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = (![3, 6, 4, 1, 5] : Fin 5 → ℚ) i :=
  86  (census4_with_const_span_iff _).mpr (by
  87    simp [dot4, cert4, Fin.sum_univ_five] <;> norm_num)
  88
  89/-- The inverse the reverse direction exhibits is honest: the coefficients it
  90returns really reconstruct the input. Checked on `(3, 6, 4, 1, 5)` with the
  91module's own formula, `a = 3t3/8 - t2/12`, `b = t2/12 - t3/8`,
  92`c = (t0 - a - 15b)/24`, `e = t4 - a`. -/
  93example : (3 * (6 : ℚ) / 8 - 4 / 12) * 1 + (4 / 12 - 3 * (6 : ℚ) / 8) * 15
  94    + ((3 - (3 * (6 : ℚ) / 8 - 4 / 12) - 15 * (4 / 12 - 3 * (6 : ℚ) / 8)) / 24) * 24
  95    + (1 - (3 * (6 : ℚ) / 8 - 4 / 12)) * 0 = 3 := by norm_num
  96
  97/-! ## §4. The corollary really specializes to the headline -/
  98
  99example : ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 100    a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = mFor4 i :=
 101  no_pure_surface_term_in_census_span 48 (by norm_num)
 102
 103/-- ... at every nonzero scale, not just the measured one. -/
 104example (a : ℚ) (ha : a ≠ 0) : ¬ ∃ p q r s : ℚ, ∀ i : Fin 5,
 105    p * mV4 i + q * mE4 i + r * mT4 i + s * mC4 i
 106      = (![0, a, 0, 0, 0] : Fin 5 → ℚ) i :=
 107  no_pure_surface_term_in_census_span a ha
 108
 109/-! ## §5. The negated premise is inhabited, so the gate is not vacuous -/
 110
 111example : FixedKindTotals (fun _ _ _ => (0 : ℝ)) :=
 112  ⟨0, 0, 0, fun _ _ => ⟨by simp, by simp, by simp⟩⟩
 113
 114/-! ## §6. The witness complexes are the claimed ones -/
 115
 116example : oneTet.nT = 1 ∧ twoTets.nT = 2 ∧ oneTet.nV = 4 ∧ twoTets.nV = 5 :=
 117  ⟨rfl, rfl, rfl, rfl⟩
 118
 119/-! ## §7. Witness arithmetic, recomputed independently -/
 120
 121example : facetImbalanceSq oneTet (0 : Fin 1) = 4 := by decide
 122example : imbalanceSqTotal twoTets = 6 := by decide
 123example : faceImbalance twoTets (facetTriple twoTets (0 : Fin 2) (0 : Fin 4)) = 0 := by decide
 124example : faceImbalance oneTet (facetTriple oneTet (0 : Fin 1) (0 : Fin 4)) = 1 := by decide
 125example : faceImbalance oneTet
 126    (revFace (facetTriple oneTet (0 : Fin 1) (0 : Fin 4))) = -1 := by decide
 127
 128/-! ## §8. The certificate structure is inhabited as claimed -/
 129
 130example : OrientedFaceSpanVerdict := orientedFaceSpanVerdict
 131
 132/-! ## Independent axiom audit -/
 133
 134#print axioms orientSign_rev
 135#print axioms faceImbalance_reverse
 136#print axioms faceImbalance_reverse_nonvacuous
 137#print axioms orientSign_degenerate_witness
 138#print axioms historyCost_jFaceCost
 139#print axioms historyCost_jFaceCost_eq
 140#print axioms jFaceCost_vanishes_on_balanced_tet
 141#print axioms orientSign_map
 142#print axioms facetTriple_relabel
 143#print axioms faceImbalance_relabel
 144#print axioms facetImbalanceSq_relabel
 145#print axioms jFaceCost_equivariant
 146#print axioms facetImbalanceSq_oneTet
 147#print axioms imbalanceSqTotal_oneTet
 148#print axioms imbalanceSqTotal_twoTets
 149#print axioms twoTets_shared_facet_balanced_others_not
 150#print axioms blockSum_oneTet
 151#print axioms blockSum_twoTets
 152#print axioms jFaceCost_not_fixedKindTotals
 153#print axioms cert4_sees_mFor4
 154#print axioms cert4_sees_mForRaw4
 155#print axioms cert4_sees_mCurl4
 156#print axioms census4_with_const_span_iff
 157#print axioms no_pure_surface_term_in_census_span
 158#print axioms mFor4_not_in_census_span
 159#print axioms mFor4_not_in_census_span_with_const
 160#print axioms mForRaw4_not_in_census_span_with_const
 161#print axioms mCurl4_not_in_census_span_with_const
 162#print axioms ocert4e_annihilates_census
 163#print axioms ocert4e_sees_oFor4e
 164#print axioms ocert4o_annihilates_census
 165#print axioms ocert4o_sees_oFor4o
 166#print axioms oFor4e_not_in_census_span_with_const
 167#print axioms oFor4o_not_in_census_span_with_const
 168#print axioms cert3_sees_mFor3
 169#print axioms mFor3_not_in_census_span
 170#print axioms orientedFaceSpanVerdict
 171
 172end Gap2OrientedFaceSpanHostileProbe
 173end SevenGaps
 174end Gravity
 175end IndisputableMonolith
 176