bilinear_family_reduction

proof body

Tactic-mode proof.

 204      let H := fun t => 1 + (c/2) * G t
 205      ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u := by
 206  intro G H t u
 207  simp only [H, G]
 208  -- We need to prove:
 209  -- (1 + c/2*F(exp(t+u))) + (1 + c/2*F(exp(t-u))) = 2 * (1 + c/2*F(exp t)) * (1 + c/2*F(exp u))
 210  -- LHS = 2 + c/2 * (F(xy) + F(x/y))  where x=exp t, y=exp u
 211  -- RHS = 2 * (1 + c/2*Fx + c/2*Fy + c^2/4*Fx*Fy)
 212  --     = 2 + c*Fx + c*Fy + c^2/2*Fx*Fy
 213  --
 214  -- LHS using bilinear:
 215  -- LHS = 2 + c/2 * (2Fx + 2Fy + c*Fx*Fy)
 216  --     = 2 + c*Fx + c*Fy + c^2/2*Fx*Fy
 217  --
 218  -- LHS = RHS. QED.
 219  let x := Real.exp t
 220  let y := Real.exp u
 221  have h_eq := h_bilinear x y
 222  -- Transform using exp_add and exp_sub
 223  have hxy : Real.exp t * Real.exp u = Real.exp (t + u) := (Real.exp_add t u).symm
 224  have hxy' : Real.exp t / Real.exp u = Real.exp (t - u) := by
 225    rw [Real.exp_sub]
 226  -- The goal is: H(t+u) + H(t-u) = 2 * H(t) * H(u)
 227  -- where H(t) = 1 + (c/2) * F(exp(t))
 228  -- LHS = (1 + c/2*F(exp(t+u))) + (1 + c/2*F(exp(t-u)))
 229  --     = 2 + c/2*(F(exp(t+u)) + F(exp(t-u)))
 230  --     = 2 + c/2*(F(x*y) + F(x/y))
 231  --     = 2 + c/2*(2Fx + 2Fy + c*Fx*Fy)  [by h_eq]
 232  --     = 2 + c*Fx + c*Fy + c²/2*Fx*Fy
 233  -- RHS = 2*(1 + c/2*Fx)*(1 + c/2*Fy)
 234  --     = 2*(1 + c/2*Fx + c/2*Fy + c²/4*Fx*Fy)
 235  --     = 2 + c*Fx + c*Fy + c²/2*Fx*Fy
 236  -- LHS = RHS ✓
 237  -- The goal involves H and G which are let-bindings
 238  -- We need to show: H(t+u) + H(t-u) = 2 * H(t) * H(u)
 239  -- With H(s) = 1 + (c/2) * G(s) = 1 + (c/2) * F(exp(s))
 240  -- Note: x = exp(t), y = exp(u), so x*y = exp(t+u), x/y = exp(t-u)
 241  -- h_eq : F(x*y) + F(x/y) = 2Fx + 2Fy + c*Fx*Fy
 242  -- Rewrite the goal using hxy and hxy'
 243  have goal_lhs : F (Real.exp (t + u)) = F (x * y) := by rw [hxy]
 244  have goal_lhs' : F (Real.exp (t - u)) = F (x / y) := by rw [hxy']
 245  rw [goal_lhs, goal_lhs']
 246  -- Now the goal is in terms of F(x*y), F(x/y), F(x), F(y)
 247  -- Use h_eq to substitute F(x*y) + F(x/y)
 248  -- Actually, we need to prove an algebraic identity
 249  -- LHS = 1 + c/2*F(xy) + 1 + c/2*F(x/y) = 2 + c/2*(F(xy) + F(x/y))
 250  -- RHS = 2*(1 + c/2*Fx)*(1 + c/2*Fy)
 251  --     = 2 + c*Fx + c*Fy + c²/2*Fx*Fy
 252  -- Using h_eq: F(xy) + F(x/y) = 2Fx + 2Fy + c*Fx*Fy
 253  -- LHS = 2 + c/2*(2Fx + 2Fy + c*Fx*Fy)
 254  --     = 2 + c*Fx + c*Fy + c²/2*Fx*Fy
 255  --     = RHS ✓
 256  calc 1 + c / 2 * F (x * y) + (1 + c / 2 * F (x / y))
 257      = 2 + c / 2 * (F (x * y) + F (x / y)) := by ring
 258    _ = 2 + c / 2 * (2 * F x + 2 * F y + c * F x * F y) := by rw [h_eq]
 259    _ = 2 * (1 + c / 2 * F x) * (1 + c / 2 * F y) := by ring
 260
 261/-! ## Step 5: Calibration Fixes the Coefficient c = 2 -/
 262
 263/-!
 264`calibration_forces_c_eq_two` was an older, “paper-facing” lemma that tried to
 265pin the remaining bilinear parameter `c` by specializing to the canonical solution.
 266
 267For this paper (1.2), the stronger and cleaner story is:
 268- this module forces the **bilinear family** `2u + 2v + c·uv` from polynomial consistency;
 269- the reduction to classical d’Alembert is handled in `bilinear_family_reduction`;
 270- the choice `c = 2` is a **normalization of units** (handled elsewhere, together with solution classification).
 271-/
 272
 273/-! ## The Main Theorem: Bilinear Family is Forced -/
 274
 275/-- **THEOREM: The consistency requirement forces the unique bilinear family.**
 276
 277Given:
 2781. F : ℝ₊ → ℝ is a cost functional
 2792. F is symmetric: F(x) = F(1/x)
 2803. F is normalized: F(1) = 0
 2814. F has multiplicative consistency: F(xy) + F(x/y) = P(F(x), F(y)) for some **symmetric quadratic polynomial** P
 2825. F is non-trivial (not constant 0)
 283
 284-- ... 6 more lines elided ...