AI Contract Suite

This lesson is the working front door for the Circle Calculus AI contracts. The goal is not to claim better models. The goal is to make finite AI infrastructure questions checkable before they become vague architecture claims.

Goal

Use the four flagship contracts as a guided suite: RoPE position distinguishability, KV-cache ring-buffer freshness plus sink-window policy, sparse-attention coverage, and looped recurrence schedule accounting. For each one, identify the circular address space, run or export the certificate, read the theorem ids, and state what the certificate does not prove.

Concept

The common object is a finite cyclic boundary inside an AI system:

RoPE position      -> residue in a declared phase period
KV-cache token     -> slot modulo cache size plus time boundary
sparse dependency  -> lag reached by local window or stride family
recurrence schedule -> loop step and active-token work count

Circle Calculus is useful here when it turns the boundary into a proof-carrying contract:

finite address space
  -> repeated action
  -> theorem-backed pass/fail or count field
  -> Python report
  -> claim boundary

Picture

ML component
   |
   v
finite circular model
   |
   v
Lean theorem ids -----> theorem manifest
   |
   v
Python certificate --> text / JSON report
   |
   v
Living Book lesson --> what this proves / does not prove

The diagram is explanatory only. The theorem ids and Lean declarations are the proof layer.

The certifiers on this page prove finite structural facts only. They do not prove model quality, speed, memory savings, context-length improvement, reasoning ability, deployment safety, or implementation correctness.

One Contract Reading Loop

Use the same loop for every contract on this page:

  1. name the finite circular object;
  2. run the CLI or open the generated JSON record;
  3. inspect the main evidence fields;
  4. check the cited theorem ids and proof status;
  5. read the explicit non-claims before treating the result as useful.

A PASS, FAIL, GAPS, or READY label is only the report summary. The reusable artifact is the theorem-linked evidence plus its boundary.

Reading Path

Use this page as the guided entrance to the contract lane, then open the focused lesson for the component you care about:

Step Lesson What To Learn First Command
1 Circle phase probe demo why circle phase features can expose a synthetic periodic rule python scripts/circle_phase_probe_demo.py --backend numpy
2 ML engineer quickstart how to run the four flagship receipts without reading Lean first python scripts/circle_ai_certify.py rope --head-dim 128 --base 10000 --context 131072 --requested-margin 1/328459
3 RoPE certifier how a rotary phase bank becomes a position-distinguishability contract python scripts/circle_ai_contract_ready.py --kind rope_position_distinguishability
4 KV-cache ring buffer how residue plus overwrite boundary gives freshness and stale-read certificates python scripts/circle_ai_contract_ready.py --kind kv_cache_ring_buffer
5 Sparse attention coverage how local windows and stride families expose covered lags, gaps, and repair targets python scripts/circle_ai_contract_ready.py --kind sparse_attention_coverage
6 Looped recurrence contracts how recurrence schedules expose finite work, exit, and index-reuse contracts python scripts/circle_ai_contract_ready.py --kind recurrence_schedule
7 AI contract runner how to run the same contract shape on your own parameters and get a text/JSON receipt python scripts/circle_ai_certify.py rope --head-dim 128 --base 10000 --context 131072 --requested-margin 1/328459
8 AI contract pack audit how another project consumes the public JSON pack without reading Lean files python scripts/circle_ai_contract_ready.py --fingerprints

Each focused lesson follows the same reading shape: concept, finite circular object, worked example, theorem ids, executable certificate, and exact non-claims. Use the audit pages only when you want the full theorem-card trail.

Contract Anatomy

Read the flagship contracts as four worked examples of the same method:

Contract Concept Picture To Keep In Mind First Example Theorem / Certificate What It Does Not Prove
RoPE position distinguishability positions become phases in a finite declared bank clock hands that should not all return to the same phase inside the context python scripts/rope_certify.py --preset llama_style_10000_4k integer-bank collision theorems plus D19 real-phase margin fields language-model quality, useful context length, or all-channel standard-RoPE separation
KV-cache ring buffer a token has a slot residue and a freshness time boundary a circular cache with old writes overwritten by later tokens in the same slot python scripts/kv_cache_certify.py --cache-size 16 --current 31 --token 20 --batch-tokens 20,24,29,31 --sink-size 4 retained-window, stale-member, and sink-window request certificates paging performance, memory savings, retrieval quality, or implementation correctness
Sparse-attention coverage local windows and stride coils cover some positive lags and miss others a finite context with highlighted reached lags and explicit gaps python scripts/stride_family_certify.py --context 120 --strides 7,13 --path-length 3 --local-window 4 covered/uncovered partitions, gap witnesses, repair windows, and budget fields attention quality, runtime speed, or optimal sparse layout design
Looped recurrence schedules repeated passes have loop phase, active work, exit, and shift invariants a cyclic schedule where active tokens shrink and whole-period shifts reuse the same pattern python scripts/recurrence_schedule_certify.py active/inactive work accounting, exit boundaries, post-period extension, and shift invariants reasoning ability, training benefit, or recursive-transformer model quality

That table is the textbook view. The JSON pack and audit pages are the machine view of the same material.

First 10 Minutes

Start with the contract pack before reading individual theorem trails:

make circle-ai-contracts-ready
python scripts/circle_ai_contract_ready.py
python scripts/circle_ai_contract_ready.py --kind rope_position_distinguishability
python scripts/circle_ai_contract_ready.py --kind sparse_attention_coverage --digest --field first_uncovered_lag --include-recommendations

The no-argument readiness command is the table of contents for the public contract pack. It should say that all nine exported contract families are ready before you drill into a single one:

circle AI contract readiness summary ok: contracts=9 ready=9 not_ready=0 ...
kind=rope_position_distinguishability ... ready=True ... proof_proved=True ...
kind=kv_cache_ring_buffer ... ready=True ... proof_proved=True ...
kind=sparse_attention_coverage ... ready=True ... proof_proved=True ...

Read each readiness line in this order:

