RoPE Certifier

This lesson is the first standalone Circle Calculus AI contract meant for an ML engineer who does not know Lean.

The question is narrow:

Given a RoPE-like position configuration, can this declared phase bank distinguish positions in the inspected context?

The formal answer starts with an exact discretized model. Each channel has an integer period, and a position is represented by its residue modulo that period. The real-phase program also has theorem-backed finite-margin examples: a rational/discretized 1/4099 preset, a bounded standard-RoPE channel-0 interval seed, and a conditional bank bridge when that channel is present. Model-scale real-valued RoPE phases are still scanned numerically, and that margin report is not a formal proof.

Goal

Learn how the certifier turns RoPE position indistinguishability into a finite divisibility check, then inspect a configuration with the browser widget or Python CLI.

Reading Path

Read this chapter in four passes:

The discrete contract: learn why integer-period phase-bank collisions reduce to divisibility by a common gap.
The executable report: run the widget or CLI and read exact_discrete_contract, common_collision_gap, and total_bank_collision_pair_count before looking at any other field.
The real-phase boundary: separate theorem-backed finite-margin certificates from numerical scans.
The theorem cards: use the cards as the proof-status index after the ideas and report fields make sense.

The Contract

For one integer-period channel:

phase(period, position) = position mod period

For a finite bank of periods, two ordered positions collide exactly when every declared period divides the position gap:

bank_collision(left, right)
iff
forall period in periods:
  period divides (right - left)

That is the main theorem-backed contract. The Python and browser certifiers compute the common collision gap implied by the declared integer periods. If that gap is at least the context length, no unequal pair inside the inspected context collides in every discrete channel.

The widget output is an explanation and executable check. It is not proof by itself. The proof source is the Lean declaration named by the theorem card.

A Tiny Hand Check

Before reading a full report, do the smallest version by hand. Suppose the declared phase bank has periods:

6, 9, 13, 18

The first all-channel repeat gap is the least common multiple:

lcm(6, 9, 13, 18) = 234

If the inspected context is 128, then no unequal positions inside 0..127 can be exactly 234 apart. So the exact discrete contract passes for that context.

Now change the bank to:

32, 48, 96

The least common multiple is 96. In context 256, the repeat gaps 96 and 192 both fit. That creates theorem-backed collisions:

0 and 96
1 and 97
...
159 and 255

for the first gap, plus the shorter list at gap 192. The certifier reports 224 total ordered all-channel collision pairs for this declared integer-period bank. The theorem content is the reason this scales: Lean proves that checking every pair is equivalent to checking whether the LCM gap fits in the context.

Python CLI

Use the public certifier from the repository root:

python scripts/rope_certify.py --head-dim 128 --base 10000 --context 32768 --tolerance 1e-6

Named public-safe presets:

python scripts/rope_certify.py --preset llama_style_10000_4k
python scripts/rope_certify.py --preset llama_style_10000_128k
python scripts/rope_certify.py --preset llama_style_500000_128k

Diagnostic exact-discrete failure presets:

python scripts/rope_certify.py --preset diagnostic_single_channel_10000_20
python scripts/rope_certify.py --preset diagnostic_two_channel_36_128
python scripts/rope_certify.py --preset diagnostic_prefix_pass_4_128
python scripts/rope_certify.py --preset diagnostic_shared_factor_25_64

For machine-readable output:

python scripts/rope_certify.py --preset llama_style_10000_4k --format json

The JSON report includes theorem ids, Lean declarations, assumptions, exact discrete pass/fail, bounded prefix collision reports, sample exact collisions when present, and numerical real-phase margin diagnostics.

For an explicit integer phase bank that is not derived from a RoPE base/head-dimension pair:

python scripts/phase_bank_certify.py --periods 6,9,13,18 --context 128
python scripts/phase_bank_certify.py --preset quantized_shared_factor_256
python scripts/phase_bank_certify.py --preset quantized_lcm_boundary_fail_241
python scripts/phase_bank_certify.py --preset interpolated_x4_boundary_pass_960
python scripts/phase_bank_certify.py --preset interpolated_x4_boundary_fail_961

That exact-only path emits theorem-linked discrete certificate fields without a real-phase margin section.

How To Read One Report

Start with the exact discrete layer. It is the part whose pass/fail result is backed by Lean for the declared integer-period phase bank.

exact_discrete_contract=PASS
common_collision_gap=>= context
total_bank_collision_pair_count=0
theorem_ids=...

Read those fields in this order:

exact_discrete_contract says whether the declared integer-period bank distinguishes every unequal ordered position pair in the inspected context.
common_collision_gap is the least all-channel repeated gap implied by the period-bank LCM. If it is >= context, no repeated all-channel gap fits inside the inspected range.
total_bank_collision_pair_count counts all ordered all-channel colliding pairs for the declared integer-period bank. It is theorem-backed count evidence, not a sampled diagnostic.
theorem_ids tells you which manifest entries and Lean declarations justify the exact layer. The browser theorem cards below resolve those ids to proof status and source links.

Detailed exact-discrete proof trail

AIRA-T0179 proves that the positive-period input policy gives the positive LCM required by these count theorems. AIRA-T0180 proves the exact pass/fail iff: no unequal all-channel collision in the inspected context exactly when that LCM reaches the context. AIRA-T0184 proves that this boolean no-collision contract is equivalent to total_bank_collision_pair_count = 0. AIRA-T0174 and AIRA-T0175 prove the zero boundary: under a positive LCM, this count is zero exactly in the LCM-reaches-context pass case. AIRA-T0176 proves the nonzero case is equivalent to the existence of an unequal all-channel collision witness.

