Lemma. The local chord formula [cn-0014]

Status:

Statement. Let \(C,E\) be oriented straight chords of a round disk, with four distinct boundary endpoints. Write \(\partial C,\partial E\) for their endpoint sets and \(\epsilon _C(u),\epsilon _E(w)\) for their endpoint coefficients [cn-0068]: \(-1\) at the start of the corresponding chord and \(+1\) at its end. Choose a boundary cut avoiding the endpoints. The counterclockwise comparison sign [cn-0011] \(T(u,w)\) is \(+1\) if \(u\) precedes \(w\) when reading from the cut, and \(-1\) otherwise. Then their signed intersection [cn-0010] is

\[I(C,E)=\frac 12\sum _{u\in \partial C}\sum _{w\in \partial E}\epsilon _C(u)\epsilon _E(w)T(u,w).\]

Proof. Moving the cut past an endpoint changes the expression by a multiple of the other chord's total endpoint coefficient, which is zero. Cut just before the start of \(C\). The expression simplifies to minus the sum of the coefficients of \(E\)'s endpoints on the open counterclockwise arc from the start to the end of \(C\). This boundary arc lies on the right of directed \(C\).

If the endpoints do not alternate, that sum is zero. If they alternate, \(E\) goes from right to left or from left to right across \(C\), giving respectively \(+1\) or \(-1\). These are precisely the determinant signs of the two chord directions.

Proof dependencies
Signed intersections [cn-0010]; Comparison signs [cn-0011]; Endpoint coefficients [cn-0068]
Provenance
OpenAI, 23 September 2026 [cn-0042], equation (3.3), inside the proof of Lemma 3.1; reconstructed as a reading account on 9 October 2026. Lean source: ChordPairing.