valueFunctional_nonneg

formal source

  51    valueFunctional s s = 1 := by
  52  unfold valueFunctional; rw [div_self h, Jcost_unit0]; ring
  53
  54theorem valueFunctional_nonneg (s s_max : ℝ) (hs : 0 < s) (hsm : 0 < s_max)
  55    (h_le : Jcost (s / s_max) ≤ 1) :
  56    0 ≤ valueFunctional s s_max := by
  57  unfold valueFunctional; linarith
  58
  59/-- Consent criterion: action is consensual if V does not decrease. -/
  60def IsConsensual (sigma_before sigma_after sigma_max : ℝ) : Prop :=
  61  valueFunctional sigma_after sigma_max ≥ valueFunctional sigma_before sigma_max
  62
  63/-- Consensual action preserves or improves value. -/
  64theorem consensual_iff_jcost_nondecreasing
  65    (s_b s_a s_max : ℝ) (hs_b : 0 < s_b) (hs_a : 0 < s_a) (hsm : 0 < s_max) :
  66    IsConsensual s_b s_a s_max ↔
  67    Jcost (s_a / s_max) ≤ Jcost (s_b / s_max) := by
  68  unfold IsConsensual valueFunctional; constructor
  69  · intro h; linarith
  70  · intro h; linarith
  71
  72/-- A σ-preserving action that does not increase J-cost is consensual. -/
  73theorem sigma_preserving_consensual
  74    (sigma sigma_max : ℝ) (hs : 0 < sigma) (hsm : 0 < sigma_max) :
  75    IsConsensual sigma sigma sigma_max := by
  76  unfold IsConsensual; exact le_refl _
  77
  78structure ConsentInterfaceCert where
  79  value_at_opt : ∀ s : ℝ, s ≠ 0 → valueFunctional s s = 1
  80  sigma_pres_consensual : ∀ s s_max : ℝ, 0 < s → 0 < s_max →
  81    IsConsensual s s s_max
  82
  83noncomputable def cert : ConsentInterfaceCert where
  84  value_at_opt := valueFunctional_at_optimum