Use This As A Library

Claim boundary proved finite facts executable receipts benchmarks separate no model-quality claim

This is the shortest public path for using Circle Calculus as code. The stable facades are:

Finite Circle Orbit

from circle_math.core import finite_orbit, finite_period, is_full_coil

orbit = finite_orbit(12, 5)
period = finite_period(12, 5)
full = is_full_coil(12, 5)

print(orbit)
print(period)
print(full)

Expected output:

[0, 5, 10, 3, 8, 1, 6, 11, 4, 9, 2, 7]
12
True

Finite Fourier And Circulant Algebra

from circle_math.core import (
    circular_convolution,
    spectral_aliasing_report,
    spectral_convolution_report,
)

signal = [1, 2, 0, -1]
kernel = [2, 0, 1, 0]

print(circular_convolution(kernel, signal))
print(spectral_convolution_report(kernel, signal).passed)
print(spectral_aliasing_report(4, [-1, 0, 3, 4, 7]))

The Lean layer proves the finite character, shift, and circulant convolution identities in Circle.Core.FiniteFourier and Circle.Applications.CirculantSpectral. The Python residual check is an executable floating-point diagnostic.

Position Phase Bank

from circle_math.ai_contracts import (
    phase_bank_collision_report,
    phase_bank_from_periods,
)

bank = phase_bank_from_periods("diagnostic", [6, 9, 13])
report = phase_bank_collision_report(bank, 0, 36)

print(report.all_channels_collide)
print(report.witness_channels)
print([row.period_divides_gap for row in report.channel_results])

Expected output:

False
('phase_2',)
[True, True, False]

The Lean layer proves the integer residue/divisibility contract in Circle.Applications.PositionPhase. This does not prove real-valued RoPE-family margins or model-quality claims.

Circle Graph Coverage

from circle_math.ai_contracts import circle_graph_coverage_report

report = circle_graph_coverage_report(
    context=9,
    strides=(3, 4, 7),
    path_length=2,
    local_window=2,
)

print(report.coverage_complete)
print(report.uncovered_lags)
print(report.directed_edge_count)

Expected output:

True
()
72

The Lean layer proves the finite direct-lag coverage contract in Circle.Applications.CircleGraphCoverage. This does not prove sparse-attention quality, speed, or memory savings.

Circular Statistics

from math import tau

from circle_math.core import (
    circular_mean_report,
    finite_residue_histogram,
    finite_wrapped_distance,
)

print(finite_wrapped_distance(12, 1, 11))
print(finite_residue_histogram(5, [0, 5, 7, 12], include_zero_counts=True))

report = circular_mean_report([0.0, tau / 4.0])
print(report.mean_angle)
print(report.mean_resultant_length)
print(report.undefined_mean)

The Lean layer proves finite residue, same-phase, wrapped-distance, and histogram contracts in Circle.Applications.CircularStatistics. The real-valued circular mean/resultant fields are executable diagnostics, not statistical-quality or numerical-stability claims.

Cyclic Equivariance

from circle_math.core import (
    circulant_equivariance_report,
    cyclic_sum_invariance_report,
    dihedral_transform,
)

print(dihedral_transform([10, 20, 30, 40], shift=1, reflected=True))

report = circulant_equivariance_report(
    [2, 0, 1, 0],
    [[1, 2, 0, -1], [0, 3, 1, 2]],
)
print(report.passed)
print(report.max_abs_delta)

pooling = cyclic_sum_invariance_report([[1, 2, 3, 4]])
print(pooling.passed)

The Lean layer proves finite cyclic-shift laws, circulant-layer equivariance, sum-pooling invariance, and minimal reflection laws in Circle.Applications.CyclicEquivariance. It does not prove continuous rotation equivariance, robustness, or model-quality improvements.

Phase Loop And Locking

from circle_math.core import phase_lock_report, phase_loop_report

loop = phase_loop_report(12, [3, 4, 7], base_gauge=5)
print(loop.charge)
print(loop.reverse_charge)
print(loop.charge_plus_reverse)
print(loop.closed_loop_gauge_invariant)

locked = phase_lock_report(12, [1, 13, 25])
print(locked.all_locked)
print(locked.order_parameter)

The Lean layer proves finite modular loop-charge, reverse-charge, closed-loop gauge cancellation, phase-locking, and winding reconstruction facts in Circle.Applications.PhaseLoop. It does not prove Kuramoto stability, synchronization thresholds, continuum vortices, quantum holonomy, or physics claims.

RoPE Contract Receipt

from circle_math.ai_contracts import build_contract_pack, build_rope_receipt

pack = build_contract_pack()
receipt = build_rope_receipt(
    head_dim=128,
    base=10000,
    context=4096,
    requested_margin="1/328459",
    pack=pack,
)

print(receipt["contract_id"])
print(receipt["decision"]["verdict"])
print(receipt["decision"]["claim_status"])
print(receipt["decision"]["all_theorem_ids_proved"])
print(receipt["evidence"]["standard_channel0_d19_bank_bridge"]["applies"])

