pith. machine review for the scientific record. sign in
def definition def or abbrev

HasMultiplicativeConsistency

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)

  72def HasMultiplicativeConsistency (F : ℝ → ℝ) : Prop :=

proof body

Definition body.

  73  ∃ P : ℝ → ℝ → ℝ, ∀ x y : ℝ, 0 < x → 0 < y →
  74    F (x * y) + F (x / y) = P (F x) (F y)
  75
  76/-! ## The Ultimate Theorem -/
  77
  78/-- **THEOREM (Ultimate Inevitability)**
  79
  80The three primitive requirements (symmetry, normalization, consistency)
  81plus regularity (smoothness, calibration) uniquely determine:
  821. F = J
  832. P = the RCL
  84
  85There is no weaker foundation that still defines "cost of comparison."
  86-/

used by (20)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (18)

Lean names referenced from this declaration's body.