From a51fb99e3cf11c32d7318bd12c35f6d08e07927e Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Wed, 11 Nov 2026 13:32:03 +0000 Subject: [PATCH] Prove the sharp n-axis monomial elimination record count. The column charge tightens the separate-maxima ceiling used at n=9 and the square ceiling in the #7000 application review, without a kappa change. Co-authored-by: unpaidmoon --- research/n-axis-monomial-records/PROOF.md | 204 +++++++++++++++ research/n-axis-monomial-records/README.md | 139 +++++++++++ research/n-axis-monomial-records/SOURCES.json | 30 +++ research/n-axis-monomial-records/TASK.json | 101 ++++++++ research/n-axis-monomial-records/VERIFY.json | 32 +++ research/n-axis-monomial-records/verify.py | 236 ++++++++++++++++++ 6 files changed, 742 insertions(+) create mode 100644 research/n-axis-monomial-records/PROOF.md create mode 100644 research/n-axis-monomial-records/README.md create mode 100644 research/n-axis-monomial-records/SOURCES.json create mode 100644 research/n-axis-monomial-records/TASK.json create mode 100644 research/n-axis-monomial-records/VERIFY.json create mode 100644 research/n-axis-monomial-records/verify.py diff --git a/research/n-axis-monomial-records/PROOF.md b/research/n-axis-monomial-records/PROOF.md new file mode 100644 index 0000000000..0621ca291d --- /dev/null +++ b/research/n-axis-monomial-records/PROOF.md @@ -0,0 +1,204 @@ +# Record count of one n-axis monomial elimination + +This is a proof about one synthesis. It is not a lower bound on every +recipe in the selected primitive alphabet, and it does not change κ. + +## Normal form + +Use the nine-axis shape from `research/final4610-independent-admission/SPECIALIZATION.md`, +with the axis count left free. An n-axis monomial is an invertible matrix +`A` over `F_2`, a translation `b` in `F_2^n`, a global phase `a` modulo 4, +linear coefficients `alpha_i` modulo 4, and off-diagonal bits `Q_ij` for +`i < j`. The diagonal of `Q` is carried by `alpha_i mod 2` and is not a +separate controlled-sign record. On a basis address the monomial applies +the quadratic phase and then the affine map `x -> A x + b`. + +The selected-bit primitives used here are one row addition, one translation +of a single bit, one unit phase on a single bit, one controlled sign on a +pair of bits, and one global factor of `i`. A row swap is three row +additions: over `F_2`, + +```text +u <- u+v, v <- v+u, u <- u+v +``` + +sends `(u, v)` to `(v, u)`. Two additions do not. + +## Elimination + +Start from `M = A`. For `k = 0, ..., n-1`: + +1. Let `r` be the least index at least `k` with `M_{r k} = 1`. +2. If `r != k`, swap rows `r` and `k`. +3. For every `i != k` with `M_{i k} = 1`, add row `k` into row `i`. + +**Block form.** At the start of column `k` the matrix is + +```text +[ I_k B ] +[ 0 C ] +``` + +with `C` of size `n-k`. Swaps are among rows `k, ..., n-1`, and those rows +have zeros in columns `0, ..., k-1`, so a swap does not change the finished +columns. Row `k`, once it holds the pivot, also has zeros in columns +`0, ..., k-1`, because that row was taken from the bottom block. Adding it +to other rows therefore does not change finished columns. Clearing column +`k` makes that column equal to `e_k`. By induction the algorithm ends at +`I_n` whenever every pivot exists. + +**Pivot existence.** The elementary steps are invertible, so `A` is +invertible if and only if the current matrix is. In the block form that is +equivalent to `C` being invertible. The first column of an invertible `C` +is nonzero, so a pivot row `r >= k` exists. At `k = n-1` the only eligible +row is `n-1`, so the last column never swaps. Thus the number of swaps is +at most `n-1`. + +**Column charge.** Fix column `k`. Let `s_k` be 1 if a swap occurs and 0 +otherwise, and let `a_k` be the number of additions. There are `n-1` rows +other than the pivot. + +- If `s_k = 0`, at most those `n-1` rows are cleared, so `a_k <= n-1`. +- If `s_k = 1`, then `M_{k k} = 0` before the swap. After the swap that + zero lies in the row that was exchanged. That row is not cleared, so + `a_k <= n-2`. + +In both cases `a_k + s_k <= n-1`. Summing over columns, + +```text +sum a_k + sum s_k <= n(n-1), sum s_k <= n-1. +``` + +The address recipe replaces each swap by three additions, so its length is + +```text +sum a_k + 3 sum s_k + = sum (a_k + s_k) + 2 sum s_k + <= n(n-1) + 2(n-1) + = (n+2)(n-1). +``` + +The separate ceilings `sum a_k <= n(n-1)` and `sum s_k <= n-1` are true, +but adding them charges `3(n-1)` for the swaps on top of `n(n-1)` +additions and produces the longer count `(n+3)(n-1)`. The column charge +removes `n-1` from that count. For `n > 1` the two separate ceilings are +not achieved by one matrix: a swapped column has at least one uncleared +row. The exhaustive check for `n <= 4` records that fact. The inequality +above does not need it. + +## Phase and translation + +These records do not depend on `A`. + +- `b` has at most `n` ones, one translation each. +- Each `alpha_i` lies in `{0,1,2,3}`, so at most `3n` unit phase records. +- At most one controlled sign for each of the `n(n-1)/2` pairs. +- The global phase `a` needs at most three factors of `i`. + +Adding these ceilings to the address bound gives + +```text +R(n) = (n+2)(n-1) + 4n + 3 + n(n-1)/2 = (3n^2 + 9n + 2)/2. +``` + +The numerator is even because `n(n+3)` is even, so `3n(n+3) + 2` is even. +The same count is an integer recipe length for every positive integer `n`. + +## The bound is achieved by this synthesis + +For `n = 1` the matrix `(1)`, the translation `1`, `alpha_0 = 3` and global +phase `3` emit `0 + 1 + 3 + 0 + 3 = 7 = R(1)` records. + +For `n >= 2` define `A` by + +```text +row 0 = e_{n-1}, row i = e_0 + e_i for i = 1, ..., n-1. +``` + +At the start of column `k`, for `0 <= k <= n-1`, + +- row `i` equals `e_i + e_k` for every `i < k`, +- row `k` equals `e_{n-1}`, +- row `i` equals `e_k + e_i` for every `i > k`. + +This holds at `k = 0`. If `k < n-1`, row `k` has a zero in column `k` and +row `k+1` has a one there, so the pivot is row `k+1`. After that swap, +clearing column `k` adds the pivot row to the `k` rows above it and to the +`n-k-2` rows below `k+1`, which is `n-2` additions, and produces the same +description at column `k+1`. At column `n-1` there is no swap, and each of +the `n-1` earlier rows has a one in the last column. + +Thus the algorithm swaps on exactly the first `n-1` columns, performs +`(n-1)(n-2)` additions there and `n-1` additions on the last column, and +the address length is + +```text +(n-1)^2 + 3(n-1) = (n+2)(n-1). +``` + +Choose every bit of `b` equal to 1, every `alpha_i` equal to 3, every +`Q_ij` equal to 1, and global phase 3. Then `alpha_i` is odd, so the +stored diagonal bit is 1, and no extra controlled sign is emitted for it. +This one monomial makes the synthesis emit exactly `R(n)` records. + +Reaching `I_n` also shows that this `A` is invertible. The census for +`n <= 4` finds exactly one maximizer in each `GL(n, F_2)`, and it is this +matrix. + +## Comparison with the published sufficient counts + +The `#4610` specialization charges at most `n(n-1)` additions and at most +`n-1` swaps separately. That address length is `(n+3)(n-1)`, and the full +record ceiling is + +```text +L(n) = (3n^2 + 11n)/2 = R(n) + (n-1). +``` + +At `n = 9` this is `96 + 9 + 27 + 36 + 3 = 171`, matching the published +line. The sharper count is `R(9) = 163`. Both are sufficient. The value +171 is not false; it does not use the column charge. + +The operation list in section 6 of the `#7000` application review is +`n(n-1)+3n` row additions, `n` affine flips, `3n` unit phases, +`n(n-1)/2` controlled signs and three global phases. Its sum is + +```text +S(n) = L(n) + 3 = R(n) + n + 2, +``` + +because `n(n-1)+3n` charges `n` swaps rather than `n-1`. At `n = 9` the +sum is 174. The review then uses the still larger per-map ceiling +`4(n+1)^2`. The gap is an integer: + +```text +4(n+1)^2 - R(n) = (5n^2 + 7n + 6)/2. +``` + +It is positive for every positive integer `n`. At `n = 153`, + +```text +R(153) = 35803, 4(154)^2 = 94864. +``` + +The review multiplies the square ceiling by its stated map count +`311304` and obtains `29531542656`, which is below `2^35` and therefore +below the stated `2^40`. The same map count times `R(153)` is +`11145617112`, which is below `2^34`. These are comparisons of the +integers already fixed by the formulas. They do not rederive the map +count 311304, and they do not change the admitted κ +`363005817/100000000000`. + +## What is not claimed + +The algorithm accepts exactly the invertible matrices: every successful run +ends at `I_n` by invertible steps, and every invertible matrix has a pivot +at each column. The exhaustive check for `n <= 4` matches `|GL(n, F_2)|`. +That census is not the proof for larger `n`. + +`R(n)` is the exact length of this synthesis on one monomial. Another +factorization into the same primitives might be shorter. No such search is +claimed to be exhaustive. Assumption `precision_tape` is not discharged: +the proof bounds the record list that the retained tape tariff multiplies. +It does not prove the movement exponent, the storage prescription, or the +outer threshold calculation. diff --git a/research/n-axis-monomial-records/README.md b/research/n-axis-monomial-records/README.md new file mode 100644 index 0000000000..6f193f6e09 --- /dev/null +++ b/research/n-axis-monomial-records/README.md @@ -0,0 +1,139 @@ +# An n-axis monomial elimination uses at most (3n^2+9n+2)/2 records + +**Proof, with an exhaustive census for n <= 4. No new κ.** The selected +conditional value stays `363005817/100000000000`. + +## Result + +Fix the monomial normal form used for nine axes in the `#4610` +specialization, and let the axis count be any positive integer `n`. +Eliminate the invertible binary address matrix by the pivot rule below, +replace each row swap by three `F_2` row additions, and emit one record +for each translation bit, each unit of a mod-4 linear phase, each +off-diagonal controlled sign, and each global factor of `i`. + +**Theorem.** This synthesis emits at most + +```text +R(n) = (3n^2 + 9n + 2)/2 +``` + +elementary records, and there is a monomial for which it emits exactly +`R(n)`. The argument is in [PROOF.md](PROOF.md). + +The column charge is the new step. On column `k`, if `a_k` is the number +of eliminations and `s_k` is 1 when a swap occurs, then `a_k + s_k <= n-1`. +Summing and replacing each swap by three additions gives the address +length `(n+2)(n-1)`. Charging at most `n(n-1)` additions and `n-1` swaps +separately gives the longer address length `(n+3)(n-1)`. + +At `n = 9` the separate-maxima count is the published + +```text +96 + 9 + 27 + 36 + 3 = 171, +``` + +while `R(9) = 163`. The value 171 remains a correct sufficient count. It +does not use the column charge. The operation list in section 6 of the +`#7000` application review sums to `R(n) + n + 2`, which is 174 at +`n = 9`, and the review then uses `4(n+1)^2`. At `n = 153` that square is +`94864` and `R(153) = 35803`. With the review's own map count `311304`, +the square product `29531542656` is below `2^35`, and the sharp product +`11145617112` is below `2^34`. The review's comparison `< 2^40` remains +true. None of these integers changes the admitted κ. + +Assumption `precision_tape` is the interface being bounded: the record +list is the fixed finite template that the retained tape tariff multiplies. +The assumption is not discharged. The caller is this elimination, which is +the grammar specialized at `n = 9` and invoked for general `n` by that +application review. `frontier7000-verify` was not run. + +## Evidence classes + +The column charge, the closed form, the witness family, and the comparison +with 171 and with `4(n+1)^2` are a proof for every positive integer `n`. +The witness check through `n = 64` in the verifier is finite corroboration +of that one family, not the proof. + +Separately, for every matrix in `M_n(F_2)` with `n <= 4`, the algorithm +accepts a matrix if and only if it lies in `GL(n, F_2)`, never swaps the +last column, obeys the column charge, attains `n(n-1)` additions on some +matrix, attains `n-1` swaps on some matrix, and attains the address bound +on exactly one matrix. That statement is an exhaustive finite census. +Its domain is finite, the enumeration runs through every bit mask, and the +acceptance count is checked against the product formula for `|GL(n, F_2)|`. +It is not a proof for `n > 4`. A failed search is not used anywhere in +this package. + +`R(n)` is exact for this synthesis. It is not proved to be a lower bound +on every other recipe built from the same primitives. + +## Scope and evidence + +Catalogue card `formal-interface-lemma`, priority revision 8, base commit +`e54523517d0f03e58352e647c403a5af3e525a57`. Scope status: **changed**. +The card asks for a formalized interface lemma. This package does not +start a proof-assistant development. It answers the all-size request for +one assumption id, one caller, and one proved proposition: the record +count above, under `precision_tape`. + +Ordered eligible list for this session, after dropping every unpaidmoon +pull request and fork `cursor/*` branch named in the session brief. The +revision-8 next-decision table comes first. Catalogue cards that the table +does not name by id follow, in catalogue order. + +1. Complex helpers (`p104-side-correction`, `coverage-law-change`). +2. BIT helper contract (`bit-helper-contract`). +3. New decoders and interfaces. +4. Supplier audit. +5. All-size audit and formalization. +6. Verification tooling. +7. `bit-new-register-model`. +8. `r437-carrier-integration`. +9. `complex-rank-shape-decoder`. +10. `complex-new-helper-inventory`. + +Item 5 is this package. It is not a register-model, paired-star, G20, or +conditional-κ continuation. The original card is copied in +[TASK.json](TASK.json). Pins are in [SOURCES.json](SOURCES.json). + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 -B research/n-axis-monomial-records/verify.py +python3 -O -B research/n-axis-monomial-records/verify.py +python3 -B scripts/research_package.py --package research/n-axis-monomial-records --check-only +python3 -B scripts/research_package.py --package research/n-axis-monomial-records +``` + +The verifier prints `PASS_N_AXIS_MONOMIAL_RECORDS`. Checks raise +`SystemExit`, so optimized mode does not drop them. Not run: Lean, Docker, +a physical caller, and `make frontier7000-verify`. +`scripts/research_selected_baseline.py` returned +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` and is not a scientific replay. + +## Open next questions + +- Is `R(n)` a lower bound on every selected-primitive recipe of some + monomial, or only the exact length of this elimination? The tariff uses + a sufficient count. A matching lower bound would show that this alphabet + cannot price that monomial more cheaply. The first step is the `n = 2` + witness, whose sharp recipe has 16 records. The selected rewrite system + is not a finite search here. +- Does replacing the review's per-map `94864` by `R(153) = 35803` lower a + cutoff integer in section 6 without changing the admitted κ? The review + already says those finite constants leave the rank and exponent + inequalities unchanged. No isolated cutoff checker is included, and the + full admission replay was not run. + +## Credit + +The nine-axis normal form and the count 171 are Cao Yifan / intqwq, +PR `#4610`, as recorded in +`research/final4610-independent-admission/SPECIALIZATION.md`. The loose +general list and the map count `311304` are the `#7000` application +review, section 6. The package scaffold is Douglas Colkitt's. Prepared by +unpaidmoon with substantial Cursor Grok assistance. New work is +Apache-2.0. No independent human or formal-kernel review is claimed. diff --git a/research/n-axis-monomial-records/SOURCES.json b/research/n-axis-monomial-records/SOURCES.json new file mode 100644 index 0000000000..f4ab6efa5b --- /dev/null +++ b/research/n-axis-monomial-records/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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": "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md", + "usage": "input", + "git_blob": "3dd1af2285e597676725e85ad4f65e7ad326d695", + "sha256": "4501502c2ceb9759b20372435fe4beb51082c5a5e2910c1fd5dbe6edca415055" + }, + { + "path": "research/final4610-independent-admission/SPECIALIZATION.md", + "usage": "input", + "git_blob": "7ee84b30892f7354e1c36611f1a5e9b082dc6147", + "sha256": "70430114f744108223bc1d44b98bc25b696c4b408b7b044c2a8bbdfdb434ac5c" + } + ] +} diff --git a/research/n-axis-monomial-records/TASK.json b/research/n-axis-monomial-records/TASK.json new file mode 100644 index 0000000000..afa998e854 --- /dev/null +++ b/research/n-axis-monomial-records/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Assumption precision_tape, one caller: the selected-bit monomial elimination. For every n and every n-axis monomial in the #4610 normal form, that elimination emits at most (3n^2+9n+2)/2 elementary records, and some monomial emits exactly that many. No kappa change and no discharge of the assumption.", + "scope_change_reason": "The catalogue card asks for a formalized interface lemma with a proof-assistant binding. This package keeps the assumption and the caller fixed and gives a written record-count proof instead of a Lean development. The five selected assumptions stay open. The n=9 count 171 is the predecessor upper bound being tightened, not a result being copied.", + "bottleneck_link": "Side result on the finite-record constant inside the selected conditional assembly. The admitted kappa multiplies a paid profile whose tape tariff uses this record count only through fixed thresholds. A smaller sufficient count does not by itself raise kappa. It is the constant the #7000 application review left at 4(n+1)^2.", + "budget_minutes": 60, + "stop_rule": "Stop when the column charge, the closed form, the witness family, and the n<=4 exhaustive comparison with GL(n,F2) are checked. Do not rerun frontier admission or treat a shorter unknown synthesis as impossible.", + "outcome": "completed", + "evidence": "Proof of the column charge and of a sharp witness family, plus an exhaustive census for n<=4 that the algorithm accepts exactly the invertible matrices and obeys the charge. Arithmetic identifies the #4610 count 171 and the #7000 count 4(n+1)^2 as strictly looser sufficient bounds for n>1. No search failure is used as nonexistence.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance: the column-charge argument, the witness family, the verifier, and the packaging. No SAT solver was called.", + "open_questions": [ + { + "question": "Is (3n^2+9n+2)/2 a lower bound on every selected-primitive recipe for some n-axis monomial, or only on this elimination?", + "why_it_matters": "The tariff needs a sufficient count. A matching lower bound would show that this alphabet cannot price that monomial more cheaply.", + "first_step": "For n=2, list every selected-bit recipe shorter than 16 records and test it on the sharp witness.", + "blocked_by": "The selected primitive rewrite system is not formalized as a finite search in this package. This note bounds one synthesis." + }, + { + "question": "Does substituting R(153)=35803 for the review's per-map 94864 lower any cutoff integer in section 6 of the #7000 application review without changing the admitted kappa?", + "why_it_matters": "That review lists tightening the loose scalar and route constants as open work. The rank and exponent inequalities are stated to be unchanged by those constants.", + "first_step": "Compare the two C_move coefficients against the written threshold inequalities only.", + "blocked_by": "No isolated cutoff checker is in this package. frontier7000-verify was not run, and a full replay would be a different claim." + } + ] +} diff --git a/research/n-axis-monomial-records/VERIFY.json b/research/n-axis-monomial-records/VERIFY.json new file mode 100644 index 0000000000..2d2f677729 --- /dev/null +++ b/research/n-axis-monomial-records/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md", + "research/final4610-independent-admission/SPECIALIZATION.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Closed form, witness family through n=64, exhaustive GL(n,F2) census for n<=4, three-XOR swap control, and the pinned 171 and 4(n+1)^2 comparisons." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks with assert statements removed by the optimizer, so every check must raise SystemExit on its own." + } + ] +} diff --git a/research/n-axis-monomial-records/verify.py b/research/n-axis-monomial-records/verify.py new file mode 100644 index 0000000000..42380d15e2 --- /dev/null +++ b/research/n-axis-monomial-records/verify.py @@ -0,0 +1,236 @@ +#!/usr/bin/env python3 +"""Check the n-axis monomial record bound. Standard library only.""" + +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +MAPS = 311304 + + +def fail(message): + raise SystemExit(message) + + +def require(condition, message): + if not condition: + fail(message) + + +def record_bound(n): + """R(n) = (3n^2 + 9n + 2) / 2.""" + numerator = 3 * n * n + 9 * n + 2 + require(numerator % 2 == 0, "record numerator is odd at n=%s" % n) + return numerator // 2 + + +def loose_specialization_bound(n): + """#4610 accounting: n(n-1) additions and n-1 swaps, charged separately.""" + address = n * (n - 1) + 3 * (n - 1) + return address + n + 3 * n + n * (n - 1) // 2 + 3 + + +def review_sum(n): + """Operation list in the #7000 application review, summed.""" + return n * (n - 1) + 3 * n + n + 3 * n + n * (n - 1) // 2 + 3 + + +def loose_square(n): + return 4 * (n + 1) * (n + 1) + + +def witness_matrix(n): + matrix = [[0] * n for _ in range(n)] + if n == 1: + matrix[0][0] = 1 + return matrix + matrix[0][n - 1] = 1 + for i in range(1, n): + matrix[i][0] = 1 + matrix[i][i] = 1 + return matrix + + +def eliminate(matrix): + """Return per-column (swap, additions), or None if a pivot is missing. + + The final matrix must be the identity. A missing pivot or a non-identity + result is rejection, not a successful recipe. + """ + n = len(matrix) + rows = [row[:] for row in matrix] + columns = [] + for k in range(n): + pivot = None + for r in range(k, n): + if rows[r][k] == 1: + pivot = r + break + if pivot is None: + return None + swapped = 0 + if pivot != k: + rows[k], rows[pivot] = rows[pivot], rows[k] + swapped = 1 + additions = 0 + for i in range(n): + if i != k and rows[i][k] == 1: + for j in range(n): + rows[i][j] ^= rows[k][j] + additions += 1 + columns.append((swapped, additions)) + for i in range(n): + for j in range(n): + if rows[i][j] != (1 if i == j else 0): + return None + return columns + + +def address_count(columns): + return sum(additions + 3 * swapped for swapped, additions in columns) + + +def monomial_records(n, columns): + return address_count(columns) + n + 3 * n + n * (n - 1) // 2 + 3 + + +def gl_order(n): + order = 1 + for i in range(n): + order *= (1 << n) - (1 << i) + return order + + +def check_algebra(): + for n in range(1, 65): + address = (n + 2) * (n - 1) + phase = n + 3 * n + n * (n - 1) // 2 + 3 + require(record_bound(n) == address + phase, "closed form disagrees at n=%s" % n) + require( + loose_specialization_bound(n) - record_bound(n) == n - 1, + "gap against the separate-maxima count is not n-1", + ) + require(review_sum(n) - record_bound(n) == n + 2, "review gap is not n+2") + gap_num = 5 * n * n + 7 * n + 6 + require(gap_num % 2 == 0, "square gap is not an integer") + require(loose_square(n) - record_bound(n) == gap_num // 2, "square gap formula") + require(loose_square(n) > record_bound(n), "square bound does not dominate") + require(record_bound(1) == 7, "n=1 record count") + require(record_bound(9) == 163, "n=9 sharp count") + require(loose_specialization_bound(9) == 171, "n=9 specialization count") + require(review_sum(9) == 174, "n=9 review sum") + require(loose_square(9) == 400, "n=9 square") + require(record_bound(153) == 35803, "n=153 sharp per-map count") + require(loose_square(153) == 94864, "n=153 square per-map count") + loose_product = MAPS * loose_square(153) + sharp_product = MAPS * record_bound(153) + require(loose_product == 29531542656, "loose product %s" % loose_product) + require(sharp_product == 11145617112, "sharp product %s" % sharp_product) + require(loose_product < 2**35 < 2**40, "loose product is not below 2^35") + require(sharp_product < 2**34, "sharp product is not below 2^34") + return sharp_product + + +def check_swap_identity(): + """Three XOR additions swap two rows. Two do not.""" + left = [1, 0, 1, 1] + right = [0, 1, 1, 0] + a, b = left[:], right[:] + a = [x ^ y for x, y in zip(a, b)] + b = [x ^ y for x, y in zip(b, a)] + require(a != right or b != left, "two XOR additions already swapped the control rows") + a, b = left[:], right[:] + a = [x ^ y for x, y in zip(a, b)] + b = [x ^ y for x, y in zip(b, a)] + a = [x ^ y for x, y in zip(a, b)] + require(a == right and b == left, "three XOR additions did not swap the control rows") + + +def check_witness_family(): + for n in range(1, 65): + columns = eliminate(witness_matrix(n)) + require(columns is not None, "witness is singular at n=%s" % n) + require(address_count(columns) == (n + 2) * (n - 1), "witness address at n=%s" % n) + require(monomial_records(n, columns) == record_bound(n), "witness records at n=%s" % n) + if n == 1: + require(columns == [(0, 0)], "n=1 column charge") + continue + for k, (swapped, additions) in enumerate(columns): + if k < n - 1: + require(swapped == 1 and additions == n - 2, "early witness column n=%s k=%s" % (n, k)) + else: + require(swapped == 0 and additions == n - 1, "final witness column n=%s" % n) + + +def matrices(n): + size = n * n + for mask in range(1 << size): + yield [[(mask >> (i * n + j)) & 1 for j in range(n)] for i in range(n)] + + +def check_exhaustive_census(): + """Every matrix of size n<=4. Acceptance count equals |GL(n,F2)|.""" + expected_maximizers = {1: 1, 2: 1, 3: 1, 4: 1} + for n in range(1, 5): + accepted = 0 + maximizers = 0 + joint = 0 + max_adds = -1 + max_swaps = -1 + target = (n + 2) * (n - 1) + for matrix in matrices(n): + columns = eliminate(matrix) + if columns is None: + continue + accepted += 1 + additions = sum(item[1] for item in columns) + swaps = sum(item[0] for item in columns) + max_adds = max(max_adds, additions) + max_swaps = max(max_swaps, swaps) + for k, (swapped, added) in enumerate(columns): + require(added + swapped <= n - 1, "column charge failed") + if k == n - 1: + require(swapped == 0, "last column swapped") + if address_count(columns) == target: + maximizers += 1 + if additions == n * (n - 1) and swaps == n - 1: + joint += 1 + require(accepted == gl_order(n), "accepted %s invertible matrices at n=%s, |GL|=%s" % (accepted, n, gl_order(n))) + require(max_adds == n * (n - 1), "addition maximum is short at n=%s" % n) + require(max_swaps == n - 1, "swap maximum is short at n=%s" % n) + require(maximizers == expected_maximizers[n], "maximizer count %s at n=%s" % (maximizers, n)) + require(joint == (1 if n == 1 else 0), "joint separate-maxima count %s at n=%s" % (joint, n)) + zero = eliminate([[0, 0], [0, 0]]) + require(zero is None, "the zero matrix was accepted") + identity = eliminate([[1, 0], [0, 1]]) + require(identity == [(0, 0), (0, 0)], "identity elimination") + + +def check_sources(): + selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")) + require(selected["kappa"] == "363005817/100000000000", "selected kappa changed") + require(selected["previous_kappa"] == "781451/250000000", "previous kappa pin") + review = (ROOT / "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md").read_text(encoding="utf-8") + for phrase in ("n(n-1)+3n", "4(n+1)^2", "311,304", "29,531,542,656", "precision_tape"): + require(phrase in review, "application review is missing %r" % phrase) + specialization = (ROOT / "research/final4610-independent-admission/SPECIALIZATION.md").read_text(encoding="utf-8") + require("96+9+27+36+3 = 171" in specialization, "n=9 specialization count is missing") + + +def main(): + check_swap_identity() + check_algebra() + check_witness_family() + check_exhaustive_census() + check_sources() + print( + "PASS_N_AXIS_MONOMIAL_RECORDS" + " R9=163 specialization9=171 review9=174 square9=400" + " R153=35803 square153=94864" + " sharp_product=11145617112 loose_product=29531542656" + " census=GL(n,2) for n<=4 no_new_kappa" + ) + + +if __name__ == "__main__": + main()