Field Meaning Stop If
ready=True the selected contract has its required fields and proof-status metadata ready=False
proof_proved=True every theorem id used by the contract resolves to a proved manifest entry unproved > 0
missing_fields=0 the downstream evidence fields are present in the generated pack missing_fields > 0
planner_recommendations copy-safe finite audit or repair actions attached to theorem ids a recommendation lacks theorem ids or non-claims

Then open one focused lesson. For example, read the RoPE certifier page to see how the finite phase-bank idea turns into a theorem-backed JSON receipt, or read the sparse-attention coverage page to see how covered lags, uncovered intervals, and repair windows are separated.

The suite-level machine-readable artifact is the generic Circle pack:

make circle-ai-contracts
make circle-ai-contracts-check
make circle-ai-contracts-ready
python scripts/circle_ai_contract_ready.py --kind sparse_attention_coverage

It writes site/data/generated/circle_ai_contract_pack.json with schema circle_calculus.ai_contract_pack.v0. The pack includes explicit records for the four contracts on this page plus broader integration fixtures for strided fanout, cyclic memory, multicoil phase features, structured mixers, and seed-rule regeneration with finite storage accounting for the public C_128 fixture. The older Theseus-Hive JSON export is a compatibility view for one downstream private lane, not the public center of this contract suite.

The first downstream gate is machine-readable:

contract_schema.required_contract_keys
contract_schema.minimum_fields_by_kind
contract_readiness_index.<kind>.ready_for_downstream_fixture_use
contract_readiness_index.<kind>.all_theorem_ids_proved
contract_readiness_index.<kind>.planner_recommendation_count
contract_readiness_index.<kind>.planner_recommendation_ids
contract_fingerprint_index.<kind>.content_fingerprint
contract.consumer_check.ready_for_downstream_fixture_use
contract.proof_status.all_theorem_ids_proved

If either readiness field is false, the consumer should reject the fixture before adding private metrics or benchmark rows. The readiness index is the quick path for external tools; the fingerprint index is the stable audit-log surface; the full contract record is the detailed evidence trail.

Run Your Own Config

Use the unified runner when you want a receipt for parameters that are not one of the public fixture rows:

python scripts/circle_ai_certify.py rope \
  --head-dim 128 \
  --base 10000 \
  --context 131072 \
  --requested-margin 1/328459 \
  --format json

The receipt schema is circle_calculus.ai_contract_receipt.v0. Its core fields are decision, normalized_request, evidence, proof_status, proof_layers, support, and not_claimed. Read the AI Contract Runner lesson before wiring the JSON into another project.

For CI, add gates directly to the runner:

python scripts/circle_ai_certify.py rope \
  --head-dim 128 \
  --base 10000 \
  --context 131072 \
  --requested-margin 1/328459 \
  --gate-report-out reports/rope_gate.json \
  --require-status proved \
  --require-decision passed \
  --require-assurance mixed_theorem_and_computation \
  --require-passed

--gate-report-out writes the schema-validated pass/fail report for the in-memory receipt. Use --json-out plus --receipt-check-out when an audit log should also retain the full receipt JSON. Use --certification-bundle-out plus --certification-bundle-check-out when the audit log should retain the full request preflight, theorem-linked receipt, gate report, model-config provenance when present, and a CI-readable verification report for the bundle. For model-config imports, pass the model_config_fingerprint from the import report to --require-model-config-fingerprint in the certification-bundle checker, artifact-manifest checker, or standalone downstream verifier when CI must pin the source config.json. Those handoff checkers can also require embedded receipt theorem ids, evidence fields, recommendation ids, validation commands, and normalized request parameters, so downstream CI can fail on missing dependencies without parsing the receipt by hand.

python scripts/circle_ai_certify.py rope \
  --model-config examples/circle_ai_model_configs/standard_rope_config.json \
  --requested-margin 1/328459 \
  --artifact-dir reports/rope_contract \
  --require-status proved \
  --require-decision passed \
  --require-assurance mixed_theorem_and_computation \
  --require-passed

--artifact-dir writes the request, request-validation report, model-config import report when present, receipt, receipt-check report, gate report, certification bundle, bundle-check report, artifact manifest, and artifact-manifest-check report with stable names. scripts/check_circle_ai_artifact_manifest.py can re-run that manifest check after handoff by re-hashing each referenced file.

make circle-ai-contracts-check validates the generated JSON artifact itself: schema id, required contract keys, minimum fields, theorem ids, proof-status metadata, dictionary ids, source paths, quickstart docs, Living Book pages, and Python entrypoint paths.

Audit CLI And Consumer Adapter Details

For a single contract kind, the consumer CLI performs the pack validation first, then exits 0 only when the requested kind is ready:

