AI Contract Ladder

This lesson turns the AI application lane into a sequence of proof-carrying contracts. The point is not to claim that circular structure improves every model. The point is to learn how a real ML component can expose a finite circular boundary, attach theorem ids to that boundary, and keep performance claims separate from proof claims.

Goal

Read the Circle AI contracts in dependency order: exact phase banks, ring-buffer freshness, sparse-attention coverage, and circulant mixing. By the end, you should be able to name the circular address space, the repeated action, the Lean-backed statement, the executable sidecar, and the claim boundary for each contract.

Contract Pattern

Every usable contract in this lane has the same shape:

engineering object
  -> finite circular address space
  -> repeated action or stride
  -> theorem-backed boundary
  -> Python/browser certificate
  -> explicit non-claim

The non-claim matters. Theorem cards certify structural facts such as collision, coverage, freshness, equivariance, or exact budget accounting. They do not certify model quality, speed, memory savings, or production safety.

The browser widgets, Python CLIs, benchmarks, and fixtures on this page are executable references and not proofs. This page does not claim model-quality, speed, memory, or real-data usefulness results; theorem cards and Lean declarations remain the proof source of truth.

Ladder

Step	Component	Circular Object	What Gets Certified	Main Lesson
1	RoPE phase-bank certifier	residues modulo declared periods	exact discrete position collision and distinguishability	proof-carrying phase contracts
2	Real-phase RoPE seed	turn ratio below a finite context	theorem-backed one-channel finite margin examples	numerical diagnostics need proof-backed bounds
3	KV-cache ring buffer	token slots modulo cache size	slot collision, retained-window membership, trace-fresh batch slot distinctness, live-window duplicate freedom, sink-window request membership	freshness is residue plus time boundary plus explicit request policy
4	Sparse attention	local windows plus stride-family lag candidates	covered lags, gap witnesses, hit/gap list iffs, budget caps, no-duplicate candidate survival	sparse plans need hit and gap certificates, not just examples
5	Looped recurrence	loop phase and finite recurrence budgets	budget closure, exit certificates, active-token boundaries, route bounds	recursive-transformer ideas need schedule contracts before quality claims
6	Circulant mixers	cyclic shift on token indices	shift equivariance, convolution laws, linearity	structure can be guaranteed before benchmarking

Hands-On Sequence

Read and run the contracts in this order:

RoPE certifier: start with a position-distinguishability contract, where pass/fail is easiest to see.
KV-cache ring buffer: add the time boundary that distinguishes a live residue from a stale same-slot token, then add the sink-window policy that pins only the seen prefix before the rolling window.
Sparse-attention coverage: inspect a plan that intentionally has both covered lags and theorem-backed gap witnesses.

After those three, the cyclic-memory, multicoil phase-feature, recurrence, and mixer lessons should read as variations on the same pattern: identify the finite circular object, name the repeated action, expose a failure mode, and keep empirical model claims separate.

Run The Ladder

The fastest way to understand the lane is to run one certificate from each major family, then inspect the generated theorem ids and non-claims:

python scripts/rope_certify.py --preset llama_style_10000_4k
python scripts/kv_cache_certify.py --cache-size 16 --current 31 --token 20 --batch-tokens 20,24,29,31 --sink-size 4
python scripts/stride_family_certify.py --context 120 --strides 7,13 --path-length 3 --local-window 4
python scripts/recurrence_schedule_certify.py
python scripts/circulant_block_cyclic_mixer_certify.py
python scripts/circle_ai_contract_ready.py --action-plan --format json

Guided lessons: RoPE certifier, KV-cache ring buffer, sparse-attention coverage, looped recurrence contracts, and circulant/block-cyclic mixers.

1. Exact RoPE Phase Banks

The exact certifier models a declared phase bank as integer periods. Two positions collide in one channel exactly when the period divides their ordered gap, and they collide in the whole bank exactly when every declared period divides that same gap.

This is the cleanest contract because it gives both pass and fail evidence: a context either fits before the common collision gap, or the certifier can show sample colliding pairs.

This is exact for the declared integer-period phase-bank model. It is not a claim that real-valued RoPE channels have exact integer periods.

2. Real-Phase RoPE Seeds

Real RoPE moves from divisibility to distance from an integer turn. The current theorem program proves finite-margin certificates for named ratios and a bounded standard channel-0 seed. That is the important shift: the question becomes quantitative, and the proof has to account for every inspected positive gap.

The longest current proved standard seed is a one-channel statement for the standard channel-0 turn ratio:

turn ratio = 1 / (2*pi)
context    = 196608
margin     = 1 / 328459

