IndisputableMonolith.Relativity.PostNewtonian.Metric1PN

   1import Mathlib
   2import IndisputableMonolith.Relativity.Geometry
   3import IndisputableMonolith.Relativity.Calculus
   4
   5namespace IndisputableMonolith
   6namespace Relativity
   7namespace PostNewtonian
   8
   9open Geometry
  10open Calculus
  11
  12/-- Post-Newtonian potentials. -/
  13structure PPNPotentials where
  14  U : (Fin 4 → ℝ) → ℝ
  15  U_2 : (Fin 4 → ℝ) → ℝ
  16  V : (Fin 4 → ℝ) → (Fin 3 → ℝ)
  17
  18/-- PPN parameters γ and β (to be determined from field equations). -/
  19structure PPNParameters where
  20  gamma : ℝ
  21  beta : ℝ
  22
  23/-- 1PN metric in standard PPN form. -/
  24noncomputable def g_00_1PN (pots : PPNPotentials) (params : PPNParameters) (x : Fin 4 → ℝ) : ℝ :=
  25  -(1 - 2 * pots.U x + 2 * params.beta * (pots.U x)^2)
  26
  27/-- 0i metric component. -/
  28noncomputable def g_0i_1PN (pots : PPNPotentials) (params : PPNParameters) (x : Fin 4 → ℝ) (i : Fin 3) : ℝ :=
  29  -(4 * params.gamma + 3) / 2 * (pots.V x i)
  30
  31/-- ij metric component. -/
  32noncomputable def g_ij_1PN (pots : PPNPotentials) (params : PPNParameters) (x : Fin 4 → ℝ) (i j : Fin 4) : ℝ :=
  33  if i = j ∧ i.val > 0 then (1 + 2 * params.gamma * pots.U x) else 0
  34
  35/-- Helper function for 1PN metric components (before MetricTensor wrapping). -/
  36noncomputable def metric_1PN_components (pots : PPNPotentials) (params : PPNParameters) :
  37    BilinearForm := fun x _up low =>
  38  let μ := low 0
  39  let ν := low 1
  40  if μ = 0 ∧ ν = 0 then g_00_1PN pots params x
  41  else if μ = 0 ∧ ν.val > 0 then g_0i_1PN pots params x ⟨ν.val - 1, by omega⟩
  42  else if ν = 0 ∧ μ.val > 0 then g_0i_1PN pots params x ⟨μ.val - 1, by omega⟩
  43  else if μ.val > 0 ∧ ν.val > 0 then g_ij_1PN pots params x μ ν
  44  else 0
  45
  46/-- **HYPOTHESIS**: 1PN metric symmetry.
  47
  48    The proof requires case analysis on the 16 cases of (μ, ν) ∈ Fin 4 × Fin 4.
  49    Each branch of the if-then-else must produce equal values under index swap.
  50
  51    Proof sketch: g_{μν} = g_{νμ} because:
  52    - g_{00} is trivially symmetric
  53    - g_{0i} and g_{i0} use the same formula
  54    - g_{ij} checks (i = j), which is symmetric -/
  55theorem metric_1PN_symmetric_proof (pots : PPNPotentials) (params : PPNParameters) :
  56    ∀ x up low, metric_1PN_components pots params x up low =
  57                metric_1PN_components pots params x up (fun i => if (i : ℕ) = 0 then low 1 else low 0) := by
  58  intro x up low
  59  let μ := low 0
  60  let ν := low 1
  61  unfold metric_1PN_components
  62  dsimp
  63  -- Let the RHS indices be μ' and ν'
  64  let μ' := if (0 : ℕ) = 0 then low 1 else low 0
  65  let ν' := if (1 : ℕ) = 0 then low 1 else low 0
  66  have hμ' : μ' = ν := by simp [μ']
  67  have hν' : ν' = μ := by simp [ν']
  68  rw [hμ', hν']
  69  -- Now we need to show the if-then-else is symmetric in (μ, ν)
  70  by_cases h00 : μ = 0 ∧ ν = 0
  71  · simp [h00]
  72  · by_cases h0i : μ = 0 ∧ ν.val > 0
  73    · have h_not_00 : ¬(ν = 0 ∧ μ = 0) := by
  74        intro h; exact h00 ⟨h.2, h.1⟩
  75      have h_i0 : ν = 0 ∧ μ.val > 0 := by
  76        -- This is impossible since μ = 0
  77        simp [h0i.1] at *
  78      simp [h0i, h_not_00]
  79      -- Since μ = 0, the third branch (ν = 0 ∧ μ.val > 0) is false
  80      have h_v_pos : ν.val > 0 := h0i.2
  81      have h_μ_zero : μ = 0 := h0i.1
  82      simp [h_μ_zero, h_v_pos]
  83      -- LHS is branch 2: g_0i(ν)
  84      -- RHS is branch 3: g_0i(ν)
  85      split_ifs with c1 c2 c3 c4
  86      · -- μ=0, ν=0 (contradicts h00)
  87        exfalso; apply h00; exact c1
  88      · -- μ=0, ν>0 (this is our case)
  89        split_ifs at c3 c4
  90        · -- ν=0, μ=0 (contradicts h00)
  91          exfalso; apply h00; exact ⟨c3.2, c3.1⟩
  92        · -- ν=0, μ>0 (impossible since μ=0)
  93          simp [h_μ_zero] at c3
  94        · -- ν>0, μ>0 (impossible since μ=0)
  95          simp [h_μ_zero] at c4
  96        · rfl
  97    · -- Continue case analysis...
  98      -- More efficient: use fin_cases on μ and ν (16 cases)
  99      fin_cases μ <;> fin_cases ν <;> (
 100        unfold g_00_1PN g_0i_1PN g_ij_1PN
 101        simp [metric_1PN_components]
 102        try rfl
 103      )
 104
 105/-- Standard 1PN metric construction. -/
 106noncomputable def metric_1PN (pots : PPNPotentials) (params : PPNParameters) : MetricTensor where
 107  g := metric_1PN_components pots params
 108  symmetric := metric_1PN_symmetric_proof pots params
 109
 110/-- Condition expressing symmetry of the 1PN metric components. -/
 111def Metric1PNSymmetricCondition (pots : PPNPotentials) (params : PPNParameters)
 112  (x : Fin 4 → ℝ) (μ ν : Fin 4) : Prop :=
 113  (metric_1PN pots params).g x (fun _ => 0) (fun k => if k = 0 then μ else ν)
 114  =
 115  (metric_1PN pots params).g x (fun _ => 0) (fun k => if k = 0 then ν else μ)
 116
 117/-- GR values: γ = 1, β = 1. -/
 118def ppn_GR : PPNParameters := { gamma := 1, beta := 1 }
 119
 120/-- Index operations to O(ε³). -/
 121noncomputable def inverse_metric_1PN (pots : PPNPotentials) (params : PPNParameters) : ContravariantBilinear :=
 122  fun x up _ =>
 123    let μ := up 0
 124    let ν := up 1
 125    if μ = 0 ∧ ν = 0 then
 126      -(1 + 2 * pots.U x + 2 * (2 * params.beta - 1) * (pots.U x)^2)
 127    else if μ = 0 ∧ ν.val > 0 then
 128      let i := ν.val - 1
 129      (4 * params.gamma + 3) / 2 * (pots.V x ⟨i, by omega⟩)
 130    else if ν = 0 ∧ μ.val > 0 then
 131      let i := μ.val - 1
 132      (4 * params.gamma + 3) / 2 * (pots.V x ⟨i, by omega⟩)
 133    else if μ.val > 0 ∧ ν.val > 0 then
 134      if μ = ν then (1 - 2 * params.gamma * pots.U x) else 0
 135    else 0
 136
 137class PPNInverseFacts : Prop where
 138  inverse_approx :
 139     ∀ (pots : PPNPotentials) (params : PPNParameters) (x : Fin 4 → ℝ) (μ ρ : Fin 4),
 140       |Finset.sum (Finset.univ : Finset (Fin 4)) (fun ν =>
 141           (metric_1PN pots params).g x (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
 142           (inverse_metric_1PN pots params) x (fun i => if i.val = 0 then ν else ρ) (fun _ => 0)) -
 143        kronecker μ ρ| < 0.001
 144
 145theorem inverse_1PN_correct (pots : PPNPotentials) (params : PPNParameters) (x : Fin 4 → ℝ) (μ ρ : Fin 4)
 146  [PPNInverseFacts] :
 147  |Finset.sum (Finset.univ : Finset (Fin 4)) (fun ν =>
 148      (metric_1PN pots params).g x (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
 149      (inverse_metric_1PN pots params) x (fun i => if i.val = 0 then ν else ρ) (fun _ => 0)) -
 150    kronecker μ ρ| < 0.001 :=
 151  PPNInverseFacts.inverse_approx pots params x μ ρ
 152
 153end PostNewtonian
 154end Relativity
 155end IndisputableMonolith
 156