IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpanHostileProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan
   2
   3/-!
   4# Hostile probe for the A15 J-Ehrhart span NO-GO (review 2026-07-30)
   5
   6Adversarial module written by the hostile reviewer of `Gap2JEhrhartSpan`.  It
   7edits nothing and attacks the reviewed module from four sides; every attack
   8that fails to land is itself evidence for the reviewed claim.
   9
  101. **Uniqueness of the obstruction.**  `cert4_left_null_unique` and
  11   `cert3_left_null_unique`: every functional annihilating the census columns
  12   is a scalar multiple of the exhibited certificate, so the kill does not
  13   rest on one lucky find among many candidate functionals.
  142. **Exact residuals, kernel-checked.**  `residual4_with_const_exact`,
  15   `residual4_no_const_exact`, `residual3_no_const_exact`: the least-squares
  16   residuals the report quotes (`4096` with the constant column,
  17   `5154048/1093` without it, `648/23` in three dimensions) are reproduced
  18   inside the kernel with explicit projection coefficients, and each residual
  19   is orthogonal to every census column, which is what makes it *the*
  20   residual rather than an arbitrary nonzero vector.
  213. **Hypothesis tightness.**  `jCost_at_zero_kappa_is_fixedKindTotals`: at
  22   Casimir zero every letter costs `0`, so the `kappa ≠ 0` hypothesis of
  23   `jCost_not_fixedKindTotals` cannot be dropped.
  244. **The `j0 ≠ c_V` content.**  `probe_3D_solution_reconstructs` and
  25   `probe_3D_inversion_numbers`: the published inversion really does return
  26   `c_V = -4` on `J`'s measured moments while `j0 = 2`.
  275. **Concrete instantiation.**  `probe_edge_cost_at_two`: a single edge costs
  28   `1/2` at Casimir `2`, so the letter-cost theorems talk about a live object.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Gravity
  33namespace SevenGaps
  34namespace Gap2JEhrhartSpanHostileProbe
  35
  36open PathSumMeasure GaugeHistoryMeasure Gap2PostingCostDerivation Gap2JEhrhartSpan
  37
  38/-- **The 4D obstruction is the only one.**  The left null space of the four
  39census columns is one-dimensional, spanned by `cert4`. -/
  40theorem cert4_left_null_unique (u : Fin 5 → ℚ)
  41    (hV : dot4 u mV4 = 0) (hE : dot4 u mE4 = 0)
  42    (hT : dot4 u mT4 = 0) (hC : dot4 u mC4 = 0) :
  43    u = (u 1) • cert4 := by
  44  simp [dot4, mV4, Fin.sum_univ_five] at hV
  45  simp [dot4, mE4, Fin.sum_univ_five] at hE
  46  simp [dot4, mT4, Fin.sum_univ_five] at hT
  47  simp [dot4, mC4, Fin.sum_univ_five] at hC
  48  funext i
  49  fin_cases i <;> simp [Pi.smul_apply, cert4] <;> linarith
  50
  51/-- **The 3D obstruction is the only one.** -/
  52theorem cert3_left_null_unique (u : Fin 4 → ℚ)
  53    (hV : dot3 u mV3 = 0) (hE : dot3 u mE3 = 0) (hT : dot3 u mT3 = 0) :
  54    u = (u 1) • cert3 := by
  55  simp [dot3, mV3, Fin.sum_univ_four] at hV
  56  simp [dot3, mE3, Fin.sum_univ_four] at hE
  57  simp [dot3, mT3, Fin.sum_univ_four] at hT
  58  funext i
  59  fin_cases i <;> simp [Pi.smul_apply, cert3] <;> linarith
  60
  61/-- **Kernel-checked 4D residual with the constant column.**  The projection of
  62`mJ4` onto the four census columns leaves exactly the residual the report
  63quotes, and it is orthogonal to every column. -/
  64theorem residual4_with_const_exact :
  65    mJ4 = ((-212 : ℚ) / 9) • mV4 + ((188 : ℚ) / 9) • mE4
  66        + ((-326 : ℚ) / 27) • mT4 + ((230 : ℚ) / 9) • mC4
  67        + ![0, 64 / 3, -128 / 3, 128 / 3, 0]
  68      ∧ dot4 (![0, 64 / 3, -128 / 3, 128 / 3, 0] : Fin 5 → ℚ) mV4 = 0
  69      ∧ dot4 (![0, 64 / 3, -128 / 3, 128 / 3, 0] : Fin 5 → ℚ) mE4 = 0
  70      ∧ dot4 (![0, 64 / 3, -128 / 3, 128 / 3, 0] : Fin 5 → ℚ) mT4 = 0
  71      ∧ dot4 (![0, 64 / 3, -128 / 3, 128 / 3, 0] : Fin 5 → ℚ) mC4 = 0
  72      ∧ dot4 (![0, 64 / 3, -128 / 3, 128 / 3, 0] : Fin 5 → ℚ)
  73          (![0, 64 / 3, -128 / 3, 128 / 3, 0] : Fin 5 → ℚ) = 4096 := by
  74  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
  75  · funext i
  76    fin_cases i <;> simp [mV4, mE4, mT4, mC4, mJ4] <;> norm_num
  77  · simp [dot4, mV4, Fin.sum_univ_five] <;> norm_num
  78  · simp [dot4, mE4, Fin.sum_univ_five] <;> norm_num
  79  · simp [dot4, mT4, Fin.sum_univ_five] <;> norm_num
  80  · simp [dot4, mC4, Fin.sum_univ_five] <;> norm_num
  81  · simp [dot4, Fin.sum_univ_five] <;> norm_num
  82
  83/-- **Kernel-checked 4D residual without the constant column.** -/
  84theorem residual4_no_const_exact :
  85    mJ4 = ((-24310 : ℚ) / 1093) • mV4 + ((22530 : ℚ) / 1093) • mE4
  86        + ((-39205 : ℚ) / 3279) • mT4
  87        + ![0, 26016 / 1093, -49824 / 1093, 42096 / 1093, 26496 / 1093]
  88      ∧ dot4 (![0, 26016 / 1093, -49824 / 1093, 42096 / 1093, 26496 / 1093] :
  89          Fin 5 → ℚ) mV4 = 0
  90      ∧ dot4 (![0, 26016 / 1093, -49824 / 1093, 42096 / 1093, 26496 / 1093] :
  91          Fin 5 → ℚ) mE4 = 0
  92      ∧ dot4 (![0, 26016 / 1093, -49824 / 1093, 42096 / 1093, 26496 / 1093] :
  93          Fin 5 → ℚ) mT4 = 0
  94      ∧ dot4 (![0, 26016 / 1093, -49824 / 1093, 42096 / 1093, 26496 / 1093] :
  95          Fin 5 → ℚ)
  96          (![0, 26016 / 1093, -49824 / 1093, 42096 / 1093, 26496 / 1093] :
  97          Fin 5 → ℚ) = 5154048 / 1093 := by
  98  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  99  · funext i
 100    fin_cases i <;> simp [mV4, mE4, mT4, mJ4] <;> norm_num
 101  · simp [dot4, mV4, Fin.sum_univ_five] <;> norm_num
 102  · simp [dot4, mE4, Fin.sum_univ_five] <;> norm_num
 103  · simp [dot4, mT4, Fin.sum_univ_five] <;> norm_num
 104  · simp [dot4, Fin.sum_univ_five] <;> norm_num
 105
 106/-- **Kernel-checked 3D residual without the constant column.** -/
 107theorem residual3_no_const_exact :
 108    mJ3 = ((-62 : ℚ) / 23) • mV3 + ((264 : ℚ) / 23) • mE3
 109        + ((-893 : ℚ) / 69) • mT3 + ![0, 18 / 23, -54 / 23, 108 / 23]
 110      ∧ dot3 (![0, 18 / 23, -54 / 23, 108 / 23] : Fin 4 → ℚ) mV3 = 0
 111      ∧ dot3 (![0, 18 / 23, -54 / 23, 108 / 23] : Fin 4 → ℚ) mE3 = 0
 112      ∧ dot3 (![0, 18 / 23, -54 / 23, 108 / 23] : Fin 4 → ℚ) mT3 = 0
 113      ∧ dot3 (![0, 18 / 23, -54 / 23, 108 / 23] : Fin 4 → ℚ)
 114          (![0, 18 / 23, -54 / 23, 108 / 23] : Fin 4 → ℚ) = 648 / 23 := by
 115  refine ⟨?_, ?_, ?_, ?_, ?_⟩
 116  · funext i
 117    fin_cases i <;> simp [mV3, mE3, mT3, mJ3] <;> norm_num
 118  · simp [dot3, mV3, Fin.sum_univ_four] <;> norm_num
 119  · simp [dot3, mE3, Fin.sum_univ_four] <;> norm_num
 120  · simp [dot3, mT3, Fin.sum_univ_four] <;> norm_num
 121  · simp [dot3, Fin.sum_univ_four] <;> norm_num
 122
 123/-- **The `kappa ≠ 0` hypothesis cannot be dropped.**  At Casimir zero every
 124letter costs nothing, and the all-zero rates witness `FixedKindTotals`. -/
 125theorem jCost_at_zero_kappa_is_fixedKindTotals : FixedKindTotals (jCost 0) := by
 126  refine ⟨0, 0, 0, fun B K => ⟨?_, ?_, ?_⟩⟩ <;> simp [jCost]
 127
 128/-- **The published 3D inversion applied to `J`'s moments.**  The exhibited
 129solution of `census3_with_const_is_onto` is exactly the JSON's
 130`(c_V, c_E, c_T, c_0) = (-4, 12, -40/3, 6)`, and it reconstructs `mJ3`. -/
 131theorem probe_3D_solution_reconstructs :
 132    ∀ i : Fin 4, (-4 : ℚ) * mV3 i + 12 * mE3 i + (-40 / 3) * mT3 i
 133      + 6 * mC3 i = mJ3 i := by
 134  intro i
 135  fin_cases i <;> simp [mV3, mE3, mT3, mC3, mJ3] <;> norm_num
 136
 137/-- **The `j0 ≠ c_V` numbers.**  `c_V = -4` by the published formula,
 138`j0 = 2`. -/
 139theorem probe_3D_inversion_numbers :
 140    (3 * mJ3 2 - mJ3 1) / 6 = -4 ∧ mJ3 3 = 2 ∧ (2 : ℚ) ≠ -4 := by
 141  refine ⟨?_, ?_, ?_⟩ <;> simp [mJ3] <;> norm_num
 142
 143/-- **A live instantiation.**  The single edge costs `1/2` at Casimir `2`. -/
 144theorem probe_edge_cost_at_two :
 145    historyCost (jCost 2) 4 edgeComplex = 1 / 2 := by
 146  rw [historyCost_jCost, blockSum_edge 2 (by norm_num : (2 : ℝ) ≠ 0)]
 147
 148end Gap2JEhrhartSpanHostileProbe
 149end SevenGaps
 150end Gravity
 151end IndisputableMonolith
 152