Skip to main content

67  Circle Calculus and Proof-Carrying AI Contracts

67.1 Chapter status

Field	Value
Chapter ID	circle-calculus-and-proof-carrying-ai-contracts
Part	Part III - Routing, Compression, Representation, and Substrates
Status	conceptual
Manuscript maturity	v0.3 manuscript draft
Last updated	2026-08-08
Primary source records	circle_calculus_core, circle_ai_contract_suite, rope_position_certifier, proof_carrying_circular_computation, circle_ai_architectures
Claim label	Design rationale
Evidence level	argument
Source queue	primary: circle_calculus_core, circle_ai_contract_suite, rope_position_certifier; supporting: proof_carrying_circular_computation, circle_ai_architectures
Source loading state	source notes: circle_calculus_core, circle_ai_contract_suite, rope_position_certifier, proof_carrying_circular_computation, circle_ai_architectures
Test state	proof_target_record.valid.json and proof_contract_receipt_record.valid.json pass repository-level protocol fixture validation, with proof-contract receipts now covering receipt state, proof boundary, fingerprint status, consumer state, staleness policy, source refs, support-state effect, and non-claims; AsiStackProofs.ProofCarryingContracts passes the Lean build for receipt-boundary, consumer-gate, missing-boundary, missing-readiness, stale/unsupported-consumer, and replay-artifact predicates; python3 scripts/validate_circle_public_replay.py validates the pinned Circle consumer-gate fixture and rejects digest-mismatch, missing-theorem, stale-contract, and unsupported-transfer mutations; python3 scripts/validate_circle_contract_pack_archive.py validates the archived public-safe pack and acceptance-policy report; python3 scripts/validate_circle_concrete_evidence_surface.py checks that the concrete Circle receipt facts remain visible without chapter-core or model-quality promotion; theorem-id resolution, clean Circle replay from this repo, and downstream workload preservation checks remain planned.

67.2 Drafting guardrail

This chapter uses the Circle Calculus source family as proof-boundary context for finite structural AI contracts. It does not claim that this ASI Stack repo has built Circle, resolved external theorem IDs, replayed receipt packs from source, or validated downstream model behavior. The public consumer gate checks a pinned receipt boundary and overclaim controls. The local Lean surface now also proves a finite seven-transition contract lifecycle in which root revocation persistently invalidates a descendant without disabling an unrelated lineage; those authored state semantics are not deployed transport or revocation evidence.

Optional substrates need baselines before adoption. Proof-carrying contracts supply the narrower transport layer for one class of substrate evidence: finite structural facts that can travel with proof references, deterministic fields, receipts, and non-claims. The contract does not decide that the substrate is useful; it prevents a useful structural fact from losing its boundary on the way to memory, routing, compression, or runtime decisions.

The receipt is a passport for a structural fact, not a promotion ticket for a substrate. It lets a downstream consumer know what was proven, how to check the package boundary, and which claims remain outside the proof.

67.3 Human Reading Path

Concrete lens. The simpler verified-badge baseline treats a theorem name as architecture approval. The transport envelope instead resolves the exact receipt and asks whether the requested consumer claim lies inside its authority.

Optional substrates need baselines before their structure can travel safely into contracts. Circle Calculus narrows that idea to proof-carrying structural facts: finite claims that can move through the stack with receipt references, deterministic fields, and replay expectations. The target is not grand certainty, but portable restraint. It is small certified structure that other layers can consume without guessing what was checked.

This is not a claim that every AI behavior can be proved. It is a way to keep small structural guarantees from dissolving into prose. A proof-carrying contract should say exactly what was checked, where the receipt lives, who may consume it, and what the result does not imply. That makes formal work useful without letting theorem language overrun the evidence boundary. The discipline is strongest when the formal artifact is boring, replayable, and narrow. Narrow proof is valuable because it tells the rest of the system exactly where not to overclaim.

The receipt should make a limited guarantee easier to trust and easier to refuse. Trust begins where the contract names its own edge clearly enough.

67.4 Problem

Selected mathematical and AI-infrastructure claims need theorem-linked, machine-readable contracts without treating proofs as model-quality evidence. Circle-style artifacts are useful because they can identify theorem IDs, proof status, deterministic certificate fields, fingerprints, consumer checks, and explicit non-claims.

The hard problem is authority transfer. A finite cyclic-address proof can be valid and still say nothing about language-model quality, runtime, memory, context length, deployment safety, or ASI capability. The ASI Stack therefore needs a contract boundary that lets downstream systems consume structural facts while preserving the limits of those facts.

Proof authority and consumer authority are separate. A theorem can authorize a structural statement; it does not authorize a routing decision, architecture adoption, benchmark promotion, or reader-facing capability claim. Those later moves need their own workloads, baselines, metrics, and evidence artifacts.

67.5 Why existing approaches are insufficient

Ordinary prose, tests, and diagrams can show intent, but they do not give downstream systems stable theorem IDs, proof status, receipt fingerprints, replay checks, and explicit non-claims. Without those fields, a reader cannot tell whether a claim is a Lean theorem, a Python fixture, a generated report, a model benchmark, or a design hypothesis.

Lean is the external proof-assistant baseline named here through ext_lean4_theorem_proving. Circle contracts borrow the need for stable theorem names, records, propositions, proof terms, and computation boundaries, then add receipt and replay fields around circular-computation claims. That comparison does not mean Circle statements have been imported into Lean or that proof-carrying AI contracts validate runtime behavior.

The key insufficiency is theorem laundering: a finite structural result gets repeated as if it were evidence for quality or deployment behavior. The proof-carrying contract blocks that move by carrying its own consumer gate and non-claim boundary.

Another insufficiency is stale proof reference drift. The text may preserve a theorem name while the external project changes the declaration, proof policy, sidecar schema, or generated artifact. A contract needs version, hash, resolver status, validation command, and failure behavior so staleness becomes visible.

67.6 Core Claim

Reader claim. A proof-carrying contract lets a small formal fact travel without turning that fact into a claim about model behavior or deployment.

