Simson's line: the feet of the perpendiculars from a concyclic point are collinear, and the minimal condition set depends on the FIELD rather than on the budget
This page records one proposition and the evidence attached to it. Text from the source ledger is shown as record data.
Let A, B, C, P be points of the plane whose concyclicity determinant vanishes -- they lie on a common circle or on a common line. Let X lie on line BC with PX perpendicular to BC, Y on line CA with PY perpendicular to CA, and Z on line AB with PZ perpendicular to AB. If |BC|^2, |CA|^2 and |AB|^2 are all nonzero, then X, Y and Z are collinear. Over the real plane those three conditions say exactly that A, B and C are pairwise distinct, so read there this is Simson's theorem (Wallace, 1799) in its classical forward direction: P on the circumcircle of a triangle ABC implies the three feet are collinear. The three conditions are minimal, and the minimality is a statement about characteristic zero rather than about the real plane -- a distinction this fact exists to keep visible. Over a field containing i, |BC|^2 = 0 does NOT imply B = C, because x^2 + y^2 has the isotropic directions (1, +-i); a side line can be perpendicular to itself, its foot floats free along it while the other two stay pinned, and the conclusion fails. Each condition's necessity is exhibited at exact Q(i) points: A=(1,i), B=(1,0), C=(0,0), P=(-i,1) all lie on the circle -(x^2+y^2) + x + i*y = 0, the feet X=(-i,0) and Z=(1,1) are pinned, Y is free along the isotropic line CA, and Y=(0,0) leaves X, Y, Z a triangle -- so |CA|^2 != 0 is needed even though |BC|^2 and |AB|^2 are nonzero. The same four points relabelled cyclically give the other two. Over the REALS the picture is the opposite one and is stated here rather than left for a reader to assume: two of the three conditions are redundant, because B = C makes lines CA and AB the same line, hence Y = Z, hence X, Y, Z collinear whatever X does. Only the total collapse A = B = C breaks the theorem over the reals, and the configuration A = B = C = (0,0), P = (1,0), X = (0,1), Y = (2,0), Z = (4,0) is committed for that. So the minimal real condition set is any one of the three singletons and the minimal characteristic-zero set is all three; the certificate proves the second, and reading it as the first would overstate what it establishes.
The graph shows direct ledger edges. Follow a node to open its artifact page.
0 direct dependencies0 direct dependents
Evidence
geometry-certificate-simson-line
Kind
witness-replay
Status
checked
Supports: the saturated cofactor certificate over the three isotropy conditions, re-checked from the committed artifact by a checker that shares no code with the search that produced it
Checker command
cargo test -p axeyum-cas --test geometry_certificate_artifacts && python3 scripts/check-geometry-fact-transcription.py F:geometry-simson-line
Evidence notes
The certificate uses the Rabinowitsch trick three times: fresh variables Zinv0, Zinv1, Zinv2 and the generators `|BC|^2 * Zinv0 - 1`, `|CA|^2 * Zinv1 - 1`, `|AB|^2 * Zinv2 - 1`. Specialising each Zinv to the inverse of its condition is legitimate exactly when that condition is nonzero, and that is the ONLY place the side conditions enter. Every tamper control in the cited suite runs against this certificate: 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 counterexamples is rejected, and replacing one with the on-locus-but-harmless configuration (A = B = C = (0,0) with the three feet back on the x-axis, which annihilates all three conditions just as thoroughly and yet leaves X, Y, Z collinear) is rejected. One control is new and exists for this certificate: `a_gaussian_counterexample_with_its_imaginary_part_dropped_is_rejected` deletes the imaginary part of a Q(i) witness and requires rejection, because the same real parts alone are an ordinary configuration that SATISFIES the theorem -- a checker that read the file and ignored the new field would accept a certificate whose negative controls prove nothing, and would look exactly like a passing run.
geometry-condition-minimality-simson-line
Kind
witness-replay
Status
checked
Supports: that the three-condition set is minimal ABSOLUTELY (ADR-0455) and independently of the producer's decomposition (ADR-0460) -- over characteristic zero, which is the field the certificate is a theorem of
Checker command
cargo test -p axeyum-cas --test geometry_certificate_artifacts && cargo test -p axeyum-cas --lib geometry_corpus
Evidence notes
ADR-0460 asks two things of an absolute minimality claim: every removal test decided, and the test independent of anything the producer chose. Both hold here and neither is established by a search. The subset search is not consulted at all: each refutation is a single evaluation of the hypothesis, condition and conclusion polynomials at one exact point, with no budget, no monomial order and no algorithm in the argument. `searchable_subsets` now uses the same refutations to PRUNE the search rather than to audit it afterwards, which is ADR-0460's preferred remedy in its cleanest form -- a subset that is dropped because a counterexample refutes it cannot later be mistaken for a subset the producer's decomposition could not pay for. On this theorem that prunes all seven proper subsets and leaves one elimination to run; without it the search spends its budget on subsets that provably cannot succeed. The nine certificates that predate the change re-emit BYTE FOR BYTE -- `emit_geometry_certificates` reported `0 written, 10 unchanged` on the first full run after the pruning and the Q(i) format extension landed together, and `1 written, 9 unchanged` on a later one whose single write was this certificate's own witness prose. Either way the nine are untouched, so the change altered reach and cost and no evidence at all.
geometry-real-versus-complex-simson-line
Kind
witness-replay
Status
checked
Supports: that the minimality above is NOT a claim about the real plane, and that over the reals the same theorem needs only ONE of the three conditions -- so a reader who takes the certificate's condition set for the classical hypothesis set overstates it
Checker command
cargo test -p axeyum-cas --test geometry_certificate_artifacts
Evidence notes
This row exists because the two readings license different ledger entries and the difference is invisible in the certificate. A cofactor identity has rational coefficients, so it holds in every Q-algebra: what a certificate proves is a theorem of EVERY field of characteristic zero, and there is no way to make it a statement about the real plane specifically. The forward implication therefore needs no transfer principle at all -- substitute reals into a polynomial identity, take Zinv_k := 1/condition_k, and the conclusion follows -- which is the standard reading in this literature (Pottier 2010 states the certificate-level version; Harrison 2009 states the model-level one, `if a universal formula holds over C it also holds over R`). Where the two readings come apart is the CONDITIONS, and they come apart in the direction that inflates rather than deflates: the certificate's three conditions are minimal over characteristic zero and NOT minimal over the reals. The previous lane (`pappus-minimality`) posed exactly this as an open question and expected the real-plane answer to be the awkward one; it is the other way round, and the resolution is that both answers are true of different theorems. The ledger records the stronger hypothesis set because that is what the certificate consumes, and records here that the real-plane reading is weaker, rather than letting a characteristic-zero minimality claim be quoted as a real-plane one.
Provenance
{
"date": "2026-08-15",
"established_by": "lane simson: axeyum_cas::linear_elim (adjugate elimination of the three licensed 2x2 foot blocks) + axeyum_cas::geometry_certify::certify_by_linear_elimination with licensed_blocks and the new witness-pruned subset search + axeyum_cas::geometry_check (independent re-derivation, extended to replay Q(i) counterexamples)",
"source": "classical; coordinatised, certified and filed by the `simson` lane after the `pappus-minimality` lane recorded the field question as the deliverable and deliberately did NOT state the problem, on the grounds that what was missing was a decision about which field rather than a GeometryProblem",
"prior_art": [
{
"who": "William Wallace",
"what": "if a triangle is inscribed in a circle and perpendiculars are dropped from any point of the circumference to the sides, the feet of those perpendiculars are collinear",
"where": "T. Leybourn (ed.), Mathematical Repository, 1799; the attribution to Simson is traditional and mistaken, and the history is J. S. Mackay, 'The Wallace line and the Wallace point', Proceedings of the Edinburgh Mathematical Society 9 (1890), 83-91",
"year": 1799,
"attribution": "standard historical attribution, cross-checked against Mackay's historical study and the MacTutor biography of Wallace; this lane did not consult Wallace's original, and did not establish its volume or page"
},
{
"who": "Shang-Ching Chou and Xiao-Shan Gao",
"what": "Simson's theorem as the motivating example of a statement that Wu's method and the Groebner-basis method CANNOT confirm under 'A, B, C are not collinear' alone, and the isotropy conditions that fix it: isotropic(A,B) is defined as perpendicular(A,B,A,B), i.e. |AB|^2 = 0, which over the reals degenerates to A = B and over other models of metric geometry (e.g. C^2) does not",
"where": "'A Class of Geometry Statements of Constructive Type and Geometry Theorem Proving', CADE-11, 1992, section 2, example 2.1",
"year": 1992,
"attribution": "read within this lane from the authors' copy at mmrc.iss.ac.cn (a delegated literature search, not a memory of the paper); the two quoted phrases are verbatim from that PDF. The condition set this fact certifies is the one that paper prescribes, which was found AFTER the coordinatisation was chosen rather than copied from it -- the agreement is a cross-check, not a derivation"
},
{
"who": "John Harrison",
"what": "a Wu's-method run on Simson whose non-degeneracy output is squared-length conditions, with the field distinction stated explicitly: 'In the intended interpretation as real numbers, there is some redundancy, since bx - cx = 0 implies (bx - cx)^2 + (by - cy)^2 = 0. However, this is not in general the case over the complex numbers'; and the transfer direction this fact relies on, 'if a universal formula holds over C it also holds over R'",
"where": "Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009, section 5.12, pp. 414-424 (Simson at pp. 422-423)",
"year": 2009,
"attribution": "read within this lane from the PDF at kwarc.info (a delegated literature search, not a memory of the book); both quotations are verbatim. Page numbers are as reported by that copy and were not cross-checked against the print edition"
}
]
}
