Two distinct lines meet in at most one point, in any incidence structure

Identifier: F:geo-distinct-lines-meet-once
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

In any incidence structure -- any inhabitant of the record Geo.Incidence, not any particular plane -- two lines that are not equal cannot both carry two points that are apart. Stated contrapositively, which is the form this kernel can express without subtracting points: given lines l and m, points P and Q that are apart, and all four incidences (P and Q each on both l and m), the assumption that l and m are unequal is refuted. This is the classical 'two distinct lines meet in at most one point' and it is a THEOREM about the axioms rather than a fact about coordinates: its proof is the uniqueness half of Hilbert I.1 applied to the four incidences, and nothing else. The distinctness of the two points is an apartness in the structure's own sense, not the negation of point equality, which is what lets one statement serve a model over the rationals and a model over the reals.

Formal statement

theorem Geo.Incidence.distinct_lines_meet_once : ((x0 : Geo.Incidence) -> ((x1 : Geo.Incidence.point x0) -> ((x2 : Geo.Incidence.point x0) -> ((x3 : Geo.Incidence.line x0) -> ((x4 : Geo.Incidence.line x0) -> ((x5 : ((x5 : Geo.Incidence.lEq x0 x3 x4) -> False)) -> ((x6 : Geo.Incidence.apart x0 x1 x2) -> ((x7 : Geo.Incidence.on x0 x1 x3) -> ((x8 : Geo.Incidence.on x0 x2 x3) -> ((x9 : Geo.Incidence.on x0 x1 x4) -> ((x10 : Geo.Incidence.on x0 x2 x4) -> False)))))))))))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

kernel-Geo.Incidence.distinct_lines_meet_once

Kind: kernel-term
Status: checked

Supports: Geo.Incidence.distinct_lines_meet_once is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection -- --require-declaration Geo.Incidence.distinct_lines_meet_once --require-kind theorem

Evidence notes

The exit status depends on the finding: --require-declaration exits 1 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. --release is MANDATORY: the binary builds the constructed carriers and overflows the default debug thread stack.

generality-Geo.Incidence.distinct_lines_meet_once

Kind: instance-pin
Status: checked

Supports: The theorem really is stated over an ARBITRARY incidence structure and not over a fixed plane: its type binds Geo.Incidence itself.

Checker command

cargo test -p axeyum-lean-kernel --lib -- geo::geo_tests::every_derived_theorem_quantifies_over_the_record

Evidence notes

The test reads each derived declaration's type back out of the environment and requires `Geo.Incidence` to appear in it. A theorem specialised to Geo.qplane would render the model's name instead and fail. The population is the five derived declarations, listed against the prelude handle -- the same handle the axiom-freedom test's environment-derived set equality covers.

footprint-Geo.Incidence.distinct_lines_meet_once

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the theorem's transitive dependencies contain no Axiom, Opaque or Quotient declaration.

Checker command

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

Evidence notes

Environment::contains is asserted BEFORE the footprint: an empty Kernel::axiom_footprint is also what a missing name returns, so the two assertions together are what makes the empty footprint mean something. Confirm a NONZERO test count.

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_geo_prelude (crates/axeyum-lean-kernel/src/geo.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`."
}