Sparse Attention Proof Audit
This appendix keeps the theorem-card trail for the Sparse Attention Coverage lesson. The lesson teaches the coverage contract; this page is for auditing the finite proof family.
These cards certify finite candidate-set coverage, gap witnesses, count/budget fields, no-zero residue conditions, and dedup-loss facts for declared sparse plans. They do not prove attention quality, long-context model behavior, runtime, memory savings, or model quality.
Audit Reading Order
Use this page as an audit trail, not as the first explanation. The main lesson gives the worked example; this appendix resolves the theorem ids.
| Proof Family | What To Check Here |
|---|---|
| Basic reachability | local-window and stride-step predicates mean the same thing in Lean, Python, and the report fields |
| Candidate lists | generated lag/query lists have bounded size and expose the raw candidate budget |
| Covered and uncovered lists | every positive lag is either covered or uncovered, and the two lists account for n - 1 lags |
| Shortfalls and counts | raw-budget and deduplicated-count shortfalls are theorem-backed gap evidence under explicit hypotheses |
| Period thresholds | no-zero-residue and period-threshold checks make the structural assumptions visible |
| Planner rows | public rows certify collision counts, dedup loss, first-gap repair, first-interval repair, and dense fallback fields |
Basic Reachability And Gap Predicates
Candidate Lists And Budget Bounds
Covered And Uncovered List Semantics
Query Counts, Shortfalls, And Candidate Range
Period Thresholds And Zero-Residue Counts
Public Planner Rows And Dedup Loss
Source Trail
Paper source: Coil Attention And Memory
Lean source: Circle/Applications/CircleTransformer.lean
Python source: circle_math/applications/circle_transformer.py
CLI source: scripts/stride_family_certify.py
Quickstart: Sparse-Attention Certifier Quickstart