J_nonneg

formal source

  72  Jcost_symm hx
  73
  74/-- **Non-negativity**: All costs are non-negative on ℝ₊. -/
  75theorem J_nonneg (x : ℝ) (hx : 0 < x) : 0 ≤ J x :=
  76  Jcost_nonneg hx
  77
  78/-- **Defect characterization**: J(x) = (x − 1)²/(2x) for x ≠ 0. -/
  79theorem J_defect_form (x : ℝ) (hx : x ≠ 0) : J x = (x - 1) ^ 2 / (2 * x) :=
  80  Jcost_eq_sq hx
  81
  82/-! ## §2. The Recognition Composition Law (RCL) -/
  83
  84/-- The **Recognition Composition Law**: the ONE primitive of Recognition Science.
  85
  86    J(xy) + J(x/y) = 2·J(x)·J(y) + 2·J(x) + 2·J(y)
  87
  88    In the log-coordinate form (t = ln x, u = ln y), this becomes:
  89    G(t+u) + G(t−u) = 2·G(t)·G(u) + 2·(G(t) + G(u))
  90
  91    which is a calibrated multiplicative form of the d'Alembert functional equation. -/
  92def SatisfiesRCL (F : ℝ → ℝ) : Prop :=
  93  ∀ x y : ℝ, 0 < x → 0 < y →
  94    F (x * y) + F (x / y) = 2 * F x * F y + 2 * F x + 2 * F y
  95
  96/-- **THEOREM: J satisfies the RCL.**
  97    This is the foundational identity — everything else follows. -/
  98theorem RCL_holds : SatisfiesRCL J := by
  99  intro x y hx hy
 100  unfold J Jcost
 101  have hx0 : x ≠ 0 := ne_of_gt hx
 102  have hy0 : y ≠ 0 := ne_of_gt hy
 103  have hxy0 : x * y ≠ 0 := mul_ne_zero hx0 hy0
 104  have hxy_div0 : x / y ≠ 0 := div_ne_zero hx0 hy0
 105  field_simp [hx0, hy0, hxy0, hxy_div0]