IndisputableMonolith.Gravity.Analysis.MetricEdgeImage4D

   1import Mathlib
   2import IndisputableMonolith.Foundation.PairKernelDiscreteGauss
   3
   4/-!
   5# Finite linearized metric edge image on the Freudenthal patch
   6
   7Frozen world metric-null of
   8`holography/plans/OrderSensitive_Gravity_Proposition_20260802.html`.
   9
  10`MetricEdgeImage F` means `F` is the strain current of some `Mat4`
  11perturbation on the sixteen-site patch. The strain formula and binary
  12patch coordinates match `FreudenthalCoverEdgeCurrentAction4D` /
  13`FreudenthalCoverLedgerGraphPatch4D`, reproduced here so this module
  14does not import the heavy analysis chain.
  15
  16## Honesty
  17
  18* THEOREM: nontriviality, symmetry, properness against antisymmetric posting.
  19* Scope: linearized flat-patch metric perturbations via `strainCurrent`.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Gravity
  24namespace Analysis
  25namespace MetricEdgeImage4D
  26
  27open Foundation.PairKernelDiscreteGauss
  28open BigOperators
  29
  30abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
  31
  32/-- Binary site coordinates of the unit hypercube (matches `patchSite`). -/
  33def patchSite (v : Fin 16) (μ : Fin 4) : ℤ :=
  34  match μ with
  35  | 0 => ((v.val % 2 : ℕ) : ℤ)
  36  | 1 => ((v.val / 2 % 2 : ℕ) : ℤ)
  37  | 2 => ((v.val / 4 % 2 : ℕ) : ℤ)
  38  | 3 => ((v.val / 8 % 2 : ℕ) : ℤ)
  39
  40def patchDisp (i j : Fin 16) : Fin 4 → ℤ :=
  41  fun μ => patchSite j μ - patchSite i μ
  42
  43/-- Strain formula matching `ReggeExactFlatHessianBlochSymbol4D.edgeStrain`. -/
  44def edgeStrain (H : Mat4) (D : Fin 4 → ℤ) : ℝ :=
  45  ∑ i : Fin 4, ∑ j : Fin 4, H i j * (D i : ℝ) * (D j : ℝ)
  46
  47/-- Strain current on patch edges. -/
  48def strainCurrent (H : Mat4) : Fin 16 → Fin 16 → ℝ :=
  49  fun i j => edgeStrain H (patchDisp i j)
  50
  51/-- Finite linearized metric edge image on the patch. -/
  52def MetricEdgeImage (F : Fin 16 → Fin 16 → ℝ) : Prop :=
  53  ∃ H : Mat4, F = strainCurrent H
  54
  55theorem edgeStrain_neg (H : Mat4) (D : Fin 4 → ℤ) :
  56    edgeStrain H (fun μ => -D μ) = edgeStrain H D := by
  57  unfold edgeStrain
  58  simp [mul_neg, neg_mul, neg_neg]
  59
  60theorem patchDisp_symm (i j : Fin 16) (μ : Fin 4) :
  61    patchDisp j i μ = -patchDisp i j μ := by
  62  simp [patchDisp, sub_eq_add_neg, add_comm]
  63
  64theorem strainCurrent_symm (H : Mat4) (i j : Fin 16) :
  65    strainCurrent H i j = strainCurrent H j i := by
  66  unfold strainCurrent
  67  have hD : patchDisp j i = fun μ => -patchDisp i j μ := by
  68    funext μ; exact patchDisp_symm i j μ
  69  rw [hD, edgeStrain_neg]
  70
  71/-- Symmetric off-diagonal witness: H_{23} = H_{32} = 1. -/
  72def axisTTCross : Mat4 := fun i j =>
  73  if (i = 2 ∧ j = 3) ∨ (i = 3 ∧ j = 2) then (1 : ℝ) else 0
  74
  75theorem axisTTCross_in_MetricEdgeImage :
  76    MetricEdgeImage (strainCurrent axisTTCross) :=
  77  ⟨axisTTCross, rfl⟩
  78
  79private theorem patchDisp_zero_twelve :
  80    patchDisp (0 : Fin 16) 12 = fun μ =>
  81      (match μ with | 0 => (0 : ℤ) | 1 => 0 | 2 => 1 | 3 => 1) := by
  82  funext μ
  83  fin_cases μ <;> rfl
  84
  85theorem strainCurrent_axisTTCross_zero_twelve :
  86    strainCurrent axisTTCross (0 : Fin 16) 12 = 2 := by
  87  unfold strainCurrent
  88  rw [patchDisp_zero_twelve]
  89  unfold edgeStrain axisTTCross
  90  simp [Fin.sum_univ_four]
  91  norm_num
  92
  93theorem MetricEdgeImage_nontrivial :
  94    ∃ F, MetricEdgeImage F ∧ F ≠ fun _ _ => 0 := by
  95  refine ⟨strainCurrent axisTTCross, axisTTCross_in_MetricEdgeImage, ?_⟩
  96  intro h
  97  have := congrFun (congrFun h (0 : Fin 16)) (12 : Fin 16)
  98  rw [strainCurrent_axisTTCross_zero_twelve] at this
  99  exact absurd this (by norm_num)
 100
 101theorem elementaryPosting_zero_four_nonzero :
 102    elementaryPosting (0 : Fin 16) 4 0 4 = 1 := by
 103  unfold elementaryPosting
 104  simp
 105
 106theorem elementaryPosting_not_in_MetricEdgeImage :
 107    ¬ MetricEdgeImage (elementaryPosting (0 : Fin 16) 4) := by
 108  rintro ⟨H, hF⟩
 109  have hsym := strainCurrent_symm H (0 : Fin 16) 4
 110  have h0 := congrFun (congrFun hF (0 : Fin 16)) (4 : Fin 16)
 111  have h1 := congrFun (congrFun hF (4 : Fin 16)) (0 : Fin 16)
 112  have hanti : elementaryPosting (0 : Fin 16) 4 4 0 =
 113      -elementaryPosting (0 : Fin 16) 4 0 4 :=
 114    elementaryPosting_antisym (0 : Fin 16) 4 4 0
 115  have : elementaryPosting (0 : Fin 16) 4 0 4 =
 116      elementaryPosting (0 : Fin 16) 4 4 0 := by
 117    calc
 118      elementaryPosting (0 : Fin 16) 4 0 4 = strainCurrent H 0 4 := h0
 119      _ = strainCurrent H 4 0 := hsym
 120      _ = elementaryPosting (0 : Fin 16) 4 4 0 := h1.symm
 121  have hnz := elementaryPosting_zero_four_nonzero
 122  rw [hanti, hnz] at this
 123  linarith
 124
 125theorem zero_in_MetricEdgeImage :
 126    MetricEdgeImage (fun _ _ => 0) := by
 127  refine ⟨0, ?_⟩
 128  funext i j
 129  unfold strainCurrent edgeStrain
 130  simp
 131
 132end MetricEdgeImage4D
 133end Analysis
 134end Gravity
 135end IndisputableMonolith
 136