AI

This page covers the Circle AI program, and it is important not to confuse its three tiers:

Proof-carrying architecture contracts (the AIT and selected AIRA families, below) — real structural facts about transformer components: strided-attention coverage, RoPE relative position, RoPE position distinguishability under a declared discretized phase bank, and circulant equivariance. This is the substantive proved content, and it is what makes circle math earn a place here.
Finite-indexing bookkeeping (the AIA / AIM / AIRA families) — elementary facts that an index stays in range and is unchanged by a full period, e.g. memory_slot(bank, token) = token mod bank. These are honest but trivial: they are instances of the S1 closure spine, infrastructure rather than evidence that circles help a model.
Exploratory fixtures (the -B ids) — tiny synthetic benchmarks with ordinary baselines and controls; not model-quality claims, and several are illustrative-only (see below).

Local compute language is MLX/Mac-first.

The flagship standalone contract is the RoPE position-distinguishability certifier. It lets a non-Lean reader provide a rotary-position configuration and receive a theorem-linked exact discrete collision certificate plus a separate numerical real-phase margin report.

For a guided sequence through the standalone contract pattern, read the AI contract ladder before opening the theorem shelves.

The exploratory fixtures (AIA-B*, AIM-B*, AIRA-B*, twenty-odd in all) follow one recipe: pit a circular feature against ordinary baselines — a scalar threshold, a learned-position lookup, a wrong-period table — plus a nonperiodic control where the circular feature should not win, with optional MLX scoring. That discipline (baselines and negative controls) is the good part. The honest caveat: many of these tasks are tautological by construction — the synthetic label is defined as a function of the phase, so a phase lookup wins by definition, demonstrating plumbing rather than usefulness. These fixtures are not model-quality claims and not performance claims.

Showcase evidence: SHOW-010 AI memory, loop, and adapter schedules.

How To Read This Chapter

Read the AI lane in this order:

Start with the contract pattern: circular address space, repeated action, formal boundary, executable fixture, and ordinary baseline.
Study the flagship RoPE certifier, because it is the clearest proof-carrying contract for a real ML engineering concern.
Use the KV-cache ring-buffer and sparse-attention sections as the next contract examples: both expose exact indexing or coverage facts without claiming model quality.
Treat phase channels, recurrence, adapters, and mixers as benchmark harnesses until they have public learned baselines and negative controls.
Open the theorem shelves only when you want source-level evidence; the main text is the guided path.

Case-Study Frame

The circular address spaces are phase channels, memory slots, adapter blocks, sparse-attention strides, and RoPE phase banks. The serious AI contribution is proof-carrying structure: exact coverage, collision, aliasing, and equivariance contracts that ordinary experiments often leave implicit. Performance stays a benchmark question.

What Circle Math Actually Proves Here

Most of this page is exploratory benchmark scaffolding. But several real transformer or transformer-adjacent components are finite-circle structures whose structural guarantees are now Lean-proved — not relabeled modular arithmetic, and not model-quality claims, but exact facts about architecture that practitioners actually reason about:

Strided (“coil”) attention coverage. A strided head lets each token attend to i, i±k, i±2k, … — a coil orbit on C_n. So the orbit/period theory is the reachability theory:

a stride-k head reaches exactly n / gcd(n,k) distinct positions (AIT-T0001);
it reaches every position iff gcd(n,k) = 1 (AIT-T0002, AIT-T0003);
a local+coil hybrid reaches any dependency lag reached by either the local window or the admitted coil path (AIT-T0010 through AIT-T0014);
a finite family of admitted coil strides has exact reach/miss conditions, local-window thresholds, complete-coverage iff no positive uncovered-lag witness, raw and clipped candidate-budget bounds, theorem-side candidate-list semantics, no-duplicate budget-survival criteria, finite positive-lag coverage iff, finite covered/uncovered-list iffs/counts, first-gap field semantics, public interval-summary certificates, concrete default-plan hit/gap witnesses, and a compact complete-coverage PASS fixture (AIT-T0015 through AIT-T0105).

That is a proved design rule for sparse/dilated attention: pick strides coprime to the context length and every token provably reaches every other; combine local and coil paths when the task mixes near and long dependencies.

The gap theorem is the contract form: it lets a tool report not only “these lags are reachable” but also “these lags are uncovered by this declared sparse plan.” That is coverage bookkeeping, not attention quality.

KV-cache ring-buffer safety. A fixed-size KV cache is a circular address space: token t writes slot t mod cache_size. The proved contract says what that finite address arithmetic can and cannot certify:

