Hilbert's three incidence axioms are consistent, witnessed by the rational coordinate plane

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

Recorded description

The three incidence axioms of Hilbert's Grundlagen -- through two distinct points there is exactly one line; every line carries two distinct points; there exist three points not all on one line -- are stated in this kernel as the record Geo.Incidence, and Geo.qplane is a constructive witness that they are jointly satisfiable: points are pairs of rationals, lines are coefficient triples (a, b, c) with (a, b) not both zero, and incidence is a*x + b*y + c = 0. Because the witness is a term the kernel admitted rather than a model argued about, the consistency claim is checkable in one command. The axioms are stated with an ABSTRACT apartness relation rather than with the negation of point equality; over the rationals the model instantiates that apartness AS the negation, which is why the negation being usable here is a fact about the rationals (decidable equality, unique reduced representative) and not about the axioms.

Formal statement

def Geo.qplane : Geo.Incidence

Dependencies

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

0 direct dependencies 3 direct dependents

Evidence

kernel-Geo.qplane

Kind: kernel-term
Status: checked

Supports: Geo.qplane 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.

Checker command

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

Evidence notes

The exit status depends on the finding, not on the run completing: --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 -- a deleted or renamed declaration must not read as a present one. 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 and explicitly exclude Definitions. --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-qplane

Kind: instance-pin
Status: checked

Supports: What the model MEANS, at the level the kernel gate cannot reach: a Definition computing the wrong value has the right type, so each definition the model rests on is evaluated, and each evaluation carries its negative half.

Checker command

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

Evidence notes

Four evaluation tests, each with a negative half: the projections pick the field their name claims (and NOT the other field), Geo.QPlane.join's coefficients are (y Q - y P, x P - x Q, ...) IN THAT ORDER and the swap is explicitly refuted, Geo.QPlane.shift moves along the line rather than across it, and Geo.QPlane.onRaw pairs each coefficient with its own coordinate rather than the swapped pairing (which type-checks and states a different relation). The join pin runs at FREE VARIABLES on purpose -- a concrete pair of points can make two coefficients coincide and a numeral test would not see the swap. Confirm a NONZERO test count: 12.

footprint-geo-qplane

Kind: exhaustive-enumeration
Status: checked

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

Checker command

cargo test -p axeyum-lean-kernel --lib -- geo::geo_tests::every_declaration_is_present_and_axiom_free geo::geo_tests::the_handle_names_every_live_geo_declaration

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. It carries a vacuity floor (>= 70 live names) because an empty `live` set would make the equality trivially true and a filter typo produces exactly that. Measured: 75.

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_geo_prelude (crates/axeyum-lean-kernel/src/geo.rs, crates/axeyum-lean-kernel/src/geo/qplane.rs)",
  "source": "ADR-1635 (docs/research/09-decisions/adr-1635-incidence-geometry-needs-apartness-in-exactly-one-axiom-and-the-rational-ring-normalizer-could-not-cancel.md); roadmap W3-8. formal.statement is the rendered type of the admitted declaration, taken verbatim from the unfiltered emit of `cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection`."
}