flat_ode_unique
plain-language theorem explainer
Uniqueness theorem for the flat second-order ODE: any C² function G:ℝ→ℝ obeying G''=1 with G(0)=G'(0)=0 must equal t²/2. Workers on the analytic bridge from consistency axioms to d'Alembert structure cite it to exclude non-quadratic solutions in the additive case. Proof constructs the deviation function f=G−t²/2, shows f''=0, deduces f' constant via local constancy, forces the constant to zero from the initial derivative, then repeats for f itself.
Claim. Let $G : ℝ → ℝ$ be twice continuously differentiable. Suppose $G''(t) = 1$ for all real $t$, $G(0) = 0$, and $G'(0) = 0$. Then $G(t) = t^2 / 2$ for all $t$.
background
The AnalyticBridge module proves that structural consistency plus interaction forces the d'Alembert functional equation on the log-lifted combiner H(t) = F(e^t) + 1. This flat ODE uniqueness result supplies the differential characterization of the non-interacting (additive) sector within that case analysis. SatisfiesFlatODE G encodes the condition that the second derivative equals one everywhere, arising when the interaction term Q vanishes.
proof idea
Tactic-mode proof in four blocks. Define f := G - t²/2 and compute f'' = 0 directly from the ODE hypothesis and ContDiff assumptions using deriv_sub and deriv_div_const. Establish that deriv f is locally constant by applying IsLocallyConstant.of_hasDeriv to the fact that its derivative vanishes. Use the initial condition deriv G 0 = 0 to force this constant to zero. Repeat the local-constancy argument on f itself together with f(0) = 0 to conclude f ≡ 0.
why it matters
The result closes the additive branch of the bridge theorem by showing that the flat ODE forces the quadratic solution under the given boundary conditions. It thereby supports the module claim that interaction is required to reach the hyperbolic (cosh) solutions of d'Alembert structure. Within Recognition Science it supplies the differential counterpart to the J-uniqueness step (T5) in the forcing chain when the interaction term is absent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.