diff --git a/research/selected-bit-qadic-route/README.md b/research/selected-bit-qadic-route/README.md new file mode 100644 index 0000000000..1b897f839c --- /dev/null +++ b/research/selected-bit-qadic-route/README.md @@ -0,0 +1,258 @@ +# One selected BIT route with explicit q-adic carries + +This package lowers one nontrivial selected BIT port route into exact low/high +row-field updates. The written identity holds at every atom width. Its executable +receipt contains 77 elementary column factors, 4,928 row-field steps per route, +and 24 comparisons with a separate dense modular oracle. Ancestors, the physical +role slot, unused descendant stock, and head/data spectators remain unchanged. + +This is a row-index implementation of one missing interface, not the full GL64 +compiler, a physical routing implementation, a stock-bound improvement, or a new +kappa. The selected frontier and all predecessor files remain unchanged. + +## Scope and predecessors + +The scientific base is main `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority +revision 4. The selected record binds PR1094's assembly, which cites the exact +PR589 BIT receipt by Git blob. That receipt binds the tuned P111 word. Its live +port 8 is original E8 port 8 with root `[0,1,1,0,1,0,0,1]`. The ambient dimension +is 64. The complex supplier's dimension 73 is not substituted into this argument. + +This takes the released field-split handoff from +[PR2120](https://github.com/CrocSwap/integer-mult-bounds/pull/2120), head +`378593574261e0b0915e7e8a83147aa640274fc8`, and +[Discussion 2114](https://github.com/CrocSwap/integer-mult-bounds/discussions/2114). +Adam Gall's [PR2084](https://github.com/CrocSwap/integer-mult-bounds/pull/2084), +head `8001a23b003bec5dff5e61edec907b652c475932`, supplies the conditional BIT +packet/restoration implication. [PR2097](https://github.com/CrocSwap/integer-mult-bounds/pull/2097), +head `1d3ee0926656d5260c6cb1c0b81964ffe9fe1377`, proves fresh-fiber counting +under a field-dependency contract and leaves its selected lowering open. +Those results are credited, not claimed as new here. None of their verifiers +is imported or executed, and none of their packages is vendored. + +The task's scope changes from computing a reserve coefficient to this concrete +implementation obligation. The existing notes already state affine chart routing +and fresh fields. The new artifact emits the low/high carry program for an exact +selected rational route, proves its integer formula, and checks its factor order, +field isolation and inverse. It does not claim that affine routing itself is new. +See [TASK.json](TASK.json) for the selection override and limits of live overlap. +No Discussion claim was posted because the local engineering workflow prohibits +human-directed posts. The public artifact is the contribution PR. + +## Source-bound rational route + +The pinned `code/nine/geometry.py` constructs an isometry `g` taking the first +root to the port root up to sign, using its fixed breadth-first reflection rule. +With `q_port` the root, it sets + +``` +P = q_port*q_port^t / 4 +A = g[:,1:] +rho = [[P, A], [A^t, 0_7]] +``` + +The retained PR545 adapter builds this geometry over all 120 original roots, +then selects and reindexes the 111 live ports. This checker independently +reconstructs that rule with rational arithmetic and emits only port 8. It checks +`rho^t=rho`, `rho^2=I_15`, and the exact elementary product. The route acts on +axes `0..7` plus one exterior seven-block. The receipt checks both stage 1, +axes `8..14`, and stage 8, axes `57..63`. Other columns remain fixed. + +Gaussian row elimination gives `E_k ... E_1 rho = I`. Thus right multiplication +by `rho` executes the column factors `E_1^-1, ..., E_k^-1` in that order. +A row operation adding `c` times row j to row i becomes a right-action column +operation adding `-c` times column i to column j. All 77 factors are checked +against the rational matrix; deleting any single factor changes the product. +A separate noncommuting fixture tests column orientation and order, since the +selected route's symmetry could otherwise hide a transpose error. + +There are 63 column additions, seven swaps and seven scalings. Each operates +on 64 matrix rows. The 4,928 count is row-field instructions, not scalar writes, +recursive children, measured runtime, or a paid physical invoice. The only +coefficient numerators and denominators have prime factor 2. Every odd radix +therefore makes the factors invertible. For the full-cover interpretation, +retain the source's stronger eligible-prime conditions. + +## Exact all-width carry lemma + +Let q be an integer at least two, w at least one, and `Q=q^(w-1)`. Write two +current matrix entries uniquely as + +``` +x = x0 + q*X, y = y0 + q*Y, +0 <= x0,y0 < q, 0 <= X,Y < Q. +``` + +For a rational coefficient `a/d` with `d>0` coprime to q, the elementary +addition `y <- y + (a/d)*x` modulo `q^w` has the following exact lowering: + +``` +t = ((d*y0 + a*x0) * inverse(d,q)) mod q +c = (d*y0 + a*x0 - d*t) / q +Y_new = ((d*Y + a*X + c) * inverse(d,Q)) mod Q +(y0_new, Y_new) = (t, Y_new) +``` + +The numerator defining c is divisible by q by the definition of t. In integers, + +``` +d*y + a*x = d*t + q*(d*Y + a*X + c). +``` + +Reducing modulo `q^w` and multiplying by the inverse of d proves the result. +This permits negative carries. For example, adding half of 1 to 0 at q=5, +w=2 gives `(t,c,Y_new)=(3,-1,2)`, hence entry 13 modulo 25. Omitting the carry +would give 3 and is wrong. + +For scaling `y <- (a/d)*y`, replace the two numerators by `a*y0` and `a*Y`. +Require a coprime to q as well to make scaling a permutation. Swapping entries +swaps both their low and high fields. At w=1 the high field has one value, 0; +the high congruence modulo one is vacuous. These derivations require no bound +on w and no floating-point approximation. + +Each factor is an invertible map on every matrix over `Z/q^w Z`. Composing the +emitted factors therefore gives exactly `G <- G*rho` for all such matrices, +and in particular permutes the invertible ones. Low reduction depends only on +the current low matrix. For each fixed low matrix, the high update is affine +and bijective onto the complete high fiber over the new low matrix. Thus the +route preserves all `q^(4096*(w-1))` high completions; it does not silently drop +the high fibers charged by the stock proofs. + +### Why low routing and row restoration do not suffice + +A concrete carry-omission mutant applies the rational route separately modulo +5 to the low matrix and to the high matrix, then rejoins them. At w=2 it has +the correct low routing, fixes all other fields, and restores the entire row +after two applications because `rho^2=I` in each separate factor. Nevertheless +it is not right multiplication modulo 25. For the receipt's stage-8 invertible +fixture, matrix entry `[0,6]` is 19 instead of 14. Both reduce to 4 modulo 5. +The active input row is retained in the receipt. + +This is a counterexample to those checks being sufficient, not a defect found +in the selected compiler. No selected all-size q-adic compiler was executed. +It explains the need for a full-width oracle in this contribution. + +## Parent/child field boundary + +Consider a complete row represented as + +``` +(ancestor_fields, role_slot, current_low, current_high, unused_child_stock, + head_data, other_spectators). +``` + +The emitted operation reads and writes only the current low/high matrices. +Its program and coefficients are fixed by the selected port and stage, not by +unused child stock or head/data values. Consequently it is the identity on +every other factor of this product, for arbitrary initial values of those +factors. Its inverse restores the entire original row, not merely its low +residue. Changing another factor cannot change the current route's result. + +If unused stock is a complete range divisible by the next role-packet divisor, +Euclidean quotient/remainder splitting still supplies all next-role values +with equal multiplicity after this route. At a child boundary, the exposed +parent fields may become ancestors without changing the unused range. This +is the local field-preservation implication needed by the handoff. Complete +invocation domains, ancestor-only child weights, every other owner route and +restoration of a completed child still need their own certificates. This +single routing identity does not establish those assumptions by itself. + +The selected finite program describes orthogonal cover classes. Transferring +its complete physical recipe to the local-ring GL64 full cover remains the +explicit inherited realization assumption in PR2084/2097/2120. The present +matrix identity works over GL64, but does not prove that transfer, common-label +or mutable-source realization, or fixed-tape physical hosting. + +## Reproduction and failure controls + +Standard-library Python 3.12, from the repository root: + +``` +python3.12 -I -B research/selected-bit-qadic-route/verify.py +python3.12 -I -O -B research/selected-bit-qadic-route/test_route.py +python3.12 scripts/research_package.py --package research/selected-bit-qadic-route +``` + +Expected output includes: + +``` +PASS_SELECTED_BIT_QADIC_ROUTE factors=77 cases=24 no_new_kappa +Ran 11 tests +OK +``` + +Every live input is authenticated before semantic use. The registered metadata +check authenticates the historical selected record at the pinned base; the +verifier links its frozen PR1094 assembly citation, tuned receipt and word. +The moving selected pointer is provenance, not a live replay input. A later +frontier change does not silently change this scientific baseline. +Predecessor Python is read as pinned source, never executed. The regenerated +receipt must equal the committed [RESULT.json](RESULT.json); missing or corrupt +receipts fail. `--write-result PATH` is explicit and refuses to overwrite files. + +The route cases use dense invertible `L*U` matrices at q=5, 7 and `2^89-1`, +widths 1, 2, 3 and 8, in both exterior-block embeddings. A direct dense modular +right product is the oracle; it does not use the carry interpreter or elementary +program. Exact inverse replay restores all fields. These finite cases do not +prove the all-width lemma, which is the integer identity above. No eligible +selected-prime inference follows merely from testing a large prime. + +Eleven test groups include the carry-omission mutant, 1,493 exhaustive +elementary-addition cases, scaling bijections, signed carry fixtures, +noncommuting order, inactive columns, +arbitrary spectators, wrong selected citations, all eight external input +corruptions, and optimized public-CLI missing/corrupt-receipt and no-overwrite +controls. Acceptance uses explicit exceptions, not removable assertions. + +## Implementation and verification limits + +The executable is a bounded research checker. Its public carry evaluator caps +w at 16, q below `2^127`, and rational coefficient components at 16 bits. +The proof has no such width bound. Matrices are at most 64 by 64, +local rational matrices are 15 by 15, programs have at +most 240 factors, and the source BFS has at most 120 rounds over 120 roots. +Inputs and decompressed words are capped at 8 MiB. Each subprocess test has a +15-second timeout. All loops have finite collection or numeric bounds; there +is no recursion or background work. + +Power-of-Ten deviations concern Python managed allocation and unittest/import +dispatch. Runtime arithmetic and collections allocate dynamically; dimensions, +widths, file caps and bounded fixture counts constrain their live size. The +fixed local imports are the only added module targets, and tests exercise both +normal and optimized entry points. Syntax compilation and warnings-as-errors +are the available diagnostics. A native fixed-capacity implementation and +physical interpreter remain follow-ups if this is used outside a research +checker. No repository-wide lint or compiler configuration is changed. + +No full selected cold replay, physical routing benchmark, native compiler, +formal-kernel proof, independent human review, or new stock coefficient is +claimed. Scalar gates, owner/slot permutations, weighted children, ordinary +leaf borrowing, all-size physical lowering, precision/tapes, recovery and outer +analytic obligations remain outside this package. + +## Open next questions + +1. Can every selected helper/bank/hosted route and child-weight descriptor + satisfy the same field-dependency contract? Begin with one residual-isometry + route and emit its ancestor-only reads. This matters because a single data + route cannot establish the full fresh-field premise. The all-size compiler + and complete invocation domains remain blockers. +2. Can these field operations be physically implemented with the retained + ordered-affine and completed ordinary-leaf costs? Begin with one + carry-controlled shift or scaling, including preserved spectators and its actual + ordinary-call bill. Exact row-index arithmetic does not discharge fixed-tape, + hosting, internal borrowing or precision obligations. + +## Credit + +The rational port geometry and reflection construction are retained from +Zhihao Chen's PR386 and its credited PR370 lineage. DreamingOfClouds supplied +PR545's live-port adapter and the selected PR589 tuned BIT pipeline on eumemic's +base. Rohan Arun supplied the selected PR1094 assembly on Jeremy Kothe's PR1087 +predecessor and the retained completed-row contracts. Adam Gall's PR2084 and +PR2097, Nick Petalas's PR2120, Josie Elliston's PR1956/1965 and ToikY's PR1990 +identify the stock and field obligations used here. Their constructions, +conditional envelopes and numerical receipts are not claimed as new. + +Nick Petalas retains authorship and responsibility for this scoped lowering +and checker. Apache-2.0, following the repository license. diff --git a/research/selected-bit-qadic-route/RESULT.json b/research/selected-bit-qadic-route/RESULT.json new file mode 100644 index 0000000000..1af61d1e59 --- /dev/null +++ b/research/selected-bit-qadic-route/RESULT.json @@ -0,0 +1,934 @@ +{ + "status": "PASS_SELECTED_BIT_QADIC_ROUTE", + "selected_port": 8, + "original_port": 8, + "ambient_dimension": 64, + "local_dimension": 15, + "root": [ + 0, + 1, + 1, + 0, + 1, + 0, + 0, + 1 + ], + "matrix": [ + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/2", + "1/2", + "0", + "1/2", + "0", + "0", + "1/2" + ], + [ + "0", + "1/4", + "1/4", + "0", + "1/4", + "0", + "0", + "1/4", + "1/2", + "0", + "0", + "0", + "0", + "1/2", + "-1/2" + ], + [ + "0", + "1/4", + "1/4", + "0", + "1/4", + "0", + "0", + "1/4", + "0", + "1/2", + "0", + "-1/2", + "0", + "-1/2", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1/4", + "1/4", + "0", + "1/4", + "0", + "0", + "1/4", + "0", + "-1/2", + "0", + "1/2", + "0", + "-1/2", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/2", + "-1/2", + "0", + "-1/2", + "0", + "0", + "1/2" + ], + [ + "0", + "1/4", + "1/4", + "0", + "1/4", + "0", + "0", + "1/4", + "-1/2", + "0", + "0", + "0", + "0", + "1/2", + "1/2" + ], + [ + "1/2", + "1/2", + "0", + "0", + "0", + "0", + "1/2", + "-1/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1/2", + "0", + "1/2", + "0", + "-1/2", + "0", + "-1/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1/2", + "0", + "-1/2", + "0", + "1/2", + "0", + "-1/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1/2", + "-1/2", + "0", + "-1/2", + "0", + "0", + "1/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1/2", + "-1/2", + "0", + "0", + "0", + "0", + "1/2", + "1/2", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ], + "column_program": [ + [ + "swap", + 8, + 0, + "1" + ], + [ + "scale", + 0, + 0, + "1/2" + ], + [ + "add", + 0, + 9, + "1/2" + ], + [ + "add", + 0, + 11, + "1/2" + ], + [ + "add", + 0, + 14, + "1/2" + ], + [ + "scale", + 1, + 1, + "1/4" + ], + [ + "add", + 1, + 0, + "1" + ], + [ + "add", + 1, + 2, + "1/4" + ], + [ + "add", + 1, + 4, + "1/4" + ], + [ + "add", + 1, + 7, + "1/4" + ], + [ + "add", + 1, + 9, + "-1/2" + ], + [ + "add", + 1, + 11, + "-1/2" + ], + [ + "add", + 1, + 13, + "1/2" + ], + [ + "add", + 1, + 14, + "-1" + ], + [ + "swap", + 9, + 2, + "1" + ], + [ + "add", + 2, + 0, + "-1" + ], + [ + "add", + 2, + 1, + "1" + ], + [ + "add", + 2, + 13, + "-1" + ], + [ + "add", + 2, + 14, + "1" + ], + [ + "swap", + 10, + 3, + "1" + ], + [ + "swap", + 11, + 4, + "1" + ], + [ + "add", + 4, + 0, + "-1" + ], + [ + "add", + 4, + 1, + "1" + ], + [ + "add", + 4, + 13, + "-1" + ], + [ + "add", + 4, + 14, + "1" + ], + [ + "swap", + 12, + 5, + "1" + ], + [ + "swap", + 13, + 6, + "1" + ], + [ + "scale", + 6, + 6, + "-2" + ], + [ + "add", + 6, + 0, + "-1" + ], + [ + "add", + 6, + 1, + "2" + ], + [ + "add", + 6, + 2, + "-1" + ], + [ + "add", + 6, + 4, + "-1" + ], + [ + "add", + 6, + 14, + "2" + ], + [ + "swap", + 14, + 7, + "1" + ], + [ + "scale", + 7, + 7, + "2" + ], + [ + "add", + 7, + 0, + "-1" + ], + [ + "add", + 7, + 1, + "1" + ], + [ + "add", + 7, + 6, + "-1" + ], + [ + "scale", + 8, + 8, + "1/2" + ], + [ + "add", + 8, + 1, + "1/2" + ], + [ + "add", + 8, + 2, + "1/2" + ], + [ + "add", + 8, + 4, + "1/2" + ], + [ + "add", + 8, + 7, + "1/2" + ], + [ + "add", + 8, + 9, + "-1/2" + ], + [ + "add", + 8, + 11, + "-1/2" + ], + [ + "add", + 8, + 13, + "1/2" + ], + [ + "add", + 8, + 14, + "-1" + ], + [ + "add", + 9, + 1, + "-1/2" + ], + [ + "add", + 9, + 2, + "-1/2" + ], + [ + "add", + 9, + 4, + "-1/2" + ], + [ + "add", + 9, + 7, + "-1/2" + ], + [ + "add", + 9, + 8, + "1" + ], + [ + "add", + 9, + 13, + "-1" + ], + [ + "add", + 9, + 14, + "1" + ], + [ + "add", + 11, + 1, + "-1/2" + ], + [ + "add", + 11, + 2, + "-1/2" + ], + [ + "add", + 11, + 4, + "-1/2" + ], + [ + "add", + 11, + 7, + "-1/2" + ], + [ + "add", + 11, + 8, + "1" + ], + [ + "add", + 11, + 13, + "-1" + ], + [ + "add", + 11, + 14, + "1" + ], + [ + "scale", + 13, + 13, + "-2" + ], + [ + "add", + 13, + 1, + "-1/2" + ], + [ + "add", + 13, + 2, + "-1/2" + ], + [ + "add", + 13, + 4, + "-1/2" + ], + [ + "add", + 13, + 7, + "-1/2" + ], + [ + "add", + 13, + 8, + "2" + ], + [ + "add", + 13, + 9, + "-1" + ], + [ + "add", + 13, + 11, + "-1" + ], + [ + "add", + 13, + 14, + "2" + ], + [ + "scale", + 14, + 14, + "2" + ], + [ + "add", + 14, + 1, + "-1/2" + ], + [ + "add", + 14, + 2, + "-1/2" + ], + [ + "add", + 14, + 4, + "-1/2" + ], + [ + "add", + 14, + 7, + "-1/2" + ], + [ + "add", + 14, + 8, + "1" + ], + [ + "add", + 14, + 13, + "-1" + ] + ], + "field_contract": { + "reads": [ + "current_low", + "current_high" + ], + "writes": [ + "current_low", + "current_high" + ], + "preserves": [ + "ancestors", + "role_type", + "unused_child_stock", + "head_data", + "spectators" + ] + }, + "elementary_column_factors": 77, + "row_field_steps_per_route": 4928, + "omitted_factor_controls": 77, + "cases": [ + { + "q": "5", + "width": 1, + "stage": 1, + "dense_sha256": "f5909d62d55d7787f517d66459eccd9c87ebdc977c665cd6ba1046e03ffdb562" + }, + { + "q": "5", + "width": 1, + "stage": 8, + "dense_sha256": "dcc11c7cd2a66f9b185045d229d310929bf75b0464e0c3ef7a3d062207d16094" + }, + { + "q": "5", + "width": 2, + "stage": 1, + "dense_sha256": "cabdf486902a06da2c23e7d874288e9a147c1460335be0bec329f1e3c8b51a83" + }, + { + "q": "5", + "width": 2, + "stage": 8, + "dense_sha256": "e8a6b041174d0a59b31f7e8f52f2e959a11f13a75a93ffc31c2d0a948c9b8165" + }, + { + "q": "5", + "width": 3, + "stage": 1, + "dense_sha256": "fccceed880eb1fb2f9563b7b0b1c97a1119dde1bd7a16a21aaf480b965647a37" + }, + { + "q": "5", + "width": 3, + "stage": 8, + "dense_sha256": "f8dfabba76b114ceb9307f19b60351bd3a964861b78f99b2ce64686adb31fa1a" + }, + { + "q": "5", + "width": 8, + "stage": 1, + "dense_sha256": "05f682ff8c0205a2d0b4a6e73e55a86c39226df90916358925b01e157f707296" + }, + { + "q": "5", + "width": 8, + "stage": 8, + "dense_sha256": "c251e91b782193ace65b80c426f7bd9943219a832c36b49b5229daf3b5fb3c37" + }, + { + "q": "7", + "width": 1, + "stage": 1, + "dense_sha256": "c0e91bc882dc1d807200ad0497bb69723fe7f2f22d3edca7f3050aa68688c8ef" + }, + { + "q": "7", + "width": 1, + "stage": 8, + "dense_sha256": "5f79076f7c11a96c2bdd62eccf713e1a8dc74e75353aee0b7889fad61f08de67" + }, + { + "q": "7", + "width": 2, + "stage": 1, + "dense_sha256": "931bfad398ed886f83fe5c3d7247abb39a25b4a6b796f67c4384c73dc908e4d6" + }, + { + "q": "7", + "width": 2, + "stage": 8, + "dense_sha256": "3b6a9818453daac2d1639a967c4d9cd294ccd7bb8972b035c7117ff96addf82a" + }, + { + "q": "7", + "width": 3, + "stage": 1, + "dense_sha256": "44a35cad05146cbb11ef816fedefe70b1e526de4be2f3a23e0a00e815fa7f13b" + }, + { + "q": "7", + "width": 3, + "stage": 8, + "dense_sha256": "4dadaa091db0c4a4c7c8d1abac3edfde318bdcd22fdd9d9061757067ee254980" + }, + { + "q": "7", + "width": 8, + "stage": 1, + "dense_sha256": "47d8786039fdf1064e49c01513032c038518036d5f82fd535cb1135ee1a713e7" + }, + { + "q": "7", + "width": 8, + "stage": 8, + "dense_sha256": "38ffc60b053fcb2924bc53d47e6d3110f5441c6f9f6f2ce7551e154b9174e9b5" + }, + { + "q": "618970019642690137449562111", + "width": 1, + "stage": 1, + "dense_sha256": "4632cd14a4c081d188f4ad5c425923940566ea5e64a4df79fdfaad87bcd04bb0" + }, + { + "q": "618970019642690137449562111", + "width": 1, + "stage": 8, + "dense_sha256": "e0722ddcaddc8ddf1195a0c414a186bd2d90ff936ecac16c81e6117cb825b8eb" + }, + { + "q": "618970019642690137449562111", + "width": 2, + "stage": 1, + "dense_sha256": "497486969eeea04630f9f42343ba75b4f2f9fe3dd6f1114f60d76838f6dd62ca" + }, + { + "q": "618970019642690137449562111", + "width": 2, + "stage": 8, + "dense_sha256": "991568566d9422ed7ed0dadafd07ca7fda297f92bd15eeeb19546c741844e225" + }, + { + "q": "618970019642690137449562111", + "width": 3, + "stage": 1, + "dense_sha256": "e7ca9f3d6816d62fe0712afe838528892c12b20473a5d7aa7fb55b8f908380a4" + }, + { + "q": "618970019642690137449562111", + "width": 3, + "stage": 8, + "dense_sha256": "f2d7f6b2b9e62d8f91bea20a9876622ef2e771b4a5a01e90e4a25d54f88b4e26" + }, + { + "q": "618970019642690137449562111", + "width": 8, + "stage": 1, + "dense_sha256": "fda2519ad057d8d18f4a79ac41f13b734ec4efbb23f8da47916be7dcd640bbfe" + }, + { + "q": "618970019642690137449562111", + "width": 8, + "stage": 8, + "dense_sha256": "b66cc35a7106effc6377d09431b054a216b4db90393e6ad9cd1265bd97781f54" + } + ], + "carry_omission_counterexample": { + "q": 5, + "width": 2, + "stage": 8, + "row": 0, + "column": 6, + "uncarried_entry": 19, + "correct_entry": 14, + "active_input_row": [ + 1, + 17, + 6, + 20, + 9, + 23, + 12, + 1, + 1, + 15, + 4, + 18, + 7, + 21, + 10 + ], + "low_residues_correct": true, + "two_applications_restore": true, + "full_right_product_correct": false + }, + "scope": "One selected route's exact row-index lowering; no physical compiler, supplier or new kappa." +} diff --git a/research/selected-bit-qadic-route/SELECTION.json b/research/selected-bit-qadic-route/SELECTION.json new file mode 100644 index 0000000000..8df6a924fb --- /dev/null +++ b/research/selected-bit-qadic-route/SELECTION.json @@ -0,0 +1,145 @@ +{ + "seed": "9bc79982c2b5ec6b061620fa5fc31c80", + "track": "complex-mechanisms", + "suggestions": [ + { + "task_id": "complex-new-helper-inventory", + "scope_key": "5868e5281a1e63d41a22", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "method": "Propose a changed helper inventory and derive an optimistic exact moment.", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "complex-rank-shape-decoder", + "scope_key": "cad3ba853d7f324f16fa", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "method": "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration.", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "p104-side-correction", + "scope_key": "c5367b1a1b7bed20db53", + "question": "Can the native P104 low-rank channel be completed with a legal, fully charged I-G/2 side correction?", + "method": "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "starting_points": [ + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md" + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the P104 open next questions and its fixed local histogram; inspect why appending I-G/2 after source completion is not justified. #1991 supplies the checked native channel, not the missing correction.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one exact side-correction cut and bound its allowed cost from a favorable completed moment at a declared target. Stop or hand off if the necessary source/target access cannot be justified or even the optimistic total misses the target.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "catalog_assessed_on": "2026-10-14", + "priority_revision": 4, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/selected-bit-qadic-route/SOURCES.json b/research/selected-bit-qadic-route/SOURCES.json new file mode 100644 index 0000000000..f2009db7e3 --- /dev/null +++ b/research/selected-bit-qadic-route/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/nine/geometry.py", + "usage": "input", + "git_blob": "91594e0223e8fac49162b5aef834ffaa8e94a254", + "sha256": "36eeda3184bd009e89462b65c8725d10860c444f8da8f1f87e5f6e50120011ca" + }, + { + "path": "research/e8-bit-carrier-skeleton/data/bit/bitE8-r865.json.gz", + "usage": "input", + "git_blob": "8bec1751f7e33c3a1e4673ef5dbc34d6f205321e", + "sha256": "1fb726ea3818fe0837cceb0dd22a71a0814f064e5e781628104610d6468e0e55" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr545/code/adapt.py", + "usage": "input", + "git_blob": "bd1552af18ae259c01039627aa06006b9d5e760f", + "sha256": "b9a50303147a3003ad94fc4b1a822d4fca7f9b9e917d165e3c45152575302a0e" + }, + { + "path": "research/five-stage-source527-banks/proof/three-stage-cover-bit.tex", + "usage": "input", + "git_blob": "f05225d21f92cf8cef21b6e12601d5b4d61991f0", + "sha256": "47123a756f823c83a0d48cca2bf5add6472cd88410b13aed345e70c8834fb511" + }, + { + "path": "research/five-stage-source527-banks/proof/three-stage-cover-rows.tex", + "usage": "input", + "git_blob": "590da4b892a08b9d5182fb3d8a983c6239dd27db", + "sha256": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8" + } + ] +} diff --git a/research/selected-bit-qadic-route/TASK.json b/research/selected-bit-qadic-route/TASK.json new file mode 100644 index 0000000000..1fd49a1a99 --- /dev/null +++ b/research/selected-bit-qadic-route/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "selected-stock-envelope", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #1956/#1965/#1990 in the batch review and the stock-audit source boundary. Its actual selected coefficient remains uncomputed.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one of the fourteen recorded stages, pin its producer, and derive the parent reserve and depth coefficient. Stop with a precise source-level missing lemma if that coefficient cannot yet be bounded; do not rerun the already checked headroom arithmetic as a new result.", + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990" + ] + }, + "scope_status": "changed", + "actual_scope": "Certify the exact low/high q-adic row-chart lowering and ancestor/descendant field isolation for selected BIT port 8, stages 1 and 8, without claiming full compiler realization.", + "scope_change_reason": "Took PR2120's released field-split handoff after live overlap. PR2084/2120 already supply conditional stock coefficients; PR2097 proves fresh-fiber counting conditionally but leaves emitted field-dependency certificates open. This contribution addresses one route's missing carry lowering instead of repeating stock arithmetic. The initial random complex-mechanisms suggestions are retained in SELECTION.json and overridden for this central handoff, not redrawn.", + "bottleneck_link": "A stock magnitude alone cannot establish complete fresh descendant fields. An explicit selected route lowering can certify one required row-field map and identify which physical compiler obligations still remain.", + "budget_minutes": 60, + "coordination": { + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2114#discussioncomment-18933061", + "discussion_posted": false, + "reason": "The loaded engineering workflow prohibits human-directed Discussion posts. Scope was recorded locally before implementation; no retrospective claim is asserted.", + "entry_overlap": {"pr_fetched_at": "2026-10-14T20:24:08.298802+00:00", "open_prs": 389, "discussion_fetched_at": "2026-10-14T20:25:35.516970+00:00", "discussion_records": 798, "complete_pagination": true}, + "coverage_limits": "Titles/bodies/comments/replies and top-level local package notes; not every code diff, nested file or unpublished result. No absence-based novelty guarantee.", + "submission_refresh": { + "upstream_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "pr_fetched_at": "2026-10-14T20:39:42.804492+00:00", + "open_prs": 396, + "discussion_fetched_at": "2026-10-14T20:41:06.213047+00:00", + "discussion_records": 807, + "complete_pagination": true, + "warnings": [], + "decision": "Continue the one-route handoff. Canonical main, all scientific inputs and all three directly rechecked predecessor heads are unchanged. No completed overlapping q-adic carry lowering was identified in the metadata search." + }, + "predecessor_heads": {"2084": "8001a23b003bec5dff5e61edec907b652c475932", "2097": "1d3ee0926656d5260c6cb1c0b81964ffe9fe1377", "2120": "378593574261e0b0915e7e8a83147aa640274fc8"} + }, + "stop_rule": "Stop after one source-bound nontrivial route, exact all-width carry proof, dense modular oracle, all omitted-factor controls, source/receipt controls and registered replay. Do not claim the full GL64 compiler or search another unrelated mechanism.", + "outcome": "completed", + "evidence": "README.md proves the all-width row-index identity; RESULT.json binds the rational route, 77 factors, 24 exact modular cases and a carry-omission witness that passes low-routing and involution checks but fails the full matrix product. Registered Python 3.12 normal/optimized replay and 11 tests pass; all 65 research-workflow tests and selected-record integrity pass.", + "verification_limits": "Author-checked with code-disjoint dense modular and rational-factor oracles, not an independent human or formal review. No subagent review capability was available. No cold supplier replay, physical routing cost, full GL64 compiler or new kappa.", + "author": "Nick Petalas", + "ai_assistance": "Authorship and responsibility remain with Nick Petalas; no independent human review is claimed.", + "open_questions": [ + { + "question": "Can every selected owner route and child-weight descriptor be lowered with this same field-isolation contract?", + "why_it_matters": "One route does not establish the full fresh-field interface required by the conditional stock and averaging arguments.", + "first_step": "Cover helper/bank and hosted owner routes, then emit each child descriptor's ancestor-only reads.", + "blocked_by": "The finite selected program does not itself emit the all-size GL64 compiler or physical stream/tape realization." + }, + { + "question": "Can the low/high field operations be given a source-bound physical cost and completed-leaf implementation?", + "why_it_matters": "An exact row-index permutation is not an uncharged physical dense address pass or supplier admission.", + "first_step": "Implement one carry-controlled ordered shift or scaling and bind its preserved complete spectators and charged ordinary calls.", + "blocked_by": "Ordered-affine, fixed-tape, leaf borrowing and physical hosting contracts remain inherited. Local instruction counts are not a paid recursive profile." + } + ] +} diff --git a/research/selected-bit-qadic-route/VERIFY.json b/research/selected-bit-qadic-route/VERIFY.json new file mode 100644 index 0000000000..17222104cf --- /dev/null +++ b/research/selected-bit-qadic-route/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/e8-bit-carrier-skeleton/code/nine/geometry.py", + "research/e8-bit-carrier-skeleton/data/bit/bitE8-r865.json.gz", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/vendor/pr545/code/adapt.py", + "research/five-stage-source527-banks/proof/three-stage-cover-bit.tex", + "research/five-stage-source527-banks/proof/three-stage-cover-rows.tex" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticated selected route, exact factor product, dense modular oracle, all omitted factors and field restoration" + }, + { + "argv": ["{python}", "-I", "-W", "error", "-O", "-B", "{package}/test_route.py"], + "timeout_seconds": 120, + "checks": "Exact carry exhaustions, signed/scaled factors, noncommuting order, field isolation and source/receipt rejection" + } + ] +} diff --git a/research/selected-bit-qadic-route/route.py b/research/selected-bit-qadic-route/route.py new file mode 100644 index 0000000000..fc95a43dad --- /dev/null +++ b/research/selected-bit-qadic-route/route.py @@ -0,0 +1,137 @@ +"""Exact q-adic row-chart updates, not a physical address compiler. + +Apache-2.0. Rational geometry follows Zhihao Chen's retained PR386/PR370 +construction, selected through DreamingOfClouds' PR545 and PR589 pipeline. +""" +from fractions import Fraction as F +from math import gcd + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return [[F(i == j) for j in range(n)] for i in range(n)] + + +def multiply(a, b): + n = len(a) + require(1 <= n <= 64 and len(b) == n, "matrix dimension") + require(all(len(r) == n for r in a + b), "square matrices") + return [[sum(a[i][k] * b[k][j] for k in range(n)) + for j in range(n)] for i in range(n)] + + +def selected_reflection(lines, target): + """Reconstruct the source's first-discovery BFS, stopping at this port.""" + require(len(lines) == 120 and 0 <= target < 120, "root inventory") + require(all(len(r) == 8 for r in lines), "root dimension") + maps = {0: identity(8)} + frontier = [0] + for _ in range(120): + if target in maps: + g = maps[target] + q = lines[target] + p = [[F(x * y, 4) for y in q] for x in q] + a = [r[1:] for r in g] + return [p[i] + a[i] for i in range(8)] + [ + [a[i][j] for i in range(8)] + [F(0)] * 7 + for j in range(7)] + following = [] + for i in frontier: + for j in range(120): + dot = sum(x * y for x, y in zip(lines[i], lines[j])) + if j in maps or abs(dot) != 2: + continue + sign = 1 if dot == 2 else -1 + d = [x - sign * y for x, y in zip(lines[i], lines[j])] + norm = sum(x * x for x in d) + r = [[F(x == y) - F(2 * d[x] * d[y], norm) + for y in range(8)] for x in range(8)] + maps[j] = multiply(r, maps[i]) + following.append(j) + frontier = following + raise ValueError("unreachable root") + + +def column_program(matrix): + """If E_k ... E_1 R = I, right multiplication uses E_1^-1 ... E_k^-1.""" + n = len(matrix) + require(1 <= n <= 15 and all(len(r) == n for r in matrix), "route size") + z = [list(map(F, r)) for r in matrix] + ops = [] + for j in range(n): + pivots = [i for i in range(j, n) if z[i][j]] + require(bool(pivots), "singular route") + p = pivots[0] + if p != j: + z[p], z[j] = z[j], z[p] + ops.append(("swap", p, j, F(1))) + if z[j][j] != 1: + c = 1 / z[j][j] + z[j] = [c * x for x in z[j]] + ops.append(("scale", j, j, 1 / c)) + for i in range(n): + if i != j and z[i][j]: + c = -z[i][j] + z[i] = [x + c * y for x, y in zip(z[i], z[j])] + ops.append(("add", j, i, -c)) + require(z == identity(n), "elimination endpoint") + require(len(ops) <= n * (n + 1), "factor capacity") + return ops + + +def carry_update(low, high, source_low, source_high, coefficient, q, width, scale): + """Compute y <- c*y or y <- y+c*x using separate residue and high fields.""" + require(2 <= q < 2**127 and 1 <= width <= 16, "radix/width capacity") + require(isinstance(coefficient, F), "rational coefficient") + a, d = coefficient.numerator, coefficient.denominator + require(max(abs(a).bit_length(), d.bit_length()) <= 16, "coefficient capacity") + require(gcd(d, q) == 1 and (not scale or gcd(a, q) == 1), "nonunit factor") + modulus = q ** (width - 1) + require(0 <= low < q and 0 <= source_low < q, "low field range") + require(0 <= high < modulus and 0 <= source_high < modulus, "high field range") + low_numerator = a * low if scale else d * low + a * source_low + high_numerator = a * high if scale else d * high + a * source_high + new_low = low_numerator * pow(d, -1, q) % q + carry, remainder = divmod(low_numerator - d * new_low, q) + require(remainder == 0, "integral carry") + new_high = (high_numerator + carry) * pow(d, -1, modulus) % modulus + return new_low, new_high + + +def route_fields(fields, program, axes, q, width): + """Only current_low/current_high are replaced; all other fields are retained.""" + require(1 <= len(axes) <= 15 and len(set(axes)) == len(axes), "route axes") + require(all(type(i) is int and 0 <= i < 64 for i in axes), "ambient axes") + require(len(program) <= 240 and len(fields) <= 16, "program/field capacity") + low, high = fields["current_low"], fields["current_high"] + require(len(low) == len(high) == 64, "ambient rows") + require(all(len(r) == 64 for r in low + high), "ambient columns") + require(2 <= q < 2**127 and 1 <= width <= 16, "radix/width capacity") + require(all(type(x) is int and 0 <= x < q for r in low for x in r), "low matrix range") + cap = q ** (width - 1) + require(all(type(x) is int and 0 <= x < cap for r in high for x in r), "high matrix range") + low, high = [list(r) for r in low], [list(r) for r in high] + for kind, dest, src, c in program: + require(kind in ("swap", "scale", "add"), "unknown operation") + require(0 <= dest < len(axes) and 0 <= src < len(axes), "operation axes") + i, j = axes[dest], axes[src] + require(kind == "scale" or i != j, "aliased operation") + for row in range(64): + if kind == "swap": + low[row][i], low[row][j] = low[row][j], low[row][i] + high[row][i], high[row][j] = high[row][j], high[row][i] + else: + low[row][i], high[row][i] = carry_update( + low[row][i], high[row][i], low[row][j], high[row][j], + c, q, width, kind == "scale") + return {**fields, "current_low": low, "current_high": high} + + +def inverse_program(program): + require(len(program) <= 240, "program capacity") + return [(kind, i, j, 1 / c if kind == "scale" else -c if kind == "add" else c) + for kind, i, j, c in reversed(program)] diff --git a/research/selected-bit-qadic-route/test_route.py b/research/selected-bit-qadic-route/test_route.py new file mode 100644 index 0000000000..a50455a264 --- /dev/null +++ b/research/selected-bit-qadic-route/test_route.py @@ -0,0 +1,191 @@ +#!/usr/bin/env python3 +"""Exact positive fixtures and failure controls, including optimized execution.""" +from fractions import Fraction as F +import copy +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import route as R +import verify as V + + +class CarryTests(unittest.TestCase): + def test_literal_signed_carries(self): + self.assertEqual(R.carry_update(0, 0, 1, 0, F(1, 2), 5, 2, False), (3, 2)) + self.assertEqual(R.carry_update(0, 0, 1, 0, F(-1, 2), 5, 2, False), (2, 2)) + self.assertEqual(R.carry_update(4, 0, 4, 0, F(1), 5, 2, False), (3, 1)) + self.assertEqual(R.carry_update(1, 0, 0, 0, F(1, 2), 5, 2, True), (3, 2)) + self.assertEqual(R.carry_update(1, 0, 0, 0, F(1, 2), 5, 1, True), (3, 0)) + + def test_exhaustive_elementary_ring_maps(self): + count = 0 + for q, width, coefficients in ((3, 2, (F(1, 2), F(-3, 2), F(2))), + (5, 2, (F(-7, 3), F(1, 2)))): + modulus = q**width + for c in coefficients: + cm = c.numerator * pow(c.denominator, -1, modulus) % modulus + for x in range(modulus): + for y in range(modulus): + low, high = R.carry_update(y % q, y // q, x % q, x // q, + c, q, width, False) + self.assertEqual(low + q * high, (y + cm * x) % modulus) + count += 1 + if c.numerator % q: + image = set() + for y in range(modulus): + low, high = R.carry_update(y % q, y // q, 0, 0, c, q, width, True) + self.assertEqual(low + q * high, cm * y % modulus) + image.add(low + q * high) + self.assertEqual(len(image), modulus) + self.assertEqual(count, 1493) + + def test_bad_boundaries(self): + base = [0, 0, 0, 0, F(1), 5, 2, False] + for index, value in ((0, 5), (1, 5), (2, -1), (3, 5), (5, 1), (5, 2**127), (6, 0), (6, 17)): + args = base[:] + args[index] = value + with self.assertRaises(ValueError): + R.carry_update(*args) + with self.assertRaisesRegex(ValueError, "nonunit"): + R.carry_update(0, 0, 0, 0, F(1, 5), 5, 2, False) + with self.assertRaisesRegex(ValueError, "nonunit"): + R.carry_update(0, 0, 0, 0, F(0), 5, 2, True) + with self.assertRaisesRegex(ValueError, "coefficient capacity"): + R.carry_update(0, 0, 0, 0, F(2**16), 5, 2, False) + with self.assertRaisesRegex(ValueError, "rational coefficient"): + R.carry_update(0, 0, 0, 0, 0.5, 5, 2, False) + q = 2**127 - 1 + modulus = q**16 + x, y = modulus - 2, modulus - 1 + low, high = R.carry_update(y % q, y // q, x % q, x // q, F(1, 2), q, 16, False) + self.assertEqual(low + q * high, (y + pow(2, -1, modulus) * x) % modulus) + + def test_noncommuting_column_orientation(self): + program = [("add", 0, 1, F(1, 2)), ("add", 1, 2, F(-2))] + axes = list(range(15)) + matrix = V.program_matrix(program) + self.assertEqual(matrix[1][0], F(1, 2)) + self.assertEqual(matrix[2][1], F(-2)) + self.assertEqual(matrix[2][0], 0) + self.assertNotEqual(V.program_matrix(list(reversed(program))), matrix) + V.check_case(matrix, program, 5, 3, axes) + + +class RouteTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.data = V.authenticated_inputs() + cls.matrix, cls.program = V.selected_route(cls.data) + + def test_fixed_route_and_receipt(self): + actual = V.receipt(self.data) + self.assertEqual(actual, json.loads((HERE / "RESULT.json").read_text())) + self.assertEqual(actual["elementary_column_factors"], 77) + self.assertEqual(actual["row_field_steps_per_route"], 4928) + self.assertEqual(actual["omitted_factor_controls"], 77) + self.assertEqual(len(actual["cases"]), 24) + + def test_low_and_restoration_checks_can_miss_carry_fault(self): + witness = V.carry_omission_control(self.matrix) + self.assertEqual((witness["q"], witness["width"], witness["stage"]), (5, 2, 8)) + self.assertEqual(witness["active_input_row"], [1, 17, 6, 20, 9, 23, 12, 1, 1, 15, 4, 18, 7, 21, 10]) + self.assertEqual((witness["row"], witness["column"], witness["uncarried_entry"], + witness["correct_entry"]), (0, 6, 19, 14)) + self.assertTrue(witness["low_residues_correct"]) + self.assertTrue(witness["two_applications_restore"]) + self.assertFalse(witness["full_right_product_correct"]) + + def test_arbitrary_spectators_and_inactive_columns(self): + axes = list(range(8)) + list(range(57, 64)) + fields = V.split_fields(V.fixture(5, 3), 5) + first = R.route_fields(fields, self.program, axes, 5, 3) + for name in ("ancestors", "role_type", "unused_child_stock", "head_data", "spectators"): + changed = copy.deepcopy(fields) + changed[name] = ("different arbitrary dirt", 1234567) + second = R.route_fields(changed, self.program, axes, 5, 3) + self.assertEqual(second["current_low"], first["current_low"]) + self.assertEqual(second["current_high"], first["current_high"]) + self.assertEqual(second[name], changed[name]) + for i in range(64): + for j in range(8, 57): + self.assertEqual(first["current_low"][i][j], fields["current_low"][i][j]) + self.assertEqual(first["current_high"][i][j], fields["current_high"][i][j]) + + def test_invalid_route_contracts(self): + fields = V.split_fields(V.fixture(5, 2), 5) + for program, axes in ((self.program, [0] * 15), + ([("read_child_stock", 0, 1, F(1))], list(range(15))), + ([("add", 0, 0, F(1))], list(range(15))), + ([("add", 15, 0, F(1))], list(range(15)))): + with self.assertRaises(ValueError): + R.route_fields(fields, program, axes, 5, 2) + bad = copy.deepcopy(fields) + bad["current_high"][0][0] = 5 + with self.assertRaisesRegex(ValueError, "high matrix range"): + R.route_fields(bad, self.program, list(range(15)), 5, 2) + with self.assertRaisesRegex(ValueError, "singular"): + R.column_program([[F(0)]]) + with self.assertRaisesRegex(ValueError, "program/field capacity"): + R.route_fields(fields, [("swap", 0, 1, F(1))] * 241, list(range(15)), 5, 2) + bad = {**fields, "current_low": [[]] * 65} + with self.assertRaisesRegex(ValueError, "ambient rows"): + R.route_fields(bad, self.program, list(range(15)), 5, 2) + + def test_detached_selected_binding(self): + for key, value in (("pr", 555), ("git_blob_sha1", "0" * 40)): + data = dict(self.data) + assembly = json.loads(data[V.ASSEMBLY]) + assembly["bit_supplier"][key] = value + data[V.ASSEMBLY] = json.dumps(assembly).encode() + with self.assertRaises(ValueError): + V.selected_route(data) + + def test_each_source_corruption_rejected(self): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for item in manifest["files"]: + if item["usage"] != "input": + continue + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + for name, payload in self.data.items(): + path = root / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(payload + b"corrupt" if name == item["path"] else payload) + with self.assertRaisesRegex(ValueError, "source hash"): + V.authenticated_inputs(root) + + def test_optimized_cli_receipt_and_no_overwrite(self): + with tempfile.TemporaryDirectory() as directory: + checkout = Path(directory) + root = checkout / "research" / HERE.name + root.mkdir(parents=True) + for path in HERE.glob("*.py"): + (root / path.name).write_bytes(path.read_bytes()) + for name, payload in self.data.items(): + path = checkout / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(payload) + (root / "SOURCES.json").write_bytes((HERE / "SOURCES.json").read_bytes()) + command = [sys.executable, "-I", "-O", "-B", str(root / "verify.py")] + missing = subprocess.run(command, capture_output=True, timeout=15) + self.assertNotEqual(missing.returncode, 0) + self.assertIn(b"RESULT.json", missing.stderr) + (root / "RESULT.json").write_text("{}") + wrong = subprocess.run(command, capture_output=True, timeout=15) + self.assertNotEqual(wrong.returncode, 0) + self.assertIn(b"required result mismatch", wrong.stderr) + target = root / "existing.json" + target.write_text("preserve me") + overwrite = subprocess.run(command + ["--write-result", str(target)], capture_output=True, timeout=15) + self.assertNotEqual(overwrite.returncode, 0) + self.assertEqual(target.read_text(), "preserve me") + + +if __name__ == "__main__": + unittest.main() diff --git a/research/selected-bit-qadic-route/verify.py b/research/selected-bit-qadic-route/verify.py new file mode 100644 index 0000000000..b83ddb79e5 --- /dev/null +++ b/research/selected-bit-qadic-route/verify.py @@ -0,0 +1,211 @@ +#!/usr/bin/env python3 +"""Source-bound selected-route receipt. No predecessor Python is executed.""" +import argparse +import gzip +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import route as R + +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +ROOTS = "research/e8-bit-carrier-skeleton/data/bit/bitE8-r865.json.gz" +EXPECTED = "research/e8-bit-p111-tuned/tune/EXPECTED.json" +ASSEMBLY = "research/community-frontier1094-audit/ASSEMBLY.json" + + +def authenticated_inputs(root=ROOT): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + R.require(len(manifest["files"]) <= 16, "source count") + result = {} + for item in manifest["files"]: + if item["usage"] != "input": + continue + path = root / item["path"] + R.require(path.stat().st_size <= 8 * 1024**2, "source byte capacity") + data = path.read_bytes() + R.require(hashlib.sha256(data).hexdigest() == item["sha256"], "source hash: " + item["path"]) + result[item["path"]] = data + return result + + +def decoded_word(data): + # The authenticated inputs are immutable; also cap decompression before JSON. + import io + with gzip.GzipFile(fileobj=io.BytesIO(data)) as stream: + payload = stream.read(8 * 1024**2 + 1) + R.require(len(payload) <= 8 * 1024**2, "word byte capacity") + return json.loads(payload) + + +def selected_route(data): + assembly = json.loads(data[ASSEMBLY]) + expected = json.loads(data[EXPECTED]) + citation = assembly["bit_supplier"] + blob = hashlib.sha1(b"blob " + str(len(data[EXPECTED])).encode() + b"\0" + data[EXPECTED]).hexdigest() + R.require(citation["pr"] == 589 and citation["path"] == EXPECTED, "BIT producer") + R.require(citation["git_blob_sha1"] == blob, "BIT citation blob") + word = decoded_word(data[WORD]) + old = decoded_word(data[ROOTS]) + R.require((word["h"], word["v"], word["R"]) == (8, 111, 439), "word parameters") + R.require(expected["word"]["file_sha256"] == hashlib.sha256(data[WORD]).hexdigest(), "word binding") + R.require(len(old["lines"]) == 120 and len(word["ports_geom"]) == 111, "port inventory") + port = 8 + original = word["ports_geom"][port] + R.require(original == 8 and word["lines"][port] == old["lines"][original], "selected port") + matrix = R.selected_reflection(old["lines"], original) + R.require(R.multiply(matrix, matrix) == R.identity(15), "reflection involution") + R.require(matrix == [list(r) for r in zip(*matrix)], "reflection symmetry") + R.require(any(x.denominator > 1 for row in matrix for x in row), "nontrivial rational route") + program = R.column_program(matrix) + return matrix, program + + +def modular_matrix(matrix, modulus): + return [[x.numerator * pow(x.denominator, -1, modulus) % modulus for x in row] + for row in matrix] + + +def dense_oracle(values, matrix, axes, modulus): + """Direct modular right product, independent of elementary carry updates.""" + local = modular_matrix(matrix, modulus) + result = [r[:] for r in values] + for row in range(64): + for j, dest in enumerate(axes): + result[row][dest] = sum(values[row][src] * local[i][j] + for i, src in enumerate(axes)) % modulus + return result + + +def fixture(q, width): + """An invertible dense matrix L U with arbitrary high digits, no GL enumeration.""" + modulus = q**width + values = [[int(i == j) for j in range(64)] for i in range(64)] + for i in range(1, 64): + values[i][0] = (q * (i * i + 7) + i + 1) % modulus + for j in range(1, 64): + c = (q * (3 * j + 1) - j - 2) % modulus + for i in range(64): + values[i][j] = (values[i][j] + c * values[i][0]) % modulus + return values + + +def split_fields(values, q): + return {"ancestors": (19, (4, 7), "arbitrary dirty prefix"), + "role_type": 28424, "unused_child_stock": (23, 0, 8191), + "head_data": (3, 11, 5), "spectators": (29, 31), + "current_low": [[x % q for x in row] for row in values], + "current_high": [[x // q for x in row] for row in values]} + + +def join_fields(fields, q): + return [[low + q * high for low, high in zip(a, b)] + for a, b in zip(fields["current_low"], fields["current_high"])] + + +def check_case(matrix, program, q, width, axes): + values = fixture(q, width) + fields = split_fields(values, q) + original = json.loads(json.dumps(fields)) + routed = R.route_fields(fields, program, axes, q, width) + expected = dense_oracle(values, matrix, axes, q**width) + R.require(join_fields(routed, q) == expected, "dense route mismatch") + R.require(json.loads(json.dumps(fields)) == original, "input mutated") + for name in fields.keys() - {"current_low", "current_high"}: + R.require(routed[name] == fields[name], "spectator changed: " + name) + restored = R.route_fields(routed, R.inverse_program(program), axes, q, width) + R.require(restored == fields, "inverse restoration") + # Transpose/order mistakes can survive a symmetric route. Literal factor + # replay is checked separately against the full noncommuting program below. + return hashlib.sha256(json.dumps(expected, separators=(",", ":")).encode()).hexdigest() + + +def program_matrix(program): + z = R.identity(15) + for kind, i, j, c in program: + for row in range(15): + if kind == "swap": + z[row][i], z[row][j] = z[row][j], z[row][i] + elif kind == "scale": + z[row][i] *= c + else: + z[row][i] += c * z[row][j] + return z + + +def carry_omission_control(matrix): + """A wrong router can preserve all low classes and pass an inverse test.""" + q, width = 5, 2 + axes = list(range(8)) + list(range(57, 64)) + original = fixture(q, width) + value = original + first = None + for step in range(2): + low = dense_oracle([[x % q for x in r] for r in value], matrix, axes, q) + high = dense_oracle([[x // q for x in r] for r in value], matrix, axes, q) + value = [[a + q * b for a, b in zip(x, y)] for x, y in zip(low, high)] + if step == 0: + first = value + expected = dense_oracle(original, matrix, axes, q**width) + R.require(value == original, "uncarried mutant restoration") + R.require(all(first[i][j] % q == expected[i][j] % q + for i in range(64) for j in range(64)), "uncarried low route") + R.require((first[0][6], expected[0][6]) == (19, 14), "carry omission witness") + return {"q": q, "width": width, "stage": 8, "row": 0, "column": 6, + "uncarried_entry": 19, "correct_entry": 14, + "active_input_row": [original[0][k] for k in axes], + "low_residues_correct": True, "two_applications_restore": True, + "full_right_product_correct": False} + + +def receipt(data): + matrix, program = selected_route(data) + R.require(program_matrix(program) == matrix, "factor product") + omitted = 0 + for i in range(len(program)): + R.require(program_matrix(program[:i] + program[i + 1:]) != matrix, "ineffective factor") + omitted += 1 + cases = [] + # Small odd radices test carries; 2^89-1 is a known Mersenne prime >2^80. + # No primality inference or selected-prime eligibility follows from fixtures. + for q in (5, 7, 2**89 - 1): + for width in (1, 2, 3, 8): + for stage in (1, 8): + axes = list(range(8)) + list(range(8 + 7 * (stage - 1), 8 + 7 * stage)) + digest = check_case(matrix, program, q, width, axes) + cases.append({"q": str(q), "width": width, "stage": stage, "dense_sha256": digest}) + return {"status": "PASS_SELECTED_BIT_QADIC_ROUTE", "selected_port": 8, "original_port": 8, + "ambient_dimension": 64, "local_dimension": 15, + "root": [0, 1, 1, 0, 1, 0, 0, 1], + "matrix": [[str(x) for x in row] for row in matrix], + "column_program": [[kind, i, j, str(c)] for kind, i, j, c in program], + "field_contract": {"reads": ["current_low", "current_high"], + "writes": ["current_low", "current_high"], + "preserves": ["ancestors", "role_type", "unused_child_stock", "head_data", "spectators"]}, + "elementary_column_factors": len(program), "row_field_steps_per_route": 64 * len(program), + "omitted_factor_controls": omitted, "cases": cases, + "carry_omission_counterexample": carry_omission_control(matrix), + "scope": "One selected route's exact row-index lowering; no physical compiler, supplier or new kappa."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path) + args = parser.parse_args() + result = receipt(authenticated_inputs()) + if args.write_result: + with args.write_result.open("x") as out: + out.write(json.dumps(result, indent=2) + "\n") + else: + expected = json.loads((HERE / "RESULT.json").read_text()) + R.require(result == expected, "required result mismatch") + print(result["status"], "factors=" + str(result["elementary_column_factors"]), + "cases=" + str(len(result["cases"])), "no_new_kappa") + + +if __name__ == "__main__": + main()