Applications

Where does circular structure already live in the real world? Schedules repeat. Signals oscillate. Buffers wrap. Positions in a transformer rotate. The applications unit is a tour of domains where periodic, rotational, or phase-like structure is already present — and where making it explicit lets you test and verify it.

Unit Goal

For each domain, identify its circular address space and its repeated action, and learn to separate the Lean-proved finite seeds from the claims that still need benchmarks.

The Idea

Every application reuses the same small vocabulary from S1:

address -> stride -> orbit -> period -> phase -> checked status

The claim is not that circular language automatically improves every domain. It is narrower and more honest: where the structure is genuinely periodic, an explicit finite representation can be checked, and a handful of finite facts can be Lean-proved. Benchmarks and fixtures are executable references, not proof of real-world performance or usefulness — so for each page, ask:

What is the circular address space?
What is the stride, phase, schedule, or repeated action?
Which claims are Lean-proved finite seeds, and which still require benchmarks?

Case-Study Tracks

Classical bridges — Erdős-style combinatorics restated through Circle vocabulary (Lean-checked wrappers, not new results).
AI — phase channels, cyclic memory, coil retrieval, routing, and adapter-block indexing seeds.
Circle phase probe demo — a tiny executable periodic-label probe showing circle phase features as a learning prelude, not a proof certificate.
ML engineer quickstart — one guided first-run path for the phase probe plus RoPE, KV-cache, sparse-attention, and recurrence receipts.
RoPE certifier — the flagship applied demo: proof-carrying position-distinguishability certificates for exact discretized rotary phase banks and the current bounded standard-channel frontier.
Position phase banks — generic finite residue/divisibility contracts for sinusoidal, RoPE-family, scaled, and 2D positional phase descriptors.
AI contract ladder — guided sequence from RoPE phase certificates to KV-cache freshness, sparse-attention coverage, recurrence schedules, and circulant mixer guarantees.
AI contract suite — compact working entry point for RoPE, KV-cache, sparse-attention, recurrence, and the public contract-pack certificates.
AI contract runner — parameterized CLI and Python API for turning your RoPE, KV-cache, sparse-attention, or recurrence config into a theorem-linked receipt.
KV-cache ring buffer — proof-carrying finite slot and retained-window certificates for ring-buffer cache indexing.
Sparse attention coverage — proof-carrying finite coverage, gap-witness, and candidate-budget certificates for local-window plus stride-family sparse plans.
Circle graph coverage — graph-shaped wrapper for finite direct positive-lag coverage on circular sparse-attention layouts.
Circular statistics contracts — finite same-phase, wrapped-distance, residue-list, and histogram facts with executable circular mean/resultant helpers.
Cyclic equivariance contracts — finite shift equivariance, sum-pooling invariance, circulant-layer equivariance, and minimal reflection laws.
Phase loop contracts — finite loop charge, vortex-charge vocabulary, closed-loop gauge cancellation, phase locking, and winding reconstruction.
Looped recurrence contracts — guided finite recurrence-budget, exit-certificate, token-route, middle-block, and multi-resolution schedule contracts.
Strided candidate fanout — finite stride-orbit traversal and duplicate-collapsed candidate-budget certificates.
Cyclic memory residue winding — finite alias-provenance certificates that keep residue and winding together.
Multicoil phase features — joint-repeat and relative-shift certificates for finite phase-bank features.
Circulant and block-cyclic mixers — structured-mixer parity and parameter-accounting certificates.
Physics — finite gauge links, path holonomy, Wilson-loop certificates, plaquettes.
Generative structures — seed-rule provenance and exact-regeneration fixtures.
Compute — cyclic addresses, direction bins, stride layouts, round-robin schedules.
Rendering — direction-bin sampling vocabulary.
Data analysis — finite phase coordinates and synthetic periodic-signal fixtures.
AI contract pack audit — generated minimum-field checklist for downstream consumers of the public contract pack.
Application proof audit — representative theorem-card appendix for the application unit.
RoPE proof audit — focused theorem-card appendix for the certifier’s discrete, real-phase, rational-margin, and standard-channel proof families.
KV-cache proof audit — theorem-card appendix for slot, window, trace, stale-request, live-window, and sink-window claims.
Sparse attention proof audit — theorem-card appendix for coverage, gap, count, candidate-range, period-threshold, and dedup-loss facts.
Looped recurrence proof audit — theorem-card appendix for loop budgets, exits, active-token boundaries, routes, and recurrent-state closure.

These are active but exploratory tracks: theorem cards are the status source, and benchmarks and fixtures are executable references, not proof of real-world performance or usefulness. See What “Proved” Means Here.

Checkpoint

Pick one application page and name its finite circular address space before reading any theorem card.

How To Read This Unit

Start with the page whose domain you care about, not with the theorem index. Each page should teach the domain object first and then expose the proof trail:

concept -> finite circular object -> example -> theorem card -> code/certificate -> non-claim

If you want to audit the application theorem cards directly, use the Application Proof Audit. If you are here for AI, start with the AI Contract Suite, run your own parameters through the AI Contract Runner, then walk the AI Contract Ladder.