IndisputableMonolith.ILG.PoissonKernel

   1import Mathlib
   2import IndisputableMonolith.ILG.Kernel
   3
   4namespace IndisputableMonolith
   5namespace ILG
   6
   7open Real
   8
   9/-!
  10# Target A: Poisson-with-kernel statement
  11
  12This module defines the modified Poisson equation as a Fourier-space multiplier
  13and proves basic stability/scaling bounds relative to standard GR.
  14-/
  15
  16/-- The modified Poisson equation in Fourier space:
  17    -k² Φ(k, a) = 4πG * w(k, a) * δρ(k, a)
  18    We define the operator-theoretic mapping from source density to potential. -/
  19noncomputable def poisson_operator (P : KernelParams) (k a δρ : ℝ) : ℝ :=
  20  if k = 0 then 0 else -(4 * Real.pi * kernel P k a * δρ) / k^2
  21
  22/-- Predicate: Φ solves the modified Poisson equation for a given source δρ. -/
  23def SolvesModifiedPoisson (P : KernelParams) (k a δρ Φ : ℝ) : Prop :=
  24  - (k^2 * Φ) = 4 * Real.pi * kernel P k a * δρ
  25
  26/-- The operator definition satisfies the predicate. -/
  27theorem poisson_operator_solves (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) :
  28    SolvesModifiedPoisson P k a δρ (poisson_operator P k a δρ) := by
  29  unfold SolvesModifiedPoisson poisson_operator
  30  simp only [if_neg hk]
  31  have hk2 : (k^2 : ℝ) ≠ 0 := pow_ne_zero 2 hk
  32  field_simp
  33
  34/-- Stability/Scaling Bound: The ILG potential Φ is strictly enhanced relative to
  35    the GR potential Φ_GR by exactly the kernel factor w(k, a). -/
  36theorem poisson_enhancement (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) :
  37    let Φ_ILG := poisson_operator P k a δρ
  38    let Φ_GR  := -(4 * Real.pi * δρ) / k^2
  39    |Φ_ILG| = kernel P k a * |Φ_GR| := by
  40  unfold poisson_operator
  41  simp only [if_neg hk]
  42  have h_kernel_pos : 0 < kernel P k a := kernel_pos P k a
  43  -- Rewrite -(4πw·δρ)/k² as w·(-(4π·δρ)/k²) under absolute value.
  44  have h_eq : -(4 * Real.pi * kernel P k a * δρ) / k^2
  45              = kernel P k a * (-(4 * Real.pi * δρ) / k^2) := by ring
  46  rw [h_eq, abs_mul, abs_of_pos h_kernel_pos]
  47
  48/-- Coercivity Bound: The modified potential is non-vanishing for any non-vanishing source. -/
  49theorem poisson_coercive (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) (hδρ : δρ ≠ 0) :
  50    poisson_operator P k a δρ ≠ 0 := by
  51  unfold poisson_operator
  52  simp only [if_neg hk]
  53  have hk2 : (k^2 : ℝ) ≠ 0 := pow_ne_zero 2 hk
  54  have h4pi_ne : (4 * Real.pi : ℝ) ≠ 0 :=
  55    mul_ne_zero (by norm_num) Real.pi_ne_zero
  56  have hkern_ne : kernel P k a ≠ 0 := (kernel_pos P k a).ne'
  57  have hnum_ne : (4 * Real.pi * kernel P k a * δρ : ℝ) ≠ 0 :=
  58    mul_ne_zero (mul_ne_zero h4pi_ne hkern_ne) hδρ
  59  have hneg_ne : -(4 * Real.pi * kernel P k a * δρ : ℝ) ≠ 0 := neg_ne_zero.mpr hnum_ne
  60  exact div_ne_zero hneg_ne hk2
  61
  62/-! ## Causality-bound Poisson operators (Beltracchi 2026 resolution)
  63
  64The original `poisson_operator` above is preserved unchanged. The two
  65operators below split the Poisson equation into a background piece
  66(unmodified standard GR) and a perturbation piece (ILG-modified, with the
  67IR cutoff that prevents the `k → 0` divergence). Together they form a
  68self-consistent ILG Poisson system that resolves Beltracchi's IR concern.
  69-/
  70
  71/-- The background Poisson operator: standard FRW, no ILG modification.
  72The homogeneous mode `ρ̄` sits at the J-cost minimum and does not source
  73any ledger gradient flow, so the background gravitational potential is
  74sourced by the standard Poisson equation. -/
  75noncomputable def poisson_operator_background (a ρ_bar : ℝ) : ℝ :=
  76  4 * Real.pi * a^2 * ρ_bar / 3
  77
  78/-- The perturbation Poisson operator: ILG-modified with explicit IR
  79cutoff `k_min`. Below `k_min` the kernel saturates at its IR-floor value,
  80preventing the divergence at `k = 0`. The canonical RS choice for the
  81cutoff is the Hubble wavenumber `k_min = a H / c`. -/
  82noncomputable def poisson_operator_perturbation (P : KernelParams)
  83    (k_min k a δρ : ℝ) : ℝ :=
  84  if k = 0 then 0
  85  else -(4 * Real.pi * kernel_perturbation P k_min k a * δρ) / k^2
  86
  87/-- The combined causality-bound Poisson operator: background plus
  88perturbation, with the kernel acting only on the perturbation. -/
  89noncomputable def poisson_operator_full (P : KernelParams)
  90    (k_min k a ρ_bar δρ : ℝ) : ℝ :=
  91  poisson_operator_background a ρ_bar + poisson_operator_perturbation P k_min k a δρ
  92
  93/-- The background piece is independent of the kernel parameters. -/
  94@[simp] theorem poisson_background_independent_of_kernel
  95    (P : KernelParams) (a ρ_bar : ℝ) :
  96    poisson_operator_full P 0 0 a ρ_bar 0
  97      = poisson_operator_background a ρ_bar := by
  98  unfold poisson_operator_full poisson_operator_perturbation
  99  simp
 100
 101/-- The perturbation kernel inside `poisson_operator_perturbation` is
 102bounded above by its IR-saturated value. This is the operator-level
 103restatement of `kernel_perturbation_bounded_above`: the multiplier in
 104front of `δρ/k²` is uniformly bounded above by a finite ceiling fixed by
 105the IR cutoff, so the perturbation operator does not run away as
 106`k → 0`. -/
 107theorem poisson_operator_perturbation_kernel_bounded
 108    (P : KernelParams) {k_min : ℝ} (hkmin : 0 < k_min)
 109    {a : ℝ} (ha : 0 < a) (k : ℝ) :
 110    kernel_perturbation P k_min k a
 111      ≤ 1 + P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha :=
 112  kernel_perturbation_bounded_above P hkmin ha k
 113
 114/-- **Background-mode invariance.** When the perturbation `δρ = 0` (pure
 115homogeneous configuration), the perturbation operator vanishes and only
 116the standard FRW background remains. This is the operator-level statement
 117that the ILG kernel does not affect the homogeneous mode. -/
 118@[simp] theorem poisson_operator_perturbation_homogeneous
 119    (P : KernelParams) (k_min k a : ℝ) :
 120    poisson_operator_perturbation P k_min k a 0 = 0 := by
 121  unfold poisson_operator_perturbation
 122  by_cases hk : k = 0
 123  · simp [hk]
 124  · simp [hk]
 125
 126/-- The full operator at zero perturbation reduces to the background. -/
 127theorem poisson_operator_full_homogeneous
 128    (P : KernelParams) (k_min k a ρ_bar : ℝ) :
 129    poisson_operator_full P k_min k a ρ_bar 0
 130      = poisson_operator_background a ρ_bar := by
 131  unfold poisson_operator_full
 132  rw [poisson_operator_perturbation_homogeneous]
 133  ring
 134
 135/-- **Master certificate for the causality-bound Poisson layer.** -/
 136structure CausalityBoundsPoissonCert where
 137  background_indep : ∀ (P : KernelParams) (a ρ_bar : ℝ),
 138                      poisson_operator_full P 0 0 a ρ_bar 0
 139                        = poisson_operator_background a ρ_bar
 140  perturbation_homogeneous : ∀ (P : KernelParams) (k_min k a : ℝ),
 141                              poisson_operator_perturbation P k_min k a 0 = 0
 142  full_homogeneous : ∀ (P : KernelParams) (k_min k a ρ_bar : ℝ),
 143                      poisson_operator_full P k_min k a ρ_bar 0
 144                        = poisson_operator_background a ρ_bar
 145
 146noncomputable def causalityBoundsPoissonCert : CausalityBoundsPoissonCert where
 147  background_indep := poisson_background_independent_of_kernel
 148  perturbation_homogeneous := poisson_operator_perturbation_homogeneous
 149  full_homogeneous := poisson_operator_full_homogeneous
 150
 151end ILG
 152end IndisputableMonolith
 153