THM0083canonicalv1Pasch Axiom
The Pasch axiom holds in tau^3: the proof reduces to combinatorial cylinder containment via the ultrametric isosceles property.
Payload
Pasch Axiom
The Pasch axiom holds in tau^3: the proof reduces to combinatorial cylinder containment via the ultrametric isosceles property.
Pasch Axiom
Summary
The Pasch axiom holds in tau^3: the proof reduces to combinatorial cylinder containment via the ultrametric isosceles property.
Statement
%
\label{thm:pasch}
Let $a, b, c, p, q \in \tau^3$
with $B(a, p, c)$ and $B(b, q, c)$.
Then there exists $x \in \tau^3$
such that $B(p, x, b)$ and $B(q, x, a)$.
Proof / Justification
No immediate manuscript proof block was extracted in this pilot run.
Source Context
- Registry source:
book-02.jsonlline 53 - Manuscript source:
2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part04/ch20-pasch-parallel.texlines 85-92
Lean / Formalization Notes
- Formalization:
formalized - Module:
TauLib.BookII.Geometry.PaschParallel - Name:
pasch_spot_check
Dependencies
- Canonical: II.D19, II.D20, II.T15
Related Results
Generated by later projection phases.
Related Publications
Generated by later projection phases.
Revision Notes
- 2026-04-24: Initial pilot migration.
Identifiers
Aliases & legacy IDs
II.T17pasch-axiomthm:paschRelease lines
corpus_v3_workingcorpus_v2Relations
Appears in (1)
Sources
Version & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.