IndisputableMonolith.Information.JCostNecessity

   1import IndisputableMonolith.Cost
   2import IndisputableMonolith.Cost.Convexity
   3
   4/-!
   5# Phase 7.5.1: J-Cost Uniqueness from Information Theory
   6
   7This module packages the information-cost side of the J-cost story.
   8
   9Symmetry, a minimum at `1`, and convexity do not by themselves force the
  10canonical reciprocal cost.  The theorem below states the calibrated-family
  11claim used here: inside the reciprocal affine family `a * (x + 1/x) + b`,
  12the unit minimum and calibration `a = 1/2` force `J`.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Information
  17
  18open Cost
  19
  20/-- **DEFINITION: Recognition Information Cost**
  21    The cost function F must satisfy:
  22    1. Symmetric: F(x) = F(1/x) (Recognition is bi-directional).
  23    2. Minimum: F(1) = 0 (Balanced state has zero cost).
  24    3. Convexity: F is strictly convex (Unique stable equilibrium). -/
  25structure InformationCost (F : ℝ → ℝ) : Prop where
  26  symmetric : ∀ {x : ℝ}, x > 0 → F x = F (1 / x)
  27  minimum   : F 1 = 0
  28  convex    : StrictConvexOn ℝ (Set.Ioi 0) F
  29
  30/-- **THEOREM: calibrated reciprocal-affine uniqueness.**
  31    If an information cost lies in the reciprocal affine family and carries
  32    the RS calibration `a = 1/2`, then the zero-at-one condition forces it
  33    to be the canonical J-cost on positive ratios. -/
  34theorem jcost_is_unique (F : ℝ → ℝ) (h : InformationCost F)
  35    (a b : ℝ) (h_form : ∀ x > 0, F x = a * (x + 1 / x) + b)
  36    (h_calibrated : a = 1 / 2) :
  37    ∀ x > 0, F x = Cost.Jcost x := by
  38  intro x hx
  39  have h1 : F 1 = 0 := h.minimum
  40  rw [h_form 1 (by norm_num)] at h1
  41  have hb : b = -2 * a := by linarith
  42  have hb_val : b = -1 := by linarith
  43  rw [h_form x hx, h_calibrated, hb_val]
  44  unfold Cost.Jcost
  45  field_simp [ne_of_gt hx]
  46  ring
  47
  48/-- **Canonical J-Cost satisfies InformationCost** -/
  49theorem jcost_satisfies_information_cost : InformationCost Cost.Jcost := {
  50  symmetric := fun {x} hx => by
  51    simpa [one_div] using (Cost.Jcost_symm hx)
  52  minimum := Cost.Jcost_unit0
  53  convex := Cost.Jcost_strictConvexOn_pos
  54}
  55
  56end Information
  57end IndisputableMonolith
  58