Chapter 12: partial formalization of the slope problem

[AItoBit]

Summary

• Replaces the Chapter 12 stub with a kernel-checked, still incomplete development of the slope problem (Aigner–Ziegler, printed pp. 83–87).
• Defines directions including the vertical slope, proves the 3-slope bound for a noncollinear triple, the even-case reduction, the p. 83 examples, and the letter-crossing counting lemmas from step (3).
• Does not assert Ungar’s general bound n-1.

Test plan

• CI: lake build FormalBook.Chapter_12 (and the full project lint) succeeds on Lean 4.35.0-rc3
• Confirm there are no sorry/admit in FormalBook/Chapter_12.lean
• Spot-check that the even-case theorem is only an equivalence of statements, not a proof of the boxed slope bound

Made with Cursor