diff --git a/research/p111-copy-rank-certificate/METHOD.md b/research/p111-copy-rank-certificate/METHOD.md new file mode 100644 index 0000000000..dc6aa6c6c1 --- /dev/null +++ b/research/p111-copy-rank-certificate/METHOD.md @@ -0,0 +1,118 @@ +# Local claim, search budget and verification record + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The clone was clean before this package was added. No applicable `AGENTS.md` +was present in the workspace ancestry or repository. The Gist, CONTRIBUTING, +selected certificate, current-status page, review ledger and selected review +were read. The accepted conditional kappa was +`51110230636731/31250000000000000`; pending PR titles were not substituted for it. + +## Claim and task selection + +OS-random assignment seed **41**, drawn with `secrets.randbelow(100)` at +2026-10-13 04:23 UTC, selects **structural decoder research**. + +Three narrow tasks were considered: + +1. Asymmetric paired-hypercube star punctures: recent #669 overlaps directly. +2. Generalized P111 label-functional totals: selected because #620's claimed + obstruction lacked proof logs and exact source binding; #555 is the primary + fixture (seed 41 is odd), #545 is the predecessor/control. +3. Repeated-label E8 planes: #446 already reports extensive fixed-dimension + SAT results, and broader vector-label mechanisms exceed this bounded task. + +The local claim was to establish or improve the minimum of +`sum rank_Q G[S(x_i),S(y_i)]` subject to `sum x_i y_i^t = B^-1` over F2, +with arbitrary nonzero nine-bit vectors and repeated terms allowed. Expected +deliverable: exact witnesses or a scoped obstruction, a deterministic verifier, +source pins and a local patch. No new supplier or exponent was promised. + +No pinned sprint coordination issue was found; the only returned issue was +#650, requesting a discussion channel. The user's instruction also required +local review before any public submission, so this claim remained local. +Six pages of open-PR metadata and the relevant descriptions were read for +overlap. The read snapshots and source text are preserved outside this package +in the task's `evidence/` directory. + +A final six-page metadata refresh observed PRs through #720 (537 unique +open PRs; pagination was not atomic). Relevant new descriptions #703, +#708 and #715, plus the source README section 5 of #717 at its pinned head, +were read. Their quaternionic, operand-preparation, mixed-port and complex +decoder scopes differ from this fixed bit-label problem. Main still pointed +to the same base commit. This is an overlap check, not a global novelty proof. + +The pre-submission refresh on 2026-10-13 also inspected all eight PRs returned +by an all-state `P111` search and the 100 most recently updated PRs, through +#748. New #728 optimizes punctured-word mini-node XORs, #738 concerns Gaussian +lines, #747 concerns paired-geometry global stars, and #748 changes an R420 +source representation while retaining copy ranks. Their descriptions add no +matching proof for these two fixed bit-label fixtures. Main and CONTRIBUTING +were unchanged. The exact heads are retained in `SOURCES.json`. + +## Fork-and-flush adaptation + +The installed `fork-and-flush` skill and its execution protocol were followed +using the supported `collaboration.spawn_agent` API, `fork_turns="none"`, and +three isolated filesystem copies of one frozen standalone starting artifact. +The user requested Astra/max. Each branch received the same objective, +evaluator, fixtures, predecessor context and limits, with no parent reasoning +or assigned approach. Branches did not spawn additional agents. + +Budget: one round, at most three candidate episodes per branch, at most 90 +seconds of search/evaluation per episode, and 12 minutes wall time per branch. +Each episode could include one bounded exhaustive proof search. Setup, +coordinator checks and final verification were additional reserved work inside +a 45-minute overall wall-clock ceiling starting at 04:23 UTC. At least the +final quarter was reserved for source binding, proof review and packaging. +Model token consumption was unavailable; episode counts are not token counts. + +The primary score was integer copied rank, lower is better; exact reconstruction +was mandatory. There was no noisy timing selection. Each baseline scored 63. +Branches used 1, 3 and 3 candidate evaluations respectively, all retaining the +same baseline. Their exact finite proof experiments included row-space, +unit-subset and Hamming-distance certificates. Each branch encountered and +documented one Python 3.9 `int.bit_count` compatibility failure in scratch +exploration, then used a portable popcount. No branch computation approached +90 seconds. The coordinator reran all three nominations serially: all scored +63, so the incumbent was retained on the exact tie. + +## Evaluator correction and re-evaluation + +Final source binding discovered an input defect in evaluator version 1: +`hamming_e8()` generates the correct root set in sorted Hamming-word order, +but numeric deletion indices refer to the supplier's different ordering. +The initial branch reports now explicitly say **archived-order model**. +They remain preserved and are not presented as replays of the published words. + +The evaluator was corrected to consume the pinned supplier root table, both +actual baselines were rebuilt, and both still have nine exact cost-seven +terms. The all-length analytic proof was checked against those corrected +geometric premises. An independent branch reran its finite obstruction for +both corrected fixtures: maximum nine-term benefit 9; minimum target distance +to a nonzero rank-one matrix 27; minimum target ones outside two rows/columns +31. Both baselines independently passed. The corrected incumbent was retained. + +Three bounded review follow-ups (at most five minutes each) reviewed the +projection proof, reviewed code/source binding, and independently reran the +corrected finite certificates. These are final verification, not another +exploration round. No errors remained in the reviewed proof. The compact +rank-three minor checks in the final package provide another exact obstruction +for the two actual fixtures. + +The original round used **seven** candidate-evaluator calls in aggregate, +plus three coordinator nomination checks. Input repair added two corrected +baseline rebuild checks and independent corrected-fixture checks. The full +standard-library verifier and selected-record integrity checks were then run. +Raw branch reports, failures, hashes, elapsed times and review receipts are +preserved in the task's `fork-workspaces/` and `evidence/` directories; this +package contains only the final mathematical artifact and its deterministic +receipt. No performance speedup or paper-reported fork-and-flush gain is claimed. + +## Verification limits + +This adds a standalone research package. Existing generators, suppliers, +selected-frontier pointers and `upstream/` were not edited. The relevant +package checks and selected-record source integrity check passed. The expensive +repository-wide `make verify` / cold supplier replay was not run; this package +does not claim to re-certify those constructions. No credential change, +security change or package installation was required. diff --git a/research/p111-copy-rank-certificate/NOTICE.md b/research/p111-copy-rank-certificate/NOTICE.md new file mode 100644 index 0000000000..ee8a450a6f --- /dev/null +++ b/research/p111-copy-rank-certificate/NOTICE.md @@ -0,0 +1,38 @@ +# Attribution and license + +This local contribution was prepared by OpenAI Codex at Russell Seligmann's +request, with substantial AI assistance in mathematics, implementation, +verification and writing. Three fresh Astra/max agents independently explored +the same fixed objective and subsequently checked the corrected artifact. +Their reviews are AI reviews, not human-only or Lean reviews. + +New material is offered under the repository's Apache-2.0 license. The root +table in `roots.json` is extracted from the pinned R420 supplier. Its source +and all consumed word bytes retain their original attribution and notices. + +Predecessor credit: + +- **Dylan Crow / utcorvusvolat-dotcom (#370)**: E8 bit geometry and the original + bit word/checker lineage. +- **DreamingOfClouds (#545)**: the punctured-star bit unit and nine rank-seven + decoder totals. +- **eumemic (#543, #555)**: the R420 carrier skeleton and the different P111 + puncture realized on that skeleton. +- **Joel Pulikkan / GamingPuzzled (#620)**: generalized decoder experiments, + the 6/7/8 cost classification and the reported cost-63 SAT obstruction. +- **DreamingOfClouds (#446, #595)**: the per-total drop-pricing framework and + the format-limit analysis that motivated the copied-information question. +- **Jacob Sussman**, the upstream multiplication framework's authors, and the + full contributor lineage retained in those packages: the frame and network + setting. This note does not re-verify that full framework. +- **vectorsss (#631)** and **Sam Sung / the-missionary-company (#669)**: + related E8 and paired-hypercube puncture results consulted for overlap. +- **Douglas R. Colkitt / Mister-Meeseeks (#703)**, **Sagar Thakrar / + thakrarsagar (#708, #715)** and **DreamingOfClouds (#717)**: related + quaternionic, bit-circuit, mixed-port and complex-decoder work consulted + during the final overlap review; no proof or code imported. + +The value 63 and its previously reported optimality are not claimed as new. +The added contribution is the solver-free argument, exact source-bound +verification for both actual punctures, and the ordering regression evidence. +No global novelty or priority claim is made. diff --git a/research/p111-copy-rank-certificate/ORDERING.json b/research/p111-copy-rank-certificate/ORDERING.json new file mode 100644 index 0000000000..ab04cd853a --- /dev/null +++ b/research/p111-copy-rank-certificate/ORDERING.json @@ -0,0 +1,172 @@ +{ + "first_mismatch": { + "index": 8, + "archived_root": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "supplier_root": [ + 0, + 1, + 1, + 0, + 1, + 0, + 0, + 1 + ] + }, + "same_signed_root_set": true, + "archived_to_supplier_permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 112, + 113, + 114, + 115, + 116, + 117, + 118, + 119, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71 + ], + "mapped_archived_punctures": { + "pr545": [ + 9, + 31, + 37, + 52, + 66, + 76, + 78, + 111, + 119 + ], + "pr555": [ + 8, + 17, + 39, + 51, + 53, + 58, + 63, + 72, + 114 + ] + } +} diff --git a/research/p111-copy-rank-certificate/PROOF.md b/research/p111-copy-rank-certificate/PROOF.md new file mode 100644 index 0000000000..0ce5a79742 --- /dev/null +++ b/research/p111-copy-rank-certificate/PROOF.md @@ -0,0 +1,191 @@ +# A solver-free lower bound for P111 generalized label decoders + +This is a scoped lower bound on a sum of rational pairing ranks. It is not a +new multiplication exponent, and it does not assert that every abstract term +can be implemented at its lower-bound price. The physical interpretation uses +the per-total drop-pricing premise of DreamingOfClouds' #446, Theorem C. + +## 1. Fixed model and exact geometric premises + +Let `L` be the 120 E8 root-line representatives in the extended-Hamming +numbering used by #370 and the punctured-star packages. Each has squared norm +4, and `G = LL^t/2` has diagonal 2 and off-diagonal entries in `{−1,0,1}`. +Put `B0 = (J + G) mod 2`. + +Delete one of these nine-element sets: + +- #545: `{39,52,57,71,76,78,103,109,114}`; +- #555: `{10,15,51,53,56,66,72,89,111}`. + +Write `P` for the ordered deletion list and `V` for the 111 live indices. +Let `B = B0[P,P]`, `M = B^(-1)` and `R = B0[V,P]`, all over F2. +The verifier establishes the following exact finite premises separately for +each set: + +1. `B` is symmetric and invertible, with every diagonal entry equal to one. +2. `R` has column rank nine and `B0[V,V] = R M R^t`. +3. For every nonzero `x in F2^9`, put + `S(x) = {v in V : R[v,:] x = 1}` and + `W(x) = span_Q {L[v] : v in S(x)}`. + Precisely the nine vectors `x=e_i` have deficient span; for them + `W(e_i) = L[P_i]^perp` has dimension seven. Every other `W(x)` is Q^8. + +A generalized **label** decoder here is any finite list of nonzero binary +vectors `(x_i,y_i)` satisfying + +`sum_i x_i y_i^t = M` over F2. + +Equivalently its source/reader rectangles reproduce the fixed binary decoder +`B0[V,V]`. Both sides of every rectangle are evaluations of linear +functionals of the fixed nine-dimensional label space. Arbitrary port-subset +rectangles outside this class, a changed decoder matrix, vector-valued labels, +and changes to the correction network are not covered. + +The priced objective is + +`C = sum_i beta(x_i,y_i)`, +`beta(x,y) = rank_Q G[S(x),S(y)]`. + +Premise 3 and nondegeneracy of the Euclidean form give: + +- cost 8 if neither vector is a coordinate unit; +- cost 7 if exactly one vector is a coordinate unit; +- cost 6 for `x=e_a,y=e_b` when `L[P_a] . L[P_b] = 0`; +- cost 7 for the remaining unit/unit pairs. + +For the hyperplane/hyperplane case, the pairing kernel on `a^perp` is +`a^perp intersect span(b)`. It has dimension one exactly when `a.b=0`. +All other cases follow immediately. Every cost-6 term therefore has distinct +coordinate indices and `B[a,b]=1`. Conversely, distinct unit indices with +`B[a,b]=1` have cost 6. The verifier checks the finite premises using integer +elimination and cross-checks all 100 pairs of span classes by Fraction +elimination. Thus the classification covers all 511^2 ordered nonzero pairs. + +## 2. Nine totals cost at least 63 + +Let `X` and `Y` have the `x_i` and `y_i` as columns. If there are nine terms, +`XY^t=M` is invertible, so both matrices are invertible and + +`Y^t B X = I_9`. + +Let `a` be the number of unit columns of `X`, `b` the number of unit columns +of `Y`, and `c` the number of terms with `x_i=y_i=e_j` for some coordinate +`j`. Unit coordinates do not repeat inside either invertible matrix. +Furthermore, if `x_i=y_j=e_t`, then `(Y^t B X)[j,i]=B[t,t]=1`, forcing +`i=j`. Hence the union of unit coordinates has size `a+b-c`, and + +`a+b-c <= 9`. + +If both sides of a term are distinct units, its diagonal entry in +`Y^t B X` is one, so it is a cost-6 term. A term with just one unit, or the +same unit on both sides, costs seven. The exact total is consequently + +`C = 8*9 - (a+b-c) >= 63`. + +This argument permits arbitrary bases and asymmetric source/reader choices; +it is not restricted to stars or symmetric factorizations. + +## 3. Ten totals cost at least 64 + +For ten terms, `X,Y` are 9-by-10 of rank nine. Define + +`K = Y^t B X`. + +The identity `XY^t=M` gives `K^2=K` and `rank(K)=9`. Its complement has rank +one, so over F2 + +`K = I_10 + alpha beta^t` + +for nonzero `alpha,beta` (with `beta^t alpha=1`). + +Let `S` index the `k` cost-6 terms. Their diagonal entries `K[i,i]` equal +one, hence `alpha_i beta_i=0` for every `i in S`. In particular the +restrictions of `alpha` and `beta` to S have disjoint supports. The principal +submatrix + +`K[S,S] = I_k + alpha_S beta_S^t` + +is invertible: its square is the identity, since `beta_S^t alpha_S=0`. +Thus the corresponding unit columns of `X` are distinct, as are those of +`Y`. Let A and D be their two k-element sets of coordinate indices. + +There are at least `2k-9` coordinates in `A intersect D`. Any such +coordinate has a unique representation `x_i=y_j=e_t`, with `i,j in S`. +Here `i != j` because a cost-6 term cannot have the same unit on both sides. +Since `B[t,t]=1`, + +`1 = K[j,i] = alpha_j beta_i`. + +Distinct common coordinates use distinct i and distinct j. Their number is +at most each of `|supp(alpha_S)|` and `|supp(beta_S)|`, whose sum is at most k. +Therefore + +`2k-9 <= |A intersect D| <= floor(k/2)`, + +which forces `k <= 6`. All other terms cost at least seven, giving + +`C >= 6k + 7(10-k) = 70-k >= 64`. + +No enumeration of SAT models or selection of a term-type pattern is used. +The bound 64 is only a lower bound for ten totals; attainability at 64 is +not asserted. + +## 4. Arbitrarily many totals and attainment + +Fewer than nine rank-one terms cannot sum to the rank-nine matrix M. +Eleven or more nonzero terms cost at least `6*11=66`. Terms with a zero +factor can be deleted without changing the decoder and need not be counted. +Sections 2–3 therefore cover every possible improvement over 63, even when +the number of totals is not bounded in advance and repeated terms are allowed. + +For each of the two fixtures, the row decomposition + +`M = sum_{i=0}^8 e_i (row_i(M))` + +has nine cost-7 terms. Its literal vectors are supplied in the two baseline +JSON files and checked against all 111-by-111 live decoder entries. Hence +the exact optimum of this abstract copied-rank objective is **63** for both +fixtures. + +## 5. What this adds and what remains open + +GamingPuzzled's #620 already reports that cost <=62 is infeasible for a +nine-line puncture identified there as #545, using CaDiCaL without proof logs. +That reported optimum is predecessor work, not a novelty claim here. +There is a source-binding discrepancy: the archived `hamming_e8()` sorts the +Hamming words, while the actual supplier files use a different order of the +same signed root set. The report's literal indices select supplier-index set +`{9,31,37,52,66,76,78,111,119}`, rather than the actual #545 deletion set above. +`ORDERING.json` records the complete exact permutation. The reported 44 +cost-6 ordered pairs belong to that archived-order example; the actual #545 +example has 36 (the actual #555 example has 44). + +The contribution is a short algebraic proof independent of that solver, +exact portable verification bound to the actual supplier files (the archived +exploration uses floating rank in `geo.py`), and explicit coverage of #555's +different puncture. The ordering discrepancy does not refute the reported +optimum; the present proof establishes 63 for both actual published inputs. +#631 proves a broader puncture threshold for star decoders; the present class instead +permits asymmetric factorizations and extra totals for two fixed punctures. +#669 concerns paired-hypercube stars, a different geometry. + +The final overlap review also read #717's section 5. Its complex P111 +examples have eight rational terms priced by binary label-pairing rank; +the present bit model has binary label terms priced by rational pairing +rank. #717 explicitly credits the bit-side value 63 to #620 and does not +repeat that calculation. #703 proves a quaternionic copy-cost floor; +#708 reduces R420 operand-preparation XORs while retaining its nine copies; +#715 studies a non-root-port extension. None of those results is used as a +premise here. This review is not a global priority or novelty claim. + +The proof does not certify the general drop-pricing interface, simultaneous +frame scheduling, source access, helper preparation/restoration, common-cut +or mutable-basis assumptions, the suppliers, the assembly, or the full +multiplication theorem. It does not show uniqueness of every possible E8 +decoder matrix. It closes only the stated label-functional factorization +mechanism for reducing this copy-rank objective. There is no new kappa claim +or claim to improve the selected frontier. + +The all-length conclusion comes from the written linear-algebra proof. +Finite code checks support its premises and test its finite-dimensional +identities; they are not a formal proof-assistant verification. diff --git a/research/p111-copy-rank-certificate/README.md b/research/p111-copy-rank-certificate/README.md new file mode 100644 index 0000000000..1756b7d57b --- /dev/null +++ b/research/p111-copy-rank-certificate/README.md @@ -0,0 +1,98 @@ +# P111 copied-rank optimum, without a SAT solver + +**Scoped negative result: the generalized label-decoder copy-rank optimum is +63 for the actual #545 and #555 E8 punctures. No new kappa is claimed.** + +The [proof](PROOF.md) permits asymmetric rank-one factorizations, repeated +terms and any finite number of totals. Nine totals cost at least 63; ten cost +at least 64; eleven or more cost at least 66. Literal nine-term witnesses +attain 63. This closes one precise way to reduce copied information, under +the stated per-total pairing-rank price, without pricing a new supplier. + +It also resolves a source-binding discrepancy in the archived #620 decoder +experiment. Its sorted Hamming-root numbering differs from the actual word +files. Applying the same numeric deletion list selects a different puncture. +The exact permutation is in [ORDERING.json](ORDERING.json); the checker binds +all roots, live indices and deletions to the pinned supplier files. The +reported optimum is corroborated for the actual published examples, but the +archived geometry is not silently treated as their replay. + +## Reproduce + +From the repository root at base +`66849e1475c930fd7732b1a0067ffee7e1e95f60`, with this package applied: + +```sh +python3 -B research/p111-copy-rank-certificate/verify.py --check research/p111-copy-rank-certificate/RESULTS.json +``` + +Python 3.9 or later, standard library only; no installation, optimizer, +network connection or source generation is needed. Expected output: + +```text +PASS_P111_COPY_RANK: optimum 63 on two fixtures; exact geometry, independent minors, 18 negative controls +``` + +`--write /absolute/path/results.json` writes a fresh deterministic receipt. +The verifier works from another current directory as well. It is safe to +run with Python's `-O`: checks do not depend on `assert` statements. + +The narrower candidate evaluator can be run separately: + +```sh +python3 -B research/p111-copy-rank-certificate/evaluate.py research/p111-copy-rank-certificate/baseline-pr555.json +``` + +It returns a valid nine-term cost-63 decomposition. Its search interface caps +input length at 20; the written proof's all-length conclusion does not rely +on that implementation cap. + +## Evidence and scope + +For **each** published fixture, the checker verifies: + +- all 511 nonzero functional supports with independent integer and rational + elimination: nine hyperplanes of dimension seven, 502 full spaces; +- all 100 ordered pairs of span classes, covering all 261,121 ordered + nonzero functional pairs by the proved span classification; +- all 12,321 live decoder matrix entries and the literal optimum witness; +- an independent rank-three target minor untouched by every cost-six term, + excluding a ten-term solution below 63; +- nine failure controls, including the wrong-root-order regression. + +In addition, all nonsingular symmetric unit-diagonal 3-by-3 binary matrices +are exercised across 672 square and 40,320 one-extra-term factorizations. +These finite controls test the projection mechanism; the dimension-nine, +arbitrary-length conclusion is the written algebraic proof, not an inference +from those smaller examples. The stronger ten-term lower bound of 64 uses +that proof; the independent minor certificates only exclude costs below 63. + +The geometric premises, source pins and baseline witnesses are exact. +The interpretation as a price for physical copy trees inherits #446's +Theorem C and its model assumptions. Arbitrary non-label rectangles, changed +decoder matrices, vector-valued labels, helper work, frame scheduling, +restoration, all-size compilation and the full multiplication theorem remain +outside scope. The selected frontier and `upstream/` are unchanged. + +## Provenance and prior work + +[SOURCES.json](SOURCES.json) pins the base and 16 repository files, including +the original compressed word bytes. `roots.json` is a small extraction of +the R420 root table; it is compared to that source and to a freshly generated +E8 root set. No upstream implementation is imported by the arithmetic code. + +DreamingOfClouds' #545 and eumemic's #555 provide the two punctured suppliers; +GamingPuzzled's #620 reports the earlier cost-63 SAT obstruction without proof +logs; DreamingOfClouds' #446 provides the drop-pricing framework. The point of +this contribution is a portable algebraic proof and precise source binding, +not priority for the number 63. Related #631 and #669 study different decoder +classes. The final overlap review also read #717's complex decoder section: +its P111 examples use eight rational terms and a binary pairing-rank price, +whereas this result uses binary label terms and a rational pairing-rank price. +#703 concerns quaternionic lines; #708 changes operand preparation, and #715 +adds non-root ports. See [NOTICE.md](NOTICE.md) and [METHOD.md](METHOD.md) for attribution, +the bounded fork-and-flush run, the corrected evaluator and verification limits. + +This is a research contribution for review. No human-only review or +proof-assistant verification is claimed. Local test details are in +[VALIDATION.md](VALIDATION.md). diff --git a/research/p111-copy-rank-certificate/RESULTS.json b/research/p111-copy-rank-certificate/RESULTS.json new file mode 100644 index 0000000000..61d4020215 --- /dev/null +++ b/research/p111-copy-rank-certificate/RESULTS.json @@ -0,0 +1,211 @@ +{ + "fixtures": { + "pr545": { + "attainment": { + "cost": 63, + "instance": "pr545", + "term_costs": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "terms": 9, + "valid": true + }, + "binary_puncture_gram_rows": [ + 17, + 314, + 284, + 462, + 471, + 418, + 472, + 248, + 382 + ], + "independent_ten_term_minor": { + "columns": [ + 0, + 1, + 2 + ], + "cost6_cells_on_minor": 0, + "minor_rows_binary": [ + 4, + 6, + 3 + ], + "rank": 3, + "rows": [ + 0, + 1, + 2 + ] + }, + "live_decoder_entries": 12321, + "negative_controls": [ + "wrong_coefficient", + "missing_total", + "zero_factor", + "boolean_factor", + "corrupted_target", + "corrupted_live_label", + "wrong_root_order", + "false_copy_discount", + "missing_unit_diagonal" + ], + "ordered_nonzero_pairs_covered": 261121, + "ordered_span_class_pairs": 100, + "pair_cost_histogram": { + "6": 36, + "7": 9081, + "8": 252004 + }, + "punctures": [ + 39, + 52, + 57, + 71, + 76, + 78, + 103, + 109, + 114 + ], + "reader_spans": 511, + "span_dimensions": { + "7": 9, + "8": 502 + }, + "target_inverse_rows": [ + 380, + 422, + 147, + 25, + 381, + 307, + 401, + 326, + 499 + ] + }, + "pr555": { + "attainment": { + "cost": 63, + "instance": "pr555", + "term_costs": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "terms": 9, + "valid": true + }, + "binary_puncture_gram_rows": [ + 507, + 135, + 238, + 349, + 185, + 437, + 205, + 503, + 425 + ], + "independent_ten_term_minor": { + "columns": [ + 1, + 4, + 8 + ], + "cost6_cells_on_minor": 0, + "minor_rows_binary": [ + 1, + 4, + 2 + ], + "rank": 3, + "rows": [ + 1, + 4, + 8 + ] + }, + "live_decoder_entries": 12321, + "negative_controls": [ + "wrong_coefficient", + "missing_total", + "zero_factor", + "boolean_factor", + "corrupted_target", + "corrupted_live_label", + "wrong_root_order", + "false_copy_discount", + "missing_unit_diagonal" + ], + "ordered_nonzero_pairs_covered": 261121, + "ordered_span_class_pairs": 100, + "pair_cost_histogram": { + "6": 44, + "7": 9073, + "8": 252004 + }, + "punctures": [ + 10, + 15, + 51, + 53, + 56, + 66, + 72, + 89, + 111 + ], + "reader_spans": 511, + "span_dimensions": { + "7": 9, + "8": 502 + }, + "target_inverse_rows": [ + 374, + 79, + 99, + 226, + 417, + 381, + 239, + 344, + 177 + ] + } + }, + "format": "p111-copy-rank-certificate-v1", + "optimum": 63, + "proved_bounds_by_term_count": { + "n_eq_10": 64, + "n_eq_9": 63, + "n_ge_11": "6*n >= 66", + "n_lt_9": "rank obstruction" + }, + "root_ordering_checked": true, + "scope": "Written algebraic proof plus exact finite premise checks; no new kappa or full supplier proof", + "small_projection_checks": { + "binary_gram_matrices": 4, + "dimension": 3, + "one_extra_term_factorizations": 40320, + "square_factorizations": 672 + }, + "source_pins_checked": 16 +} diff --git a/research/p111-copy-rank-certificate/SOURCES.json b/research/p111-copy-rank-certificate/SOURCES.json new file mode 100644 index 0000000000..c6593bb475 --- /dev/null +++ b/research/p111-copy-rank-certificate/SOURCES.json @@ -0,0 +1,96 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "files": { + "CONTRIBUTING.md": "a10dd640ec6f4b1d8b6acc31220af512335dc093f634cd25f601acb07ac53d53", + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/current-status.md": "197319a6edf04340ec3623d09d03714fcd6a981359f22bdcefdd06e7e2f4174d", + "docs/research/pr-ledger.md": "2e811684201e08007377ee97b1c35c0f0b3c026dd8207e7b0de3ff7cd1e13a91", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "research/e8-punctured111-star/README.md": "1e376d9fc28860adb0c68a0e92123e035ccb903794c457c43ba1f05d61d54625", + "research/e8-bit-p111/README.md": "481431e35bd831ec3d0bb8edc01abdfa49d5caeabebab67ac839a35053e9ef85", + "research/e8-bit-p111/data/punct.json": "dd371e1d6fe57602f242920b582ec4c133efc8ede4a849fd701ac90b7f6e1853", + "research/format-limits-corrected/README.md": "1bcd80c1cd61fddae9f3a7f00fc9d1c796410408251e576600e94c19b16b1e5e", + "research/format-limits-corrected/scripts/e8units.py": "3134443d8327d0bf2a8a66c26327cf5268cec6b7ffd85dde750b7e197ce63ef1", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/REPORT.md": "16c53bf8afd9f91eca02b2af9c9f5f09385823fc705dd1a48153508cfdff28b6", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/dec9sat.py": "1a1a41bb4195a238bff0c576d6cd8ba22f327670f39fd63495970e953f120788", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/geo.py": "73f9c4e4fb7d424fcba45eb5da36bdab694b10020341924b7ebfe7276868716a", + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "research/e8-bit-p111/data/bitE8mut-p111.json.gz": "1bc3c53d4baf4927c6a00c339ea3975516471a48074d4d97c6addaded2a4d858", + "research/e8-punctured111-star/data/bitE8mut-v111-r489.json.gz": "c78317ab05ea175dc380f4dce2bafdbcd7e8b46f0c9d6baf350c2f604bb3ae4e" + }, + "external_references": [ + { + "pr": 446, + "author": "DreamingOfClouds", + "head": "309482849b6ddf34db998f53612d34c19f6e3233", + "path": "research/format-obstructions/PROOF.md", + "url": "https://github.com/DreamingOfClouds/integer-mult-bounds/blob/309482849b6ddf34db998f53612d34c19f6e3233/research/format-obstructions/PROOF.md", + "sha256": "7a8c3bab633c08e7d96297dec9f9e7ed68d6bd0e076b73310c7d6b08a16df017", + "role": "Read as the inherited drop-pricing premise; not executed or reverified by this package." + }, + { + "pr": 631, + "head": "fb893b5ee1317c2da3b297e6fe78eca0857d1a76", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/631", + "role": "Overlap inspection of description; proof not used." + }, + { + "pr": 669, + "head": "308f1e6ec3bb0b6ec0584cf7bfe219addc219b1e", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/669", + "role": "Overlap inspection of description; proof not used." + }, + { + "pr": 703, + "head": "358383e2f1b0f292d4d6eb897c06fd8558a4f5e6", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/703", + "role": "Overlap inspection of description; quaternionic geometry; proof not used." + }, + { + "pr": 708, + "head": "2ec522a466ec448f148d4355dc43b51c0ef1e0b5", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/708", + "role": "Overlap inspection of description; operand preparation; proof not used." + }, + { + "pr": 715, + "head": "d8ed5c6cf2781d6efa0062a2636e1a2644f96c85", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/715", + "role": "Overlap inspection of description; mixed-port geometry; proof not used." + }, + { + "pr": 717, + "head": "07f4671a838088b59c6356ab2b5ffe30038d4b1a", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/717", + "role": "Read source README section 5 for complex decoder scope; proof not used.", + "path": "research/format-limits-2/README.md", + "source_url": "https://github.com/DreamingOfClouds/integer-mult-bounds/blob/07f4671a838088b59c6356ab2b5ffe30038d4b1a/research/format-limits-2/README.md", + "local_snapshot_sha256": "f15d9c66008b323d76b431f130a7ce1e65f018d87721beb37e3a242195bf3f1a" + }, + { + "pr": 728, + "head": "d454ae19fdd474b4dfa7bd2c28bbe5b0996365fb", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/728", + "role": "Pre-submission description review for overlap: punctured-word mini-node XORs; proof and code not used." + }, + { + "pr": 738, + "head": "9671c5d72f3119ba26f3774f40aa7130c67bcf77", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/738", + "role": "Pre-submission description review for overlap: Gaussian line geometry; proof and code not used." + }, + { + "pr": 747, + "head": "aeaf0899179a14644b412e838ede14db967c765e", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/747", + "role": "Pre-submission description review for overlap: paired-geometry global stars; proof and code not used." + }, + { + "pr": 748, + "head": "0ccc0b425d2b9667108d3a0918a5cfa0aa7a5861", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/748", + "role": "Pre-submission description review for overlap: R420 source representation; proof and code not used." + } + ] +} diff --git a/research/p111-copy-rank-certificate/VALIDATION.md b/research/p111-copy-rank-certificate/VALIDATION.md new file mode 100644 index 0000000000..16e3c5c135 --- /dev/null +++ b/research/p111-copy-rank-certificate/VALIDATION.md @@ -0,0 +1,27 @@ +# Local validation + +Platform: macOS 26.6.2, arm64. Validation date: 2026-10-13 UTC. + +The complete verifier passed on Python 3.9.6 and on Python 3.13.14 with +`-O -B`, the latter from a different current directory. Both regenerated +byte-identical receipts with SHA-256 +`38eae5165067234caf23a7a950fc009afec799bf13f02dbcdaed29982547f520`. +Measured runtimes were approximately 5.78 and 2.59 seconds respectively; +these are observations, not a benchmark comparison. + +Each run checked both pinned published fixtures, every nonzero functional +support, all span-class pairings, all live decoder entries, the attaining +witnesses, both independent rank-three minor obstructions, 18 negative +controls and the exhaustive three-dimensional projection controls. + +The package was also replayed after applying its patch to a relocated +minimal base containing only the 16 pinned input files. Source-byte and +receipt tampering were separately rejected. Whitespace and selected-result +integrity checks passed. Raw commands, versions, receipts and elapsed times +are retained in the task's external `evidence/` directory. + +Three fresh Astra/max branches participated in the bounded search. Final +AI reviews separately checked the algebraic projection proof, code/source +binding and an independent exhaustive obstruction on the corrected fixtures. +No human-only review, Linux CI run, Lean verification, repository-wide +`make verify`, or full supplier cold replay is claimed. diff --git a/research/p111-copy-rank-certificate/baseline-pr545.json b/research/p111-copy-rank-certificate/baseline-pr545.json new file mode 100644 index 0000000000..ec5d52f548 --- /dev/null +++ b/research/p111-copy-rank-certificate/baseline-pr545.json @@ -0,0 +1,41 @@ +{ + "instance": "pr545", + "terms": [ + [ + 1, + 380 + ], + [ + 2, + 422 + ], + [ + 4, + 147 + ], + [ + 8, + 25 + ], + [ + 16, + 381 + ], + [ + 32, + 307 + ], + [ + 64, + 401 + ], + [ + 128, + 326 + ], + [ + 256, + 499 + ] + ] +} diff --git a/research/p111-copy-rank-certificate/baseline-pr555.json b/research/p111-copy-rank-certificate/baseline-pr555.json new file mode 100644 index 0000000000..2daca704d8 --- /dev/null +++ b/research/p111-copy-rank-certificate/baseline-pr555.json @@ -0,0 +1,41 @@ +{ + "instance": "pr555", + "terms": [ + [ + 1, + 374 + ], + [ + 2, + 79 + ], + [ + 4, + 99 + ], + [ + 8, + 226 + ], + [ + 16, + 417 + ], + [ + 32, + 381 + ], + [ + 64, + 239 + ], + [ + 128, + 344 + ], + [ + 256, + 177 + ] + ] +} diff --git a/research/p111-copy-rank-certificate/evaluate.py b/research/p111-copy-rank-certificate/evaluate.py new file mode 100644 index 0000000000..8b74aa2cc7 --- /dev/null +++ b/research/p111-copy-rank-certificate/evaluate.py @@ -0,0 +1,11 @@ +"""Fixed fork-round evaluator; lower total copied rank is better.""" +import argparse +import json +from pathlib import Path +from exact import Instance + +parser = argparse.ArgumentParser() +parser.add_argument("candidate", type=Path) +args = parser.parse_args() +candidate = json.loads(args.candidate.read_text()) +print(json.dumps(Instance(candidate["instance"]).evaluate(candidate["terms"]), sort_keys=True)) diff --git a/research/p111-copy-rank-certificate/exact.py b/research/p111-copy-rank-certificate/exact.py new file mode 100644 index 0000000000..b97ee64deb --- /dev/null +++ b/research/p111-copy-rank-certificate/exact.py @@ -0,0 +1,180 @@ +"""Independent, standard-library arithmetic for P111 label decoders. + +E8 root numbering follows the extended-Hamming construction used by the +repository. No repository implementation is imported. +""" +from itertools import product +from math import gcd +import json +from pathlib import Path + +PUNCTURES = { + "pr545": [39, 52, 57, 71, 76, 78, 103, 109, 114], + "pr555": [10, 15, 51, 53, 56, 66, 72, 89, 111], +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def parity(x): + return bin(x).count("1") % 2 + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def generated_root_set(): + generators = [ + (1, 1, 1, 1, 0, 0, 0, 0), + (0, 0, 1, 1, 1, 1, 0, 0), + (0, 0, 0, 0, 1, 1, 1, 1), + (0, 1, 0, 1, 0, 1, 0, 1), + ] + code = {tuple(sum(c[i] * generators[i][j] for i in range(4)) % 2 + for j in range(8)) for c in product((0, 1), repeat=4)} + weight4 = sorted(c for c in code if sum(c) == 4) + out = [tuple(2 * (a == b) for b in range(8)) for a in range(8)] + for word in weight4: + support = [i for i, x in enumerate(word) if x] + for signs in product((1, -1), repeat=3): + r = [0] * 8 + for i, sign in zip(support, (1,) + signs): + r[i] = sign + out.append(tuple(r)) + require(len(out) == 120 and len(set(out)) == 120, "bad root census") + require(all(dot(r, r) == 4 for r in out), "bad root norm") + return out + + +def roots(): + """Pinned supplier ordering, checked against an independently generated set. + + Sorting Hamming words generates the right set in a different order; numeric + puncture IDs must instead follow the actual supplier's root table. + """ + data = json.loads((Path(__file__).resolve().parent / "roots.json").read_text()) + out = [tuple(row) for row in data["lines"]] + require(len(out) == 120 and set(out) == set(generated_root_set()), "bad indexed root table") + return out + + +def row_basis_q(rows): + """Fraction-free integer elimination; output spans the same Q-space.""" + basis = [] + for row in rows: + v = list(row) + for p, b in basis: + if v[p]: + g, f = b[p], v[p] + v = [g * x - f * y for x, y in zip(v, b)] + content = 0 + for x in v: + content = gcd(content, x) + if content > 1: + v = [x // content for x in v] + pivot = next((i for i, x in enumerate(v) if x), None) + if pivot is not None: + if v[pivot] < 0: + v = [-x for x in v] + basis.append((pivot, v)) + return [v for _, v in basis] + + +def rank_f2(rows): + pivots = {} + for x in rows: + while x: + p = x.bit_length() - 1 + if p in pivots: + x ^= pivots[p] + else: + pivots[p] = x + break + return len(pivots) + + +def inverse_f2(rows, n): + augmented = [row | (1 << (n + i)) for i, row in enumerate(rows)] + for j in range(n): + pivot = next((i for i in range(j, n) if (augmented[i] >> j) & 1), None) + require(pivot is not None, "singular binary matrix") + augmented[j], augmented[pivot] = augmented[pivot], augmented[j] + for i in range(n): + if i != j and (augmented[i] >> j) & 1: + augmented[i] ^= augmented[j] + require([r & ((1 << n) - 1) for r in augmented] == [1 << i for i in range(n)], + "bad inverse") + return [r >> n for r in augmented] + + +def pairing_rows(lines): + out = [] + for r in lines: + require(all(dot(r, s) % 2 == 0 for s in lines), "nonintegral Gram") + out.append(sum(((1 + dot(r, s) // 2) % 2) << j for j, s in enumerate(lines))) + return out + + +class Instance: + def __init__(self, name): + require(name in PUNCTURES, "unknown fixture") + self.name = name + self.lines = roots() + self.punctures = PUNCTURES[name] + self.live = [i for i in range(120) if i not in self.punctures] + full_pairing = pairing_rows(self.lines) + self.B = [sum(((full_pairing[i] >> j) & 1) << a + for a, j in enumerate(self.punctures)) for i in self.punctures] + self.target = inverse_f2(self.B, 9) + self.labels = [sum(((full_pairing[i] >> j) & 1) << a + for a, j in enumerate(self.punctures)) for i in self.live] + require(rank_f2(self.labels) == 9, "live labels do not span") + self.readers = {} + self.bases = {} + for x in range(1, 512): + indices = [i for i, r in zip(self.live, self.labels) if parity(r & x)] + self.readers[x] = indices + self.bases[x] = row_basis_q(self.lines[i] for i in indices) + deficient = [x for x, basis in self.bases.items() if len(basis) < 8] + require(deficient == [1 << i for i in range(9)], "unexpected deficient functionals") + for i, p in enumerate(self.punctures): + require(len(self.bases[1 << i]) == 7, "bad hyperplane dimension") + require(all(dot(r, self.lines[p]) == 0 for r in self.bases[1 << i]), + "bad hyperplane normal") + + def cost(self, x, y): + require(type(x) is int and type(y) is int and 0 < x < 512 and 0 < y < 512, + "terms must contain two nonzero 9-bit integers") + ux, uy = x & (x - 1) == 0, y & (y - 1) == 0 + if not ux and not uy: + return 8 + if not (ux and uy): + return 7 + i, j = x.bit_length() - 1, y.bit_length() - 1 + return 6 if dot(self.lines[self.punctures[i]], self.lines[self.punctures[j]]) == 0 else 7 + + def direct_cost(self, x, y): + a, b = self.bases[x], self.bases[y] + return len(row_basis_q([[dot(r, s) for s in b] for r in a])) + + def baseline(self): + return [[1 << i, row] for i, row in enumerate(self.target)] + + def evaluate(self, terms): + require(isinstance(terms, list) and 1 <= len(terms) <= 20, "bad term count") + rows = [0] * 9 + costs = [] + for term in terms: + require(isinstance(term, list) and len(term) == 2, "bad term") + x, y = term + costs.append(self.cost(x, y)) + for i in range(9): + if (x >> i) & 1: + rows[i] ^= y + require(rows == self.target, "rank-one sum fails target identity") + return {"instance": self.name, "cost": sum(costs), "term_costs": costs, + "terms": len(terms), "valid": True} diff --git a/research/p111-copy-rank-certificate/roots.json b/research/p111-copy-rank-certificate/roots.json new file mode 100644 index 0000000000..9fd083d700 --- /dev/null +++ b/research/p111-copy-rank-certificate/roots.json @@ -0,0 +1,1205 @@ +{ + "source": "research/e8-bit-r420/data/bitE8mut-r420.json.gz", + "lines": [ + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + [ + 0, + 1, + 1, + 0, + 1, + 0, + 0, + 1 + ], + [ + 0, + 1, + 1, + 0, + 1, + 0, + 0, + -1 + ], + [ + 0, + 1, + 1, + 0, + -1, + 0, + 0, + 1 + ], + [ + 0, + 1, + 1, + 0, + -1, + 0, + 0, + -1 + ], + [ + 0, + 1, + -1, + 0, + 1, + 0, + 0, + 1 + ], + [ + 0, + 1, + -1, + 0, + 1, + 0, + 0, + -1 + ], + [ + 0, + 1, + -1, + 0, + -1, + 0, + 0, + 1 + ], + [ + 0, + 1, + -1, + 0, + -1, + 0, + 0, + -1 + ], + [ + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + [ + 1, + 0, + 1, + 0, + 1, + 0, + -1, + 0 + ], + [ + 1, + 0, + 1, + 0, + -1, + 0, + 1, + 0 + ], + [ + 1, + 0, + 1, + 0, + -1, + 0, + -1, + 0 + ], + [ + 1, + 0, + -1, + 0, + 1, + 0, + 1, + 0 + ], + [ + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0 + ], + [ + 1, + 0, + -1, + 0, + -1, + 0, + 1, + 0 + ], + [ + 1, + 0, + -1, + 0, + -1, + 0, + -1, + 0 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 1 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + -1, + 1 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + -1, + -1 + ], + [ + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1 + ], + [ + 1, + -1, + 0, + 0, + 0, + 0, + 1, + -1 + ], + [ + 1, + -1, + 0, + 0, + 0, + 0, + -1, + 1 + ], + [ + 1, + -1, + 0, + 0, + 0, + 0, + -1, + -1 + ], + [ + 1, + 1, + 0, + 0, + 1, + 1, + 0, + 0 + ], + [ + 1, + 1, + 0, + 0, + 1, + -1, + 0, + 0 + ], + [ + 1, + 1, + 0, + 0, + -1, + 1, + 0, + 0 + ], + [ + 1, + 1, + 0, + 0, + -1, + -1, + 0, + 0 + ], + [ + 1, + -1, + 0, + 0, + 1, + 1, + 0, + 0 + ], + [ + 1, + -1, + 0, + 0, + 1, + -1, + 0, + 0 + ], + [ + 1, + -1, + 0, + 0, + -1, + 1, + 0, + 0 + ], + [ + 1, + -1, + 0, + 0, + -1, + -1, + 0, + 0 + ], + [ + 1, + 0, + 1, + 0, + 0, + 1, + 0, + 1 + ], + [ + 1, + 0, + 1, + 0, + 0, + 1, + 0, + -1 + ], + [ + 1, + 0, + 1, + 0, + 0, + -1, + 0, + 1 + ], + [ + 1, + 0, + 1, + 0, + 0, + -1, + 0, + -1 + ], + [ + 1, + 0, + -1, + 0, + 0, + 1, + 0, + 1 + ], + [ + 1, + 0, + -1, + 0, + 0, + 1, + 0, + -1 + ], + [ + 1, + 0, + -1, + 0, + 0, + -1, + 0, + 1 + ], + [ + 1, + 0, + -1, + 0, + 0, + -1, + 0, + -1 + ], + [ + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 0 + ], + [ + 0, + 1, + 1, + 0, + 0, + 1, + -1, + 0 + ], + [ + 0, + 1, + 1, + 0, + 0, + -1, + 1, + 0 + ], + [ + 0, + 1, + 1, + 0, + 0, + -1, + -1, + 0 + ], + [ + 0, + 1, + -1, + 0, + 0, + 1, + 1, + 0 + ], + [ + 0, + 1, + -1, + 0, + 0, + 1, + -1, + 0 + ], + [ + 0, + 1, + -1, + 0, + 0, + -1, + 1, + 0 + ], + [ + 0, + 1, + -1, + 0, + 0, + -1, + -1, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + -1, + 1 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + -1, + -1 + ], + [ + 0, + 0, + 0, + 0, + 1, + -1, + 1, + 1 + ], + [ + 0, + 0, + 0, + 0, + 1, + -1, + 1, + -1 + ], + [ + 0, + 0, + 0, + 0, + 1, + -1, + -1, + 1 + ], + [ + 0, + 0, + 0, + 0, + 1, + -1, + -1, + -1 + ], + [ + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + -1, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + -1, + 1, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + -1, + -1, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + 1, + 1, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + 1, + -1, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + 1, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1 + ], + [ + 1, + 0, + 0, + 1, + 1, + 0, + 0, + -1 + ], + [ + 1, + 0, + 0, + 1, + -1, + 0, + 0, + 1 + ], + [ + 1, + 0, + 0, + 1, + -1, + 0, + 0, + -1 + ], + [ + 1, + 0, + 0, + -1, + 1, + 0, + 0, + 1 + ], + [ + 1, + 0, + 0, + -1, + 1, + 0, + 0, + -1 + ], + [ + 1, + 0, + 0, + -1, + -1, + 0, + 0, + 1 + ], + [ + 1, + 0, + 0, + -1, + -1, + 0, + 0, + -1 + ], + [ + 0, + 1, + 0, + 1, + 1, + 0, + 1, + 0 + ], + [ + 0, + 1, + 0, + 1, + 1, + 0, + -1, + 0 + ], + [ + 0, + 1, + 0, + 1, + -1, + 0, + 1, + 0 + ], + [ + 0, + 1, + 0, + 1, + -1, + 0, + -1, + 0 + ], + [ + 0, + 1, + 0, + -1, + 1, + 0, + 1, + 0 + ], + [ + 0, + 1, + 0, + -1, + 1, + 0, + -1, + 0 + ], + [ + 0, + 1, + 0, + -1, + -1, + 0, + 1, + 0 + ], + [ + 0, + 1, + 0, + -1, + -1, + 0, + -1, + 0 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + -1, + 1 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + -1, + -1 + ], + [ + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 1 + ], + [ + 0, + 0, + 1, + -1, + 0, + 0, + 1, + -1 + ], + [ + 0, + 0, + 1, + -1, + 0, + 0, + -1, + 1 + ], + [ + 0, + 0, + 1, + -1, + 0, + 0, + -1, + -1 + ], + [ + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0 + ], + [ + 0, + 0, + 1, + 1, + 1, + -1, + 0, + 0 + ], + [ + 0, + 0, + 1, + 1, + -1, + 1, + 0, + 0 + ], + [ + 0, + 0, + 1, + 1, + -1, + -1, + 0, + 0 + ], + [ + 0, + 0, + 1, + -1, + 1, + 1, + 0, + 0 + ], + [ + 0, + 0, + 1, + -1, + 1, + -1, + 0, + 0 + ], + [ + 0, + 0, + 1, + -1, + -1, + 1, + 0, + 0 + ], + [ + 0, + 0, + 1, + -1, + -1, + -1, + 0, + 0 + ], + [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1 + ], + [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + -1 + ], + [ + 0, + 1, + 0, + 1, + 0, + -1, + 0, + 1 + ], + [ + 0, + 1, + 0, + 1, + 0, + -1, + 0, + -1 + ], + [ + 0, + 1, + 0, + -1, + 0, + 1, + 0, + 1 + ], + [ + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1 + ], + [ + 0, + 1, + 0, + -1, + 0, + -1, + 0, + 1 + ], + [ + 0, + 1, + 0, + -1, + 0, + -1, + 0, + -1 + ], + [ + 1, + 0, + 0, + 1, + 0, + 1, + 1, + 0 + ], + [ + 1, + 0, + 0, + 1, + 0, + 1, + -1, + 0 + ], + [ + 1, + 0, + 0, + 1, + 0, + -1, + 1, + 0 + ], + [ + 1, + 0, + 0, + 1, + 0, + -1, + -1, + 0 + ], + [ + 1, + 0, + 0, + -1, + 0, + 1, + 1, + 0 + ], + [ + 1, + 0, + 0, + -1, + 0, + 1, + -1, + 0 + ], + [ + 1, + 0, + 0, + -1, + 0, + -1, + 1, + 0 + ], + [ + 1, + 0, + 0, + -1, + 0, + -1, + -1, + 0 + ] + ] +} diff --git a/research/p111-copy-rank-certificate/verify.py b/research/p111-copy-rank-certificate/verify.py new file mode 100644 index 0000000000..334ea4c98f --- /dev/null +++ b/research/p111-copy-rank-certificate/verify.py @@ -0,0 +1,296 @@ +"""Exact premise checks and independent certificates for PROOF.md (stdlib). + +No SAT solver, numerical rank routine, or upstream implementation is imported. +The written proof covers arbitrary lengths; this program verifies its finite +geometric premises and independently excludes the only ten-term threat. +""" +import argparse +import copy +from collections import Counter +from fractions import Fraction +import gzip +import hashlib +from itertools import combinations, product +import json +from pathlib import Path + +from exact import Instance, dot, generated_root_set, inverse_f2, parity, rank_f2, require + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] +WORDS = { + "pr545": "research/e8-punctured111-star/data/bitE8mut-v111-r489.json.gz", + "pr555": "research/e8-bit-p111/data/bitE8mut-p111.json.gz", +} + + +def fraction_basis(rows): + """Gaussian elimination with explicit rational division, separate from exact.py.""" + echelon = {} + for row in rows: + row = list(map(Fraction, row)) + for pivot in sorted(echelon): + scale = row[pivot] + if scale: + row = [x - scale * y for x, y in zip(row, echelon[pivot])] + p = next((i for i, x in enumerate(row) if x), None) + if p is not None: + scale = row[p] + echelon[p] = [x / scale for x in row] + return list(echelon.values()) + + +def decoder_entries(instance): + """Compare reconstructed and geometric decoder on every live ordered pair.""" + count = 0 + for t, r in zip(instance.live, instance.labels): + for s, q in zip(instance.live, instance.labels): + rq = 0 + for j, row in enumerate(instance.target): + rq |= parity(row & q) << j + actual = parity(r & rq) + want = (1 + dot(instance.lines[t], instance.lines[s]) // 2) % 2 + require(actual == want, "live decoder entry mismatch") + count += 1 + return count + + +def geometry(instance): + full_word = json.loads(gzip.decompress((REPO / "research/e8-bit-r420/data/bitE8mut-r420.json.gz").read_bytes())) + require(full_word["lines"] == [list(r) for r in instance.lines], "full root ordering/source mismatch") + word = json.loads(gzip.decompress((REPO / WORDS[instance.name]).read_bytes())) + require(word["punctured"] == instance.punctures, "puncture/source mismatch") + require(word["ports_geom"] == instance.live, "live/source mismatch") + require(word["lines"] == [list(instance.lines[i]) for i in instance.live], + "root numbering/source mismatch") + require(all((row >> i) & 1 for i, row in enumerate(instance.B)), "missing unit diagonal") + require(all(((instance.B[i] >> j) & 1) == ((instance.B[j] >> i) & 1) + for i in range(9) for j in range(9)), "nonsymmetric puncture Gram") + independent = {} + for x in range(1, 512): + # Derive support directly from root inner products, without labels. + support = [] + for v in instance.live: + bit = sum(((1 + dot(instance.lines[v], instance.lines[p]) // 2) % 2) + for j, p in enumerate(instance.punctures) if (x >> j) & 1) % 2 + if bit: + support.append(v) + require(support == instance.readers[x], "reader support mismatch") + independent[x] = fraction_basis(instance.lines[v] for v in support) + unit = x & (x - 1) == 0 + require(len(independent[x]) == (7 if unit else 8), "rational span mismatch") + if unit: + normal = instance.lines[instance.punctures[x.bit_length() - 1]] + require(all(dot(v, normal) == 0 for v in independent[x]), "wrong normal") + + # Nine deficient hyperplanes and the full space: complete span-class cover. + representatives = [1 << i for i in range(9)] + [3] + for x, y in product(representatives, repeat=2): + block = [[dot(r, s) for s in independent[y]] for r in independent[x]] + require(len(fraction_basis(block)) == instance.cost(x, y), "copy-rank mismatch") + costs = Counter(instance.cost(x, y) for x in range(1, 512) for y in range(1, 512)) + return { + "reader_spans": 511, + "span_dimensions": {"7": 9, "8": 502}, + "ordered_span_class_pairs": 100, + "ordered_nonzero_pairs_covered": 511 ** 2, + "pair_cost_histogram": {str(k): v for k, v in sorted(costs.items())}, + "live_decoder_entries": decoder_entries(instance), + "punctures": instance.punctures, + "binary_puncture_gram_rows": instance.B, + "target_inverse_rows": instance.target, + } + + +def minor_rank(rows, row_indices, column_indices): + sub = [sum(((rows[r] >> c) & 1) << j for j, c in enumerate(column_indices)) + for r in row_indices] + return rank_f2(sub), sub + + +def ten_term_minor(instance): + """A second, finite obstruction, independent of the projection proof. + +Find a rank-three target minor on which every cost-six unit cell vanishes. +Then at least three noncheap terms are needed; cost <=62 at n=10 permits +at most two. This check proves infeasibility below63, not the stronger >=64. +""" + for rows in combinations(range(9), 3): + for columns in combinations(range(9), 3): + if any(instance.cost(1 << r, 1 << c) == 6 for r in rows for c in columns): + continue + rank, minor = minor_rank(instance.target, rows, columns) + if rank == 3: + return {"rows": list(rows), "columns": list(columns), + "minor_rows_binary": minor, "rank": 3, + "cost6_cells_on_minor": 0} + raise ValueError("no independent ten-term minor certificate") + + +def binary_matvec(columns, bits): + out = 0 + for i, c in enumerate(columns): + if (bits >> i) & 1: + out ^= c + return out + + +def small_projection_checks(): + """Exhaust all nonsingular symmetric unit-diagonal 3x3 B and all + nonzero 3x3/3x4 factorizations B^-1=XY^t. Tests the proof mechanism, + not a substitute for the dimension-nine argument. + """ + dimension = 3 + count = {3: 0, 4: 0} + matrices = 0 + for mask in range(8): + B = [1 << i for i in range(3)] + for bit, (i, j) in enumerate(combinations(range(3), 2)): + if (mask >> bit) & 1: + B[i] |= 1 << j + B[j] |= 1 << i + if rank_f2(B) != 3: + continue + matrices += 1 + target = inverse_f2(B, 3) + for n in (3, 4): + for X in product(range(1, 8), repeat=n): + if rank_f2(X) != 3: + continue + preimages = [[] for _ in range(8)] + for z in range(1 << n): + preimages[binary_matvec(X, z)].append(z) + # target is symmetric, so its rows are also its columns. + for zcols in product(*(preimages[t] for t in target)): + Y = [sum(((zcols[j] >> i) & 1) << j for j in range(3)) for i in range(n)] + if not all(Y): + continue + count[n] += 1 + unitX = {x for x in X if x & (x - 1) == 0} + unitY = {y for y in Y if y & (y - 1) == 0} + K = [] + for y in Y: + row = 0 + for j, x in enumerate(X): + bx = sum(parity(b & x) << a for a, b in enumerate(B)) + row |= parity(y & bx) << j + K.append(row) + if n == 3: + require(K == [1 << i for i in range(n)], "biorthogonality failed") + same = sum(x == y and x & (x - 1) == 0 for x, y in zip(X, Y)) + require(len(unitX & unitY) == same, "unit-intersection lemma failed") + else: + require(rank_f2([r ^ (1 << i) for i, r in enumerate(K)]) == 1, + "rank-one projection complement failed") + cheap = [i for i, (x, y) in enumerate(zip(X, Y)) + if x in unitX and y in unitY and x != y and (K[i] >> i) & 1] + k = len(cheap) + require(k <= (2 * dimension) // 3, "cheap-term projection bound failed") + rank, _ = minor_rank(K, cheap, cheap) + require(rank == k, "cheap principal minor singular") + return {"dimension": 3, "binary_gram_matrices": matrices, + "square_factorizations": count[3], "one_extra_term_factorizations": count[4]} + + +def rejected(fn): + try: + fn() + except (ValueError, TypeError, IndexError): + return + raise ValueError("negative control was not rejected") + + +def negative_controls(instance): + baseline = instance.baseline() + wrong = copy.deepcopy(baseline) + wrong[0][1] ^= 1 + rejected(lambda: instance.evaluate(wrong)) + rejected(lambda: instance.evaluate(baseline[:-1])) + wrong = copy.deepcopy(baseline) + wrong[0][0] = 0 + rejected(lambda: instance.evaluate(wrong)) + wrong = copy.deepcopy(baseline) + wrong[0][0] = True + rejected(lambda: instance.evaluate(wrong)) + bad = copy.deepcopy(instance) + bad.target[0] ^= 1 + rejected(lambda: decoder_entries(bad)) + bad = copy.deepcopy(instance) + bad.labels[0] ^= 1 + rejected(lambda: decoder_entries(bad)) + bad = copy.deepcopy(instance) + bad.lines = generated_root_set() + rejected(lambda: geometry(bad)) + # A false unit-pair discount must disagree with direct rational rank. + rejected(lambda: require(instance.direct_cost(1, 1) == 6, "false discount")) + # Without unit diagonal, the endpoint-count lemma really is false: + # B=[[0,1],[1,0]], X=I, Y=B yields biorthogonality but four distinct + # endpoint occurrences across two coordinates and no same-term match. + B = [2, 1] + require(inverse_f2(B, 2) == B, "control inverse") + X, Y = [1, 2], [2, 1] + require(sum(x == y for x, y in zip(X, Y)) == 0 and len(set(X) & set(Y)) == 2, + "diagonal-premise counterexample lost") + rejected(lambda: require(all((r >> i) & 1 for i, r in enumerate(B)), "missing diagonal premise")) + return ["wrong_coefficient", "missing_total", "zero_factor", "boolean_factor", + "corrupted_target", "corrupted_live_label", "wrong_root_order", "false_copy_discount", "missing_unit_diagonal"] + + +def source_pins(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for name, expected in sources["files"].items(): + actual = hashlib.sha256((REPO / name).read_bytes()).hexdigest() + require(actual == expected, "source pin mismatch: " + name) + return len(sources["files"]) + + +def run(): + pins = source_pins() + results = {} + for name in ("pr545", "pr555"): + instance = Instance(name) + row = geometry(instance) + witness = json.loads((HERE / ("baseline-" + name + ".json")).read_text()) + require(witness["instance"] == name, "witness fixture mismatch") + row["attainment"] = instance.evaluate(witness["terms"]) + require(row["attainment"]["cost"] == 63, "baseline cost changed") + row["independent_ten_term_minor"] = ten_term_minor(instance) + row["negative_controls"] = negative_controls(instance) + results[name] = row + old = generated_root_set() + actual = Instance("pr545").lines + permutation = [actual.index(r) for r in old] + ordering = {"first_mismatch": {"index": 8, "archived_root": list(old[8]), "supplier_root": list(actual[8])}, + "same_signed_root_set": set(old) == set(actual), + "archived_to_supplier_permutation": permutation, + "mapped_archived_punctures": {name: sorted(permutation[i] for i in row["punctures"]) + for name, row in results.items()}} + require(ordering == json.loads((HERE / "ORDERING.json").read_text()), "root ordering receipt mismatch") + return { + "format": "p111-copy-rank-certificate-v1", + "source_pins_checked": pins, + "root_ordering_checked": True, + "fixtures": results, + "small_projection_checks": small_projection_checks(), + "proved_bounds_by_term_count": {"n_lt_9": "rank obstruction", + "n_eq_9": 63, "n_eq_10": 64, "n_ge_11": "6*n >= 66"}, + "optimum": 63, + "scope": "Written algebraic proof plus exact finite premise checks; no new kappa or full supplier proof", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path) + parser.add_argument("--check", type=Path) + args = parser.parse_args() + result = run() + if args.check: + require(json.loads(args.check.read_text()) == result, "receipt mismatch") + if args.write: + args.write.write_text(json.dumps(result, sort_keys=True, indent=2) + "\n") + print("PASS_P111_COPY_RANK: optimum 63 on two fixtures; exact geometry, independent minors, 18 negative controls") + + +if __name__ == "__main__": + main()