IndisputableMonolith.Foundation.GroundStateDynamics

   1import Mathlib
   2import IndisputableMonolith.Foundation.VariationalDynamics
   3
   4namespace IndisputableMonolith
   5namespace Foundation
   6namespace GroundStateDynamics
   7
   8open VariationalDynamics
   9open InitialCondition
  10
  11/-!
  12# Ground State from Stable Variational Dynamics
  13
  14This module extracts the B4-style dynamic statement from the existing
  15variational ledger update rule:
  16
  17- equilibria coincide with variational minimizers;
  18- in a zero-charge sector, the unique equilibrium is the unity configuration;
  19- for a one-channel ratio observable, stability therefore forces `r = 1`.
  20-/
  21
  22/-- Any equilibrium coincides with the uniform minimizer of its conserved sector. -/
  23theorem equilibrium_entries_eq_uniform {N : ℕ} (hN : 0 < N)
  24    (c : Configuration N) (hEq : IsEquilibrium c) :
  25    c.entries = (uniform_config hN (log_charge c)).entries := by
  26  exact variational_step_unique hN c c (uniform_config hN (log_charge c))
  27    hEq (uniform_is_variational_successor hN c)
  28
  29/-- The zero-charge equilibrium is the unity configuration. -/
  30theorem zero_charge_equilibrium_is_unity {N : ℕ} (hN : 0 < N)
  31    (c : Configuration N) (hEq : IsEquilibrium c)
  32    (hCharge : log_charge c = 0) :
  33    c.entries = (unity_config N hN).entries := by
  34  calc
  35    c.entries = (uniform_config hN (log_charge c)).entries :=
  36      equilibrium_entries_eq_uniform hN c hEq
  37    _ = (uniform_config hN 0).entries := by rw [hCharge]
  38    _ = (unity_config N hN).entries := by
  39      funext i
  40      simp [uniform_config, unity_config]
  41
  42/-- A one-channel ratio packaged as a `Configuration 1`. -/
  43def ratioConfig (r : ℝ) (hr : 0 < r) : Configuration 1 where
  44  entries := fun _ => r
  45  entries_pos := fun _ => hr
  46
  47@[simp] theorem ratioConfig_entry (r : ℝ) (hr : 0 < r) (i : Fin 1) :
  48    (ratioConfig r hr).entries i = r := rfl
  49
  50@[simp] theorem ratioConfig_log_charge (r : ℝ) (hr : 0 < r) :
  51    log_charge (ratioConfig r hr) = Real.log r := by
  52  unfold log_charge ratioConfig
  53  simp
  54
  55/-- Stable one-channel ratios in the neutral sector are forced to unity. -/
  56theorem stable_zero_charge_ratio_eq_one (r : ℝ) (hr : 0 < r)
  57    (hEq : IsEquilibrium (ratioConfig r hr))
  58    (hCharge : log_charge (ratioConfig r hr) = 0) :
  59    r = 1 := by
  60  have hEntries :
  61      (ratioConfig r hr).entries = (unity_config 1 (by norm_num)).entries :=
  62    zero_charge_equilibrium_is_unity (N := 1) (by norm_num) (ratioConfig r hr) hEq hCharge
  63  have h0 := congrFun hEntries ⟨0, by simp⟩
  64  simpa [ratioConfig, unity_config] using h0
  65
  66end GroundStateDynamics
  67end Foundation
  68end IndisputableMonolith
  69