If the exact layer fails, the same fields become a debugging guide:

exact_discrete_contract=FAIL
common_collision_gap=96
total_bank_collision_pair_count=224
sample_collision_pairs=(0,96),(1,97),...

That says the declared bank repeats after gap 96, and the report lists actual position pairs that collide in every declared discrete channel. It still does not say the real-valued model fails; it says the exact integer-period contract for the declared bank fails.

The real-phase row is separate. It is useful evidence about the floating-point RoPE schedule, but this page only treats it as a theorem-backed result when it points to a named finite-margin certificate or standard channel-0 interval seed.

What This Proves, And What It Does Not

Layer	Status	Reader Takeaway
Declared integer-period phase bank	Lean-proved for the theorem ids in the exact layer	The pass/fail/count fields are exact for the periods stated in the report.
Rational finite-margin examples	Lean-proved when the report points to a named certificate	The finite nearest-integer certificate is a formal proof for that declared rational ratio and context.
Standard channel-0 D19 frontier	Lean-proved, conditional, one-channel based	Inside the D19 range, requests are classified as proved, impossible, or deliberately undecided for the stated channel-0 margin contract.
Full real-valued all-channel model behavior	Not proved here	Numerical rows are engineering diagnostics unless backed by a named theorem id and compiled Lean declaration.
Model quality or long-context performance	Not claimed	The certifier checks phase distinguishability contracts; it does not prove lower loss, better reasoning, speed, safety, or deployment fitness.

Proof Map

The main lesson uses only the proof families needed to read a report. The full audit page keeps the longer theorem-card trail.

Report layer	What the reader should trust	Primary theorem ids
Exact integer-period bank	All-channel collisions are exactly common LCM gaps, and the pass/fail/count fields are exact for the declared periods.	`AIRA-T0024`, `AIRA-T0179`, `AIRA-T0180`, `AIRA-T0184`
Prefix and subfamily reports	A passing prefix or contained subbank is enough to certify the whole declared integer-period bank.	`AIRA-T0051`, `AIRA-T0052`, `AIRA-T0190`, `AIRA-T0194`
Real-phase reduction	One-channel real phase margin reduces to finite generated gaps and nearest-integer floor/ceiling witnesses.	`AIRA-T0041`, `AIRA-T0054`, `AIRA-T0059`, `AIRA-T0183`
Exact finite-margin certificates	A named weakest-gap certificate can prove or reject a requested margin for rational/discretized ratios.	`AIRA-T0214`, `AIRA-T0215`, `AIRA-T0230`, `AIRA-T0231`
Standard channel-0 frontier	The current proved standard-channel frontier reaches D19; it is conditional and one-channel based.	`AIRA-T0139`, `AIRA-T0173`, `AIRA-T0208`, `AIRA-T0217`

ML-Engineer Quickstart

The short non-Lean entrypoint is RoPE Certifier Quickstart. It covers installation, presets, custom configs, text and JSON output, theorem ids, and limitations.

For the shortest current findings summary, read the RoPE Certifier Results Note. It is the compact bridge between the preset table, the D19 one-channel real-phase frontier, the reproduction commands, and the non-claims.

Reproducible Results

The paper sidecar generates the current preset results:

python sidecars/PAPER_AI_04_ROPE_POSITION_CERTIFIER/python/benchmark_rope_certifier.py --format markdown

Committed fixtures:

Preset JSON: rope_certifier_presets.json

Preset Markdown: rope_certifier_presets.md

The model-like presets pass the exact discrete contract under the rounded integer-period phase-bank model. The diagnostic presets include intentional failures and a prefix-pass case so the sample-collision, theorem-backed count, shared-factor, and prefix fields are visible. The exact phase-bank diagnostics include quantized shared-factor cases and interpolation-style scaled-period boundary cases. The sidecar JSON uses compact summaries for readability; the CLI can still emit the full nested certificate. The real-phase rows are numerical diagnostics only.

Reading The Current Results

The committed sidecar results are meant to be read as contract evidence, not as benchmark wins. A PASS in the exact column means the declared integer-period phase bank has no unequal all-channel collision inside the inspected context. A FAIL gives a theorem-backed common collision gap and collision count for that declared model.

Preset	Context	Exact Discrete Contract	Main Evidence	Real-Phase Row
`llama_style_10000_4k`	4096	PASS	common gap is outside context; first reported prefix already passes at length `5`; the D19 one-channel standard seed covers this request through the 192k proved horizon	numerical scan PASS
`llama_style_10000_128k`	131072	PASS	common gap is outside context; first reported prefix already passes at length `8`; the exact result is still the rounded integer-period model, while the separate real-phase proof layer is one-channel/conditional	numerical scan PASS
`llama_style_500000_128k`	131072	PASS	common gap is outside context; bounded subfamily report finds a sufficient subbank; prefix search does not find a passing prefix in the bounded report; exact result is still the rounded integer-period model	numerical scan PASS
`diagnostic_single_channel_10000_20`	20	FAIL	common gap `6`; exact integer-bank collision-pair count `24`	numerical scan PASS
`diagnostic_two_channel_36_128`	128	FAIL	common gap `114`; exact integer-bank collision-pair count `14`	numerical scan PASS
`diagnostic_shared_factor_25_64`	64	FAIL	common gap `54`; exact integer-bank collision-pair count `10`	numerical scan PASS

The most important distinction is that the first three rows are exact only after the real-valued RoPE schedule has been converted into the declared integer periods used by the certifier. The numerical real-phase scan is reported beside the proof-carrying discrete contract because it is useful engineering evidence, but this page does not call it a proof.

