dotCooCoo e314c9a4f2 linesweeper: the left-scan lemma in docs/sweep.typ takes ordering on alpha^(i+1) ...

The lemma for the intersection scan to the left asked for the ordering
invariant on (alpha^1, ..., alpha^i) and the crossing invariant on
(alpha^1, ..., alpha^(i+1)). The bidirectional lemma applies it with
alpha^(i+1) = beta before the extended list is known to satisfy the
crossing invariant, so the premises now mirror the right scan: ordering
on (alpha^1, ..., alpha^(i+1)), crossing on (alpha^1, ..., alpha^i).

The argument that the order invariant holds between events cited a
"third invariant"; the document defines two, and it now cites the
crossing invariant.

SOURCE.json gets a local_patches entry and the new sha256 of
docs/sweep.typ, and README.craft.md lists the change.

2026-11-11 21:37:35 -08:00

..

sweep.typ

linesweeper: the left-scan lemma in docs/sweep.typ takes ordering on alpha^(i+1)

2026-11-11 21:37:35 -08:00