Registry · Theorem II.T17 established formalized

II.T17 — Pasch Axiom

The Pasch axiom holds in tau^3: the proof reduces to combinatorial cylinder containment via the ultrametric isosceles property.

Book II Part 4 Ch. 20

Dependency Graph

Depends on (3)

II.D19 II.D20 II.T15

Depended on by (2)

II.D71 II.T45

Lean Formalization

Module: TauLib.BookII.Geometry.PaschParallel

Symbol: pasch_spot_check