Operational rule. A consumer may use a formal receipt only after resolving its theorem identity, assumptions, source and toolchain, fingerprints, replay state, expiry, and non-claims. The consumer must separately justify every empirical or operational decision it wants to make from that fact.

[circle-calculus-and-proof-carrying-ai-contracts.core, label: Design rationale, support: argument] Circle Calculus and Proof-Carrying AI Contracts owns a theorem-, model-, artifact-, implementation-, consumer-, claim-, version-, and time-specific Proof Contract Transport Envelope: a finite formal fact may travel only with resolvable proof identity, exact assumptions and semantics, source and toolchain provenance, content fingerprints, deterministic recomputation or replay, least-authority consumer gates, expiry and revocation, and preserved non-claims; theorem validity, receipt readiness, archive integrity, or transport success alone confers no model-quality, runtime, memory, safety, deployment, transfer, support, or SOTA authority.

The distinct owner is transport of an already scoped formal fact from a named producer artifact to a named consumer. Formal Methods retains theorem truth; Executable Specifications retains the engineering-to-model refinement; Runtime retains behavior; Evidence retains empirical support; Readiness, Incident, and Release retain operational and public authority. The envelope cannot manufacture any of those facts—it can only keep a real one from changing identity, scope, assumptions, or non-claims in transit.

Circle source mappings ground the discussion of theorem-linked contract families, proof-status discipline, receipt fields, exact/discretized RoPE boundaries, cyclic address proofs, CLI reports, and explicit non-claims. The separate external receipt slice and ASI-side consumer gate show a bounded structural receipt path, not a local Circle proof stack or downstream model-behavior improvement.

67.6.1 Claim-source mapping status

Appendix C now records passage-reviewed mappings for all five assigned sources. The mappings support theorem-status discipline, machine-readable receipts, proof-boundary preservation, exact/discretized RoPE boundaries, cyclic compute contracts, consumer gates, and non-claims. The external receipt slice and public consumer gate support only their recorded structural boundaries, not downstream model quality, local Circle proof ownership, clean replay from this repo, or substrate-performance claims.

Source	What it supports	Limit
circle_calculus_core	Lean declarations, theorem manifests, Python reference models, JSON schemas, generated contract packs, proof boundaries, stable APIs, verification commands, and explicit non-claims.	A separate external Circle rope receipt slice is recorded in docs/circle_external_receipt_slice.md, a separate ASI-side consumer gate is recorded in docs/circle_public_replay_consumer_gate.md, and a bounded public-safe pack archive is recorded in docs/circle_contract_pack_archive.md; none claims chapter-core theorem transport or downstream model-quality evidence.
circle_ai_contract_suite	Finite engineering-object mappings, theorem ids, Python certificates, schema fields, consumer reports, require gates, bundle checks, fingerprints, and non-claim boundaries.	A separate external Circle rope receipt slice is recorded in docs/circle_external_receipt_slice.md, the ASI-side consumer gate validates one public receipt boundary, and the Circle contract-pack archive verifies a generated pack snapshot; no downstream consumer or chapter-core proof-transport claim is validated.
rope_position_certifier	Exact/discretized RoPE position-bookkeeping contracts with phase banks, collision reports, theorem ids, machine-readable certificates, public commands, numerical-diagnostic boundaries, and explicit non-claims.	A separate external rope receipt slice is recorded in docs/circle_external_receipt_slice.md; it does not support model-quality, context-length, speed, memory, training-stability, deployment, or chapter-core proof-transport claims.
proof_carrying_circular_computation	Cyclic-address primitives, rewrite/address transformations, theorem manifests, backend-selection discipline, and benchmark requirements for proof-carrying cyclic computation.	A separate external Circle rope receipt slice is recorded in docs/circle_external_receipt_slice.md, but no Circle sidecar examples, CoilIR lowering, or backend benchmarks were run here.
circle_ai_architectures	Separation between finite-indexing facts and ML-relevant guarantees, plus ordinary baselines, wrong-period controls, scalar controls, learned-position controls, and negative results.	A separate external Circle rope receipt slice is recorded in docs/circle_external_receipt_slice.md, but no model-quality experiment, benchmark fixture, sidecar test, cyclic-architecture test, or MLX run was executed here.

67.7 Mechanism

Proof-carrying contracts sit one layer below substrate adoption. They do not decide whether a substrate is useful; they decide whether a finite structural fact can travel without losing its theorem status, deterministic fields, fingerprints, replay requirements, and non-claim boundary. The Circle source family supplies the pattern: theorem manifests and proof policy from the core project, consumer fields and receipt gates from the AI contract suite, exact/discretized phase-bank boundaries from the RoPE certifier, cyclic-address and backend-separation discipline from circular computation, and baseline discipline from Circle AI Architectures.

The working mechanism is an eighteen-stage transport lifecycle. It separates theorem verification, semantic correspondence, deterministic computation, artifact transport, consumer authority, and downstream empirical support so a green state in one cannot silently fill another.

The receipt boundary is the main artifact. It lets the book say “this finite structural fact is proof-linked” without smuggling in claims about model behavior. In this repo, the new proof-contract receipt fixture is intentionally conservative: it can describe a source-reported external theorem family and a not-run replay state, but it cannot make the theorem local, replayed, or performance-bearing.

flowchart LR
  Object["Engineering object"] -- "finite model" --> Finite["Finite address, window, phase, or schedule"]
  Finite -- "theorem refs" --> Theorems["Lean theorem ids and proof status"]
  Finite -- "deterministic fields" --> Fields["Deterministic certificate fields"]
  Theorems -- "attach proof boundary" --> Receipt["Proof-carrying receipt"]
  Fields -- "attach replay boundary" --> Receipt
  Receipt -- "consumer checks" --> Consumer["Consumer gate and replay check"]
  Consumer -- "passes structural gate" --> Structural["Structural claim"]
  Consumer -- "preserves scope" --> Nonclaims["Explicit non-claims"]
  Structural -- "may request" --> Workload["Optional downstream workload"]
  Workload -- "only if run" --> Metrics["Baselines, controls, metrics, reports"]
  Metrics -- "opens review" --> Promotion["Possible support-state promotion"]
  Nonclaims -. "blocks overreach" .-> Overreach["Quality, speed, context, safety, or ASI claim"]

