IndisputableMonolith.Gravity.Analysis.OrderSensitiveHistoryResponse4D

   1import Mathlib
   2import IndisputableMonolith.Loom.Separation
   3import IndisputableMonolith.Gravity.Analysis.ClassicalSourceProjection
   4import IndisputableMonolith.Gravity.Analysis.Q3PatchSeating
   5import IndisputableMonolith.Gravity.Analysis.MetricEdgeImage4D
   6
   7/-!
   8# Order-sensitive history → edge-current response on the Freudenthal patch
   9
  10Frozen claims G2/G3 of
  11`holography/plans/OrderSensitive_Gravity_Proposition_20260802.html`.
  12
  13The response is built from the depth-two commutator reading of a Loom
  14`Config` (the same second-order content `Core.pairTraces` /
  15`HolonomyExpansion.pairSum` isolate). The reading is seated as an
  16antisymmetric Fin 16 edge current on the generator-(0,2) edge at
  17record-time false via `Q3PatchSeating`. No metric `H`, no `muCoord` table.
  18
  19## Honesty
  20
  21* THEOREM: separation, action firing, metric-image exclusion on cfgA/cfgB.
  22* MODEL: treating the depth-two fingerprint amplitude as a physical current.
  23* Scope of outside-image: not a linearized flat-patch metric perturbation.
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Gravity
  28namespace Analysis
  29namespace OrderSensitiveHistoryResponse4D
  30
  31open IndisputableMonolith.Loom
  32open IndisputableMonolith.Loom.Certificate
  33open ClassicalSourceProjection
  34open Q3PatchSeating
  35open MetricEdgeImage4D
  36open BigOperators
  37
  38noncomputable section
  39
  40/-- Polynomial fingerprint of a Nat list. -/
  41def listFingerprint (l : List Nat) : Nat :=
  42  l.foldl (fun a x => a * 17 + x) 0
  43
  44def antisymEdge (a b : Fin 16) (amp : ℝ) : Fin 16 → Fin 16 → ℝ :=
  45  fun i j =>
  46    if i = a ∧ j = b then amp
  47    else if i = b ∧ j = a then -amp
  48    else 0
  49
  50/-- Generator-1 endpoints `(0,2)` seated at record-time false (`Loom.gen₁`). -/
  51def seatGen1 : Fin 16 × Fin 16 :=
  52  (seat (fun _ => false) false, seat (fun i => i = (1 : Fin 3)) false)
  53
  54/-- History response from depth-two reading. -/
  55def historyResponse (c : Config) : Fin 16 → Fin 16 → ℝ :=
  56  antisymEdge seatGen1.1 seatGen1.2 (listFingerprint (depthTwoReading c) : ℝ)
  57
  58def responseDiff (c₁ c₂ : Config) : Fin 16 → Fin 16 → ℝ :=
  59  fun i j => historyResponse c₁ i j - historyResponse c₂ i j
  60
  61/-- Local edge-current first variation (matches FreudenthalCoverEdgeCurrentAction4D). -/
  62def edgeCurrentFirstVariation (weight F VF : Fin 16 → Fin 16 → ℝ) : ℝ :=
  63  ∑ i, ∑ j, weight i j * Real.sinh (F i j) * VF i j
  64
  65def diracProbe (a b : Fin 16) : Fin 16 → Fin 16 → ℝ :=
  66  fun i j => if i = a ∧ j = b then (1 : ℝ) else 0
  67
  68def unitWeight : Fin 16 → Fin 16 → ℝ := fun _ _ => 1
  69
  70theorem seatGen1_ne : seatGen1.1 ≠ seatGen1.2 := by
  71  change (0 : Fin 16) ≠ 2
  72  decide
  73
  74theorem antisymEdge_fwd (a b : Fin 16) (amp : ℝ) (h : a ≠ b) :
  75    antisymEdge a b amp a b = amp := by
  76  unfold antisymEdge; simp [h]
  77
  78theorem antisymEdge_rev (a b : Fin 16) (amp : ℝ) (h : a ≠ b) :
  79    antisymEdge a b amp b a = -amp := by
  80  unfold antisymEdge; simp [h, Ne.symm h]
  81
  82theorem historyResponse_fwd (c : Config) :
  83    historyResponse c seatGen1.1 seatGen1.2 =
  84      (listFingerprint (depthTwoReading c) : ℝ) := by
  85  unfold historyResponse
  86  exact antisymEdge_fwd _ _ _ seatGen1_ne
  87
  88theorem historyResponse_rev (c : Config) :
  89    historyResponse c seatGen1.2 seatGen1.1 =
  90      -((listFingerprint (depthTwoReading c) : ℝ)) := by
  91  unfold historyResponse
  92  exact antisymEdge_rev _ _ _ seatGen1_ne
  93
  94theorem fingerprint_separates_cfgAB :
  95    listFingerprint (depthTwoReading cfgA) ≠
  96      listFingerprint (depthTwoReading cfgB) := by
  97  decide
  98
  99theorem historyResponse_separates_cfgAB :
 100    historyResponse cfgA ≠ historyResponse cfgB := by
 101  intro h
 102  have := congrFun (congrFun h seatGen1.1) seatGen1.2
 103  rw [historyResponse_fwd, historyResponse_fwd] at this
 104  exact fingerprint_separates_cfgAB (Nat.cast_injective this)
 105
 106theorem finiteCertificate_cfgAB :
 107    depthOneSource cfgA = depthOneSource cfgB ∧
 108      historyResponse cfgA ≠ historyResponse cfgB :=
 109  ⟨depth_one_is_blind, historyResponse_separates_cfgAB⟩
 110
 111theorem edgeCurrentFirstVariation_dirac (weight F : Fin 16 → Fin 16 → ℝ)
 112    (a b : Fin 16) :
 113    edgeCurrentFirstVariation weight F (diracProbe a b) =
 114      weight a b * Real.sinh (F a b) := by
 115  unfold edgeCurrentFirstVariation diracProbe
 116  have houter : ∀ i ∈ (Finset.univ : Finset (Fin 16)), i ≠ a →
 117      (∑ j, weight i j * Real.sinh (F i j) *
 118        (if i = a ∧ j = b then (1 : ℝ) else 0)) = 0 := by
 119    intro i _ hi
 120    apply Finset.sum_eq_zero
 121    intro j _
 122    rw [if_neg (fun h => hi h.1), mul_zero]
 123  rw [Finset.sum_eq_single a houter (fun h => absurd (Finset.mem_univ a) h)]
 124  have hinner : ∀ j ∈ (Finset.univ : Finset (Fin 16)), j ≠ b →
 125      weight a j * Real.sinh (F a j) *
 126        (if a = a ∧ j = b then (1 : ℝ) else 0) = 0 := by
 127    intro j _ hj
 128    rw [if_neg (fun h => hj h.2), mul_zero]
 129  rw [Finset.sum_eq_single b hinner (fun h => absurd (Finset.mem_univ b) h)]
 130  simp
 131
 132theorem edgeAction_separates_cfgAB :
 133    edgeCurrentFirstVariation unitWeight (historyResponse cfgA)
 134        (diracProbe seatGen1.1 seatGen1.2) ≠
 135      edgeCurrentFirstVariation unitWeight (historyResponse cfgB)
 136        (diracProbe seatGen1.1 seatGen1.2) := by
 137  rw [edgeCurrentFirstVariation_dirac, edgeCurrentFirstVariation_dirac,
 138    historyResponse_fwd, historyResponse_fwd]
 139  simp only [unitWeight, one_mul]
 140  intro hEq
 141  exact fingerprint_separates_cfgAB (Nat.cast_injective (Real.sinh_inj.mp hEq))
 142
 143theorem responseDiff_fwd :
 144    responseDiff cfgA cfgB seatGen1.1 seatGen1.2 =
 145      (listFingerprint (depthTwoReading cfgA) : ℝ) -
 146        (listFingerprint (depthTwoReading cfgB) : ℝ) := by
 147  simp [responseDiff, historyResponse_fwd]
 148
 149theorem responseDiff_rev :
 150    responseDiff cfgA cfgB seatGen1.2 seatGen1.1 =
 151      -responseDiff cfgA cfgB seatGen1.1 seatGen1.2 := by
 152  simp [responseDiff, historyResponse_rev, historyResponse_fwd]
 153  ring
 154
 155theorem responseDiff_fwd_ne :
 156    responseDiff cfgA cfgB seatGen1.1 seatGen1.2 ≠ 0 := by
 157  rw [responseDiff_fwd]
 158  have h := fingerprint_separates_cfgAB
 159  exact sub_ne_zero.mpr (fun hEq => h (Nat.cast_injective hEq))
 160
 161theorem responseDiff_cfgAB_not_in_MetricEdgeImage :
 162    ¬ MetricEdgeImage (responseDiff cfgA cfgB) := by
 163  rintro ⟨H, hF⟩
 164  have h0 := congrFun (congrFun hF seatGen1.1) seatGen1.2
 165  have h1 := congrFun (congrFun hF seatGen1.2) seatGen1.1
 166  have hsym := strainCurrent_symm H seatGen1.1 seatGen1.2
 167  have hanti := responseDiff_rev
 168  have hne := responseDiff_fwd_ne
 169  have : responseDiff cfgA cfgB seatGen1.1 seatGen1.2 =
 170      responseDiff cfgA cfgB seatGen1.2 seatGen1.1 := by
 171    calc
 172      responseDiff cfgA cfgB seatGen1.1 seatGen1.2
 173          = strainCurrent H seatGen1.1 seatGen1.2 := h0
 174      _ = strainCurrent H seatGen1.2 seatGen1.1 := hsym
 175      _ = responseDiff cfgA cfgB seatGen1.2 seatGen1.1 := h1.symm
 176  rw [hanti] at this
 177  have : responseDiff cfgA cfgB seatGen1.1 seatGen1.2 = 0 := by linarith
 178  exact hne this
 179
 180theorem decoy_depthOne_blind : depthOneSource cfgA = depthOneSource cfgB :=
 181  depth_one_is_blind
 182
 183theorem discovery_pair_is_certificate_cfgAB :
 184    depthTwoReading cfgA ≠ depthTwoReading cfgB :=
 185  depth_two_separates
 186
 187theorem orderSensitive_finite_gate_cfgAB :
 188    depthOneSource cfgA = depthOneSource cfgB ∧
 189      historyResponse cfgA ≠ historyResponse cfgB ∧
 190      ¬ MetricEdgeImage (responseDiff cfgA cfgB) :=
 191  ⟨depth_one_is_blind, historyResponse_separates_cfgAB,
 192    responseDiff_cfgAB_not_in_MetricEdgeImage⟩
 193
 194end
 195
 196end OrderSensitiveHistoryResponse4D
 197end Analysis
 198end Gravity
 199end IndisputableMonolith
 200