Mamikon's theorem: the swept area is half the integral of squared segment lengths
ProvedGerver.mamikon_areaThe generalized Mamikon theorem of the source: if a family of tangent segments is generated by a continuously differentiable base curve z whose derivative at each interior parameter is parallel to the wall direction v_t, with continuously varying lengths α(t), and the family has no self-overlap on the open parameter rectangle, then the area of the region swept over a turning interval of length less than π is exactly half the integral of the squared lengths. The statement is the mission's abridgement of the source's Theorem 7.4.1, stated for exactly the smooth, non-self-overlapping families that the endgame applies it to, with the turning interval bounded by a < b < a + π.
import Mathlib import Definitions.Def_Gerver_arena import Definitions.Def_Gerver_monotone import Definitions.Def_Gerver_sofa
namespace Gerver
/-- Step 3 machinery (Theorem 7.4.1, generalized Mamikon theorem): the area of
the region swept out by a continuously differentiable family of tangent
segments — base curve z with z'(t) parallel to v_t at each t, segment lengths
α(t), no self-overlap on the open parameter rectangle — is exactly half the
integral of the squared lengths over the interval of turning. -/
theorem mamikon_area (z : ℝ → ℝ × ℝ) (α : ℝ → ℝ) {a b : ℝ}
(hab : a < b) (hb : b < a + Real.pi)
(hz : ContDiffOn ℝ 1 z (Set.Icc a b)) (hα : ContinuousOn α (Set.Icc a b))
(htan : ∀ t ∈ Set.Ioo a b, dot (derivWithin z (Set.Icc a b) t) (u t) = 0)
(hinj : ∀ t ∈ Set.Ioo a b, ∀ s ∈ Set.Ioo 0 1, ∀ t' ∈ Set.Ioo a b,
∀ s' ∈ Set.Ioo 0 1,
z t + scale (s * α t) (v t) = z t' + scale (s' * α t') (v t') →
t = t' ∧ s = s') :
area (swept z α a b) = ∫ t in a..b, α t ^ 2 / 2 := by
sorry
end Gerver
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every curve z of planar points, every real-valued function α, and real numbers a, b with a < b and b < a + π, if z is continuously differentiable on the closed interval [a, b], α is continuous on [a, b], at every interior t of (a, b) the one-sided derivative of z on [a, b] has inner product zero with the vector u t, and the family of segments z t + s · α t · v t for s in (0, 1) meets the same family at t' , s' only when t = t' and s = s' , then the two-dimensional area of the region swept out by the family over [a, b] equals the integral over [a, b] of α t squared over two.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.