IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondRankHostileProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondRank
   2
   3/-!
   4# Hostile probe for the C15 J-diamond rank lattice (review 2026-07-30)
   5
   6Adversarial module against `Gap2JDiamondRank`. Edits nothing in the reviewed
   7module. Every attack that fails to land is evidence for the reviewed claim.
   8
   91. **Witness arithmetic, kernel-checked.** Seed diamond SJ costs (direct 2,
  10   glued 4, defect 2); out-star defect `-4`; disjoint control `0`; count-vector
  11   conflict on `(2,1,0)` with SJ costs `2` vs `0`.
  122. **J-unit defects.** Re-check `diamond_J_*` at a concrete Casimir.
  133. **Inconsistency really is unsatisfiability.** The seed and count systems
  14   have no rational solution; the last two seed equations alone already clash.
  154. **Localization identity on the seed.** Interface coupling equals the defect.
  165. **Axiom re-audit** on the headline and the two inconsistency witnesses.
  176. **Scope pressure.** The inconsistency theorems quantify over `Fin 3 → ℚ`
  18   rate triples, not over library `LetterCost`; the probe records that gap as a
  19   prose scope note, not a false theorem.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Gravity
  24namespace SevenGaps
  25namespace Gap2JDiamondRankHostileProbe
  26
  27open PathSumMeasure GaugeHistoryMeasure Gap2PostingCostDerivation Gap2JEhrhartSpan
  28open Gap2JDiamondRank
  29
  30/-! ## 1. Count-vector carriers and SJ costs -/
  31
  32theorem probe_edge_counts :
  33    edgeComplex.nV = 2 ∧ edgeComplex.nE = 1 ∧ edgeComplex.nT = 0 :=
  34  ⟨rfl, rfl, rfl⟩
  35
  36theorem probe_loopPoint_counts :
  37    loopPointComplex.nV = 2 ∧ loopPointComplex.nE = 1 ∧ loopPointComplex.nT = 0 :=
  38  ⟨rfl, rfl, rfl⟩
  39
  40theorem probe_same_count_vector :
  41    edgeComplex.nV = loopPointComplex.nV
  42      ∧ edgeComplex.nE = loopPointComplex.nE
  43      ∧ edgeComplex.nT = loopPointComplex.nT :=
  44  ⟨rfl, rfl, rfl⟩
  45
  46theorem probe_edge_SJ : imbalanceSq edgeComplex = 2 := by decide
  47
  48theorem probe_loopPoint_SJ : imbalanceSq loopPointComplex = 0 :=
  49  imbalanceSq_loopPoint
  50
  51theorem probe_path_SJ : imbalanceSq pathComplex = 2 := by decide
  52
  53theorem probe_twoEdge_SJ : imbalanceSq twoEdgeComplex = 4 :=
  54  imbalanceSq_twoEdge
  55
  56theorem probe_outStar_SJ : imbalanceSq outStarComplex = 12 :=
  57  imbalanceSq_outStar
  58
  59theorem probe_fork_SJ : imbalanceSq forkComplex = 6 :=
  60  imbalanceSq_fork
  61
  62/-! ## 2. Seed / out-star / disjoint defects in SJ and J units -/
  63
  64theorem probe_seed_defect_SJ :
  65    diamondDefect pathComplex pathLeft pathRight = 2 :=
  66  seed_diamond_defect
  67
  68theorem probe_seed_localized :
  69    diamondDefect pathComplex pathLeft pathRight
  70      = -2 * ∑ v ∈ pathLeft.verts ∩ pathRight.verts,
  71          subImbalance pathComplex pathLeft.edges v
  72            * subImbalance pathComplex pathRight.edges v :=
  73  seed_diamond_localized
  74
  75theorem probe_seed_inner_product :
  76    (∑ v ∈ pathLeft.verts ∩ pathRight.verts,
  77      subImbalance pathComplex pathLeft.edges v
  78        * subImbalance pathComplex pathRight.edges v) = -1 :=
  79  seed_inner_product
  80
  81theorem probe_outStar_defect_SJ :
  82    diamondDefect outStarComplex outStarFork outStarSpur = -4 :=
  83  outStar_diamond_defect
  84
  85theorem probe_disjoint_defect_SJ :
  86    diamondDefect twoEdgeComplex twoEdgeLeft twoEdgeRight = 0 :=
  87  twoEdge_diamond_defect
  88
  89theorem probe_seed_J_at_one :
  90    historyCost (jCost 1) 4 edgeComplex
  91      + historyCost (jCost 1) 4 edgeComplex
  92      - historyCost (jCost 1) 4 pointComplex
  93      - historyCost (jCost 1) 4 pathComplex = (1 : ℝ) / 1 :=
  94  diamond_J_seed 1 (by norm_num)
  95
  96theorem probe_outStar_J_at_one :
  97    historyCost (jCost 1) 4 forkComplex
  98      + historyCost (jCost 1) 4 edgeComplex
  99      - historyCost (jCost 1) 4 pointComplex
 100      - historyCost (jCost 1) 4 outStarComplex = (-2 : ℝ) / 1 :=
 101  diamond_J_outStar 1 (by norm_num)
 102
 103theorem probe_disjoint_J_at_one :
 104    historyCost (jCost 1) 4 edgeComplex
 105      + historyCost (jCost 1) 4 edgeComplex
 106      - historyCost (jCost 1) 4 (emptyComplex 4)
 107      - historyCost (jCost 1) 4 twoEdgeComplex = 0 :=
 108  diamond_J_disjoint 1 (by norm_num)
 109
 110theorem probe_count_conflict_J_at_one :
 111    historyCost (jCost 1) 4 edgeComplex = (1 : ℝ) / 1
 112      ∧ historyCost (jCost 1) 4 loopPointComplex = 0 := by
 113  constructor
 114  · exact historyCost_edge (1 : ℝ) (by norm_num)
 115  · exact historyCost_loopPoint (1 : ℝ)
 116
 117/-! ## 3. Unsatisfiability of the rate systems -/
 118
 119/-- The two path equations alone already contradict; the point/edge rows are
 120not needed for the clash. -/
 121theorem probe_seed_clash_from_path_rows_alone :
 122    ¬ ∃ C : Fin 3 → ℚ,
 123        3 * C 0 + 2 * C 1 = 2 ∧ 3 * C 0 + 2 * C 1 = 4 := by
 124  rintro ⟨C, h2, h4⟩
 125  linarith
 126
 127theorem probe_count_clash_alone :
 128    ¬ ∃ C : Fin 3 → ℚ, 2 * C 0 + C 1 = 2 ∧ 2 * C 0 + C 1 = 0 := by
 129  rintro ⟨C, h2, h0⟩
 130  linarith
 131
 132theorem probe_inconsistent_seed :
 133    ¬ ∃ C : Fin 3 → ℚ,
 134        C 0 = 0
 135        ∧ 2 * C 0 + C 1 = 2
 136        ∧ 3 * C 0 + 2 * C 1 = 2
 137        ∧ 3 * C 0 + 2 * C 1 = 4 :=
 138  lattice_inconsistent_seed
 139
 140theorem probe_inconsistent_counts :
 141    ¬ ∃ C : Fin 3 → ℚ,
 142        C 0 = 0 ∧ 2 * C 0 + C 1 = 2 ∧ 2 * C 0 + C 1 = 0 :=
 143  lattice_inconsistent_counts
 144
 145theorem probe_not_function_of_counts :
 146    edgeComplex.nV = loopPointComplex.nV ∧ edgeComplex.nE = loopPointComplex.nE
 147      ∧ edgeComplex.nT = loopPointComplex.nT
 148      ∧ historyCost (jCost 1) 4 edgeComplex
 149        ≠ historyCost (jCost 1) 4 loopPointComplex :=
 150  jCost_not_a_function_of_counts 1 (by norm_num)
 151
 152/-! ## 4. Rank facts on the hardcoded LHS list -/
 153
 154theorem probe_lhs_length : latticeLHS.length = 21 := latticeLHS_count
 155
 156theorem probe_lhs_rank_two :
 157    (∀ r ∈ latticeLHS, r = (r.1 - r.2.1) • rowU + r.2.1 • rowW)
 158      ∧ (∀ x y : ℚ, x • rowU + y • rowW = 0 → x = 0 ∧ y = 0)
 159      ∧ rowU ∈ latticeLHS ∧ rowW ∈ latticeLHS :=
 160  lattice_lhs_rank_two
 161
 162theorem probe_aug_independent :
 163    ∀ x y z : ℚ, x • augPoint + y • augEdge + z • augPath = 0 →
 164      x = 0 ∧ y = 0 ∧ z = 0 :=
 165  seed_augmented_independent
 166
 167/-! ## 5. Corollaries really follow from the localization identity -/
 168
 169theorem probe_empty_iface_is_corollary
 170    (K : BoundedComplex 4) (A Bd : Subcomplex K)
 171    (he : A.edges ∪ Bd.edges = Finset.univ) (hd : Disjoint A.edges Bd.edges)
 172    (hi : A.verts ∩ Bd.verts = ∅) :
 173    diamondDefect K A Bd = 0 :=
 174  diamondDefect_eq_zero_of_inter_empty K A Bd he hd hi
 175
 176theorem probe_balanced_iface_is_corollary
 177    (K : BoundedComplex 4) (A Bd : Subcomplex K)
 178    (he : A.edges ∪ Bd.edges = Finset.univ) (hd : Disjoint A.edges Bd.edges)
 179    (hb : ∀ v ∈ A.verts ∩ Bd.verts,
 180      subImbalance K A.edges v = 0 ∨ subImbalance K Bd.edges v = 0) :
 181    diamondDefect K A Bd = 0 :=
 182  diamondDefect_eq_zero_of_interface_balanced K A Bd he hd hb
 183
 184theorem probe_verdict : JDiamondRankVerdict := jDiamondRankVerdict
 185
 186/-! ## 6. Axiom re-audit -/
 187
 188#print axioms jDiamondRankVerdict
 189#print axioms lattice_inconsistent_seed
 190#print axioms lattice_inconsistent_counts
 191#print axioms jCost_not_a_function_of_counts
 192#print axioms diamondDefect_eq_neg_two_inner
 193#print axioms diamond_J_seed
 194#print axioms diamond_J_outStar
 195#print axioms diamond_J_disjoint
 196#print axioms seed_diamond_defect
 197#print axioms probe_seed_clash_from_path_rows_alone
 198#print axioms probe_count_clash_alone
 199#print axioms probe_seed_J_at_one
 200#print axioms probe_outStar_J_at_one
 201#print axioms probe_count_conflict_J_at_one
 202#print axioms probe_verdict
 203
 204end Gap2JDiamondRankHostileProbe
 205end SevenGaps
 206end Gravity
 207end IndisputableMonolith
 208