a token’s slot is always inside the declared cache size (AIM-T0059);
ordered same-slot collision is exactly divisibility of the token gap (AIM-T0061);
retained-window membership is exactly the next-overwrite boundary (AIM-T0069);
a non-future stale token is exactly one whose next same-slot overwrite has already happened (AIM-T0070);
a retained token has no later same-slot writer before the current read point (AIM-T0075);
a stale non-future token has an explicit later same-slot overwrite witness at token + cache_size (AIM-T0076);
a non-future token is stale iff some later write up to current reuses its ring-buffer slot (AIM-T0099);
under non-future duplicate-free request assumptions, adapter-request failure is exactly stale requested-member existence (AIM-T0100);
under the same request assumptions, stale requested-member count zero is exactly pass and positive stale count is exactly failure (AIM-T0101 through AIM-T0103);
the generated sink-window request list is exactly the pinned seen prefix plus filtered rolling live window policy (AIM-T0104 and AIM-T0105);
every generated sink-window request list is duplicate-free and bounded by sink_size + cache_size (AIM-T0110 and AIM-T0117);
when the fully seen sink prefix lies before the rolling live window, the generated request length is exactly sink_size + live_window_length (AIM-T0119);
the public sink_size = 4, cache_size = 16, current = 31 sink-window request has exactly 20 token entries (AIM-T0118);
a non-future token is retained iff there is no later same-slot writer in the finite trace up to current (AIM-T0077);
a non-future read batch is retained iff every requested token has no later same-slot writer in that finite trace (AIM-T0078);
a duplicate-free non-future read batch with no later same-slot writer for each token maps to duplicate-free ring-buffer slots (AIM-T0079);
the CLI packages those batch facts as a named modeled adapter request trace with a pass/fail certificate boundary.
the generated live-token list exactly matches retained-window membership, maps to duplicate-free slots, and gives a full-window finite slot-coverage contract (AIM-T0071 through AIM-T0074).

This is an implementation-facing safety contract for finite indexing and freshness bookkeeping. It does not prove paging quality, retrieval quality, memory savings, or deployment safety.

RoPE relative position. Rotary embeddings encode position as rotation; their defining property — interaction depends only on relative position — is the rotation law:

shifting query and key by the same amount leaves the relative phase fixed (AIT-T0004);
rotary rotations compose by adding strides (AIT-T0005).

RoPE position distinguishability. A discretized RoPE phase bank represents a position by residues modulo declared integer periods. This is not a claim that real RoPE has exact integer periods; it is the exact contract a certifier can check:

one-channel collision is equivalent to the period dividing the ordered position gap (AIRA-T0021);
one-channel distinguishability is equivalent to that period not dividing the gap (AIRA-T0022);
if a context fits inside one declared period, that channel is injective on the context (AIRA-T0023);
all-channel bank collision is equivalent to every declared period dividing the same gap (AIRA-T0024);
bank distinguishability is equivalent to at least one declared period not dividing the gap (AIRA-T0025);
if the bank contains a period at least the context length, every unequal pair in context is distinguished (AIRA-T0026).

The real-phase RoPE program is separate from that exact integer-period contract. It now has theorem-backed finite-margin seeds, including the rational/discretized 1/4099 context-4096 certificate, generated-gap and floor/ceiling nearest-integer bridges, interval-certificate and band-endpoint bridges, and genuine standard channel-0 interval seeds for 1 / (2*pi) through context 196608 at margin 1/328459. The generated D15 through D19 bridge theorems package conditional one-separating-channel bank consequences when a bank contains standard channel 0. The bracket theorems package the channel-0 reading as: 1/104219 is proved through 64k and 1/328459 is proved through 192k; margins at or above 1/104218 are impossible once gap 710 is in context, and margins at or above 1/328458 are impossible once gap 103993 is in context. The D19 request classifier exposes that frontier as three statuses at context 131072: proved for 1/328459, impossible for 1/328458, and undecided_margin_gap for the narrow open interval between them; AIRA-T0238 proves the public 2/656917 undecided probe lies inside that open gap. AIRA-T0239 adds a Dirichlet witness saying every nontrivial finite context has some in-context near-integer gap with error at most 1/context, and AIRA-T0240 turns that into the direct ceiling that any advertised finite-context margin strictly above 1/context is impossible. AIRA-T0139 through AIRA-T0141 power the generated D15/D16/D17/D18/D19 rational-band certificates without another large per-gap interval-case expansion. These are one-channel or conditional bank-level real-phase certificates plus certificate-generation infrastructure and a general upper-bound guardrail, not a full standard-RoPE bank theorem.

Circulant (“CoilLinear”) token mixing. A circulant mixer (c ⋆ x)ᵢ = ∑ⱼ cⱼ·x(i−j) is the C_n group algebra — the math behind FNet / long-convolution mixing. Its structure is proved:

it commutes with cyclic shift — translation equivariance for the circulant mixer structure (AIT-T0006);
circular convolution is commutative (AIT-T0007) and linear (AIT-T0008);
the cyclic shift is a genuine group action (AIT-T0009).

Open theorem-card shelf for the core AI architecture contracts

The honest split for AI: Lean proves structure (coverage, relative position, equivariance, and algebraic mixer laws) — facts it genuinely can certify; experiments prove performance (accuracy, efficiency, extrapolation) — which Lean cannot, and which remain benchmark work, not proof claims. See What “Proved” Means Here.

A Runnable Block And An Honest Experiment

The proved components above are assembled into a small, runnable CircleFormerBlock (RoPE encoding + coil sparse-attention + circulant mixing) in circle_math/applications/circle_transformer.py. Its tests don’t measure accuracy — they verify the proved properties hold in code: circulant shift-equivariance to machine precision, RoPE scores depending only on relative position, and strided-head coverage matching gcd(n,k) exactly.

For the performance question — which only an experiment can answer — there is a controlled, honestly-reported bias–variance study (circle_math/applications/circle_transformer_experiment.py): a circulant mixer (n parameters by construction, shift-structured bias) versus a dense mixer (n² parameters, no bias), both fit by exact least squares, on a shift-structured target and on an unstructured control. The measured held-out error:

