theorem
proved
tactic proof
separable_forces_flat_ode
show as:
view Lean formalization →
formal statement (Lean)
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 →
164 SatisfiesFlatODE G := by
proof body
Tactic-mode proof.
165 intro G hFE hG0 hGderiv0 hCalib hSmooth t
166 -- Differentiate hFE twice with respect to u at u=0
167 -- LHS: d²/du² [G(t+u) + G(t-u)] = G''(t+u) + G''(t-u) => 2G''(t) at u=0
168 -- RHS: d²/du² [2G(t) + 2G(u)] = 2G''(u) => 2G''(0) = 2 at u=0
169 let f := fun u => G (t + u) + G (t - u)
170 let g := fun u => 2 * G t + 2 * G u
171 have hfg : f = g := by funext u; exact hFE t u
172
173 -- First derivative of f
174 have h_deriv_f : ∀ u, deriv f u = deriv G (t + u) - deriv G (t - u) := by
175 intro u
176 have h1 : HasDerivAt (fun u => G (t + u)) (deriv G (t + u)) u := by
177 have hd : HasDerivAt G (deriv G (t + u)) (t + u) := hSmooth.differentiable (by decide) |>.differentiableAt.hasDerivAt
178 exact hd.comp u (hasDerivAt_id u |>.const_add t)
179 have h2 : HasDerivAt (fun u => G (t - u)) (- deriv G (t - u)) u := by
180 have hd : HasDerivAt G (deriv G (t - u)) (t - u) := hSmooth.differentiable (by decide) |>.differentiableAt.hasDerivAt
181 have hsub : HasDerivAt (fun u => t - u) (-1) u := by
182 apply HasDerivAt.sub (hasDerivAt_const u t) (hasDerivAt_id u)
183 exact hd.comp u hsub
184 exact (h1.add h2).deriv
185
186 -- Second derivative of f at 0
187 have h_2deriv_f_0 : deriv (deriv f) 0 = 2 * deriv (deriv G) t := by
188 simp_rw [h_deriv_f]
189 have h1 : HasDerivAt (fun u => deriv G (t + u)) (deriv (deriv G) t) 0 := by
190 have hd : HasDerivAt (deriv G) (deriv (deriv G) t) t :=
191 hSmooth.iterate_deriv 1 1 |>.differentiable (by decide) |>.differentiableAt.hasDerivAt
192 exact hd.comp 0 (hasDerivAt_id 0 |>.const_add t)
193 have h2 : HasDerivAt (fun u => - deriv G (t - u)) (deriv (deriv G) t) 0 := by
194 have hd : HasDerivAt (deriv G) (deriv (deriv G) t) t :=
195 hSmooth.iterate_deriv 1 1 |>.differentiable (by decide) |>.differentiableAt.hasDerivAt
196 have hsub : HasDerivAt (fun u => t - u) (-1) 0 := by
197 apply HasDerivAt.sub (hasDerivAt_const 0 t) (hasDerivAt_id 0)
198 have h_neg_deriv := hd.comp 0 hsub
199 -- h_neg_deriv is deriv of u => deriv G (t - u), which is -G''(t)
200 -- So deriv of u => -deriv G (t - u) is G''(t)
201 convert h_neg_deriv.neg; ring
202 exact (h1.add h2).deriv
203
204 -- Second derivative of g at 0
205 have h_2deriv_g_0 : deriv (deriv g) 0 = 2 := by
206 unfold g
207 rw [deriv_const_add, deriv_const_mul]
208 · rw [hCalib]
209 · exact hSmooth.differentiable (by decide) |>.differentiableAt
210
211 -- Equate
212 have h_eq : deriv (deriv f) 0 = deriv (deriv g) 0 := by rw [hfg]
213 rw [h_2deriv_f_0, h_2deriv_g_0] at h_eq
214 unfold SatisfiesFlatODE
215 linarith
216
217/-- **Axiom (Entangling Case)**: If P has the RCL form (P = 2uv + 2u + 2v after
218 boundary conditions), then the log-consistency equation
219 G(t+u) + G(t-u) = 2G(t)G(u) + 2G(t) + 2G(u) with initial conditions
220 G(0) = 0, G'(0) = 0, G''(0) = 1 forces G''(t) = G(t) + 1 for all t.
221
222 **Proof**:
223 1. Differentiate functional equation twice in u:
224 G''(t+u) + G''(t-u) = 2G(t)G''(u) + 2G''(u).
225 2. Evaluate at u=0: 2G''(t) = 2G(t)G''(0) + 2G''(0) = 2G(t) + 2.
226 3. Thus G''(t) = G(t) + 1. -/