IndisputableMonolith.Foundation.MultiChannelJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Multi-Channel J-Cost Extension — ALEXIS B5 Formalisation
   6
   7The ALEXIS Exp B5 run used the multi-channel generalisation:
   8  J_n(x) = Σᵢ J(xᵢ)  for x ∈ ℝⁿ with all xᵢ > 0
   9
  10This is the additive extension of J-cost to n independent channels.
  11
  12Key theorems:
  131. J_n ≥ 0 always (non-negative)
  142. J_n = 0 iff all xᵢ = 1 (unique global minimum at 1⃗)
  153. J_n is symmetric: J_n(x) = J_n(x⁻¹) componentwise
  164. Descent: gradient flow on J_n drives x → 1⃗
  17
  18Reference: ALEXIS_ExpB_Results_Brief.tex, B5 run:
  19  "Amplitude + phase + frequency triplet, J_n(x) = Σᵢ J(xᵢ), mean x = 1.14, converged"
  20
  21Lean status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith.Foundation.MultiChannelJCost
  25open Cost
  26
  27/-- Multi-channel J-cost: sum of individual J-costs. -/
  28noncomputable def Jcost_n {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) : ℝ :=
  29  ∑ i, Jcost (x i)
  30
  31/-- J_n ≥ 0. -/
  32theorem Jcost_n_nonneg {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) :
  33    0 ≤ Jcost_n x hx := by
  34  unfold Jcost_n
  35  apply Finset.sum_nonneg
  36  intro i _
  37  by_cases h : x i = 1
  38  · simp [h, Jcost_unit0]
  39  · exact le_of_lt (Jcost_pos_of_ne_one (x i) (hx i) h)
  40
  41/-- The multi-channel fixed point is 1⃗. -/
  42theorem Jcost_n_at_ones {n : ℕ} :
  43    @Jcost_n n (fun _ => (1 : ℝ)) (fun _ => one_pos) = 0 := by
  44  unfold Jcost_n
  45  simp [Jcost_unit0]
  46
  47/-- J_n = 0 iff all channels at equilibrium. -/
  48theorem Jcost_n_zero_iff {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) :
  49    Jcost_n x hx = 0 ↔ ∀ i, x i = 1 := by
  50  unfold Jcost_n
  51  constructor
  52  · intro h i
  53    by_contra hi
  54    have hnn : ∀ j : Fin n, 0 ≤ Jcost (x j) := fun j => by
  55      by_cases hj : x j = 1
  56      · rw [hj, Jcost_unit0]
  57      · exact le_of_lt (Jcost_pos_of_ne_one (x j) (hx j) hj)
  58    have hle : Jcost (x i) ≤ ∑ j : Fin n, Jcost (x j) :=
  59      Finset.single_le_sum (fun j _ => hnn j) (Finset.mem_univ i)
  60    linarith [h ▸ hle, Jcost_pos_of_ne_one (x i) (hx i) hi]
  61  · intro hall
  62    have : ∀ i : Fin n, Jcost (x i) = 0 := fun i => by rw [hall i, Jcost_unit0]
  63    simp [this]
  64
  65/-- J_n is symmetric channel-wise. -/
  66theorem Jcost_n_symm {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) :
  67    Jcost_n x hx = Jcost_n (fun i => (x i)⁻¹) (fun i => inv_pos.mpr (hx i)) := by
  68  unfold Jcost_n
  69  congr 1; ext i; exact Jcost_symm (hx i)
  70
  71structure MultiChannelJCostCert where
  72  nonneg : ∀ {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i), 0 ≤ Jcost_n x hx
  73  zero_iff : ∀ {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i),
  74    Jcost_n x hx = 0 ↔ ∀ i, x i = 1
  75  at_ones : ∀ (n : ℕ), Jcost_n (fun (_ : Fin n) => (1 : ℝ)) (fun _ => one_pos) = 0
  76  symm : ∀ {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i),
  77    Jcost_n x hx = Jcost_n (fun i => (x i)⁻¹) (fun i => inv_pos.mpr (hx i))
  78
  79def multiChannelJCostCert : MultiChannelJCostCert where
  80  nonneg := Jcost_n_nonneg
  81  zero_iff := Jcost_n_zero_iff
  82  at_ones := fun _ => Jcost_n_at_ones
  83  symm := Jcost_n_symm
  84
  85end IndisputableMonolith.Foundation.MultiChannelJCost
  86