What the proof receipt flow shows: The receipt flow separates finite structural facts from downstream performance claims. Theorem references and deterministic fields can support a structural claim only within scope; quality, speed, context, safety, and ASI claims remain blocked until workload evidence exists.

Operationally, the layer should produce artifacts that can be inspected without rerunning the whole cognition path. A downstream reader or executor should be able to locate the relevant theorem references, validation commands, deterministic fields, receipt fingerprints, unsupported axes, and failure conditions.

The repository now mechanizes the smallest boundary that can be stated without importing the external Circle proof stack: a downstream-ready receipt must expose theorem references, deterministic fields, and an explicit non-claim boundary, and a downstream promotion gate must demand workload, baseline, metric, and evidence-artifact fields beyond contract readiness. The public proof_contract_receipt_record schema adds the adjacent receipt fields that prose needs: receipt state, finite-model scope, proof boundary, proof status, source version, content fingerprint, fingerprint status, resolver status, replay status, consumer permissions, consumer state, staleness policy, failure behavior, source refs, support-state effect, and evidence references. The Circle consumer-gate validator applies those fields to the pinned CC-AI-CONTRACT-ROPE-001 receipt and rejects malformed or overclaimed uses, while remaining silent about unrun Circle commands in this repository.

The contract should therefore be read in two layers. The proof layer says whether a finite structural fact has a theorem-linked receipt. The consumer layer says whether that receipt is adequate for a particular downstream use. Passing the first layer can be necessary for the second, but it is never sufficient by itself.

67.7.1 Worked proof-transport trace: one receipt, two consumers

The public Circle lane carries one exact object through both layers. Receipt CC-AI-CONTRACT-ROPE-001 names the rope_position_distinguishability contract at Circle commit 63b0f511, requested margin 1/328459, seven required theorem IDs, deterministic evidence fields, and four content fingerprints. The ASI-side validator accepts that pinned record and rejects four mutations: a digest mismatch, a missing theorem, a stale contract fingerprint, and an attempt to use the receipt for unsupported transfer authority.

Now give the same receipt to two consumers:

Consumer	Question	Decision	Reason
Position-bookkeeping diagnostic	Does this declared finite RoPE contract carry the required theorem identities and exact/discretized collision fields?	Accept the bounded structural receipt.	The pinned identity, theorem set, deterministic fields, and fingerprints satisfy that consumer’s narrow contract.
Architecture promotion gate	Does the receipt show that a trained model uses longer context better, faster, or with less memory?	Reject promotion.	No model workload, baseline, quality metric, runtime trace, or memory result is present.

Nothing about the theorem changes between those decisions. What changes is the authority requested by the consumer, so proof transport cannot collapse into a single green badge. A valid receipt can be enough for a diagnostic and insufficient for adoption at the same time.

The simpler baseline is to paste a theorem name into an architecture proposal and call the proposal “verified.” The transport envelope instead makes the requested downstream claim explicit, checks whether the receipt actually owns that claim, and leaves the missing workload evidence as an open residual.

67.7.2 Concrete Circle Receipt Boundary

The public-safe Circle lane is now concrete enough to show, but only as a bounded receipt boundary. The imported record says that an external Circle checkout at commit 63b0f511 built the Circle Lean target, certified the CC-AI-CONTRACT-ROPE-001 rope_position_distinguishability contract for requested margin 1/328459, emitted a ready digest, accepted a receipt, and passed the recorded public-safe external test batch. That does not promote the Circle core claim; it shows one narrow proof-contract receipt path that downstream ASI Stack consumers can check.

Field	Recorded value	Boundary
External source state	Circle checkout commit 63b0f511, clean after the corrected commands	External local replay summary; the Circle project is not vendored here.
Contract	CC-AI-CONTRACT-ROPE-001, family rope_position_distinguishability	Structural proof-contract receipt only.
Requested margin	1/328459	Recorded request boundary; not a general context-length result.
Certifier result	status proved, request_passed true, decision passed, assurance mixed_theorem_and_computation, theorem_count 55	Certifier receipt evidence, not model-quality evidence.
Ready digest	ready=True fields=31 missing=0 theorems=75	Contract-pack readiness summary, not downstream usefulness.
Deterministic evidence fields	evidence.d19_proved_request_status="proved", evidence.d19_proved_first_channel_bank_transfer=true, evidence.real_phase_dirichlet_witness_guardrail=true, evidence.exact_discrete_pass=true, evidence.total_bank_collision_pair_count=0	Exact/discretized receipt fields and guardrails only.
Seven theorem IDs checked by the ASI consumer gate	AIRA-T0058, AIRA-T0059, AIRA-T0171, AIRA-T0172, AIRA-T0239, AIRA-T0240, AIRA-T0241	Required theorem references for this receipt boundary only.
Recommendation	ROPE-USE-D19-MARGIN-FRONTIER	Planner guidance attached to the receipt, not an adoption decision.
Fingerprints	receipt 91b72a6dcf821a9733f21800cd1093a3d0665588022031ba72c94893800330c3; normalized request 20e68c5f787e267c6611bc57b8d8e98e1cb0f5a74f272379716a5d83e761407d; contract pack df673f8a661fc89a26372685986c92f2221aaa617d6738fce5c2a76bd5d0eeae; contract a0f35d3e89e9b6eac555f0392450f4f75cf7e70f30cff44ec7434f61bd85b468	Replay and staleness checks, not proof of deployed transport.
External test batch	145 passed in 718.24s (0:11:58)	External Circle public-safe batch; not an ASI Stack runtime or workload evaluation.
ASI consumer gate	Rejects digest mismatch, missing required theorem ID, stale contract fingerprint status, and unsupported transfer-claim use	Public fixture guard for downstream receipt use.

The concrete surface matters because it gives readers numbers, theorem IDs, fingerprints, and rejection behavior instead of abstract proof language. Its non-claims matter just as much: it does not prove model quality, reasoning ability, context length, speed, memory scaling, deployment safety, transfer, or ASI; it does not prove deployed proof-contract transport inside The ASI Stack; and it does not promote any chapter core claim above argument.

