modules

geometor.staudt

Exact symbolic straightedge-only projective geometry, von Staudt’s Algebra of Throws, and Moritz Pasch’s planar order axiomatics for GEOMETOR.

Submodules

Attributes

__version__

Classes

ConcordanceEntry

Single locus cross-reference across the GEOMETOR historical and formal canon.

SourceWitness

Archival public-domain primary German text witness tracked by SHA-256.

PaschAuditResult

Exact symbolic audit of Pasch's planar transversal axiom on \(\triangle ABC\).

Functions

get_repo_root() → pathlib.Path

Return the root directory of the geometor/staudt repository.

load_concordance([repo_root]) → list[ConcordanceEntry]

Load structured cross-repository concordance entries from resources/staudt/concordance.json.

load_sources_manifest([repo_root]) → list[SourceWitness]

Load archival primary source metadata from resources/staudt/sources_manifest.json.

verify_source_witnesses([repo_root]) → dict[str, Any]

Verify existence, byte size, and SHA-256 digest of every primary source witness.

demonstrate_euclid_i16_pasch_gap() → tuple[geometor.model.Model, dict[str, Any]]

Construct Euclid I.16 (Exterior Angle Theorem) and verify the Pasch order step.

demonstrate_euclid_i21_pasch_gap() → tuple[geometor.model.Model, dict[str, Any]]

Prove Euclid I.21's unstated ray-exit assumption directly from Pasch's IV. Grundsatz.

demonstrate_pasch_axiom(model, A, B, C, line_P, line_Q) → PaschAuditResult

Audit and verify Pasch's IV. Grundsatz (1882, § 2, p. 21) & 10. Lehrsatz (p. 25) on \(\triangle ABC\).

assert_straightedge_only(model) → None

Assert that model contains zero compass circles (sympy.geometry.Circle).

is_between(A, B, C) → bool

Return True iff C lies strictly between A and B (Pasch § 1 Grundsatz V–VIII).

is_collinear(A, B, C) → bool

Return True iff points A, B, C are collinear in exact SymPy algebra.

pair_separates(A, B, C, D) → bool

Return True iff collinear point-pair {A, B} projectively separates {C, D}.

point_from_abscissa(P0, P1, Pinf, coord) → sympy.geometry.Point

Return the exact collinear sympy.geometry.Point whose projective abscissa is coord.

projective_abscissa(P0, P1, Pinf, X) → sympy.Expr

Compute von Staudt's exact projective abscissa (Beiträge § 29, art. 404) of X.

construct_harmonic_fourth_straightedge(model, A, B, C) → sympy.geometry.Point

Construct the fourth harmonic point D to (A, B; C, D) = -1 using only a straightedge.

prove_symbolic_quadrangle_uniqueness() → dict[str, sympy.Expr]

Prove over free symbolic coordinates in SymPy that D is independent of the quadrangle.

verify_quadrangle_independence(A, B, C, quad1, quad2) → dict[str, Any]

Verify in SymPy that two completely distinct auxiliary quadrangles construct the identical point D.

construct_harmonic_scale(model, P0, P1, Pinf[, max_n]) → dict[int, sympy.geometry.Point]

Construct the Möbius–von Staudt harmonic integer scale P_{-1}, P_0, P_1, ..., P_n by straightedge.

construct_parallel_straightedge(model, A, B, rail_U0, ...) → sympy.geometry.Line

Construct the line through R parallel to [AB] using only an unmarked straightedge.

construct_von_staudt_addition(model, P0, P1, Pinf, X, Y, *) → sympy.geometry.Point

Construct the projective sum S = X + Y on (P0, P1, Pinf) using only a straightedge.

construct_von_staudt_multiplication(model, P0, P1, ...) → sympy.geometry.Point

Construct the projective product P = X * Y on (P0, P1, Pinf) using only a straightedge.

verify_golden_throw_identity(P0, P1, Pinf) → dict[str, Any]