target          n_train   circulant      dense     winner
shift-struct         12     0.0003       3.2636   circulant
shift-struct         24     0.0001       0.0064   circulant
unstructured         24     1.0156       0.0041   dense
unstructured        200     0.9784       0.0002   dense

The honest reading — including where circle structure loses: when the dependency is shift-structured, the circulant model generalizes far better from few samples (right bias, fewer parameters); when it is not, the circulant model hits an irreducible error floor — it structurally cannot represent a non-circulant map — and the dense model wins. The inductive bias helps iff the assumption holds. This is a controlled linear study, not a claim about deep transformers; it is exactly the kind of result the AI track should report straight, wins and losses alike.

AI Program Map

AI is now a dedicated Circle Calculus program, not a side note. The avenues to explore are:

phase channels and periodic feature routing,
cyclic memory slots, alias diagnostics, and retrieval fixtures,
coil/sparse attention for long-context path selection,
looped and recursive transformer schedules with loop phase, exit certificates, and overthinking guardrails,
adapter blocks, CoilLinear/circulant mixers, CoilRA, and block-cyclic parameter sharing,
RoPE, MultiCoil RoPE, winding-aware positions, and torus-valued positional views,
recurrent, state-space, and convolutional sequence models with explicit period structure,
harmonic, Fourier, circulant, and NTT-adjacent features,
quaternion, spherical, Hopf/fiber, and rotation-aware representations, and
proof-carrying model components whose indexing or schedule behavior can be checked in Lean.

Every avenue needs ordinary baselines, negative controls, and reproducible scripts before it becomes a claim about model quality or speed.

Optional Downstream Transfer Lane

Circle AI should stand on its own first: public theorem ids, executable fixtures, ordinary baselines, negative controls, and Living Book explanations must be useful without any private project. A local Theseus-Hive transfer lane exists as optional downstream context, but it is not the source of truth for Circle AI claims, so the operational details live in docs/THESEUS_HIVE_AI_TRANSFER.md rather than in this textbook chapter.

Circle AI proofs and fixtures
  -> recurrence / routing / memory / phase / mixer contracts
  -> private Theseus-Hive experiments
  -> ordinary baselines and negative controls
  -> only then usefulness claims

The public-safe generic contract pack is built with make circle-ai-contracts. The older Theseus compatibility view can still be built with make theseus-ai-contracts, and the sanitized feedback import can still be built with make theseus-ai-feedback when the private companion workspace is present. Those compatibility outputs are handoff artifacts, not textbook prerequisites and not public evidence that Circle Calculus improved an AI system.

This lane is optional downstream transfer context. Lean can certify finite schedule, index, coverage, relative-phase, and equivariance facts; public standalone benchmarks must carry public claims, and private downstream benchmarks remain separate evidence.

Phase-Channel Baseline Path

The first AI fixture asks the smallest useful question: if labels are actually periodic, can a phase-channel lookup recover them, and do ordinary controls stay visible? The same widget also includes a nonperiodic scalar-threshold task where the circular feature should not be treated as helpful.

Learned-Feature Baseline Path

The next AI fixture keeps the feature tiny but adds ordinary learned controls. A correct cyclic phase table is compared against a dense scalar threshold, an absolute-position lookup, and a wrong-period phase table. The nonperiodic control keeps the scalar threshold visible as the right baseline when the target is not periodic.

Harmonic/Fourier Feature Path

The harmonic feature fixture asks the same known-period question with a sine/cosine encoding instead of an integer phase key. The correct period should match the phase lookup, while a wrong-frequency feature, scalar threshold, and absolute-position lookup remain visible controls.

This is the safe first step toward RoPE-adjacent thinking: it shows the finite phase arithmetic behind a Fourier-style feature, not a language-model result.

Backend Parity Path

Backend parity asks a different question from model quality: do the deterministic fixture scores agree when the same predictions are scored on CPU and optional MLX? The static widget shows the fixed CPU cases used by AIA-B0003; the local Python fixture is still the source for MLX availability and MLX-vs-CPU delta.

Cyclic Memory Slot Path

Cyclic memory starts with a plain finite address: memory_slot(bank_size, token) = token mod bank_size. The useful interface question is not whether this improves a model by itself, but whether slot assignment, alias collisions, and closure after full bank passes are visible before running a benchmark.

The widget below shows that finite layer. It is not a retrieval-quality result and not a memory-scaling claim; it is only the indexing and collision bookkeeping used by the current Lean/Python artifacts.

The public contract-pack version of this fixture is available as a standalone certifier. It reports the selected event’s residue slot, winding number, same-residue alias class, maximum alias load, theorem ids, and downstream readiness gate.

python scripts/cyclic_memory_certify.py
python scripts/cyclic_memory_certify.py --format json
python scripts/circle_ai_contract_ready.py --kind cyclic_memory_residue_winding --digest --field max_alias_load --include-recommendations

The generic AI contract pack exposes two planner-facing records for this fixture. MEMORY-ATTACH-WINDING-ALIAS-PROVENANCE tells a consumer to keep winding/provenance beside same-slot aliases, and MEMORY-AUDIT-FINITE-ALIAS-LOAD reports finite slot-load pressure for the declared trace. They are audit records for residue/winding bookkeeping, not retrieval, memory capacity, allocation-policy, throughput, or model-quality claims.