67.7.3 Proof receipt lifecycle

The complete lifecycle is:

1. Register the exact theorem, statement, assumptions, finite model, source, toolchain, implementation object, intended consumer, and prohibited inferences.
2. Pin public-safe source, dependencies, prover, build configuration, theorem manifest, schema, dictionary, and artifact digests.
3. Build the named formal target and retain the command, environment, logs, failures, proof boundary, and compiled-declaration receipt.
4. Resolve every theorem and dictionary ID to one compiled declaration, exact statement, assumptions, proof status, source location, and version.
5. Bind the engineering object to the formal model through explicit abstraction, discretization, numerical, representation, and implementation-refinement obligations.
6. Canonicalize the contract and fingerprint source, model, theorem set, deterministic fields, receipt, consumer policy, and pack.
7. Recompute bounded reference outputs from pinned inputs while separating exact arithmetic, tolerances, numerical diagnostics, nondeterminism, and non-proof layers.
8. Attach non-claims for all unproved semantic, empirical, causal, resource, safety, deployment, transfer, support, and SOTA axes.
9. Validate schemas, fields, state transitions, provenance closure, consumer policy, staleness, failure behavior, and support-state effect.
10. Replay in a clean environment from public-safe artifacts, checking digests, resolution, build, recomputation, receipt fingerprint, and archived output.
11. Reject missing theorem, changed statement, digest mismatch, stale proof, ambiguous resolver, altered assumptions, forged status, missing non-claim, unsupported consumer, replay omission, and promotion-overclaim mutations.
12. Issue a least-authority gate naming the exact fact, object, version, permitted use, prohibited inference, evidence state, expiry, verifier command, fallback, and residual owner.
13. Require separate natural workloads, strong baselines, controls, metrics, complete costs, independent evaluation, and result artifacts before empirical promotion.
14. Transport through artifact graphs with authenticated provenance, immutable lineage, dependency closure, custody, access and rights controls, acknowledgements, and consumer receipts.
15. Monitor theorem, source, toolchain, schema, implementation, consumer, policy, rights, and threat drift and invalidate all affected descendants.
16. Fail closed, quarantine, use the last verified or ordinary fallback, repair, replay, and recover without retaining stale authority.
17. Reproduce resolution, build, recomputation, transport, invalidation, and recovery with independent producers, resolvers, and consumers, then test heterogeneous transfer.
18. Expire on material change or horizon and assign every model gap, unverifiable dependency, replay failure, consumer misuse, revocation, and residual.

The shorter receipt-state vocabulary below remains useful, but it is not the whole transport protocol. A fingerprinted receipt can still have the wrong semantic model; a resolver_checked receipt can still be stale downstream; and a consumer_gated receipt can still lack empirical evidence.

The receipt lifecycle is explicit:

State	Meaning	Allowed use
theorem_linked	A theorem reference is named with proof-status scope.	Structural discussion only until resolver status is known.
dictionary_bound	The finite model and engineering object are tied to a recognized contract family.	Receipt design and local surrogate tests.
fingerprinted	Content or normalized parameters have a recorded fingerprint.	Replay candidate, not quality evidence.
resolver_checked	The theorem reference has been resolved or failed by a stated command.	Structural use if the consumer gate allows it.
consumer_gated	Allowed and blocked downstream uses are recorded.	Only the allowed consumer uses.
workload_blocked	Workload, baseline, metric, or evidence artifact is missing.	No quality, runtime, memory, or transfer promotion.
retired_or_superseded	The receipt is stale, replaced, or contradicted.	Historical evidence only.

67.8 Interfaces

• Formal Methods owns theorem truth, statement, assumptions, proof status, compiled declarations, and prover soundness; Transport owns their envelope only.
• Executable Specifications owns the engineering-to-model refinement obligation; a receipt cannot invent semantic correspondence.
• Artifact Graphs and Supply Chain own source, dependency, build, signature, custody, access, and lineage provenance.
• Runtime owns executable binding and behavioral conformance; a structural receipt is not runtime behavior.
• Context, Memory, Recurrence, Routing, Compression, and Cyclic Substrates consume only named structural facts within their gates.
• Verification owns evaluator adequacy, theorem resolution, replay, negative controls, and dispute state.
• Security, Privacy, and Rights own adversarial provenance, trust roots, confidentiality, license, data, access, and revocation.
• Resource Economics owns build, resolution, recomputation, storage, verification, transport, human, recovery, and opportunity costs.
• Claim Ledgers and Evidence own support states, transitions, non-claims, contrary evidence, reproduction, transfer, expiry, and residuals.
• Readiness and Incident Response own admission, quarantine, rollback, recovery, and descendant invalidation.
• Release owns public artifact and statement authority; transport cannot publish or promote by itself.
• Private consumers may return public-safe receipts and boundaries, but private outcomes cannot be inferred from acceptance.

The interface lets adjacent layers compose without absorbing each other’s authority. Coil memory can consume a freshness or coverage receipt as a structural guardrail. Cyclic mixers can consume a phase-bank or collision receipt as a diagnostic. Evidence ledgers should still demand workloads, baselines, metrics, and run artifacts before quality or runtime claims move.

A useful receipt records theorem refs, proof policy, source version, content fingerprint, deterministic fields, verifier command, resolver status, consumer requirements, failure behavior, and non-claims. If any of those are missing, the receipt can still be discussed as design context, but downstream use should remain blocked or residual.

Minimum proof-contract receipt fields:

• receipt_id
• receipt_state
• source_project
• contract_family
• engineering_object
• finite_model
• proof_boundary
• theorem_refs
• proof_status
• source_version
• content_fingerprint
• fingerprint_status
• deterministic_fields
• verifier_command
• verifier_result
• resolver_status
• replay_status
• consumer_gate
• consumer_state
• staleness_policy
• failure_behavior
• source_refs
• support_state_effect
• non_claims
• evidence_refs

67.9 Invariants

The proof-contract invariants keep structural receipts from inflating into quality claims: theorem references, executable checks, and non-claim boundaries must survive every downstream transfer.