Verify over \(\mathbb{Q}(\phi)\) that von Staudt's straightedge product & sum satisfy \(P_\phi \cdot P_\phi = P_\phi + P_1\).

Package Contents

geometor.staudt.__version__ = '0.1.0'
class geometor.staudt.ConcordanceEntry

Single locus cross-reference across the GEOMETOR historical and formal canon.

id: str
treatise: str
locus_de: str
title: str
codex_ref: str
cross_refs: dict[str, str]
summary: str
class geometor.staudt.SourceWitness

Archival public-domain primary German text witness tracked by SHA-256.

id: str
author: str
work: str
edition: str
year: int
language: str
license: str
relative_path: str
sha256: str
bytes: int
geometor.staudt.get_repo_root() → pathlib.Path

Return the root directory of the geometor/staudt repository.

geometor.staudt.load_concordance(repo_root: pathlib.Path | None = None) → list[ConcordanceEntry]

Load structured cross-repository concordance entries from resources/staudt/concordance.json.

geometor.staudt.load_sources_manifest(repo_root: pathlib.Path | None = None) → list[SourceWitness]

Load archival primary source metadata from resources/staudt/sources_manifest.json.

geometor.staudt.verify_source_witnesses(repo_root: pathlib.Path | None = None) → dict[str, Any]

Verify existence, byte size, and SHA-256 digest of every primary source witness.

class geometor.staudt.PaschAuditResult

Exact symbolic audit of Pasch’s planar transversal axiom on \(\triangle ABC\).

triangle: tuple[sympy.geometry.Point, sympy.geometry.Point, sympy.geometry.Point]
transversal: sympy.geometry.Line
passes_through_vertex: bool
vertex_hits: tuple[str, ...]
entered_sides: tuple[tuple[str, sympy.geometry.Point], ...]
vertex_orientations: dict[str, int]
satisfies_pasch: bool
geometor.staudt.demonstrate_euclid_i16_pasch_gap() → tuple[geometor.model.Model, dict[str, Any]]

Construct Euclid I.16 (Exterior Angle Theorem) and verify the Pasch order step.

In Elements Book I Prop. 16, Euclid bisects \(AC\) at \(E\), prolongs median \(BE\) to \(F\) with \(BE = EF\), joins \(CF\), and infers from visual inspection of the diagram that \(F\) lies inside exterior angle \(\angle ACD\) so that \(\angle ACD > \angle ECF\) (Common Notion 5). On a sphere (elliptic plane) where straight lines are closed geodesics lacking open linear betweenness, \(F\) can wrap past the antipode and violate I.16.

Using Pasch’s linear betweenness (§ 1) and planar separation (IV. Grundsatz, § 2): since \(C\) lies between \(B\) and \(D\) (\(B\text{--}C\text{--}D\)), \(E\) lies between \(A\) and \(C\) (\(A\text{--}E\text{--}C\)), and \(E\) lies between \(B\) and \(F\) (\(B\text{--}E\text{--}F\)), ray \(CF\) lies strictly inside \(\angle ACD\) (i.e., any segment joining \(A_1 \in CA_{\text{ext}}\) or \(D \in BC_{\text{ext}}\) to \(A\) is cut internally by ray \(CF\) via Pasch’s Axiom on \(\triangle ABD\)).

geometor.staudt.demonstrate_euclid_i21_pasch_gap() → tuple[geometor.model.Model, dict[str, Any]]

Prove Euclid I.21’s unstated ray-exit assumption directly from Pasch’s IV. Grundsatz.

In Elements Book I Prop. 21, given \(\triangle ABC\) and an interior point \(D\), Euclid writes “let BD be drawn through to E [on AC]” without proving that prolonging \(BD\) must intersect open side \(AC\) between \(A\) and \(C\).

