The real coordinate plane satisfies Playfair's parallel axiom, with parallelism stated positively

Identifier: F:geo-affine-model-real-plane
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Geo.raffine is a constructive witness that the REAL plane is an affine plane: it supplies every field of the record Geo.Affine, which is Geo.Incidence plus Playfair's parallel axiom split into its existence and uniqueness halves. Parallelism is NOT the classical negative predicate 'the two lines share no point'. It is stated positively as parPos l m := CReal.Equiv (a l * b m - b l * a m) 0 together with a witness exists k, CReal.PosBound ((a l * c m - c l * a m)^2 + (b l * c m - c l * b m)^2) k -- same direction, and a distinctness that is WITNESSED rather than negated. The same move is made for the point-off-a-line relation: off P l is exists k, CReal.PosBound (e_P * e_P) k where e_P is the incidence expression, because over the reals the negation 'P is not on l' constructs no modulus and the existence half needs one. ADR-1652 section 5 measured that the negative form makes uniqueness end at Not (Apart (a*B - b*A) 0), whose closure is tightness -- a principle creal.rs documents as neither proved nor assumed -- so this is the fix that avoids acquiring a classical principle rather than the one that acquires it. Existence needs NO division: the parallel through P is (a, b, -(a*x P + b*y P)), whose leading coefficients are the original line's so its non-degeneracy is the original's outright, and whose distinctness witness is the PRODUCT of two PosBound moduli, since dAC^2 + dBC^2 = (a^2 + b^2) * e_P^2. Uniqueness divides once, by a^2 + b^2, through the same cancelPosBound that Geo.RPlane.joinUnique uses.

Formal statement

def Geo.raffine : Geo.Affine

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

2 direct dependencies 0 direct dependents

Evidence

kernel-Geo.raffine

Kind: kernel-term
Status: checked

Supports: Geo.raffine is a Definition admitted by the trusted kernel gate at the type Geo.Affine, which re-derives the type from the term -- so all seven of the record's fields, including the two Playfair axioms, were supplied and checked over the reals.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection -- --require-declaration Geo.raffine --require-kind definition

Evidence notes

The exit status depends on the finding: --require-declaration exits 1 and prints to stderr when no constructed prelude's environment holds a declaration with that exact rendered name, and --require-kind exits 1 when the match is of a different kind. This is the only in-tree inventory tool that can assert a Definition exists -- theorem_dependency_inventory, nat_theorem_inventory and prelude_theorem_inventory all filter to Declaration::Theorem. --release is MANDATORY: the binary builds creal/complex/cpoint/metric/rn/geo, which recurse deep enough to overflow the default debug thread stack.

evaluation-geo-raffine

Kind: instance-pin
Status: checked

Supports: What the real affine model MEANS, at the level the kernel gate cannot reach. The positive parallel predicate is pinned as a STORED-VALUE comparison: its second conjunct is an Exists over CReal.PosBound and NOT the negation (Equiv (dAC^2 + dBC^2) 0 -> False), and the wrong shape is asserted to be a different interned ExprId so the comparison could have failed.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- geo:: --test-threads=4

Evidence notes

Confirm a NONZERO test count: measured 27 passed, 0 failed in 101.90s (--release, --test-threads=4). Five new pins, each with a discriminating half: the two affine planes are two models and not one (Geo.qaffine's inc is Geo.qplane and NOT Geo.rplane); positive parallelism is witnessed over the reals and negated over the rationals; dropping the distinctness conjunct would make a line parallel to itself (COMPUTED at the line (1,0,0), where all three proportionalities against ITSELF reduce to Rat.zero = Rat.zero); the parallel through a point keeps the leading coefficients and negates the constant; and the three derived affine theorems instantiate at BOTH models. The real-side pins are stored-value comparisons and not def_eq refutations, because over CReal a failing def_eq between two arithmetic terms is a search that does not finish -- see ADR-1652's Consequences.

mutation-geo-affine

Kind: exhaustive-enumeration
Status: checked

Supports: The two design decisions are load-bearing rather than conventional: swapping Playfair's uniqueness conclusion to the other order, and dropping the distinctness conjunct from the positive parallel predicate, each stop the real model from being assembled at all.

Checker command

python3 scripts/tests/mutation_controls.py geo-affine

Evidence notes

Baseline green at 1 test; both mutants killed. Both fail at PRELUDE-BUILD time, which is the finding rather than an inconvenience -- neither predicate can be weakened and left provable. Extensional line equality is And A B against And B A under the swap, symmetric propositionally and NOT definitionally, so neither model's playfairUnique keeps the field's type; and without the distinctness witness Geo.RPlane.parPosDisjoint has nothing to contradict, with the degenerate consequence computed rather than argued in dropping_the_distinctness_conjunct_would_make_a_line_parallel_to_itself.

Provenance

{
  "date": "2026-09-06",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_geo_prelude (crates/axeyum-lean-kernel/src/geo/affine.rs, crates/axeyum-lean-kernel/src/geo/raffine.rs)",
  "source": "ADR-1659 (docs/research/09-decisions/adr-1659-parallelism-is-positive-and-both-planes-are-affine.md); roadmap W3-8, third slice. formal.statement is the rendered type of the admitted declaration."
}