• Every fact is specific to theorem, statement, assumptions, model, artifact, implementation relation, consumer, use, version, and time.
• Theorem identity resolves uniquely to a compiled declaration under pinned source and toolchain, or the envelope fails closed.
• Proof, schema, deterministic computation, numerical diagnostics, replay, archive integrity, consumer readiness, and empirical support remain distinct.
• A theorem authorizes only its statement under its assumptions; semantic correspondence and implementation refinement are separate obligations.
• Fingerprints cover canonical content and dependencies; algorithm, canonicalization, collision policy, and trust root remain explicit.
• Deterministic fields reproduce from pinned public-safe inputs, with tolerances, nondeterminism, failures, and discarded attempts visible.
• Every theorem, dictionary, artifact, source, dependency, schema, policy, and consumer reference resolves or remains an explicit residual.
• Non-claims survive quotation, summary, serialization, transport, caching, supersession, and downstream consumption.
• Consumer permission is least-authority across fact, object, use, claim axis, environment, version, and expiry.
• Downstream quality, runtime, memory, safety, deployment, or transfer promotion requires separate natural workload evidence with strong controls.
• Missing, ambiguous, stale, altered, revoked, unsupported, rights-incompatible, or unreplayable envelopes block use.
• Every descendant, cache, citation, claim, artifact, and consumer receipt inherits upstream invalidation.
• The ordinary or last verified fallback remains executable, tested, rights-compatible, and reachable within the recovery window.
• Independent reproduction does not share the decisive producer, resolver, consumer, trust root, or implementation defect.
• Private inputs and outcomes never enter public evidence through inference from a public-safe receipt.
• Support, deployment, release, safety, transfer, or SOTA movement requires an accepted transition for that exact claim and scope.
• Qualifications expire on material theorem, source, toolchain, model, implementation, schema, consumer, policy, rights, threat, or time change.
• Every theorem-model gap, unverifiable dependency, replay failure, consumer misuse, revocation, and residual has an owner and reopening condition.

Non-claim preservation is the proof-contract invariant that matters most. A proof-carrying receipt must not lose its boundaries when it is copied into a later chapter, benchmark card, route decision, or prototype roadmap.

Consumer specificity keeps the receipt from becoming universal by accident. A receipt accepted for one consumer does not automatically transfer to another consumer with different workloads, numeric tolerances, threat model, or evidence standard.

67.10 Failure modes

• A theorem name, badge, diagram, proof count, or green build creates authority beyond the statement.
• A theorem ID resolves to the wrong declaration, changed statement, different assumptions, stale source, or incompatible toolchain.
• The formal model is correct but does not faithfully represent the engineering object or deployed implementation.
• Exact finite facts are applied to approximate, floating-point, probabilistic, continuous, or adversarial behavior without a bridge.
• Canonicalization, hash coverage, collision policy, signatures, or trust roots omit a decision-relevant field.
• Replay checks a copied receipt instead of rebuilding, resolving, and recomputing from pinned sources.
• Generated fields, tolerances, nondeterminism, failed commands, or discarded attempts disappear behind a passing summary.
• Non-claims disappear in an appendix, summary, API conversion, cache, prompt, or downstream chapter.
• Consumer readiness, archive integrity, or transport success is mistaken for workload success, model quality, or deployment safety.
• A consumer broadens fact, use, claim axis, environment, version, or expiry beyond the gate.
• Baselines, controls, evaluator independence, or complete costs are waived because the structural proof is strong.
• Revocation or theorem drift fails to reach descendants, cached receipts, citations, releases, or private consumers.
• Fallback depends on the invalid envelope, is stale or rights-incompatible, or exceeds the recovery window.
• Producer, resolver, verifier, consumer, and trust root share one defect while appearing independent.
• Private results or inaccessible artifacts are implied by a public-safe receipt or acceptance record.
• A clean checkout, archived pack, fixture, or finite Lean bridge is described as deployed proof-contract transport.
• A narrow external rope result is generalized to all Circle contracts, substrates, real RoPE, model quality, safety, or transfer.
• Transport and governance cost exceed ambiguity reduction, but institutional commitment prevents retirement.

Theorem laundering should block support-state promotion. Stale theorem IDs should remain residuals until a resolver or external build confirms them. Missing baselines should prevent downstream adoption. Exact finite models should stay distinct from numerical diagnostics and real-valued deployment behavior.

Proof cargo-culting is the dangerous reader-facing failure: diagrams, theorem names, and receipt tables appear rigorous enough that the reader stops asking what the theorem actually says. The antidote is a consumer gate that states the exact downstream claim being blocked or allowed.

Receipts can also drift when the proof receipt remains attached after the contract fields it certified have changed.

67.11 Minimum Viable Implementation

The first transportable Circle artifact is a proof or contract record with theorem IDs, proof status, content fingerprint, deterministic fields, validation commands, consumer checks, ordinary baselines, and non-claims.

The current implementation has five public pieces. The proof_target_record fixture validates the record shape for proof targets. The proof_contract_receipt_record fixture validates the record shape for theorem-linked structural receipts, including receipt state, not-run resolver and replay states, fingerprint status, consumer state, staleness policy, source refs, support-state effect, and non-claims. The Lean module AsiStackProofs.ProofCarryingContracts implements finite-record predicates requiring theorem references, deterministic fields, and a non-claim boundary before downstream use, requiring workload, baseline, metric, and evidence artifacts before downstream promotion, and modeling the public Circle consumer-gate fixture as one valid receipt, four rejected mutation controls, seven required theorem IDs, pinned digest fields, blocked support movement, no chapter-core promotion, and no deployed-transport claim. The Circle public consumer-gate lane validates one pinned receipt fixture, checks seven theorem IDs and the recorded fingerprints, and rejects missing-theorem, digest-mismatch, stale-contract, and unsupported-transfer mutations. The Circle contract-pack archive validates a public-safe pack snapshot from Circle commit 63b0f511 with 9 archived contracts, 4 acceptance-policy receipts, pack fingerprint df673f8a661fc89a26372685986c92f2221aaa617d6738fce5c2a76bd5d0eeae, raw pack digest b5488c93109ef120b97fdea7bd5d5605f32b2618c6cbfb9dde9a3328652551c4, and no-promotion decision circle_contract_pack_archive_no_change.json.