Deductive proof via Pasch’s Axiom (Vorlesungen § 2, p. 21):

  1. For interior point \(D\) of \(\triangle ABC\), line \([CD]\) meets open side \(AB\) at \(M\) strictly between \(A\) and \(B\), with \(D\) strictly between \(C\) and \(M\).

  2. Apply demonstrate_pasch_axiom() to sub-triangle \(\triangle AMC\) and transversal \(\ell = [BD]\):

    • \(\ell\) misses all three vertices \(A, M, C\) (since \(A\text{--}M\text{--}B\)).

    • \(\ell\) enters side \(CM\) strictly at \(D\).

    • \(\ell\) cannot exit side \(AM\), because \(\ell \cap [AM] = B\) lies outside segment \(AM\).

    • Therefore, by Pasch’s Grundsatz IV, \(\ell = [BD]\) must exit side \(AC\) at an interior point \(E\) strictly between \(A\) and \(C\)!

geometor.staudt.demonstrate_pasch_axiom(model: geometor.model.Model, A: sympy.geometry.Point, B: sympy.geometry.Point, C: sympy.geometry.Point, line_P: sympy.geometry.Point, line_Q: sympy.geometry.Point) → PaschAuditResult

Audit and verify Pasch’s IV. Grundsatz (1882, § 2, p. 21) & 10. Lehrsatz (p. 25) on \(\triangle ABC\).

Given non-collinear vertices \(A, B, C\) in the plane and a straight line \(\ell = [P Q]\):

  • Computes exact signed half-plane orientations \(\operatorname{orient}(P, Q, V) \in \{-1, 0, +1\}\) for each vertex \(V \in \{A, B, C\}\).

  • When \(\ell\) passes through no vertex (\(\operatorname{orient} \neq 0\) for all three): if \(\ell\) meets any open triangle side strictly between its endpoints (is_between()), it must exit strictly through one and only one of the remaining two sides (10. Lehrsatz, p. 25: it cannot meet all three open sides, nor meet only one).

geometor.staudt.assert_straightedge_only(model: geometor.model.Model) → None

Assert that model contains zero compass circles (sympy.geometry.Circle).

Von Staudt’s Geometrie der Lage (1847) and Rechnung mit Würfen (1857) require that every projective construction proceed strictly by unmarked straightedge incidence without metric compass transfers or circle intersections.

Raises:

ProofAssertionError – If any sympy.geometry.Circle exists in model.

geometor.staudt.is_between(A: sympy.geometry.Point, B: sympy.geometry.Point, C: sympy.geometry.Point) → bool

Return True iff C lies strictly between A and B (Pasch § 1 Grundsatz V–VIII).

Verifies exact collinearity together with positive inner product of directed segments \(\overrightarrow{AC} \cdot \overrightarrow{CB} > 0\).

geometor.staudt.is_collinear(A: sympy.geometry.Point, B: sympy.geometry.Point, C: sympy.geometry.Point) → bool

Return True iff points A, B, C are collinear in exact SymPy algebra.

geometor.staudt.pair_separates(A: sympy.geometry.Point, B: sympy.geometry.Point, C: sympy.geometry.Point, D: sympy.geometry.Point) → bool

Return True iff collinear point-pair {A, B} projectively separates {C, D}.

In Pasch (Vorlesungen § 1 Lehrsätze 19–23 & § 11) and Vailati (1895), four distinct collinear points exhibit cyclic pair separation AB // CD iff the projective cross-ratio \((A, B; C, D)\) is strictly negative. Every harmonic range satisfies \((A, B; C, D) = -1 < 0\) and therefore separates conjugate pairs.

geometor.staudt.point_from_abscissa(P0: sympy.geometry.Point, P1: sympy.geometry.Point, Pinf: sympy.geometry.Point | None, coord: sympy.Expr | int) → sympy.geometry.Point

Return the exact collinear sympy.geometry.Point whose projective abscissa is coord.

