diff --git a/research/first-failure-one-sided-copy/README.md b/research/first-failure-one-sided-copy/README.md new file mode 100644 index 0000000000..fc2caa8ad7 --- /dev/null +++ b/research/first-failure-one-sided-copy/README.md @@ -0,0 +1,197 @@ +# A fixed-frame COPY saving at the one-sided first-failure boundary + +Two finite exact constructions on the 93-line unit of +[ToikY's PR1609](https://github.com/CrocSwap/integer-mult-bounds/pull/1609): + +| Construction | Separate-term binary pairing ranks | Total | +|---|---|---:| +| All-pairs identity in the exhibited non-coordinate frame | 9,9,9,9,9,9,9,9 | 72 | +| One-sided mask-only completion in that same frame | 8,9,9,9,9,9,9,9 | 71 | +| Another all-pairs identity on the same live lines | 7,8,7,8,8,8,8,9 | 63 | + +The new step is an explicit non-coordinate frame in which one-sided masked +freedom saves one COPY unit. The COPY63 construction shows why this does not +establish a saving against an appropriate all-pairs comparator. Neither +construction is asserted optimal. This is a finite certificate and a written +linear-algebra derivation, with no new kappa or physical supplier. + +## Model and fixed input + +Use doubled E8 roots `q`, of squared norm eight, with first nonzero coordinate +positive. Their lexicographically sorted list has 120 lines. Write `r=q/2` +and `G_ij = r_i dot r_j`. The required mask consists of equal or orthogonal +root lines. The binary pairing table is + +```text +N_ij = 1 if G_ij is even, and 0 otherwise. +``` + +A term with actual top support `S` and bottom support `T` costs +`rank_F2 N[S,T]`. We sum the ranks of all eight terms separately. + +The fixed predecessor instance has + +```text +q_t = (2,2,0,0,0,0,0,0), n = (1,-1,2,0,0,0,0,0). +``` + +Delete exactly the orthogonal lines `q_i` with `q_i dot n != 0`. There are +27 deleted and 93 live lines. The target neighbourhood consists of the +target and 36 live orthogonal lines, all annihilated by `n`. PR1609 supplies +this instance and its first-failure interpretation. Its sharp threshold +and flat census are cited, not re-proved here. The verifier binds the +predecessor certificate hash and checks the exact deleted-index list. + +## The non-coordinate construction + +Let the bottom directions be the rows + +```text +w_0 = 13 q_t + 7 n = (33,19,14,0,0,0,0,0), +w_1 = e_1, ..., w_7 = e_7. +``` + +Let `u_0,...,u_7` be their dual basis, so `u_k dot w_l = delta_kl`. +Explicitly, `u_0=e_0/33`, `u_1=e_1-19e_0/33`, +`u_2=e_2-14e_0/33`, and `u_k=e_k` for `k>=3`. +For a scalar `c`, put `s_j=q_j` except `s_t=q_t+c n`, and set + +```text +D_ik = q_i dot u_k, T_jk = (s_j dot w_k)/2. +``` + +Biorthogonality gives the identity + +```text +(D T^T - 2G)_ij = 0 if j != t, +(D T^T - 2G)_it = (c/2) (q_i dot n). +``` + +Thus every `c` preserves all masked entries. The top factor is root-linear. +At `c=0` the product equals `2G` on every pair. Choose + +```text +c = -(w_0 dot q_t)/(w_0 dot n) = -104/42 = -52/21. +``` + +This removes the target from the first bottom support. That support was +exactly the 56 lines odd to the target together with the target itself; +it becomes those 56 lines. The verifier enumerates these sets and checks +that their full pairing-row spans have ranks nine and eight, respectively. +The first top support spans the full rank-nine pairing-row space. +Direct elimination of the actual rectangular pairing submatrices gives +first-term rank nine before the change and eight after it. Every other +term has rank nine in both cases. + +The verifier checks all 8,649 entries of each product. At `c=-52/21`, +exactly 56 entries differ from `2G`, all unmasked and in the target column. +This proves the finite COPY72 to COPY71 comparison in this frame. +For every positive power `p`, the same comparison is strict: +`8^p + 7*9^p < 8*9^p`. + +## The all-pairs comparator + +Choose these eight independent top directions, all doubled root vectors: + +```text +(0,0,2,0,0,0,0,2) +(0,0,2,0,0,0,-2,0) +(1,-1,1,-1,-1,-1,-1,-1) +(1,-1,1,-1,1,-1,-1,1) +(1,-1,1,1,1,1,-1,1) +(1,-1,1,-1,1,1,-1,-1) +(1,-1,1,-1,-1,1,-1,1) +(1,1,1,1,-1,1,-1,1) +``` + +Use their duals as bottom directions and set every `s_j=q_j`. The same +biorthogonality identity gives `D T^T=2G` on every pair. The computed +ranks are `7,8,7,8,8,8,8,9`, summing to 63. Seven top directions are +among the deleted lines; factor directions need not themselves be live +ports. The full rational duals are generated in [RESULT.json](RESULT.json). + +After sorting, this comparator's ranks are coordinatewise no larger than +those of the COPY71 mask-only construction, with seven strict inequalities. +It therefore has a smaller COPY power sum for every positive power `p`. +This compares the two exhibited profiles and supplies no optimum or lower +bound for either decoder class. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/first-failure-one-sided-copy +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/first-failure-one-sided-copy/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/first-failure-one-sided-copy/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/first-failure-one-sided-copy --check-source-history +``` + +Another CPython 3.12 installation can replace the interpreter path. +Both registered commands have 120-second limits and print +`PASS_FIRST_FAILURE_ONE_SIDED_COPY one_sided=71 same_frame=72 all_pairs=63 no_new_kappa`. +Default replay writes no files. To generate a fresh receipt, pass +`--write /absolute/path/to/new-result.json`; existing destinations are rejected. +The receipt binds the verifier and predecessor certificate SHA256 hashes. + +Each actual support pairing rank is cross-checked by bitset elimination and +separate dense F2 elimination. Rejection controls plant a masked coefficient +error, expose a nonzero masked error upon each of the 27 possible one-line +restorations, and test a frame whose first pairing rank is eight. +No predecessor executable is imported or run. + +The verifier has no recursion, subprocesses or network calls. Functions fit +within 60 physical lines. Loops are bounded by 120 lines, eight dimensions, +eight terms, 27 restorations or the fixed root generator's 256 sign patterns. +Binary elimination has an explicit 120-step inner bound. Checks remain active +under Python optimization; both registered runs treat warnings as errors. + +Power of Ten rule 3 deviation: CPython allocates managed objects during exact +arithmetic. Live matrices have at most 120 rows and 120 columns; rational +frames are 8 by 8, and residual maps have at most 93 squared entries. The +fixed input certificate is capped at 1 MiB. A fixed-allocation rewrite would +require another runtime. Reassess these bounds before parameterizing the +geometry. No additional static analyzer or repository-wide configuration +change is introduced. + +## Scope, overlap and remaining obligations + +The result covers this fixed unit, the displayed frames and separate-term +binary pairing-rank charges. Gathering, native endpoints, arbitrary-dirty +restoration, frame changes, hosting, precision/tape, all-size/compiler +realization and analytic transfer remain unpriced and unproved here. +No selected cold replay, Lean or Docker run was performed. Independent human +and formal proof-kernel review are unclaimed. + +The original [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19530146) +planned a coordinate census as well. That census is omitted from this delivery +because the [earlier coordinate-perturbation claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19530120) +covers it. This package claims only the explicit non-coordinate construction +and displayed comparator, and does not claim the best root-frame comparator. +The P112 results of merged #2816 concern another live set and their stated +one-sided classes. Merged #5232 concerns fixed A7+A1 normals and another +puncture. Neither supplies the finite constructions given here. +[TASK.json](TASK.json) records the changed scope and overlap coverage; +[SOURCES.json](SOURCES.json) binds historical provenance and the live input. + +## Open next questions + +Can an eight-term one-sided mask-only completion on this fixed unit beat the +exhibited all-pairs profile `7,7,7,8,8,8,8,9`? A first step is to parameterize +root-linear top frames and the one-dimensional target-row freedom, then +compare actual support pairing ranks. This matters because a fixed-frame +saving does not settle the comparison over frames. No global optimization +or lower bound is supplied; physical realization would remain an additional +obligation. The structured question is in TASK.json. + +## Credit + +This contribution was produced by Nick Petalas. New work is Apache-2.0. +ToikY's #1609 supplies the 27-deletion boundary, exact instance and open COPY +question. Philipp / mightyOil's #1191 supplies the one-sided local-spanning +mechanism. DreamingOfClouds's #717 and #2338 supply the separate-term COPY +model and accounting context. Joaqcoo's #1224 and Adam Gall's #2062 develop +the row-shift normal form; Nick Petalas's #5232 applies row shifts to the +different A7+A1 puncture. The E7 geometry retains the predecessor credit of +DreamingOfClouds #595 and DaysSky #897. The displayed frame, its COPY71 +completion and the explicit COPY63 comparison are the contribution here. diff --git a/research/first-failure-one-sided-copy/RESULT.json b/research/first-failure-one-sided-copy/RESULT.json new file mode 100644 index 0000000000..df8e0f36e7 --- /dev/null +++ b/research/first-failure-one-sided-copy/RESULT.json @@ -0,0 +1,410 @@ +{ + "all_pairs": { + "bottoms": [ + [ + "0", + "0", + "1/2", + "0", + "0", + "0", + "1/2", + "0" + ], + [ + "-1/2", + "0", + "0", + "0", + "0", + "0", + "-1/2", + "0" + ], + [ + "1/4", + "-1/4", + "1/4", + "1/4", + "-1/4", + "-1/4", + "1/4", + "-1/4" + ], + [ + "1/4", + "1/4", + "-1/4", + "-1/4", + "1/4", + "-1/4", + "-1/4", + "1/4" + ], + [ + "0", + "-1/2", + "0", + "1/2", + "0", + "0", + "0", + "0" + ], + [ + "1/4", + "1/4", + "1/4", + "-1/4", + "1/4", + "1/4", + "1/4", + "-1/4" + ], + [ + "-1/4", + "-1/4", + "-1/4", + "-1/4", + "-1/4", + "1/4", + "-1/4", + "1/4" + ], + [ + "1/2", + "1/2", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ], + "copy_ranks": [ + 7, + 8, + 7, + 8, + 8, + 8, + 8, + 9 + ], + "masked_errors": 0, + "tops": [ + [ + "0", + "0", + "2", + "0", + "0", + "0", + "0", + "2" + ], + [ + "0", + "0", + "2", + "0", + "0", + "0", + "-2", + "0" + ], + [ + "1", + "-1", + "1", + "-1", + "-1", + "-1", + "-1", + "-1" + ], + [ + "1", + "-1", + "1", + "-1", + "1", + "-1", + "-1", + "1" + ], + [ + "1", + "-1", + "1", + "1", + "1", + "1", + "-1", + "1" + ], + [ + "1", + "-1", + "1", + "-1", + "1", + "1", + "-1", + "-1" + ], + [ + "1", + "-1", + "1", + "-1", + "-1", + "1", + "-1", + "1" + ], + [ + "1", + "1", + "1", + "1", + "-1", + "1", + "-1", + "1" + ] + ], + "unmasked_errors": 0 + }, + "claim_type": "finite exact constructions", + "deleted_indices": [ + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 106 + ], + "live_ports": 93, + "no_new_kappa": true, + "one_sided": { + "bottoms": [ + [ + "33", + "19", + "14", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ] + ], + "copy_ranks": [ + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "first_bottom_support_sizes": [ + 57, + 56 + ], + "masked_errors": 0, + "same_frame_all_pairs_ranks": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "target_scale": "-52/21", + "tops": [ + [ + "1/33", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "-19/33", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "-14/33", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ] + ], + "unmasked_errors": 56 + }, + "restoration_controls": 27, + "schema_version": 1, + "source_sha256": "3fd9189d8d8c2d97ff0224544c1415a0a4b700062fe0eafbf2571a448e1a7cf0", + "status": "PASS_FIRST_FAILURE_ONE_SIDED_COPY", + "verifier_sha256": "e413616a79cf2ecca824bc388588147316ad5c1863c12d571f305515526ecabf" +} diff --git a/research/first-failure-one-sided-copy/SOURCES.json b/research/first-failure-one-sided-copy/SOURCES.json new file mode 100644 index 0000000000..b57d785ddf --- /dev/null +++ b/research/first-failure-one-sided-copy/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/masked-e8-puncture-threshold/CERTIFICATE.json", + "usage": "input", + "git_blob": "234719192377e15199c710acfc21df9177d4a476", + "sha256": "3fd9189d8d8c2d97ff0224544c1415a0a4b700062fe0eafbf2571a448e1a7cf0" + } + ] +} diff --git a/research/first-failure-one-sided-copy/TASK.json b/research/first-failure-one-sided-copy/TASK.json new file mode 100644 index 0000000000..273a0ad403 --- /dev/null +++ b/research/first-failure-one-sided-copy/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "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": "changed", + "actual_scope": "Exhibit a non-coordinate eight-term one-sided mask-only completion with COPY71 versus COPY72 in the same frame on the fixed 93-line first-failure unit of PR1609, and an all-pairs COPY63 comparator on that same unit.", + "scope_change_reason": "The assigned card asks for a legal complete supplier invoice. This side result isolates the separate-term binary pairing-rank diagnostic at PR1609's first-failure boundary. The coordinate perturbation census belongs to the earlier public claim #discussioncomment-19530120 and is omitted here.", + "bottleneck_link": "A mask-only identity can lower a fixed-frame COPY bill without beating another all-pairs frame. The two explicit constructions distinguish those comparisons before spending effort on unpriced physical acquisition, restoration and delivery.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified non-coordinate completion and explicit same-unit comparator. Do not optimize frames further or construct a physical supplier.", + "outcome": "completed", + "evidence": "RESULT.json is generated by verify.py and binds the verifier and predecessor certificate hashes. Exact rational checks cover every entry of the two new constructions and the same-frame baseline. Every support pairing rank is computed by bitset and dense F2 elimination. The one-sided ranks are [8,9,9,9,9,9,9,9]; the all-pairs ranks are [7,8,7,8,8,8,8,9].", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can any eight-term one-sided mask-only completion on this fixed 93-line unit beat the exhibited all-pairs profile [7,7,7,8,8,8,8,9] under separate-term COPY pricing?", + "why_it_matters": "The fixed-frame saving alone does not improve the best exhibited all-pairs comparator.", + "first_step": "Use the rank-seven target neighbourhood to parameterize root-linear top frames and the one-dimensional target-row freedom; first test support pairing ranks against the explicit comparator.", + "blocked_by": "No global optimization or lower bound over arbitrary frames is supplied; physical costs remain additional obligations." + } + ], + "overlap": { + "upstream_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19530146", + "prior_coordinate_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19530120", + "coverage": "Live open PR titles/bodies, account PRs, latest 30 handoff comments and merged GitHub searches for 1609, one-sided COPY and 93 decoder; main README searches for first-failure, 27-deletion, 93-line and COPY63. The overlap helper reports 466 open PRs and 7089 discussion records, with complete pagination, and 10178 tracked local notes. Search is not a novelty proof.", + "excluded_work": "No coordinate scalar census, general first-failure census, root-frame optimum, physical supplier, kappa or selected-frontier change.", + "progress": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19537518", + "checked_at": "2026-11-11T08:00:00Z" + } +} diff --git a/research/first-failure-one-sided-copy/VERIFY.json b/research/first-failure-one-sided-copy/VERIFY.json new file mode 100644 index 0000000000..6a954c9d56 --- /dev/null +++ b/research/first-failure-one-sided-copy/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/masked-e8-puncture-threshold/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact rational 93x93 endpoint identities, all separate-term support pairing ranks through two F2 engines, generated receipt hashes, planted masked error and restoration controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same finite constructions and rejection controls with Python assertions disabled." + } + ] +} diff --git a/research/first-failure-one-sided-copy/verify.py b/research/first-failure-one-sided-copy/verify.py new file mode 100644 index 0000000000..f79ff2dc91 --- /dev/null +++ b/research/first-failure-one-sided-copy/verify.py @@ -0,0 +1,344 @@ +#!/usr/bin/env python3 +"""One-sided COPY recount at the 27-deletion first-failure boundary of PR1609. + +Standard library only; exact Fraction arithmetic. Any failed check exits nonzero. +The E8 geometry is rebuilt here (doubled coordinates, norm 8); no predecessor +code is imported. PR1609's CERTIFICATE.json is a live input whose witness fields +are compared with the reconstruction. + +Model (PR1609 and its copy diagnostic, restated): live lines L, a decoder +target 2G, with D = R A root-linear and T arbitrary, exact on the mask (orthogonal or +equal pairs, i.e. even root inner product). Term k has top support +S_k = {i in L : D[i,k] != 0} and bottom support T_k = {j in L : T[j,k] != 0}; +The checker uses doubled roots q and puts a factor 1/2 in the bottom factor. +Its price is the F2 rank of the pairing matrix N[S_k, T_k] with N[i,j] = 1 iff +the root inner product of lines i and j is even. +""" +import argparse +import hashlib +import json +import sys +from fractions import Fraction as Fr +from itertools import combinations, product +from pathlib import Path + +HERE = Path(__file__).resolve().parent +CERT = HERE.parent / "masked-e8-puncture-threshold" / "CERTIFICATE.json" + +# The PR1609 witness: doubled target root and the vector annihilating its neighbourhood. +TARGET = (2, 2, 0, 0, 0, 0, 0, 0) +NORMAL = (1, -1, 2, 0, 0, 0, 0, 0) +# One-sided frame: first bottom is a TARGET + b NORMAL, the other seven are e_1..e_7. +FRAME_AB = (13, 7) +# Eight root tops (doubled coordinates) of an all-pairs design on the same live lines. +COMPARATOR_TOPS = [ + (0, 0, 2, 0, 0, 0, 0, 2), (0, 0, 2, 0, 0, 0, -2, 0), + (1, -1, 1, -1, -1, -1, -1, -1), (1, -1, 1, -1, 1, -1, -1, 1), + (1, -1, 1, 1, 1, 1, -1, 1), (1, -1, 1, -1, 1, 1, -1, -1), + (1, -1, 1, -1, -1, 1, -1, 1), (1, 1, 1, 1, -1, 1, -1, 1), +] +SAME_FRAME_COPY = 72 +ONE_SIDED_COPY = 71 +COMPARATOR_COPY = 63 + + +def need(ok, message): + """Fail the whole run with a readable message.""" + if not ok: + raise SystemExit("FAIL: " + message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def build_lines(): + """The 120 E8 root lines in doubled coordinates, first nonzero entry positive.""" + roots = [] + for i, j in combinations(range(8), 2): + for si, sj in product((2, -2), repeat=2): + v = [0] * 8 + v[i], v[j] = si, sj + roots.append(tuple(v)) + for s in product((1, -1), repeat=8): + if s.count(-1) % 2 == 0: + roots.append(s) + lines = sorted(r for r in roots if next(x for x in r if x) > 0) + need(len(roots) == 240 and len(lines) == 120, "E8 root and line counts") + need(all(dot(r, r) == 8 for r in lines), "root norms") + return lines + + +LINES = build_lines() +NL = len(LINES) +IP = [[dot(a, b) // 4 for b in LINES] for a in LINES] +need(all(dot(a, b) % 4 == 0 for a in LINES for b in LINES), "Gram entries divisible by 4") +NR = [sum(1 << j for j in range(NL) if IP[i][j] % 2 == 0) for i in range(NL)] +INDEX = {r: i for i, r in enumerate(LINES)} + + +def rank2(rows): + """F2 rank of integer bitmask rows.""" + basis = {} + for v in rows: + for _ in range(NL): + if not v: + break + p = v.bit_length() - 1 + if p in basis: + v ^= basis[p] + else: + basis[p] = v + break + else: + need(v == 0, "F2 elimination exceeded the 120-bit bound") + return len(basis) + + +def rank_f2_dense(matrix): + """Independent F2 rank on explicit 0/1 lists (cross-check of rank2).""" + m = [row[:] for row in matrix] + rank = 0 + for c in range(len(m[0]) if m else 0): + pivot = next((r for r in range(rank, len(m)) if m[r][c]), None) + if pivot is None: + continue + m[rank], m[pivot] = m[pivot], m[rank] + for r in range(len(m)): + if r != rank and m[r][c]: + m[r] = [x ^ y for x, y in zip(m[r], m[rank])] + rank += 1 + return rank + + +def rational_rank(vectors): + m = [[Fr(x) for x in v] for v in vectors] + rank = 0 + for c in range(8): + p = next((r for r in range(rank, len(m)) if m[r][c] != 0), None) + if p is None: + continue + m[rank], m[p] = m[p], m[rank] + for r in range(len(m)): + if r != rank and m[r][c] != 0: + f = m[r][c] / m[rank][c] + m[r] = [a - f * b for a, b in zip(m[r], m[rank])] + rank += 1 + return rank + + +def invert(rows): + """Inverse of an 8x8 rational matrix given as rows.""" + a = [[Fr(x) for x in row] + [Fr(int(i == j)) for j in range(8)] for i, row in enumerate(rows)] + for c in range(8): + p = next((r for r in range(c, 8) if a[r][c] != 0), None) + need(p is not None, "singular frame") + a[c], a[p] = a[p], a[c] + pv = a[c][c] + a[c] = [x / pv for x in a[c]] + for r in range(8): + if r != c and a[r][c] != 0: + f = a[r][c] + a[r] = [x - f * y for x, y in zip(a[r], a[c])] + return [row[8:] for row in a] + + +def dual_basis(vectors): + """Vectors u_k with dot(v_l, u_k) = delta_lk (columns of the inverse).""" + inv = invert(vectors) + return [tuple(inv[i][k] for i in range(8)) for k in range(8)] + + +def boundary(t, normal): + """Deleted and live line indices for target t and a neighbourhood normal.""" + need(dot(LINES[t], normal) == 0, "normal not orthogonal to target") + deleted = [i for i in range(NL) if i != t and IP[t][i] == 0 and dot(LINES[i], normal) != 0] + live = [i for i in range(NL) if i not in deleted] + need(len(deleted) == 27 and len(live) == 93, "puncture size") + nbhd = [i for i in live if i == t or IP[t][i] == 0] + need(all(dot(LINES[i], normal) == 0 for i in nbhd), "neighbourhood not annihilated by normal") + return deleted, live + + +def ranks_for(live, source, tops, bottoms): + """Eight separate-term COPY ranks for a biorthogonal frame (tops, bottoms).""" + out = [] + for u, w in zip(tops, bottoms): + left = [i for i in live if dot(LINES[i], u) != 0] + right_indices = [j for j in live if dot(source[j], w) != 0] + right = sum(1 << j for j in right_indices) + rank = rank2([NR[i] & right for i in left]) + dense = [[int(IP[i][j] % 2 == 0) for j in right_indices] for i in left] + need(rank == rank_f2_dense(dense), "two F2 rank engines disagree") + out.append(rank) + return out + + +def source_rows(live, t, scale): + """Bottom rows: the lines themselves, with the target row moved to TARGET + scale NORMAL.""" + src = {j: LINES[j] for j in live} + src[t] = tuple(x + scale * y for x, y in zip(TARGET, NORMAL)) + return src + + +def exactness(live, source, tops, bottoms): + """Entries of D T^T - 2G over live pairs: (masked errors, unmasked errors, error map).""" + d = {i: [dot(LINES[i], u) for u in tops] for i in live} + tm = {j: [dot(source[j], w) for w in bottoms] for j in live} + masked = unmasked = 0 + errs = {} + for i in live: + for j in live: + e = (sum(a * b for a, b in zip(d[i], tm[j])) - dot(LINES[i], LINES[j])) / Fr(2) + if e != 0: + errs[(i, j)] = e + if IP[i][j] % 2 == 0: + masked += 1 + else: + unmasked += 1 + return masked, unmasked, errs + + +def check_geometry_and_certificate(): + need(rank2(NR) == 9, "F2 rank of the pairing matrix is not 9") + t = INDEX[TARGET] + deleted, live = boundary(t, NORMAL) + nbhd = [LINES[i] for i in live if i == t or IP[t][i] == 0] + need(len(nbhd) == 37 and rational_rank(nbhd) == 7, "deficient neighbourhood") + need(rational_rank([LINES[i] for i in live]) == 8, "live rank") + cert = json.loads(CERT.read_text())["witness"] + need(tuple(cert["target_doubled_root"]) == TARGET and tuple(cert["normal"]) == NORMAL, "witness vectors") + need(cert["live_ports"] == 93 and len(cert["deleted_indices"]) == 27, "certificate puncture size") + need(cert["deleted_indices"] == deleted, "certificate deleted line indices") + return t, deleted, live + + +def structured_frame(a, b): + w1 = tuple(a * x + b * y for x, y in zip(TARGET, NORMAL)) + return [w1] + [tuple(int(i == k) for i in range(8)) for k in range(1, 8)] + + +def check_one_sided_frame(t, live): + a, b = FRAME_AB + bottoms = structured_frame(a, b) + tops = dual_basis(bottoms) + need(all(dot(u, w) == int(i == j) for i, u in enumerate(tops) for j, w in enumerate(bottoms)), "biorthogonality") + star = Fr(-dot(bottoms[0], TARGET), dot(bottoms[0], NORMAL)) + r0 = ranks_for(live, source_rows(live, t, Fr(0)), tops, bottoms) + rs = ranks_for(live, source_rows(live, t, star), tops, bottoms) + need(star == Fr(-52, 21), "special scale") + need(r0 == [9] * 8 and sum(r0) == SAME_FRAME_COPY, "same-frame all-pairs baseline is not 72") + need(rs == [8] + [9] * 7 and sum(rs) == ONE_SIDED_COPY, "one-sided completion is not 71") + src0, srcs = source_rows(live, t, Fr(0)), source_rows(live, t, star) + m0, u0, e0 = exactness(live, src0, tops, bottoms) + ms, us, es = exactness(live, srcs, tops, bottoms) + need((m0, u0) == (0, 0), "all-pairs comparator is not exact on every pair") + need(ms == 0 and us == 56 and all(j == t for (_, j) in es), "one-sided completion is not mask-exact with 56 target-column errors") + need(all(es[(i, t)] == star * dot(LINES[i], NORMAL) / 2 for (i, _) in es), "error formula") + return tops, bottoms, star, r0, rs + + +def check_mechanism(t, live, tops, bottoms, star): + """Why one rank drops: the target is a coloop of the first bottom's live support.""" + odd = {i for i in range(NL) if IP[t][i] % 2} + need(len(odd) == 56, "56 lines odd to the target") + s0 = {j for j in live if dot(source_rows(live, t, Fr(0))[j], bottoms[0]) != 0} + ss = {j for j in live if dot(source_rows(live, t, star)[j], bottoms[0]) != 0} + need(s0 == odd | {t} and ss == odd, "bottom support is the root-ray support, minus the target at the special scale") + need(rank2([NR[i] for i in s0]) == 9 and rank2([NR[i] for i in ss]) == 8, "label span 9 with the target, 8 without") + top_support = [i for i in live if dot(LINES[i], tops[0]) != 0] + need(rank2([NR[i] for i in top_support]) == 9, "first top has full label span") + n = [[(NR[i] >> j) & 1 for j in sorted(ss)] for i in top_support] + need(rank_f2_dense(n) == 8, "dense cross-check of the rank-8 term") + need(rank_f2_dense([[(NR[i] >> j) & 1 for j in sorted(s0)] for i in top_support]) == 9, "dense cross-check of the rank-9 term") + + +def check_comparator(live): + tops = [tuple(Fr(x) for x in u) for u in COMPARATOR_TOPS] + need(all(tuple(u) in INDEX or tuple(-x for x in u) in INDEX for u in COMPARATOR_TOPS), "tops are root lines") + need(len({tuple(u) for u in COMPARATOR_TOPS}) == 8 and rational_rank(COMPARATOR_TOPS) == 8, "tops independent") + bottoms = dual_basis(tops) + src = {j: LINES[j] for j in live} + m, u, _ = exactness(live, src, tops, bottoms) + need((m, u) == (0, 0), "comparator is exact on all pairs") + ranks = ranks_for(live, src, tops, bottoms) + need(ranks == [7, 8, 7, 8, 8, 8, 8, 9] and sum(ranks) == COMPARATOR_COPY, "comparator ranks") + n_deleted_tops = sum(1 for u in COMPARATOR_TOPS if INDEX.get(u, INDEX.get(tuple(-x for x in u))) not in live) + need(n_deleted_tops == 7, "seven tops are deleted lines") + return tops, bottoms, ranks + + +def check_controls(t, deleted, live, tops, bottoms, star): + bad = [list(w) for w in bottoms] + bad[1][0] += 1 + masked, _, _ = exactness(live, source_rows(live, t, star), tops, [tuple(w) for w in bad]) + need(masked > 0, "planted bottom error not detected") + for x in deleted: + e = star * dot(LINES[x], NORMAL) + need(IP[x][t] % 2 == 0 and e != 0, "restoring a deleted line must expose a masked error") + sensitive = [(3, 1, 2, 0, 0, 0, 0, 0), (3, 1, -1, 0, 0, 0, 0, 0), (2, 0, -1, 0, 0, 0, 0, 0)] + sensitive += [tuple(int(i == k) for i in range(8)) for k in range(3, 8)] + r = ranks_for(live, source_rows(live, t, Fr(0)), dual_basis(sensitive), sensitive) + need(r == [8] + [9] * 7, "recount can return 8 when a top is a deleted-root direction") + return len(deleted) + + +def fraction_rows(rows): + return [[str(x) for x in row] for row in rows] + + +def result(): + t, deleted, live = check_geometry_and_certificate() + print("ok pinned 93-line instance reconstructed; no predecessor census replayed") + tops, bottoms, star, r0, rs = check_one_sided_frame(t, live) + print("ok non-coordinate frame: all-pairs 72, mask-only 71, scale %s" % star) + check_mechanism(t, live, tops, bottoms, star) + print("ok first bottom support loses the target; first pairing rank drops 9 -> 8") + ctops, cbottoms, cranks = check_comparator(live) + print("ok all-pairs comparator ranks %s total %d" % (cranks, sum(cranks))) + n_ctl = check_controls(t, deleted, live, tops, bottoms, star) + print("ok controls: planted masked error, %d restorations, rank sensitivity" % n_ctl) + return { + "schema_version": 1, + "status": "PASS_FIRST_FAILURE_ONE_SIDED_COPY", + "claim_type": "finite exact constructions", + "verifier_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(), + "source_sha256": hashlib.sha256(CERT.read_bytes()).hexdigest(), + "live_ports": len(live), + "deleted_indices": deleted, + "one_sided": { + "tops": fraction_rows(tops), "bottoms": fraction_rows(bottoms), + "target_scale": str(star), "same_frame_all_pairs_ranks": r0, + "copy_ranks": rs, "masked_errors": 0, "unmasked_errors": 56, + "first_bottom_support_sizes": [57, 56], + }, + "all_pairs": { + "tops": fraction_rows(ctops), "bottoms": fraction_rows(cbottoms), + "copy_ranks": cranks, "masked_errors": 0, "unmasked_errors": 0, + }, + "restoration_controls": n_ctl, + "no_new_kappa": True, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write a generated receipt; refuse overwrite") + args = parser.parse_args() + if args.write is not None: + need(not args.write.exists(), "receipt destination already exists") + need(CERT.stat().st_size <= 1024 * 1024, "source certificate exceeds 1 MiB") + sources = json.loads((HERE / "SOURCES.json").read_text()) + pin = next(row for row in sources["files"] if row["path"] == str(CERT.relative_to(HERE.parent.parent))) + need(hashlib.sha256(CERT.read_bytes()).hexdigest() == pin["sha256"], "source certificate hash") + receipt = result() + if args.write is not None: + with args.write.open("x") as stream: + stream.write(json.dumps(receipt, indent=2, sort_keys=True) + "\n") + else: + need(receipt == json.loads((HERE / "RESULT.json").read_text()), "generated receipt differs") + print("PASS_FIRST_FAILURE_ONE_SIDED_COPY one_sided=71 same_frame=72 all_pairs=63 no_new_kappa") + + +if __name__ == "__main__": + sys.exit(main())