valueFunctional

formal source

  44noncomputable section
  45
  46/-- Agent recognition value functional: 1 - J(sigma_ratio). -/
  47def valueFunctional (sigma sigma_max : ℝ) : ℝ :=
  48  1 - Jcost (sigma / sigma_max)
  49
  50theorem valueFunctional_at_optimum (s : ℝ) (h : s ≠ 0) :
  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