washburn_uniqueness

formal source

 758
 759This theorem corresponds to Theorem 1.1 in:
 760  J. Washburn & M. Zlatanović, "Uniqueness of the Canonical Reciprocal Cost" -/
 761theorem washburn_uniqueness (F : ℝ → ℝ)
 762    (hRecip : IsReciprocalCost F)
 763    (hNorm : IsNormalized F)
 764    (hComp : SatisfiesCompositionLaw F)
 765    (hCalib : IsCalibrated F)
 766    (hCont : ContinuousOn F (Set.Ioi 0))
 767    -- Regularity hypotheses (from Aczél theory)
 768    (h_smooth : dAlembert_continuous_implies_smooth_hypothesis (H F))
 769    (h_ode : dAlembert_to_ODE_hypothesis (H F))
 770    (h_cont : ode_regularity_continuous_hypothesis (H F))
 771    (h_diff : ode_regularity_differentiable_hypothesis (H F))
 772    (h_boot : ode_linear_regularity_bootstrap_hypothesis (H F)) :
 773    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 774  -- The proof follows the structure of T5_uniqueness_complete:
 775  -- 1. Convert composition law to CoshAddIdentity on G
 776  -- 2. Shift to H = G + 1 to get standard d'Alembert equation
 777  -- 3. Apply Aczél's theorem: continuous d'Alembert solutions are cosh
 778  -- 4. Calibration H''(0) = 1 selects cosh (not cos or constant)
 779  -- 5. Unshift: G = cosh - 1, hence F = J
 780  intro x hx
 781  -- Convert hypotheses to the required format
 782  have hSymm : ∀ {y}, 0 < y → F y = F y⁻¹ := fun {y} hy => hRecip y hy
 783  have hCoshAdd : CoshAddIdentity F := composition_law_equiv_coshAdd F |>.mp hComp
 784
 785  -- Step 1: Set up G and H
 786  let Gf : ℝ → ℝ := G F
 787  let Hf : ℝ → ℝ := H F
 788
 789  -- Step 2: Derive key properties of G and H
 790  have h_G_even : Function.Even Gf := G_even_of_reciprocal_symmetry F hSymm
 791  have h_G0 : Gf 0 = 0 := G_zero_of_unit F hNorm