Looped Recurrence Contracts

Looped and recursive transformer ideas reuse computation: the same block, or a selected band of blocks, runs more than once. Circle Calculus should not treat that as a vague metaphor. The useful contract is a finite schedule record:

sample or token
  -> loop phase
  -> recurrence budget
  -> active step set
  -> optional exit certificate
  -> optional block or resolution route
  -> explicit control cases

This page is a guided lesson for that record. It is not a claim that recurrence improves reasoning, perplexity, context length, speed, memory, or model quality.

Goal

Learn how Circle Calculus represents looped transformer work as finite recurrence-budget and routing contracts, then separate the theorem-backed schedule facts from the exploratory benchmark fixtures.

The widgets and Python fixtures on this page are executable references, not proofs. The theorem cards report finite schedule, index, closure, and route facts only. They do not certify semantic convergence, adaptive-exit quality, recursive reasoning, throughput, memory savings, or language-model performance.

What This Proves, And What It Does Not

Layer	Status	Reader Takeaway
Loop phase and recurrence budget	Lean-proved for the finite schedule fixtures	Required loop counts, whole-period shifts, and capped budgets are exact finite index facts.
Exit and active-token schedules	Lean-proved for modeled traces	Exit availability, no-exit controls, active-set counts, and work-accounting identities are theorem-linked schedule facts.
Periodic index reuse	Lean-proved for the declared shift witness	A whole-period token shift preserves the reported schedule fields in the finite model.
Planner recommendations	Theorem-backed finite records	The exported active-work and period-shift recommendations are reusable audit fixtures, not performance promises.
Recursive-transformer capability	Not proved here	The contract does not prove better reasoning, convergence, adaptive-halting quality, speed, memory savings, or model quality.

Why This Belongs In Circle Math

A looped model has a repeated action:

apply block again

That repeated action naturally has a phase:

loop step modulo loop period

The contract asks finite questions that can be checked before any model-quality experiment:

Is the required loop count bounded by the declared loop period?
Does the schedule repeat after a whole loop-period shift?
Which tokens are still active at each step?
Does a declared budget reach the first valid exit?
Does a selected middle-block route stay inside its block band?
Does a learned phase table have ordinary wrong-period and fixed-budget controls?

This is the right altitude for the current project. The proof layer can certify the finite bookkeeping. Benchmark fixtures can compare routing assumptions. Real model usefulness remains separate evidence.

Run the public recurrence certifier:

python scripts/recurrence_schedule_certify.py
python scripts/recurrence_schedule_certify.py --format json

1. Recurrence Budget Timeline

The first contract turns a sample or token index into a required loop count. In the current finite fixture, the required count is:

required_loops = sample mod loop_period + 1

That gives a positive budget, an upper bound by the loop period, and closure after whole loop-period shifts. The widget shows the schedule record, the capped training-free budget, exit availability, and overthinking guardrail boundary.

2. Exit Certificate

Adaptive recurrence needs an audit trail. The current loop-exit certificate records:

required step
score trace
first exit step
whether the exit is inside budget
whether the exit stays inside the guardrail boundary

The useful failure mode is visible too: a fixed budget can be insufficient, which produces a no-exit control. That is more honest than reporting only successful examples.

The score trace has its own formal contract. A step is active exactly when it lies between the required loop depth and the overthinking boundary. The first active trace step is the required loop depth, and a budgeted exit exists exactly when that first active step is inside maxLoops. The no-exit control is theorem-backed too: no exit is available exactly when every step inside the max-loop budget is outside the active score band.

3. Token-Level Recurrence

Token-level recurrence changes the question from “how many loops for the whole sample?” to “which tokens are still active at this loop step?”

token
  -> recurrence budget
  -> active or halted at step s
  -> selected middle-block range
  -> coarse/fine resolution label

The widget exposes active-token counts, resolution labels, selected middle-block bookkeeping, and fixed, wrong-budget, over-loop, and nonperiodic controls. AIM-T0111 and AIM-T0112 turn the schedule endpoints into list-level facts: step one activates the full token range, while any step beyond the loop period activates no tokens. AIM-T0113 and AIM-T0114 add the monotone-work contract: later active-token sets are subsets of earlier ones. AIM-T0115 and AIM-T0116 certify that the generated schedule has no duplicate token entries and never exceeds the declared token count.

The exported contract pack now also reports exact work-count fields. AIM-T0120 through AIM-T0125, plus AIM-T0128 and AIM-T0129, prove the active-token count is bounded, active work is nonincreasing, inactive work is nondecreasing, the first step has zero inactive tokens, the overrun step has zero active tokens, and active plus inactive tokens equals the declared token count. AIM-T0126 and AIM-T0127 pin the public loop_period=4, token_count=8, step=2 fixture to active count 6 and inactive count 2.