Used strictly for setting up test inputs and checking closed-form algebraic identities; straightedge constructions in geometor.staudt.quadrangle and geometor.staudt.throws never invoke coordinate inversion.

geometor.staudt.projective_abscissa(P0: sympy.geometry.Point, P1: sympy.geometry.Point, Pinf: sympy.geometry.Point | None, X: sympy.geometry.Point) → sympy.Expr

Compute von Staudt’s exact projective abscissa (Beiträge § 29, art. 404) of X.

Relative to three distinct collinear reference points \((P_0, P_1, P_\infty)\):

  • When Pinf is a finite projective horizon point on line \([P_0 P_1]\), returns the exact cross-ratio \((P_\infty, P_0; P_1, X)\), mapping \(P_0 \mapsto 0\), \(P_1 \mapsto 1\), and \(P_\infty \mapsto \infty\).

  • When Pinf is None (ideal point at infinity along \([P_0 P_1]\)), returns the exact affine ratio \(\frac{(X - P_0) \cdot d}{d \cdot d}\) with \(d = P_1 - P_0\).

Raises:

ValueError – If reference points coincide, X is not collinear with [P0 P1], or X coincides with Pinf.

geometor.staudt.construct_harmonic_fourth_straightedge(model: geometor.model.Model, A: sympy.geometry.Point, B: sympy.geometry.Point, C: sympy.geometry.Point, aux_P: sympy.geometry.Point | None = None, aux_Q: sympy.geometry.Point | None = None, *, label: str = 'D') → sympy.geometry.Point

Construct the fourth harmonic point D to (A, B; C, D) = -1 using only a straightedge.

Implements Karl Georg Christian von Staudt’s pure-incidence construction (Geometrie der Lage, 1847, § 8, arts. 93–96):

  1. Join carrier line \(\ell = [AB]\) containing collinear points \(A, B, C\).

  2. From auxiliary vertex \(E = P_{\text{aux}} \notin \ell\), draw lines \([AE]\), \([BE]\), and first diagonal \([CE]\).

  3. Select second diagonal vertex \(G \in [CE] \setminus \{C, E\}\) (either aux_Q directly if incident to \([CE]\), or the straightedge intersection of \([CE]\) with \([A, Q_{\text{aux}}]\)).

  4. Intersect opposite quadrangle sides \(F = [AE] \cap [BG]\) and \(H = [AG] \cap [BE]\).

  5. Draw the second diagonal \([FH]\) meeting \(\ell\) in the fourth harmonic conjugate \(D\), satisfying \((A, B; C, D) = -1\) with zero circles.

Parameters:
  • model – Target Model (recommended auto_intersect=False).

  • A – First fundamental point of the harmonic pair {A, B}.

  • B – Second fundamental point of the harmonic pair {A, B}.

  • C – Given third collinear point (distinct from A and B).

  • aux_P – Optional off-line auxiliary vertex E.

  • aux_Q – Optional second auxiliary point determining G on [CE].

  • label – Point identifier for the constructed harmonic conjugate D.

Returns:

Exact sympy.geometry.Point D registered in model.

geometor.staudt.prove_symbolic_quadrangle_uniqueness() → dict[str, sympy.Expr]

Prove over free symbolic coordinates in SymPy that D is independent of the quadrangle.

Places \(A = (0, 0)\), \(B = (1, 0)\), \(C = (c, 0)\) and constructs the complete quadrangle from indeterminate parameters \(E = (u, v)\) and \(G = ((1 - t) c + t u, t v)\) on \([CE]\). Simplifies the algebraic intersection \(D = [FH] \cap [AB]\) and verifies \(D_x = \frac{c}{2c - 1}\) with zero free dependence on \((u, v, t)\) and exact cross-ratio \((A, B; C, D) = -1\).

