CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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 $(B - A, C - A)$ is linearly dependent.

Facts & Assumptions

Given: Vertices $A, B, C \in R^{2}$ .

[L1]

Every triangle $T (A, B, C)$ has content $\frac{1}{2} ∣ \det [B - A C - A] ∣$ (A triangle has content $\frac{1}{2} ∣ \det [B - A C - A] ∣$ , equal to half base times height when the chosen side is nonzero).

[L2]

For a real square matrix, $∣ \det M ∣$ is the ordinary absolute value of its real determinant (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[L3]

A finite vector list is linearly dependent when a nonzero scalar list has zero linear combination (Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent).

Proof

technique · direct

1.1L1L2L3algebra

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.

2.1L1L2L3algebra∎

For the converse implication, suppose the content is zero. By [L1] and [L2], $\det [B - A C - A] = 0$ . If $B - A = 0$ the list is dependent by [L3]; otherwise one coordinate of $B - A = (u_{1}, u_{2})$ is nonzero, and the equation $u_{1} v_{2} - u_{2} v_{1} = 0$ for $C - A = (v_{1}, v_{2})$ shows by division in that nonzero coordinate that $C - A$ is a scalar multiple of $B - A$ . Thus [L3] gives collinearity.

Depends on

Used by

Three collinear vertices give a triangle of zero content Example

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

W. F. Trench, Introduction to Real Analysis, §7.3 (standard reference, not scraped)