IndisputableMonolith.Gravity.RecordFluxStress

   1import IndisputableMonolith.Gravity.ClausiusEinsteinBridge
   2import IndisputableMonolith.Holography.LocalRecognitionHorizonCut
   3
   4/-!
   5# Record-flux event stress (probe-independent)
   6
   7This module constructs one probe-independent symmetric stress-like matrix from
   8signed exterior cut-channel events and an explicit MODEL covector assignment.
   9Its quadratic contraction is proved for every probe of that fixed matrix.
  10
  11Honesty tags:
  12
  13* covector assignment `p` is an explicit MODEL interface;
  14* signed channel weights are derived from posted cut records;
  15* this module does **not** claim continuum stress-energy, Unruh, Ricci,
  16  focusing, all-null equality, EFE, or C-gap1 closure.
  17
  18Anti-tautology: the stress is defined once from `(w, p)` and then contracted;
  19there is no `∀ k, ∃ T(k)` interface and no structure field storing a target
  20equality.
  21-/
  22
  23noncomputable section
  24
  25namespace IndisputableMonolith
  26namespace Gravity
  27namespace RecordFluxStress
  28
  29open ClausiusEinsteinBridge
  30open Holography.LocalRecognitionHorizonCut
  31open Holography.RecordMonotonicity
  32
  33/--
  34Probe-independent event stress: the sum of weighted outer products of the
  35assigned covectors.  Defined componentwise so the matrix is fixed before any
  36probe appears.
  37-/
  38def eventStress {E : Type*} [Fintype E] (w : E → ℝ) (p : E → Fin 4 → ℝ) :
  39    Matrix (Fin 4) (Fin 4) ℝ :=
  40  fun a b => ∑ e : E, w e * p e a * p e b
  41
  42/-- Outer-product summands are symmetric, hence so is `eventStress`. -/
  43theorem eventStress_symmetric {E : Type*} [Fintype E]
  44    (w : E → ℝ) (p : E → Fin 4 → ℝ) :
  45    Symmetric4 (eventStress w p) := by
  46  intro i j
  47  simp only [eventStress]
  48  refine Finset.sum_congr rfl fun e _ => by ring
  49
  50private lemma sum_mul_sq (q k : Fin 4 → ℝ) (w : ℝ) :
  51    (∑ i, ∑ j, w * q i * q j * k i * k j) =
  52      w * (∑ μ, q μ * k μ) ^ 2 := by
  53  have h1 :
  54      (∑ i, ∑ j, w * q i * q j * k i * k j) =
  55        ∑ i, ∑ j, (w * (q i * k i)) * (q j * k j) := by
  56    refine Finset.sum_congr rfl fun i _ =>
  57      Finset.sum_congr rfl fun j _ => by ring
  58  rw [h1]
  59  have h2 :
  60      (∑ i, ∑ j, (w * (q i * k i)) * (q j * k j)) =
  61        ∑ i, (w * (q i * k i)) * ∑ j, q j * k j := by
  62    refine Finset.sum_congr rfl fun i _ => ?_
  63    rw [← Finset.mul_sum]
  64  rw [h2, ← Finset.sum_mul]
  65  have h3 :
  66      (∑ i, w * (q i * k i)) = w * ∑ i, q i * k i := by
  67    simp only [Finset.mul_sum]
  68  rw [h3]
  69  ring
  70
  71/--
  72Quadratic contraction of the fixed event stress against an arbitrary probe.
  73The stress is constructed from `(w, p)` before `k` appears.
  74-/
  75theorem quadContr_eventStress {E : Type*} [Fintype E]
  76    (w : E → ℝ) (p : E → Fin 4 → ℝ) (k : Fin 4 → ℝ) :
  77    quadContr (eventStress w p) k =
  78      ∑ e : E, w e * (∑ μ, p e μ * k μ) ^ 2 := by
  79  unfold quadContr eventStress
  80  have hpull (i j : Fin 4) :
  81      (∑ e : E, w e * p e i * p e j) * k i * k j =
  82        ∑ e : E, w e * p e i * p e j * k i * k j := by
  83    rw [mul_assoc, Finset.sum_mul]
  84    exact Finset.sum_congr rfl fun e _ => by ring
  85  simp_rw [hpull]
  86  have hinner (i : Fin 4) :
  87      (∑ j, ∑ e : E, w e * p e i * p e j * k i * k j) =
  88        ∑ e : E, ∑ j, w e * p e i * p e j * k i * k j :=
  89    Finset.sum_comm
  90  simp_rw [hinner]
  91  rw [Finset.sum_comm]
  92  exact Finset.sum_congr rfl fun e _ => sum_mul_sq (p e) k (w e)
  93
  94/-- Zero covectors force zero event stress (load-bearing decoy). -/
  95theorem eventStress_zero_of_covector_zero {E : Type*} [Fintype E]
  96    (w : E → ℝ) :
  97    eventStress w (fun _ _ => (0 : ℝ)) = 0 := by
  98  ext i j
  99  simp [eventStress]
 100
 101/-- Zero covectors force zero quadratic contraction for every probe. -/
 102theorem quadContr_eventStress_zero_of_covector_zero {E : Type*} [Fintype E]
 103    (w : E → ℝ) (k : Fin 4 → ℝ) :
 104    quadContr (eventStress w (fun _ _ => (0 : ℝ))) k = 0 := by
 105  rw [quadContr_eventStress]
 106  simp
 107
 108/-- Exterior cut channels: exterior-private bits plus seam bits. -/
 109abbrev ExteriorCutChannel (a s : ℕ) := Fin a ⊕ Fin s
 110
 111/-- Posted Boolean bit on one exterior cut channel. -/
 112def channelBitReadout {a s b r : ℕ} {kappa : ℝ}
 113    {H : LocalHorizonContext a s b r kappa}
 114    (c : LocalCut H) (ch : ExteriorCutChannel a s) : Bool :=
 115  match ch with
 116  | Sum.inl i => bitReadout (c.cfg.1 i)
 117  | Sum.inr j => bitReadout (c.cfg.2.1 j)
 118
 119/-- Signed integer channel delta from cut `c` to cut `c'`. -/
 120def channelDeltaZ {a s b r : ℕ} {kappa : ℝ}
 121    {H : LocalHorizonContext a s b r kappa}
 122    (c c' : LocalCut H) (ch : ExteriorCutChannel a s) : ℤ :=
 123  (if channelBitReadout c' ch then (1 : ℤ) else 0) -
 124    (if channelBitReadout c ch then 1 else 0)
 125
 126/-- Real channel weight used by the event-stress construction. -/
 127def channelDelta {a s b r : ℕ} {kappa : ℝ}
 128    {H : LocalHorizonContext a s b r kappa}
 129    (c c' : LocalCut H) (ch : ExteriorCutChannel a s) : ℝ :=
 130  (channelDeltaZ c c' ch : ℝ)
 131
 132/--
 133Cut event stress: one fixed symmetric matrix from signed exterior channel
 134weights and an explicit MODEL covector assignment.
 135-/
 136def cutEventStress {a s b r : ℕ} {kappa : ℝ}
 137    {H : LocalHorizonContext a s b r kappa}
 138    (c c' : LocalCut H) (p : ExteriorCutChannel a s → Fin 4 → ℝ) :
 139    Matrix (Fin 4) (Fin 4) ℝ :=
 140  eventStress (channelDelta c c') p
 141
 142theorem cutEventStress_symmetric {a s b r : ℕ} {kappa : ℝ}
 143    {H : LocalHorizonContext a s b r kappa}
 144    (c c' : LocalCut H) (p : ExteriorCutChannel a s → Fin 4 → ℝ) :
 145    Symmetric4 (cutEventStress c c' p) :=
 146  eventStress_symmetric _ _
 147
 148theorem quadContr_cutEventStress {a s b r : ℕ} {kappa : ℝ}
 149    {H : LocalHorizonContext a s b r kappa}
 150    (c c' : LocalCut H) (p : ExteriorCutChannel a s → Fin 4 → ℝ)
 151    (k : Fin 4 → ℝ) :
 152    quadContr (cutEventStress c c' p) k =
 153      ∑ ch : ExteriorCutChannel a s,
 154        channelDelta c c' ch * (∑ μ, p ch μ * k μ) ^ 2 :=
 155  quadContr_eventStress _ _ _
 156
 157/-- Zero cut-channel covectors force zero cut event stress. -/
 158theorem cutEventStress_zero_of_covector_zero {a s b r : ℕ} {kappa : ℝ}
 159    {H : LocalHorizonContext a s b r kappa}
 160    (c c' : LocalCut H) :
 161    cutEventStress c c' (fun _ _ => (0 : ℝ)) = 0 :=
 162  eventStress_zero_of_covector_zero _
 163
 164/--
 165Non-tautology witness: a single event with unit weight and a nonzero covector
 166produces a nonzero stress matrix.
 167-/
 168theorem eventStress_ne_zero_of_unit_channel :
 169    eventStress (fun _ : Fin 1 => (1 : ℝ))
 170        (fun _ μ => if μ = (0 : Fin 4) then (1 : ℝ) else 0) ≠ 0 := by
 171  intro h
 172  have h00 := congrFun (congrFun h (0 : Fin 4)) (0 : Fin 4)
 173  simp [eventStress] at h00
 174
 175/-! ## Heat ↔ channel-delta bridge -/
 176
 177private def bitDelta (b b' : Bool) : ℤ :=
 178  (if b' then (1 : ℤ) else 0) - (if b then 1 else 0)
 179
 180private lemma recordFlux_eq_sum_bitDelta (r r' : List Bool) :
 181    recordFlux r r' = (List.zipWith bitDelta r r').sum :=
 182  rfl
 183
 184private lemma exteriorRecord_as_channels {a s b r : ℕ} {kappa : ℝ}
 185    {H : LocalHorizonContext a s b r kappa} (c : LocalCut H) :
 186    exteriorRecord c =
 187      List.ofFn (fun i : Fin a => channelBitReadout c (Sum.inl i)) ++
 188        List.ofFn (fun j : Fin s => channelBitReadout c (Sum.inr j)) :=
 189  rfl
 190
 191private lemma zipWith_bitDelta_ofFn {n : ℕ} (f g : Fin n → Bool) :
 192    List.zipWith bitDelta (List.ofFn f) (List.ofFn g) =
 193      List.ofFn fun i => bitDelta (f i) (g i) := by
 194  apply List.ext_getElem
 195  · simp [List.length_zipWith, List.length_ofFn]
 196  · intro i h₁ h₂
 197    have hi : i < n := by
 198      simpa [List.length_ofFn] using h₂
 199    simp [List.getElem_zipWith, List.getElem_ofFn]
 200
 201private lemma sum_ofFn_eq_sum {n : ℕ} (f : Fin n → ℤ) :
 202    (List.ofFn f).sum = ∑ i : Fin n, f i := by
 203  simp [List.sum_ofFn]
 204
 205/--
 206Posted exterior heat equals the sum of signed exterior channel deltas.
 207This links the new channel weights to the committed cut heat.
 208-/
 209theorem exteriorStepHeat_eq_sum_channelDeltaZ {a s b r : ℕ} {kappa : ℝ}
 210    {H : LocalHorizonContext a s b r kappa}
 211    (c c' : LocalCut H) :
 212    exteriorStepHeat c c' = ∑ ch : ExteriorCutChannel a s, channelDeltaZ c c' ch := by
 213  unfold exteriorStepHeat
 214  rw [recordFlux_eq_sum_bitDelta, exteriorRecord_as_channels c, exteriorRecord_as_channels c']
 215  set fA := fun i : Fin a => channelBitReadout c (Sum.inl i)
 216  set fS := fun j : Fin s => channelBitReadout c (Sum.inr j)
 217  set gA := fun i : Fin a => channelBitReadout c' (Sum.inl i)
 218  set gS := fun j : Fin s => channelBitReadout c' (Sum.inr j)
 219  have hlen : (List.ofFn fA).length = (List.ofFn gA).length := by
 220    simp [List.length_ofFn]
 221  rw [List.zipWith_append (f := bitDelta) hlen]
 222  rw [zipWith_bitDelta_ofFn fA gA, zipWith_bitDelta_ofFn fS gS, List.sum_append]
 223  rw [sum_ofFn_eq_sum, sum_ofFn_eq_sum, Fintype.sum_sum_type]
 224  refine congrArg₂ (· + ·) ?_ ?_
 225  · refine Finset.sum_congr rfl fun i _ => ?_
 226    simp only [channelDeltaZ, bitDelta, fA, gA, channelBitReadout]
 227  · refine Finset.sum_congr rfl fun j _ => ?_
 228    simp only [channelDeltaZ, bitDelta, fS, gS, channelBitReadout]
 229
 230end RecordFluxStress
 231end Gravity
 232end IndisputableMonolith
 233