For genuine standard channel 0, the Lean-proved margin currently reaches context 196608 at margin 1/328459. The exact-rational planner and generated Lean certificate route still prove the sharper 32k and 64k rows at margin 1/104219; the stronger 128k request at that same margin fails at gap 103993. The important user-facing result is the D19 classifier: at context 131072, margin 1/328459 is proved, margin 1/328458 is impossible, and the exact open interval of width 1/107884986222 between those thresholds remains deliberately undecided. Lean also proves that every in-range request falls into exactly one of those semantic branches. The general Dirichlet guardrails AIRA-T0239 through AIRA-T0241 add the opposite kind of information: every nontrivial finite context has some in-context gap with nearest-integer error at most 1/context, any advertised margin strictly above 1/context is impossible, and any exact weakest-gap margin report is itself bounded by that same ceiling.

Detailed D19 proof route

The proved AIRA-T0139 through AIRA-T0141 bridge says how a generated rational-band list can become a Lean interval certificate without expanding every gap into a separate case; AIRA-T0142 through AIRA-T0173 are the generated 32k/64k/128k/160k/192k certificates, bridges, and endpoint brackets built on that route. AIRA-T0209 gives the generic context-range bracket from one certified horizon plus one obstruction gap, and AIRA-T0208 specializes it to D19 for every 103993 < context <= 196608. AIRA-T0216 and AIRA-T0217 turn that bracket into the request classifier: margins at or below 1/328459 are proved, margins at or above 1/328458 are rejected, and the open gap between them remains undecided. AIRA-T0218 and AIRA-T0219 add the classifier consistency guard: the thresholds are ordered, and the proved/impossible branches cannot overlap. AIRA-T0220 and AIRA-T0221 make the remaining status exact: the undecided status is precisely the open interval between the thresholds, and every requested margin falls into proved, impossible, or that open interval. AIRA-T0233 strengthens the report semantics by proving that every in-range request is in exactly one branch: proved with a finite-margin proof, impossible with a finite-margin refutation, or the deliberate undecided gap. AIRA-T0232 proves the exact rational width of that open interval, matching the public undecided_margin_interval_width field, AIRA-T0238 proves the public 2/656917 undecided probe lies inside that open gap, AIRA-T0239 imports Dirichlet’s approximation theorem as a general finite-context upper-bound guardrail, AIRA-T0240 turns that guardrail into a direct impossibility theorem for requested margins above 1/context, and AIRA-T0241 applies the same ceiling to exact weakest-gap report objects. The generated table now proves coverage by checking one contiguous gap chain, checks endpoints on compact uniform rows, and then derives ordinary band coverage and validity by generic Lean bridges.

The public Circle AI contract pack exports three D19 classifier probes at context 131072: margin 1/328459 has status proved, margin 1/328458 has status impossible, and margin 2/656917 has status undecided_margin_gap. The same record now exposes requested_margin_relation labels, the exact undecided interval width 1/107884986222, d19_undecided_probe_margin_in_open_gap, d19_in_range_semantic_trichotomy, and the proved-branch first-channel context-wide bank-transfer fields, giving downstream tools a theorem-backed frontier check without requiring them to import Lean.

Downstream D19 planner and receipt commands

For downstream AI tools, the compact digest also exposes two copy-safe planner records:

python scripts/circle_ai_contract_ready.py \
  --kind rope_position_distinguishability \
  --digest \
  --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

For CI, use the strict receipt form when a downstream project must pin the first-channel bank-transfer payload and the AIRA-T0234 through AIRA-T0241 theorem ids:

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

ROPE-AUDIT-EXACT-INTEGER-PHASE-BANK points a consumer to the declared integer-period phase-bank collision audit. ROPE-USE-D19-MARGIN-FRONTIER points a consumer to the D19 standard-channel-0 margin frontier. The flagship acceptance policy pins both records, so downstream consumers preserve the exact discrete collision audit alongside the D19 request frontier. They are planner/audit records over theorem-backed fields, not claims that a real model gets longer context, lower loss, or full all-channel real-RoPE guarantees.

Checkpoint

In the exact discrete model, which field tells you whether the first repeated all-channel position gap is inside the inspected context?
Why can the llama_style_10000_128k row be exact for its declared integer-period bank without proving a full all-channel real-valued 128k RoPE theorem?
In a failure row, what is the difference between a common collision gap and the total integer-bank collision-pair count?

Real-Phase Proof Front

The exact integer-period contract is already complete enough to use for declared discrete phase banks. Real-valued RoPE needs a different theorem shape because the channel angle usually does not have an exact integer period.

The current real-phase program proves this reduction:

real phase error
-> turn-ratio nearest-integer error
-> positive generated gaps below the context
-> floor and ceiling witnesses for each gap

The useful idea is that the real-valued question becomes a finite nearest-integer certificate: check each positive gap below the context, and for each gap check the floor and ceiling integer turns. That gives Python a finite audit shape and gives Lean exact theorem ids for the reduction.

Detailed real-phase reduction trail