The archive leaves the chapter core claim at argument, creates no support-state transition, and reruns no Circle Lean target. Its value is archive integrity and boundary discipline, not deployed transport, model quality, context length, runtime speed, memory scaling, deployment safety, transfer, safety, or ASI evidence.

The exact current minimum is therefore two schema-valid records; one external clean-checkout Circle rope slice with a narrow non-core argument-to-prototype-backed transition; one ASI-side consumer gate with one valid receipt and four rejected mutations but no core effect; one archive of nine contracts and four policy receipts with five rejected controls and a no-change decision; and ten local theorem declarations. It does not provide a general resolver built in this repo, producer-to-multiple-consumer service, authenticated transport, engineering-to-model refinement proof, descendant revocation, liveness, recovery, independent reproduction, downstream empirical benefit, or chapter-core transition.

67.12 Mature Research Target

In its finished form, Circle proof-carrying contracts act as a proof-contract transport service. It moves finite structural facts through the ASI Stack with theorem references, deterministic fields, fingerprints, resolver state, replay commands, consumer gates, and non-claims intact.

Proof-carrying AI contracts would become useful only when the receipt itself is precise enough to travel. A contract pack would bind an engineering object to a finite model, proof boundary, theorem references, proof status, source version, content fingerprint, deterministic fields, verifier command, resolver state, replay state, consumer gate, staleness policy, failure behavior, support-state effect, evidence refs, and explicit non-claims. Those fields make a proof receipt consumable without pretending it proves model quality, real-valued deployment behavior, runtime efficiency, or downstream usefulness.

The mature transport lane would separate receipt states from capability states. A theorem-linked, dictionary-bound, fingerprinted, resolver-checked, consumer-gated, workload-blocked, retired, or superseded receipt is a statement about proof transport, not a measured model result. Lean and proof manifests would expose proof status; CLI or Python tools would emit receipts and validation reports; memory, RoPE, cyclic mixer, and substrate chapters would consume structural receipts only through consumer gates. Stale theorem IDs would become residuals, fingerprint mismatches would block replay, consumer-gate failures would prevent downstream use, and workload-blocked receipts would preserve structural facts without quality promotion.

67.12.1 Argument-exit campaign

The mature test uses natural multi-consumer work rather than another authored receipt. Independent producers emit formal facts for several contract families; independently implemented resolvers and clean builders identify declarations, statements, assumptions, source versions, toolchains, and proof status; at least two consumers accept, refuse, cache, supersede, and revoke those facts through ordinary artifact infrastructure. Strong controls include signed manifests, plain hashes, schemas and type checks, conventional tests, SBOM or provenance attestations, and ordinary versioned APIs without theorem-linked transport.

The preregistration freezes source and toolchain matrices, trust roots, canonicalization, hash coverage, public-safe artifacts, theorem-model refinement obligations, consumer policies, mutation families, network and cache faults, expiry, revocation graph, fallback, recovery window, costs, and promotion rule. Measurements include unique-resolution and statement-match accuracy, semantic-refinement defect detection, false acceptance and refusal, clean-replay determinism, tamper and stale-proof detection, descendant revocation completeness, availability and liveness, fallback success, recovery time, latency, storage, compute, verifier and operator work, rights compliance, consumer misuse, and residuals. Failures and unavailable dependencies remain in the denominator.

Causal ablations remove theorem resolution, semantic refinement checks, canonical fingerprints, non-claim preservation, consumer specificity, authenticated provenance, expiry, descendant revocation, or replay while holding ordinary controls and resources fixed. Each proposed mechanism must produce its preregistered signature. Independent producer, resolver, verifier, and consumer implementations then reproduce the transport result across different theorem families, languages or provers, artifacts, organizations, rights regimes, attacks, and time. Downstream model quality, runtime, memory, safety, deployment, transfer, support, and SOTA remain separate campaigns even if transport succeeds.

The current book has not demonstrated that service. argument remains the right core state until natural multi-consumer transport clears semantic- refinement, strong-control, adversarial, cost, rights, revocation, liveness, recovery, causal, independent-reproduction, and heterogeneous-transfer gates. The honest terminal result may be qualified, narrowed, null, refuted, retired, or blocked after a competent full attempt.

67.13 Codex test plan

