`HasMultiplicativeConsistency`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.DAlembert.Ultimate
domain: Foundation
line: 72 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.DAlembert.Ultimate on GitHub at line 72.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  69
  70/-- Consistency: F(xy) + F(x/y) = P(F(x), F(y)) for some P.
  71    This is the DEFINITION of multiplicative consistency. -/
  72def HasMultiplicativeConsistency (F : ℝ → ℝ) : Prop :=
  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-/
  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
  97  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  98  -- Symmetry
  99  · intro x hx
 100    simp only [Cost.Jcost]
 101    ring
 102  -- Normalization

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.