AIRA-T0041 converts one-channel real phase error into the normalized nearest-integer expression |gap * alpha - turns|, where alpha = frequency / fullTurn. AIRA-T0054 says the finite-context predicate is equivalent to checking the generated positive gaps in List.range context. AIRA-T0058 proves that for one fixed real value, checking the integer floor and integer ceiling is equivalent to checking every integer. AIRA-T0059 applies that result to every generated gap, reducing the remaining integer-turn side of the finite-context margin predicate to two witnesses per gap. AIRA-T0182 packages the two endpoint errors for one gap into a scalar nearest-gap margin, and AIRA-T0183 proves that a finite-context margin is equivalent to lower-bounding that scalar for every generated positive gap. AIRA-T0214 adds the exact-weakest-gap report shape: a reported weakest margin is justified by a finite lower-bound proof plus one inspected witness gap that actually attains that margin. AIRA-T0126 adds the generated-band endpoint bridge: if a whole gap band shares one integer cell and the band endpoints satisfy the lower/upper inequalities, Lean derives interval witnesses for every gap in the band. The generated coverage side is now a separate contiguous-chain certificate, and the endpoint side is checked on compact rows with shared lower/upper bounds, so the Lean proof mirrors the Python audit instead of rebuilding a different expanded-table argument.

That is a real formal improvement, but it is not the final Diophantine theorem. The next mathematical step is to prove, by continued fractions, Diophantine estimates, or an exact finite certificate, that those floor/ceiling inequalities hold for a concrete nonperiodic RoPE turn ratio and margin.

First Named Finite-Margin Certificate

The first complete certificate on this path is deliberately rational/discretized:

turn ratio = 1 / 4099
context    = 4096
margin     = 1 / 4099

Lean proves that every positive gap below 4096 stays at least 1/4099 away from an integer turn for this declared ratio. The reason is finite and exact: the ratio is reduced, and the denominator return gap 4099 is outside the inspected context.

The Python API exposes the same certificate:

from circle_math.applications import certify_rational_preset_4099

certificate = certify_rational_preset_4099()
certificate.pass_certificate      # True
certificate.certified_margin      # 1 / 4099 as a Python float
certificate.exact_nearest_gap_margin  # "1/4099"
certificate.exact_nearest_gap         # 1
certificate.zero_margin_witness       # None
certificate.theorem_ids           # includes AIRA-T0061, AIRA-T0185, AIRA-T0215

The public lesson-facing conclusion is simple: this ratio has a certified weakest gap of 1, an exact weakest margin of 1/4099, and no zero-margin witness before the denominator return.

Detailed rational finite-margin theorem trail

AIRA-T0182 and AIRA-T0183 justify the exact weakest-gap scalar reported by Python: the scalar is the minimum of the floor and ceiling nearest-integer errors, and lower-bounding that scalar over every generated gap is equivalent to the finite-context margin predicate. AIRA-T0214 states the reusable exact-weakest-gap contract: the report is correct when the finite lower bound holds and the named gap realizes it. AIRA-T0060 is the generic proof-carrying certificate interface. AIRA-T0177 proves that this finite nearest-integer certificate object is equivalent to the abstract finite-context margin predicate. AIRA-T0186 proves that any strictly positive finite-margin certificate rules out exact zero turn error for every generated positive gap. AIRA-T0061 is the named 1/4099 context-4096 finite-margin theorem. AIRA-T0185 proves the preset’s exact weakest-gap ingredients: gap 1 realizes margin 1/4099, and no positive generated gap has smaller scalar nearest-integer margin. AIRA-T0215 packages those ingredients into the reusable report contract. AIRA-T0222 and AIRA-T0223 generalize that exact-gap result to every rational/discretized 1/d turn ratio in a nontrivial context that stays before the denominator return gap. AIRA-T0224 through AIRA-T0226 generalize the report shape further: when a reduced rational turn ratio has a concrete gap whose numerator product is one residue away from an integer number of denominators, Lean proves that witness realizes the exact weakest scalar margin 1/denominator before the denominator return gap. AIRA-T0227 proves that the full denominator context always has such a witness for reduced natural-rational turn ratios, so Python no longer has to treat full-period exact-gap existence as an unchecked search fact. AIRA-T0228 adds the exact full-denominator threshold: in that context, margins at or below 1/denominator pass and larger advertised margins fail. AIRA-T0229 adds the request-facing failure witness: above that threshold, Lean proves an explicit positive gap and integer turn whose error is already below the requested margin. AIRA-T0230 and AIRA-T0231 generalize the request threshold to any exact weakest-gap certificate. The Python report summarizes that request branch as requested_margin_status: proved, impossible, unproved_above_certified_lower_bound, or unproved. AIRA-T0187 specializes the no-zero theorem to the named preset, matching the public zero_margin_witness = None field. AIRA-T0196 proves that the finite certificate object itself is equivalent to the one-channel no-near-turn contract. AIRA-T0062 is the named one-channel no-near-turn consequence below that certified margin.

This is the first end-to-end theorem-backed certificate shape. It does not certify the standard irrational 1 / (2π) RoPE channel.

Current Standard RoPE Interval Seed

The theorem-backed certificates for the genuine standard channel are deliberately bounded. The longest current named seed is:

turn ratio = 1 / (2π)
context    = 196608
margin     = 1 / 328459

Lean proves this by enclosing each inspected value with exact rational bounds. The initial context-7 seed uses:

gap / 8 <= gap / (2π) <= 25*gap / 157

for gaps 1 through 6, using π <= 4 for the lower side and 3.14 < π for the sharper upper side. Later seeds reuse already-certified gaps at smaller advertised margins, then continue with new interval bands. Lean certifies gaps 7 through 43 with:

10*gap / 63 <= gap / (2π) <= 25*gap / 157

using π < 3.15 for the lower side and 3.14 < π for the upper side, split across integer cells 1 through 6. The next obstruction appears at gap 44, where the older enclosure straddles an integer turn. The current seed crosses it with:

5000*gap / 31416 <= gap / (2π) <= 5000*gap / 31415