make circle-ai-contracts-ready
python scripts/circle_ai_contract_ready.py
python scripts/circle_ai_contract_ready.py --kind sparse_attention_coverage
python scripts/circle_ai_contract_ready.py --kind sparse_attention_coverage --format json
python scripts/circle_ai_contract_ready.py --list-kinds
python scripts/circle_ai_contract_ready.py --list-recommendations
python scripts/circle_ai_contract_ready.py --fingerprints
python scripts/circle_ai_contract_ready.py --acceptance-policy
python scripts/circle_ai_contract_ready.py --acceptance-policy --format json
python scripts/circle_ai_contract_ready.py --action-plan
python scripts/circle_ai_contract_ready.py --action-plan --recommendation ROPE-USE-D19-MARGIN-FRONTIER --format json
python scripts/circle_ai_contract_ready.py --kind seed_rule_exact_regeneration --action-plan --include-values --format json
python scripts/circle_ai_contract_ready.py --kind rope_position_distinguishability --digest --format json --field d19_proved_request_status --field d19_impossible_request_status --field d19_undecided_request_status --field d19_proved_first_channel_bank_transfer --field d19_proved_first_channel_bank_shape --field d19_proved_first_channel_pair_scope --field d19_proved_first_channel_context_wide_contract --field d19_proved_first_channel_radian_bank_form --field d19_proved_first_channel_bank_tolerance_rule --field d19_impossible_obstruction_gap --field d19_impossible_obstruction_turns --field d19_undecided_probe_margin_in_open_gap --field real_phase_nearest_integer_certificate_bridge --field real_phase_dirichlet_witness_guardrail --field real_phase_margin_ceiling_guardrail --field real_phase_exact_weakest_margin_ceiling_guardrail --include-recommendations
python scripts/circle_ai_contract_ready.py --kind rope_position_distinguishability --receipt --format json --field d19_proved_request_status --field d19_impossible_request_status --field d19_undecided_request_status --field d19_proved_first_channel_bank_transfer --field d19_proved_first_channel_bank_shape --field d19_proved_first_channel_pair_scope --field d19_proved_first_channel_context_wide_contract --field d19_proved_first_channel_radian_bank_form --field d19_proved_first_channel_bank_tolerance_rule --field d19_impossible_obstruction_gap --field d19_impossible_obstruction_turns --field d19_undecided_probe_margin_in_open_gap --field real_phase_nearest_integer_certificate_bridge --field real_phase_dirichlet_witness_guardrail --field real_phase_margin_ceiling_guardrail --field real_phase_exact_weakest_margin_ceiling_guardrail --require-theorem AIRA-T0058 --require-theorem AIRA-T0059 --require-theorem AIRA-T0171 --require-theorem AIRA-T0172 --require-theorem AIRA-T0177 --require-theorem AIRA-T0178 --require-theorem AIRA-T0182 --require-theorem AIRA-T0183 --require-theorem AIRA-T0234 --require-theorem AIRA-T0235 --require-theorem AIRA-T0236 --require-theorem AIRA-T0237 --require-theorem AIRA-T0238 --require-theorem AIRA-T0239 --require-theorem AIRA-T0240 --require-theorem AIRA-T0241 --require-recommendation ROPE-USE-D19-MARGIN-FRONTIER --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_proved_first_channel_bank_transfer --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_proved_first_channel_context_wide_contract --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_proved_first_channel_radian_bank_form --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_undecided_probe_margin_in_open_gap --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_impossible_obstruction_gap --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_impossible_obstruction_turns --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=real_phase_nearest_integer_certificate_bridge --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=real_phase_dirichlet_witness_guardrail --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=real_phase_margin_ceiling_guardrail --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=real_phase_exact_weakest_margin_ceiling_guardrail --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0234 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0235 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0236 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0237 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0238 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0058 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0059 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0177 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0178 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0182 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0183 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0239 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0240 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0241 --require-recommendation-action-parameter ROPE-USE-D19-MARGIN-FRONTIER=proved_branch_bank_transfer --require-recommendation-action-parameter ROPE-USE-D19-MARGIN-FRONTIER=impossible_obstruction_gap --require-recommendation-action-parameter ROPE-USE-D19-MARGIN-FRONTIER=impossible_obstruction_turns --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=impossible_obstruction_gap --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=impossible_obstruction_turns --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=proved_branch_bank_transfer.applies --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=proved_branch_bank_transfer.context_wide_contract --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=proved_branch_bank_transfer.radian_bank_form --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=proved_branch_bank_transfer.theorem_ids
python scripts/circle_ai_contract_ready.py --kind kv_cache_ring_buffer --digest --field stale_probe_first_stale_token --include-recommendations
python scripts/circle_ai_contract_ready.py --kind sparse_attention_coverage --digest --field first_uncovered_lag --include-recommendations
python scripts/circle_ai_contract_ready.py \
  --kind sparse_attention_coverage \
  --receipt \
  --format json \
  --field first_uncovered_lag \
  --field first_uncovered_interval_start \
  --field complete_repair_window \
  --field complete_repair_window_covers_context \
  --field complete_repair_window_minimal_for_declared_stride_family \
  --field complete_repair_window_minimal_witness_lag \
  --require-theorem AIT-T0104 \
  --require-theorem AIT-T0172 \
  --require-recommendation SPARSE-LOCAL-FIRST-INTERVAL-REPAIR \
  --require-recommendation SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK \
  --require-recommendation-evidence-field SPARSE-LOCAL-FIRST-INTERVAL-REPAIR=first_uncovered_interval_start \
  --require-recommendation-evidence-field SPARSE-LOCAL-FIRST-INTERVAL-REPAIR=first_uncovered_interval_stop \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=complete_repair_window \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=complete_repair_window_covers_context \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=complete_repair_window_uses_dense_threshold \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=local_window_complete_threshold_is_exact_local_minimum \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=complete_repair_window_minimal_for_declared_stride_family \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=complete_repair_window_minimal_witness_lag \
  --require-recommendation-theorem SPARSE-LOCAL-FIRST-INTERVAL-REPAIR=AIT-T0104 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0023 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0034 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0172 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0168 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0169 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0170 \
  --require-recommendation-action-parameter SPARSE-LOCAL-FIRST-INTERVAL-REPAIR=proposed_local_window \
  --require-recommendation-action-parameter SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=proposed_local_window \
  --require-recommendation-action-parameter SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=additional_local_slots \
  --require-recommendation-action-parameter-path SPARSE-LOCAL-FIRST-INTERVAL-REPAIR=proposed_local_window \
  --require-recommendation-action-parameter-path SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=proposed_local_window \
  --require-recommendation-action-parameter-path SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=additional_local_slots
python scripts/check_circle_ai_contract_acceptance_policy.py --format json
python scripts/circle_ai_contract_ready.py --print-refreshed-policy
python scripts/circle_ai_contract_ready.py --acceptance-policy-report --format json
python scripts/circle_ai_contract_ready.py --kind strided_candidate_fanout --digest --field full_coverage --field effective_candidate_budget --field duplicate_count --include-recommendations
python scripts/circle_ai_contract_ready.py --kind cyclic_memory_residue_winding --digest --field max_alias_load --include-recommendations
python scripts/circle_ai_contract_ready.py --kind multicoil_phase_feature --digest --field joint_repeat_horizon --field relative_phase --include-recommendations
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
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
python scripts/circle_ai_contract_ready.py --kind seed_rule_exact_regeneration --digest --field storage_saving --include-recommendations

A ready line should have this shape:

ready=True proof_resolved=True proof_proved=True missing_fields=0 unresolved=0 unproved=0

For audit logs, record this shape too:

python scripts/circle_ai_contract_ready.py --fingerprints

