Prove2Me

Matrix-pencil/Maslov incidence equivalence

Proved
StickyKakeya4.maslov_incidence_equivalence

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

contact-geometrygeometric-measure-theorykakeya

Let A,BA,B be real 3×33\times3 matrices and assume c↦(Ac,Bc)c\mapsto(Ac,Bc) is injective. For every real ss, det⁡(B+sA)=0\det(B+sA)=0 exactly when the graph plane {(Ac,Bc)}\{(Ac,Bc)\} has a nonzero incidence with the Lagrangian pencil {(x,−sx)}\{(x,-sx)\}.

This is the precise linear-algebraic Maslov incidence used by the contact-geometric collision analysis.

Preamble
import Definitions.Def_sticky_kakeya4_core
Formal statement
namespace StickyKakeya4

theorem maslov_incidence_equivalence (A B : Mat3) (s : ℝ)
    (hframe : Function.Injective (fun c : E3 => (A.mulVec c, B.mulVec c))) :
    Matrix.det (pencil A B s) = 0 ↔
      ∃ point : E3 × E3,
        point ∈ graphPlane A B ∧
        point ∈ lagrangianPencil s ∧
        point ≠ 0 := by sorry

end StickyKakeya4
Source
Chenxi Cai, source manuscript https://cchx0000.github.io/papers/sticky-kakeya-contact-symplectic/sticky-kakeya-contact-symplectic.pdf, Theorem 4.3.
Read-back

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

For all real 3×33\times 3 matrices AA and BB, and every real number ss, assume that the linear map R3→R3×R3\mathbb R^3\to\mathbb R^3\times\mathbb R^3 given by c↦(Ac,Bc)c\mapsto(Ac,Bc) is injective. Then

det⁡(B+sA)=0⟺∃ c,x,y∈R3,  x=Ac,y=Bc,y=−s x,(x,y)≠(0,0).\det(B+sA)=0 \quad\Longleftrightarrow\quad \exists\,c,x,y\in\mathbb R^3,\; x=Ac,\quad y=Bc,\quad y=-s\,x,\quad (x,y)\ne(0,0).

Equivalently, the pencil matrix B+sAB+sA has zero determinant exactly when the graph plane {(Ac,Bc):c∈R3}\{(Ac,Bc):c\in\mathbb R^3\} and the set {(x,y):y=−s x}\{(x,y):y=-s\,x\} have a common nonzero point.

View graph