using π < 3.1416 and 3.1415 < π. The context-333 seed uses that same four-decimal enclosure for every gap 1 through 332, split across generated integer cells 0 through 52.

The context-710 seed moves to six-decimal bounds:

500000*gap / 3141593 <= gap / (2π) <= 500000*gap / 3141592

using π < 3.141593 and 3.141592 < π, split across generated cells 0 through 112 for gaps 1 through 709.

Lean also proves why this exact 1/1024 margin stops there: gap 710 is already within that margin of integer turn 113. A larger context for channel 0 must therefore use a smaller advertised margin or a different theorem shape; it cannot extend the same lower bound.

The first context-4096 seed lowers the advertised margin and moves to twenty-decimal π bounds:

100000000000000000000*gap / 628318530717958647694
  <= gap / (2π)
  <= 100000000000000000000*gap / 628318530717958647692

Those exact rational bands now certify gaps 1 through 196607, split across generated integer cells 0 through 31290. D9 first certified the conservative margin 1/131072; D10 reused the same 20-decimal bounds and cell table to certify the tighter margin 1/105000; D11 tightened the 4k certificate shape to 1/104219; D12 reached 8k at the weaker margin 1/104220; D13 reaches 8k at 1/104219; D14 reaches 16k at 1/104219; D15 reaches 32k; D16 reaches 64k; D17 reaches 128k by lowering the advertised margin to 1/328459; D18 carries that lower margin to 160k; and D19 carries it to 192k.

D19 is the current proved standard-channel frontier. The D19 bridge turns that channel-0 seed into a conditional one-separating-channel bank certificate when standard channel 0 is present: the proved branch at or below 1/328459 transfers to a first-channel finite-bank no-near-turn guarantee over every ordered unequal pair inside the requested context, while every margin at or above 1/328458 is impossible only for the one-channel margin throughout 103993 < context <= 196608. The remaining open interval has exact rational width 1/107884986222, AIRA-T0238 places the public 2/656917 undecided probe inside that interval, AIRA-T0233 proves the in-range semantic partition is exclusive, AIRA-T0234 packages the proved-branch bank transfer, AIRA-T0235 packages its context-wide pair scope, AIRA-T0236 specializes that scope to the ordinary radian bank form with first frequency 1 and full turn 2π, and AIRA-T0237 packages the in-range request trichotomy with that radian first-channel consequence in the proved branch. AIRA-T0239 through AIRA-T0241 are the complementary global guardrails: they prove a close-return witness exists below every nontrivial finite context, that margins strictly above 1/context cannot hold, and that exact weakest-gap report margins cannot exceed that scale. They do not identify the standard-channel worst gap or prove a positive margin. This is still not a full all-channel margin theorem.

Detailed D19 classifier theorem trail

AIRA-T0173 packages the 192k endpoint bracket, AIRA-T0209 proves the generic horizon-plus-obstruction bridge, and AIRA-T0208 specializes it to the D19 range bracket. AIRA-T0216 and AIRA-T0217 package the same fact as a request-level classifier: a requested margin below the proved threshold is certified, a requested margin above the obstruction threshold is rejected, and a requested margin strictly between those two thresholds is deliberately reported as undecided. AIRA-T0218 proves the two rational thresholds are ordered, AIRA-T0219 proves the proved and impossible request branches are disjoint, AIRA-T0220 identifies the undecided branch with the exact open interval, AIRA-T0221 proves those three margin regions are exhaustive, AIRA-T0233 proves the in-range semantic branches are exclusive and carry the correct proof/refutation/open-gap meaning, AIRA-T0234 transfers the proved branch to a conditional first-channel bank no-near-turn guarantee, AIRA-T0235 packages that guarantee for all ordered unequal pairs in the requested context, AIRA-T0236 rewrites it into the ordinary radian first-channel bank form, AIRA-T0237 combines the in-range semantic classifier with that radian first-channel consequence, AIRA-T0232 proves the interval width is exactly 1/107884986222, AIRA-T0238 proves the public undecided probe 2/656917 lies strictly inside the interval, AIRA-T0239 gives the general Dirichlet close-return ceiling for any turn ratio and finite context, AIRA-T0240 gives the direct no-margin-above-1/context consequence, and AIRA-T0241 bounds any exact weakest-gap report margin by 1/context.

Lean also proves sharper negative companions for this seed family. Gap 710 is already within 1/65536, within 1/104000, and within 1/104218 of integer turn 113. That means the D9 1/131072 margin cannot simply be doubled, the D10 1/105000 margin cannot simply be raised to 1/104000, and the D16 1/104219 margin cannot simply be raised to 1/104218 for any context containing gap 710. Gap 103993 is already within 1/328458 of integer turn 16551, so D19 cannot raise its advertised margin to 1/328458.

The Python API exposes the theorem-backed seed:

from circle_math.applications import certify_standard_channel0_interval_seed

certificate = certify_standard_channel0_interval_seed()
certificate.pass_certificate      # True
certificate.certified_margin      # 1/328459
certificate.theorem_ids           # includes AIRA-T0063, AIRA-T0173, AIRA-T0208

The certificate object is the API-level bridge between generated rational bands, Lean declarations, and a downstream planner that only wants a pass/fail or request-status field.

Detailed standard-channel seed theorem trail

