Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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 complement of a polygonal arc in R2 is polygonally connected

Facts & Assumptions

Given: A polygonal arc A and points x,yA.

[F1]

A polygonal path is specified by a finite list of vertices and is a path in the ambient subset (Polygonal paths and polygonally connected subsets of Rn).

[L1]

A polygon has exactly two complementary regions, each with the polygon as frontier (Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each).

Proof

technique · constructive
1.1

Complete A to a polygon P=AB, where B is a polygonal arc with the same endpoints as A, has no other point in common with A, and avoids x,y. To construct B, take a sufficiently thin polygonal regular neighbourhood of the finite arc A: disjoint small vertex neighbourhoods joined by narrow strips along the edge interiors form a polygonal disk, and either boundary chain, capped to the two endpoints, supplies B. General position permits the finitely many boundary vertices to avoid x,y.

F1construct
2.1

By [L1], P has regions U and V. If x,y lie in the same region, polygonal connectedness of open components joins them there. If they lie in opposite regions, choose a point z in the relative interior of B. A sufficiently short segment transverse to B at z has one endpoint zU in U and the other zV in V. Join x to the endpoint on its side and y to the other by polygonal paths within those regions, then concatenate those paths with zUzzV.

step 1.1F1L1
3.1

The paths in step 2.1 avoid all of P except possibly at zB, and BA consists only of the two common endpoints, so the concatenated path avoids A. Since x,y were arbitrary, R2A is polygonally connected.

step 2.1discharge-construct

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 100 results over 18 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