Test	Purpose	Status
Proof target record fixture validation	Validate that a proof target record names chapter, Lean tag, target kind, formal target, artifact refs, verifier command/result, support-state effect, limitations, and non-claims.	implemented; passing via python3 scripts/validate_protocol_examples.py
Proof contract receipt record fixture validation	Validate that a theorem-linked receipt record exposes receipt state, finite-model scope, proof boundary, theorem refs, proof status, fingerprint field/status, resolver/replay states, consumer gate/state, staleness policy, failure behavior, source refs, support-state effect, evidence references, and non-claims.	implemented; passing via python3 scripts/validate_protocol_examples.py
Circle public consumer-gate validation	Validate the pinned CC-AI-CONTRACT-ROPE-001 receipt boundary against the proof-contract receipt schema and reject digest-mismatch, missing-theorem, stale-contract, and unsupported-transfer mutations.	implemented; passing via python3 scripts/validate_circle_public_replay.py
Circle concrete receipt evidence-surface validation	Check that the concrete public-safe Circle facts remain visible in the Circle chapter and the outline while preserving chapter-core, model-quality, context-length, runtime, transfer, deployment, and ASI non-claims.	implemented; passing via python3 scripts/validate_circle_concrete_evidence_surface.py
Circle contract-pack archive validation	Validate the archived public-safe Circle contract-pack snapshot, acceptance-policy report, 9 archived contracts, 4 acceptance-policy receipts, public_safe_fixture status, pack fingerprint df673f8a661fc89a26372685986c92f2221aaa617d6738fce5c2a76bd5d0eeae, raw pack digest b5488c93109ef120b97fdea7bd5d5605f32b2618c6cbfb9dde9a3328652551c4, raw report digest f1671f5cecdee311185f7e4508b21c139d4ae4bd1fa9610a12827f4d31c7985a, and five expected-invalid controls while preserving circle_contract_pack_archive_no_change.json.	implemented; passing via python3 scripts/validate_circle_contract_pack_archive.py; does not promote any chapter core claim, does not create a support-state transition, does not rerun Circle Lean, and does not prove deployed proof-contract transport, model quality, context length, runtime speed, memory scaling, deployment safety, transfer, safety, or ASI
Circle public consumer-gate Lean fixture bridge	Model the public consumer-gate result as one valid receipt, four rejected mutation controls, seven required theorem IDs, pinned digest fields, blocked support movement, no chapter-core promotion, and no deployed-transport claim.	implemented; passing via cd lean && lake build
Versioned proof-contract lifecycle and descendant revocation	Recompile the 28-declaration Lean surface and independently check arbitrary-run custody, zero-authority and revocation coherence, all eight trace splits, 45 reachable states through 360 transitions, nine revoked-lineage states through 72 contained transitions, unrelated-lineage availability, 16 rejecting lifecycle mutations, and 15 semantic mutations.	implemented; passing via python3 scripts/validate_circle_contract_pack_archive.py; finite authored lifecycle only, with no external theorem resolution, semantic refinement, authenticated transport, deployed revocation, support transition, or chapter-core effect
Receipt boundary Lean predicate	Prove that a downstream-ready proof-carrying receipt exposes theorem references, deterministic fields, and an explicit non-claim boundary.	implemented in AsiStackProofs.ProofCarryingContracts; passing via cd lean && lake build
Consumer gate promotion predicate	Prove that contract readiness alone cannot promote a downstream claim when workload, baseline, metric, or evidence-artifact fields are missing.	implemented in AsiStackProofs.ProofCarryingContracts; passing via cd lean && lake build
Missing receipt-boundary negative case	Reject downstream-ready receipt status when theorem refs, deterministic fields, or non-claim boundary fields are missing.	implemented; passes via Lean negative case; no theorem-resolution or replay claim
Contract-readiness promotion negative case	Reject promoted downstream claims when the consumer gate would require contract readiness but the contract-ready field is false.	implemented; passes via Lean negative case; no consumer acceptance or quality claim
Stale or unsupported consumer-gate negative case	Reject consumer-gate acceptance when theorem refs are unresolved, fingerprints mismatch, the contract is stale, the consumer is disallowed, unsupported transfer is claimed, or non-claims are not preserved.	implemented; passes via Lean negative case; no transfer or support-state claim
Replay artifact negative case	Reject passing replay status when replay command, source digest, receipt fingerprint, recomputed deterministic fields, or theorem refs are missing.	implemented; passes via Lean negative case; no replay execution claim
Contract schema validation test	Validate a Circle-specific contract pack with theorem refs, deterministic fields, verifier commands, consumer gates, and explicit non-claims.	partly implemented by the archived pack validator; full theorem-id resolution and clean replay remain planned
Theorem-id resolution test	Resolve each theorem ID to a compiled declaration or block downstream proof-backed use when a reference is missing.	planned; not run
Non-claim preservation test	Check that summaries and consumers preserve the non-claim boundary in text and records rather than treating readiness as proof of workload performance.	planned; not run
Receipt replay and fingerprint test	Replay the receipt, recompute fingerprints, and fail the contract when content, theorem refs, or deterministic fields diverge.	planned; not run

The implemented rows validate fixture/schema consistency, the ASI-side public Circle consumer gate, and local finite-record Lean predicates only. The remaining rows require Circle contract artifacts or a local surrogate with theorem IDs, receipts, fingerprints, replay commands, and explicit non-claims; they are not reported results. When a stronger contract test is implemented, the Circle chapter should link to the command, fixture, environment notes, artifact pack, and result summary, and Appendix E should be regenerated or updated accordingly.

67.13.1 Formalization hooks

Tag	Module	Target	Status
lean:circle_contracts.receipt_requires_boundary.operational_invariant	AsiStackProofs.ProofCarryingContracts	A finite proof-contract receipt missing theorem references, deterministic fields, or an explicit non-claim boundary is rejected from downstream use.	implemented
lean:circle_contracts.consumer_gate.failure_blocks_promotion	AsiStackProofs.ProofCarryingContracts	A downstream claim cannot be promoted solely from contract readiness without a workload, baseline, metric, and evidence artifact.	implemented
lean:circle_contracts.public_consumer_gate.fixture_bridge	AsiStackProofs.ProofCarryingContracts	Any record satisfying the finite Circle public-consumer acceptance contract loses acceptance when promotion/deployed-transport overclaims or required mutation-control rejections are present; an independent replay validator separately computes one valid receipt and four invalid controls.	implemented
lean:circle_contracts.versioned_transport.descendant_revocation	AsiStackProofs.ProofCarryingContracts	The finite versioned transport state machine preserves theorem, parent, consumer, support, and external-effect custody plus zero-authority and revocation coherence across arbitrary event lists; rejects invalid events without state change; composes traces; confines revoked descendants across arbitrary suffixes; and preserves unrelated-lineage availability.	implemented

The first three Lean hooks remain local finite-record predicates over receipt, consumer-gate, and replay records. The fourth adds explicit lifecycle semantics: every finite event list preserves eight theorem, parent, and consumer identity fields plus zero support and external-effect authority; accepted transitions preserve revocation coherence; rejected events preserve the exact state; root revocation confines descendant use through every later suffix; and unrelated-lineage availability survives arbitrary suffixes. The independent Python consumer recompiles the exact module, reconstructs the seven-transition reference trace, checks all eight append splits, explores 45 reachable states through 360 transitions, checks 72 transitions from nine revoked-lineage states, and rejects 16 lifecycle mutations plus 15 semantic mutations.

The 28 declarations prove only the authored finite transition system. Digest equality is an input, not evidence that a theorem resolved correctly. The model does not establish statement equivalence, semantic refinement, authentic signatures, complete dependency closure, real cache invalidation, concurrent or distributed revocation, service liveness, recovery, Circle theorem validity, downstream utility, independent reproduction, or transfer. It does not approve a support transition or chapter-core promotion.

