pith. machine review for the scientific record. sign in
theorem proved term proof

ultimate_inevitability

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  87theorem ultimate_inevitability :
  88    -- The primitive requirements
  89    IsSymmetricComparison Cost.Jcost ∧
  90    IsNormalizedCost Cost.Jcost ∧
  91    HasMultiplicativeConsistency Cost.Jcost ∧
  92    -- The consequences (all proved)
  93    (∀ x : ℝ, 0 < x → Cost.Jcost x = (x + x⁻¹) / 2 - 1) ∧
  94    (∀ P : ℝ → ℝ → ℝ,
  95      (∀ x y, 0 < x → 0 < y → Cost.Jcost (x*y) + Cost.Jcost (x/y) = P (Cost.Jcost x) (Cost.Jcost y)) →
  96      ∀ u v, 0 ≤ u → 0 ≤ v → P u v = 2*u*v + 2*u + 2*v) := by

proof body

Term-mode proof.

  97  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  98  -- Symmetry
  99  · intro x hx
 100    simp only [Cost.Jcost]
 101    ring
 102  -- Normalization
 103  · simp only [Cost.Jcost, inv_one]
 104    ring
 105  -- Consistency (existence of P)
 106  · use fun u v => 2*u*v + 2*u + 2*v
 107    intro x y hx hy
 108    exact J_computes_P x y hx hy
 109  -- F = J (definitional)
 110  · intro x _
 111    simp only [Cost.Jcost]
 112  -- P uniqueness (from Unconditional)
 113  · exact rcl_unconditional
 114
 115/-! ## What Each Requirement Means -/
 116
 117/-- Symmetry is NOT negotiable: without it, comparison is directional. -/

depends on (27)

Lean names referenced from this declaration's body.