AIRA-T0063 proves that one rational interval witness covers every integer turn for one gap. AIRA-T0064 turns a finite table of those witnesses into a finite-context margin. AIRA-T0077 and AIRA-T0078 prove that interval witnesses and certificates survive when the advertised margin is decreased. AIRA-T0065 through AIRA-T0138 build the standard channel-0 seed family through context 16384, including the D12/D13/D14 conditional bank bridges and brackets. AIRA-T0139 through AIRA-T0141 package the rational-band list compression and rational-endpoint reflection bridge. AIRA-T0142 through AIRA-T0147 are the generated D15 context-32768 seed, one-channel no-near-turn theorem, bank bridges, and margin bracket. AIRA-T0148 through AIRA-T0153 are the generated D16 context-65536 seed. AIRA-T0154 through AIRA-T0161 are the D17 128k obstruction, interval certificate, one-channel no-near-turn theorem, bank bridges, and margin bracket; AIRA-T0162 through AIRA-T0167 are the generated D18 160k interval certificate, one-channel no-near-turn theorem, bank bridges, and margin bracket; AIRA-T0168 through AIRA-T0173 are the generated D19 192k interval certificate, one-channel no-near-turn theorem, bank bridges, and endpoint margin bracket; AIRA-T0209 is the generic context-range bracket bridge; AIRA-T0208 is the D19 context-range margin bracket; and AIRA-T0216/AIRA-T0217 are the request-level classifier bridge and D19 specialization.

This is standard RoPE, but it is still channel-0 based. The D19 bridge can rule out an all-bank near-turn event when standard channel 0 is present and the requested context and margin fit inside the D19 seed; it does not prove independent margins for every channel.

from fractions import Fraction
from circle_math.applications import certify_standard_channel0_d19_bank_request

request = certify_standard_channel0_d19_bank_request(
    requested_context=196608,
    requested_margin=Fraction(1, 328459),
)
request.pass_certificate  # True
request.theorem_ids       # AIRA-T0171,AIRA-T0172,AIRA-T0234,AIRA-T0235,AIRA-T0236,AIRA-T0237
request.tolerance_rule    # tolerance < fullTurn * requestedMargin

For direct one-channel margin classification inside the D19 obstruction range:

from fractions import Fraction
from circle_math.applications import (
    certify_standard_channel0_d19_range_request_margin_bracket,
)

request = certify_standard_channel0_d19_range_request_margin_bracket(
    requested_context=131072,
    requested_margin=Fraction(1, 328458),
)
request.request_status  # "impossible"
request.theorem_ids     # AIRA-T0216,AIRA-T0217,AIRA-T0218,AIRA-T0219,AIRA-T0220,AIRA-T0221,AIRA-T0233,AIRA-T0232
request.proved_impossible_branches_disjoint  # True
request.margin_status_exhaustive             # True
request.in_range_semantic_trichotomy         # True

Larger contexts and full all-channel RoPE-bank margins need generated interval data plus sharper π, continued-fraction bounds, or a different proof shape before they can be marked proved.

The Python sidecar now exposes the proved generated plans, the proved D19 192k plan, and the stronger 128k frontier that still fails at margin 1/104219:

from fractions import Fraction
from circle_math.applications import (
    audit_standard_channel0_rational_band_certificate,
    plan_standard_channel0_interval_bands,
)

d4_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d4",
    margin=Fraction(1, 512),
)
d6_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d6",
    margin=Fraction(1, 1024),
)
d20_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d20",
    margin=Fraction(1, 104219),
)
d20_8k_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d20",
    margin=Fraction(1, 104219),
    max_context_length=8192,
)
d20_16k_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d20",
    margin=Fraction(1, 104219),
    max_context_length=16384,
)
d20_32k_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d20",
    margin=Fraction(1, 104219),
    max_context_length=32768,
)
d20_64k_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d20",
    margin=Fraction(1, 104219),
    max_context_length=65536,
)
d20_128k_frontier_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d20",
    margin=Fraction(1, 104219),
    max_context_length=131072,
)
d20_128k_d17_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d20",
    margin=Fraction(1, 328459),
    max_context_length=131072,
)
d20_160k_d18_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d20",
    margin=Fraction(1, 328459),
    max_context_length=163840,
)
d20_192k_d19_plan = plan_standard_channel0_interval_bands(
    pi_bound_preset="d20",
    margin=Fraction(1, 328459),
    max_context_length=196608,
)

d4_plan.theorem_status  # lean_proved_interval_seed_AIRA-T0087_to_AIRA-T0089
d6_plan.context_length  # 710
d6_plan.theorem_status  # lean_proved_interval_seed_AIRA-T0090_to_AIRA-T0094
d20_plan.context_length # 4096
d20_plan.theorem_status # lean_proved_interval_seed_AIRA-T0111_to_AIRA-T0114
d20_8k_plan.context_length # 8192
d20_8k_plan.theorem_status # lean_proved_interval_seed_AIRA-T0127_to_AIRA-T0129
d20_16k_plan.context_length # 16384
d20_16k_plan.theorem_status # lean_proved_interval_seed_AIRA-T0133_to_AIRA-T0135
d20_32k_plan.context_length # 32768
d20_32k_plan.theorem_status # lean_proved_interval_seed_AIRA-T0142_to_AIRA-T0144
d20_64k_plan.context_length # 65536
d20_64k_plan.theorem_status # lean_proved_interval_seed_AIRA-T0148_to_AIRA-T0150
d20_128k_frontier_plan.first_uncovered_gap # 103993
d20_128k_d17_plan.context_length # 131072
d20_128k_d17_plan.theorem_status # lean_proved_interval_seed_AIRA-T0156_to_AIRA-T0158
d20_160k_d18_plan.context_length # 163840
d20_160k_d18_plan.theorem_status # lean_proved_interval_seed_AIRA-T0162_to_AIRA-T0164
d20_192k_d19_plan.context_length # 196608
d20_192k_d19_plan.theorem_status # lean_proved_interval_seed_AIRA-T0168_to_AIRA-T0170

