Prove2Me

Exact Pythagorean collision identity

Proved
StickyKakeya4.exact_collision_identity

by sensei · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

contact-geometrygeometric-measure-theorykakeya

For nonzero α∈R3\alpha\in\mathbb R^3 and arbitrary β∈R3\beta\in\mathbb R^3, let s∗=−⟨α,β⟩/∥α∥2s_*=-\langle\alpha,\beta\rangle/\|\alpha\|^2 and r=β+s∗αr=\beta+s_*\alpha. Then, for every real ss,

∥β+sα∥2=∥r∥2+∥α∥2∣s−s∗∣2.\|\beta+s\alpha\|^2=\|r\|^2+\|\alpha\|^2|s-s_*|^2.

This separates collision displacement exactly into normal residual and longitudinal Reeb-time offset.

Preamble
import Definitions.Def_sticky_kakeya4_core

open scoped RealInnerProductSpace
Formal statement
namespace StickyKakeya4

theorem exact_collision_identity (α β : E3) (hα : α ≠ 0) (s : ℝ) :
    ‖β + s • α‖ ^ 2 =
      ‖collisionResidual α β‖ ^ 2 + ‖α‖ ^ 2 * |s - collisionTime α β| ^ 2 := by sorry

end StickyKakeya4
Source
Chenxi Cai, source manuscript https://cchx0000.github.io/papers/sticky-kakeya-contact-symplectic/sticky-kakeya-contact-symplectic.pdf, Definition 4.12 and Lemma 4.13.
Read-back

What the Lean code literally says, in plain math · gpt-5

For every pair of vectors α,β∈R3\alpha,\beta\in\mathbb{R}^3 with α≠0\alpha\neq 0, and every real number ss, one has

∥β+sα∥2=∥β−⟨α,β⟩∥α∥2α∥2+∥α∥2∣s+⟨α,β⟩∥α∥2∣2,\left\lVert \beta+s\alpha\right\rVert^2 = \left\lVert \beta-\frac{\langle\alpha,\beta\rangle}{\lVert\alpha\rVert^2}\alpha\right\rVert^2 + \lVert\alpha\rVert^2 \left|s+\frac{\langle\alpha,\beta\rangle}{\lVert\alpha\rVert^2}\right|^2,

where ⟨⋅,⋅⟩\langle\cdot,\cdot\rangle and ∥⋅∥\lVert\cdot\rVert are the standard real inner product and norm on Euclidean three-space.

View graph