Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A triangle has zero Jordan content if and only if its vertices are collinear

Statement

A triangle has zero Jordan content if and only if its vertices are collinear.

Here collinear means that the displacement list (BA,CA) is linearly dependent.

Facts & Assumptions

Given: Vertices A,B,CR2.

[L1]

Every triangle T(A,B,C) has content 12det[BA CA] (A triangle has content 12det[BA CA], equal to half base times height when the chosen side is nonzero).

[L2]

For a real square matrix, detM is the ordinary absolute value of its real determinant (For n1, the determinant over a commutative ring by the Leibniz formula, and detA for a real matrix).

Proof

technique · direct
1.1

For the forward implication from collinearity to zero content, dependence in [L3] makes one of the two displacement vectors a scalar multiple of the other, including when either is zero; the two columns then have determinant zero, so [L1] and [L2] give content zero.

L1L2L3algebra
2.1

For the converse implication, suppose the content is zero. By [L1] and [L2], det[BA CA]=0. If BA=0 the list is dependent by [L3]; otherwise one coordinate of BA=(u1,u2) is nonzero, and the equation u1v2u2v1=0 for CA=(v1,v2) shows by division in that nonzero coordinate that CA is a scalar multiple of BA. Thus [L3] gives collinearity.

L1L2L3algebra

Depends on

Used by

Dependency tree · two levels

28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources