Pappus's hexagon theorem: the three cross intersections are collinear, and ONE non-degeneracy condition suffices

Identifier: F:geometry-pappus-hexagon
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-rational-polynomial-normal-form, geometry.cartesian-coordinatisation-of-the-euclidean-plane, geometry.characteristic-zero-specialisation, geometry.rabinowitsch-inverse-specialisation, geometry.nondegeneracy.ae-meets-bd

Recorded description

Let A, B, C be collinear points of the Euclidean plane and let D, E, F be collinear. Let X lie on line AE and on line BD, let Y lie on line AF and on line CD, and let Z lie on line BF and on line CE. If AE is not parallel to BD -- that is, det(E-A, D-B) is nonzero -- then X, Y and Z are collinear. Exactly one condition is used and exactly one is needed. The two other conditions this configuration invites (AF not parallel to CD, BF not parallel to CE) are individually REDUNDANT, and by the symmetry that exchanges (B,E) with (C,F) either of them would serve equally well as the single condition, so this theorem has three distinct minimal condition sets, each a singleton. The condition that is kept is essential and its failure is exhibited rather than asserted: A=(0,0), B=(1,0), C=(3,0), D=(1,0), E=(0,0), F=(5,0) puts all six points on the x-axis, so every incidence hypothesis holds vacuously or forces its point onto that axis, while X=(0,1), Y=(2,0), Z=(4,0) is a genuine triangle. Sitting on the degeneracy locus is not by itself enough to break the theorem: the same configuration with X=(0,0) also annihilates the condition and yet leaves X, Y, Z collinear on the x-axis, and the checker rejects a certificate offering THAT configuration as its counterexample. The redundancy of the other two conditions is not an absence of evidence: it is decided exhaustively over F_p for p = 5, 7, 11, 13, 17, 19 and 23, where of the eight zero/nonzero patterns of the three conditions the ONLY one admitting a configuration that satisfies every hypothesis and falsifies the conclusion is the pattern with all three zero.

Formal statement

(assert (forall ((ax Real) (ay Real) (bx Real) (by Real) (cx Real) (cy Real) (dx Real) (dy Real) (ex Real) (ey Real) (fx Real) (fy Real) (xx Real) (xy Real) (yx Real) (yy Real) (zx Real) (zy Real))
  (=> (and (= (- (* (- bx ax) (- cy ay)) (* (- by ay) (- cx ax))) 0.0)
           (= (- (* (- ex dx) (- fy dy)) (* (- ey dy) (- fx dx))) 0.0)
           (= (- (* (- ex ax) (- xy ay)) (* (- ey ay) (- xx ax))) 0.0)
           (= (- (* (- dx bx) (- xy by)) (* (- dy by) (- xx bx))) 0.0)
           (= (- (* (- fx ax) (- yy ay)) (* (- fy ay) (- yx ax))) 0.0)
           (= (- (* (- dx cx) (- yy cy)) (* (- dy cy) (- yx cx))) 0.0)
           (= (- (* (- fx bx) (- zy by)) (* (- fy by) (- zx bx))) 0.0)
           (= (- (* (- ex cx) (- zy cy)) (* (- ey cy) (- zx cx))) 0.0)
           (not (= (- (* (- ex ax) (- dy by)) (* (- ey ay) (- dx bx))) 0.0)))
      (= (- (* (- yx xx) (- zy xy)) (* (- yy xy) (- zx xx))) 0.0))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

geometry-certificate-pappus-hexagon

Kind: witness-replay
Status: checked

Supports: the saturated cofactor certificate over a SINGLE non-degeneracy condition, re-checked from the committed artifact by a checker that shares no code with either of the two searches that produced it

Checker command

cargo test -p axeyum-cas --test geometry_certificate_artifacts

Evidence notes

The certificate uses the Rabinowitsch trick: a fresh variable Zinv0 and the generator `parallel(A,E,B,D) * Zinv0 - 1`. Specialising Zinv0 := 1/det(E-A, D-B) is legitimate exactly when AE is not parallel to BD, and that is the ONLY place the side condition enters. The multiplier is the condition polynomial to the FIRST power, so the saturation cofactor is the familiar minus-the-conclusion rather than euler-line's squared-multiplier shape. Every tamper control in the cited suite runs against this certificate too: a cofactor edited by one is rejected, a conclusion edited by one is rejected, a swapped non-degeneracy condition is rejected, cofactors donated by a neighbouring certificate are rejected, deleting the degenerate counterexample is rejected, and replacing it with the on-locus-but-harmless configuration (the same six collinear points with X=(0,0) instead of (0,1), which violates the condition just as thoroughly and yet leaves X, Y, Z collinear) is rejected.

geometry-condition-minimality-pappus-hexagon

Kind: witness-replay
Status: checked

Supports: that the single non-degeneracy condition this certificate consumes is minimal ABSOLUTELY rather than budget-relative (ADR-0455)

Checker command

cargo test -p axeyum-cas --test geometry_certificate_artifacts

Evidence notes

The only proper subset of a one-element condition set is the empty one, and the six-collinear-points configuration satisfies all eight hypotheses while falsifying the conclusion -- so the conclusion is not in the plain hypothesis ideal, decided, with no budget, no monomial order and no algorithm anywhere in the argument. This is the second geometry fact whose minimality is established this way rather than by the 2^n subset audit `geometry_order_audit` runs, and on this theorem the audit is not an option: the Groebner route does not return here at all.

geometry-condition-redundancy-pappus-hexagon

Kind: witness-replay
Status: checked

Supports: that the two conditions this theorem states and does NOT use are individually redundant -- so the three-element set previously reported for it was not merely unproved-minimal but genuinely non-minimal

Checker command

cargo test -p axeyum-cas --lib geometry_certify && cargo run -p axeyum-cas --release --example pappus_condition_subsets -- 5 7 11

Evidence notes

This row exists because the previous lane's reading of the same evidence was the opposite one. Three attempts to find a configuration isolating a single condition had collapsed, always because killing one intersection forced the two other constructed points onto the very line the freed point was confined to, and that was recorded as an obstruction to claiming minimality. It is not: it is the reason each condition is redundant. The incidence hypotheses assert that X, Y and Z EXIST on their line pairs, so a configuration where one line pair degenerates does not lose that point, it frees it along a line -- and every way that can happen drags the other two cross points onto that same line. The distinction matters for the ledger because the two readings differ in what they license: 'we could not decide the subsets' invites a budget-relative fact, while 'a smaller subset provably suffices' means the larger set must not be filed at all.

Provenance

{
  "date": "2026-08-15",
  "established_by": "lane pappus-minimality: axeyum_cas::linear_elim (adjugate elimination of the single licensed 2x2 block) + axeyum_cas::cofactor_ansatz (bounded-degree ideal membership by exact sparse linear algebra, which settles the residue Buchberger does not return on) + axeyum_cas::geometry_certify::certify_by_linear_elimination with licensed_blocks (the condition subset chooses the decomposition, not the other way round) + axeyum_cas::geometry_check (independent re-derivation)",
  "source": "classical; coordinatised and certified with three conditions by the `euler-linearity` lane, which held it off the ledger because it could not establish minimality, and completed by the `pappus-minimality` lane, which found that the three-condition set was not minimal at all",
  "prior_art": [
    {
      "who": "Pappus of Alexandria",
      "what": "if A, B, C lie on one line and D, E, F on another, the three cross intersections AE.BD, AF.CD and BF.CE are collinear",
      "where": "Synagoge (Mathematical Collection), Book VII, propositions 138-139, c. 340 CE",
      "attribution": "standard historical attribution; this lane did not consult the primary source"
    }
  ]
}