IndisputableMonolith.Cost.Ndim.Neutrality

   1import IndisputableMonolith.Cost.Ndim.Core
   2
   3/-!
   4# Ledger neutrality surface
   5-/
   6
   7namespace IndisputableMonolith
   8namespace Cost
   9namespace Ndim
  10
  11/-- Aggregate equals one exactly when the weighted log sum is zero. -/
  12theorem aggregate_eq_one_iff {n : ℕ} (α x : Vec n) :
  13    aggregate α x = 1 ↔ dot α (logVec x) = 0 := by
  14  unfold aggregate
  15  constructor
  16  · intro h
  17    have : Real.exp (dot α (logVec x)) = Real.exp 0 := by simpa using h
  18    exact Real.exp_injective this
  19  · intro h
  20    simp [h]
  21
  22/-- Zero-cost iff weighted log sum vanishes. -/
  23theorem zero_cost_iff_dot_zero {n : ℕ} (α x : Vec n) :
  24    JcostN α x = 0 ↔ dot α (logVec x) = 0 :=
  25  JcostN_eq_zero_iff α x
  26
  27/-- Zero-cost iff aggregate equals one. -/
  28theorem zero_cost_iff_aggregate_one {n : ℕ} (α x : Vec n) :
  29    JcostN α x = 0 ↔ aggregate α x = 1 := by
  30  constructor
  31  · intro h
  32    exact (aggregate_eq_one_iff α x).2 ((zero_cost_iff_dot_zero α x).1 h)
  33  · intro h
  34    exact (zero_cost_iff_dot_zero α x).2 ((aggregate_eq_one_iff α x).1 h)
  35
  36end Ndim
  37end Cost
  38end IndisputableMonolith
  39