AI Contract Ladder Proof Audit

This appendix keeps the theorem-card trail for the AI Contract Ladder. The ladder page teaches the contract pattern; this page is for auditing the proof families.

Theorem cards summarize generated manifest data. The cards are not proof artifacts; the manifest entries and compiled Lean declarations remain the source of proof status.

How To Audit The Ladder

Use the same sequence as the lesson:

  1. RoPE exact phase-bank contract.
  2. RoPE real-phase finite-margin seeds.
  3. KV-cache ring-buffer freshness and sink-window policy.
  4. Sparse-attention coverage and gap witnesses.
  5. Looped recurrence schedules.
  6. Circulant mixer laws.

Each group below lists the theorem cards that were intentionally moved out of the guided lesson.

Exact RoPE Phase Banks

Real-Phase RoPE Seeds

The full RoPE audit page contains the focused current proof families. These cards are the extended historical trail from the ladder.

Focused RoPE audit: RoPE Proof Audit

KV-Cache Ring Buffer

Sparse-Attention Coverage

Looped Recurrence

Circulant Mixers

Source Trail

RoPE paper: Proof-Carrying RoPE Position Distinguishability

Attention and memory paper: Coil Attention And Memory

Architecture paper: Circle AI Architectures

Back: AI Contract Ladder Next: RoPE Certifier