normalization_is_essential

formal source

 122  simp at this
 123
 124/-- Normalization is NOT negotiable: without it, "no deviation" has cost. -/
 125theorem normalization_is_essential :
 126    ¬ IsNormalizedCost (fun x => (x + x⁻¹) / 2) := by
 127  intro h
 128  simp [IsNormalizedCost] at h
 129
 130/-- Consistency IS what defines compositional structure.
 131    If you don't have it, you don't have a compositional cost theory. -/
 132theorem consistency_defines_composition :
 133    HasMultiplicativeConsistency Cost.Jcost := by
 134  use fun u v => 2*u*v + 2*u + 2*v
 135  intro x y hx hy
 136  exact J_computes_P x y hx hy
 137
 138/-! ## The Philosophical Point -/
 139
 140/-- The RCL is not a choice. It's what "comparison" IS.
 141
 142    Just as the Pythagorean theorem is not a choice in Euclidean geometry
 143    (it follows from the axioms), the RCL is not a choice in comparison theory
 144    (it follows from symmetry + normalization + consistency).
 145
 146    But unlike Euclidean geometry (where non-Euclidean alternatives exist),
 147    there is NO alternative to the RCL. Any symmetric, normalized, consistent
 148    cost function is J, and its combiner is the RCL.
 149
 150    This is the deepest sense in which Recognition Science is "inevitable."
 151-/
 152theorem rcl_is_inevitable :
 153    ∀ P : ℝ → ℝ → ℝ,
 154    (∀ x y, 0 < x → 0 < y →
 155      Cost.Jcost (x*y) + Cost.Jcost (x/y) = P (Cost.Jcost x) (Cost.Jcost y)) →