IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumBridgeHostileProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumBridge
   2
   3/-!
   4# Hostile probe for A24 Gap5MomentumBridge (review 2026-07-30)
   5
   6Adversarial module against `Gap5MomentumBridge`. Edits nothing in the reviewed
   7module. Leave uncommitted.
   8
   9Attacks:
  101. Ray witness: `scaleFreePackage_on_ray` at `a = 2`, kinetic/EEC iff `a^2 = 1`.
  112. Sign residue: `scaledImbalance (-1)` passes package + kinetic + EEC, ≠ imbalance.
  123. Chart product at a concrete orbit point (stipulated vs derived forms).
  134. Ground-state algebra: `lam^2 = 1/4` ⇒ `cKin = 1/2 ∧ cMom = 2 cGrad`.
  145. Axiom re-audit on five load-bearing certificates (incl. the wall and cluster).
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Gravity
  19namespace SevenGaps
  20namespace Gap5MomentumBridgeHostileProbe
  21
  22open ChartFromLedgerMomentum MomentumAdditivity MomentumMagnitudeBridge
  23open EnergyEqualsCostDerivation MomentumBridge
  24
  25noncomputable section
  26
  27/-! ## 1. Ray witness at a = 2 -/
  28
  29theorem probe_package_at_two :
  30    ScaleFreeMomentumPackage (scaledImbalance 2) :=
  31  scaleFreePackage_on_ray two_ne_zero
  32
  33theorem probe_kinetic_iff_unit (a : ℝ) :
  34    KineticCondition (scaledImbalance a) ↔ a ^ 2 = 1 :=
  35  kineticCondition_on_ray_iff a
  36
  37theorem probe_kinetic_fails_at_two :
  38    ¬ KineticCondition (scaledImbalance 2) :=
  39  (kineticCondition_on_ray_iff 2).not.mpr (by norm_num)
  40
  41theorem probe_eec_fails_at_two :
  42    ¬ EnergyEqualsCost (scaledImbalance 2) :=
  43  (energyEqualsCost_on_ray_iff 2).not.mpr (by norm_num)
  44
  45theorem probe_kinetic_holds_at_one :
  46    KineticCondition (scaledImbalance 1) :=
  47  (kineticCondition_on_ray_iff 1).mpr (by norm_num)
  48
  49theorem probe_wall :
  50    (∀ a : ℝ, a ≠ 0 → ScaleFreeMomentumPackage (scaledImbalance a)) ∧
  51    (∀ a : ℝ, KineticCondition (scaledImbalance a) ↔ a ^ 2 = 1) ∧
  52    (∀ a : ℝ, EnergyEqualsCost (scaledImbalance a) ↔ a ^ 2 = 1) ∧
  53    (∀ a : ℝ, scaledImbalance a ((1, 0) : LedgerState) ^ 2 = 1 ↔ a ^ 2 = 1) ∧
  54    (ScaleFreeMomentumPackage (scaledImbalance 2) ∧
  55      ¬ KineticCondition (scaledImbalance 2) ∧
  56      ¬ EnergyEqualsCost (scaledImbalance 2)) ∧
  57    (ScaleFreeMomentumPackage (scaledImbalance 1) ∧
  58      KineticCondition (scaledImbalance 1) ∧
  59      EnergyEqualsCost (scaledImbalance 1)) :=
  60  bridge_not_forced_by_scale_free_package
  61
  62theorem probe_exhibited_pair :
  63    ScaleFreeMomentumPackage (scaledImbalance 1) ∧
  64    ScaleFreeMomentumPackage (scaledImbalance 2) ∧
  65    KineticCondition (scaledImbalance 1) ∧ ¬ KineticCondition (scaledImbalance 2) :=
  66  exhibited_pair_disagrees_on_bridge
  67
  68/-! ## 2. Sign residue at unit scale -/
  69
  70theorem probe_sign_wall :
  71    ScaleFreeMomentumPackage (scaledImbalance (-1)) ∧
  72    scaledImbalance (-1) ((1, 0) : LedgerState) ^ 2 = 1 ∧
  73    KineticCondition (scaledImbalance (-1)) ∧
  74    EnergyEqualsCost (scaledImbalance (-1)) ∧
  75    scaledImbalance (-1) ≠ imbalance :=
  76  sign_not_forced_with_unit_scale
  77
  78theorem probe_neg_one_is_neg_imbalance (z : LedgerState) :
  79    scaledImbalance (-1) z = - imbalance z := by
  80  simp only [scaledImbalance]
  81  ring
  82
  83theorem probe_neg_one_ne_imbalance_at_unit_debit :
  84    scaledImbalance (-1) ((1, 0) : LedgerState) ≠
  85      imbalance ((1, 0) : LedgerState) := by
  86  simp only [scaledImbalance, imbalance, sub_zero, mul_one]
  87  norm_num
  88
  89/-! ## 3. Chart product: stipulated form matches library derived chart -/
  90
  91/-- Instantiating the stipulated chart at `p = imbalance` and
  92`lam = 1/(2√k)` recovers the library theorem `chart_is_the_imbalance_coordinate`. -/
  93theorem probe_stipulated_matches_derived (k t : ℝ) (hk : 0 < k) :
  94    t = 2 * Real.arsinh
  95      ((1 / (2 * Real.sqrt k)) * imbalance (orbitPoint k t)) := by
  96  have h := chart_is_the_imbalance_coordinate k t hk
  97  -- rewrite the derived chart into the stipulated half-imbalance shape
  98  have e : (1 / (2 * Real.sqrt k)) * imbalance (orbitPoint k t) =
  99      imbalance (orbitPoint k t) / (2 * Real.sqrt k) := by
 100    field_simp
 101  rwa [e]
 102
 103theorem probe_chart_product_on_imbalance (k : ℝ) (hk : 0 < k) (t : ℝ) :
 104    (1 / (2 * Real.sqrt k)) * imbalance (orbitPoint k t) =
 105      imbalance (orbitPoint k t) / (2 * Real.sqrt k) := by
 106  have hstip : ∀ s : ℝ,
 107      s = 2 * Real.arsinh
 108        ((1 / (2 * Real.sqrt k)) * imbalance (orbitPoint k s)) :=
 109    fun s => probe_stipulated_matches_derived k s hk
 110  exact chart_product_of_stipulated_chart k (1 / (2 * Real.sqrt k))
 111    imbalance hk hstip t
 112
 113/-! ## 4. Ground-state constants cluster (k = 1 ⇒ lam² = 1/4) -/
 114
 115theorem probe_lam_sq_at_ground_from_bridge (lam : ℝ) (p : LedgerState → ℝ)
 116    (hkin : ∀ t : ℝ, p (orbitPoint 1 t) ^ 2 = imbalance (orbitPoint 1 t) ^ 2)
 117    (hchart : ∀ t : ℝ, lam * p (orbitPoint 1 t) =
 118      imbalance (orbitPoint 1 t) / (2 * Real.sqrt 1)) :
 119    lam ^ 2 = 1 / 4 := by
 120  have h := lam_sq_of_magnitude_bridge 1 lam p one_pos hkin hchart
 121  rwa [mul_one] at h
 122
 123theorem probe_constants_cluster (lam cKin cGrad cMom : ℝ)
 124    (hlam : lam ^ 2 = 1 / 4) (hcKin : cKin = 2 * lam ^ 2)
 125    (hcMom : cMom = 4 * cKin * cGrad) :
 126    cKin = 1 / 2 ∧ cMom = 2 * cGrad :=
 127  constants_cluster_of_magnitude_bridge (lam := lam) (cKin := cKin)
 128    (cGrad := cGrad) (cMom := cMom) hlam hcKin hcMom
 129
 130/-- Off ground state the same algebra gives `cKin = 1/(2k)` when
 131`lam^2 = 1/(4k)` and `cKin = 2 lam^2`. -/
 132theorem probe_cKin_k_dependence (k lam cKin : ℝ) (hk : 0 < k)
 133    (hlam : lam ^ 2 = 1 / (4 * k)) (hcKin : cKin = 2 * lam ^ 2) :
 134    cKin = 1 / (2 * k) := by
 135  rw [hcKin, hlam]
 136  field_simp
 137  ring
 138
 139end
 140
 141#print axioms probe_package_at_two
 142#print axioms probe_kinetic_iff_unit
 143#print axioms probe_wall
 144#print axioms probe_sign_wall
 145#print axioms probe_constants_cluster
 146
 147end Gap5MomentumBridgeHostileProbe
 148end SevenGaps
 149end Gravity
 150end IndisputableMonolith
 151