The receipt is a theorem-linked structural certificate for the declared request. Here the D19 first-channel bank bridge is the theorem-backed payload that makes the smaller-context request pass. It is conditional on the standard channel-0 first-frequency bank shape, and it is not a language-model quality, speed, memory, or deployment-safety result.

Sparse-Attention Coverage Contract

from circle_math.ai_contracts import (
    build_contract_pack,
    build_sparse_attention_receipt,
)

pack = build_contract_pack()
receipt = build_sparse_attention_receipt(
    context=9,
    strides=(3, 4, 7),
    path_length=2,
    local_window=2,
    pack=pack,
)

print(receipt["contract_id"])
print(receipt["decision"]["verdict"])
print(receipt["evidence"]["coverage_complete"])
print(receipt["evidence"]["uncovered_lag_count"])

The compact fixture is a complete finite coverage example. To inspect a gap certificate instead, use context=120, strides=(7, 13), path_length=3, and local_window=4.

CLI Entry Points

After installing the package in editable mode:

python -m pip install -e .
circle-ai-certify rope --model-config-file examples/circle_ai_model_configs/standard_rope_config.json --request-out /tmp/circle_rope_request.json --request-validation-report-out /tmp/circle_rope_request_validation.json --model-config-import-report-out /tmp/circle_rope_import_report.json --format json
circle-ai-certify kv-cache --cache-size 16 --current 31 --token 20 --batch-tokens 20,24,29,31 --sink-size 4 --require-passed --format json
circle-ai-certify sparse-attention --context 9 --strides 3,4,7 --path-length 2 --local-window 2 --format json
circle-ai-certify sparse-attention --context 9 --strides 3,4,7 --path-length 2 --local-window 2 --format compact-json
circle-ai-certify recurrence --format json
circle-ai-certify strided-fanout --format compact-json
circle-ai-certify cyclic-memory --format compact-json
circle-ai-certify multicoil-phase --format compact-json
circle-ai-certify cyclic-mixer --format compact-json
circle-ai-certify seed-rule --format compact-json
circle-ai-contract-ready --kind sparse_attention_coverage
circle-ai-contract-receipt --kind rope --model-config-file examples/circle_ai_model_configs/standard_rope_config.json
circle-ai-contract-receipt --request-file examples/circle_ai_requests/kv_cache_request.json --request-out /tmp/circle_kv_request.json --require-passed --require-status proved --require-decision passed
circle-ai-contract-receipt --kind sparse-attention --parameters '{"context": 9, "strides": [3, 4, 7], "path_length": 2, "local_window": 2}'
circle-rope-certify --preset llama_style_10000_4k
circle-sparse-attention-certify --context 9 --strides 3,4,7 --path-length 2 --local-window 2

circle-ai-certify is the guided installed command for normal downstream receipts. The richer repository maintenance commands under scripts/ remain the source tools for generating and validating every audit artifact. Installed wheels carry a generated theorem-status snapshot under circle_math/data/generated/theorem_status_index.json, so contract readiness can still resolve theorem ids when the repository manifests/ directory is not present.

For RoPE model configs, add --request-out and --request-validation-report-out when you want the exact Circle request and its schema-validated preflight report saved beside the receipt. Add --model-config-import-report-out for the parameter-source audit report. For KV-cache, sparse attention, recurrence, strided-fanout, cyclic-memory, multicoil-phase, cyclic-mixer, seed-rule, and already-normalized RoPE requests, use --request-file with a circle_calculus.ai_contract_request.v0 JSON object. Use --require-passed, --require-status, --require-decision, and --require-assurance when the command should fail CI unless the emitted receipt satisfies a narrow acceptance policy. Use --gate-report-out, --receipt-check-out, and --receipt-replay-check-out when CI should save compact machine-readable receipt diagnostics without using repository-only scripts. Use --format compact-json or --compact-json-out when another project only needs the stable receipt decision, selected evidence, theorem summary, replay commands, non-claims, and the full receipt fingerprint. Use --certification-bundle-out with --certification-bundle-check-out when the installed CLI should also archive a request-validation, receipt, gate, and bundle-check handoff object. Use --artifact-manifest-out with --artifact-manifest-check-out when it should also fingerprint the sidecar files and verify the manifest. Use --artifact-dir when it should choose stable names for the full sidecar set automatically.

Non-default rope_scaling values are rejected by this standard-RoPE importer until there is separate theorem coverage for the scaled variant.

Lean Imports

import Circle.Core
import Circle.Contracts

Use Circle.Applications.Public when you want application facts without the large generated RoPE certificate module.

Rust Prime Engine

cargo run -p circle-prime -- --help
cargo run -p circle-prime --bin circle-prime-count -- --help
cargo doc -p circle-prime --no-deps

The Rust crate stays focused on prime decisions, prime counts, and horizon/coil inspection. It does not contain the Lean theorem corpus or the Python reference models.