washburn_uniqueness

proof body

Tactic-mode proof.

 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
 792  have h_H0 : Hf 0 = 1 := by
 793    show H F 0 = 1
 794    simp only [H, G, Real.exp_zero]
 795    -- Goal is F 1 + 1 = 1, and hNorm says F 1 = 0
 796    rw [hNorm]
 797    ring
 798
 799  -- Step 3: G is continuous (F continuous on (0,∞), exp continuous)
 800  have h_G_cont : Continuous Gf := by
 801    have h := ContinuousOn.comp_continuous hCont continuous_exp
 802    have h' : Continuous (fun t => F (Real.exp t)) :=
 803      h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
 804    simp [Gf, G] at h'
 805    exact h'
 806  have h_H_cont : Continuous Hf := by
 807    simpa [Hf, H] using h_G_cont.add continuous_const
 808
 809  -- Step 4: Convert CoshAddIdentity to d'Alembert equation for H
 810  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
 811  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
 812    intro t u
 813    have hG := h_direct t u
 814    have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
 815      calc (Gf (t + u) + 1) + (Gf (t - u) + 1)
 816          = (Gf (t + u) + Gf (t - u)) + 2 := by ring
 817        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simp [hG]
 818        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
 819    simp [Hf, H, Gf] at h_goal
 820    exact h_goal
 821
 822  -- Step 5: Second derivative condition
 823  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
 824    have hG_d2 : deriv (deriv Gf) 0 = 1 := by simpa [Gf, G] using hCalib
 825    have hderiv : deriv Hf = deriv Gf := by
 826      funext t
 827      change deriv (fun y => Gf y + 1) t = deriv Gf t
 828      simpa using (deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ)))
 829    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
 830    exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
 831
 832  -- Step 6: Apply d'Alembert uniqueness theorem
 833  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
 834    dAlembert_cosh_solution Hf h_H0 h_H_cont h_dAlembert h_H_d2
 835      h_smooth h_ode h_cont h_diff h_boot
 836
 837  -- Step 7: Unshift to get G = cosh - 1
 838  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
 839    intro t
 840    have hH := h_H_cosh t
 841    have hH' : Gf t + 1 = Real.cosh t := by simpa [Hf, H, Gf] using hH
 842    linarith
 843
 844  -- Step 8: Convert back via log parametrization
 845  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
 846  have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
 847    Jcost_G_eq_cosh_sub_one (Real.log x)
 848  calc F x
 849      = F (Real.exp (Real.log x)) := by rw [ht]
 850    _ = Gf (Real.log x) := rfl
 851    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
 852    _ = G Cost.Jcost (Real.log x) := by simpa using hJG.symm
 853    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
 854-- ... 6 more lines elided ...