The second memory contract is a KV-cache ring-buffer window certificate. Given cache_size, current, and token, the CLI and sidecar report the token slot, current slot, lag from current, whether the token is retained, whether a retained older token is distinct from the current slot, whether the next same-slot overwrite occurs after the current read point, whether the token is stale by the overwrite boundary, whether any later token up to current has reused the same slot, whether a stale token has the explicit same-slot overwrite witness token + cache_size, and whether retention is equivalent to no later same-slot write in the finite trace. They also check ordered, unordered, and batch slot distinctness for retained tokens in the same live window, the batch-level trace iff for declared non-future reads, trace-fresh duplicate-free read-batch slot distinctness, duplicate-free ordered live-window subrequest pass status, a named modeled adapter request-trace pass/fail certificate with stale requested-member count, a generated live-window finite slot-coverage flag, and an optional sink-window policy report for pinned seen-prefix tokens plus the filtered rolling live window. The Lean theorems AIM-T0059 through AIM-T0079, AIM-T0086 through AIM-T0089, AIM-T0091 through AIM-T0105, AIM-T0108 through AIM-T0110, and AIM-T0117 through AIM-T0119 certify the finite slot, overwrite-window, generated-live-window, sink-window policy, sink-window request-size budget, subrequest, stale-member success/failure, counted stale-request, and compact-boundary consequence facts, including the iff that retained-window membership is exactly the non-future plus next-overwrite-after-current boundary, the stale converse where the next same-slot overwrite is at or before the current token, the retained-token no-same-slot-overwrite-before-current guard, the stale-token same-slot witness, the single-token and batch trace iffs, trace-fresh batch slot distinctness, the generated live-window/full-coverage contracts, the generated sink-window exact-membership contract, the general duplicate-free generated sink-window request theorem, the sink_size + cache_size length bound, the exact sink_size + live_window_length count condition for disjoint fully seen sink prefixes, the compact adapter request pass iff, the duplicate-free ordered subrequest pass theorem, exact stale-member pass/fail iffs under non-future duplicate-free request assumptions, stale-count zero/positive pass/fail iffs, and direct all-retained/slot-distinct consequences of the compact boundary checklist; the request-trace certificate packages those facts for a modeled read request, not a real kernel, serving stack, paging policy, deployment-safety proof, throughput result, memory-saving result, retrieval-quality claim, or sink-token model-quality claim.

Open the guided KV-cache ring-buffer lesson.

python scripts/kv_cache_certify.py --cache-size 16 --current 31 --token 20 --batch-tokens 20,24,29,31 --sink-size 4
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_kv_cache_ring_buffer.py
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_kv_cache_ring_buffer.py --format json
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_kv_cache_ring_buffer.py --format markdown

Committed result fixtures:

KV-cache JSON: kv_cache_ring_buffer.json

KV-cache Markdown: kv_cache_ring_buffer.md

Coil Retrieval Reachability Path

Coil retrieval asks a narrower question than “does this improve attention?”: can a fixed finite stride path reach a known long-lag dependency that a local window misses, while ordinary local attention still wins on a near-lag control?

AIM-B0002 is the current executable fixture for that question. The widget below exposes the candidate-set arithmetic behind it: selected coil path, local window, wrong stride, full-attention oracle, and near-lag controls. It is not a retrieval-quality claim and not a replacement for learned attention baselines.

Content-Gated Coil/Local Path

The next retrieval question is routing: if a query needs a long dependency, use the coil path; if it needs a near dependency, use the local window. The current AIM-B0004 fixture is hand-coded so the route is visible and auditable before any learned gate is introduced.

The widget below compares content-gated routing against static coil, static local, wrong-gate, union-candidate, and full-attention oracle baselines. Candidate budget is shown beside hit rate so a full oracle does not look cheaper than it is.

The learned version fits a tiny phase-to-route lookup from training examples, then compares it with static coil, static local, wrong-period, flipped-gate, union-candidate, and full-attention controls. It is a route-table fixture, not a learned-model quality claim.

Hybrid Sparse-Attention Path

The next standalone sparse-attention step is not Theseus-specific: combine local and coil candidates, then ask whether the combined sparse set covers the dependencies it was designed for while staying cheaper than full attention.

AIM-B0016 is the current executable fixture. It mixes near dependencies with long dependencies that lie on the selected coil path. The hybrid local+coil candidate set reaches all structured targets with average candidate count 9, while the full-attention oracle uses 96 candidates. Local-only, coil-only, and wrong-stride controls miss part of the structured task. The nonstructured control is just as important: arbitrary lags are not covered by the sparse pattern, so full attention remains the oracle.