d20_64k_audit = audit_standard_channel0_rational_band_certificate(
    d20_64k_plan,
    requested_context_length=65536,
)
d20_64k_audit.pass_audit # True

d20_128k_audit = audit_standard_channel0_rational_band_certificate(
    d20_128k_frontier_plan,
    requested_context_length=131072,
)
d20_128k_audit.pass_audit # False
d20_128k_audit.first_uncovered_gap # 103993

The d4, d6, conservative d20, tighter d20, sharp 4k d20, weaker 8k d20, sharp 8k d20, sharp 16k d20, sharp 32k d20, sharp 64k d20, D17 128k d20, D18 160k d20, and D19 192k d20 plans are now source tables for compiled Lean declarations. The sidecar now emits a standard_channel0_frontier_summary and standard_band_certificate_audits: Lean-proved standard channel-0 margin 1/328459 reaches context 196608, while the stronger 128k margin 1/104219 request first fails audit coverage at gap 103993. Each emitted band also records the lower endpoint value, upper endpoint value, whether the endpoint cell-margin check passes, and bridge_theorem_id = AIRA-T0126; the generated route is the AIRA-T0139/AIRA-T0140/AIRA-T0141 band-list and endpoint-reflection bridge. In Lean, the large generated tables are stored as compact uniform bands: each row records only the gap range and integer cell, while the shared 20-decimal rational bounds are attached once before the proof bridge consumes the list. Coverage and endpoint validity are both checked against that compact shape before reflection into the expanded certificate object. That is source/proof-build compression, not a stronger theorem.

Read one band like this:

start_gap = 1
end_gap = 6
cell = 0
start_lower_value = 625 / 3927
end_upper_value = 6000 / 6283
endpoint_cell_margin_ok = true

This says the generator has one cell band covering gaps 1 through 6. The lower endpoint already lies at least the requested margin after integer cell 0, and the upper endpoint still lies at least the requested margin before integer cell 1. Because multiplication by the rational lower and upper turn-ratio bounds is monotone over nonnegative gaps, AIRA-T0126 fills in every gap between those endpoints. Future exact-rational plans remain planning artifacts until matching declarations compile and manifest ids are marked proved.

The generated sidecar Markdown and JSON have Band Endpoint Audit summaries that sample the first and last band for each standard interval plan. Rerun the Python planner for the complete deterministic band list.

What To Notice

Exact collision is not guessed by scanning every pair. The theorem reduces it to divisibility of the position gap.
If the common exact collision gap is inside the context, the report lists sample colliding position pairs.
Counts have layers. Common-gap counts, total all-channel bank counts, and per-channel counts answer different questions.
Prefix and subfamily reports are shortcuts for engineers: they explain which smaller part of a period bank already certifies the whole declared integer-period bank.
If the exact discrete contract passes, the report still does not claim real model quality or long-context success.
The real-phase margin scan is useful engineering evidence, but it is not a Lean proof over real-valued trigonometric RoPE.
The current standard-RoPE frontier is useful but narrow: it is channel-0 based, conditional, and not a continued-fraction theorem.

Detailed theorem trail for report fields

The guaranteed common-gap count is context - gap: every counted start gives an all-channel collision at that gap. The LCM theorem upgrades the positive common-gap-multiple sum into the exact total bank collision count for the declared integer-period model. The positive-period-bank theorem proves the LCM is positive under the certifier’s input policy. The exact pass/fail iff says the whole context is collision-free exactly when that LCM reaches the context. The fail-witness theorem proves an explicit unequal collision exists when the positive LCM is below the context, the count-zero theorem proves the positive-multiple total is zero exactly in the pass case, and the count-positive theorem proves the nonzero total is equivalent to an unequal all-channel collision witness.

Bounded prefix reports apply the same LCM theorem spine to early channel prefixes, so first_exact_pass_prefix_length identifies the first reported prefix whose integer-bank LCM already reaches the inspected context. AIRA-T0051 proves that appending suffix channels cannot create an unequal full-bank collision after such a prefix already passes. AIRA-T0190 proves that a certified first passing prefix length is unique, and AIRA-T0191 turns that first-prefix certificate into a full-bank no-collision bridge.

Bounded subfamily reports search small selected subbanks; AIRA-T0052 proves the same no-collision bridge when any contained subbank’s LCM reaches the inspected context. AIRA-T0193 proves that a certified smallest sufficient subfamily size is unique, and AIRA-T0194 turns that smallest-subfamily certificate into a full-bank no-collision bridge.

For the diagnostic prefix preset [6, 9, 13, 18] at context 128, AIRA-T0188 proves that the first passing prefix has length 3, AIRA-T0192 proves that this satisfies the reusable first-prefix predicate, AIRA-T0189 proves that singleton subbanks are insufficient while [13, 18] is sufficient, and AIRA-T0195 proves that [13, 18] satisfies the reusable smallest-subfamily predicate. AIRA-T0198 through AIRA-T0202 add named finite count certificates for the public shared-factor, quantized-boundary, and scaled-period diagnostic rows. AIRA-T0206 and AIRA-T0207 add the reusable first-repeat boundary formula behind one-token-past-boundary counts. AIRA-T0210 adds the quotient bound behind the common_gap_fitting_multiple_count and prefix fitting_collision_multiple_count fields, AIRA-T0211 proves the total positive-multiple count equals the finite sum over that fitting range, AIRA-T0212 proves the doubled triangular closed-form numerator, and AIRA-T0213 proves the exact divided closed form. These are exact integer-period count theorems, not global optimization theorems for arbitrary real-valued RoPE banks.