The module contains 28 theorem declarations. Seven retained declarations cover receipt boundaries, downstream promotion separation, replay prerequisites, and public-gate overclaim controls. Twenty-one lifecycle declarations add rejected-event noninterference, protected identity and authority fields, trace composition, arbitrary-run custody and zero-authority invariants, descendant invalidation, persistent revocation and suffix containment, a reachable consume-then-revoke witness, post-revocation rejection, arbitrary-run unrelated-lineage availability, and exact identity and parent-link countermodels. This is a stronger local contract model, not proof of unique theorem resolution, statement equivalence, semantic correspondence, implementation refinement, authenticated transport, deployed revocation, liveness, recovery, independent reproduction, downstream utility, or transfer.

67.14 Source crosswalk

Source ID	Title	Layer	Planned use	Readiness
circle_calculus_core	Circle Calculus	proof_carrying_mathematical_substrate	Proof-carrying finite cyclic mathematics project with Lean proofs, Python reference models, Rust utilities, theorem manifests, papers, and Quarto living book.	source note available
circle_ai_contract_suite	Circle Calculus AI Contract Suite	proof_carrying_ai_contracts	Theorem-linked AI contract families for RoPE, KV-cache freshness, sparse attention, recurrence schedules, strided fanout, cyclic memory, multicoil phase, cyclic mixers, and seed-rule regeneration.	source note available
rope_position_certifier	Proof-Carrying RoPE Position Distinguishability	proof_carrying_position_contract	Externally usable RoPE position-distinguishability certifier with theorem-linked exact collision reports, bounded real-phase frontier, machine-readable receipts, and explicit non-claims.	source note available
proof_carrying_circular_computation	Proof-Carrying Circular Computation	proof_carrying_compute_substrate	CoilIR-style path from circle/coil expressions to dictionary-recognized cyclic structure, Lean-proved rewrite/address transformations, backend selection, and benchmark validation.	source note available
circle_ai_architectures	Circle AI Architectures	cyclic_ai_architecture	Disciplined Circle AI thesis: use phase, recurrence, rotation, sparse cyclic mixing, circular memory, harmonic transforms, or geometry-aware structure only where the structure is real and baselines support it.	source note available

The crosswalk preserves external proof authority. circle_calculus_core supplies proof-status discipline, circle_ai_contract_suite supplies contract families and consumer fields, rope_position_certifier supplies the exact/discretized RoPE boundary, proof_carrying_circular_computation supplies cyclic-address compute lineage, and circle_ai_architectures supplies the anti-overclaim rule. None of these source notes converts structural proof into model-quality evidence.

67.15 Summary

Circle Calculus and proof-carrying AI contracts let finite structural facts travel with theorem IDs, receipts, fingerprints, validation commands, and non-claims. Their job is boundary preservation.

The ASI Stack should consume those contracts as structural guardrails, not as model-quality evidence. Downstream promotion still requires workloads, ordinary baselines, negative controls, metrics, and replayable result artifacts. The same receipt boundary applies to memory and recurrence, where the central risk is mistaking slot coverage for semantic adequacy.

A proof receipt should make overclaiming harder. If a receipt makes it easier to sell a substrate result that was not tested, the contract boundary failed. The constructive path is still powerful: finite structural predicates can become machine-checkable attachments for plans, memory layouts, routing decisions, or substrate candidates. Those attachments can reduce ambiguity, prevent category errors, and give reviewers something precise to inspect. They simply do not replace ordinary evaluation. The proof-carrying contract is therefore a disciplined interface between formal structure and empirical adoption, not a shortcut around evidence.

67.16 Evidence reconciliation (2026-07-16)

The invariant protocol, field meanings, and inference limits are stated once in Living Book Methodology. This packet contains only the chapter-specific projection; its authoritative per-atom rows are the circle-calculus-and-proof-carrying-ai-contracts slice of experiments/claim_family_terminal_coverage/results/result.json.

The core remains blocked after full attempt at argument support. The strongest family attempt was KERC canonical-language and hierarchical-residual campaign. Its exact boundary is: The historical broad-efficiency transition is N1: the frozen implementation was inadequate, so broader KERC remains untested; two narrow finite observations survive, with no semantic, multilingual, production, energy, or core claim. Across 74 atoms, the terminal ledger records 73 blocked_after_full_attempt; 1 promoted_at_bounded_scope.

Chapter-specific field	Value
Family / atom denominator	CF-06 / 74 atoms
Terminal dispositions	73 blocked_after_full_attempt; 1 promoted_at_bounded_scope
Core	circle-calculus-and-proof-carrying-ai-contracts.core: blocked_after_full_attempt at argument
Core attempted / missing lanes	causal, empirical, executable, formal, source-synthesis / normative, transfer
Attempted local lanes	causal, empirical, executable, formal, source-synthesis
Missing or unproved lanes	normative, transfer
Strongest family bundle	KERC canonical-language and hierarchical-residual campaign (natural_work_and_end_to_end): A 192-record bilingual templated compiler/runtime study with 64 held-out records, five seeds, eight baseline families, 13 ablations, and 20 attacks.
Negative controls	surface and kernel-native baselines; 13 ablations; 20 attacks; ten laundering mutations.
Accepted transitions	post_v2_3.p5.circle_named_target_receipt.promote
Maximum inference	The historical broad-efficiency transition is N1: the frozen implementation was inadequate, so broader KERC remains untested; two narrow finite observations survive, with no semantic, multilingual, production, energy, or core claim.
Reproduction / next burden	Replay scripts/validate_p4_m8_kerc_campaign.py and scripts/validate_claim_family_terminal_program.py; fill the named atom-specific lanes under a new prospective protocol.

67.17 Handoff

Proof-carrying contracts are most useful when they protect a concrete boundary rather than decorate an abstract idea. Coil Attention, Cyclic Memory, and Recurrence Contracts applies that rule to memory and recurrence. It asks which slot, winding, freshness, coverage, active-work, loop-exit, stale-read, and fallback facts can be checked structurally while preserving the non-claim that retrieval and reasoning quality remain unproven.