AIM-B0017 extends that idea from one coil stride to a finite stride family. This is the first multi-head sparse-attention coverage lesson: a family of admitted strides can cover a wider set of generated lags than a single stride while keeping candidate count far below full attention. It now emits an explicit coverage certificate too: for the default C_120 plan with local window 4, path length 3, and strides (7,13), only positive lags 1,2,3,4,7,14,21,13,26,39 are covered. The other 109 positive lags are gap certificates under AIT-T0020, with the concrete no-local/no-stride-step condition stated by AIT-T0021; AIT-T0028 proves the local miss condition is exactly window < lag for positive lags, AIT-T0022 records the dense-local complete-coverage limit, AIT-T0023 proves the local-only threshold is exact, AIT-T0024/AIT-T0025 prove the exact recursion for adding one stride to the family, AIT-T0026/AIT-T0027 prove the empty-family control reduces to local reachability, and AIT-T0029 through AIT-T0032 prove that conservative increases to local-window or path-length budgets preserve already covered lags. AIT-T0033 through AIT-T0035 package the certificate status: complete coverage is exactly no positive uncovered-lag witness, dense local coverage implies complete coverage, and conservative budget increases preserve complete coverage. AIT-T0036 through AIT-T0038 make raw candidate-budget accounting explicit, AIT-T0039 through AIT-T0042 add the tighter context-clipped deduplicated-budget cap min(context, raw_budget), AIT-T0043 through AIT-T0050 prove the theorem-side lag-candidate list has exact in-context reachability semantics, AIT-T0078 proves that complete coverage is equivalent to every generated positive lag in List.range' 1 (n - 1) appearing in that theorem-side candidate list, AIT-T0090 makes the covered-lag list proof-carrying, and AIT-T0081 through AIT-T0085 make the complementary uncovered-lag list proof-carrying: membership is exactly a semantic miss, zero uncovered lags is complete coverage, default lag 5 is explicitly listed as uncovered, and the default uncovered count is exactly 109. AIT-T0091 proves the default covered count is exactly 10, AIT-T0096 proves that a positive uncovered count is equivalent to the existence of an actual uncovered positive-lag witness, and AIT-T0097 proves that covered-count shortfall is equivalent to that same witness condition. AIT-T0086 through AIT-T0089 add the PASS counterpart: C_9, local window 2, path length 2, and strides (3,4,7) have no uncovered lags and preserve the raw lag/query candidate budget. AIT-T0051 through AIT-T0054 map reached lags into query-indexed predecessor candidates, AIT-T0055/AIT-T0056 prove no-collision lists deduplicate without budget loss, AIT-T0076/AIT-T0077 prove the iff endpoint that raw-budget survival is equivalent to no duplicates, AIT-T0057/AIT-T0058 derive those no-collision predicates from structural checks, AIT-T0059 through AIT-T0062 prove the first singleton no-wrap numeric sufficient condition, AIT-T0063 makes residue no-collision compositional across a finite stride family, AIT-T0064 proves a numeric no-wrap separation condition for the head/tail disjointness premise, AIT-T0065 proves duplicate-free residues for an ordered no-wrap separated stride family, AIT-T0066/AIT-T0067 lift separated families whose strides start beyond the local window to duplicate-free theorem-side lag candidates, AIT-T0068 through AIT-T0070 package query no-collision plus exact raw-budget endpoints under predecessor injectivity, and AIT-T0071 through AIT-T0075 prove the numeric window < n condition that supplies predecessor injectivity for the generated lag candidates. AIT-T0112 through AIT-T0119 add the count-based coverage endpoint: once generated lag candidates are positive and in context, unique lag count is an iff test for complete coverage; ordered no-wrap separated families and the broader no-zero-residue condition each discharge that range hypothesis structurally. AIT-T0120 through AIT-T0125 add the failure-side shortfall iffs for both lag-side and query-indexed unique candidate counts, including no-wrap and no-zero structural versions. AIT-T0126 and AIT-T0127 make the singleton no-zero rule exact: for one stride, the admitted path budget avoids zero residues exactly when it stops before the finite coil period. AIT-T0128 extends that exact threshold to finite stride families by requiring every admitted stride period to exceed the path budget. The wrong-family and nonstructured controls keep the claim honest.

AIT-T0129 and AIT-T0130 now package that period-threshold rule as the lag-side and query-side shortfall/gap equivalence used by the executable sparse-attention certificate. AIT-T0131 adds the failure-side witness: when a stride period is at most the path budget, the report constructs a concrete zero-residue candidate with step = period instead of merely saying the threshold failed. AIT-T0132 and AIT-T0133 make the corresponding failure booleans exact, linking no-zero failure to both the zero-residue witness and the period-threshold violation. AIT-T0134 and AIT-T0135 then certify the witness is first-alias exact: the reported period is positive, generates zero, and no smaller positive step for that stride does. AIT-T0136 adds the one-stride count version: for each stride, the number of admitted positive zero-residue aliases is exactly path_length / period. AIT-T0137 and AIT-T0138 make the family-total status proof-carrying too: the total is the sum of those counts, and total zero is equivalent to the no-zero structural condition in nonzero contexts. AIT-T0139 and AIT-T0140 make the public 4096 no-wrap planner row exact at the row level: 44 covered positive lags and 4051 uncovered positive lags are Lean-proved counts, not just Python fixture output. AIT-T0141 and AIT-T0142 make the public 8192 coprime planner row exact at the same count level, using the broader no-zero candidate-range route because the row is not no-wrap separated. AIT-T0143 and AIT-T0144 add the matching query-side count guarantees: every query index in those rows has exactly the reported raw-budget number of deduplicated predecessor candidates. AIT-T0145 through AIT-T0150 add exact lag/query dedup-loss semantics: zero loss is equivalent to no duplicate candidates, positive loss is equivalent to duplicate collision, unique candidates plus loss equals raw budget, and the sidecar’s C_16 alias-collision probe shows the positive-loss case. AIT-T0151 through AIT-T0154 add fixture-level pair-collision counts, separating simple dedup loss from the number of equal-candidate pairs. AIT-T0155 through AIT-T0158 add the reusable pair-count boundary semantics: zero pair count is equivalent to no duplicate candidates, and positive pair count is equivalent to duplicate collision, on both lag and query sides. AIT-T0159 and AIT-T0160 add the severity bridge: pair-collision counts bound deduplication loss on lag and query sides, so the excess field measures repeated multiplicity beyond ordinary lost-candidate accounting. AIT-T0161 through AIT-T0167 make first-gap and first-interval repair boundaries theorem-backed, AIT-T0172 gives the reusable final-lag condition for minimal dense fallback, and AIT-T0168 through AIT-T0170 prove that the default row’s complete repair window 119 is exact and minimal for the declared path/stride family.

