fix(lean): complete picard-lindelof existence proof in legacy HamiltonianMechanics

Browse source

The existence half of Picard-Lindelöf for finite-dimensional systems (Fin n → ℝ)
is now fully proven. The proof factors into:

1. exists_forward_solution — generic lemma building a forward solution on [0,∞)
   for any Lipschitz vector field via Nat.rec over τ-intervals with
   HasDerivWithinAt.union at boundaries and Nat.find indexing.

2. Time reversal via f_neg (x ↦ -f x) applied to exists_forward_solution gives
   the backward solution.

3. γ_full splices both halves with case split at t=0.

4. The splice point t=0 is resolved via
   hasDerivAt_iff_tendsto_slope_left_right, with the left slope obtained by
   composing the negative-forward slope with y ↦ -y and an algebraic identity
   γ_full(y) = γ_neg_fwd(-y) on y ≤ 0.

Previously 1 sorry (the existence existence) remained; it is now closed.
The uniqueness half was already proven via ODE_solution_unique_univ.

Build: 3583 jobs, 0 errors (lake build)

...

This commit is contained in:

allaun 2026-06-16 00:09:31 -05:00

parent 5f80fd8429

commit f59926e488

1 changed files with 578 additions and 921 deletions

Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL

Show stats Download patch file Download diff file Expand all files Collapse all files

1499

0-Core-Formalism/lean/Semantics/legacy/6point5sigma/HamiltonianMechanics.lean

View file

File diff suppressed because it is too large Load diff