The real coordinate plane is a model of Hilbert's incidence axioms, with apartness as a witnessed positive bound

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

Recorded description

Geo.rplane is a constructive witness that the three incidence axioms stated as the record Geo.Incidence are satisfied by the REAL plane: points are CPoint (pairs of Cauchy reals, equal up to CPoint.Equiv rather than Eq), lines are coefficient triples (a, b, c) carrying a witness that a*a + b*b is positively bounded away from zero, and incidence is CReal.Equiv (a*x + b*y + c) 0. Two points are apart when there is a Nat k with CReal.PosBound (CPoint.distSq P Q) k -- a WITNESS, not the negation of equality, which over the reals would construct nothing that CReal.inv could consume. This is the second model of the same record; the first is Geo.qplane over the rationals, whose point equality is the kernel's own Eq and whose apartness IS the negation. That one record serves both is what the abstract apart field of ADR-1635 was for, and this fact is the measurement that the field was necessary.

Formal statement

def Geo.rplane : Geo.Incidence

Dependencies

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

1 direct dependencies 1 direct dependents

Evidence

kernel-Geo.rplane

Kind: kernel-term
Status: checked

Supports: Geo.rplane is a Definition admitted by the trusted kernel gate at the type Geo.Incidence, which re-derives the type from the term -- so every one of the record's 21 fields, including the four axiom fields, was supplied and checked over the reals.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection -- --require-declaration Geo.rplane --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-rplane

Kind: instance-pin
Status: checked

Supports: What the real model MEANS, at the level the kernel gate cannot reach. Each definition it rests on is evaluated by Kernel::def_eq and each evaluation carries its negative half -- including the two that encode the design decision: Nondeg is a PosBound witness and NOT the negation, and Apart is a PosBound on distSq and NOT the negation of CPoint.Equiv.

Checker command

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

Evidence notes

Seven new evaluation pins, each with a discriminating half: the RLine0 projections pick the field their name claims; Geo.RPlane.join's coefficients are (y Q - y P, x P - x Q, ...) IN THAT ORDER and the swap is refuted at FREE VARIABLES (a concrete pair can make two coefficients coincide); Geo.RPlane.onRaw pairs each coefficient with its own coordinate; Geo.RLine0.Nondeg is the PosBound existential and NOT (Equiv (a*a+b*b) 0 -> False); Geo.RPlane.Apart is the PosBound existential and NOT (CPoint.Equiv P Q -> False); CPoint.distSq unfolds definitionally to the coordinate difference squares and NOT to the sum form (joinUnique's cancellation rests on that defeq); and Geo.rplane's carriers are CPoint / Geo.RLine and NOT Geo.QPoint, so the two models are two and not one written twice. Confirm a NONZERO test count: measured 20 passed, 0 failed in 117.22s (--release, --test-threads=2). The pins are written as STORED-VALUE comparisons and not as `def_eq` refutations: over CReal a failing `def_eq` between two arithmetic terms is a search that did not finish in ten minutes, while a succeeding one is delta/iota plus congruence and is fast. See ADR-1652's Consequences.

footprint-geo-rplane

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- every declaration under `Geo.`, the 41 new real-plane ones included, is axiom-free, over a population read from the environment rather than from a list.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- geo::geo_tests::every_declaration_is_present_and_axiom_free geo::geo_tests::the_handle_names_every_live_geo_declaration --test-threads=2

Evidence notes

Environment::contains is asserted BEFORE the footprint, because an empty Kernel::axiom_footprint is also what a MISSING name returns. The population is the set of names rendering under `Geo.`, collected from Environment::iter and required to equal the set the prelude handle names, so a declaration added and forgotten fails and so does one named in the handle the build never emitted. The vacuity floor moves from 70 to 110 with the real model's 41 names. Measured green at 20 passed, 0 failed.

Provenance

{
  "date": "2026-09-06",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_geo_prelude (crates/axeyum-lean-kernel/src/geo.rs, crates/axeyum-lean-kernel/src/geo/rplane.rs)",
  "source": "ADR-1652 (docs/research/09-decisions/adr-1652-the-real-plane-is-a-model-and-it-needs-no-case-split.md); roadmap W3-8, second slice. formal.statement is the rendered type of the admitted declaration."
}