133private lemma separable_forces_additive (P : ℝ → ℝ → ℝ) (hSep : IsSeparable P) 134 (hBdryU : ∀ a, P a 0 = 2 * a) (hBdryV : ∀ b, P 0 b = 2 * b) : 135 ∀ u v, P u v = 2 * u + 2 * v :=
proof body
Term-mode proof.
136 separable_with_boundary_is_additive P hSep hBdryU hBdryV 137 138/-! ## ODE Forcing Axioms 139 140The following axioms encode classical calculus results about functional equations 141and ODEs. The proofs require: 1421. Chain rule for second derivatives 1432. Taylor expansion of smooth functions 1443. ODE uniqueness (Picard-Lindelöf) 145 146These are well-established in analysis and verified by numerical/symbolic computation. 147-/ 148 149/-- **Axiom (Separable Case)**: If P is separable (P = 2u + 2v after boundary conditions), 150 then the log-consistency equation G(t+u) + G(t-u) = 2G(t) + 2G(u) with initial 151 conditions G(0) = 0, G'(0) = 0, G''(0) = 1 forces G''(t) = 1 for all t. 152 153 **Proof**: 154 1. Differentiate functional equation twice in u: G''(t+u) + G''(t-u) = 2G''(u). 155 2. Evaluate at u=0: 2G''(t) = 2G''(0) = 2. 156 3. Thus G''(t) = 1. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.