theorem
proved
tactic proof
composition_law_forces_reciprocity
show as:
view Lean formalization →
formal statement (Lean)
139theorem composition_law_forces_reciprocity
140 (F : ℝ → ℝ)
141 (hNorm : IsNormalized F)
142 (hComp : SatisfiesCompositionLaw F) :
143 IsReciprocalCost F := by
proof body
Tactic-mode proof.
144 intro x hx
145 let Hf : ℝ → ℝ := H F
146 have h_H0 : Hf 0 = 1 := by
147 dsimp [Hf]
148 simpa [H, G, IsNormalized] using hNorm
149 have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
150 have h_direct : DirectCoshAdd (G F) := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
151 have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
152 intro t u
153 have hG := h_direct t u
154 have h_goal :
155 (G F (t + u) + 1) + (G F (t - u) + 1) = 2 * (G F t + 1) * (G F u + 1) := by
156 calc
157 (G F (t + u) + 1) + (G F (t - u) + 1)
158 = (G F (t + u) + G F (t - u)) + 2 := by ring
159 _ = (2 * (G F t * G F u) + 2 * (G F t + G F u)) + 2 := by simpa [hG]
160 _ = 2 * (G F t + 1) * (G F u + 1) := by ring
161 simpa [Hf, H] using h_goal
162 have h_even : Function.Even Hf := dAlembert_even Hf h_H0 h_dAlembert
163 have h_even_at_log := h_even (Real.log x)
164 have h_eq_plus :
165 F x + 1 = F x⁻¹ + 1 := by
166 simpa [Hf, H, G, Real.exp_log hx, Real.exp_neg] using h_even_at_log.symm
167 linarith
168
169/-- `C²` d'Alembert solutions are determined by calibration and equal `cosh`. -/