That prints the deterministic sha256-json-v1 pack fingerprint and one content fingerprint per contract kind. The fingerprints identify the exported contract record; they are reproducibility metadata, not mathematical proofs. Use --expect-pack-fingerprint <sha256> and --expect-contract-fingerprint kind=<sha256> in downstream CI when a project should fail if the exported pack or one selected contract record changed.

For Python projects, the same gate is available as an importable adapter:

from circle_math.applications.circle_ai_contract_consumer import (
    contract_acceptance_receipt,
    contract_acceptance_policy_report,
    contract_digest,
    contract_recommendations,
    contract_fingerprint_summary,
    load_contract_pack,
    planner_action_plan,
    require_fingerprint_expectations,
    require_ready_contract,
)

pack = load_contract_pack("site/data/generated/circle_ai_contract_pack.json")
fingerprints = contract_fingerprint_summary(pack)
require_fingerprint_expectations(
    pack,
    expected_pack_fingerprint=fingerprints["pack_content_fingerprint"],
    expected_contract_fingerprints={
        "kv_cache_ring_buffer": fingerprints["contract_fingerprint_index"][
            "kv_cache_ring_buffer"
        ]["content_fingerprint"],
    },
)
contract = require_ready_contract(pack, "kv_cache_ring_buffer")
digest = contract_digest(pack, "kv_cache_ring_buffer")

assert digest["ready_for_downstream_fixture_use"] is True
assert digest["missing_requested_fields"] == []
assert digest["evidence_fields"]["stale_requested_count"] == 0
receipt = contract_acceptance_receipt(
    pack,
    "kv_cache_ring_buffer",
    required_fields=("adapter_request_pass", "stale_requested_count"),
    required_theorem_ids=("AIM-T0103",),
    required_recommendation_ids=("KV-DROP-STALE-REQUEST-TOKEN",),
    required_recommendation_evidence_fields={
        "KV-DROP-STALE-REQUEST-TOKEN": (
            "stale_probe_first_stale_token",
            "stale_probe_stale_requested_count",
        ),
    },
    required_recommendation_theorem_ids={
        "KV-DROP-STALE-REQUEST-TOKEN": ("AIM-T0103",),
    },
    required_recommendation_action_parameters={
        "KV-DROP-STALE-REQUEST-TOKEN": (
            "target_token",
            "next_same_slot_overwrite_token",
        ),
    },
    required_recommendation_action_parameter_paths={
        "KV-DROP-STALE-REQUEST-TOKEN": ("target_token",),
    },
)
assert receipt["accepted"] is True
assert contract_recommendations(pack, "sparse_attention_coverage")
policy_report = contract_acceptance_policy_report(
    pack,
    {
        "schema_id": "circle_calculus.ai_contract_acceptance_policy.v0",
        "policy_id": "kv_policy",
        "expected_pack_fingerprint": fingerprints["pack_content_fingerprint"],
        "contracts": [
            {
                "kind": "kv_cache_ring_buffer",
                "expected_contract_fingerprint": fingerprints[
                    "contract_fingerprint_index"
                ]["kv_cache_ring_buffer"]["content_fingerprint"],
                "required_fields": [
                    "stale_probe_first_stale_token",
                    "sink_tokens_retained_by_policy",
                ],
                "required_recommendation_ids": [
                    "KV-DROP-STALE-REQUEST-TOKEN",
                ],
                "required_recommendation_evidence_fields": {
                    "KV-DROP-STALE-REQUEST-TOKEN": [
                        "stale_probe_first_stale_token",
                        "stale_probe_stale_requested_count",
                    ],
                },
            },
        ],
    },
)
assert policy_report["accepted"] is True
planner = planner_action_plan(pack, ["sparse_attention_coverage"], include_values=True)
assert planner["action_plan"][0]["action_parameters"]["proposed_local_window"] == 6
assert planner["action_plan"][0]["validation_commands"]
single_action = planner_action_plan(
    pack,
    ["sparse_attention_coverage"],
    recommendation_ids=["SPARSE-LOCAL-FIRST-INTERVAL-REPAIR"],
    include_values=True,
)
assert single_action["planner_recommendation_count"] == 1
print(contract["id"], digest["theorem_ids"])

This adapter checks the public JSON invariants needed by a downstream project: schema id, readiness-index consistency, minimum evidence fields, proof-status flags, and the non-claim boundary. planner_action_plan is the data-first surface for repair and audit actions; each action also carries validation commands so an external project can rerun the relevant checks before consuming the recommendation. The shell examples below are a copyable way to inspect the same information. It does not replace Circle’s repository-side Lean, manifest, dictionary, or Living Book checks.

The direct --action-plan CLI is the same idea for non-Python consumers. It turns planner recommendations into a theorem-linked action list, and --include-values resolves evidence fields into concrete certificate values. For the seed-rule fixture, this exposes the exact-regeneration recipe and the bounded shorter-candidate selection with stable candidate ids. Use --recommendation RECOMMENDATION_ID when a downstream planner needs one named action; missing recommendation ids fail instead of being silently ignored.