The conditional bank bridge says that if a finite real-phase bank contains that channel and the inspected context and margin are within a seed, then the all-channel near-turn condition is ruled out under the stated tolerance scaling. The bracket theorems package the useful engineering reading: the sharp 1/104219 margin reaches 64k, and the lower 1/328459 margin reaches 192k.

The same lane also proves a useful ceiling. For any nontrivial finite context, Dirichlet-style approximation gives some inspected positive gap whose nearest-integer error is at most 1/context; therefore a requested margin strictly above that scale is impossible, and any exact weakest-gap report must also sit below that ceiling. That is a guardrail, not a positive margin proof.

Representative proof cards:

Full theorem audit: AI Contract Ladder Proof Audit and RoPE Proof Audit.

This is not a full real-RoPE bank theorem. It is a theorem-backed channel-0 seed plus a one-separating-channel conditional bank transfer. The remaining hard work is broader channel-wise certification or sharper Diophantine machinery.

3. KV-Cache Ring Buffer

A fixed-size KV cache writes token t to slot t mod cache_size. The slot residue alone cannot prove freshness, because stale and live tokens can share a slot across time. The useful contract is the retained-window boundary:

token is retained at current
iff
token <= current and current < token + cache_size

The generated live-window theorem then upgrades a Python-style list of live tokens into a theorem-backed object: membership in the list is equivalent to retention, the whole live window maps to duplicate-free slots, and a full live window has one in-range emitted entry per declared cache slot. The count and coverage iffs say the generated slot list reaches the full cache_size contract exactly when the live window is full. The read/write guard says that a retained token has no later same-slot writer before the current read point, the stale-witness theorem gives token + cache_size as the concrete later same-slot write for stale non-future tokens, the stale-trace iff says staleness is exactly the existence of a later same-slot writer up to current, the trace iff says those two sides exactly characterize freshness, and the batch trace theorem lifts the same check to a declared read batch. The request-level failure theorem now says a stale requested member blocks the modeled adapter pass bit; under non-future duplicate-free request assumptions, passing is exactly stale requested-member count zero and failing is exactly positive stale requested-member count.

4. Sparse-Attention Coverage

A strided sparse-attention path is a coil orbit on a finite context. The basic theorem says a stride reaches every position iff it is coprime to the context size. The useful engineering contract is stronger: for a local window plus a finite family of stride paths, the certifier should report covered lags, uncovered-lag witnesses, and candidate-budget boundaries.

This is why the sparse lane now emphasizes iffs and gap certificates. A sparse plan is more useful when it can tell you what it misses.

The sparse contract now has both sides of the story: the default C_120 fixture reports 109 uncovered positive lags, while the compact C_9 fixture with local window 2, path length 2, and strides (3,4,7) has an empty uncovered-lag list and preserves the raw lag/query candidate budget. The current partition theorem says the finite covered and uncovered lists account for all n - 1 positive lags, the covered-count theorem says complete coverage is exactly the case where the covered list itself has length n - 1, the uncovered-count witness theorem says a positive uncovered count is exactly the existence of an actual uncovered positive lag, and the covered-count shortfall theorem says falling below n - 1 is exactly the same gap-witness condition.

Open the guided sparse-attention coverage lesson. For the narrower candidate-budget slice, continue with the strided candidate fanout lesson.

5. Looped Recurrence

Looped and recursive transformer proposals are easy to overstate because “more computation” can sound like “more reasoning.” The contract form keeps the finite part separate: loop budgets, exit certificates, active-token boundaries, selected-block routes, and wrong-period controls.

Open the guided looped recurrence contracts lesson.

6. Circulant Mixers

A circulant mixer is not a proof that a model will perform well. It is a structure with a guarantee: cyclic shifts commute with the mixer, and the convolution laws are fixed before training. That makes it a good negative-control example for the whole AI lane: the proof can certify equivariance, while benchmarks decide whether that bias fits the data.

Open the focused circulant and block-cyclic mixer lesson.

Full theorem-card trail for this ladder: AI Contract Ladder Proof Audit.

How To Use This Ladder

For a new AI component, fill in this checklist before writing a theorem or benchmark:

What is the finite circular address space?
What operation repeats, wraps, rotates, or strides?
What exact failure mode should the contract expose?
Which statement needs an iff, counterexample witness, count, or quantitative bound?
What Python/browser certificate would a non-Lean engineer run?
Which claim is deliberately outside the theorem?

If the answer is only “this has a circle metaphor,” it is not ready. If the answer produces a pass/fail certificate, a gap witness, a collision count, or a margin bound, it belongs in this lane.

Source Trail

RoPE paper: Proof-Carrying RoPE Position Distinguishability

Attention and memory paper: Coil Attention And Memory

Architecture paper: Circle AI Architectures