theorem
proved
term proof
differentiation_key_lemma
show as:
view Lean formalization →
formal statement (Lean)
524theorem differentiation_key_lemma (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
525 (hNorm : F 1 = 0)
526 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
527 (hSmooth : ContDiff ℝ 2 F)
528 (hCalib : deriv (deriv (G_of F)) 0 = 1)
529 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
530 (hPsmooth : ContDiff ℝ 2 (fun p : ℝ × ℝ => P p.1 p.2))
531 -- Boundary conditions derived from consistency
532 (hBdryU : ∀ u, P u 0 = 2 * u)
533 (hBdryV : ∀ v, P 0 v = 2 * v) :
534 -- If P is separable (additive), then G'' = 1 (flat)
535 -- If P is entangling, then G'' = G + 1 (hyperbolic)
536 (IsSeparable P → SatisfiesFlatODE (G_of F)) ∧
537 (IsEntangling P → SatisfiesHyperbolicODE (G_of F)) := by
proof body
Term-mode proof.
538 constructor
539 · -- Separable case: P = 2u + 2v, so use separable_combiner_forces_flat
540 intro hSep
541 exact separable_combiner_forces_flat F P hNorm hSymm hSmooth hCalib hCons hSep hBdryU hBdryV
542 · -- Entangling case: P = 2uv + 2u + 2v (RCL form), use entangling_combiner_forces_hyperbolic
543 intro hEnt
544 have hRCL : ∀ u v, P u v = 2 * u * v + 2 * u + 2 * v :=
545 entangling_with_boundary_is_RCL P hEnt hBdryU hBdryV hPsmooth
546 exact entangling_combiner_forces_hyperbolic F P hNorm hSymm hSmooth hCalib hCons hEnt hRCL
547
548/-! ## The Bridge Theorem -/
549
550/-- **Axiom (Entangling Combiner is RCL)**: If P is entangling and satisfies the
551 boundary conditions P(u,0) = 2u and P(0,v) = 2v, then P has the RCL form.
552
553 Proof sketch: From separable_implies_zero_mixed_diff, if P is not separable,
554 the mixed difference is nonzero. Combined with boundary conditions and
555 continuity, the only bilinear extension with the right boundaries is 2uv + 2u + 2v. -/