The --digest form is the smallest copy-safe surface for another AI project: it emits the contract id, theorem ids, selected evidence fields, source trails, and the non-claim boundary without asking that project to know Circle’s manifests or Lean file layout. The first-party --receipt form is stricter: it rejects the selected contract if a requested evidence field, required theorem id, required planner recommendation id, required recommendation evidence field, or required recommendation theorem id is missing. Use --require-recommendation-action-parameter RECOMMENDATION_ID=parameter_key when a direct receipt must pin a value-mode planner payload key; policy gates can enforce the same action-parameter pins. Use --require-recommendation-action-parameter-path RECOMMENDATION_ID=classifier_regions[region=proved].theorem_ids when the consumer depends on a nested path inside a structured planner payload. Successful receipts emit the pack fingerprint, contract fingerprint, theorem ids, source trails, validation commands, and non-claim boundary. The multi-contract policy gate is stricter again: it reads examples/circle_ai_contract_acceptance_policy.json, pins the pack fingerprint and selected contract fingerprints, requires the action evidence and theorem trails used by downstream recommendations, then emits one report containing strict receipts for the four flagship contracts. Before it prints success, the checker validates that report and every receipt against the generated report and receipt schema sidecars named by the pack. The same receipt bundle can be emitted through the main CLI with python scripts/circle_ai_contract_ready.py --acceptance-policy-report --format json. The generated pack advertises this route directly under acceptance_policy: that block names the default policy path, checker scripts, report schema id circle_calculus.ai_contract_acceptance_policy_report.v0, receipt schema id circle_calculus.ai_contract_acceptance_receipt.v0, rejection report schema id circle_calculus.downstream_ci_rejection_report.v0, policy schema path site/data/generated/circle_ai_contract_acceptance_policy.schema.json, report schema path site/data/generated/circle_ai_contract_acceptance_policy_report.schema.json, receipt schema path site/data/generated/circle_ai_contract_acceptance_receipt.schema.json, rejection report schema path site/data/generated/circle_ai_downstream_rejection_report.schema.json, fingerprint refresh command, and the pinned requirement keys a downstream project should preserve when locking a receipt. Use python scripts/circle_ai_contract_ready.py --print-refreshed-policy only when the requirements are intentionally unchanged and the generated pack fingerprints need to be refreshed; it preserves field pins, theorem pins, recommendation pins, action-parameter pins, and nested action-parameter path pins. When --include-recommendations is passed, the digest also includes optional copy-safe repair/audit actions such as the sparse first-interval repair target and largest-gap repair target and dense-local fallback, the KV stale-token/sink-window actions, or the RoPE exact integer-bank audit and D19 margin-frontier actions, or the strided-fanout full-coverage and duplicate-budget audits, or the cyclic-memory winding/provenance and alias-load records. Phase-feature recommendations expose joint-repeat and relative-shift records. Mixer recommendations expose dense-parity and block-cyclic parameter-budget records. Recurrence recommendations expose active-work and whole-period index-reuse records. Seed-rule recommendations expose an exact-regeneration recipe and a bounded finite-search shorter-candidate selection.

For a copyable downstream-consumer pattern, run:

python scripts/example_consume_circle_ai_contract_pack.py --kind rope_position_distinguishability --field d19_proved_request_status --field d19_impossible_request_status --field d19_undecided_request_status --field d19_proved_first_channel_bank_transfer --field d19_proved_first_channel_bank_shape --field d19_proved_first_channel_pair_scope --field d19_proved_first_channel_context_wide_contract --field d19_proved_first_channel_radian_bank_form --field d19_proved_first_channel_bank_tolerance_rule --field d19_impossible_obstruction_gap --field d19_impossible_obstruction_turns --field d19_undecided_probe_margin_in_open_gap --field real_phase_nearest_integer_certificate_bridge --field real_phase_dirichlet_witness_guardrail --field real_phase_margin_ceiling_guardrail --field real_phase_exact_weakest_margin_ceiling_guardrail --include-recommendations
python scripts/example_consume_circle_ai_contract_pack.py --kind rope_position_distinguishability --receipt --field d19_proved_request_status --field d19_impossible_request_status --field d19_undecided_request_status --field d19_proved_first_channel_bank_transfer --field d19_proved_first_channel_bank_shape --field d19_proved_first_channel_pair_scope --field d19_proved_first_channel_context_wide_contract --field d19_proved_first_channel_radian_bank_form --field d19_proved_first_channel_bank_tolerance_rule --field d19_impossible_obstruction_gap --field d19_impossible_obstruction_turns --field d19_undecided_probe_margin_in_open_gap --field real_phase_nearest_integer_certificate_bridge --field real_phase_dirichlet_witness_guardrail --field real_phase_margin_ceiling_guardrail --field real_phase_exact_weakest_margin_ceiling_guardrail --require-theorem AIRA-T0058 --require-theorem AIRA-T0059 --require-theorem AIRA-T0171 --require-theorem AIRA-T0172 --require-theorem AIRA-T0177 --require-theorem AIRA-T0178 --require-theorem AIRA-T0182 --require-theorem AIRA-T0183 --require-theorem AIRA-T0234 --require-theorem AIRA-T0235 --require-theorem AIRA-T0236 --require-theorem AIRA-T0237 --require-theorem AIRA-T0238 --require-theorem AIRA-T0239 --require-theorem AIRA-T0240 --require-theorem AIRA-T0241 --require-recommendation ROPE-USE-D19-MARGIN-FRONTIER --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_proved_first_channel_bank_transfer --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_proved_first_channel_context_wide_contract --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_proved_first_channel_radian_bank_form --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_undecided_probe_margin_in_open_gap --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_impossible_obstruction_gap --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=d19_impossible_obstruction_turns --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=real_phase_nearest_integer_certificate_bridge --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=real_phase_dirichlet_witness_guardrail --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=real_phase_margin_ceiling_guardrail --require-recommendation-evidence-field ROPE-USE-D19-MARGIN-FRONTIER=real_phase_exact_weakest_margin_ceiling_guardrail --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0234 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0235 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0236 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0237 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0238 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0058 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0059 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0177 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0178 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0182 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0183 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0239 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0240 --require-recommendation-theorem ROPE-USE-D19-MARGIN-FRONTIER=AIRA-T0241 --require-recommendation-action-parameter ROPE-USE-D19-MARGIN-FRONTIER=proved_branch_bank_transfer --require-recommendation-action-parameter ROPE-USE-D19-MARGIN-FRONTIER=impossible_obstruction_gap --require-recommendation-action-parameter ROPE-USE-D19-MARGIN-FRONTIER=impossible_obstruction_turns --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=impossible_obstruction_gap --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=impossible_obstruction_turns --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=proved_branch_bank_transfer.applies --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=proved_branch_bank_transfer.context_wide_contract --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=proved_branch_bank_transfer.radian_bank_form --require-recommendation-action-parameter-path ROPE-USE-D19-MARGIN-FRONTIER=proved_branch_bank_transfer.theorem_ids
python scripts/example_consume_circle_ai_contract_pack.py --fingerprints
python scripts/example_consume_circle_ai_contract_pack.py --kind kv_cache_ring_buffer --readiness
python scripts/example_consume_circle_ai_contract_pack.py --all-readiness
python scripts/example_consume_circle_ai_contract_pack.py --kind sparse_attention_coverage --field first_uncovered_lag --include-recommendations --expect-pack-fingerprint <pack_sha256> --expect-contract-fingerprint sparse_attention_coverage=<contract_sha256>
python scripts/example_consume_circle_ai_contract_pack.py \
  --kind sparse_attention_coverage \
  --receipt \
  --field first_uncovered_lag \
  --field first_uncovered_interval_start \
  --field complete_repair_window \
  --field complete_repair_window_covers_context \
  --field complete_repair_window_minimal_for_declared_stride_family \
  --field complete_repair_window_minimal_witness_lag \
  --require-theorem AIT-T0104 \
  --require-theorem AIT-T0172 \
  --require-recommendation SPARSE-LOCAL-FIRST-INTERVAL-REPAIR \
  --require-recommendation SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK \
  --require-recommendation-evidence-field SPARSE-LOCAL-FIRST-INTERVAL-REPAIR=first_uncovered_interval_start \
  --require-recommendation-evidence-field SPARSE-LOCAL-FIRST-INTERVAL-REPAIR=first_uncovered_interval_stop \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=complete_repair_window \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=complete_repair_window_covers_context \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=complete_repair_window_uses_dense_threshold \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=local_window_complete_threshold_is_exact_local_minimum \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=complete_repair_window_minimal_for_declared_stride_family \
  --require-recommendation-evidence-field SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=complete_repair_window_minimal_witness_lag \
  --require-recommendation-theorem SPARSE-LOCAL-FIRST-INTERVAL-REPAIR=AIT-T0104 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0023 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0034 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0172 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0168 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0169 \
  --require-recommendation-theorem SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=AIT-T0170 \
  --require-recommendation-action-parameter SPARSE-LOCAL-FIRST-INTERVAL-REPAIR=proposed_local_window \
  --require-recommendation-action-parameter SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=proposed_local_window \
  --require-recommendation-action-parameter SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=additional_local_slots \
  --require-recommendation-action-parameter-path SPARSE-LOCAL-FIRST-INTERVAL-REPAIR=proposed_local_window \
  --require-recommendation-action-parameter-path SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=proposed_local_window \
  --require-recommendation-action-parameter-path SPARSE-DENSE-LOCAL-COMPLETE-FALLBACK=additional_local_slots \
  --expect-pack-fingerprint <pack_sha256> \
  --expect-contract-fingerprint sparse_attention_coverage=<contract_sha256>