The same pack exposes a planner-facing whole-period shift witness: in the default fixture, base token 7 shifted by 3 * 5 loop-period slots lands at token 22, while required steps, recurrence budget, training-free wrapper budget, exit step, guardrail boundary, and active-at-step status remain unchanged. AIM-T0026 through AIM-T0030, AIM-T0033, AIM-T0034, and AIM-T0036 are the Lean-backed schedule facts behind those fields. This is an index-reuse contract; it does not say that a real looped transformer will reason better.

The v0.2 work-budget extension sums those per-step active-token counts over a finite horizon. AIM-T0130 proves that scheduled active-token work is bounded by the fixed-depth schedule that processes every token at every step. AIM-T0131 proves the saved-work accounting identity. AIM-T0144 proves that active token-work plus inactive token-work exactly recovers the full fixed-depth budget, and AIM-T0145 proves that scheduled work saving is exactly total inactive token-work. AIM-T0138 proves the planner-facing positive-saving iff: scheduled work saving is positive exactly when scheduled active-token work is strictly below full fixed-depth token-work. AIM-T0139 proves the complementary zero-saving iff: scheduled work saving is zero exactly when scheduled active-token work matches the full fixed-depth budget. AIM-T0132 through AIM-T0135, plus AIM-T0146, pin the public loop_period=4, token_count=8, steps=4 fixture to 20 active token-steps, 32 fixed-depth token-steps, and 12 inactive/saved token-steps. AIM-T0140 through AIM-T0143, plus AIM-T0147, pin the default exported recurrence contract fixture, loop_period=5, token_count=8, steps=5, to 21 active token-steps, 40 fixed-depth token-steps, and 19 inactive/saved token-steps with exact accounting. The public contract now exposes the stop schedule behind those totals: active-count trace [8,6,4,2,1], inactive-count trace [0,2,4,6,7], and a per-token first_inactive_steps table where each token stops at active_budget + 1. This is the scheduler-facing object a downstream project can consume before implementing recurrence reuse. AIM-T0150 through AIM-T0154 add the one-step post-period boundary: moving the default horizon from 5 to 6 adds no active-token work and raises scheduled-work saving from 19 to 27. AIM-T0155 through AIM-T0159 generalize that boundary to any declared number of extra steps after the loop period: active work stays fixed and inactive/saved work increases by extra_steps * token_count; the default horizon=8 fixture raises scheduled-work saving from 19 to 43. These are planner fields, not runtime measurements.

The generic AI contract pack now exposes those planner fields as two recommendation records. RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE packages the theorem-backed active-token work schedule, while RECURRENCE-REUSE-WHOLE-PERIOD-SHIFT packages the whole-period index-reuse witness. A downstream project can read them with:

python scripts/circle_ai_certify.py recurrence --period 6 --position 9 --horizon-steps 8 --sequence-length 24 --block-start 6 --block-width 6 --shift-amount 18
python scripts/circle_ai_contract_ready.py --kind recurrence_schedule --digest --field scheduled_work_saving --field post_period_multi_extension_scheduled_work_saving --include-recommendations

The first command uses looped-transformer aliases and emits the same canonical receipt fields as --loop-period, --sample-index, --max-loops, --token-count, --selected-block-start, --selected-block-width, and --shift-passes. --shift-amount must be a whole multiple of the period, so the whole-period index-reuse theorem remains the checked object.

The flagship acceptance policy pins both records, so consumers preserve the work-accounting fixture and the periodic index-reuse fixture together. They are finite schedule/index fixtures, not claims about runtime, memory savings, adaptive halting, or reasoning quality.

Strict recurrence downstream receipt command

For CI-style downstream use, require the strict receipt:

