TheoremStatement: 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.

The shoelace formula for the area of a counterclockwise simple polygon

Statement

The shoelace formula gives the Jordan content of a counterclockwise simple polygon.

Precisely, if its cyclic boundary vertices are $v_{i} = (x_{i}, y_{i})$ for $i < n$ , with $v_{n} = v_{0}$ , then

$cont (P) = \frac{1}{2} \sum_{i < n} (x_{i} y_{i + 1} - y_{i} x_{i + 1}) .$

Facts & Assumptions

Given: A counterclockwise simple polygonal region $P$ with cyclic vertices $v_{0}, \dots, v_{n - 1}$ and $v_{n} = v_{0}$ (Simple polygonal regions, diagonals, and triangulations).

[L1]

A simple polygon is Jordan measurable and its content is the sum of the triangle contents in any triangulation (A simple polygon is Jordan measurable and its content is the sum of the contents of its triangles).

[L0]

Every simple polygon admits a triangulation (Every simple polygon admits a triangulation).

[L2]

A triangle has content one half of the absolute determinant of two displacement vectors (A triangle has content $\frac{1}{2} ∣ \det [B - A C - A] ∣$ , equal to half base times height when the chosen side is nonzero).

[L3]

Finite sums are additive and commute with scalar multiplication (Laws of finite sums and finite products).

Proof

technique · direct

1.1

Choose a triangulation by [L0] and orient every triangular face counterclockwise. By [L1] and [L2], the polygon content is the sum over faces of one half of the signed boundary-edge expression $\det [p, q] + \det [q, r] + \det [r, p]$ .

L0L1L2choose

2.1

By [L3], the finite face sum may be regrouped by oriented edges. Every internal edge is traversed once in each direction by its two incident faces, so its two determinant terms cancel.

step 1.1L3algebra

3.1

Only the counterclockwise boundary edges remain. A triangulation may subdivide the polygon edge from $v_{i}$ to $v_{i + 1}$ at ordered points $p_{j} = (1 - t_{j}) v_{i} + t_{j} v_{i + 1}$ , but direct bilinearity gives $\det [p_{j}, p_{j + 1}] = (t_{j + 1} - t_{j}) \det [v_{i}, v_{i + 1}]$ , so [L3] makes the subdivision sum equal $\det [v_{i}, v_{i + 1}]$ . This includes the final edge from $v_{n - 1}$ to $v_{0}$ ; expanding the determinants gives the stated cyclic shoelace sum.

step 2.1L3algebra∎

Depends on

Used by

An irregular pentagon computed by triangulation and the shoelace formula Example

Dependency tree · two levels

33 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

Geometry: Combinatorics & Algorithms 2020, Exercise 4.14 (standard reference, not scraped)