separable_forces_additive

formal source

 130-/
 131
 132/-- Helper: If P is separable with boundary conditions, P must be additive. -/
 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 :=
 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. -/
 157theorem separable_forces_flat_ode :
 158    ∀ G : ℝ → ℝ,
 159    (∀ t u, G (t + u) + G (t - u) = 2 * G t + 2 * G u) →
 160    G 0 = 0 →
 161    deriv G 0 = 0 →
 162    deriv (deriv G) 0 = 1 →
 163    ContDiff ℝ 2 G →