python scripts/circle_ai_contract_ready.py \
  --kind recurrence_schedule \
  --receipt \
  --format json \
  --field periodic_shift_required_steps_invariant \
  --field periodic_shift_active_at_step_invariant \
  --field total_active_token_work \
  --field scheduled_work_saving \
  --field scheduled_work_saving_accounting \
  --field active_inactive_work_accounting \
  --field scheduled_work_saving_positive \
  --field post_period_multi_extension_scheduled_work_saving \
  --require-theorem AIM-T0026 \
  --require-theorem AIM-T0130 \
  --require-theorem AIM-T0159 \
  --require-recommendation RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE \
  --require-recommendation RECURRENCE-REUSE-WHOLE-PERIOD-SHIFT \
  --require-recommendation-evidence-field RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=total_active_token_work \
  --require-recommendation-evidence-field RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=scheduled_work_saving \
  --require-recommendation-evidence-field RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=post_period_multi_extension_scheduled_work_saving \
  --require-recommendation-evidence-field RECURRENCE-REUSE-WHOLE-PERIOD-SHIFT=periodic_shift_required_steps_invariant \
  --require-recommendation-evidence-field RECURRENCE-REUSE-WHOLE-PERIOD-SHIFT=periodic_shift_active_at_step_invariant \
  --require-recommendation-theorem RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=AIM-T0130 \
  --require-recommendation-theorem RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=AIM-T0159 \
  --require-recommendation-theorem RECURRENCE-REUSE-WHOLE-PERIOD-SHIFT=AIM-T0026 \
  --require-recommendation-action-parameter RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=loop_period \
  --require-recommendation-action-parameter RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=scheduled_work_saving \
  --require-recommendation-action-parameter RECURRENCE-REUSE-WHOLE-PERIOD-SHIFT=base_token \
  --require-recommendation-action-parameter-path RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=loop_period \
  --require-recommendation-action-parameter-path RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=token_count \
  --require-recommendation-action-parameter-path RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=horizon_steps \
  --require-recommendation-action-parameter-path RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=scheduled_work_saving \
  --require-recommendation-action-parameter-path RECURRENCE-USE-ACTIVE-TOKEN-WORK-SCHEDULE=post_period_multi_extension_scheduled_work_saving \
  --require-recommendation-action-parameter-path RECURRENCE-REUSE-WHOLE-PERIOD-SHIFT=base_token \
  --require-recommendation-action-parameter-path RECURRENCE-REUSE-WHOLE-PERIOD-SHIFT=shifted_token \
  --require-recommendation-action-parameter-path RECURRENCE-REUSE-WHOLE-PERIOD-SHIFT=shift_amount

4. Training-Free Wrapper

A training-free wrapper uses phase as a fixed loop-budget prior. This is attractive because it can be tested without changing model weights, but the claim boundary has to stay strict: the fixture only checks schedule behavior and synthetic controls.

The widget compares the phase-derived budget against single-pass, fixed-loop, wrong-period, over-loop, and scalar-threshold controls.

5. Learned Phase Tables

The learned recurrence fixtures fit tiny lookup tables from phase to schedule choices. That makes the router auditable before any neural claim:

training examples
  -> phase-to-budget table
  -> held-out schedule prediction
  -> fixed, wrong-period, shifted, and over-loop controls

The widgets below are still small synthetic fixtures. Their purpose is to force controls and provenance into the workflow.

6. Middle-Block And Multi-Resolution Routes

Two useful recurrence variants are now represented as finite routing fixtures:

Middle-block recurrence: run only a selected band of blocks more than once.
Multi-resolution recurrence: alternate coarse and fine passes by phase.

The theorem cards for middle-block recurrence certify route bounds and closure for the selected block band and the combined block/budget route. The widgets show learned block and budget tables, wrong-block and wrong-period controls, single-resolution controls, and active-sample accounting.

7. Tiny Recurrent-State Prototype

The current prototype gives a finite hidden-state register to the loop:

sample
  -> certified recurrence budget
  -> finite state after that many loop passes
  -> state-to-label lookup
  -> one-step, wrong-period, scalar, and nonperiodic controls

The formal facts here are state-index facts: bounded state, sample-zero behavior, phase recovery when read at the certified budget, and closure after whole periods. They are not evidence that a recursive transformer learns better representations.

The full theorem-card trail for loop budgets, exits, token active sets, middle-block routes, and recurrent-state closure lives in the Looped Recurrence Proof Audit.

What To Notice

The loop phase is a finite address, not a model-quality guarantee.
Exit certificates expose no-exit and over-budget controls instead of hiding them.
Token-level recurrence has active-set accounting: the generated token list is checked against the active-at-step predicate, not just an average loop count.
Learned phase tables are useful only with wrong-period, fixed-budget, shifted-budget, and over-loop controls.
Middle-block and multi-resolution routes are finite routing contracts until real model baselines exist.
The next deep target should be stronger contract statements: iffs, coverage boundaries, or counterexample witnesses for recurrence schedules, not more names for the same bookkeeping.

Checkpoint

For a proposed recursive-transformer experiment, name the finite circular address space, the repeated action, one failure mode the certificate should expose, and one ordinary baseline that must be reported.

Source Trail

Run the deterministic sidecars from the repository root:

python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_loop_exit_certificate.py
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_token_level_recurrence.py
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_training_free_loop_wrapper.py
python sidecars/PAPER_AI_02_COIL_ATTENTION_AND_MEMORY/python/benchmark_middle_block_recurrence.py

Paper source: Coil Attention And Memory

Lean source: Circle/Applications/CircleAI.lean

Python source: circle_math/applications/circle_ai.py