Classical Bridges

This page is the reader-facing bridge between Circle Calculus and the established Erdos-style combinatorics lanes in the proof-backed showcase. It exists to make the hard-math advertisement auditable without forcing readers to start in the theorem index.

These are proof-backed bridges to established mathematics, not new proofs of the imported theorems and not progress claims on open Erdos problems. This page is not proof by itself; a theorem card below is Lean-proved only when the generated theorem data and local Lean build support that status.

Why This Page Matters

Circle Calculus should earn attention by showing that it can express structures mathematicians already care about, then show where the Circle presentation adds inspection value. The current hard-math bridge set covers five lanes:

zero-sum and sumset structure on cyclic groups,
Katona’s circle method and Erdos-Ko-Rado,
Roth-style three-term progression structure,
Hales-Jewett and Ramsey-style unavoidable lines, and
circulant graph geometry.

Read these as standard-math parity demonstrations first. The Circle-native value is the audit trail: finite-circle vocabulary, examples in Python sidecars, theorem ids, papers, and explicit boundaries.

Bridge Map

Showcase	Standard Anchor	Circle Presentation	Boundary
SHOW-001	EGZ and Cauchy-Davenport	zero-sum witnesses and prime-circle sumsets over `C_n` and `C_p`	no new EGZ or Cauchy-Davenport proof
SHOW-002	Katona and Erdos-Ko-Rado	cyclic-order counting atoms and intersecting-family handles	no new EKR proof or extremal classification
SHOW-003	Roth and three-term progressions	finite witness search tied to formal Roth handles	no improved bounds or cyclic transfer theorem
SHOW-004	Hales-Jewett and Ramsey structure	finite coloring examples tied to formal unavoidable-line theorems	finite searches are examples only
SHOW-005	cycle, circulant, connected, and unit-distance graph vocabulary	cyclic graph models with checked graph handles	no unit-distance or distinct-distance progress claim