The per-channel single-period counts are exact for each individual integer period; they are not all-channel bank counts. AIRA-T0204 proves the threshold condition for one positive period: no unequal in-context collision exists exactly when the context length is at most the period. AIRA-T0203 proves the zero-count interpretation, and AIRA-T0205 proves the positive-count interpretation: nonzero means there is an actual unequal in-context collision witness in that one channel. AIRA-T0206 and AIRA-T0207 give the first-repeat-only closed form and the count-1 one-token-past-boundary case; AIRA-T0210 proves that (context - 1) / period is exactly the number of positive period multiples that can contribute, AIRA-T0211 proves the executable count loop may sum over only those multiples, AIRA-T0212 proves the doubled triangular closed-form numerator for that loop, and AIRA-T0213 proves the exact divided closed form.

The real-valued formal work has begun with an unwrapped phase-gap formula (AIRA-T0029), lower-bound precursor (AIRA-T0030), one-turn endpoint-error precursor (AIRA-T0031), nonnegative full-turn-multiple precursor (AIRA-T0032), signed full-turn-multiple precursor (AIRA-T0033), turn-separation predicate (AIRA-T0037), no-near-turn consequence (AIRA-T0038), finite bank-level no-near-turn bridge (AIRA-T0039, AIRA-T0040), turn-ratio Diophantine scaling bridge (AIRA-T0041), finite-context margin consequence (AIRA-T0042), bank finite-context margin consequence (AIRA-T0043), finite-context monotonicity (AIRA-T0044), bank-level certified-context transfer (AIRA-T0045), conservative margin downgrade (AIRA-T0047), combined context-plus-margin bank transfer (AIRA-T0050), integer-turn-ratio and natural-rational-turn-ratio no-positive-margin guardrails (AIRA-T0053, AIRA-T0055), a positive reduced-rational finite-context certificate before the denominator gap (AIRA-T0056), an exact reduced-rational denominator-boundary iff (AIRA-T0057), generated-gap finite-enumeration bridge (AIRA-T0054), floor/ceiling nearest-integer witness bridge (AIRA-T0058, AIRA-T0059), scalar nearest-gap margin bridge (AIRA-T0182, AIRA-T0183), exact weakest-gap report bridge (AIRA-T0214, AIRA-T0215), finite certificate equivalence (AIRA-T0177), positive-margin no-zero-error bridge (AIRA-T0186), negative obstruction equivalence (AIRA-T0178), one-channel scaled no-near-turn equivalence (AIRA-T0181), certificate-object no-near-turn equivalence (AIRA-T0196), finite-certificate bank bridge (AIRA-T0197), the named rational/discretized 1/4099 certificate and no-zero witness bridge (AIRA-T0060 through AIRA-T0062, AIRA-T0185, AIRA-T0187), the reusable 1/d exact weakest-gap family (AIRA-T0222, AIRA-T0223), the generic reduced-rational modular-inverse exact-gap report family (AIRA-T0224 through AIRA-T0226), the full-denominator reduced-rational exact-gap existence, exact-threshold, and request-obstruction theorems (AIRA-T0227 through AIRA-T0229), the generic exact-weakest request-threshold theorems (AIRA-T0230, AIRA-T0231), interval-certificate margin monotonicity (AIRA-T0077, AIRA-T0078), the standard channel-0 seed family through D14 (AIRA-T0063 through AIRA-T0138), the rational-band compression route (AIRA-T0139 through AIRA-T0141), the generated D15/D16 32k/64k certificates and bank bridges (AIRA-T0142 through AIRA-T0153), the generated D17 128k certificate, obstruction, bank bridges, and bracket (AIRA-T0154 through AIRA-T0161), the generated D18 160k certificate, bank bridges, and bracket (AIRA-T0162 through AIRA-T0167), the generated D19 192k certificate, bank bridges, and endpoint bracket (AIRA-T0168 through AIRA-T0173), the generic context-range bracket bridge (AIRA-T0209), the D19 context-range bracket (AIRA-T0208), the request-level D19 classifier (AIRA-T0216, AIRA-T0217), its threshold-order/disjoint-branch consistency guards (AIRA-T0218, AIRA-T0219), the exact open-gap/exhaustive-status theorems (AIRA-T0220, AIRA-T0221), the in-range semantic trichotomy theorem (AIRA-T0233), the proved-branch first-channel bank-transfer theorem (AIRA-T0234), the context-wide first-channel pair-scope theorem (AIRA-T0235), the ordinary radian first-channel specialization (AIRA-T0236), the in-range radian first-channel semantic trichotomy (AIRA-T0237), the exact open-gap width theorem (AIRA-T0232), the public undecided-probe open-gap theorem (AIRA-T0238), the general finite-context Dirichlet upper-bound witness (AIRA-T0239), the direct no-margin-above-1/context corollary (AIRA-T0240), and the exact weakest-gap report ceiling (AIRA-T0241). The longest proved standard seed is still channel-0 based; it is not a full all-channel bank theorem or a continued-fraction theorem.

Core Proof Cards

The lesson keeps only the cards needed to follow the proof chain while reading. The full audit trail lives in RoPE proof audit and the generated Theorem Index.

Dictionary

Source Trail

Paper source: Proof-Carrying RoPE Position Distinguishability

Lean source: Circle/Applications/RoPECertifier.lean

Python source: circle_math/applications/rope_certifier.py

CLI source: scripts/rope_certify.py

Exact phase-bank CLI source: scripts/phase_bank_certify.py