RoPE Proof Audit

This appendix is the proof audit trail for the RoPE Certifier lesson. The lesson explains the contract; this page keeps the proof-status map and source trail close without forcing every reader through a long theorem-card wall.

The theorem cards below are still summaries, not proof artifacts and not model-quality claims. The generated Theorem Index, theorem manifests, and Lean declarations remain the source of proof status.

Audit Route

Use this order when checking a RoPE claim:

  1. Read the report field in the Python or sidecar output.
  2. Match the field to a theorem family below.
  3. Open the theorem card and verify the Lean declaration name.
  4. Follow the Lean source link from the card.
  5. Check the exact non-claim boundary in the lesson or paper.
Claim family Use it when checking Theorem-card section
Exact integer phase-bank exact_discrete_contract, common_collision_gap, and all-channel collision pass/fail. Discrete Phase-Bank Contract
Prefix/subfamily/count reports first_exact_pass_prefix_length, sufficient subbanks, and collision-count fields. Prefix, Subfamily, And Count Reports
Real-phase finite reduction Nearest-integer gap predicates and finite generated-gap checks. Real-Phase Reduction
Rational exact-margin certificates Discretized 1/d turn-ratio certificates and request thresholds. Rational Exact-Margin Certificates
Standard channel-0 frontier D19 channel-0 interval certificates and request classifier fields. Standard Channel-0 Frontier

Discrete Phase-Bank Contract

These cards are the finite integer-period layer: residue collision, period-bank collision, LCM pass/fail, and count semantics.

Prefix, Subfamily, And Count Reports

These cards support prefix/subfamily no-collision reports and finite collision-count fields. They are exact for declared positive integer-period banks, not real-valued RoPE quality claims.

Real-Phase Reduction

These cards are the nearest-integer bridge: they reduce one-channel real-phase separation to finite turn-ratio margin predicates and exact weakest-gap reports.

Rational Exact-Margin Certificates

These cards cover the named rational/discretized preset and the reduced-rational exact weakest-gap threshold family. They do not prove the irrational standard RoPE bank theorem.

Standard Channel-0 Frontier

These cards are the current standard-channel frontier. The proved seed is channel-0 based and conditionally transfers to a bank when that channel is present.

Source Trail

Paper source: Proof-Carrying RoPE Position Distinguishability

Lean source: Circle/Applications/RoPECertifier.lean

Python source: circle_math/applications/rope_certifier.py

Generated result fixture: rope_certifier_presets.md

Back: RoPE Certifier Next: KV-Cache Ring Buffer