geometor.staudt.verify_quadrangle_independence(A: sympy.geometry.Point, B: sympy.geometry.Point, C: sympy.geometry.Point, quad1: tuple[sympy.geometry.Point, sympy.geometry.Point], quad2: tuple[sympy.geometry.Point, sympy.geometry.Point]) → dict[str, Any]

Verify in SymPy that two completely distinct auxiliary quadrangles construct the identical point D.

In Geometrie der Lage (§ 7 arts. 87–92 & § 8 art. 93), von Staudt proves without any appeal to metric cross-ratios that two complete quadrangles sharing A, B, and C have perspective vertex triangles by Desargues’s Theorem, forcing their sixth sides to meet [AB] in the selfsame fourth harmonic point \(D_1 = D_2\).

geometor.staudt.construct_harmonic_scale(model: geometor.model.Model, P0: sympy.geometry.Point, P1: sympy.geometry.Point, Pinf: sympy.geometry.Point, max_n: int = 5) → dict[int, sympy.geometry.Point]

Construct the Möbius–von Staudt harmonic integer scale P_{-1}, P_0, P_1, ..., P_n by straightedge.

In Beiträge § 19 art. 267, von Staudt observes that \((P_{k-1}, P_{k+1}; P_k, P_\infty) = -1\) for every integer \(k\), so each successive integer mark \(P_{k+1}\) is the fourth harmonic conjugate to \((P_{k-1}, P_{k+1}; P_k, P_\infty) = -1\) — equivalently \((P_k, P_\infty; P_{k-1}, P_{k+1}) = -1\)! Constructs P_{-1} and P_2 .. P_{max_n} exclusively via construct_harmonic_fourth_straightedge().

geometor.staudt.construct_parallel_straightedge(model: geometor.model.Model, A: sympy.geometry.Point, B: sympy.geometry.Point, rail_U0: sympy.geometry.Point, rail_U1: sympy.geometry.Point, R: sympy.geometry.Point, *, guide: bool = True) → sympy.geometry.Line

Construct the line through R parallel to [AB] using only an unmarked straightedge.

Given carrier line \(\ell = [AB]\) and a single auxiliary parallel rail \(m = [U_0 U_1] \parallel \ell\) (representing the shared ideal point \(P_\infty\) at infinity, with \(|AB| \neq |U_0 U_1|\)), executes the two-stage Steiner–Poncelet pure-incidence construction:

  1. Affine midpoint via trapezoid quadrangle: \(O = [A U_0] \cap [B U_1]\) and \(K_0 = [A U_1] \cap [B U_0]\); line \([O K_0]\) meets \(\ell\) in the exact harmonic conjugate \(M\) of \(P_\infty\), i.e., the midpoint of \(AB\).

  2. Parallel through R via Steiner harmonic cevian: join \([AR]\) meeting \(m\) at \(Q\) (if \(R \in m\), \(m\) itself is already the required parallel); intersect \(K = [BR] \cap [QM]\) and \(L = [AK] \cap [QB]\). Then \([RL] \parallel [AB]\) with zero circles and zero coordinate helpers.

geometor.staudt.construct_von_staudt_addition(model: geometor.model.Model, P0: sympy.geometry.Point, P1: sympy.geometry.Point, Pinf: sympy.geometry.Point | None, X: sympy.geometry.Point, Y: sympy.geometry.Point, *, aux_U: sympy.geometry.Point | None = None, aux_V: sympy.geometry.Point | None = None, parallel_rail: tuple[sympy.geometry.Point, sympy.geometry.Point] | None = None, label: str = 'S') → sympy.geometry.Point

Construct the projective sum S = X + Y on (P0, P1, Pinf) using only a straightedge.

