IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGeneratedHostileProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGenerated
   2
   3/-!
   4# Hostile probe for C14 LedgerGenerated (review 2026-07-30)
   5
   6Adversarial module against `Gap2LedgerGenerated`. Edits nothing in the reviewed
   7module. Leave uncommitted.
   8
   9Attacks:
  101. Witness arithmetic: jCost letterwise equals fV(m)=m²/(2κ) with null edges/tets.
  112. Decoy discrimination: censusVertexCost fails the global predicate.
  123. Gaming cost: SJ-share on vertices is not ledger-generated (same m, different shares).
  134. C27 trigger shape: LedgerGeneratedAt ∧ ∃ nonzero historyCost at the cap.
  145. Flag unmoved index.
  156. Axiom re-audit on the load-bearing certificates.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Gravity
  20namespace SevenGaps
  21namespace Gap2LedgerGeneratedHostileProbe
  22
  23open PathSumMeasure GaugeHistoryMeasure Gap2PostingCostDerivation
  24open Gap2JEhrhartSpan Gap2JDiamondRank Gap2GluingDerivation Gap2LedgerGenerated
  25
  26noncomputable section
  27
  28/-! ## 1. Witness equals jCost letterwise -/
  29
  30theorem probe_jCost_vertex_matches_charge (kappa : ℝ) (B : ℕ) (K : BoundedComplex B)
  31    (v : Fin K.nV) :
  32    jCost kappa B K (Sum.inl v) = jCostVertexCharge kappa (vertexImbalance K v) := by
  33  simp only [jCost_inl, jCostVertexCharge]
  34
  35theorem probe_jCost_edge_zero (kappa : ℝ) (B : ℕ) (K : BoundedComplex B)
  36    (e : Fin K.nE) :
  37    jCost kappa B K (Sum.inr (Sum.inl e)) = (0 : ℝ) :=
  38  jCost_edge kappa B K e
  39
  40theorem probe_jCost_tet_zero (kappa : ℝ) (B : ℕ) (K : BoundedComplex B)
  41    (t : Fin K.nT) :
  42    jCost kappa B K (Sum.inr (Sum.inr t)) = (0 : ℝ) :=
  43  jCost_tet kappa B K t
  44
  45theorem probe_jCost_ledgerGenerated :
  46    LedgerGenerated (jCost 1) :=
  47  jCost_ledgerGenerated (by norm_num : (1 : ℝ) ≠ 0)
  48
  49/-! ## 2. Decoy fails -/
  50
  51theorem probe_decoy_fails : ¬ LedgerGenerated censusVertexCost :=
  52  censusVertexCost_not_ledgerGenerated
  53
  54/-! ## 3. Gaming: SJ-share is not a function of imbalance alone -/
  55
  56/-- Intuitively non-local: each vertex is charged the complex's total SJ. -/
  57def sjTotalVertexCost : LetterCost := fun _ K a =>
  58  match a with
  59  | Sum.inl _ => (imbalanceSq K : ℝ)
  60  | Sum.inr _ => 0
  61
  62theorem probe_sjTotal_not_ledgerGenerated :
  63    ¬ LedgerGenerated sjTotalVertexCost := by
  64  rintro ⟨fV, cE, cT, hV, hE, hT⟩
  65  -- point: SJ = 0, every vertex row m = 0, charge 0
  66  have hp := hV 4 pointComplex ⟨0, by decide⟩
  67  have mp : vertexImbalance pointComplex (⟨0, by decide⟩ : Fin 1) = 0 := by decide
  68  -- edge: vertices have m = ±1, but also compare two m = 0 carriers of different SJ:
  69  -- loopPoint has SJ = 0 at m = 0; path's middle vertex has m = 0 and SJ = 2.
  70  have hlp := hV 4 loopPointComplex ⟨1, by decide⟩
  71  have mlp : vertexImbalance loopPointComplex (⟨1, by decide⟩ : Fin 2) = 0 := by
  72    decide
  73  have hmid := hV 4 pathComplex ⟨1, by decide⟩
  74  have mmid : vertexImbalance pathComplex (⟨1, by decide⟩ : Fin 3) = 0 := by decide
  75  simp only [sjTotalVertexCost] at hp hlp hmid
  76  have eq0 : (0 : ℝ) = fV 0 := by
  77    have : imbalanceSq pointComplex = 0 := by decide
  78    simpa [mp, this] using hp
  79  have eq_lp : (0 : ℝ) = fV 0 := by
  80    have : imbalanceSq loopPointComplex = 0 := by decide
  81    simpa [mlp, this] using hlp
  82  have eq_path : (2 : ℝ) = fV 0 := by
  83    have : imbalanceSq pathComplex = 2 := by decide
  84    simpa [mmid, this] using hmid
  85  linarith [eq0, eq_path]
  86
  87/-! ## 4. Seed history costs and C27 shape -/
  88
  89theorem probe_seed_history :
  90    historyCost (jCost 1) 4 edgeComplex = 1
  91      ∧ historyCost (jCost 1) 4 loopPointComplex = 0
  92      ∧ historyCost (jCost 1) 4 pathComplex = 1
  93      ∧ historyCost (jCost 1) 4 forkComplex = 3 := by
  94  refine ⟨?_, ?_, ?_, ?_⟩
  95  · exact historyCost_jCost_one_edge
  96  · exact historyCost_jCost_one_loopPoint
  97  · exact historyCost_jCost_one_path
  98  · exact historyCost_jCost_one_fork
  99
 100theorem probe_C27_shape_cap2 : C27TriggerAt 2 (jCost 1) :=
 101  C27_trigger_armed_cap2
 102
 103theorem probe_C27_hard_stop_bool : C27_hard_stop_armed = true :=
 104  C27_hard_stop_armed_eq
 105
 106theorem probe_flag_unmoved : ledgerGeneratedIndex.measure_flag_moved = false :=
 107  index_flag_unmoved
 108
 109theorem probe_verdict : LedgerGeneratedVerdict :=
 110  ledgerGeneratedVerdict
 111
 112end
 113
 114#print axioms probe_jCost_ledgerGenerated
 115#print axioms probe_decoy_fails
 116#print axioms probe_sjTotal_not_ledgerGenerated
 117#print axioms probe_C27_shape_cap2
 118#print axioms probe_verdict
 119
 120end Gap2LedgerGeneratedHostileProbe
 121end SevenGaps
 122end Gravity
 123end IndisputableMonolith
 124