Run the same certificate outside the browser:

python scripts/stride_family_certify.py --context 120 --strides 7,13 --path-length 3 --local-window 4
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_stride_family_sparse_attention.py
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_stride_family_sparse_attention.py --format json
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_stride_family_sparse_attention.py --format markdown

Committed result fixtures:

Stride-family sparse-attention JSON: stride_family_sparse_attention.json

Stride-family sparse-attention Markdown: stride_family_sparse_attention.md

This is the right kind of Circle AI evidence: useful when the dependency structure matches the circle/coil assumption, visibly wrong when it does not. It is candidate-set reachability and budget accounting only, not a neural attention-quality, runtime, memory, or model-quality claim.

Adapter Parameter-Budget Path

CoilRA-style adapter work needs ordinary accounting before it can make any efficiency claim: how many parameters does a dense adapter use, how many does a LoRA-style count use, and how much alias pressure is introduced when channels share a block-cyclic table?

AIRA-B0004 is the current executable fixture for that boundary. The widget below compares dense per-channel, LoRA-style low-rank, and block-cyclic shared-table counts, then shows how channels load into adapter blocks. It is not evidence about fine-tuning quality, runtime, memory, training stability, or hardware efficiency.

Circulant Mixer Validation Path

CoilLinear/circulant-mixer work starts with a basic validation question: does the circular convolution path produce exactly the same output as the dense circulant matrix it claims to represent?

AIRA-B0005 is the current executable fixture for that boundary. The widget below compares circular convolution with the dense circulant-matrix product, shows a wrong-shift control, and reports dense-vs-circulant parameter counts. It is not a neural-layer quality, runtime, memory, training-stability, or hardware-efficiency result.

Block-Cyclic Mixer Validation Path

Block-cyclic mixer work asks the next finite-addressing question: when a dense matrix cell (row, column) is represented by the shared cell (row mod block_size, column mod block_size), do the row and column residue rules close exactly as advertised?

The proved facts AIRA-T0011 through AIRA-T0015 certify the row/column cell bounds and closure under whole block-size passes. AIRA-B0007 is the executable fixture: it compares the block-cyclic matrix-vector path against the dense matrix it represents, records a wrong-row-shift control, and reports parameter/cell-alias diagnostics. It is not a neural-layer quality, runtime, memory, training-stability, or hardware-efficiency result.

The public structured-mixer contract packages the circulant dense-parity check and block-cyclic parameter/load accounting into one downstream-readable certificate. It is useful for checking a proposed structured mixer interface, not for claiming speed, quality, training stability, or hardware efficiency.

python scripts/circulant_block_cyclic_mixer_certify.py
python scripts/circulant_block_cyclic_mixer_certify.py --format json
python scripts/circle_ai_contract_ready.py --kind circulant_block_cyclic_mixer --digest --field max_abs_dense_delta --field block_to_dense_ratio --include-recommendations

The digest adds MIXER-AUDIT-CIRCULANT-DENSE-PARITY and MIXER-AUDIT-BLOCK-CYCLIC-PARAMETER-BUDGET as copy-safe audit records over theorem-linked fixture fields. They remain fixture/accounting records, not speed, memory, hardware-efficiency, or model-quality claims.

MultiCoil Positional Phase Path

MultiCoil/RoPE-style work begins with a modest bookkeeping question: if a position has several phase periods, what is its combined phase tuple and when does that tuple repeat?

AIRA-B0002 is the executable fixture for positional phase labels. AIRA-T0016 through AIRA-T0020 add the first formal two-period closure spine: each phase coordinate is bounded by its period, position zero maps to the zero pair, and adding period_a * period_b or any whole number of product-cycle passes preserves the pair. AIRA-B0008 is the matching closure fixture; it compares the proof-backed product cycle, the ordinary lcm cycle, and a wrong-shift control.

The widget below shows the combined phase tuple, product-cycle closure, lcm comparison, and wrong-shift mismatch. It is not evidence that MultiCoil improves RoPE, attention, or language models.

The public phase-feature contract packages the same kind of finite evidence as a downstream-readable certificate: declared periods, phase tuple, joint repeat horizon, shifted phase tuple, relative phase, theorem ids, and the non-claim boundary.

python scripts/multicoil_phase_feature_certify.py
python scripts/multicoil_phase_feature_certify.py --format json
python scripts/circle_ai_contract_ready.py --kind multicoil_phase_feature --digest --field joint_repeat_horizon --field relative_phase --include-recommendations

The digest adds PHASE-USE-JOINT-REPEAT-HORIZON and PHASE-AUDIT-RELATIVE-SHIFT-INVARIANT as copy-safe audit records. They are phase-bookkeeping records, not learned-embedding, attention-quality, extrapolation, or model-quality claims.

