IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasureHostileProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasure
   2import IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan
   3
   4/-!
   5# Hostile probe: Gap2LabelErasure G1 / directed-Aut / fibre-count (2026-07-30)
   6
   7Uncommitted adversarial module.  Attacks A (G1 dependency graph), C (definitional
   8collapse), D (directed Aut recomputation via kernel enumeration), E (G2), G (vacuity).
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Gravity
  13namespace SevenGaps
  14namespace Gap2LabelErasureHostileProbe
  15
  16open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume
  17open Gap2GluingDerivation Gap2PostingCostDerivation Gap2JEhrhartSpan Gap2LabelErasure
  18open scoped Classical
  19
  20/-! ## A. G1 dependency-graph probe -/
  21
  22#print labeledWeight
  23#print RelabelInvariant
  24#print rename
  25#print Gap2GaugeVolume.push
  26#print BoundedComplex
  27#check pushforward_labeledWeight_eq_gauge_divisor
  28#print classMass
  29
  30theorem g1_hyp_defs_avoid_aut :
  31    (labeledWeight 0 = (BoundedComplex 0 → ℝ))
  32      ∧ (∀ (w : labeledWeight 1),
  33          RelabelInvariant w ↔
  34            ∀ (K : BoundedComplex 1) (σv : Equiv.Perm (Fin K.nV))
  35              (σe : Equiv.Perm (Fin K.nE)) (σt : Equiv.Perm (Fin K.nT)),
  36              w (rename K σv σe σt) = w K)
  37      ∧ (∀ (K : BoundedComplex 1) (σv : Equiv.Perm (Fin K.nV))
  38            (σe : Equiv.Perm (Fin K.nE)) (σt : Equiv.Perm (Fin K.nT)),
  39          rename K σv σe σt = Gap2GaugeVolume.push K (σv, σe, σt)) :=
  40  ⟨rfl, fun _ => Iff.rfl, fun _ _ _ _ => rfl⟩
  41
  42theorem push_preserves_ordered_incidence (K : BoundedComplex 4)
  43    (g : Gap2GaugeVolume.SectorGroup K) (e : Fin (push K g).nE) :
  44    (push K g).edgeVerts e
  45      = Prod.map g.1 g.1 (K.edgeVerts (g.2.1.symm e)) :=
  46  rfl
  47
  48theorem relabel_edge_comm_is_ordered {K K' : BoundedComplex 4} (r : Relabel K K')
  49    (e : Fin K.nE) :
  50    K'.edgeVerts (r.eEquiv e) = Prod.map r.vEquiv r.vEquiv (K.edgeVerts e) :=
  51  r.edge_comm e
  52
  53/-! ## C. Fibre-count / definitional-collapse probe -/
  54
  55/-- `classMass` is definitionally a fibre sum (see `#print classMass`); no Aut factor. -/
  56theorem classMass_def_is_fibre_sum :
  57    (∀ (w : BoundedComplex 1 → ℝ) (c : TriangulationClass 1),
  58      classMass w c
  59        = ∑ K : BoundedComplex 1,
  60            if Quotient.mk (relabelSetoid 1) K = c then w K else 0) := by
  61  intro w c
  62  rfl
  63
  64theorem orbit_stabilizer_is_proved (K : BoundedComplex 1) :
  65    gaugeOrbitCard K * Nat.card (Aut K)
  66      = Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) :=
  67  orbitCard_mul_autCard K
  68
  69theorem corollary_factor_explicit {c : LetterCost} (hc : Equivariant c) (K : BoundedComplex 1) :
  70    erasePush (fun K' : BoundedComplex 1 => Real.exp (-(historyCost c 1 K'))) (erase 1 K)
  71      = Real.exp (-(historyCost c 1 K))
  72          * ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
  73          / (Nat.card (Aut K) : ℝ) :=
  74  (gibbsWeight_is_the_erasure_jacobian hc K).1
  75
  76/-! ## D. Directed Aut recomputation at (4,2,0)
  77
  78`Aut K = Relabel K K` injects into `Perm nV × Perm nE × Perm nT`
  79(`Relabel.toEquivTriple_injective`).  For `nT = 0`, Aut membership is exactly
  80ordered edge-commutation on `(σv, σe)`.  Kernel enumeration of that predicate
  81is the C16 receipt. -/
  82
  83def pathPlusIsolated : BoundedComplex 4 where
  84  nV := 4
  85  nE := 2
  86  nT := 0
  87  hV := by decide
  88  hE := by decide
  89  hT := by decide
  90  edgeVerts := fun e => if e = 0 then (0, 1) else (1, 2)
  91  tetVerts := fun t => t.elim0
  92
  93theorem pathPlusIsolated_counts :
  94    pathPlusIsolated.nV = 4 ∧ pathPlusIsolated.nE = 2 ∧ pathPlusIsolated.nT = 0 :=
  95  ⟨rfl, rfl, rfl⟩
  96
  97theorem twoEdgeComplex_counts :
  98    twoEdgeComplex.nV = 4 ∧ twoEdgeComplex.nE = 2 ∧ twoEdgeComplex.nT = 0 :=
  99  ⟨rfl, rfl, rfl⟩
 100
 101def edgeCommOK (ev : Fin 2 → Fin 4 × Fin 4)
 102    (σv : Equiv.Perm (Fin 4)) (σe : Equiv.Perm (Fin 2)) : Bool :=
 103  decide (∀ e : Fin 2, ev (σe e) = Prod.map σv σv (ev e))
 104
 105def twoEdgeEV : Fin 2 → Fin 4 × Fin 4 :=
 106  fun e => if e = 0 then (0, 1) else (2, 3)
 107
 108def pathPlusEV : Fin 2 → Fin 4 × Fin 4 :=
 109  fun e => if e = 0 then (0, 1) else (1, 2)
 110
 111def twoEdgeAutCount : ℕ :=
 112  ((Finset.univ : Finset (Equiv.Perm (Fin 4) × Equiv.Perm (Fin 2))).filter
 113    fun p => edgeCommOK twoEdgeEV p.1 p.2).card
 114
 115def pathPlusAutCount : ℕ :=
 116  ((Finset.univ : Finset (Equiv.Perm (Fin 4) × Equiv.Perm (Fin 2))).filter
 117    fun p => edgeCommOK pathPlusEV p.1 p.2).card
 118
 119/-- Kernel: two disjoint directed edges have exactly 2 ordered Aut candidates. -/
 120theorem twoEdge_autCount_eq_two : twoEdgeAutCount = 2 := by native_decide
 121
 122/-- Kernel: directed 2-path + isolated vertex has exactly 1 ordered Aut candidate. -/
 123theorem pathPlus_autCount_eq_one : pathPlusAutCount = 1 := by native_decide
 124
 125/-- Component swap of the two directed edges satisfies ordered edge_comm. -/
 126def twoEdgeSwapV : Equiv.Perm (Fin 4) :=
 127  (Equiv.swap (0 : Fin 4) 2).trans (Equiv.swap (1 : Fin 4) 3)
 128
 129theorem twoEdge_component_swap_ok :
 130    edgeCommOK twoEdgeEV twoEdgeSwapV (Equiv.swap (0 : Fin 2) 1) = true := by
 131  native_decide
 132
 133/-- Identity also satisfies edge_comm (so the two candidates are inhabited). -/
 134theorem twoEdge_id_ok :
 135    edgeCommOK twoEdgeEV (1 : Equiv.Perm (Fin 4)) (1 : Equiv.Perm (Fin 2)) = true := by
 136  native_decide
 137
 138/-- Edge reversal fails ordered edge_comm (directed carrier; undirected flip absent). -/
 139theorem twoEdge_edge_flip_fails_comm :
 140    edgeCommOK twoEdgeEV (Equiv.swap (0 : Fin 4) 1) (1 : Equiv.Perm (Fin 2)) = false := by
 141  native_decide
 142
 143/-- Class-mass / mu ratio from enumerated Aut counts: 1/2, not the undirected 1/4. -/
 144theorem enumerated_mu_ratio_is_half :
 145    (1 : ℚ) / twoEdgeAutCount / ((1 : ℚ) / pathPlusAutCount) = 1 / 2 := by
 146  rw [twoEdge_autCount_eq_two, pathPlus_autCount_eq_one]
 147  norm_num
 148
 149theorem dust_aut_arithmetic :
 150    Nat.card (Aut (dust 1)) = 1
 151      ∧ Nat.card (Aut (dunion (dust 1) (dust 1))) = 2 := by
 152  constructor
 153  · rw [autCard_dust]; decide
 154  · rw [autCard_congr (dunion_dust_equivalent 1 1), autCard_dust]; decide
 155
 156theorem pathPlus_aut_inhabited : Nonempty (Aut pathPlusIsolated) :=
 157  ⟨Relabel.refl _⟩
 158
 159/-! ## E. G2 locality -/
 160
 161theorem locallyAdditive_is_explicit :
 162    LocallyAdditive (fun _ _ => (0 : ℝ)) := by
 163  intro B B' A C; simp
 164
 165theorem uniform_quantifies_all_Q :
 166    ¬ ∃ (Q : ∀ B : ℕ, BoundedComplex B → ℝ) (zV zE zT : ℝ),
 167        (∀ (B B' : ℕ) (A : BoundedComplex B) (C : BoundedComplex B'),
 168          Q (B + B') (dunion A C) = Q B A * Q B' C)
 169          ∧ (∀ (B : ℕ) (K : BoundedComplex B),
 170              Q B K * zV ^ K.nV * zE ^ K.nE * zT ^ K.nT
 171                = (Nat.card (Aut K) : ℝ)) :=
 172  uniform_is_not_a_local_pushforward
 173
 174/-! ## G. Vacuity -/
 175
 176theorem relabelInvariant_inhabited_constant :
 177    RelabelInvariant (fun _ : BoundedComplex 2 => (1 : ℝ)) :=
 178  relabelInvariant_one
 179
 180theorem relabelInvariant_inhabited_equivariant_numerator :
 181    RelabelInvariant
 182      (fun K : BoundedComplex 2 => Real.exp (-(historyCost (incidenceCost 1) 2 K))) :=
 183  relabelInvariant_exp_neg_history (incidenceCost_equivariant 1)
 184
 185theorem dust_twin_admissible_real :
 186    (dust 1 : BoundedComplex 1).nV = 1 ∧ (dust 1).nE = 0 ∧ (dust 1).nT = 0
 187      ∧ Equivalent (dunion (dust 1) (dust 1)) (dust 2) :=
 188  dust_twin_admissible
 189
 190theorem wreath_proved_not_assumed :
 191    Nat.card (Aut (dunion (dust 1) (dust 1)))
 192      = 2 * (Nat.card (Aut (dust 1))) ^ 2 :=
 193  autCard_dust_twin
 194
 195theorem flag_still_false : labelErasureIndex.measure_flag_moved = false :=
 196  index_flag_unmoved
 197
 198#print axioms g1_hyp_defs_avoid_aut
 199#print axioms push_preserves_ordered_incidence
 200#print axioms classMass_def_is_fibre_sum
 201#print axioms orbit_stabilizer_is_proved
 202#print axioms corollary_factor_explicit
 203#print axioms twoEdge_autCount_eq_two
 204#print axioms pathPlus_autCount_eq_one
 205#print axioms twoEdge_component_swap_ok
 206#print axioms twoEdge_edge_flip_fails_comm
 207#print axioms enumerated_mu_ratio_is_half
 208#print axioms dust_aut_arithmetic
 209#print axioms relabelInvariant_inhabited_equivariant_numerator
 210#print axioms dust_twin_admissible_real
 211#print axioms wreath_proved_not_assumed
 212#print axioms uniform_quantifies_all_Q
 213#print axioms flag_still_false
 214
 215end Gap2LabelErasureHostileProbe
 216end SevenGaps
 217end Gravity
 218end IndisputableMonolith
 219