python scripts/example_consume_circle_ai_contract_pack.py --kind strided_candidate_fanout --field full_coverage --field effective_candidate_budget --field duplicate_count --include-recommendations
python scripts/example_consume_circle_ai_contract_pack.py --kind cyclic_memory_residue_winding --field max_alias_load --include-recommendations
python scripts/example_consume_circle_ai_contract_pack.py --kind multicoil_phase_feature --field joint_repeat_horizon --field relative_phase --include-recommendations
python scripts/example_consume_circle_ai_contract_pack.py --kind circulant_block_cyclic_mixer --field max_abs_dense_delta --field block_to_dense_ratio --include-recommendations
python scripts/example_consume_circle_ai_contract_pack.py --kind recurrence_schedule --field scheduled_work_saving --include-recommendations
python scripts/example_consume_circle_ai_contract_pack.py --kind recurrence_schedule --receipt --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
python scripts/example_consume_circle_ai_contract_pack.py --kind seed_rule_exact_regeneration --field storage_saving --include-recommendations
python scripts/example_consume_circle_ai_contract_pack.py --planner --planner-kind sparse_attention_coverage --planner-kind rope_position_distinguishability
python scripts/example_consume_circle_ai_contract_pack.py --planner --planner-kind sparse_attention_coverage --planner-include-values
python scripts/example_consume_circle_ai_contract_pack.py --planner --planner-recommendation SPARSE-LOCAL-FIRST-INTERVAL-REPAIR --planner-include-values

The --planner form reads the generated recommendation index and emits a copy-safe action plan. Each action keeps theorem ids, source links, evidence field names, and non-claims attached, so a downstream project can choose which finite audit or repair target to try without treating the record as model-quality or performance evidence. The example consumer also has --readiness, --all-readiness, and --fingerprints modes and accepts --expect-pack-fingerprint and --expect-contract-fingerprint kind=<sha256>, matching the readiness CLI, so a project can check one contract or the whole pack, discover and pin the exact audited public pack, and consume only a narrow digest. Use --receipt when the downstream job should reject the artifact if a selected evidence field, theorem id, required planner recommendation, required recommendation evidence field, or required recommendation theorem id is missing. It emits a compact acceptance receipt with the pack fingerprint, contract fingerprint, theorem ids, source trails, validation commands, and non-claim boundary. Add --planner-include-values when a downstream planner needs the resolved field values and action parameters too. For the sparse first-interval repair, that includes the proposed local window 6, the next uncovered lag 8, and the AIT-T0104/AIT-T0166/AIT-T0167 theorem boundary. For the sparse largest-gap action, it includes target interval 40..119, proposed local window 119, and the explicit not_claimed boundary saying the record is a finite audit action, not an optimal sparse-layout or performance claim.

For a downstream project that does not want to import Circle’s Python package, use the standard-library-only CI example:

python examples/downstream_ci_accept_circle_ai_contracts.py --format json
python examples/downstream_ci_accept_circle_ai_contracts.py --format json --include-values
python examples/downstream_ci_accept_circle_ai_contracts.py --format json --planner-recommendation SPARSE-LOCAL-FIRST-INTERVAL-REPAIR --include-values
python examples/downstream_ci_accept_circle_ai_contracts.py --format json --planner-recommendation ROPE-USE-D19-MARGIN-FRONTIER --include-values
python scripts/check_downstream_ci_acceptance_example.py --summary