RoPE-Style Relative Phase Path

RoPE-style relative phase asks a related but different question: what phase feature is induced by the lag between a query position and a key position?

AIRA-B0003 is the current executable fixture for this idea. The widget below shows the correct-period relative feature, a wrong-period control, and the closure check after shifting query or key by a full period. It is not a standard RoPE benchmark or model-quality result.

RoPE Position-Distinguishability Certifier

The standalone RoPE contract asks a sharper engineering question: under a declared discretized phase-bank policy, do two positions collide in every channel, or does at least one channel distinguish them?

AIRA-T0024 is the main proof-carrying contract:

all-channel collision
iff
every declared period divides the position gap

AIRA-B0009 is the public certifier surface. It reports exact discrete pass/fail with theorem ids, then separately reports a numerical real-phase margin. The margin is useful, but it is not a Lean proof and not a context-length or model-quality claim.

Open the guided RoPE certifier lesson.

Winding-Aware Position Path

Residue-only phase answers where a position lands on the finite circle. It does not answer how many full passes have already happened. That matters for long-position bookkeeping: positions with the same residue can carry different labels, memories, or recurrence histories.

The proved facts AIRA-T0006 through AIRA-T0010 make the finite split explicit:

position = winding * period + residue

AIRA-B0006 is the executable fixture for this boundary. It compares residue-plus-winding features against residue-only, wrong-period winding, learned absolute-position, and scalar-threshold baselines. The nonperiodic control is deliberately scalar, so the ordinary threshold baseline wins there. This is not a RoPE improvement claim, a context-length claim, or a language-model result.

Looped Recurrence Path

Looped and recursive transformers reuse model blocks across multiple computation passes. The Circle Calculus version should make each pass explicit: loop phase, recurrence budget, state provenance, exit decision, and overthinking boundary. That is a possible interface contribution, not a proved model improvement.

Open the guided looped recurrence contracts lesson.

The dedicated lesson now carries the widgets and theorem-card shelf for:

loop budget timeline
exit certificate
token-level recurrence
training-free loop wrapper
learned phase tables
middle-block and multi-resolution routes
tiny recurrent-state prototype

The benchmark lane is P5-EDGE-010, seeded by AIM-B0003, AIM-B0011, AIM-B0005, AIM-B0012, AIM-B0006, AIM-B0007, AIM-B0013, AIM-B0008, AIM-B0014, AIM-B0009, and AIM-B0015. It should expand only with ordinary baselines and controls: dense transformer depth, Universal Transformer recurrence, fixed looped transformers, adaptive early-exit models, recurrent-memory transformers, token-level Mixture-of-Recursions, sparse/MoE looped models, RWKV/Mamba-style recurrent or state-space models, and nonrecursive transformer baselines. The proof boundary stays strict: Lean can certify finite schedule and indexing facts; Python or MLX benchmarks must carry model-quality, runtime, memory, and parameter claims.

Learning Path

Start with phase channels: finite indices, closure, and known-period examples.
Compare learned-feature baselines: cyclic features, dense scalar thresholds, learned absolute positions, and wrong-period controls.
Compare harmonic/Fourier features: correct sine/cosine phase features, wrong-frequency controls, and scalar controls.
Check backend parity: CPU references first, optional MLX only when available.
Add cyclic memory: slots, alias diagnostics, and nonperiodic controls.
Study coil retrieval: selected long-lag paths, local baselines, wrong-stride baselines, and full-attention oracle behavior.
Add content-gated retrieval: coil/local routing, wrong-gate controls, union/full-attention baselines, and candidate-budget accounting.
Add learned content-gate retrieval: phase-to-route lookup tables, route accuracy, wrong-period controls, flipped-gate controls, union/full-attention baselines, and candidate-budget accounting.
Add looped recurrence: loop phase, exit certificates, score traces, over-loop controls, and recursive transformer baselines.
Add token-level recurrence routing: per-token budgets, active-token counts, selected middle block, resolution labels, and wrong-loop controls.
Add learned token-level recurrence routing: phase-to-budget lookup tables, held-out token budgets, wrong-period controls, shifted-budget controls, over-loop controls, and scalar-threshold controls.
Add training-free loop wrappers: circular phase budgets, wrong-period controls, over-loop controls, scalar-threshold controls, and optional MLX scoring.
Add middle-block recurrence controls: selected-block schedules, full-block baselines, fixed budgets, wrong-block controls, over-loop controls, and block-pass accounting.
Add learned middle-block recurrence controls: phase-to-block lookup tables, phase-to-budget lookup tables, selected-band and full-block baselines, fixed budgets, wrong-period controls, wrong-block controls, over-loop controls, and block-pass accounting.
Add multi-resolution recurrence controls: coarse/fine phase routing, single-resolution baselines, fixed budgets, wrong-resolution controls, over-loop controls, and active-sample accounting.
Add learned multi-resolution recurrence controls: phase-to-budget lookup tables, phase-to-resolution lookup tables, single-resolution baselines, fixed budgets, wrong-period controls, over-loop controls, and active-sample accounting.
Add learned recurrence-schedule controls: phase-to-budget lookup tables, fixed-budget baselines, wrong-period controls, over-loop controls, and schedule accuracy.
Add tiny looped recurrent-state prototypes: certified budget state reads, state-to-label lookup, one-step controls, wrong-period controls, scalar controls, and nonperiodic controls.
Move to adapters, circulant mixers, and block-cyclic mixers: block sharing, circular-convolution parity, row/column residue cells, parameter accounting, alias diagnostics, and wrong-structure controls.
Add MultiCoil positions: combined periods, product-cycle/lcm closure, RoPE-style phase structure, and mismatch controls.
Compare RoPE-style relative phase: query/key lag labels, wrong-period controls, query-only controls, and scalar controls.
Add winding-aware positions: residue, winding, alias diagnostics, wrong-period controls, absolute-position controls, and scalar controls.
Only then compare learned model baselines and MLX prototypes, with quality, runtime, memory, parameter count, and interpretability reported separately.
Treat quaternion, spherical, Hopf/fiber, and S^7 ideas as later geometry-aware AI lessons, not as shortcuts around the lower-dimensional evidence.

