IndisputableMonolith.Papers.GCIC.ReducedPhasePotential

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Reduced Phase Potential J̃ (GCIC Paper, Sec. IV)
   7
   8Formalizes the reduced phase-mismatch potential induced by the
   9discrete scaling quotient x ~ b^n x:
  10
  11  J̃_b(δ) = cosh(lam · d_ℤ(δ)) − 1,   lam = ln b,
  12
  13where d_ℤ(δ) = min_{n ∈ ℤ} |δ − n| is the distance to the nearest integer.
  14
  15## Main results
  16
  17* `distZ` — distance to nearest integer, with periodicity and zero characterization.
  18* `Jtilde` — the reduced phase potential.
  19* `Jtilde_nonneg`, `Jtilde_periodic`, `Jtilde_zero_iff` — key structural properties.
  20* `Jtilde_stiffness_lb` — small-gradient stiffness lower bound κ = lam²/2.
  21
  22## Reference
  23
  24Thapa–Washburn, "Rigidity and Compact Phase Emergence in Scale-Invariant
  25Ratio-Based Energies" (2026), Section IV.
  26-/
  27
  28namespace IndisputableMonolith.Papers.GCIC.ReducedPhasePotential
  29
  30open Real
  31open IndisputableMonolith.Cost
  32
  33/-! ### Distance to nearest integer -/
  34
  35/-- Distance to the nearest integer: d_ℤ(δ) = min(fract(δ), 1 − fract(δ)).
  36    This is in [0, 1/2] and vanishes exactly when δ is an integer. -/
  37noncomputable def distZ (δ : ℝ) : ℝ :=
  38  min (Int.fract δ) (1 - Int.fract δ)
  39
  40theorem distZ_nonneg (δ : ℝ) : 0 ≤ distZ δ := by
  41  unfold distZ
  42  exact le_min (Int.fract_nonneg δ) (by linarith [Int.fract_lt_one δ])
  43
  44theorem distZ_le_half (δ : ℝ) : distZ δ ≤ 1 / 2 := by
  45  unfold distZ
  46  rcases le_or_gt (Int.fract δ) (1 / 2) with h | h
  47  · exact min_le_left _ _ |>.trans h
  48  · have : 1 - Int.fract δ ≤ 1 / 2 := by linarith
  49    exact min_le_right _ _ |>.trans this
  50
  51/-- d_ℤ is 1-periodic: d_ℤ(δ + n) = d_ℤ(δ) for integer n. -/
  52theorem distZ_add_int (δ : ℝ) (n : ℤ) : distZ (δ + ↑n) = distZ δ := by
  53  unfold distZ
  54  rw [Int.fract_add_intCast]
  55
  56/-- d_ℤ is 1-periodic (special case n = 1). -/
  57theorem distZ_periodic (δ : ℝ) : distZ (δ + 1) = distZ δ := by
  58  have h : δ + 1 = δ + ↑(1 : ℤ) := by push_cast; ring
  59  rw [h]
  60  exact distZ_add_int δ 1
  61
  62/-- d_ℤ(δ) = 0 iff δ is an integer. -/
  63theorem distZ_eq_zero_iff (δ : ℝ) : distZ δ = 0 ↔ ∃ n : ℤ, δ = ↑n := by
  64  unfold distZ
  65  constructor
  66  · intro h
  67    have hfrac_nonneg := Int.fract_nonneg δ
  68    have h1sub_pos : 0 < 1 - Int.fract δ := by linarith [Int.fract_lt_one δ]
  69    have hfrac_zero : Int.fract δ = 0 := by
  70      rcases le_or_gt (Int.fract δ) (1 - Int.fract δ) with h_le | h_lt
  71      · rwa [min_eq_left h_le] at h
  72      · rw [min_eq_right (le_of_lt h_lt)] at h; linarith
  73    exact ⟨⌊δ⌋, by linarith [Int.fract_add_floor δ]⟩
  74  · intro ⟨n, hn⟩
  75    rw [hn, Int.fract_intCast]
  76    simp
  77
  78/-! ### The reduced phase potential -/
  79
  80/-- The reduced phase potential: J̃(lam, δ) = cosh(lam · d_ℤ(δ)) − 1.
  81    Here lam = ln b for the base b of the discrete quotient. -/
  82noncomputable def Jtilde (lam : ℝ) (δ : ℝ) : ℝ :=
  83  cosh (lam * distZ δ) - 1
  84
  85/-- J̃ ≥ 0. -/
  86theorem Jtilde_nonneg (lam : ℝ) (δ : ℝ) : 0 ≤ Jtilde lam δ := by
  87  unfold Jtilde
  88  linarith [one_le_cosh (lam * distZ δ)]
  89
  90/-- J̃ is 1-periodic in δ. -/
  91theorem Jtilde_periodic (lam : ℝ) (δ : ℝ) : Jtilde lam (δ + 1) = Jtilde lam δ := by
  92  unfold Jtilde
  93  rw [distZ_periodic]
  94
  95/-- J̃ is 1-periodic for general integer shifts. -/
  96theorem Jtilde_add_int (lam : ℝ) (δ : ℝ) (n : ℤ) :
  97    Jtilde lam (δ + ↑n) = Jtilde lam δ := by
  98  unfold Jtilde
  99  rw [distZ_add_int]
 100
 101/-- cosh(t) = 1 iff t = 0. -/
 102private lemma cosh_eq_one_iff (t : ℝ) : cosh t = 1 ↔ t = 0 := by
 103  constructor
 104  · intro h
 105    by_contra hne
 106    exact absurd h (ne_of_gt ((one_lt_cosh).mpr hne))
 107  · intro h; rw [h, cosh_zero]
 108
 109/-- J̃(lam, δ) = 0 iff δ is an integer, for lam ≠ 0. -/
 110theorem Jtilde_zero_iff {lam : ℝ} (hlam : lam ≠ 0) (δ : ℝ) :
 111    Jtilde lam δ = 0 ↔ ∃ n : ℤ, δ = ↑n := by
 112  unfold Jtilde
 113  constructor
 114  · intro h
 115    have h1 : cosh (lam * distZ δ) = 1 := by linarith
 116    have h2 : lam * distZ δ = 0 := (cosh_eq_one_iff _).mp h1
 117    have h3 : distZ δ = 0 := by
 118      rcases mul_eq_zero.mp h2 with h | h
 119      · exact absurd h hlam
 120      · exact h
 121    exact (distZ_eq_zero_iff δ).mp h3
 122  · intro ⟨n, hn⟩
 123    have hd : distZ δ = 0 := (distZ_eq_zero_iff δ).mpr ⟨n, hn⟩
 124    simp [hd, cosh_zero]
 125
 126/-! ### Stiffness (small-gradient regime)
 127
 128For small δ (near an integer), J̃(lam, δ) ≈ lam² δ² / 2.
 129The stiffness is κ = lam²/2. -/
 130
 131/-- Small-gradient lower bound: J̃(lam, δ) ≥ (lam · d_ℤ(δ))² / 2.
 132    This follows from the quadratic lower bound cosh(t) − 1 ≥ t²/2. -/
 133theorem Jtilde_stiffness_lb (lam : ℝ) (δ : ℝ) :
 134    (lam * distZ δ) ^ 2 / 2 ≤ Jtilde lam δ := by
 135  unfold Jtilde
 136  linarith [cosh_quadratic_lower_bound (lam * distZ δ)]
 137
 138/-- The GCIC stiffness for base φ: κ = (ln φ)²/2. -/
 139noncomputable def gcic_kappa : ℝ := (log Constants.phi) ^ 2 / 2
 140
 141theorem gcic_kappa_pos : 0 < gcic_kappa := by
 142  unfold gcic_kappa
 143  apply div_pos (pow_pos (log_pos Constants.one_lt_phi) 2) (by norm_num)
 144
 145/-! ### Phase rigidity (Result 3)
 146
 147On any finite connected graph, the reduced phase energy
 148  C̃_G[Θ] = Σ_{edges} J̃(lam, Θ_v − Θ_w)
 149is minimized exactly by constant phase fields. This follows from the
 150same nonnegativity/unique-zero mechanism as Result 1. -/
 151
 152/-- **RESULT 3 (Phase Rigidity).**
 153On a connected graph, if the reduced phase cost J̃(lam, Θ_v − Θ_w) vanishes on
 154every edge, then the phase field Θ is constant modulo integers. -/
 155theorem phase_rigidity {V : Type*} {adj : V → V → Prop}
 156    (hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
 157    {lam : ℝ} (hlam : lam ≠ 0) {Θ : V → ℝ}
 158    (hzero : ∀ v w, adj v w → Jtilde lam (Θ v - Θ w) = 0) :
 159    ∀ v w : V, ∃ n : ℤ, Θ v - Θ w = ↑n := by
 160  have hadj : ∀ v w, adj v w → ∃ n : ℤ, Θ v - Θ w = ↑n :=
 161    fun v w hvw => (Jtilde_zero_iff hlam _).mp (hzero v w hvw)
 162  intro v w
 163  induction hconn v w with
 164  | refl => exact ⟨0, by simp⟩
 165  | tail _ hbc ih =>
 166    obtain ⟨n₁, hn₁⟩ := ih
 167    obtain ⟨n₂, hn₂⟩ := hadj _ _ hbc
 168    exact ⟨n₁ + n₂, by push_cast; linarith⟩
 169
 170end IndisputableMonolith.Papers.GCIC.ReducedPhasePotential
 171