That example validates the pinned policy in examples/circle_ai_contract_acceptance_policy.json against the raw generated pack. It checks every required contract fingerprint, proof/readiness flag, evidence field, theorem id, required planner recommendation, required recommendation evidence field, required recommendation theorem id, and required recommendation action-parameter key or nested action-parameter path. It also validates every emitted selected action against the source recommendation record, so action-plan drift fails even when the drifting recommendation was not explicitly pinned by policy. The default JSON keeps evidence field names only. It uses the generated acceptance report and receipt schema ids and keeps accepted_contracts as a consumer-friendly alias for the canonical receipts array. The repository-side checker runs the portable script in the default, value, sparse-selected, and RoPE-selected modes, then validates the emitted report and receipts against the generated schema sidecars. It also runs a rejection case and checks that --format json emits a circle_calculus.downstream_ci_rejection_report.v0 object on stderr against the generated rejection-report schema sidecar. The --include-values form adds resolved values, missing_evidence_fields, and source action_parameters, such as the RoPE D19 request context 131072, the RoPE D19 classifier_regions table, or the sparse first-interval repair window 6. The --planner-recommendation selector keeps vendored CI focused on one named planner action and fails if that action is not selected by the accepted pinned policy. In JSON mode, failed runs keep accepted=false, exact failures, pinned pack and policy paths, requested planner recommendation ids, and an explicit non-claim boundary, so downstream automation can distinguish stale fingerprints, unready proof status, and missing planner actions without scraping prose logs. It is an artifact-consumption gate, not a model-quality or deployment-safety proof.

When a downstream project already has a runner artifact directory, it can use the standard-library-only artifact verifier:

python examples/downstream_ci_verify_circle_ai_artifacts.py \
  reports/rope_contract/standard_rope_config_artifact_manifest.json \
  --require-kind rope_position_distinguishability \
  --require-theorem-id AIRA-T0239 \
  --require-evidence-field real_phase_dirichlet_guardrail \
  --require-recommendation-id ROPE-USE-D19-MARGIN-FRONTIER \
  --require-validation-command "python scripts/rope_certify.py --preset llama_style_10000_4k --format json" \
  --require-normalized-param head_dim=128 \
  --require-normalized-param context_length=131072 \
  --require-status proved \
  --require-decision passed \
  --require-assurance mixed_theorem_and_computation \
  --require-passed \
  --require-manifest-check

A multi-contract CI job can pass several *_artifact_manifest.json files and repeat --require-kind for every contract family that must be present. Add --require-theorem-id for theorem ids that downstream code explicitly depends on, --require-evidence-field for receipt fields it reads, and --require-recommendation-id for planner actions it invokes. Add --require-validation-command when CI depends on an exact receipt-emitted recheck command, --require-model-config-fingerprint when the RoPE receipt came from an imported model config.json, and --require-normalized-param when it must pin the certified configuration values. Use --pin-policy PATH to reload either a whole prior verifier report or just its pin_policy object; explicit --require-* flags merge with the loaded policy.

That script checks the manifest, referenced file SHA-256 hashes, declared schema ids, mirrored receipt status, and optional manifest-check report without importing Circle’s Python package.

Example

Run one representative command from each contract:

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/strided_candidate_fanout_certify.py
python scripts/circle_ai_contract_ready.py --kind strided_candidate_fanout --digest --field full_coverage --field effective_candidate_budget --field duplicate_count --include-recommendations
python scripts/recurrence_schedule_certify.py
python scripts/cyclic_memory_certify.py
python scripts/circle_ai_contract_ready.py --kind multicoil_phase_feature --digest --field joint_repeat_horizon --field relative_phase --include-recommendations
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 important habit is not just reading PASS or GAPS. Read the theorem ids and the non-claim text attached to the report.

Contract Pack Fields

For a downstream AI project, the generic pack is the stable integration surface. Start by checking contract_readiness_index, then read the minimum evidence fields for the contract kind you consume.

The complete generated-field checklist is intentionally kept out of this lesson. Use the AI Contract Pack Audit page when wiring another project to the JSON schema.

Those fields are contract evidence, not performance evidence. Attach benchmark rows beside them in downstream projects instead of overwriting them.

Sample Report Shapes

The reports are intentionally field-heavy. For a first read, focus on the status line, the main evidence fields, the theorem ids, and the boundary.

RoPE exact-discrete failure example:

exact_discrete_contract=FAIL
common_collision_gap=114
total_bank_collision_pair_count=14
sample_collision_pairs=((0, 114), ...)
theorem_ids=AIRA-T0021,AIRA-T0024,AIRA-T0036,...
boundary=Exact pass/fail is for the declared integer-period discretized RoPE model.

KV-cache live request with sink-window policy:

kv_cache_contract=LIVE cache_size=16 current=31 token=20 slot=4
adapter_request_trace=PASS tokens=(20, 24, 29, 31)
stale_requested_count=0
sink_window_policy=PINNED_PREFIX_PLUS_ROLLING sink_size=4
tokens_distinct=True
token_count=20 token_count_bound=20 token_count_le_sink_plus_cache=True
disjoint_exact_token_count=20 token_count_eq_sink_plus_live_window_when_disjoint=True
sink_tokens_non_future=True sink_tokens_retained_by_policy=True
theorem_ids=AIM-T0069,AIM-T0097,AIM-T0102,AIM-T0104,AIM-T0108,AIM-T0110,...

Sparse-attention gap certificate:

stride_family_contract=GAPS context=120 strides=(7, 13)
covered_lags=10 uncovered_lags=109 first_gap=5
raw_budget_shortfall=True certifies_incomplete=True
unique_lag_shortfall=True certifies_incomplete=True
collision_pair_counts=lag=0 query=0
collision_pair_severity=lag_bounds_dedup_loss=True lag_excess_over_dedup_loss=0 query_bounds_dedup_loss=True query_excess_over_dedup_loss=0
first_gap_local_repair=shortfall=1 needed_window=5 current_window_below_first_gap=True repair_window_reaches_first_gap=True repair_window_covers_context=False repair_window_is_final_positive_lag=False repair_threshold_matches_final_lag=True
first_interval_repair_next_gap=8 still_has_gap=True covers_context=False
complete_local_repair=window=119 additional_slots=115 covers_context=True uses_dense_threshold=True exact_local_minimum=True
theorem_ids=AIT-T0020,AIT-T0078,AIT-T0110,AIT-T0111,...