What To Notice

Phase-channel proofs are about finite indices, not model quality.
AIA-B0003 is backend parity scaffolding, not a speed, quality, or acceleration claim.
AIA-B0004 is a learned-feature baseline scaffold, not a neural-network result or real-workload benchmark.
AIA-B0005 is a harmonic/Fourier-feature scaffold, not a standard RoPE or language-model benchmark.
Positive periodic fixtures must be paired with negative controls.
AIM-B0001 is a cyclic-memory benchmark harness, not a retrieval or attention theorem.
AIM-B0002 is a reachability harness over candidate index sets, not an attention-quality theorem.
AIM-B0004 is a gated-route reachability and budget harness, not a learned attention-quality theorem.
AIM-B0010 is learned route-table bookkeeping, not evidence about neural learned gates, retrieval quality, context length, runtime, or memory scaling.
AIM-B0016 is hybrid local+coil candidate-set reachability and budget bookkeeping, not evidence about sparse-attention quality, runtime, memory scaling, or long-context model behavior.
AIM-B0017 is finite stride-family candidate-set reachability and budget bookkeeping, not evidence about sparse-attention quality, multi-head attention quality, runtime, memory scaling, throughput, or long-context model behavior.
AIM-B0003 is a looped/recursive transformer schedule harness, not a recursive reasoning, context length, speed, memory, or model-quality result.
AIM-B0011 is loop-exit certificate bookkeeping, not evidence about adaptive-exit quality, reasoning, context length, speed, memory, or throughput.
AIM-B0005 is token-level recurrence routing bookkeeping, not evidence about learned routers, reasoning, perplexity, throughput, memory, or context length.
AIM-B0012 is learned token-level recurrence bookkeeping, not evidence about learned neural token routers, reasoning, perplexity, throughput, memory, or context length.
AIM-B0006 is training-free loop-wrapper bookkeeping, not evidence about learned recurrence, reasoning, language-model quality, throughput, memory, or context length.
AIM-B0007 is middle-block recurrence bookkeeping, not evidence about neural learned block routers, reasoning, perplexity, throughput, memory, or context length.
AIM-B0013 is learned middle-block recurrence bookkeeping, not evidence about neural block routers, reasoning, perplexity, throughput, memory, or context length.
AIM-B0008 is multi-resolution recurrence bookkeeping, not evidence about learned compressed/full-resolution routing, reasoning, perplexity, throughput, memory, or context length.
AIM-B0014 is learned multi-resolution recurrence bookkeeping, not evidence about neural compressed/full-resolution routing, reasoning, perplexity, throughput, memory, or context length.
AIM-B0009 is learned recurrence-schedule bookkeeping, not evidence about learned recursive transformer quality, reasoning, perplexity, throughput, memory, or context length.
AIM-B0015 is a tiny looped recurrent-state fixture, not evidence about learned recursive transformer quality, reasoning, perplexity, throughput, memory, or context length.
AIRA-B0001 is an adapter-block benchmark harness, not a CoilRA, RoPE, parameter-efficiency, or quality theorem.
AIRA-B0002 is a MultiCoil/RoPE-style positional harness, not a standard-RoPE comparison or language-model theorem.
AIRA-B0008 is two-period MultiCoil product-cycle closure bookkeeping, not evidence that the product horizon is minimal or useful for a learned positional encoding.
AIRA-B0003 is a RoPE-style relative phase harness, not an attention-quality, context-length, or language-model theorem.
AIRA-B0004 is parameter-count accounting, not evidence about quality, runtime, memory, training stability, or fine-tuning behavior.
AIRA-B0005 is circulant-mixer validation and parameter accounting, not evidence about neural-layer quality, runtime, memory, training stability, or hardware efficiency.
AIRA-B0006 is residue-plus-winding alias-control bookkeeping, not evidence about RoPE quality, context length, perplexity, runtime, or learned positional encodings.
AIRA-B0007 is block-cyclic dense-parity and alias-load bookkeeping, not evidence about neural-layer quality, parameter efficiency, runtime, memory, training stability, or hardware efficiency.
MLX/Mac-first experiments should be reported as benchmarks, not proofs.

Checkpoint

Why is the nonperiodic control in AIA-B0002 important before making any AI-improvement claim?

Source Trail

AI architecture paper: Circle AI Architectures

Memory paper: Coil Attention And Memory

Adapter paper: CoilRA And MultiCoil RoPE

Python and optional MLX benchmark fixtures are executable references only. They do not replace Lean proofs and do not prove that circles improve neural networks.