From f9c5ad308690d9d45ff8d6ce3559194d5c13d750 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Wed, 11 Nov 2026 10:37:01 +0000 Subject: [PATCH] Count intermediate carries of the frame-506 inverse elimination The inverse of the published 5/5/14 word emits one carry digit on each scale and shear. Every low row has at most 19 nonzero digits, and the #7104 return row u(q) has exactly 13 for every odd integer q >= 5. The selected frontier is unchanged. Co-authored-by: unpaidmoon --- .../frame506-inverse-row-carries/PROOF.md | 172 +++++++ .../frame506-inverse-row-carries/README.md | 68 +++ .../frame506-inverse-row-carries/SOURCES.json | 36 ++ .../frame506-inverse-row-carries/TASK.json | 97 ++++ .../frame506-inverse-row-carries/VERIFY.json | 23 + .../frame506-inverse-row-carries/verify.py | 478 ++++++++++++++++++ 6 files changed, 874 insertions(+) create mode 100644 research/frame506-inverse-row-carries/PROOF.md create mode 100644 research/frame506-inverse-row-carries/README.md create mode 100644 research/frame506-inverse-row-carries/SOURCES.json create mode 100644 research/frame506-inverse-row-carries/TASK.json create mode 100644 research/frame506-inverse-row-carries/VERIFY.json create mode 100644 research/frame506-inverse-row-carries/verify.py diff --git a/research/frame506-inverse-row-carries/PROOF.md b/research/frame506-inverse-row-carries/PROOF.md new file mode 100644 index 0000000000..2c7fdc4b32 --- /dev/null +++ b/research/frame506-inverse-row-carries/PROOF.md @@ -0,0 +1,172 @@ +# Intermediate carries of one frame-506 inverse elimination + +This is a proof for one fixed elimination word, together with three exhaustive +finite censuses. It uses the carry formula of PR #4957, section 3, applied to +each elementary factor. It does not replace the closed-form envelope of PR +#7104, and it does not change the selected frontier. + +## Word + +The frozen frame 506 of helper 462 has rank 4. With image rows `B` and kernel +rows `A`, + +```text +S = [ B^T | A^T ]. +``` + +The same integer matrix is recorded in +`research/bit-completed-backend-api/science/RESULT.json`. Exact elimination, +the algorithm in that package's `science/check.py`, produces 5 swaps, 5 scales +and 14 shears. The published factor list is reproduced exactly, and the right +product is `S`. Reversing the word and inverting each factor produces a word +for `S^{-1}`: the same five swaps, with each scale `c` replaced by `1/c` and +each shear coefficient negated. PR #4957 does not fix this word as the physical +return. It is the inverse of the published elimination, and the count below is +the intermediate quotient of that word. + +Every scale or shear coefficient in the inverse word lies in `{1, -1, 1/2, -1/2}`. +`det S = -16`, so every denominator of `S^{-1}` divides 4. The residue used +below is unique for every odd integer `q`, because 2 is invertible modulo `q`. + +## One carry digit per scale and per shear + +A low row is an 8-tuple with coordinates in `{0, ..., q-1}`. An elementary +right factor acts on that row as follows. + +- A swap exchanges two coordinates. Both digits are already reduced, so the + PR #4957 quotient of the swap is 0. +- A scale multiplies one coordinate by a fixed rational and leaves the other + seven unchanged. The quotient of each unchanged coordinate is 0, so the + factor emits one carry digit. +- A shear adds a fixed rational multiple of one coordinate into one other + coordinate. Again only one coordinate changes, so the factor emits one + carry digit. + +The carry digit is the quotient `(z - h) / q` in `Z[1/2]`, where `z` is the +unreduced value of the updated coordinate and `h` is the unique element of +`{0, ..., q-1}` for which the difference is `q` times an element of `Z[1/2]`. +The digit is nonzero when that quotient is nonzero as a rational. + +The inverse word therefore has 19 arithmetic sites on one row. At most 19 of +them are nonzero. In particular the count is strictly less than 48, for every +low row and every odd integer `q`. This is the site bound. It is not a claim +about a longer factorization, and it is not the 48-correction closed form of +`S^{-1}` proved in #7104. + +## Named row + +PR #7104 attains its return envelope on the low type + +```text +u(q) = (q-2, q-2, q-5, q-5, 0, q-1, 0, 0), +``` + +which is a legal row for every integer `q ≥ 5`. The closed-form correction of +`u(q)` under `S^{-1}` has six nonzero entries. The calculation here follows +the inverse word instead of that closed form. + +For every odd integer `q ≥ 7`, each updated coordinate stays inside an affine +formula `A + s q` with `s ∈ {0, 1/2, 1}` and `A ∈ Z[1/2]`. The slope is the +unique value in `{0, 1/4, 1/2, 3/4, 1}` for which `A + s q` is an integer in +`{0, ..., q-1}` for every odd integer `q ≥ 7`. Integrality is checked on a +complete set of odd residues modulo the power-of-two denominator. Along each +residue class the value and the slack `q - value` are nondecreasing, because +the class step adds a nonnegative integer to both. The resulting digits are: + +| site | operation | unreduced value | residue | carry | +| ---: | --- | --- | --- | --- | +| 0 | `x7 += x3` | `q-5` | `q-5` | 0 | +| 1 | `x7 += -x2` | `0` | `0` | 0 | +| 2 | `x7 += -(1/2) x1` | `1 - q/2` | `1` | `-1/2` | +| 3 | `x7 += -(1/2) x0` | `2 - q/2` | `2` | `-1/2` | +| 4 | `x7 *= 1/2` | `1` | `1` | 0 | +| 5 | `x5 += -x3` | `4` | `4` | 0 | +| 6 | `x5 += (1/2) x1` | `3 + q/2` | `3` | `1/2` | +| 7 | `x5 += (1/2) x0` | `2 + q/2` | `2` | `1/2` | +| 8 | `x5 *= -1/2` | `-1` | `q-1` | `-1` | +| 9 | `x3 += -x7` | `q-6` | `q-6` | 0 | +| 10 | `x3 += -x2` | `-1` | `q-1` | `-1` | +| 11 | `x3 += -(1/2) x1` | `q/2` | `0` | `1/2` | +| 12 | `x3 += -(1/2) x0` | `1 - q/2` | `1` | `-1/2` | +| 13 | `x3 *= -1` | `-1` | `q-1` | `-1` | +| 14 | `x2 += x7` | `q-4` | `q-4` | 0 | +| 15 | `x2 += -x6` | `-3` | `q-3` | `-1` | +| 16 | `x2 += -x4` | `-2` | `q-2` | `-1` | +| 17 | `x1 *= 1/2` | `(q-2)/2` | `q-1` | `-1/2` | +| 18 | `x0 *= 1/2` | `(q-2)/2` | `q-1` | `-1/2` | + +Swaps sit between these sites and emit no digit: `x5` with `x6`, then `x4` +with `x5`, after site 8; `x3` with `x4` after site 13; `x1` with `x6` after +site 17; `x0` with `x5` after site 18. Thirteen of the nineteen digits are +nonzero. The final low row is + +```text +(0, q-1, q-2, 0, q-1, q-1, q-1, 1). +``` + +Starting from high part 0, the same quotients update the high coordinates. +The final high row is the constant + +```text +(0, -3/2, -1/2, 0, -1/2, -1/2, -1/2, -1/2), +``` + +which is the closed-form return correction of `u(q)` from #7104. The +intermediate word therefore emits 13 nonzero quotients on this row, and those +quotients compose to the 6-nonzero closed form. Dropping the quotients while +retaining the linear action misses that high row. + +The odd integer `q = 5` is the one odd integer `≥ 5` at which `q - 6` is +negative, so site 9 is outside the tail formula. Direct evaluation of this +single row gives the same digits, except site 9 is `-1` and site 10 is `0`. +The nonzero count remains 13, and the final low and high rows are the same +`q = 5` specializations. That evaluation visits each of the 19 sites once. + +The zero row emits the zero quotient at every site, so 13 is the count on +`u(q)`, and it is a maximum only in the sense of the separate censuses below. + +## Censuses + +For an odd prime `q`, the domain `{0, ..., q-1}^8` is finite. The base-`q` +code of an integer in `{0, ..., q^8 - 1}` visits each row once. On every +coefficient that occurs, the integer nonzero test agrees with the rational +quotient for every digit the operation reads; that agreement is checked for +`q ∈ {3, 5, 7}` before the scan. + +| q | domain | maximum nonzero sites | rows at the maximum | +| ---: | ---: | ---: | ---: | +| 3 | 6561 | 18 | 9 | +| 5 | 390625 | 18 | 575 | +| 7 | 5764801 | 19 | 245 | + +The maxima are attained by `(1,1,1,2,0,0,0,1)`, `(1,1,1,4,0,0,0,1)` and +`(5,5,6,3,0,0,0,4)` respectively. Each of those three counts was recomputed +with the rational quotient, independently of the scan. The full histograms +are the constants in `verify.py`. + +These are exhaustive censuses of those three domains. They do not by +themselves determine the maximum at any other prime. The site bound of 19 +already covers every odd integer `q`. The prime 7 shows that 19 is attained, +so no smaller uniform site bound holds for every odd prime. Every counted row +is still strictly below 48. + +## What this does not change + +The 5/5/14 word, the owners, ROW restoration, P1–P3, the native compiler and +the exponent gaps stay as PR #4957 left them. The closed-form envelopes 48 +per route and 96 for the pair, and the `q = 3` pair maximum 88, stay as +#7104 proved them. Repeating `u(q)` on all eight high rows emits +`8 * 13 = 104` nonzero intermediate quotients. That route total is a +different number from the closed-form 48, and this note does not put either +number into a charged bill. + +The selected frontier stays `363005817/100000000000`. + +## Controls + +The range test rejects residue `q - 6` at `q = 5` and accepts it for every +odd integer `q ≥ 7`. The zero row pays nothing. Omitting the quotients in the +high update misses the closed-form correction on `u(q)`. A scale or shear +coefficient outside `{±1, ±1/2}` is rejected before a census. The published +factor list, the helper-462 endpoints and the selected-frontier string are +read from the pinned inputs. diff --git a/research/frame506-inverse-row-carries/README.md b/research/frame506-inverse-row-carries/README.md new file mode 100644 index 0000000000..ebd9894f7e --- /dev/null +++ b/research/frame506-inverse-row-carries/README.md @@ -0,0 +1,68 @@ +# Intermediate carries on one row of the frame-506 inverse elimination + +**Proof, plus three exhaustive finite censuses. No new κ.** The selected +frontier stays `363005817/100000000000`. + +## Result + +The published frame-506 elimination has 5 swaps, 5 scales and 14 shears. Its +inverse is an elimination word for `S^{-1}`. PR #4957 does not fix that word +as the physical return. Each scale and each shear emits one carry digit on a +low row, under the quotient `(z - h) / q` from PR #4957, section 3. A swap +emits none. + +- On every low row, and for every odd integer `q`, at most **19** of those + digits are nonzero. Nineteen is strictly less than 48. +- On the #7104 return row `u(q) = (q-2, q-2, q-5, q-5, 0, q-1, 0, 0)`, exactly + **13** digits are nonzero for every odd integer `q ≥ 5`. The digits are + constant for every odd integer `q ≥ 7`, and the single row `q = 5` differs + in two sites while keeping the same count. The digits are attached to the + 19 factors in [PROOF.md](PROOF.md). +- Those 13 quotients compose to the 6-nonzero closed-form correction of #7104. + The closed-form route envelope remains 48. This note counts one row of one + word. +- Exhaustive base-`q` censuses give maximum 18 at `q = 3` (domain 6561), + maximum 18 at `q = 5` (domain 390625) and maximum 19 at `q = 7` (domain + 5764801). The bound 19 is attained, and every row in those domains is still + below 48. + +## Task + +Catalogue card `supplier-boundary-audit`, scope **refined**. The open question +answered here is question 1 of PR #7104: the intermediate digits of an +elimination word for `S^{-1}` on one high row. The 48/96 closed form and the +published 64/128 envelope are left as proved. Question 2 of #7104, a charged +bill that moves an exponent, is not taken. + +Base `e54523517d0f03e58352e647c403a5af3e525a57`. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B research/frame506-inverse-row-carries/verify.py +python3 -B scripts/research_package.py --package research/frame506-inverse-row-carries +``` + +The direct checker prints `PASS_FRAME506_INVERSE_ROW_CARRIES`. + +## Open next questions + +1. For which odd primes is the one-row maximum exactly 19? The censuses give + 18 at `q = 3` and `q = 5`, and 19 at `q = 7`. The next finite domain is + `q = 9`, with `9^8 = 43046721` rows, under the same base-`q` scan. No + algebraic blocker is known; this package stops after the three recorded + domains. +2. Does some other elimination word for `S^{-1}` emit 48 or more nonzero + intermediate digits on one row? The 19-site bound uses this inverse of the + published 5/5/14 word. A longer factorization has more sites. PR #4957 + does not designate another return word, and this package does not search + one. + +## Credit + +The matcher, the 5/5/14 elimination and the carry formula are from PR #4957 +(Chris R / Clear1nsight, with the retained #4760/#4814 lineage). The named +row and the closed-form correction it composes to are from PR #7104. +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/frame506-inverse-row-carries/SOURCES.json b/research/frame506-inverse-row-carries/SOURCES.json new file mode 100644 index 0000000000..710a01e60b --- /dev/null +++ b/research/frame506-inverse-row-carries/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-completed-backend-api/independent/inputs/WORD.json.gz", + "usage": "input", + "git_blob": "776ddd13d67b2259e90d39de5b42e4df4b1447f1", + "sha256": "69fc50430f0062c040e0686f59ad32ee5af2387ae9a97d7d11b4af1aa994ed5b" + }, + { + "path": "research/bit-completed-backend-api/independent/inputs/frames.json", + "usage": "input", + "git_blob": "a9a932b9268da28af9ba4bccdab205c5bcd50ad3", + "sha256": "d006b3bfe0c04afecfea7aecfa59dfe4298b99501c70da3938e40289bc2f5010" + }, + { + "path": "research/bit-completed-backend-api/science/RESULT.json", + "usage": "input", + "git_blob": "55dca30281e3375d63a128c3de041e46c8a3c5ba", + "sha256": "965b650c0e49572e028f89a60943c64ad8dff9032fc93272b86cd1f9715a77b7" + } + ] +} diff --git a/research/frame506-inverse-row-carries/TASK.json b/research/frame506-inverse-row-carries/TASK.json new file mode 100644 index 0000000000..168953007b --- /dev/null +++ b/research/frame506-inverse-row-carries/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "For the inverse of the published 5/5/14 frame-506 elimination, attach one carry digit to each of the 5 scales and 14 shears and count the nonzero digits on one low row.", + "scope_change_reason": "PR #7104 leaves open the intermediate-carry count of an elimination word for S^{-1} on one high row. This package answers that count for the inverse of the published word. It does not claim supplier admission.", + "bottleneck_link": "BIT is the next cap after the selected complex supplier. One row of intermediate carry digits is a finer reading of the same frame-506 route. The predecessor already treats a finite carry constant as lower order, so the count does not by itself move kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the site bound, the closed form on u(q), and the exhaustive censuses at q=3, 5 and 7. Do not retune an exponent or replace the 5/5/14 word.", + "outcome": "partial", + "evidence": "PROOF.md range argument for every odd integer q>=7 on u(q), direct evaluation of the one row q=5, and exhaustive base-q censuses of all 3^8, 5^8 and 7^8 low rows. The selected frontier string is read and left unchanged.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance. The proof and checker were written with that assistance; no separate human review is claimed.", + "open_questions": [ + { + "question": "For which odd primes is the one-row maximum of this inverse word exactly 19?", + "why_it_matters": "The site bound 19 is attained at q=7 and missed at q=3 and q=5, so the uniform bound is sharp while the small primes are not.", + "first_step": "Run the same base-q census on the domain of q=9, which has 9^8 = 43046721 rows.", + "blocked_by": "Nothing algebraic. The q=9 domain did not fit beside the q=7 census in this replay." + }, + { + "question": "Does another elimination word for S^{-1} emit 48 or more nonzero intermediate digits on one row?", + "why_it_matters": "The 19-site bound is special to the inverse of the published 5/5/14 word. A longer word has more sites.", + "first_step": "Fix one other explicit factorization of S^{-1} into swaps, scales and shears, and count its nonzero quotients on u(q).", + "blocked_by": "PR #4957 does not designate a second return word." + } + ] +} diff --git a/research/frame506-inverse-row-carries/VERIFY.json b/research/frame506-inverse-row-carries/VERIFY.json new file mode 100644 index 0000000000..38148b0482 --- /dev/null +++ b/research/frame506-inverse-row-carries/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/bit-completed-backend-api/independent/inputs/WORD.json.gz", + "research/bit-completed-backend-api/independent/inputs/frames.json", + "research/bit-completed-backend-api/science/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Pinned frame, helper-462 endpoints, published 5/5/14 factors, inverse word, site bound 19, closed-form 13 digits on u(q) for odd q>=7, direct q=5 row, high-part composition, zero-row and dropped-carry controls, integer-quotient agreement, exhaustive histograms at q=3, 5 and 7, selected frontier string unchanged." + } + ] +} diff --git a/research/frame506-inverse-row-carries/verify.py b/research/frame506-inverse-row-carries/verify.py new file mode 100644 index 0000000000..fdec25c673 --- /dev/null +++ b/research/frame506-inverse-row-carries/verify.py @@ -0,0 +1,478 @@ +#!/usr/bin/env python3 +"""Intermediate carries of the published frame-506 inverse elimination. + +Proof for one fixed word, plus exhaustive censuses at the odd primes 3, 5 and 7. +No new kappa. Standard library only. +""" + +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +import gzip +import json +import sys + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +QMIN_NAMED = 5 +QMIN_TAIL = 7 +CLOSED = (F(0), F(-3, 2), F(-1, 2), F(0), F(-1, 2), F(-1, 2), F(-1, 2), F(-1, 2)) +# Carry digits of the 5 scales and 14 shears, in word order, on u(q) for odd q >= 7. +TAIL_CARRIES = ( + F(0), F(0), F(-1, 2), F(-1, 2), F(0), F(0), F(1, 2), F(1, 2), F(-1), + F(0), F(-1), F(1, 2), F(-1, 2), F(-1), F(0), F(-1), F(-1), F(-1, 2), F(-1, 2), +) +# The single odd integer q = 5, where q - 6 is negative. Direct evaluation. +FIVE_CARRIES = ( + F(0), F(0), F(-1, 2), F(-1, 2), F(0), F(0), F(1, 2), F(1, 2), F(-1), + F(-1), F(0), F(1, 2), F(-1, 2), F(-1), F(0), F(-1), F(-1), F(-1, 2), F(-1, 2), +) +# First base-q row that attains the census maximum. Coordinates are base-q digits. +CENSUS = { + 3: { + "max": 18, + "witness": (1, 1, 1, 2, 0, 0, 0, 1), + "hist": (36, 36, 189, 351, 423, 675, 702, 693, 918, 747, 639, 450, 270, 189, 117, 72, 45, 0, 9, 0), + }, + 5: { + "max": 18, + "witness": (1, 1, 1, 4, 0, 0, 0, 1), + "hist": (225, 625, 3350, 7650, 15175, 26475, 28700, 35600, 50700, 50525, 42475, 38200, 32650, 25150, 15000, 9650, 5675, 2225, 575, 0), + }, + 7: { + "max": 19, + "witness": (5, 5, 6, 3, 0, 0, 0, 4), + "hist": (784, 4655, 23324, 65611, 161749, 305025, 344715, 447615, 688744, 741419, 651406, 620879, 576436, 463050, 287875, 188895, 119903, 57869, 14602, 245), + }, +} + + +def need(ok, message): + if not ok: + raise SystemExit(message) + + +def eye(n): + return [[F(i == j) for j in range(n)] for i in range(n)] + + +def mm(a, b): + return [[sum((x * y for x, y in zip(row, col)), F(0)) for col in zip(*b)] for row in a] + + +def transpose(rows): + return [list(col) for col in zip(*rows)] + + +def load_pins(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + pinned = {} + for row in sources["files"]: + if row["usage"] != "input": + continue + path = ROOT / row["path"] + data = path.read_bytes() + need(sha256(data).hexdigest() == row["sha256"], "sha256 mismatch: " + row["path"]) + pinned[row["path"]] = data + return pinned + + +def matcher_from_frame(raw): + frame = json.loads(raw)["frames"]["506"] + need(frame["dim"] == 4, "frame 506 rank") + blocks = [[F(x) for x in row] for row in frame["B"] + frame["A"]] + need(len(blocks) == 8 and all(len(row) == 8 for row in blocks), "frame 506 shape") + return transpose(blocks) + + +def decompose(matrix): + """Published deterministic elimination. Factors are the right-product for matrix.""" + work = [row[:] for row in matrix] + n = len(matrix) + factors = [] + for column in range(n): + pivot = next(row for row in range(column, n) if work[row][column]) + elementary = eye(n) + if pivot != column: + work[column], work[pivot] = work[pivot], work[column] + elementary[column], elementary[pivot] = elementary[pivot], elementary[column] + factors.append(elementary) + elementary = eye(n) + pivot_value = work[column][column] + if pivot_value != 1: + work[column] = [entry / pivot_value for entry in work[column]] + elementary[column][column] = pivot_value + factors.append(elementary) + elementary = eye(n) + for row in range(n): + if row != column and work[row][column]: + coefficient = -work[row][column] + work[row] = [entry + coefficient * source for entry, source in zip(work[row], work[column])] + elementary = eye(n) + elementary[row][column] = -coefficient + factors.append(elementary) + need(work == eye(n), "elimination did not reach I") + product = eye(n) + for factor in factors: + product = mm(product, factor) + need(product == matrix, "right product is not the matcher") + return factors + + +def transposition(factor): + n = len(factor) + images = [] + for row in factor: + hits = [column for column, entry in enumerate(row) if entry != 0] + if len(hits) != 1 or row[hits[0]] != 1: + return None + images.append(hits[0]) + if sorted(images) != list(range(n)): + return None + moved = [index for index, image in enumerate(images) if image != index] + if len(moved) != 2: + return None + left, right = moved + if images[left] != right or images[right] != left: + return None + return left, right + + +def classify(factor): + """Right action on one row: swap, scale one coordinate, or add into one coordinate.""" + swapped = transposition(factor) + if swapped: + return ("swap", swapped[0], swapped[1], F(1)) + n = len(factor) + off = [(row, column, factor[row][column]) for row in range(n) for column in range(n) if row != column and factor[row][column] != 0] + if len(off) == 1: + source, target, coefficient = off[0] + for row in range(n): + for column in range(n): + if (row, column) == (source, target): + continue + need(factor[row][column] == (1 if row == column else 0), "shear is not elementary") + return ("add", target, source, coefficient) + need(not off, "factor is not an elementary scale") + changed = [(index, factor[index][index]) for index in range(n) if factor[index][index] != 1] + need(len(changed) == 1 and changed[0][1] != 0, "scale is not a single nonzero unit") + index, coefficient = changed[0] + return ("scale", index, index, coefficient) + + +def inverse_word(factors): + word = [] + matrices = [] + n = len(factors[0]) + for factor in reversed(factors): + kind = classify(factor) + inverse = eye(n) + if kind[0] == "swap": + left, right = kind[1], kind[2] + inverse[left], inverse[right] = inverse[right], inverse[left] + elif kind[0] == "scale": + inverse[kind[1]][kind[1]] = 1 / kind[3] + else: + target, source, coefficient = kind[1], kind[2], kind[3] + inverse[source][target] = -coefficient + need(mm(factor, inverse) == eye(n), "elementary inverse") + matrices.append(inverse) + word.append(classify(inverse)) + return word + + +def prove_range(constant, slope, qmin): + """True when constant + slope*q is an integer in {0, ..., q-1} for every odd integer q >= qmin. + + The slope has to lie in [0, 1]. Integrality is checked on every odd residue class modulo the + power-of-two denominator. Both the value and the slack q - value are then nondecreasing along + that class, because a step by the period adds a nonnegative integer to each. + """ + if not (F(0) <= slope <= 1): + return False + denominator = max(constant.denominator, slope.denominator) + if denominator & (denominator - 1): + return False + if (slope * denominator).denominator != 1 or (constant * denominator).denominator != 1: + return False + period = denominator + classes = 1 if period == 1 else period // 2 + start = qmin if qmin % 2 else qmin + 1 + seen = {} + q = start + while len(seen) < classes: + residue = q % period + if residue not in seen: + value = constant + slope * q + if value.denominator != 1 or not (0 <= value < q): + return False + seen[residue] = q + q += 2 + if q > start + 4 * period + 4: + return False + step = 2 if period == 1 else period + if (slope * step).denominator != 1: + return False + if slope * step < 0 or step * (1 - slope) < 0: + return False + return len(seen) == classes + + +def choose_slope(constant, linear, qmin): + found = [] + for numerator in range(5): + slope = F(numerator, 4) + if prove_range(constant, slope, qmin): + found.append((slope, linear - slope)) + need(len(found) == 1, "carry slope is not unique at qmin %s" % qmin) + return found[0] + + +def affine_tail(word): + """Closed form of every scale and shear carry on u(q) for odd q >= 7.""" + low = [ + (F(-2), F(1)), (F(-2), F(1)), (F(-5), F(1)), (F(-5), F(1)), + (F(0), F(0)), (F(-1), F(1)), (F(0), F(0)), (F(0), F(0)), + ] + for constant, slope in low: + need(prove_range(constant, slope, QMIN_NAMED), "u(q) digit leaves range") + high = [F(0)] * 8 + carries = [] + for kind, target, source, coefficient in word: + if kind == "swap": + low[target], low[source] = low[source], low[target] + high[target], high[source] = high[source], high[target] + continue + if kind == "scale": + unreduced_constant = coefficient * low[target][0] + unreduced_linear = coefficient * low[target][1] + slope, carry = choose_slope(unreduced_constant, unreduced_linear, QMIN_TAIL) + high[target] = coefficient * high[target] + carry + low[target] = (unreduced_constant, slope) + else: + unreduced_constant = low[target][0] + coefficient * low[source][0] + unreduced_linear = low[target][1] + coefficient * low[source][1] + slope, carry = choose_slope(unreduced_constant, unreduced_linear, QMIN_TAIL) + high[target] = high[target] + coefficient * high[source] + carry + low[target] = (unreduced_constant, slope) + carries.append(carry) + return low, high, carries + + +def split(value, q): + residue = (value.numerator * pow(value.denominator, -1, q)) % q + return residue, (value - residue) / q + + +def direct(word, row, q): + low = list(row) + high = [F(0)] * 8 + carries = [] + for kind, target, source, coefficient in word: + if kind == "swap": + low[target], low[source] = low[source], low[target] + high[target], high[source] = high[source], high[target] + continue + if kind == "scale": + residue, carry = split(low[target] * coefficient, q) + high[target] = coefficient * high[target] + carry + low[target] = residue + else: + residue, carry = split(low[target] + coefficient * low[source], q) + high[target] = high[target] + coefficient * high[source] + carry + low[target] = residue + carries.append(carry) + return low, high, carries + + +def direct_without_carry(word, row, q): + low = list(row) + high = [F(0)] * 8 + for kind, target, source, coefficient in word: + if kind == "swap": + low[target], low[source] = low[source], low[target] + high[target], high[source] = high[source], high[target] + elif kind == "scale": + residue, _carry = split(low[target] * coefficient, q) + high[target] = coefficient * high[target] + low[target] = residue + else: + residue, _carry = split(low[target] + coefficient * low[source], q) + high[target] = high[target] + coefficient * high[source] + low[target] = residue + return high + + +def integer_nonzero(kind, target_digit, source_digit, coefficient, q): + """Equivalent to a nonzero rational quotient for coefficients in {±1, ±1/2}.""" + inverse_two = pow(2, -1, q) + if kind == "scale": + if coefficient.denominator == 1: + value = target_digit * int(coefficient) + return value != value % q + multiple = target_digit * int(coefficient.numerator) + residue = (multiple * inverse_two) % q + return multiple != 2 * residue + if coefficient.denominator == 1: + value = target_digit + int(coefficient) * source_digit + return value != value % q + multiple = 2 * target_digit + int(coefficient.numerator) * source_digit + residue = (multiple * inverse_two) % q + return multiple != 2 * residue + + +def fraction_nonzero(kind, target_digit, source_digit, coefficient, q): + if kind == "scale": + _residue, carry = split(target_digit * coefficient, q) + else: + _residue, carry = split(target_digit + coefficient * source_digit, q) + return carry != 0 + + +def census(word, q): + inverse_two = pow(2, -1, q) + prepared = [] + for kind, target, source, coefficient in word: + if kind == "swap": + prepared.append(("swap", target, source)) + continue + need(coefficient.denominator in (1, 2), "census coefficient outside the proved family") + prepared.append((kind, target, source, int(coefficient.numerator), coefficient.denominator)) + counts = [0] * 20 + total = q ** 8 + for code in range(total): + digits = [(code // q ** index) % q for index in range(8)] + nonzero = 0 + for op in prepared: + if op[0] == "swap": + digits[op[1]], digits[op[2]] = digits[op[2]], digits[op[1]] + continue + kind, target, source, numerator, denominator = op + if kind == "scale": + if denominator == 1: + value = digits[target] * numerator + residue = value % q + hit = value != residue + else: + multiple = digits[target] * numerator + residue = (multiple * inverse_two) % q + hit = multiple != 2 * residue + digits[target] = residue + else: + if denominator == 1: + value = digits[target] + numerator * digits[source] + residue = value % q + hit = value != residue + else: + multiple = 2 * digits[target] + numerator * digits[source] + residue = (multiple * inverse_two) % q + hit = multiple != 2 * residue + digits[target] = residue + nonzero += hit + counts[nonzero] += 1 + need(sum(counts) == total, "census missed a row at q=%s" % q) + return counts + + +def named_row(q): + return (q - 2, q - 2, q - 5, q - 5, 0, q - 1, 0, 0) + + +def returned_row(q): + return (0, q - 1, q - 2, 0, q - 1, q - 1, q - 1, 1) + + +def main(): + pinned = load_pins() + selected = json.loads(pinned["certificates/selected-result.json"]) + need(selected["kappa"] == "363005817/100000000000", "selected frontier string") + word_record = json.loads(gzip.decompress(pinned["research/bit-completed-backend-api/independent/inputs/WORD.json.gz"])) + need(word_record["start"][462] == 0 and word_record["final"][462] == 506, "helper 462 endpoints") + matrix = matcher_from_frame(pinned["research/bit-completed-backend-api/independent/inputs/frames.json"]) + published = json.loads(pinned["research/bit-completed-backend-api/science/RESULT.json"]) + need([[F(entry) for entry in row] for row in published["matcher"]] == matrix, "published matcher") + need(published["right_route_elimination_counts"] == {"swap": 5, "scale": 5, "add": 14}, "published counts") + factors = decompose(matrix) + published_factors = [[[F(entry) for entry in row] for row in factor] for factor in published["right_route_factors"]] + need(factors == published_factors, "elimination differs from the published factors") + word = inverse_word(factors) + n = 8 + product = eye(n) + for factor in reversed(factors): + kind = classify(factor) + inverse = eye(n) + if kind[0] == "swap": + inverse[kind[1]], inverse[kind[2]] = inverse[kind[2]], inverse[kind[1]] + elif kind[0] == "scale": + inverse[kind[1]][kind[1]] = 1 / kind[3] + else: + inverse[kind[2]][kind[1]] = -kind[3] + product = mm(product, inverse) + inverse_matrix = mm(matrix, product) + need(inverse_matrix == eye(n), "inverse word is not S^{-1}") + scales = [op for op in word if op[0] == "scale"] + shears = [op for op in word if op[0] == "add"] + swaps = [op for op in word if op[0] == "swap"] + need(len(scales) == 5 and len(shears) == 14 and len(swaps) == 5, "inverse word shape") + need(len(scales) + len(shears) == 19 < 48, "site bound") + + # The range prover rejects the q = 5 boundary and accepts the tail. + need(not prove_range(F(-6), F(1), 5), "q-6 must leave range at q=5") + need(prove_range(F(-6), F(1), 7), "q-6 must stay in range for odd q>=7") + + low, high, carries = affine_tail(word) + need(tuple(carries) == TAIL_CARRIES, "tail carry digits") + need(sum(carry != 0 for carry in carries) == 13, "tail nonzero count") + need(tuple(high) == CLOSED, "tail high part is not the closed-form correction") + for index, (constant, slope) in enumerate(low): + need((constant, slope) == ((F(0), F(0)), (F(-1), F(1)), (F(-2), F(1)), (F(0), F(0)), (F(-1), F(1)), (F(-1), F(1)), (F(-1), F(1)), (F(1), F(0)))[index], "tail final low digit") + + for q in (5, 7, 9, 11, 15, 21, 401): + row, carried_high, carried = direct(word, named_row(q), q) + need(tuple(row) == returned_row(q), "direct return low digits at q=%s" % q) + need(tuple(carried_high) == CLOSED, "direct return high digits at q=%s" % q) + expected = FIVE_CARRIES if q == 5 else TAIL_CARRIES + need(tuple(carried) == expected, "direct carry digits at q=%s" % q) + omitted = direct_without_carry(word, named_row(q), q) + need(tuple(omitted) != CLOSED, "dropping the intermediate carries still matched at q=%s" % q) + zero_row, _zero_high, zero_carries = direct(word, (0,) * 8, q) + need(zero_row == [0] * 8 and all(carry == 0 for carry in zero_carries), "zero row emitted a carry") + + changed = [index for index, (left, right) in enumerate(zip(FIVE_CARRIES, TAIL_CARRIES)) if left != right] + need(changed == [9, 10], "q=5 and the tail differ in more than the q-6 step and the next shear") + need(sum(carry != 0 for carry in FIVE_CARRIES) == 13, "q=5 nonzero count") + + coefficients = {op[3] for op in word if op[0] != "swap"} + need(coefficients <= {F(1), F(-1), F(1, 2), F(-1, 2)}, "unexpected coefficient") + for q in (3, 5, 7): + for kind, target, source, coefficient in word: + if kind == "swap": + continue + for left in range(q): + rights = range(q) if kind == "add" else (0,) + for right in rights: + need( + integer_nonzero(kind, left, right, coefficient, q) + == fraction_nonzero(kind, left, right, coefficient, q), + "integer carry test diverges from the quotient", + ) + + for q, record in CENSUS.items(): + counts = census(word, q) + need(tuple(counts) == record["hist"], "census histogram at q=%s" % q) + need(sum(counts) == q ** 8, "census domain at q=%s" % q) + need(max(index for index, count in enumerate(counts) if count) == record["max"], "census maximum") + _row, _high, witness_carries = direct(word, record["witness"], q) + need(sum(carry != 0 for carry in witness_carries) == record["max"], "witness count at q=%s" % q) + need(record["max"] < 48, "census row reached 48") + + print("PASS_FRAME506_INVERSE_ROW_CARRIES nonzero=13 sites=19 census_max=18,18,19") + + +if __name__ == "__main__": + try: + main() + except SystemExit as exc: + if exc.code not in (0, None): + print(exc, file=sys.stderr) + raise