Looped recurrence schedule certifier:

recurrence_schedule=READY required_steps=4 exit_step=4
work_count_step=2 active=6 inactive=2 active_plus_inactive_eq_token_count=True
total_active_token_work=21 total_inactive_token_work=19 full_loop_token_work=40 scheduled_work_saving=19 scheduled_work_saving_accounting=True
active_inactive_work_accounting=True scheduled_work_saving_matches_inactive_work=True
scheduled_work_saving_positive=True active_work_below_full_loop_work=True scheduled_work_saving_positive_iff_active_work_shortfall=True
scheduled_work_saving_zero=False active_work_equals_full_loop_work=False scheduled_work_saving_zero_iff_no_active_work_shortfall=True
active_token_counts_descend=True inactive_token_counts_ascend=True
post_period_active_token_count=0 post_period_inactive_token_count=8
public_fixture_4_8_4_total_active_token_work=20 public_fixture_4_8_4_total_inactive_token_work=12 public_fixture_8_4_full_loop_token_work=32 public_fixture_4_8_4_scheduled_work_saving=12
default_fixture_5_8_5_total_active_token_work=21 default_fixture_5_8_5_total_inactive_token_work=19 default_fixture_8_5_full_loop_token_work=40 default_fixture_5_8_5_scheduled_work_saving=19
post_period_extension_horizon_steps=6 post_period_extension_total_active_token_work=21 post_period_extension_total_inactive_token_work=27 post_period_extension_full_loop_token_work=48 post_period_extension_scheduled_work_saving=27
post_period_extension_active_work_unchanged=True post_period_extension_inactive_work_added_token_count=True post_period_extension_saving_added_token_count=True
post_period_extra_steps=3 post_period_multi_extension_horizon_steps=8 post_period_multi_extension_scheduled_work_saving=43
post_period_multi_extension_active_work_unchanged=True post_period_multi_extension_saving_added_extra_token_count=True
periodic_shift=base_token=7 passes=3 shifted_token=22 required_steps_invariant=True recurrence_budget_invariant=True active_at_step_invariant=True
theorem_ids=AIM-T0026,AIM-T0027,AIM-T0028,AIM-T0029,AIM-T0030,AIM-T0033,AIM-T0034,AIM-T0036,AIM-T0111,AIM-T0112,AIM-T0120,AIM-T0123,AIM-T0128,AIM-T0129,AIM-T0126,AIM-T0127,AIM-T0130,AIM-T0131,AIM-T0144,AIM-T0145,AIM-T0138,AIM-T0139,AIM-T0132,AIM-T0133,AIM-T0134,AIM-T0146,AIM-T0135,AIM-T0140,AIM-T0141,AIM-T0142,AIM-T0147,AIM-T0143,AIM-T0150,AIM-T0151,AIM-T0152,AIM-T0153,AIM-T0154,AIM-T0155,AIM-T0156,AIM-T0157,AIM-T0158,AIM-T0159,...

Seed-rule exact-regeneration fixture:

seed_rule_contract=READY artifact_id=finite_circle fixture_n=128 exact_regeneration=True generator_shorter=True
storage_accounting=explicit_length=454 generator_length=383 storage_saving=71 storage_saving_positive=True
bounded_search=candidate_count=3 exact_candidate_count=2 has_best_exact=True has_best_shorter=True

These snippets are examples of report fields, not proofs. The proof status comes from the cited theorem ids and Lean declarations.

Theorem Clusters

Use this map before opening theorem cards:

Contract First Proof Question Audit Page
RoPE do the declared phase-bank and D19 frontier fields resolve to proved theorem ids? RoPE proof audit
KV-cache does the live-window/stale-read predicate match the ring-buffer overwrite boundary? KV-cache proof audit
Sparse attention do covered/uncovered lag lists, candidate budgets, and repair fields resolve to proved theorem ids? Sparse attention proof audit
Looped recurrence do active-token work, post-period extension, and whole-period shift fields resolve to proved theorem ids? Looped recurrence audit
Contract pack do minimum fields, source links, validation commands, and planner recommendations match the generated JSON schema? AI contract pack audit

The cards below are representative anchors, not a reading requirement for the first pass. The individual lessons and audit pages contain the fuller theorem trails.

Representative theorem-card shelf for the AI contract suite

RoPE

KV-Cache

Sparse Attention

Looped Recurrence

Code

The CLI surfaces are the non-Lean entry points:

Certificate Schemas

Current stable or named certificate identifiers:

circle_calculus.rope_position_distinguishability.v0
circle_calculus.integer_phase_bank_distinguishability.v0
circle_calculus.rational_turn_ratio_finite_margin.v0
circle_calculus.standard_rope_interval_margin.v0
circle_calculus.kv_cache_ring_buffer_certificate.v0
circle_calculus.stride_family_sparse_attention_certificate.v0
circle_calculus.ai_contract_pack.v0

The sparse-attention report is field-oriented, but it now has the same kind of top-level schema id as the RoPE and KV-cache reports.

What This Does Not Prove

  • RoPE certificates do not prove that real-valued RoPE models have better context length or perplexity.
  • KV-cache certificates do not prove paging policy, kernel correctness, serving-stack safety, throughput, or retrieval quality.
  • Sink-window certificates do not prove StreamingLLM quality or sink-token usefulness; they only prove finite request-list membership.
  • Sparse-attention certificates do not prove attention quality, runtime, memory savings, or long-context model quality.
  • Looped recurrence certificates do not prove recursive reasoning, adaptive-exit quality, throughput, memory savings, or model quality.
  • Seed-rule certificates do not prove global minimality, universal compression, or semantic usefulness.
  • Python reports and browser widgets are executable references, not Lean proofs.

Reading Order

  1. RoPE Certifier
  2. KV-Cache Ring Buffer
  3. Sparse Attention Coverage
  4. Looped Recurrence Contracts
  5. Generative Structures
  6. AI Contract Ladder

Dictionary

Previous: AI Overview Next: RoPE Certifier