diff --git a/research/frontier-beat-2026-10-09/INSTANTIATE.md b/research/frontier-beat-2026-10-09/INSTANTIATE.md new file mode 100644 index 0000000000..9e19a3e4c5 --- /dev/null +++ b/research/frontier-beat-2026-10-09/INSTANTIATE.md @@ -0,0 +1,118 @@ +# What instantiating the bit rank-6 bank rung would take + +The cheapest way to beat the frontier is [beats.py](beats.py)'s first strict rung: +absorb the bit word's rank-6 child family into width-72 banks, worth **+2.1672%** +(`kappa` 6.831904550366e-4 → 6.979968750671e-4). This note asks what would have to +exist for it to be a construction. + +``` +python3 -B instantiate.py # ~2 s, writes instantiate.json +python3 -B instantiate.py --check # byte-for-byte comparison with it +``` + +Everything below is derived from the frontier certificate's own three-copy row; the +supplier's published bank proof is vendored beside it +([coordinated-bank-proof.md](references/queue/coordinated-bank-proof.md), hashed in +[SOURCE.json](SOURCE.json)) and read item by item. + +## The schedule, and the condition that decides it + +A bank is a width-`m` coordinate-block partition, so a family absorbs into banks only +when its own volume fills whole banks. For rank `r` on width `m` that has a one-line +form: `m/r` blocks fill a bank, so the family's child count must be **divisible by +`m/r`**. On the frontier's two words that leaves exactly four families: + +| word | rank | blocks per bank | banks (three copies) | children divisible by `m/r` | +| --- | ---: | ---: | ---: | --- | +| bit (m=72) | **6** | 12 | 1008 | yes | +| bit (m=72) | 8 | 9 | 816 | yes | +| bit (m=72) | 18 | 4 | 999 | yes | +| complex (m=66) | 11 | 6 | 177 | yes | +| bit | 1, 2, 3, 4, 9, 12 | 72, 36, 24, 18, 8, 6 | — | no | +| complex | 1, 2, 3, 6 | 66, 33, 22, 11 | — | no | + +Rank 4 is the certified block size and rank 1 is the biggest mass in the word, but +neither has a volume that fills whole banks, so neither is available without a mixed +tiling. The stride-6, 9 and stride-4 partitions are the ones the arithmetic admits. + +## The rung's arithmetic, re-derived + +| quantity | value | +| --- | --- | +| family | bit rank 6 | +| children | 12,096 over three copies = **4,032 per physical copy** | +| blocks per bank | 12 (stride 6 on width 72, `12 × 6 = 72`) | +| blocks needed | 4,032 per copy — **exactly one block per absorbed child**, count for count | +| banks | 1,008 over three copies = **336 per copy**, integral | +| removed rank volume | 72,576 | +| stock `W` | 56,402 → 55,394 (the fall is the bank count, by the row identity) | +| rank mass | 4,055,136 → 3,982,560 | +| deficit | 5,808, **unchanged** | +| retained ledger | 21 families, max child 22 | +| certified saving | 6.83657523331095e-4 → **6.98484415006068e-4** | +| kappa | 6.831904550366e-4 → **6.979968750671e-4** (+2.1672%) | + +The one-block-per-child identity is the useful structural fact: the normalizer's +targets and the absorbed children are equinumerous, so no child needs two blocks and +no block is left half-used at this rank. The certified proof's own absorption is not +like that — it removes 2,200 rank-60 gauge exteriors whose volume (396,000 over three +copies) fills 5,500 banks, and it needed nine physical replicas to make its +stage-private allocation integral. Here the per-copy count is 336, so if the rank-6 +dirt is stage-private in the same three-family way the allocation is 112 banks per +stage and needs no replicas. **That is an inference**: no pin says the rank-6 dirt is +stage-private. + +## What the published bank proof already covers + +The proof is a finite verification of a *different* absorption — the rank-60 entrance +exteriors, one per selected gauge — but several of its items are stated for any +partition, so the rung inherits them: + +* **The projector algebra.** `S_P S_Q = S_(P+Q)` and `S_P² = I` are proved by direct + expansion for *any* finite disjoint projector partition summing to `I`, and chart + conjugation telescopes for any common invertible weighted chart. A stride-6 + partition needs no new algebra; it is a new instance of the same construction. +* **The column check.** 144 columns of the two-bank address map over `F2` and over + `Z`, for the endpoint and its inverse, rejecting a missing or repeated last block in + both rings. `144 = 2 × 72` independently of which blocks fill the bank. +* **The moment-envelope parity.** The rare-class fraction `10^-16`, the fallback + `32 × 72²` children per edge and the positive atom/row-adapter toll on its own + `10^-24` grid are all unchanged by this rung, and two rational log/exp enclosures + certify the accepted moment and reject the adjacent `10^-18` point — which is + exactly what `beats.json` and `instantiate.json` already do with the supplier's own + enclosure implementation. +* **The assembly.** 47 strict constraints and 7 margins at PR207's parameters. The + rung is bit-binding, so the complex budget is untouched. + +## What it does not cover, and what is missing + +* **The normalizer.** The certified proof's banked items are the 2,200 rank-60 gauge + exteriors, and each one's *gauge itinerary* supplies its address. The rank-6 family + is interior dirt with no registered gauge address, so the child-to-block map has to + be built rather than inherited. +* **The inventory — the real gap.** No pinned package enumerates the word's rank-6 + children: not their frame or chain occurrences, not a bijection onto the 4,032 + blocks per copy, and not a proof that nothing else in their ledger row moves. This + is the same blank shape as the complex rung's inventory obligation, and it is + smaller: one family of one word, whose counts, bank schedule and divisibility + condition are pinned by this file. +* **Charts and witnesses.** Integer kernel bases with fraction-free inverses and + replayed elementary factors for the stride-6 frames, and distinct integer Gram/prime + witnesses for each of the 1,008 three-copy blocks (the certified supply is per block + *frame*, not per bank). +* **The conditional interfaces.** The inherited all-input weighted compiler, the + completed-core routing, the stage cover, local-ring precision/recovery, prime + supply, uniform setup and the all-size analytic/tape contracts stay conditional; the + bank proof discharges none of them, and neither does this package. + +## Verdict + +The rung is the closest of the pinned targets to being buildable: its algebra is +inherited from a published proof rather than invented, its allocation is integral +per copy (so it does not need the replicas the certified bank used), the block +arithmetic is exact and pinned here, and the saving and kappa are certified with +tooling that already exists. What stops it is not mathematics but an inventory: the +dirt it removes has never been enumerated anywhere in the queue, exactly as the +complex word's rank-11 family has never been. Whoever writes that enumeration — one +family, one word, 4,032 items per copy — hands this rung to the certified harness with +the stride changed from 4 to 6. diff --git a/research/frontier-beat-2026-10-09/README.md b/research/frontier-beat-2026-10-09/README.md new file mode 100644 index 0000000000..8faec11505 --- /dev/null +++ b/research/frontier-beat-2026-10-09/README.md @@ -0,0 +1,247 @@ +# Ways to beat the frontier kappa, priced exactly (2026-10-09) + +The frontier is PR207's coordinated crossover. This directory changes no pinned +artifact: it reproduces that certificate's two side savings and its kappa from the +certificate's own child ledgers with no floating point, then prices every way the +record's own composition can move the headline. + +``` +python3 -B beats.py # ~95 s, writes beats.json +python3 -B beats.py --check # re-runs and compares byte for byte +``` + +## The frontier, and why it is one number + +The certificate states `a_bit`, `a_complex` and `kappa`, and `kappa` is +`floor(min(a_bit, a_complex)/(1 + min(...)))` on a `10^-16` grid. So the headline is +a function of **one** quantity: the smaller side saving. Reproduced here: + +| quantity | value | how it is reproduced | +| --- | ---: | --- | +| `a_bit` | `136731504666219/2*10^17` = 6.83657523331095e-4 | to **sixteen significant digits** under the bit side's convention; the certificate's own fraction sits `1.4e-16` lower (`2.1e-13` relative) | +| `a_complex` | `700918443859411/10^18` = 7.00918443859411e-4 | **exact to the last digit** | +| `kappa` | `1366380910073/2*10^15` = 6.831904550365e-4 | **exact**, and the grid is discovered, not assumed | +| binding side | **bit** (6.8366e-4 vs 7.0092e-4) | | + +The bit side carries 2.5% of unused complex budget above it, and nothing in the +composition can spend it. + +**A convention worth knowing.** The certificate prices its two sides *differently*: +the bit side includes PR200's rare-class fallback term, the complex side does not. +Each is reproduced exactly under its own convention here. The pinned ladder +(`rungs.json` in the supplier's package) prices *both* sides with the fallback, so +its numbers sit about `6e-10` relative below this package's; `beats.json` records +both conventions for every rung. + +## Ranked ways to beat it + +### 1. Bank a family on the bit word — the cheapest complete way + +Banking means the family's children leave the ledger, the stock falls by the row +identity, and the paid moment pays less twice over. A family whose own blocks tile a +bank (`m % rank == 0`) and whose own volume is a whole number of banks needs no +block shape the word does not already use. **There are exactly three such families +on the bit word (6, 8, 18) and one on the complex word (11)**, and every +combination is priced here: + +| absorb | new types | banks | kappa | gain | +| --- | ---: | ---: | ---: | ---: | +| bit **{6}** | 1 | 1008 | 6.979968750671e-4 | **+2.167%** | +| bit {8} | 1 | 816 | 6.937230027167e-4 | +1.542% | +| bit {18} | 1 | 999 | 6.912953180546e-4 | +1.186% | +| bit **{6,8}** | 2 | 1824 | 7.004275013051e-4 | **+2.523%** | +| bit {6,18} / {8,18} / {6,8,18} | 2–3 | 2007/1815/2823 | 7.004275013051e-4 | +2.523% | +| bit **{6,8} + complex {11}** | 3 | 2001 | 7.082915705907e-4 | **+3.674%** | +| bit {6,18} + complex {11} | 3 | 2184 | 7.06458935046e-4 | +3.406% | +| bit {8,18} + complex {11} | 3 | 1992 | 7.020811447888e-4 | +2.765% | +| bit {6} + complex {11} | 2 | 1185 | 6.979968750671e-4 | +2.167% | +| complex {11} alone | 1 | 177 | 6.831904550366e-4 | +0.000% | + +Reading it: + +* **+2.167% is the cheapest way to beat the frontier at all**: one new residual + type, 1008 banks, the bit rank-6 family. The bit side is still binding + afterwards, so the gain is the bit side's alone. [INSTANTIATE.md](INSTANTIATE.md) + takes that rung apart: its block and bank schedule, and what the supplier's own + bank proof already covers for it — the projector algebra is inherited, the + per-copy allocation is integral, and the gap is an inventory (no pin enumerates + the word's rank-6 children), not a piece of mathematics. +* **+2.523% is the first rung that makes the complex side binding** — the bit side + clears the complex budget and the kappa becomes the complex cap. It agrees with + #219's published rung 1 (`700427501305159/10^18`) on every digit the `10^-16` + grid carries, so this rung is known and already claimed upstream. +* **+3.674% is the best rung that needs no new block shape** (bit {6,8} + + complex {11}), and it is exactly the rung priced in the queue as the boundary: + beyond it the complex word has nothing bankable on its own anymore. The two + intermediate rows ({6,18} and {8,18} with complex {11}) sit between them, and + every one of the 16 combinations is in `beats.json → strict_ladder`. +* Absorbing on the *non-binding* side is worth nothing: complex {11} alone moves + the complex saving +1.12% and the headline by `+0.000%`. + +### 2. The modelled tier — what the bank model pays, and what it assumes + +The screen below treats an absorbed family's rank as free (only its volume must +fill whole banks), which is what #205/#206/#207 certified for rank 60 on width 72. +It runs over **every** family set of up to five families per word whose volume fills +whole banks — 3,512 admissible sets on the bit word, 991 on the complex word — and +decides each one with a single exact interval evaluation, no bisection and no +tolerance. The leaders of each family count are then priced exactly: + +| families absorbed | best bit saving reached | best complex saving reached | +| ---: | ---: | ---: | +| 1 | `[22]` → 7.28397865314023e-4 (+6.54%) | `[11]` → 7.08793603125109e-4 (+1.12%) | +| 2 | `[19,21]` → 8.00024810534622e-4 (+17.02%) | `[1,8]` → 9.17460974044326e-4 (+30.89%) | +| 3 | `[1,7,21]` → 1.05220678470506e-3 (+53.91%) | `[1,2,18]` → 1.25531712077191e-3 (+79.10%) | +| 4 | `[1,3,13,21]` → 1.22799457745093e-3 (+79.62%) | `[1,2,3,9]` → 1.40686129974894e-3 (+100.72%) | +| 5 | `[1,3,13,21,22]` → 1.38023409118239e-3 (+101.89%) | `[1,2,3,4,19]` → 1.63407154980676e-3 (+133.13%) | + +Each side's column is the leader of that family count by the exact screening key, priced +exactly; the bit side's rank-1 masses (9.3% of its ledger) and the complex side's rank-1 +and rank-2 masses (11.0% and 10.0%) are the big movers, which is why the ladder is so +steep once the small families are gone. + +### 2b. One family deeper: where the model tops out on each side + +`beats.py --max-types 6` moves the screen one family further on both words (~157 s on +this machine, 1.7x the five-family screen; its artifact is `beats-six.json`). The +admissible space triples to 10,318 family +sets on the bit word and 2,725 on the complex one, and the ladder reads: + +| families | best bit saving | best complex saving | +| ---: | ---: | ---: | +| 5 | `[1,3,13,21,22]` → 1.38023409118239e-3 (+101.89%) | `[1,2,3,4,19]` → 1.63407154980676e-3 (+133.13%) | +| **6** | **`[1,3,13,20,21,22]` → 1.52739614292328e-3 (+123.42%)** | **`[1,2,3,8,15,18]` → 2.30539885681005e-3 (+228.91%)** | + +The two sides do not top out together: the six-family removals take 59.7% of the bit +ledger (33,599 banks) and 65.6% of the complex ledger (7,895 banks). Because the +headline is the *smaller* budget, the model's best pairing is bit six families with +complex four — `kappa = 1.5250667618335e-3` (**+123.23%**), 11 new residual types, +binding bit, removing 59.7% of the bit ledger and 33.8% of the complex one. The +complex side's extra hundred points are unspendable while the bit side is the lower +of the two. + +This is the same model as the four-family ladder one family deeper, so section 2's +caveats apply unchanged — and the growth is a warning about the model rather than +evidence about the word: each step removes a larger share of the paid dirt, and the +savings climb faster than the removed share because dropping small children also +shrinks the log budget `L`. + +Two facts fall out of the screen: + +* **Nearly any bit-side absorption clears the complex side**: 3,502 of the 3,512 + admissible sets do. The bit word can be lifted past 7.0092e-4 in hundreds of ways + — the family that has to move for a bigger headline is the *complex* one. +* **The best screened rung in this model is `+101.75%`**, at 9 new residual types: + (the best of the leaders of each family count, priced exactly; the screen is + exhaustive over sets of up to five families per word, but the global optimum over + all sets is not established, so this is a leader, not a proven maximum) + bit absorbs ranks {1, 3, 13, 21, 22} and complex absorbs {1, 2, 3, 9}, + `kappa = 1.3783316708213e-3`, binding bit, 33,261 banks. The pinned ladder's own + best is `+79.5%` (`1.2264884e-3`, 8 types) — the same model capped at four + families per word, so this is the pinned screen extended one family deep, not a + different construction. The four-family bit rung reproduces the pinned + `1.22799457745093e-3` to the last digit. + +**What the modelled tier assumes** (re-derived in `beats.json → audit`): + +1. **Every family left in the frontier word is retained dirt.** #207 banked the + rank-60 *entrance exteriors*, and the frontier profile no longer carries them + (bit maxchild 22, complex maxchild 20). So the exteriors are already spent, and + every rung here removes *interior* children — the top rung removes **51.8% of + the bit ledger and 33.8% of the complex ledger**. +2. **Each absorbed family needs a new residual type**, which the supplier's proof + reserves for the future. The queue's own allocation records exactly this verdict + for its single-family rung: *"needs the new residual type the supplier's proof + reserves; not buildable with the construction as published."* +3. **The rank-free rule is certified precedent only for one exterior**, of one + child per selected gauge, not for interior dirt. +4. The bank charts, the normalizers, the `F2` and defining-integer columns and the + per-bank prime witnesses are the supplier's harness and are not built here. + +So the modelled tier is a **priced upper bracket**, not a route. What it is good +for is the requirement side: it says which *family counts* each target demands, and +it shows the model's own curvature — one family buys +2.2% at the bottom of the +ladder and +6.5% at the top, because absorbing a larger family removes more rank +mass from a ledger of fixed size. + +### 3. The routes that do not need a bank at all + +* **A new bit word.** PR192 bounds the bit word *family*'s frame-layout ceiling at + `7.010e-4`, and the sinks and reuse pairs on the current bit word are maximal + (all 34 rank-21 sinks, all 1,760 pairs). A perfect new bit word therefore reaches + `7.010e-4 > 7.0092e-4` — it clears the complex side and buys **+2.523%**, no + better than the two-family bank rung, at the cost of a new word. Every bit-side + PR in the queue is bounded the same way. +* **A new complex network.** This is where the headroom actually lives. The queue's + own analysis of this complex word family (`m = 66`, deficit 1,320) puts the + implied log budget `L1 = deficit/(m·W·kappa)` at about 2.27 and the + mass-at-largest-child relaxation of the same `(m, W, s)` at a root near `9.8e-2`, + roughly 150x the current saving; that is a different (relaxation) model, quoted + rather than recomputed here, and it says the pinned complex *construction* is the + wall, not its arithmetic. +* **Assembly and grid refinements — do not bother.** The assembly's loss is `a²` + (4.7e-7, which is why `kappa ~ a/(1+a)`) plus the backoff; the grid is already + `10^-16`; re-pricing at a finer grid, or tightening the `1e-9`/`1e-10` steps the + older ladder carried, is worth less than `1e-4` relative here. + +## What each gain needs, exactly + +`beats.json → requirements`, for the smaller side saving the assembly has to see: + +| target | needed side saving | over today's binding side | +| --- | ---: | ---: | +| beat the frontier by 0.1% | 6.84341648710e-4 | +0.100% | +| by 1% | 6.90498819211e-4 | +1.001% | +| by 5% | 7.17864938186e-4 | +5.004% | +| by 10% | 7.52074691816e-4 | +10.008% | +| by 25% | 8.54717987759e-4 | +25.021% | +| by 50% | 1.02583694557e-3 | +50.051% | +| `kappa = 2^-10` | 9.77517106549e-4 | +42.983% | +| `kappa = 1e-3` | 1.00100100100e-3 | +46.419% | + +Within the bank model both sides clear all of these; that is a statement about the +model, not about the construction. + +## Verification boundary + +* Reproduced exactly from the certificate's own rows: `a_complex` to the last digit, + `a_bit` to 16 significant digits (`1.4e-16` absolute, `2.1e-13` relative), and the + certificate's `kappa` exactly, on a grid discovered by search rather than assumed. +* The ladder's zero point is the same frontier within one `10^-16` grid step, and + every rung is priced by the supplier's own enclosure implementation + (`references/pr200/interval_moment.py`, vendored; both pins are hashed against + [SOURCE.json](SOURCE.json) at the top of every run, and the run fails on a mismatch). +* The four-family bit rung and the four-family complex rung reproduce the pinned + ladder's values (`1.22799457745093e-3` and `1.406861298932255e-3`) exactly, in the + paid-convention field `beats.json` records beside every rung. +* The six-family leaders were re-derived independently of the screening code: their + absorbed rows were rebuilt from the certificate and re-priced, and their savings + matched the artifact under both conventions, as did the best rung's kappa. +* [check_docs.py](check_docs.py) re-checks every number this README and + `INSTANTIATE.md` quote against the three artifacts — 41 table numbers and 44 + required claims on the current revision — and fails if a value is altered or a + claim disappears. +* [instantiate.py](instantiate.py) re-derives the bank schedule of the +2.167% rung + from the same rows and turns the vendored bank proof into the checklist in + [INSTANTIATE.md](INSTANTIATE.md). +* **Not claimed:** any bank construction, any new residual type, any replay of the + physical words, any contributor verifier or upstream CI run. The rungs are priced + targets; the gain on the *headline* is conditional on the bank harness the + supplier's proof describes but does not instantiate. + +## Reproduce + +```sh +python3 -B beats.py # ~91 s, writes beats.json (five families per word) +python3 -B beats.py --check # byte-for-byte comparison with it +python3 -B beats.py --max-types 6 --out beats-six.json # ~157 s, one family deeper +python3 -B beats.py --max-types 6 --out beats-six.json --check # ~157 s, same comparison +python3 -B instantiate.py # ~2 s, writes instantiate.json +python3 -B instantiate.py --check +``` + +Every `--check` re-runs the whole screen and compares its text with the committed +artifact byte for byte, naming the file it compared: the two depths are checked +separately, and `--check` is the only way to tell the six-family artifact from the +five-family one. The six-family screen is the expensive one by 1.7x; `instantiate.py` +is seconds. diff --git a/research/frontier-beat-2026-10-09/SOURCE.json b/research/frontier-beat-2026-10-09/SOURCE.json new file mode 100644 index 0000000000..32cbb63ae2 --- /dev/null +++ b/research/frontier-beat-2026-10-09/SOURCE.json @@ -0,0 +1,34 @@ +{ + "status": "Read-only analysis. No pinned artifact of any other package is modified; the two files below are vendored verbatim and are verified by sha256 on every run of beats.py.", + "pins": [ + { + "path": "references/pr200/interval_moment.py", + "role": "The supplier's exact interval and exponential enclosures (PR200's own arithmetic). Every number in beats.json is computed with this module; no floating point enters a check.", + "sha256": "9d3d1d28bfb3375958995205179b171fb65c70a3792cf9f7a21ef5ee54f5460b", + "upstream": "CrocSwap/integer-mult-bounds, PR200 (research package) references/intervals used by bit/prove.py", + "license": "as published in the upstream repository" + }, + { + "path": "references/queue/pr207-coordinated-crossover.certificate.json", + "role": "The frontier certificate: the two side child ledgers (bit_profile, complex_profile), the two published side savings (a_bit, a_complex), the published kappa and the assembly status. It is the object this package reproduces and prices against.", + "sha256": "f4e30cca369fb014b729df870ca3716cc0f1e2297b9f265341492cba85a14aeb", + "upstream": "CrocSwap/integer-mult-bounds, queue snapshot 2026-10-09, PR207 coordinated crossover", + "license": "as published in the upstream repository" + }, + { + "path": "references/queue/coordinated-bank-proof.md", + "role": "The supplier's published finite bank proof for the physical bit word: the projector partition that fills a width-72 bank, the universal disjoint-projector algebra, the 144 two-bank address-map columns over F2 and Z, the exact removed exterior set (the 2,200 rank-60 gauges), the resulting stock/mass/deficit, and the conditional interfaces it does not discharge. instantiate.py reads this proof item by item against the rank-6 rung.", + "sha256": "5136565f1298b73436b164b3e9307ba00a2659da41a3a64defde4b41975dc441", + "upstream": "CrocSwap/integer-mult-bounds, research/coordinated-frames-and-entrance-banks/BANK-PROOF.md (PR186 lineage, as carried into PR205/PR206/PR207)", + "license": "as published in the upstream repository" + } + ], + "method_provenance": { + "assembly_rule": "kappa = floor(min(a_bit, a_complex)/(1 + min(...))) on the certificate's own 10^-16 grid, discovered by search in beats.py rather than assumed", + "saving_rule": "the largest 10^-18 grid point whose paid moment pays; the certificate prices its bit side with PR200's rare-class fallback term and its complex side without it, and each is reproduced exactly under its own convention", + "bank_rule": "a family is bankable when its own blocks tile a width-m bank (m % rank == 0) and its own volume is a whole number of banks; the wider screen keeps only the volume condition, which is what the queue's certified banked rows satisfy", + "signed_roots": "the contraction and bank models, their validation against the queue's published banked rows, and the closed-form bank proof are PR184/PR185/PR197/PR200/PR205/PR206/PR207's, as carried in the supplier's package; this package re-implements only the arithmetic it prices with", + "instantiation_read": "instantiate.py derives the block/bank schedule of a candidate absorption from the certificate's own histogram and maps it onto the items of the vendored bank proof; it builds no bank, chart or witness" + }, + "local_environment": "Windows checkout of CrocSwap/integer-mult-bounds (branch ordered-chain-h23), Python 3.14, beats.py run from the repository root" +} diff --git a/research/frontier-beat-2026-10-09/beats-six.json b/research/frontier-beat-2026-10-09/beats-six.json new file mode 100644 index 0000000000..9c9fee990a --- /dev/null +++ b/research/frontier-beat-2026-10-09/beats-six.json @@ -0,0 +1,829 @@ +{ + "audit": { + "arithmetic": "reproduced from scratch: the row identity after absorption, the whole-bank volume condition, the paid moment's adjacent-grid exclusion and the assembly", + "assumptions": [ + "Every family still in the frontier word is retained dirt: #207 banked the rank-60 entrance exteriors, which the frontier profile no longer carries (bit maxchild 22, complex maxchild 20). So this rung removes interior children, and no family removed here has a published bank proof.", + "The model needs one new residual type per absorbed family, which the supplier's proof reserves for the future: the queue's own allocation records that verdict for the single-family rung.", + "The absorbed family's rank is treated as free, which is what #205/#206/#207 certified for rank 60 on width 72 -- an exterior of one child per selected gauge, not interior dirt.", + "Bank charts, normalizers, the F2 and defining-integer columns and per-bank prime witnesses are the supplier's harness and are not built here." + ], + "rung": { + "banks": 38395, + "binding": "bit", + "bit_families": [ + 1, + 3, + 13, + 20, + 21, + 22 + ], + "bit_saving": "381849035730821/250000000000000000", + "bit_share_of_ledger": 0.5965590303259866, + "complex_families": [ + 1, + 2, + 3, + 4, + 19 + ], + "complex_saving": "326814309961353/200000000000000000", + "complex_share_of_ledger": 0.3986037234042553, + "gain": "8418763067969/6831904550366", + "kappa": "3050133523667/2000000000000000", + "types": 11 + }, + "verdict": "the arithmetic is exact and the rung is priced, but it is a model: it assumes new residual types that the published bank proof reserves and that no package enumerates." + }, + "best_rung": { + "banks": 38395, + "binding": "bit", + "bit_families": [ + 1, + 3, + 13, + 20, + 21, + 22 + ], + "complex_families": [ + 1, + 2, + 3, + 4, + 19 + ], + "gain": "8418763067969/6831904550366", + "kappa": "3050133523667/2000000000000000", + "types": 11 + }, + "frontier": { + "binding": "bit", + "bit_saving": "136731504666219/200000000000000000", + "complex_saving": "700918443859411/1000000000000000000", + "kappa": "3415952275183/5000000000000000", + "kappa_decimal": 0.0006831904550366, + "published": "1366380910073/2000000000000000", + "sides": { + "bit": { + "W": 56402, + "children": 879231, + "deficit": 5808, + "families": 22, + "m": 72, + "rank_mass": 4055136, + "saving": "136731504666219/200000000000000000", + "tiles_the_bank": [ + 6, + 8, + 18 + ] + }, + "complex": { + "W": 12052, + "children": 213147, + "deficit": 1320, + "families": 20, + "m": 66, + "rank_mass": 794112, + "saving": "700918443859411/1000000000000000000", + "tiles_the_bank": [ + 11 + ] + } + } + }, + "limits": [ + "No contributor verifier, CI run or upstream proof package is re-executed: the rows are the frontier certificate's own recorded ledgers and the arithmetic here is this package's.", + "The strict tier is the only tier that needs no block shape the word does not already use; the screen's larger rungs treat an absorbed family's rank as free, which is certified precedent only for an exterior of the rank-60 kind.", + "A rung's cost is measured in new residual types (families absorbed) because that is what the supplier's harness would have to instantiate; it ignores chart, normalizer and witness work entirely.", + "The pinned ladder in the supplier's package prices both sides with the rare-class fallback, so its values sit a few 1e-10 relative below the convention-matched values recorded here; both are given for every rung." + ], + "method": "PR200's exact interval and exponential enclosures on the frontier certificate's rows; the paid moment as the screen (one evaluation per candidate, rigorous, no bisection) and the adjacent-grid bisection for the prices; the assembly rule taken verbatim from the certificate it reproduces", + "requirements": [ + { + "binding_side_after": "228041792869/227885841110365", + "label": "beat the frontier by 0.1%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "342170824354851/500000000000000000", + "needed_side_saving_decimal": 0.000684341648709702, + "over_binding_side": "228041792869/227885841110365", + "over_other_side": "-16576795149709/700918443859411", + "target": "3419368227458183/5000000000000000000", + "target_decimal": 0.0006838736454916366 + }, + { + "binding_side_after": "2280431960132/227885841110365", + "label": "beat the frontier by 1%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "690498819211491/1000000000000000000", + "needed_side_saving_decimal": 0.000690498819211491, + "over_binding_side": "2280431960132/227885841110365", + "over_other_side": "-10419624647920/700918443859411", + "target": "345011179793483/500000000000000000", + "target_decimal": 0.000690022359586966 + }, + { + "binding_side_after": "11402471618266/227885841110365", + "label": "beat the frontier by 5%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "717864938185893/1000000000000000000", + "needed_side_saving_decimal": 0.000717864938185893, + "over_binding_side": "11402471618266/227885841110365", + "over_other_side": "16946494326482/700918443859411", + "target": "71734997778843/100000000000000000", + "target_decimal": 0.00071734997778843 + }, + { + "binding_side_after": "68417168485181/683657523331095", + "label": "beat the frontier by 10%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "188018672954069/250000000000000000", + "needed_side_saving_decimal": 0.000752074691816276, + "over_binding_side": "68417168485181/683657523331095", + "over_other_side": "51156247956865/700918443859411", + "target": "37575475027013/50000000000000000", + "target_decimal": 0.00075150950054026 + }, + { + "binding_side_after": "171060464428387/683657523331095", + "label": "beat the frontier by 25%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "427358993879741/500000000000000000", + "needed_side_saving_decimal": 0.000854717987759482, + "over_binding_side": "171060464428387/683657523331095", + "over_other_side": "153799543900071/700918443859411", + "target": "3415952275183/4000000000000000", + "target_decimal": 0.00085398806879575 + }, + { + "binding_side_after": "342179422238261/683657523331095", + "label": "beat the frontier by 50%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "256459236392339/250000000000000000", + "needed_side_saving_decimal": 0.001025836945569356, + "over_binding_side": "342179422238261/683657523331095", + "over_other_side": "324918501709945/700918443859411", + "target": "10247856825549/10000000000000000", + "target_decimal": 0.0010247856825549 + }, + { + "binding_side_after": "317343477669907/683657523331095", + "label": "kappa = 1/1000", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "500500500500501/500000000000000000", + "needed_side_saving_decimal": 0.001001001001001002, + "over_binding_side": "317343477669907/683657523331095", + "over_other_side": "300082557141591/700918443859411", + "target": "1/1000", + "target_decimal": 0.001 + }, + { + "binding_side_after": "19590638881218/45577168222073", + "label": "kappa = 2^-10", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "195503421309873/200000000000000000", + "needed_side_saving_decimal": 0.000977517106549365, + "over_binding_side": "19590638881218/45577168222073", + "over_other_side": "276598662689954/700918443859411", + "target": "1/1024", + "target_decimal": 0.0009765625 + } + ], + "screen": { + "bit": { + "admissible": 10318, + "best_by_size": { + "1": { + "banks": 6116, + "families": [ + 22 + ], + "gain_on_this_side": "44740341982928/683657523331095", + "rigorous_beats_target": true, + "saving": "728397865314023/1000000000000000000", + "saving_paid": "728397865314023/1000000000000000000", + "saving_without_fallback": "5827182936843/8000000000000000", + "share": 0.10859117918609881, + "taken": 440352, + "types": 1 + }, + "2": { + "banks": 13877, + "families": [ + 19, + 21 + ], + "gain_on_this_side": "38789095734509/227885841110365", + "rigorous_beats_target": true, + "saving": "400012405267311/500000000000000000", + "saving_paid": "400012405267311/500000000000000000", + "saving_without_fallback": "800024812438693/1000000000000000000", + "share": 0.24638976349991715, + "taken": 999144, + "types": 2 + }, + "3": { + "banks": 19534, + "families": [ + 1, + 7, + 21 + ], + "gain_on_this_side": "24569950758264/45577168222073", + "rigorous_beats_target": true, + "saving": "210441356941011/200000000000000000", + "saving_paid": "210441356941011/200000000000000000", + "saving_without_fallback": "263051696510933/250000000000000000", + "share": 0.3468312776686158, + "taken": 1406448, + "types": 3 + }, + "4": { + "banks": 23083, + "families": [ + 1, + 3, + 13, + 21 + ], + "gain_on_this_side": "108867410823967/136731504666219", + "rigorous_beats_target": true, + "saving": "122799457745093/100000000000000000", + "saving_paid": "122799457745093/100000000000000000", + "saving_without_fallback": "1227994578715841/1000000000000000000", + "share": 0.4098447006462915, + "taken": 1661976, + "types": 4 + }, + "5": { + "banks": 29199, + "families": [ + 1, + 3, + 13, + 21, + 22 + ], + "gain_on_this_side": "696576567851293/683657523331095", + "rigorous_beats_target": true, + "saving": "345058522795597/250000000000000000", + "saving_paid": "345058522795597/250000000000000000", + "saving_without_fallback": "1380234092525411/1000000000000000000", + "share": 0.5184358798323904, + "taken": 2102328, + "types": 5 + }, + "6": { + "banks": 33599, + "families": [ + 1, + 3, + 13, + 20, + 21, + 22 + ], + "gain_on_this_side": "843738619592189/683657523331095", + "rigorous_beats_target": true, + "saving": "381849035730821/250000000000000000", + "saving_paid": "381849035730821/250000000000000000", + "saving_without_fallback": "305479228868121/200000000000000000", + "share": 0.5965590303259866, + "taken": 2419128, + "types": 6 + } + }, + "cheapest_clearer": { + "banks": 6116, + "families": [ + 22 + ], + "gain_on_this_side": "44740341982928/683657523331095", + "rigorous_beats_target": true, + "saving": "728397865314023/1000000000000000000", + "saving_paid": "728397865314023/1000000000000000000", + "saving_without_fallback": "5827182936843/8000000000000000", + "share": 0.10859117918609881, + "taken": 440352, + "types": 1 + }, + "clearers": 10308, + "clearers_by_size": { + "1": 3, + "2": 34, + "3": 179, + "4": 748, + "5": 2538, + "6": 6806 + }, + "single_family": { + "banks": 6116, + "families": [ + 22 + ], + "gain_on_this_side": "44740341982928/683657523331095", + "rigorous_beats_target": true, + "saving": "728397865314023/1000000000000000000", + "saving_paid": "728397865314023/1000000000000000000", + "saving_without_fallback": "5827182936843/8000000000000000", + "share": 0.10859117918609881, + "taken": 440352, + "types": 1 + }, + "target": "700918443859411/1000000000000000000", + "target_source": "complex" + }, + "complex": { + "admissible": 2725, + "best_by_size": { + "1": { + "banks": 177, + "families": [ + 11 + ], + "gain_on_this_side": "7875159265698/700918443859411", + "rigorous_beats_target": true, + "saving": "708793603125109/1000000000000000000", + "saving_paid": "708793601534531/1000000000000000000", + "saving_without_fallback": "708793603125109/1000000000000000000", + "share": 0.014710771276595746, + "taken": 11682, + "types": 1 + }, + "2": { + "banks": 1883, + "families": [ + 1, + 8 + ], + "gain_on_this_side": "2741044685885/8872385365309", + "rigorous_beats_target": true, + "saving": "458730487022163/500000000000000000", + "saving_paid": "458730486434321/500000000000000000", + "saving_without_fallback": "458730487022163/500000000000000000", + "share": 0.15649933510638298, + "taken": 124278, + "types": 2 + }, + "3": { + "banks": 4704, + "families": [ + 1, + 2, + 18 + ], + "gain_on_this_side": "554398676912496/700918443859411", + "rigorous_beats_target": true, + "saving": "1255317120771907/1000000000000000000", + "saving_paid": "3138292799341/2500000000000000", + "saving_without_fallback": "1255317120771907/1000000000000000000", + "share": 0.39095744680851063, + "taken": 310464, + "types": 3 + }, + "4": { + "banks": 4062, + "families": [ + 1, + 2, + 3, + 9 + ], + "gain_on_this_side": "705942855889532/700918443859411", + "rigorous_beats_target": true, + "saving": "1406861299748943/1000000000000000000", + "saving_paid": "281372259786451/200000000000000000", + "saving_without_fallback": "1406861299748943/1000000000000000000", + "share": 0.33759973404255317, + "taken": 268092, + "types": 4 + }, + "5": { + "banks": 4796, + "families": [ + 1, + 2, + 3, + 4, + 19 + ], + "gain_on_this_side": "933153105947354/700918443859411", + "rigorous_beats_target": true, + "saving": "326814309961353/200000000000000000", + "saving_paid": "326814309812561/200000000000000000", + "saving_without_fallback": "326814309961353/200000000000000000", + "share": 0.3986037234042553, + "taken": 316536, + "types": 5 + }, + "6": { + "banks": 7895, + "families": [ + 1, + 2, + 3, + 8, + 15, + 18 + ], + "gain_on_this_side": "1604480412950641/700918443859411", + "rigorous_beats_target": true, + "saving": "576349714202513/250000000000000000", + "saving_paid": "1152699427941363/500000000000000000", + "saving_without_fallback": "576349714202513/250000000000000000", + "share": 0.6561668882978723, + "taken": 521070, + "types": 6 + } + }, + "cheapest_clearer": { + "banks": 177, + "families": [ + 11 + ], + "gain_on_this_side": "7875159265698/700918443859411", + "rigorous_beats_target": true, + "saving": "708793603125109/1000000000000000000", + "saving_paid": "708793601534531/1000000000000000000", + "saving_without_fallback": "708793603125109/1000000000000000000", + "share": 0.014710771276595746, + "taken": 11682, + "types": 1 + }, + "clearers": 2725, + "clearers_by_size": { + "1": 3, + "2": 10, + "3": 56, + "4": 231, + "5": 691, + "6": 1734 + }, + "single_family": { + "banks": 177, + "families": [ + 11 + ], + "gain_on_this_side": "7875159265698/700918443859411", + "rigorous_beats_target": true, + "saving": "708793603125109/1000000000000000000", + "saving_paid": "708793601534531/1000000000000000000", + "saving_without_fallback": "708793603125109/1000000000000000000", + "share": 0.014710771276595746, + "taken": 11682, + "types": 1 + }, + "target": "136731504666219/200000000000000000", + "target_source": "bit" + } + }, + "source": { + "arithmetic": "references/pr200/interval_moment.py", + "certificate": "references/queue/pr207-coordinated-crossover.certificate.json", + "kappa_grid": 10000000000000000, + "saving_grid": 1000000000000000000 + }, + "status": "MODEL, NOT CONSTRUCTED. Every number here is exact arithmetic on the frontier certificate's own child ledgers; the bank construction, its charts and its witnesses belong to the supplier's harness and are not built. Each rung is a priced target.", + "strict_ladder": [ + { + "banks": 2001, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 1824, + "bit_families": [ + 6, + 8 + ], + "bit_saving": "141899511517939/200000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "251011155541/6831904550366", + "kappa": "7082915705907/10000000000000000", + "types": 3 + }, + { + "banks": 3000, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 2823, + "bit_families": [ + 6, + 8, + 18 + ], + "bit_saving": "718242431279183/1000000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "251011155541/6831904550366", + "kappa": "7082915705907/10000000000000000", + "types": 4 + }, + { + "banks": 2184, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 2007, + "bit_families": [ + 6, + 18 + ], + "bit_saving": "706958372104771/1000000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "116342400047/3415952275183", + "kappa": "353229467523/500000000000000", + "types": 3 + }, + { + "banks": 1992, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 1815, + "bit_families": [ + 8, + 18 + ], + "bit_saving": "87821801129279/125000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "13493349823/487993182169", + "kappa": "438800715493/625000000000000", + "types": 3 + }, + { + "banks": 1824, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 1824, + "bit_families": [ + 6, + 8 + ], + "bit_saving": "141899511517939/200000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "172370462685/6831904550366", + "kappa": "7004275013051/10000000000000000", + "types": 2 + }, + { + "banks": 2007, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 2007, + "bit_families": [ + 6, + 18 + ], + "bit_saving": "706958372104771/1000000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "172370462685/6831904550366", + "kappa": "7004275013051/10000000000000000", + "types": 2 + }, + { + "banks": 1815, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 1815, + "bit_families": [ + 8, + 18 + ], + "bit_saving": "87821801129279/125000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "172370462685/6831904550366", + "kappa": "7004275013051/10000000000000000", + "types": 2 + }, + { + "banks": 2823, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 2823, + "bit_families": [ + 6, + 8, + 18 + ], + "bit_saving": "718242431279183/1000000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "172370462685/6831904550366", + "kappa": "7004275013051/10000000000000000", + "types": 3 + }, + { + "banks": 1008, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 1008, + "bit_families": [ + 6 + ], + "bit_saving": "174621103751517/250000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "21152028615/975986364338", + "kappa": "6979968750671/10000000000000000", + "types": 1 + }, + { + "banks": 1185, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 1008, + "bit_families": [ + 6 + ], + "bit_saving": "174621103751517/250000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "21152028615/975986364338", + "kappa": "6979968750671/10000000000000000", + "types": 2 + }, + { + "banks": 816, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 816, + "bit_families": [ + 8 + ], + "bit_saving": "347102294204153/500000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "105325476801/6831904550366", + "kappa": "6937230027167/10000000000000000", + "types": 1 + }, + { + "banks": 993, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 816, + "bit_families": [ + 8 + ], + "bit_saving": "347102294204153/500000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "105325476801/6831904550366", + "kappa": "6937230027167/10000000000000000", + "types": 2 + }, + { + "banks": 999, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 999, + "bit_families": [ + 18 + ], + "bit_saving": "691773537862501/1000000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "5789187870/487993182169", + "kappa": "3456476590273/5000000000000000", + "types": 1 + }, + { + "banks": 1176, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 999, + "bit_families": [ + 18 + ], + "bit_saving": "691773537862501/1000000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "5789187870/487993182169", + "kappa": "3456476590273/5000000000000000", + "types": 2 + }, + { + "banks": 0, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 0, + "bit_families": [], + "bit_saving": "136731504666219/200000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "0", + "kappa": "3415952275183/5000000000000000", + "types": 0 + }, + { + "banks": 177, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 0, + "bit_families": [], + "bit_saving": "136731504666219/200000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "0", + "kappa": "3415952275183/5000000000000000", + "types": 1 + } + ], + "validations": { + "a_bit": { + "certificate": "4375408149318106538866216854671930632866706725794304565219529058788314814256861959639757/6400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "convention": "child ledger plus PR200's rare-class fallback", + "delta": "901461133783145328069367133293274205695434780470941211685185743138040360243/6400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "exact": false, + "note": "the certificate carries its own higher-precision value of this quantity; the residual is recorded, not asserted away", + "recomputed": "136731504666219/200000000000000000", + "relative_delta": "6592929230053745399832586693131146510202180498142949721323097/31999999999993407070769946254600167413306868853489797819501857050278676903" + }, + "a_complex": { + "certificate": "700918443859411/1000000000000000000", + "convention": "child ledger only, no fallback term", + "exact": true, + "recomputed": "700918443859411/1000000000000000000" + }, + "conventions": { + "bit_absolute_difference": "-1720321/1000000000000000000", + "bit_other_convention": "85457190631427/125000000000000000", + "complex_absolute_difference": "1580753/1000000000000000000", + "complex_other_convention": "350459221139329/500000000000000000", + "note": "the certificate prices its two sides differently - the bit side includes PR200's rare-class fallback, the complex side does not - and each is reproduced exactly under its own convention" + }, + "kappa": { + "certificate": "1366380910073/2000000000000000", + "exact": true, + "grid": "10^-16", + "ladder_zero_point": { + "delta_from_certificate": "1/10000000000000000", + "grid_steps": 1, + "note": "the ladder is priced from the rows this package recomputed; its zero point sits this many grid steps from the certificate's own value, entirely in the last digit of the bit side's sixteen-significant-digit saving", + "value": "3415952275183/5000000000000000" + }, + "recomputed": "1366380910073/2000000000000000", + "rule": "floor(min(a_bit, a_complex)/(1 + min(...))) on the certificate's own side values, at its own grid" + } + } +} diff --git a/research/frontier-beat-2026-10-09/beats.json b/research/frontier-beat-2026-10-09/beats.json new file mode 100644 index 0000000000..1857fdba1f --- /dev/null +++ b/research/frontier-beat-2026-10-09/beats.json @@ -0,0 +1,785 @@ +{ + "audit": { + "arithmetic": "reproduced from scratch: the row identity after absorption, the whole-bank volume condition, the paid moment's adjacent-grid exclusion and the assembly", + "assumptions": [ + "Every family still in the frontier word is retained dirt: #207 banked the rank-60 entrance exteriors, which the frontier profile no longer carries (bit maxchild 22, complex maxchild 20). So this rung removes interior children, and no family removed here has a published bank proof.", + "The model needs one new residual type per absorbed family, which the supplier's proof reserves for the future: the queue's own allocation records that verdict for the single-family rung.", + "The absorbed family's rank is treated as free, which is what #205/#206/#207 certified for rank 60 on width 72 -- an exterior of one child per selected gauge, not interior dirt.", + "Bank charts, normalizers, the F2 and defining-integer columns and per-bank prime witnesses are the supplier's harness and are not built here." + ], + "rung": { + "banks": 33261, + "binding": "bit", + "bit_families": [ + 1, + 3, + 13, + 21, + 22 + ], + "bit_saving": "345058522795597/250000000000000000", + "bit_share_of_ledger": 0.5184358798323904, + "complex_families": [ + 1, + 2, + 3, + 9 + ], + "complex_saving": "1406861299748943/1000000000000000000", + "complex_share_of_ledger": 0.33759973404255317, + "gain": "6951412157847/6831904550366", + "kappa": "13783316708213/10000000000000000", + "types": 9 + }, + "verdict": "the arithmetic is exact and the rung is priced, but it is a model: it assumes new residual types that the published bank proof reserves and that no package enumerates." + }, + "best_rung": { + "banks": 33261, + "binding": "bit", + "bit_families": [ + 1, + 3, + 13, + 21, + 22 + ], + "complex_families": [ + 1, + 2, + 3, + 9 + ], + "gain": "6951412157847/6831904550366", + "kappa": "13783316708213/10000000000000000", + "types": 9 + }, + "frontier": { + "binding": "bit", + "bit_saving": "136731504666219/200000000000000000", + "complex_saving": "700918443859411/1000000000000000000", + "kappa": "3415952275183/5000000000000000", + "kappa_decimal": 0.0006831904550366, + "published": "1366380910073/2000000000000000", + "sides": { + "bit": { + "W": 56402, + "children": 879231, + "deficit": 5808, + "families": 22, + "m": 72, + "rank_mass": 4055136, + "saving": "136731504666219/200000000000000000", + "tiles_the_bank": [ + 6, + 8, + 18 + ] + }, + "complex": { + "W": 12052, + "children": 213147, + "deficit": 1320, + "families": 20, + "m": 66, + "rank_mass": 794112, + "saving": "700918443859411/1000000000000000000", + "tiles_the_bank": [ + 11 + ] + } + } + }, + "limits": [ + "No contributor verifier, CI run or upstream proof package is re-executed: the rows are the frontier certificate's own recorded ledgers and the arithmetic here is this package's.", + "The strict tier is the only tier that needs no block shape the word does not already use; the screen's larger rungs treat an absorbed family's rank as free, which is certified precedent only for an exterior of the rank-60 kind.", + "A rung's cost is measured in new residual types (families absorbed) because that is what the supplier's harness would have to instantiate; it ignores chart, normalizer and witness work entirely.", + "The pinned ladder in the supplier's package prices both sides with the rare-class fallback, so its values sit a few 1e-10 relative below the convention-matched values recorded here; both are given for every rung." + ], + "method": "PR200's exact interval and exponential enclosures on the frontier certificate's rows; the paid moment as the screen (one evaluation per candidate, rigorous, no bisection) and the adjacent-grid bisection for the prices; the assembly rule taken verbatim from the certificate it reproduces", + "requirements": [ + { + "binding_side_after": "228041792869/227885841110365", + "label": "beat the frontier by 0.1%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "342170824354851/500000000000000000", + "needed_side_saving_decimal": 0.000684341648709702, + "over_binding_side": "228041792869/227885841110365", + "over_other_side": "-16576795149709/700918443859411", + "target": "3419368227458183/5000000000000000000", + "target_decimal": 0.0006838736454916366 + }, + { + "binding_side_after": "2280431960132/227885841110365", + "label": "beat the frontier by 1%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "690498819211491/1000000000000000000", + "needed_side_saving_decimal": 0.000690498819211491, + "over_binding_side": "2280431960132/227885841110365", + "over_other_side": "-10419624647920/700918443859411", + "target": "345011179793483/500000000000000000", + "target_decimal": 0.000690022359586966 + }, + { + "binding_side_after": "11402471618266/227885841110365", + "label": "beat the frontier by 5%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "717864938185893/1000000000000000000", + "needed_side_saving_decimal": 0.000717864938185893, + "over_binding_side": "11402471618266/227885841110365", + "over_other_side": "16946494326482/700918443859411", + "target": "71734997778843/100000000000000000", + "target_decimal": 0.00071734997778843 + }, + { + "binding_side_after": "68417168485181/683657523331095", + "label": "beat the frontier by 10%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "188018672954069/250000000000000000", + "needed_side_saving_decimal": 0.000752074691816276, + "over_binding_side": "68417168485181/683657523331095", + "over_other_side": "51156247956865/700918443859411", + "target": "37575475027013/50000000000000000", + "target_decimal": 0.00075150950054026 + }, + { + "binding_side_after": "171060464428387/683657523331095", + "label": "beat the frontier by 25%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "427358993879741/500000000000000000", + "needed_side_saving_decimal": 0.000854717987759482, + "over_binding_side": "171060464428387/683657523331095", + "over_other_side": "153799543900071/700918443859411", + "target": "3415952275183/4000000000000000", + "target_decimal": 0.00085398806879575 + }, + { + "binding_side_after": "342179422238261/683657523331095", + "label": "beat the frontier by 50%", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "256459236392339/250000000000000000", + "needed_side_saving_decimal": 0.001025836945569356, + "over_binding_side": "342179422238261/683657523331095", + "over_other_side": "324918501709945/700918443859411", + "target": "10247856825549/10000000000000000", + "target_decimal": 0.0010247856825549 + }, + { + "binding_side_after": "317343477669907/683657523331095", + "label": "kappa = 1/1000", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "500500500500501/500000000000000000", + "needed_side_saving_decimal": 0.001001001001001002, + "over_binding_side": "317343477669907/683657523331095", + "over_other_side": "300082557141591/700918443859411", + "target": "1/1000", + "target_decimal": 0.001 + }, + { + "binding_side_after": "19590638881218/45577168222073", + "label": "kappa = 2^-10", + "met_by_rigorous_screen": { + "bit": true, + "complex": true + }, + "needed_side_saving": "195503421309873/200000000000000000", + "needed_side_saving_decimal": 0.000977517106549365, + "over_binding_side": "19590638881218/45577168222073", + "over_other_side": "276598662689954/700918443859411", + "target": "1/1024", + "target_decimal": 0.0009765625 + } + ], + "screen": { + "bit": { + "admissible": 3512, + "best_by_size": { + "1": { + "banks": 6116, + "families": [ + 22 + ], + "gain_on_this_side": "44740341982928/683657523331095", + "rigorous_beats_target": true, + "saving": "728397865314023/1000000000000000000", + "saving_paid": "728397865314023/1000000000000000000", + "saving_without_fallback": "5827182936843/8000000000000000", + "share": 0.10859117918609881, + "taken": 440352, + "types": 1 + }, + "2": { + "banks": 13877, + "families": [ + 19, + 21 + ], + "gain_on_this_side": "38789095734509/227885841110365", + "rigorous_beats_target": true, + "saving": "400012405267311/500000000000000000", + "saving_paid": "400012405267311/500000000000000000", + "saving_without_fallback": "800024812438693/1000000000000000000", + "share": 0.24638976349991715, + "taken": 999144, + "types": 2 + }, + "3": { + "banks": 19534, + "families": [ + 1, + 7, + 21 + ], + "gain_on_this_side": "24569950758264/45577168222073", + "rigorous_beats_target": true, + "saving": "210441356941011/200000000000000000", + "saving_paid": "210441356941011/200000000000000000", + "saving_without_fallback": "263051696510933/250000000000000000", + "share": 0.3468312776686158, + "taken": 1406448, + "types": 3 + }, + "4": { + "banks": 23083, + "families": [ + 1, + 3, + 13, + 21 + ], + "gain_on_this_side": "108867410823967/136731504666219", + "rigorous_beats_target": true, + "saving": "122799457745093/100000000000000000", + "saving_paid": "122799457745093/100000000000000000", + "saving_without_fallback": "1227994578715841/1000000000000000000", + "share": 0.4098447006462915, + "taken": 1661976, + "types": 4 + }, + "5": { + "banks": 29199, + "families": [ + 1, + 3, + 13, + 21, + 22 + ], + "gain_on_this_side": "696576567851293/683657523331095", + "rigorous_beats_target": true, + "saving": "345058522795597/250000000000000000", + "saving_paid": "345058522795597/250000000000000000", + "saving_without_fallback": "1380234092525411/1000000000000000000", + "share": 0.5184358798323904, + "taken": 2102328, + "types": 5 + } + }, + "cheapest_clearer": { + "banks": 6116, + "families": [ + 22 + ], + "gain_on_this_side": "44740341982928/683657523331095", + "rigorous_beats_target": true, + "saving": "728397865314023/1000000000000000000", + "saving_paid": "728397865314023/1000000000000000000", + "saving_without_fallback": "5827182936843/8000000000000000", + "share": 0.10859117918609881, + "taken": 440352, + "types": 1 + }, + "clearers": 3502, + "clearers_by_size": { + "1": 3, + "2": 34, + "3": 179, + "4": 748, + "5": 2538 + }, + "single_family": { + "banks": 6116, + "families": [ + 22 + ], + "gain_on_this_side": "44740341982928/683657523331095", + "rigorous_beats_target": true, + "saving": "728397865314023/1000000000000000000", + "saving_paid": "728397865314023/1000000000000000000", + "saving_without_fallback": "5827182936843/8000000000000000", + "share": 0.10859117918609881, + "taken": 440352, + "types": 1 + }, + "target": "700918443859411/1000000000000000000", + "target_source": "complex" + }, + "complex": { + "admissible": 991, + "best_by_size": { + "1": { + "banks": 177, + "families": [ + 11 + ], + "gain_on_this_side": "7875159265698/700918443859411", + "rigorous_beats_target": true, + "saving": "708793603125109/1000000000000000000", + "saving_paid": "708793601534531/1000000000000000000", + "saving_without_fallback": "708793603125109/1000000000000000000", + "share": 0.014710771276595746, + "taken": 11682, + "types": 1 + }, + "2": { + "banks": 1883, + "families": [ + 1, + 8 + ], + "gain_on_this_side": "2741044685885/8872385365309", + "rigorous_beats_target": true, + "saving": "458730487022163/500000000000000000", + "saving_paid": "458730486434321/500000000000000000", + "saving_without_fallback": "458730487022163/500000000000000000", + "share": 0.15649933510638298, + "taken": 124278, + "types": 2 + }, + "3": { + "banks": 4704, + "families": [ + 1, + 2, + 18 + ], + "gain_on_this_side": "554398676912496/700918443859411", + "rigorous_beats_target": true, + "saving": "1255317120771907/1000000000000000000", + "saving_paid": "3138292799341/2500000000000000", + "saving_without_fallback": "1255317120771907/1000000000000000000", + "share": 0.39095744680851063, + "taken": 310464, + "types": 3 + }, + "4": { + "banks": 4062, + "families": [ + 1, + 2, + 3, + 9 + ], + "gain_on_this_side": "705942855889532/700918443859411", + "rigorous_beats_target": true, + "saving": "1406861299748943/1000000000000000000", + "saving_paid": "281372259786451/200000000000000000", + "saving_without_fallback": "1406861299748943/1000000000000000000", + "share": 0.33759973404255317, + "taken": 268092, + "types": 4 + }, + "5": { + "banks": 4796, + "families": [ + 1, + 2, + 3, + 4, + 19 + ], + "gain_on_this_side": "933153105947354/700918443859411", + "rigorous_beats_target": true, + "saving": "326814309961353/200000000000000000", + "saving_paid": "326814309812561/200000000000000000", + "saving_without_fallback": "326814309961353/200000000000000000", + "share": 0.3986037234042553, + "taken": 316536, + "types": 5 + } + }, + "cheapest_clearer": { + "banks": 177, + "families": [ + 11 + ], + "gain_on_this_side": "7875159265698/700918443859411", + "rigorous_beats_target": true, + "saving": "708793603125109/1000000000000000000", + "saving_paid": "708793601534531/1000000000000000000", + "saving_without_fallback": "708793603125109/1000000000000000000", + "share": 0.014710771276595746, + "taken": 11682, + "types": 1 + }, + "clearers": 991, + "clearers_by_size": { + "1": 3, + "2": 10, + "3": 56, + "4": 231, + "5": 691 + }, + "single_family": { + "banks": 177, + "families": [ + 11 + ], + "gain_on_this_side": "7875159265698/700918443859411", + "rigorous_beats_target": true, + "saving": "708793603125109/1000000000000000000", + "saving_paid": "708793601534531/1000000000000000000", + "saving_without_fallback": "708793603125109/1000000000000000000", + "share": 0.014710771276595746, + "taken": 11682, + "types": 1 + }, + "target": "136731504666219/200000000000000000", + "target_source": "bit" + } + }, + "source": { + "arithmetic": "references/pr200/interval_moment.py", + "certificate": "references/queue/pr207-coordinated-crossover.certificate.json", + "kappa_grid": 10000000000000000, + "saving_grid": 1000000000000000000 + }, + "status": "MODEL, NOT CONSTRUCTED. Every number here is exact arithmetic on the frontier certificate's own child ledgers; the bank construction, its charts and its witnesses belong to the supplier's harness and are not built. Each rung is a priced target.", + "strict_ladder": [ + { + "banks": 2001, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 1824, + "bit_families": [ + 6, + 8 + ], + "bit_saving": "141899511517939/200000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "251011155541/6831904550366", + "kappa": "7082915705907/10000000000000000", + "types": 3 + }, + { + "banks": 3000, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 2823, + "bit_families": [ + 6, + 8, + 18 + ], + "bit_saving": "718242431279183/1000000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "251011155541/6831904550366", + "kappa": "7082915705907/10000000000000000", + "types": 4 + }, + { + "banks": 2184, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 2007, + "bit_families": [ + 6, + 18 + ], + "bit_saving": "706958372104771/1000000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "116342400047/3415952275183", + "kappa": "353229467523/500000000000000", + "types": 3 + }, + { + "banks": 1992, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 1815, + "bit_families": [ + 8, + 18 + ], + "bit_saving": "87821801129279/125000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "13493349823/487993182169", + "kappa": "438800715493/625000000000000", + "types": 3 + }, + { + "banks": 1824, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 1824, + "bit_families": [ + 6, + 8 + ], + "bit_saving": "141899511517939/200000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "172370462685/6831904550366", + "kappa": "7004275013051/10000000000000000", + "types": 2 + }, + { + "banks": 2007, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 2007, + "bit_families": [ + 6, + 18 + ], + "bit_saving": "706958372104771/1000000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "172370462685/6831904550366", + "kappa": "7004275013051/10000000000000000", + "types": 2 + }, + { + "banks": 1815, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 1815, + "bit_families": [ + 8, + 18 + ], + "bit_saving": "87821801129279/125000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "172370462685/6831904550366", + "kappa": "7004275013051/10000000000000000", + "types": 2 + }, + { + "banks": 2823, + "binding": "complex", + "binding_is_exact": true, + "bit_banks": 2823, + "bit_families": [ + 6, + 8, + 18 + ], + "bit_saving": "718242431279183/1000000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "172370462685/6831904550366", + "kappa": "7004275013051/10000000000000000", + "types": 3 + }, + { + "banks": 1008, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 1008, + "bit_families": [ + 6 + ], + "bit_saving": "174621103751517/250000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "21152028615/975986364338", + "kappa": "6979968750671/10000000000000000", + "types": 1 + }, + { + "banks": 1185, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 1008, + "bit_families": [ + 6 + ], + "bit_saving": "174621103751517/250000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "21152028615/975986364338", + "kappa": "6979968750671/10000000000000000", + "types": 2 + }, + { + "banks": 816, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 816, + "bit_families": [ + 8 + ], + "bit_saving": "347102294204153/500000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "105325476801/6831904550366", + "kappa": "6937230027167/10000000000000000", + "types": 1 + }, + { + "banks": 993, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 816, + "bit_families": [ + 8 + ], + "bit_saving": "347102294204153/500000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "105325476801/6831904550366", + "kappa": "6937230027167/10000000000000000", + "types": 2 + }, + { + "banks": 999, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 999, + "bit_families": [ + 18 + ], + "bit_saving": "691773537862501/1000000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "5789187870/487993182169", + "kappa": "3456476590273/5000000000000000", + "types": 1 + }, + { + "banks": 1176, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 999, + "bit_families": [ + 18 + ], + "bit_saving": "691773537862501/1000000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "5789187870/487993182169", + "kappa": "3456476590273/5000000000000000", + "types": 2 + }, + { + "banks": 0, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 0, + "bit_families": [], + "bit_saving": "136731504666219/200000000000000000", + "complex_banks": 0, + "complex_families": [], + "complex_saving": "700918443859411/1000000000000000000", + "gain": "0", + "kappa": "3415952275183/5000000000000000", + "types": 0 + }, + { + "banks": 177, + "binding": "bit", + "binding_is_exact": false, + "bit_banks": 0, + "bit_families": [], + "bit_saving": "136731504666219/200000000000000000", + "complex_banks": 177, + "complex_families": [ + 11 + ], + "complex_saving": "708793603125109/1000000000000000000", + "gain": "0", + "kappa": "3415952275183/5000000000000000", + "types": 1 + } + ], + "validations": { + "a_bit": { + "certificate": "4375408149318106538866216854671930632866706725794304565219529058788314814256861959639757/6400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "convention": "child ledger plus PR200's rare-class fallback", + "delta": "901461133783145328069367133293274205695434780470941211685185743138040360243/6400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "exact": false, + "note": "the certificate carries its own higher-precision value of this quantity; the residual is recorded, not asserted away", + "recomputed": "136731504666219/200000000000000000", + "relative_delta": "6592929230053745399832586693131146510202180498142949721323097/31999999999993407070769946254600167413306868853489797819501857050278676903" + }, + "a_complex": { + "certificate": "700918443859411/1000000000000000000", + "convention": "child ledger only, no fallback term", + "exact": true, + "recomputed": "700918443859411/1000000000000000000" + }, + "conventions": { + "bit_absolute_difference": "-1720321/1000000000000000000", + "bit_other_convention": "85457190631427/125000000000000000", + "complex_absolute_difference": "1580753/1000000000000000000", + "complex_other_convention": "350459221139329/500000000000000000", + "note": "the certificate prices its two sides differently - the bit side includes PR200's rare-class fallback, the complex side does not - and each is reproduced exactly under its own convention" + }, + "kappa": { + "certificate": "1366380910073/2000000000000000", + "exact": true, + "grid": "10^-16", + "ladder_zero_point": { + "delta_from_certificate": "1/10000000000000000", + "grid_steps": 1, + "note": "the ladder is priced from the rows this package recomputed; its zero point sits this many grid steps from the certificate's own value, entirely in the last digit of the bit side's sixteen-significant-digit saving", + "value": "3415952275183/5000000000000000" + }, + "recomputed": "1366380910073/2000000000000000", + "rule": "floor(min(a_bit, a_complex)/(1 + min(...))) on the certificate's own side values, at its own grid" + } + } +} diff --git a/research/frontier-beat-2026-10-09/beats.py b/research/frontier-beat-2026-10-09/beats.py new file mode 100644 index 0000000000..a645794c76 --- /dev/null +++ b/research/frontier-beat-2026-10-09/beats.py @@ -0,0 +1,609 @@ +#!/usr/bin/env python3 +"""Ways to beat the frontier kappa, priced with the frontier's own arithmetic. + +The frontier is PR207's coordinated crossover: the certificate in +`references/queue/` states + + a_bit = the bit word's coarse saving (the binding side) + a_complex= the complex word's coarse saving + kappa = floor( min(a_bit, a_complex) / (1 + min(...)) ) + +and nothing in the composition can move `kappa` except raising the *smaller* of +the two side savings. So "beating the frontier" is exactly the question of which +side can be raised, by how much, and at what cost. + +This script answers it three ways, all in exact rational arithmetic on the +supplier's own enclosure implementation (`references/pr200/interval_moment.py`): + +1. **Reproduce the frontier.** The two side savings and `kappa` are recomputed + from the certificate's own child ledgers, with no float anywhere, and the + kappa grid is discovered rather than assumed. + +2. **The strict ladder.** A family can be *banked* -- its children leave the + ledger, the stock falls by the row identity, and the paid moment pays less + twice over. Bank width is the word's `m`, so a family whose own blocks tile a + bank by themselves (`m % rank == 0`) and whose own volume is a whole number + of banks is bankable with no block shape the word does not already use. There + are very few such families on each word; every combination of them is priced + exactly here, and paired with every combination on the other side. + +3. **The rigorous screen over all family sets.** For every subset of up to + `MAX_TYPES` families per word whose removed rank volume is a whole number of + banks, the exact moment *interval* is evaluated once at the target saving: an + upper bound below one proves the subset's true saving is above the target with + no bisection and no tolerance. The best few of each size are then priced + exactly. This is the pinned ladder's own model (`rungs.py`) with the ranking + replaced by a rigorous test, and it is run exhaustively over every admissible + family set rather than over a screening window. + +4. **The audit.** The largest screened rungs are reported with what they assume: + the fraction of each word's paid dirt they remove, and the fact that every + family left in the frontier word is *retained* dirt (`#207` banked only the + rank-60 entrance exteriors, which the frontier profile no longer carries). + The arithmetic of the top rung is re-derived line by line so that a reviewer + can separate "the model pays this" from "the model is admissible here". + +Usage: + + python3 -B beats.py [--max-types 5] [--out beats.json] + python3 -B beats.py --check # re-run and compare with beats.json +""" +import argparse +import importlib.util +import itertools +import json +import sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +SAVING_GRID = 10 ** 18 # interval.saving_grid's grid, as the certificate uses +BAD = Q(1, 10 ** 16) # PR200's rare-class fallback weight +MAX_TYPES = 5 # families per word screened exhaustively +KEEP_PER_SIZE = 6 # exactly priced per (side, number of families) +MILESTONES = ("1/1000", "1/1024", "1/1250") # kappa targets for the requirement table + + +def module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + loaded = importlib.util.module_from_spec(spec) + sys.modules[name] = loaded + spec.loader.exec_module(loaded) + return loaded + + +# -------------------------------------------------------------------------- +# rows, banks, prices +# -------------------------------------------------------------------------- +def rows(profile): + """The certificate's row as `interval_moment` wants it: m, W, N, histogram.""" + m = int(profile["m"]) + hist = {int(r): int(n) for r, n in profile["child_multiplicities"].items() if n} + W = int(profile["W"]) + N = int(profile["N"]) + assert sum(r * n for r, n in hist.items()) == m * W - N, "row identity" + assert max(hist) == int(profile["maxchild"]), "maximum child" + return m, W, N, hist + + +def row_profile(m, W, N, hist): + """A profile dict the interval implementation accepts.""" + hist = {int(r): int(n) for r, n in hist.items() if n} + assert hist and all(0 < r < m and n > 0 for r, n in hist.items()), "child domain" + total = sum(r * n for r, n in hist.items()) + assert total == m * W - N, "row identity" + return dict(m=m, W=W, N=N, L=0, total_rank=total, maxchild=max(hist), + child_multiplicities={str(r): n for r, n in hist.items()}) + + +def paid_moment(interval, profile, a): + """PR200's paid price: the child ledger plus the rare-class fallback. + + This is the convention the pinned ladder (`levers.py`, `rungs.py`) prices + with; the certificate's own `a_bit`/`a_complex` are the fallback-free values. + """ + raw = interval.moment(profile, a) + m, W = profile["m"], profile["W"] + edges = sum(profile["child_multiplicities"].values()) + low, high = interval.log_interval(Q(m)) + exp_low, exp_high = interval.exp_interval(a * low, a * high) + weight = BAD * Q(32 * m * m * edges, W * m) + return raw["upper"] + weight * exp_high, raw["lower"] + weight * exp_low + + +def saving(interval, profile): + """The largest `SAVING_GRID` point that pays, fallback-free (the certificate's rule).""" + return Q(interval.saving_grid(profile, SAVING_GRID)["accepted"]["saving"]) + + +def saving_paid(interval, profile): + """The same bisection with the rare-class fallback included.""" + low, high = 0, SAVING_GRID // 100 + assert paid_moment(interval, profile, Q(low, SAVING_GRID))[0] < 1, "zero-saving" + assert paid_moment(interval, profile, Q(high, SAVING_GRID))[1] > 1, "bracket" + while high - low > 1: + mid = (low + high) // 2 + if paid_moment(interval, profile, Q(mid, SAVING_GRID))[0] < 1: + low = mid + else: + high = mid + upper = paid_moment(interval, profile, Q(low, SAVING_GRID))[0] + lower = paid_moment(interval, profile, Q(high, SAVING_GRID))[1] + assert upper < 1 < lower, "adjacent grid exclusion" + return Q(low, SAVING_GRID) + + +def beats(interval, profile, target): + """One interval evaluation: does this row's true saving exceed `target`?""" + return paid_moment(interval, profile, target)[0] < 1 + + +def whole_banks(m, hist, families): + """A bank is a width-`m` block partition, so the taken volume must fill whole banks.""" + return bool(families) and sum(r * hist[r] for r in families) % m == 0 + + +def bankable_alone(m, hist): + """Families whose own blocks tile a bank and whose own volume is whole banks.""" + return sorted(r for r in hist if m % r == 0 and (r * hist[r]) % m == 0) + + +def absorb(m, W, N, hist, families): + """Take a family set out of the ledger and into the banks.""" + kept = {r: n for r, n in hist.items() if r not in families} + taken = sum(r * n for r, n in hist.items() if r in families) + assert taken and kept, "a schedule absorbs something and leaves a ledger" + remainder = m * W - N - taken + stock, leftover = divmod(remainder + N, m) + assert leftover == 0, "half-filled stock" + return stock, remainder, kept, taken + + +def kappa(a): + """The frontier certificate's own rule, on the grid discovered in `main`. + + `kappa = floor(a/(1+a))` to that grid, with `a` the smaller of the two side savings. + """ + value = Q(a) / (1 + Q(a)) + return Q(value.numerator * KAPPA_GRID // value.denominator, KAPPA_GRID) + + +KAPPA_GRID = 10 ** 16 + + +# -------------------------------------------------------------------------- +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--max-types", type=int, default=MAX_TYPES) + parser.add_argument("--out", type=Path, default=HERE / "beats.json") + parser.add_argument("--check", action="store_true", + help="compare a fresh run with the committed beats.json") + args = parser.parse_args() + if hasattr(sys, "set_int_max_str_digits"): + sys.set_int_max_str_digits(0) + assert not sys.flags.optimize, "assertions must stay enabled" + # The vendored pins are verified by hash before they are used. + import hashlib + source = json.loads((HERE / "SOURCE.json").read_text()) + for pin in source["pins"]: + digest = hashlib.sha256((HERE / pin["path"]).read_bytes()).hexdigest() + assert digest == pin["sha256"], ("pin hash mismatch", pin["path"]) + interval = module("beats_interval_moment", HERE / "references/pr200/interval_moment.py") + cert = json.loads((HERE / "references/queue/pr207-coordinated-crossover.certificate.json").read_text()) + global KAPPA_GRID + + # -- 1. reproduce the frontier, and discover its kappa grid --------------- + # The certificate prices its two sides with two different conventions and records + # both: the bit side includes PR200's rare-class fallback term, the complex side + # does not. Reproducing each side under its own convention is exact, which is how + # the asymmetry is pinned rather than assumed. + CONVENTION = {"bit": True, "complex": False} + sides = {} + for side, key in (("bit", "bit_profile"), ("complex", "complex_profile")): + m, W, N, hist = rows(cert[key]) + profile = row_profile(m, W, N, hist) + variants = {"with_fallback": saving_paid(interval, profile), + "without_fallback": saving(interval, profile)} + base = variants["with_fallback" if CONVENTION[side] else "without_fallback"] + sides[side] = dict(m=m, W=W, N=N, hist=hist, base=base, variants=variants, + families=len(hist), children=sum(hist.values()), + rank_mass=m * W - N, tiles=bankable_alone(m, hist)) + published_a = {side: Q(cert["a_bit" if side == "bit" else "a_complex"]) for side in sides} + for side in sides: + base = sides[side]["base"] + # The complex side is reproduced to the last digit; the bit side to sixteen + # significant digits, the certificate carrying its own higher-precision value of + # the same quantity. Both residuals are recorded exactly rather than widened. + if side == "complex": + assert base == published_a[side], "complex saving not reproduced exactly" + else: + assert abs(base / published_a[side] - 1) < Q(1, 10 ** 12), float(base / published_a[side] - 1) + other = "without_fallback" if CONVENTION[side] else "with_fallback" + sides[side]["other_convention"] = sides[side]["variants"][other] + sides[side]["published"] = published_a[side] + sides[side]["published_delta"] = base - published_a[side] + sides[side]["published_relative_delta"] = base / published_a[side] - 1 + binding = min(sides, key=lambda s: sides[s]["base"]) + # Which 10^-k grid does the certificate's kappa sit on? Discover, do not assume. The + # discovery uses the certificate's *own* binding value: the assembly consumes the + # ordinary leaf, not the profile's coarse saving. + exact = published_a[binding] / (1 + published_a[binding]) + found = None + for exponent in range(8, 30): + grid = 10 ** exponent + if Q(exact.numerator * grid // exact.denominator, grid) == Q(cert["kappa"]): + found = grid + break + assert found is not None, "the certificate's kappa is not a 10^-k floor of a/(1+a)" + KAPPA_GRID = found + frontier_published = kappa(published_a[binding]) + assert frontier_published == Q(cert["kappa"]), ( + "the certificate's kappa is not reproduced", str(frontier_published), cert["kappa"]) + # The ladder's own zero point, priced from the rows this package recomputed; the + # certificate's value must agree with it to within one grid step of the discovery. + frontier = kappa(sides[binding]["base"]) + assert abs(frontier - frontier_published) <= Q(1, KAPPA_GRID), "base rung disagrees" + + def price(side, m, W, N, hist): + """Both conventions for one row, and the one this side is priced under.""" + profile = row_profile(m, W, N, hist) + plain, paid = saving(interval, profile), saving_paid(interval, profile) + return (paid if CONVENTION[side] else plain), plain, paid + + cache = {} + + def side_row(side, families): + """Absorb one side's family set once, and price the row it leaves.""" + key = (side, tuple(sorted(families))) + if key not in cache: + item = sides[side] + if not families: + cache[key] = dict( + families=[], types=0, banks=0, taken=0, share=0.0, W=item["W"], + rank_mass=item["rank_mass"], children=item["children"], + maxchild=max(item["hist"]), saving=item["base"], + saving_without_fallback=item["variants"]["without_fallback"], + saving_paid=item["variants"]["with_fallback"]) + else: + stock, remainder, kept, taken = absorb(item["m"], item["W"], item["N"], + item["hist"], set(families)) + chosen, plain, paid = price(side, item["m"], stock, item["N"], kept) + cache[key] = dict(families=sorted(families), types=len(families), + banks=taken // item["m"], taken=taken, + share=float(Q(taken, item["rank_mass"])), W=stock, + rank_mass=remainder, children=sum(kept.values()), + maxchild=max(kept), saving=chosen, + saving_without_fallback=plain, saving_paid=paid) + return cache[key] + + def rung(bit_families, complex_families): + """Absorb the two family sets and price the frontier's assembly.""" + out = {"bit": side_row("bit", bit_families), + "complex": side_row("complex", complex_families)} + budget = min(Q(out["bit"]["saving"]), Q(out["complex"]["saving"])) + value = kappa(budget) + if not (bit_families or complex_families): + # The untouched word must reproduce the frontier, conventions and all; + # anything else means the reproduction above was not the same object. + assert value == frontier, "base rung" + return dict(bit=out["bit"], complex=out["complex"], + types=out["bit"]["types"] + out["complex"]["types"], + banks=out["bit"]["banks"] + out["complex"]["banks"], + binding=("bit" if Q(out["bit"]["saving"]) <= Q(out["complex"]["saving"]) + else "complex"), + budget=budget, kappa=value, gain=value / frontier - 1, + exact=bool(Q(out["bit"]["saving"]) > Q(out["complex"]["saving"]))) + + # -- 2. the strict ladder: every combination of the self-tiling families --- + ladder = [] + for size_b in range(len(sides["bit"]["tiles"]) + 1): + for bit_families in itertools.combinations(sides["bit"]["tiles"], size_b): + for size_c in range(len(sides["complex"]["tiles"]) + 1): + for complex_families in itertools.combinations(sides["complex"]["tiles"], size_c): + ladder.append(rung(bit_families, complex_families)) + ladder.sort(key=lambda item: (-item["kappa"], item["types"])) + base_rungs = [item for item in ladder if item["types"] == 0] + assert len(base_rungs) == 1 and Q(base_rungs[0]["kappa"]) == frontier, \ + "the untouched word must be the frontier rung" + assert Q(ladder[0]["kappa"]) > frontier, "the strict ladder must contain a rung above" + + # -- 3. the rigorous screen over every admissible family set -------------- + def clean(item): + """A candidate as plain JSON: exact values as strings, the ranking key dropped.""" + if item is None: + return None + return {k: (str(v) if isinstance(v, Q) else v) for k, v in item.items() + if k != "moment_at_target"} + + screen = {} + for side, other in (("bit", "complex"), ("complex", "bit")): + item = sides[side] + target = Q(sides[other]["base"]) + candidates, admissible = [], 0 + for size in range(1, args.max_types + 1): + for combo in itertools.combinations(sorted(item["hist"]), size): + families = set(combo) + if not whole_banks(item["m"], item["hist"], families): + continue + admissible += 1 + stock, remainder, kept, taken = absorb(item["m"], item["W"], item["N"], + item["hist"], families) + profile = row_profile(item["m"], stock, item["N"], kept) + # one exact interval, two answers: does it beat the target, and by how + # much of the moment is it ahead (the ranking key, smaller is better). + moment = paid_moment(interval, profile, target)[0] + candidates.append(dict(families=sorted(families), types=size, + banks=taken // item["m"], taken=taken, + share=float(Q(taken, item["rank_mass"])), + moment_at_target=moment, + rigorous_beats_target=bool(moment < 1))) + top, ranked = [], sorted(candidates, key=lambda c: c["moment_at_target"]) + for size in range(1, args.max_types + 1): + top += [c for c in ranked if c["types"] == size][:KEEP_PER_SIZE] + for candidate in top: + stock, remainder, kept, taken = absorb(item["m"], item["W"], item["N"], + item["hist"], set(candidate["families"])) + candidate["saving"], candidate["saving_without_fallback"], candidate["saving_paid"] = \ + price(side, item["m"], stock, item["N"], kept) + candidate["gain_on_this_side"] = Q(candidate["saving"]) / item["base"] - 1 + clearers = [c for c in candidates if c["rigorous_beats_target"]] + # Only the leaders of each size were priced exactly; the cheapest *priced* + # clearer is the one whose cost in new residual types is the smallest. + priced_clearers = [c for c in clearers if "saving" in c] + best_by_size = {} + for size in range(1, args.max_types + 1): + priced = [c for c in top if c["types"] == size] + if priced: + best = max(priced, key=lambda c: Q(c["saving"])) + best_by_size[str(size)] = best + screen[side] = dict( + target=str(target), target_source=other, + admissible=admissible, clearers=len(clearers), + clearers_by_size={str(size): sum(1 for c in clearers if c["types"] == size) + for size in range(1, args.max_types + 1)}, + single_family=clean(best_by_size.get("1")), + best_by_size={size: clean(row) for size, row in best_by_size.items()}, + cheapest_clearer=clean(min(priced_clearers, + key=lambda c: (c["types"], -Q(c["saving"])))) + if priced_clearers else None) + + # -- 4. the rung above the frontier, exactly ------------------------------ + best_screen = None + for bit_row in screen["bit"]["best_by_size"].values(): + for complex_row in screen["complex"]["best_by_size"].values(): + candidate = rung(bit_row["families"], complex_row["families"]) + if best_screen is None or Q(candidate["kappa"]) > Q(best_screen["kappa"]): + best_screen = candidate + best_screen = dict(best_screen, + note="best pair drawn from the exactly priced leaders of each " + "family count on each side; the screen ranks, the price decides") + + # -- 5. the audit of the volume bracket ---------------------------------- + def audit(): + """Re-derive the top screened pair and state exactly what it assumes.""" + top = best_screen + removed = {side: top[side]["share"] for side in ("bit", "complex")} + return dict( + rung=dict(kappa=str(top["kappa"]), gain=str(top["gain"]), + binding=top["binding"], types=top["types"], banks=top["banks"], + bit_families=top["bit"]["families"], + complex_families=top["complex"]["families"], + bit_saving=str(top["bit"]["saving"]), + complex_saving=str(top["complex"]["saving"]), + bit_share_of_ledger=removed["bit"], + complex_share_of_ledger=removed["complex"]), + arithmetic="reproduced from scratch: the row identity after absorption, the " + "whole-bank volume condition, the paid moment's adjacent-grid " + "exclusion and the assembly", + assumptions=[ + "Every family still in the frontier word is retained dirt: #207 banked the " + "rank-60 entrance exteriors, which the frontier profile no longer carries " + "(bit maxchild 22, complex maxchild 20). So this rung removes interior " + "children, and no family removed here has a published bank proof.", + "The model needs one new residual type per absorbed family, which the " + "supplier's proof reserves for the future: the queue's own allocation " + "records that verdict for the single-family rung.", + "The absorbed family's rank is treated as free, which is what #205/#206/#207 " + "certified for rank 60 on width 72 -- an exterior of one child per selected " + "gauge, not interior dirt.", + "Bank charts, normalizers, the F2 and defining-integer columns and per-bank " + "prime witnesses are the supplier's harness and are not built here.", + ], + verdict="the arithmetic is exact and the rung is priced, but it is a model: it " + "assumes new residual types that the published bank proof reserves and " + "that no package enumerates.") + + def reachable(kappa_target): + """The smallest side saving the assembly needs for a kappa target.""" + value = Q(kappa_target) + needed = value / (1 - value) + return Q(needed.numerator * SAVING_GRID // needed.denominator + 1, SAVING_GRID) + + requirements = [] + targets = [("beat the frontier by 0.1%", frontier * Q(1001, 1000)), + ("beat the frontier by 1%", frontier * Q(101, 100)), + ("beat the frontier by 5%", frontier * Q(105, 100)), + ("beat the frontier by 10%", frontier * Q(11, 10)), + ("beat the frontier by 25%", frontier * Q(125, 100)), + ("beat the frontier by 50%", frontier * Q(3, 2)), + ("kappa = 1/1000", Q(1, 1000)), ("kappa = 2^-10", Q(1, 1024))] + for label, target in targets: + needed = reachable(target) + requirements.append(dict( + label=label, target=str(target), target_decimal=float(target), + needed_side_saving=str(needed), needed_side_saving_decimal=float(needed), + over_binding_side=str(needed / sides[binding]["base"] - 1), + over_other_side=str(needed / sides["complex" if binding == "bit" else "bit"]["base"] - 1), + binding_side_after=str(needed / sides[binding]["base"] - 1), + met_by_rigorous_screen={ + side: bool(screen[side]["best_by_size"] + and max(Q(c["saving"]) for c in screen[side]["best_by_size"].values()) + >= needed) for side in ("bit", "complex")})) + + out = dict( + status="MODEL, NOT CONSTRUCTED. Every number here is exact arithmetic on the " + "frontier certificate's own child ledgers; the bank construction, its " + "charts and its witnesses belong to the supplier's harness and are not " + "built. Each rung is a priced target.", + method="PR200's exact interval and exponential enclosures on the frontier " + "certificate's rows; the paid moment as the screen (one evaluation per " + "candidate, rigorous, no bisection) and the adjacent-grid bisection for the " + "prices; the assembly rule taken verbatim from the certificate it reproduces", + source=dict(certificate="references/queue/pr207-coordinated-crossover.certificate.json", + arithmetic="references/pr200/interval_moment.py", + kappa_grid=KAPPA_GRID, saving_grid=SAVING_GRID), + validations=dict( + a_bit=dict(certificate=str(published_a["bit"]), + recomputed=str(sides["bit"]["base"]), + exact=bool(sides["bit"]["base"] == published_a["bit"]), + delta=str(sides["bit"]["published_delta"]), + relative_delta=str(sides["bit"]["published_relative_delta"]), + convention="child ledger plus PR200's rare-class fallback", + note="the certificate carries its own higher-precision value of " + "this quantity; the residual is recorded, not asserted away"), + a_complex=dict(certificate=str(published_a["complex"]), + recomputed=str(sides["complex"]["base"]), + exact=bool(sides["complex"]["base"] == published_a["complex"]), + convention="child ledger only, no fallback term"), + conventions=dict( + note="the certificate prices its two sides differently - the bit side " + "includes PR200's rare-class fallback, the complex side does not - and " + "each is reproduced exactly under its own convention", + bit_other_convention=str(sides["bit"]["other_convention"]), + complex_other_convention=str(sides["complex"]["other_convention"]), + bit_absolute_difference=str(sides["bit"]["base"] + - sides["bit"]["other_convention"]), + complex_absolute_difference=str(sides["complex"]["base"] + - sides["complex"]["other_convention"])), + kappa=dict(certificate=cert["kappa"], recomputed=str(frontier_published), + exact=bool(frontier_published == Q(cert["kappa"])), + grid="10^-{}".format(len(str(KAPPA_GRID)) - 1), + rule="floor(min(a_bit, a_complex)/(1 + min(...))) on the " + "certificate's own side values, at its own grid", + ladder_zero_point=dict( + value=str(frontier), + delta_from_certificate=str(frontier - frontier_published), + grid_steps=int(abs(frontier - frontier_published) * KAPPA_GRID), + note="the ladder is priced from the rows this package " + "recomputed; its zero point sits this many grid steps from " + "the certificate's own value, entirely in the last digit " + "of the bit side's sixteen-significant-digit saving"))), + frontier=dict(kappa=str(frontier), kappa_decimal=float(frontier), + binding=binding, published=str(Q(cert["kappa"])), + bit_saving=str(sides["bit"]["base"]), + complex_saving=str(sides["complex"]["base"]), + sides={side: dict(m=sides[side]["m"], W=sides[side]["W"], + deficit=sides[side]["N"], + families=sides[side]["families"], + children=sides[side]["children"], + rank_mass=sides[side]["rank_mass"], + saving=str(sides[side]["base"]), + tiles_the_bank=sides[side]["tiles"]) + for side in sides}), + strict_ladder=[dict(kappa=str(item["kappa"]), gain=str(item["gain"]), + binding=item["binding"], types=item["types"], + banks=item["banks"], + bit_families=item["bit"]["families"], + complex_families=item["complex"]["families"], + bit_saving=str(item["bit"]["saving"]), + complex_saving=str(item["complex"]["saving"]), + bit_banks=item["bit"]["banks"], + complex_banks=item["complex"]["banks"], + binding_is_exact=item["exact"]) + for item in ladder], + screen={side: dict(target=screen[side]["target"], + target_source=screen[side]["target_source"], + admissible=screen[side]["admissible"], + clearers=screen[side]["clearers"], + clearers_by_size=screen[side]["clearers_by_size"], + single_family=screen[side]["single_family"], + best_by_size=screen[side]["best_by_size"], + cheapest_clearer=screen[side]["cheapest_clearer"]) + for side in screen}, + best_rung=dict(kappa=str(best_screen["kappa"]), gain=str(best_screen["gain"]), + binding=best_screen["binding"], types=best_screen["types"], + banks=best_screen["banks"], + bit_families=best_screen["bit"]["families"], + complex_families=best_screen["complex"]["families"]), + audit=audit(), + requirements=requirements, + limits=[ + "No contributor verifier, CI run or upstream proof package is re-executed: the " + "rows are the frontier certificate's own recorded ledgers and the arithmetic " + "here is this package's.", + "The strict tier is the only tier that needs no block shape the word does not " + "already use; the screen's larger rungs treat an absorbed family's rank as free, " + "which is certified precedent only for an exterior of the rank-60 kind.", + "A rung's cost is measured in new residual types (families absorbed) because " + "that is what the supplier's harness would have to instantiate; it ignores " + "chart, normalizer and witness work entirely.", + "The pinned ladder in the supplier's package prices both sides with the " + "rare-class fallback, so its values sit a few 1e-10 relative below the " + "convention-matched values recorded here; both are given for every rung.", + ]) + text = json.dumps(out, indent=1, sort_keys=True) + "\n" + if args.check: + # Name the artifact actually compared: the check is run against more than one + # family depth, and a hardcoded label hides which one was verified. + name = args.out.name + committed = args.out.read_text() + if committed != text: + print("[check] MISMATCH: {} does not match a fresh run".format(name)) + for line_a, line_b in zip(committed.splitlines(), text.splitlines()): + if line_a != line_b: + print(" committed:", line_a) + print(" fresh :", line_b) + break + return 1 + print("[check] {} matches a fresh run byte for byte (--max-types {})" + .format(name, args.max_types)) + return 0 + args.out.write_text(text, newline="\n") + + print("[frontier] kappa = {} ({:.15g}), binding {} (bit {} / complex {})".format( + frontier, float(frontier), binding, float(sides["bit"]["base"]), + float(sides["complex"]["base"]))) + print("[validations] a_complex exact: {}; a_bit delta {:.3g} (relative {:.2g}); " + "certificate kappa reproduced exactly: {} on the {}".format( + sides["complex"]["base"] == published_a["complex"], + float(sides["bit"]["published_delta"]), + float(sides["bit"]["published_relative_delta"]), + frontier_published == Q(cert["kappa"]), + "10^-{}".format(len(str(KAPPA_GRID)) - 1))) + print("[ladder zero] {} ({} grid step(s) from the certificate's {})".format( + frontier, int(abs(frontier - frontier_published) * KAPPA_GRID), frontier_published)) + print("[strict] {} family sets priced; best {} ({} types, {} banks)".format( + len(ladder), ladder[0]["kappa"], ladder[0]["types"], ladder[0]["banks"])) + for item in ladder[1:6]: + print(" absorb bit {} + complex {} -> kappa {} ({:+.4%}, {} type(s), " + "{} banks, binding {})".format(item["bit"]["families"] or "nothing", + item["complex"]["families"] or "nothing", + item["kappa"], float(item["gain"]), + item["types"], item["banks"], item["binding"])) + for side in ("bit", "complex"): + item = screen[side] + print("[screen {}] {} admissible family sets, {} rigorously beat {} ({})".format( + side, item["admissible"], item["clearers"], item["target"], + item["target_source"])) + best = item["best_by_size"].get("1") + if best: + print(" best single family: ranks {} -> {} banks ({:.2%} of the ledger), " + "saving {} ({:+.4%} on this side)".format( + best["families"], best["banks"], best["share"], best["saving"], + float(Q(best["gain_on_this_side"])))) + for size, row in sorted(item["best_by_size"].items()): + print(" best with {} famil{}: {} -> saving {} ({:+.4%} on this side), " + "{:.2%} of the ledger in {} banks".format( + size, "y" if size == "1" else "ies", row["families"], row["saving"], + float(Q(row["gain_on_this_side"])), row["share"], row["banks"])) + print("[best rung] kappa = {} ({:+.4%}), binding {}, {} new residual type(s)".format( + best_screen["kappa"], float(best_screen["gain"]), best_screen["binding"], + best_screen["types"])) + print("[audit] that rung removes {:.1%} of the bit ledger and {:.1%} of the complex " + "ledger".format(best_screen["bit"]["share"], best_screen["complex"]["share"])) + print("[write] " + str(args.out)) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/frontier-beat-2026-10-09/check_docs.py b/research/frontier-beat-2026-10-09/check_docs.py new file mode 100644 index 0000000000..7a1d016fc1 --- /dev/null +++ b/research/frontier-beat-2026-10-09/check_docs.py @@ -0,0 +1,115 @@ +#!/usr/bin/env python3 +"""Check the prose against the artifacts. + +The two documents in this directory quote a lot of exact numbers. This script +reads every value out of the three artifacts (`beats.json` for the five-family +screen, `beats-six.json` for six, `instantiate.json` for the bank-rung analysis) +and checks two things: + +* every number of six or more digits written in a markdown **table row** matches a + value of the artifact it belongs to, within a relative `2e-12` (the documents + render 14-15 significant digits), and +* a list of required headline claims is still present, so a rewrite cannot quietly + drop the values the package is about. + + python3 -B check_docs.py +""" +import json +import re +import sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +DOCS = { + "README.md": ("beats.json", "beats-six.json"), + "INSTANTIATE.md": ("instantiate.json", "beats.json"), +} +REQUIRED = { + "README.md": [ + "6.831904550365e-4", # the certificate's own kappa + "6.831904550366e-4", # this package's ladder zero point + "6.83657523331095e-4", # a_bit + "7.00918443859411e-4", # a_complex + "1.4e-16", "2.1e-13", # the a_bit residual + "+2.167%", "+2.523%", "+3.674%", + "6.979968750671e-4", "7.004275013051e-4", "7.082915705907e-4", + "1.3783316708213e-3", # five-family best rung + "1.52739614292328e-3", # six-family bit top + "2.30539885681005e-3", # six-family complex top + "1.5250667618335e-3", # six-family best rung + "3,512", "3,502", "991", "10,318", "2,725", + "9 new residual types", "11 new residual types", "33,261", + "SOURCE.json", # the pin hashes are verified at run time + ], + "INSTANTIATE.md": [ + "12,096", "4,032", "1,008", "336", "72,576", "55,394", "56,402", + "4,055,136", "3,982,560", "5,808", + "6.98484415006068e-4", "6.979968750671e-4", "+2.1672%", + "2,200", "5,500", "396,000", "144", "112", + "coordinated-bank-proof.md", + ], +} + + +def values(path): + """Every exact value an artifact carries, as floats.""" + found = [] + def walk(node): + if isinstance(node, dict): + for item in node.values(): + walk(item) + elif isinstance(node, list): + for item in node: + walk(item) + elif isinstance(node, str): + try: + found.append(float(Q(node))) + except Exception: + pass + elif isinstance(node, (int, float)) and not isinstance(node, bool): + found.append(float(node)) + walk(json.loads(path.read_text())) + return found + + +def main(): + artifacts = {name: values(HERE / name) + for name in {n for names in DOCS.values() for n in names}} + problems, checked = [], 0 + for doc, sources in DOCS.items(): + text = (HERE / doc).read_text(encoding="utf-8") + pool = [v for name in sources for v in artifacts[name]] + for raw in text.splitlines(): + if not raw.startswith("|"): + continue + line = re.sub(r"`[^`]*`", " ", raw) + line = re.sub(r"(?<=\d),(?=\d{3}\b)", "", line) # 33,261 -> 33261 + for token in re.findall(r"-?\d+(?:\.\d+)?(?:[eE][+-]?\d+)?", line): + if re.search(re.escape(token) + r"\s*%", line): + continue # a gain percentage + if len(re.sub(r"\D", "", token.split("e")[0].split("E")[0])) <= 5: + continue # family/type counts + value = float(token) + checked += 1 + if not any(abs(value - v) <= max(abs(v), abs(value)) * 2e-12 + for v in pool): + problems.append(f"{doc}: table number {token!r} matches no value " + f"in {'/'.join(sources)}") + for claim in REQUIRED[doc]: + if claim not in text: + problems.append(f"{doc}: required claim {claim!r} is missing") + print(f"checked {checked} table numbers and " + f"{sum(len(v) for v in REQUIRED.values())} required claims " + f"against {len(artifacts)} artifacts") + if problems: + print("MISMATCHES:") + for line in problems: + print(" -", line) + return 1 + print("every quoted number and required claim matches the artifacts") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/frontier-beat-2026-10-09/instantiate.json b/research/frontier-beat-2026-10-09/instantiate.json new file mode 100644 index 0000000000..4c845481a0 --- /dev/null +++ b/research/frontier-beat-2026-10-09/instantiate.json @@ -0,0 +1,289 @@ +{ + "checklist": [ + { + "in_the_proof": "P_s(j) = 1[j div 4 = s] for s = 0..17 and Q_s(j) = 1[j div 24 = s] for s = 0,1,2, on j = 0..71; each family disjoint, idempotent and exhaustive", + "item": "block partition of the bank", + "note": "a rank-6 partition is the same construction with stride 6 (12 blocks), so `S_P S_Q = S_{P+Q}` and `S_P^2 = I` need no new proof: the proof states them for any finite disjoint projector partition summing to I. The stride-6 partition itself is new.", + "status": "new instance, inherited algebra" + }, + { + "in_the_proof": "the banked items are the 2,200 rank-60 gauge exteriors, one per selected entrance gauge, and the gauge's own itinerary supplies the address", + "item": "normalizer and the child-to-block map", + "note": "the rank-6 family is interior dirt with no registered gauge address, and no pinned package enumerates it: this is the same gap that stops the complex rung (an inventory obligation). The counts match exactly -- one block per absorbed child -- but which child goes to which block is not in any pin.", + "status": "NEW, and blank in the queue" + }, + { + "in_the_proof": "one common invertible weighted chart per bank, with inverse; product(A S_P A^-1) = A (product S_P) A^-1", + "item": "charts for the new block frames", + "note": "integer kernel bases with fraction-free inverses and replayed elementary factors for the stride-6 blocks; the certified proof's universal conjugation covers any common weighted chart, so this is work rather than new theory.", + "status": "new instance" + }, + { + "in_the_proof": "144 columns of each two-bank address map over F2 and over Z, for the endpoint and its inverse, rejecting a missing last block and a repeated last block in both rings", + "item": "the two-bank address-map columns", + "note": "144 = 2 rings x 72 coordinates, so the check is unchanged in shape; it has to be run on the stride-6 address map.", + "status": "inherited check, new instance" + }, + { + "in_the_proof": "prime supply and residual factors below the retained q bound", + "item": "per-block prime witnesses", + "note": "12096 blocks over three copies need distinct integer Gram/prime witnesses; the certified supply is per block frame, not per bank.", + "status": "new supply" + }, + { + "in_the_proof": "rare-class fraction 10^-16, fallback 32*72^2 children per edge, the positive atom/row-adapter toll on its own 10^-24 grid, and two independent rational log/exp enclosures certifying the accepted moment and rejecting the adjacent 10^-18 grid point", + "item": "moment-envelope parity", + "note": "the retained ledger, stock and deficit are stated below and the certified saving is recomputed with the supplier's own enclosure implementation; the fallback bill is unchanged because the word's edges are unchanged.", + "status": "already satisfied in this package" + }, + { + "in_the_proof": "47 strict constraints and 7 margins at the selected parameters", + "item": "the assembly", + "note": "PR207's unchanged rule on the two side savings; the rung is bit-binding, so the complex budget is untouched and the binding side value is the banked bit row's own.", + "status": "verified here" + }, + { + "in_the_proof": "1100 selected and 47484 undeferred banks per stage, with nine physical replicas making each stage-private allocation integral", + "item": "stage-private allocation", + "note": "the per-copy bank count here is 336; reading the rung as three stage-private families gives 112 per stage, so the allocation would be integral without replicas -- but no pin states that the rank-6 dirt is stage-private, so this is an inference.", + "status": "inference, not verified" + }, + { + "in_the_proof": "all-input weighted compiler, completed-core routing, stage cover, local-ring precision/recovery, prime supply, uniform setup, all-size analytic and tape contracts remain conditional", + "item": "the inherited conditional interfaces", + "note": "no finite bank verification discharges these, and neither does this package.", + "status": "conditional in the record itself" + } + ], + "limits": [ + "No bank is built, no chart is computed, no witness is supplied and no physical word is replayed: the checklist states what would be needed.", + "The stage-private reading is an inference (the per-copy count is divisible by three); no pin says the rank-6 dirt is stage-private.", + "The rank-6 family is interior dirt: the certified proof removed the entrance exteriors, and the frontier profile no longer carries them." + ], + "method": "the frontier certificate's own three-copy rows, the supplier's enclosure implementation, and the supplier's bank proof read item by item; every count below is derived, not quoted", + "rung": { + "bank_width": 72, + "banks_per_copy": 336, + "banks_three_copies": 1008, + "blocks_per_bank": 12, + "blocks_per_copy": 4032, + "blocks_three_copies": 12096, + "certified_saving": "174621103751517/250000000000000000", + "certified_saving_decimal": 0.000698484415006068, + "children_per_copy": 4032, + "children_three_copies": 12096, + "deficit": "5808", + "family_rank": 6, + "frontier_kappa": "3415952275183/5000000000000000", + "gain": "21152028615/975986364338", + "kappa": "6979968750671/10000000000000000", + "maxchild_after": 22, + "rank_mass_after": 3982560, + "rank_mass_before": 4055136, + "rank_volume": 72576, + "retained_families": 21, + "stock_after": 55394, + "stock_before": 56402, + "stock_fall": 1008 + }, + "schedule": { + "bit": { + "W": 56402, + "deficit": 5808, + "families": 22, + "m": 72, + "schedule": [ + { + "banks": 5256, + "blocks_per_bank": 72, + "children": 378477, + "condition": "children divisible by 72", + "per_copy_banks": null, + "per_copy_children": 126159, + "rank": 1, + "rank_volume": 378477, + "whole_banks": false + }, + { + "banks": 4962, + "blocks_per_bank": 36, + "children": 178653, + "condition": "children divisible by 36", + "per_copy_banks": null, + "per_copy_children": 59551, + "rank": 2, + "rank_volume": 357306, + "whole_banks": false + }, + { + "banks": 3817, + "blocks_per_bank": 24, + "children": 91629, + "condition": "children divisible by 24", + "per_copy_banks": null, + "per_copy_children": 30543, + "rank": 3, + "rank_volume": 274887, + "whole_banks": false + }, + { + "banks": 1596, + "blocks_per_bank": 18, + "children": 28737, + "condition": "children divisible by 18", + "per_copy_banks": null, + "per_copy_children": 9579, + "rank": 4, + "rank_volume": 114948, + "whole_banks": false + }, + { + "banks": 1008, + "blocks_per_bank": 12, + "children": 12096, + "condition": "children divisible by 12", + "per_copy_banks": 336, + "per_copy_children": 4032, + "rank": 6, + "rank_volume": 72576, + "whole_banks": true + }, + { + "banks": 816, + "blocks_per_bank": 9, + "children": 7344, + "condition": "children divisible by 9", + "per_copy_banks": 272, + "per_copy_children": 2448, + "rank": 8, + "rank_volume": 58752, + "whole_banks": true + }, + { + "banks": 646, + "blocks_per_bank": 8, + "children": 5175, + "condition": "children divisible by 8", + "per_copy_banks": null, + "per_copy_children": 1725, + "rank": 9, + "rank_volume": 46575, + "whole_banks": false + }, + { + "banks": 2026, + "blocks_per_bank": 6, + "children": 12159, + "condition": "children divisible by 6", + "per_copy_banks": null, + "per_copy_children": 4053, + "rank": 12, + "rank_volume": 145908, + "whole_banks": false + }, + { + "banks": 999, + "blocks_per_bank": 4, + "children": 3996, + "condition": "children divisible by 4", + "per_copy_banks": 333, + "per_copy_children": 1332, + "rank": 18, + "rank_volume": 71928, + "whole_banks": true + } + ] + }, + "complex": { + "W": 12052, + "deficit": 1320, + "families": 20, + "m": 66, + "schedule": [ + { + "banks": 1326, + "blocks_per_bank": 66, + "children": 87534, + "condition": "children divisible by 66", + "per_copy_banks": null, + "per_copy_children": 29178, + "rank": 1, + "rank_volume": 87534, + "whole_banks": false + }, + { + "banks": 1207, + "blocks_per_bank": 33, + "children": 39834, + "condition": "children divisible by 33", + "per_copy_banks": null, + "per_copy_children": 13278, + "rank": 2, + "rank_volume": 79668, + "whole_banks": false + }, + { + "banks": 1353, + "blocks_per_bank": 22, + "children": 29769, + "condition": "children divisible by 22", + "per_copy_banks": null, + "per_copy_children": 9923, + "rank": 3, + "rank_volume": 89307, + "whole_banks": false + }, + { + "banks": 437, + "blocks_per_bank": 11, + "children": 4815, + "condition": "children divisible by 11", + "per_copy_banks": null, + "per_copy_children": 1605, + "rank": 6, + "rank_volume": 28890, + "whole_banks": false + }, + { + "banks": 177, + "blocks_per_bank": 6, + "children": 1062, + "condition": "children divisible by 6", + "per_copy_banks": 59, + "per_copy_children": 354, + "rank": 11, + "rank_volume": 11682, + "whole_banks": true + } + ] + } + }, + "source": { + "arithmetic": "references/pr200/interval_moment.py", + "bank_proof": "references/queue/coordinated-bank-proof.md", + "certificate": "references/queue/pr207-coordinated-crossover.certificate.json" + }, + "status": "Read-only: no construction, no new word, no bank. This states what the +2.167% rung's arithmetic is and what the supplier's published bank proof already covers for it.", + "tilings": { + "all_tile_the_width": true, + "patterns": { + "mixed_certified": "6 x 4 + 2 x 24", + "rank24_certified": "3 x 24", + "rank4_certified": "18 x 4", + "rank6_this_rung": "12 x 6" + }, + "sums": { + "mixed_certified": 72, + "rank24_certified": 72, + "rank4_certified": 72, + "rank6_this_rung": 72 + } + }, + "validated": { + "certificate_bit_saving": "4375408149318106538866216854671930632866706725794304565219529058788314814256861959639757/6400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "note": "the recomputation is the certificate's own value to sixteen significant digits; the residual is in beats.json's validations", + "recomputed_bit_saving": "136731504666219/200000000000000000", + "relative_gap": "6592929230053745399832586693131146510202180498142949721323097/31999999999993407070769946254600167413306868853489797819501857050278676903" + }, + "verdict": "The rung's arithmetic is exact and its saving is certifiable with the tooling already in this package. Its construction reduces to a new block stride plus the items the certified bank spent on the gauge exteriors: the universal projector algebra is inherited (the proof states it for any disjoint exhaustive partition), the 144-column address check and the moment-envelope parity are inherited in shape, and the per-copy allocation is integral, so this rung does not need the nine physical replicas the certified allocation used. What does not exist is the part that identifies the dirt: no pin enumerates the word's rank-6 children, so the normalizer, the charts and the prime witnesses have nothing to be attached to yet. That is the same blank shape as the complex rung's inventory obligation, and it is smaller: one family of one word, whose counts and bank schedule are already pinned by this file." +} diff --git a/research/frontier-beat-2026-10-09/instantiate.py b/research/frontier-beat-2026-10-09/instantiate.py new file mode 100644 index 0000000000..528863f77e --- /dev/null +++ b/research/frontier-beat-2026-10-09/instantiate.py @@ -0,0 +1,345 @@ +#!/usr/bin/env python3 +"""What instantiating the bit rank-6 bank rung would take. + +`beats.py` prices the cheapest way to beat the frontier at +2.167%: absorb the bit +word's rank-6 child family into width-72 banks. This script asks the next question -- +what would have to exist for that rung to be a construction rather than a price. + +It does three things, all with the same hashed pins: + +1. **The schedule.** For every family of either word whose rank divides the bank + width, it states the block partition (`m/rank` blocks fill a bank), the bank + count the family's own volume fills, and whether that count is integral per + physical copy. The whole-bank condition has a simple form here: for rank `r` on + width `m`, `r * count % m == 0`, i.e. the family's child count must be divisible + by `m/r`, the number of blocks per bank. + +2. **The rung's arithmetic.** Re-derived from the frontier certificate: counts per + copy and over three copies, removed rank mass, banks, the retained ledger and + stock, the certified saving, and the kappa and gain the assembly returns. + +3. **The checklist.** The supplier's own bank proof + (`references/queue/coordinated-bank-proof.md`) is a finite verification of a + *different* absorption: it removes the 2,200 rank-60 gauge exteriors, one per + selected entrance gauge, and it checks 144 columns of each two-bank address map + over F2 and over Z. Each item of that proof is listed here with what this rung + inherits from it, what it would have to add, and what in the queue already + records the gap. + + python3 -B instantiate.py [--out instantiate.json] + python3 -B instantiate.py --check +""" +import argparse +import hashlib +import importlib.util +import json +import sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +SAVING_GRID = 10 ** 18 +BAD = Q(1, 10 ** 16) +BANK_RANK = 6 # the rung this document is about +COPIES = 3 # the certificate's row is the three-copy row + + +def module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + loaded = importlib.util.module_from_spec(spec) + sys.modules[name] = loaded + spec.loader.exec_module(loaded) + return loaded + + +def rows(profile): + m = int(profile["m"]) + hist = {int(r): int(n) for r, n in profile["child_multiplicities"].items() if n} + W, N = int(profile["W"]), int(profile["N"]) + assert sum(r * n for r, n in hist.items()) == m * W - N, "row identity" + return m, W, N, hist + + +def row_profile(m, W, N, hist): + hist = {int(r): int(n) for r, n in hist.items() if n} + total = sum(r * n for r, n in hist.items()) + assert total == m * W - N, "row identity" + return dict(m=m, W=W, N=N, L=0, total_rank=total, maxchild=max(hist), + child_multiplicities={str(r): n for r, n in hist.items()}) + + +def saving_paid(interval, profile): + """The bit side's own convention in the frontier certificate: with the fallback.""" + low, high = 0, SAVING_GRID // 100 + def moment(a): + raw = interval.moment(profile, a) + m, W = profile["m"], profile["W"] + edges = sum(profile["child_multiplicities"].values()) + lo, hi = interval.log_interval(Q(m)) + elo, ehi = interval.exp_interval(a * lo, a * hi) + weight = BAD * Q(32 * m * m * edges, W * m) + return raw["upper"] + weight * ehi, raw["lower"] + weight * elo + assert moment(Q(low, SAVING_GRID))[0] < 1 and moment(Q(high, SAVING_GRID))[1] > 1 + while high - low > 1: + mid = (low + high) // 2 + if moment(Q(mid, SAVING_GRID))[0] < 1: + low = mid + else: + high = mid + assert moment(Q(low, SAVING_GRID))[0] < 1 < moment(Q(high, SAVING_GRID))[1] + return Q(low, SAVING_GRID) + + +def schedule(m, hist): + """Every family whose rank divides the bank width, with its bank arithmetic.""" + out = [] + for rank in sorted(hist): + if m % rank: + continue + blocks = m // rank + count = hist[rank] + volume = rank * count + out.append(dict( + rank=rank, children=count, blocks_per_bank=blocks, + rank_volume=volume, banks=volume // m, + whole_banks=volume % m == 0, + condition="children divisible by %d" % blocks, + per_copy_children=count // COPIES if count % COPIES == 0 else None, + per_copy_banks=(volume // m) // COPIES if volume % m == 0 + and (volume // m) % COPIES == 0 else None)) + return out + + +def checklist(rung): + """The supplier's bank proof, item by item, read against this rung.""" + return [ + dict(item="block partition of the bank", + in_the_proof="P_s(j) = 1[j div 4 = s] for s = 0..17 and Q_s(j) = " + "1[j div 24 = s] for s = 0,1,2, on j = 0..71; each family " + "disjoint, idempotent and exhaustive", + status="new instance, inherited algebra", + note="a rank-6 partition is the same construction with stride 6 " + "(12 blocks), so `S_P S_Q = S_{P+Q}` and `S_P^2 = I` need no new " + "proof: the proof states them for any finite disjoint projector " + "partition summing to I. The stride-6 partition itself is new."), + dict(item="normalizer and the child-to-block map", + in_the_proof="the banked items are the 2,200 rank-60 gauge exteriors, " + "one per selected entrance gauge, and the gauge's own " + "itinerary supplies the address", + status="NEW, and blank in the queue", + note="the rank-6 family is interior dirt with no registered gauge " + "address, and no pinned package enumerates it: this is the same " + "gap that stops the complex rung (an inventory obligation). The " + "counts match exactly -- one block per absorbed child -- but which " + "child goes to which block is not in any pin."), + dict(item="charts for the new block frames", + in_the_proof="one common invertible weighted chart per bank, with " + "inverse; product(A S_P A^-1) = A (product S_P) A^-1", + status="new instance", + note="integer kernel bases with fraction-free inverses and replayed " + "elementary factors for the stride-6 blocks; the certified proof's " + "universal conjugation covers any common weighted chart, so this is " + "work rather than new theory."), + dict(item="the two-bank address-map columns", + in_the_proof="144 columns of each two-bank address map over F2 and over " + "Z, for the endpoint and its inverse, rejecting a missing " + "last block and a repeated last block in both rings", + status="inherited check, new instance", + note="144 = 2 rings x 72 coordinates, so the check is unchanged in " + "shape; it has to be run on the stride-6 address map."), + dict(item="per-block prime witnesses", + in_the_proof="prime supply and residual factors below the retained q " + "bound", + status="new supply", + note="%d blocks over three copies need distinct integer Gram/prime " + "witnesses; the certified supply is per block frame, not per bank." + % rung["blocks_three_copies"]), + dict(item="moment-envelope parity", + in_the_proof="rare-class fraction 10^-16, fallback 32*72^2 children per " + "edge, the positive atom/row-adapter toll on its own 10^-24 " + "grid, and two independent rational log/exp enclosures " + "certifying the accepted moment and rejecting the adjacent " + "10^-18 grid point", + status="already satisfied in this package", + note="the retained ledger, stock and deficit are stated below and the " + "certified saving is recomputed with the supplier's own enclosure " + "implementation; the fallback bill is unchanged because the word's " + "edges are unchanged."), + dict(item="the assembly", + in_the_proof="47 strict constraints and 7 margins at the selected " + "parameters", + status="verified here", + note="PR207's unchanged rule on the two side savings; the rung is " + "bit-binding, so the complex budget is untouched and the binding " + "side value is the banked bit row's own."), + dict(item="stage-private allocation", + in_the_proof="1100 selected and 47484 undeferred banks per stage, with " + "nine physical replicas making each stage-private " + "allocation integral", + status="inference, not verified", + note="the per-copy bank count here is %s; reading the rung as three " + "stage-private families gives %s per stage, so the allocation would " + "be integral without replicas -- but no pin states that the rank-6 " + "dirt is stage-private, so this is an inference." + % (rung["banks_per_copy"], rung["banks_per_copy"] // 3)), + dict(item="the inherited conditional interfaces", + in_the_proof="all-input weighted compiler, completed-core routing, stage " + "cover, local-ring precision/recovery, prime supply, " + "uniform setup, all-size analytic and tape contracts remain " + "conditional", + status="conditional in the record itself", + note="no finite bank verification discharges these, and neither does " + "this package."), + ] + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, default=HERE / "instantiate.json") + parser.add_argument("--check", action="store_true") + args = parser.parse_args() + if hasattr(sys, "set_int_max_str_digits"): + sys.set_int_max_str_digits(0) + assert not sys.flags.optimize, "assertions must stay enabled" + + source = json.loads((HERE / "SOURCE.json").read_text()) + for pin in source["pins"]: + digest = hashlib.sha256((HERE / pin["path"]).read_bytes()).hexdigest() + assert digest == pin["sha256"], ("pin hash mismatch", pin["path"]) + interval = module("inst_interval_moment", HERE / "references/pr200/interval_moment.py") + cert = json.loads((HERE / "references/queue/pr207-coordinated-crossover.certificate.json").read_text()) + m, W, N, hist = rows(cert["bit_profile"]) + assert BANK_RANK in hist, "the rung's family must be in the word" + + # ---- the schedule of every bankable family on both words ---------------- + words = {} + for side, key in (("bit", "bit_profile"), ("complex", "complex_profile")): + w_m, w_W, w_N, w_hist = rows(cert[key]) + words[side] = dict(m=w_m, W=w_W, deficit=w_N, families=len(w_hist), + schedule=schedule(w_m, w_hist)) + rung_schedule = [row for row in words["bit"]["schedule"] if row["rank"] == BANK_RANK][0] + assert rung_schedule["whole_banks"] and rung_schedule["per_copy_banks"], \ + "the rung must fill whole banks with an integral per-copy count" + + # ---- the rung's arithmetic, re-derived ---------------------------------- + count_three = hist[BANK_RANK] + count_copy = count_three // COPIES + assert count_three % COPIES == 0, "the family is integral per copy" + blocks_per_bank = m // BANK_RANK + banks_copy = rung_schedule["per_copy_banks"] + taken = BANK_RANK * count_three + kept = {r: n for r, n in hist.items() if r != BANK_RANK} + mass = sum(r * n for r, n in kept.items()) + stock, leftover = divmod(mass + N, m) + assert leftover == 0 and stock == W - taken // m, "row identity after absorption" + base = saving_paid(interval, row_profile(m, W, N, hist)) + banked = saving_paid(interval, row_profile(m, stock, N, kept)) + published = Q(cert["a_bit"]) + assert abs(base / published - 1) < Q(1, 10 ** 12), "the certificate's bit saving" + grid = 10 ** 16 + kappa = lambda a: Q((a / (1 + a)).numerator * grid // (a / (1 + a)).denominator, grid) + frontier = kappa(base) + gain = kappa(banked) / frontier - 1 + rung = dict( + family_rank=BANK_RANK, bank_width=m, blocks_per_bank=blocks_per_bank, + children_three_copies=count_three, children_per_copy=count_copy, + rank_volume=taken, banks_three_copies=taken // m, banks_per_copy=banks_copy, + blocks_three_copies=blocks_per_bank * (taken // m), + blocks_per_copy=blocks_per_bank * banks_copy, + stock_before=W, stock_after=stock, stock_fall=W - stock, + rank_mass_before=m * W - N, rank_mass_after=mass, + deficit=str(N), maxchild_after=max(kept), + retained_families=len(kept), certified_saving=str(banked), + certified_saving_decimal=float(banked), frontier_kappa=str(frontier), + kappa=str(kappa(banked)), gain=str(gain)) + # one block per absorbed child, count for count: the bijection is a bijection + assert rung["blocks_per_copy"] == rung["children_per_copy"], \ + "one rank-6 block per absorbed child" + assert blocks_per_bank * BANK_RANK == m, "the blocks tile the bank" + # the block patterns that tile the same width: this rung's, and the certified ones + uniform = {"rank6_this_rung": (blocks_per_bank, BANK_RANK), "rank4_certified": (18, 4), + "rank24_certified": (3, 24)} + sums = {name: count * rank for name, (count, rank) in uniform.items()} + sums["mixed_certified"] = 6 * 4 + 2 * 24 + tilings = dict( + patterns={name: "%d x %d" % pair for name, pair in uniform.items()} | + {"mixed_certified": "6 x 4 + 2 x 24"}, + sums=sums, all_tile_the_width=all(value == m for value in sums.values())) + assert tilings["all_tile_the_width"], tilings + assert tilings["patterns"]["rank6_this_rung"] == "%d x %d" % (blocks_per_bank, BANK_RANK) + + checklist_rows = checklist(rung) + out = dict( + status="Read-only: no construction, no new word, no bank. This states what " + "the +2.167% rung's arithmetic is and what the supplier's published " + "bank proof already covers for it.", + method="the frontier certificate's own three-copy rows, the supplier's " + "enclosure implementation, and the supplier's bank proof read item by " + "item; every count below is derived, not quoted", + source=dict(certificate="references/queue/pr207-coordinated-crossover.certificate.json", + bank_proof="references/queue/coordinated-bank-proof.md", + arithmetic="references/pr200/interval_moment.py"), + validated=dict( + certificate_bit_saving=str(published), + recomputed_bit_saving=str(base), + relative_gap=str(base / published - 1), + note="the recomputation is the certificate's own value to sixteen " + "significant digits; the residual is in beats.json's validations"), + schedule={side: words[side] for side in words}, + rung=rung, + tilings=tilings, + checklist=checklist_rows, + verdict=( + "The rung's arithmetic is exact and its saving is certifiable with the " + "tooling already in this package. Its construction reduces to a new " + "block stride plus the items the certified bank spent on the gauge " + "exteriors: the universal projector algebra is inherited (the proof " + "states it for any disjoint exhaustive partition), the 144-column " + "address check and the moment-envelope parity are inherited in shape, " + "and the per-copy allocation is integral, so this rung does not need the " + "nine physical replicas the certified allocation used. What does not " + "exist is the part that identifies the dirt: no pin enumerates the " + "word's rank-6 children, so the normalizer, the charts and the prime " + "witnesses have nothing to be attached to yet. That is the same blank " + "shape as the complex rung's inventory obligation, and it is smaller: " + "one family of one word, whose counts and bank schedule are already " + "pinned by this file."), + limits=[ + "No bank is built, no chart is computed, no witness is supplied and no " + "physical word is replayed: the checklist states what would be needed.", + "The stage-private reading is an inference (the per-copy count is " + "divisible by three); no pin says the rank-6 dirt is stage-private.", + "The rank-6 family is interior dirt: the certified proof removed the " + "entrance exteriors, and the frontier profile no longer carries them.", + ]) + text = json.dumps(out, indent=1, sort_keys=True) + "\n" + if args.check: + if args.out.read_text() != text: + print("[check] MISMATCH: instantiate.json does not match a fresh run") + return 1 + print("[check] instantiate.json matches a fresh run byte for byte") + return 0 + args.out.write_text(text, newline="\n") + + print("[rung] absorb the bit word's rank-%d family on width %d" % (BANK_RANK, m)) + print(" %d children over three copies = %d per copy; %d blocks per bank, " + "one per child" % (count_three, count_copy, blocks_per_bank)) + print(" %d banks over three copies = %d per copy (integral); volume %d" + % (taken // m, banks_copy, taken)) + print(" stock %d -> %d (fall %d), rank mass %d -> %d, deficit %s unchanged" + % (W, stock, W - stock, m * W - N, mass, N)) + print(" saving %s -> %s; kappa %s -> %s (%+.4f%%)" + % (base, banked, frontier, kappa(banked), float(gain) * 100)) + for row in words["bit"]["schedule"] + words["complex"]["schedule"]: + print(" [%s] rank %-2d: %d blocks/bank, %-5s banks, children divisible " + "by %d: %s" % ("bankable" if row["whole_banks"] else "no bank ", + row["rank"], row["blocks_per_bank"], row["banks"], + row["blocks_per_bank"], "yes" if row["whole_banks"] else "NO")) + for item in checklist_rows: + print("[%-34s] %s" % (item["status"], item["item"])) + print("[write] " + str(args.out)) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/frontier-beat-2026-10-09/references/pr200/interval_moment.py b/research/frontier-beat-2026-10-09/references/pr200/interval_moment.py new file mode 100644 index 0000000000..c135d98d86 --- /dev/null +++ b/research/frontier-beat-2026-10-09/references/pr200/interval_moment.py @@ -0,0 +1,76 @@ +"""Independent exact interval moments; no floating point or producer execution. + +Positive atanh series, range reduction by 4/3, explicit geometric tails, +80 logarithm terms and degree-12 exponential enclosures. The final rounding +is outward on the 10^-45 grid. Prepared with OpenAI Codex assistance. +""" +from fractions import Fraction as Q +from functools import lru_cache +from math import factorial +GRID = 10**45 +LOG_TERMS = 80 +EXP_DEGREE = 12 + +def require(ok, reason): + if not ok: raise ValueError(reason) + +def lower(x):return Q((x*GRID).numerator//(x*GRID).denominator,GRID) +def upper(x): + y=x*GRID + return Q(-((-y.numerator)//y.denominator),GRID) + +@lru_cache(None) +def log_interval(x): + x=Q(x);require(x>=1,'log interval domain') + base=Q(4,3);k=0 + while x>base:x/=base;k+=1 + def short(y): + z=(y-1)/(y+1);power=z;s=Q(0) + for j in range(LOG_TERMS):s+=power/Q(2*j+1);power*=z*z + lo=2*s;tail=2*power/(Q(2*LOG_TERMS+1)*(1-z*z)) + return lo,lo+tail + lo,hi=short(x);blo,bhi=short(base) + return lower(k*blo+lo),upper(k*bhi+hi) + +def exp_interval(lo,hi): + require(0<=lo<=hi1 and W>0,'profile dimensions') + raw=profile['child_multiplicities'];hist={int(t):n for t,n in raw.items()} + require(len(hist)==len(raw),'aliased histogram keys') + require(all(00 for t,n in hist.items()),'invalid child or multiplicity') + mass=sum(t*n for t,n in hist.items());require(mass==profile['total_rank']==W*m-profile['N']+profile['L'],'rank mass') + require(max(hist)==profile['maxchild'],'maximum child') + require(0=0,'nonnegative saving');lo=hi=Q(0);rows=[] + for t,n,L,U in prepare(profile): + E,F=exp_interval(a*L,a*U);w=Q(t*n,profile['m']*profile['W']);lo+=w*E;hi+=w*F + if details:rows.append(dict(child=t,multiplicity=n,log_lower=L,log_upper=U,exp_lower=E,exp_upper=F,contribution_lower=w*E,contribution_upper=w*F)) + result=dict(saving=a,lower=lo,upper=hi,strict_gap_lower=1-hi) + if details:result['terms']=rows + return result + +def saving_grid(profile,denominator=10**24): + require(type(denominator) is int and denominator>0,'positive saving grid') + prepare(profile);lo=0;hi=denominator//32;iterations=0 + require(moment(profile,Q(lo,denominator))['upper']<1,'initial contraction') + require(moment(profile,Q(hi,denominator))['lower']>1,'initial exclusion') + while hi-lo>1: + mid=(hi+lo)//2;m=moment(profile,Q(mid,denominator));iterations+=1 + if m['upper']<1:lo=mid + elif m['lower']>1:hi=mid + else:raise ValueError('Moment interval overlaps one; increase enclosure precision') + accepted=moment(profile,Q(lo,denominator),True);rejected=moment(profile,Q(hi,denominator),True) + require(accepted['upper']<1