LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

Midpoint subdivision of a triangle cancels every interior edge and preserves its outer boundary integral

Statement

Let $f$ be continuous on the filled triangle $Δ [a, b, c]$ of Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter, and put

$p = \frac{a + b}{2}, q = \frac{b + c}{2}, r = \frac{c + a}{2} .$

Then

$I_{f} [a, b, c] = I_{f} [a, p, r] + I_{f} [p, b, q] + I_{f} [r, q, c] + I_{f} [p, q, r] .$

The identity remains valid when vertices coincide or are collinear.

Facts & Assumptions

Given: The ordered vertices $a, b, c$ , their side midpoints $p, q, r$ , and a function $f$ continuous on the filled triangle.

[L1]

Reversing a rectifiable contour negates its complex line integral, while concatenating compatible contours adds their integrals (Complex line integrals change sign under reversal and add under concatenation).

Proof

technique · direct

1.1

In the order fixed by the triangle definition, the four boundary edge lists are $(a \to p, p \to r, r \to a)$ , $(p \to b, b \to q, q \to p)$ , $(r \to q, q \to c, c \to r)$ , and $(p \to q, q \to r, r \to p)$ .

given

2.1

In their sum, the interior pairs $p \to r, r \to p$ , $q \to p, p \to q$ , and $r \to q, q \to r$ cancel by reversal, while concatenation joins the surviving pairs $a \to p \to b$ , $b \to q \to c$ , and $c \to r \to a$ into the three outer edges.

step 1.1L1

3.1

Additivity under concatenation now gives exactly the displayed integral identity; reversal and concatenation also hold for constant and collinear segments, so no nondegeneracy was used.

step 2.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 54 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

E. Stein and R. Shakarchi, Complex Analysis, Ch. 2, Theorem 1.1 (standard reference, not scraped)