Implements Karl Georg Christian von Staudt’s Summen von Würfen (Beiträge zur Geometrie der Lage, Heft 2, 1857, § 19, arts. 256–267): the parabolic projectivity fixing \(P_\infty\) with double contact (conjugate to \(P_0\) in the involution \(P_\infty P_\infty \cdot X Y\)) realized as a composition of two perspectivities \(\ell \xrightarrow{U} a \xrightarrow{V} \ell\) whose center join \([UV]\) and perspective axis \(a\) both pass through \(P_\infty\):

  1. Draw horizon carrier \(m\) through \(P_\infty\) containing distinct off-line centers \(U\) and \(V\) (when Pinf is None, \(m = [U V]\) is a parallel rail to \(\ell = [P_0 P_1]\)).

  2. Intersect \(R = [U P_0] \cap [V X]\) so that \(P_0 \mapsto X\).

  3. Construct perspective axis \(a\) joining \(P_\infty\) and \(R\) (when Pinf is None, construct \(a \parallel \ell\) through \(R\) purely by straightedge via construct_parallel_straightedge()).

  4. Intersect \(T = [U Y] \cap a\) and project \(S = [V T] \cap \ell\).

Verifies in SymPy that projective_abscissa(P0, P1, Pinf, S) equals projective_abscissa(P0, P1, Pinf, X) + projective_abscissa(P0, P1, Pinf, Y) and that zero circles exist in model.

geometor.staudt.construct_von_staudt_multiplication(model: geometor.model.Model, P0: sympy.geometry.Point, P1: sympy.geometry.Point, Pinf: sympy.geometry.Point | None, X: sympy.geometry.Point, Y: sympy.geometry.Point, *, aux_U: sympy.geometry.Point | None = None, aux_V: sympy.geometry.Point | None = None, parallel_rail: tuple[sympy.geometry.Point, sympy.geometry.Point] | None = None, label: str = 'P') → sympy.geometry.Point

Construct the projective product P = X * Y on (P0, P1, Pinf) using only a straightedge.

Implements Karl Georg Christian von Staudt’s Produkte aus Würfen (Beiträge zur Geometrie der Lage, Heft 2, 1857, § 20, arts. 268–275): the hyperbolic projectivity fixing both \(P_0\) and \(P_\infty\) while mapping \(P_1 \mapsto X\), realized by two perspectivities \(\ell \xrightarrow{U} a \xrightarrow{V} \ell\) whose center line \([UV]\) passes through \(P_0\) and whose axis \(a\) passes through \(P_\infty\):

  1. Choose distinct off-line centers \(U, V\) collinear with \(P_0\).

  2. Intersect \(W = [U P_1] \cap [V X]\) so that \(P_1 \mapsto X\).

  3. Draw axis \(a\) through \(P_\infty\) and \(W\) (or parallel to \(\ell\) via construct_parallel_straightedge() when Pinf is None).

  4. Intersect \(Z = [U Y] \cap a\) and project \(P = [V Z] \cap \ell\).

Verifies in SymPy that projective_abscissa(P0, P1, Pinf, P) equals projective_abscissa(P0, P1, Pinf, X) * projective_abscissa(P0, P1, Pinf, Y) and that zero circles exist in model.

geometor.staudt.verify_golden_throw_identity(P0: sympy.geometry.Point, P1: sympy.geometry.Point, Pinf: sympy.geometry.Point | None) → dict[str, Any]

Verify over \(\mathbb{Q}(\phi)\) that von Staudt’s straightedge product & sum satisfy \(P_\phi \cdot P_\phi = P_\phi + P_1\).

With \(\phi = \frac{1 + \sqrt{5}}{2}\), constructs both \(P_{\phi^2} = P_\phi \cdot P_\phi\) and \(P_{\phi + 1} = P_\phi + P_1\) purely by straightedge incidence on the projective line \((P_0, P_1, P_\infty)\) and proves exact coincidence of the two constructed points, plus exact conjugate throw relations \(P_\phi + P_{\hat{\phi}} = P_1\) and \(P_\phi \cdot P_{\hat{\phi}} = P_{-1}\) where \(\hat{\phi} = 1 - \phi = -1/\phi\).