From 6779a28938a9af1ba3d32e18ba8feb8d7cc002f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krzysztof=20W=C3=B3jt?= <97155365+krzysztofwojt@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:36:23 +0200 Subject: [PATCH] Prove the minimum affine A5 address dimension is eight --- research/a5-affine-address-minimum/README.md | 302 +++++ .../a5-affine-address-minimum/RESULT.json | 1131 +++++++++++++++++ .../a5-affine-address-minimum/SOURCES.json | 30 + research/a5-affine-address-minimum/TASK.json | 72 ++ .../a5-affine-address-minimum/VERIFY.json | 37 + .../check_algebra.py | 630 +++++++++ research/a5-affine-address-minimum/verify.py | 374 ++++++ 7 files changed, 2576 insertions(+) create mode 100644 research/a5-affine-address-minimum/README.md create mode 100644 research/a5-affine-address-minimum/RESULT.json create mode 100644 research/a5-affine-address-minimum/SOURCES.json create mode 100644 research/a5-affine-address-minimum/TASK.json create mode 100644 research/a5-affine-address-minimum/VERIFY.json create mode 100644 research/a5-affine-address-minimum/check_algebra.py create mode 100644 research/a5-affine-address-minimum/verify.py diff --git a/research/a5-affine-address-minimum/README.md b/research/a5-affine-address-minimum/README.md new file mode 100644 index 0000000000..0910ed2806 --- /dev/null +++ b/research/a5-affine-address-minimum/README.md @@ -0,0 +1,302 @@ +# Eight address bits are necessary for an algebra-faithful affine A5 action + +**Scoped mathematical proof with exact finite ingredients; no new kappa.** +The minimum is **eight binary address bits**, over **all affine A5 actions**. +This answers Open next question 2 of Nick Petalas's +[#5114](https://github.com/CrocSwap/integer-mult-bounds/pull/5114), whose +two-natural-copy construction attains eight but excludes only its particular +four-bit predecessor. The new lower bound includes nonsplit modules and +affine actions without a fixed point. It is not a census of a few candidates. + +The key reduction is stronger: the permutation action on the vectors of any +binary linear module with only one nontrivial composition factor has a nonzero +group-algebra kernel. Two explicit eight-dimensional extension modules cover +every such module by subquotients and fixed summands. Their permutation-algebra +ranks are 52 and 34, respectively, against a 60-dimensional group algebra. + +## Exact statement and relevance + +Put `k = F2` and `G = A5`. For a finite G-set X, `k[X]` means the vector space +with one independent basis vector `e_x` per **point** of X. Define + +```text +rho_X : k[G] -> End_k(k[X]), [g] e_x = e_(gx). +``` + +**Theorem.** Among homomorphisms `G -> AGL(d,2)` acting on the entire address +set `X = F2^d`, the smallest d for which `rho_X` is injective is 8. + +The distinction between an address module V and its data-array space `k[V]` +is essential: their dimensions are `dim(V)` and `2^dim(V)`. Distinguishing the +60 group elements as address maps alone is insufficient. + +This closes the proposed affine-footprint escape below #5114's 256 addresses. +It neither optimizes its address CNOTs or data XORs nor prices an actual BIT +caller. Arbitrary nonlinear address permutations are outside the theorem: +the regular action on 60 labels plus four fixed labels already gives an +algebra-faithful action on a 64-point set, with no affine realization asserted. +No supplier, recursive invoice, selected-result change or practical speedup +is claimed. These remain the same physical and consumer obligations as in +#5114; no unknown implementation cost is set to zero. + +## 1. A finite certificate for the complete list of simple modules + +Use `x=(12)(34)` and `y=(135)`. They generate G, with +`x^2=y^3=(xy)^5=1`. The two nontrivial simple binary modules are: + +* N: the natural `F4^2` module, restricted to k, where + `F4 = F2[w]/(w^2+w+1)`, + `x=[[1,1],[0,1]]`, `y=[[0,w],[w^2,1]]`. +* S: the even-parity subspace of the natural permutation module `k^5`, + in basis `e_i+e_4` for `i=0,1,2,3`. + +Here is a finite proof that this list, together with the trivial module, is +complete; no external modular-character classification is assumed. Form + +```text +Phi : k[G] -> k x M_2(F4) x M_4(k) +``` + +from augmentation, N and S. The separately implemented +[`check_algebra.py`](check_algebra.py) enumerates all even permutations, +aligns the natural matrices by generator words, and checks multiplication +on all 3,600 group pairs. The three image spans have dimensions 1, 8 and 16, +and the combined map has rank 25. Thus Phi is onto the stated product. +Its kernel J has dimension 35; exact group-algebra multiplication gives + +| Ideal | J | J^2 | J^3 | J^4 | J^5 | +|---|---:|---:|---:|---:|---:| +| Dimension over k | 35 | 27 | 17 | 9 | 0 | + +The checker also verifies both-sided ideal closure. These are computations in +the full 60-dimensional algebra, not ranks after a characteristic-zero lift. +The independent checker uses natural basis `(1,0),(0,1),(w,0),(0,w)`; +the universal-extension checker uses `(1,0),(w,0),(0,1),(0,w)`. Their two +generator matrices are explicitly bound by the coordinate permutation +`0,2,1,3`; the augmentation bases agree literally. + +If L is a simple module, JL is either zero or L. The latter would imply +`J^5 L=L`, impossible. Hence L factors through the displayed product, whose +simple modules have k-dimensions 1, 4 and 4. Conversely the natural modules +of each full matrix factor are simple. This proves the asserted complete list. + +## 2. Every single-nontrivial-factor module has a three-block form + +First, any module all of whose composition factors are trivial is itself +trivial. A composition-series basis puts its image in an upper unitriangular +binary group, a finite 2-group. The image of y, of order dividing 3, is then +the identity; the image of xy, of order dividing 5, is also the identity, +so x acts identically too. + +Let V have exactly one nontrivial composition factor R, either N or S, and +let `T=V^G` be its maximal trivial submodule. The quotient V/T has no trivial +submodule: its preimage would have only trivial factors and would therefore +enlarge T. A simple submodule of V/T must consequently be R. Its preimage W +gives a filtration + +```text +0 < T < W < V, T = k^a, W/T = R, V/W = k^b, +``` + +allowing zero-dimensional end terms. The last quotient is trivial by the +first paragraph. Since y has odd order, averaging over `` splits this +filtration as a ``-module. In a compatible basis, the generators therefore +have the form + +```text + [ I A C ] [ I 0 0 ] + X = [ 0 Rx B ], Y = [ 0 Ry 0 ], + [ 0 0 I ] [ 0 0 I ] +``` + +where Rx,Ry are the chosen four-dimensional matrices for R. This reduction +includes nonsplit G-modules: only the cyclic odd-order action has been split. + +For each of N and S, the finite checks give `rank(Rx-I)=2`, so +`im(Rx-I)=ker(Rx-I)`. The relation `X^2=I` says + +```text +A(Rx-I)=0, (Rx-I)B=0, AB=0. +``` + +The first two conditions already imply the third. Choose a row basis A0 of +the two-dimensional left kernel and a column basis B0 of the right kernel. +There are arbitrary binary matrices P and Q with +`A=P A0` and `B=B0 Q`. + +Put `D=Rx Ry`. Both R have `D^5=I` and no nonzero D-fixed vector, so +`I+D+D^2+D^3+D^4=0`. Expanding the top-right block of `(XY)^5` gives + +```text +C + A Ry (D+D^3) B. +``` + +Indeed the four intermediate coefficients are 4,3,2,1, reducing to 0,1,0,1 +in k. The other off-diagonal blocks vanish. Thus C is **uniquely forced**: + +```text +C = A Ry (D+D^3) B = P C0 Q, C0 = A0 Ry (D+D^3) B0. (1) +``` + +This bilinear identity, not a bounded enumeration of P and Q, is the +all-dimensions part of the reduction. + +## 3. Two universal extensions and their nonzero annihilators + +Define E_R by the preceding block matrices with `a=b=2`, `A=A0`, `B=B0` +and `C=C0`. For reproducibility, a matrix column is encoded as the integer +whose binary digits are that column, with the first coordinate least +significant. The exact eight-dimensional generators are: + +| R | X columns | Y columns | +|---|---|---| +| N | `1,2,4,8,21,42,70,139` | `1,2,48,16,24,44,64,128` | +| S | `1,2,9,5,34,18,77,178` | `1,2,20,12,4,36,64,128` | + +[`verify.py`](verify.py) checks each is an actual representation of the same +A5 by all 3,600 multiplication pairs; it does not rely on an unchecked group +presentation. It constructs their action on all 256 vectors and computes: + +| R | Rank of `rho_(E_R)` | Kernel dimension | Orbit inventory | +|---|---:|---:|---| +| N | 52 | 8 | `4*1 + 6*12 + 4*15 + 6*20 = 256` | +| S | 34 | 26 | `16*1 + 16*5 + 16*10 = 256` | + +The complete independent kernel bases and explicit group-basis order are in +[`RESULT.json`](RESULT.json). For example, the first nonzero kernel masks are +`000f87dbfc07efc` for N and `000000002649ffc` for S. The group order starts at +the identity and appends unseen left multiples by x then y in breadth-first +order, as recorded by all 60 explicit permutations in the receipt. Every +kernel vector is checked again by cancelling its literal output basis +vectors at **every** input address, separately from the rank elimination. + +Now let V have the block form of section 2. Choose a top complement T' to +`im P` and a linear section `s: im(Q) -> k^b` of Q. The top T' and the +bottom `ker(Q)` are trivial submodules: all off-diagonal images lie in +`im(P)`, while both B and C vanish on `ker(Q)`. The remaining invariant +core is `im(P) + R + s(im(Q))`; its bottom coordinate space alone need not +be invariant. This core is isomorphic to + +```text +(preimage of im(Q) under E_R -> k^2) / ker(P). +``` + +Here `ker(P)` lies in the top, fixed `k^2` of E_R. More explicitly, on the +preimage of `im(Q)` the map `(t,m,z) -> (Pt,m,s(z))` is equivariant by (1), +has kernel exactly `ker(P)` in the top space, and maps onto the invariant +core. Together with T' and `ker(Q)` this accounts for all of V. +Thus **V is a subquotient of E_R plus trivial direct summands**. + +A nonzero element annihilating `k[E_R]` annihilates `k[V]` as well: + +* an invariant subset gives a permutation submodule; +* an equivariant surjection of sets gives a surjection of permutation modules; +* adding a trivial linear summand makes disjoint copies of the same G-set. + +The nonzero annihilator for R from the table therefore works for every V +with that single nontrivial factor, regardless of a and b. If V has no +nontrivial factor its action is trivial and `[1]+[x]` annihilates `k[V]`. + +## 4. Affine lower bound and matching upper bound + +An affine d-bit action `v -> L_g v+t_g` homogenizes to the linear action + +```text +(v,z) -> (L_g v+z t_g, z) +``` + +on a `(d+1)`-dimensional module H. It has a trivial one-dimensional quotient, +and its invariant affine slice `z=1` is exactly the original address G-set. +If `d<=7`, then `dim(H)<=8`; section 1 and the trivial quotient allow at +most one nontrivial four-dimensional composition factor. Section 3 gives +a nonzero annihilator of `k[H]`, which also annihilates the invariant slice. +Consequently no such affine action is algebra-faithful. + +For d=8, use the predecessor's action on `M_2(F4)` by left multiplication. +The orbit of the identity matrix consists of the 60 distinct matrices of +`SL2(F4)`. For any coefficients c_g, + +```text +(sum_g c_g [g]) e_I = sum_g c_g e_g, +``` + +so a zero operator forces every coefficient to vanish. This is #5114's +regular-orbit upper bound, not a new construction. The local positive control +checks those 60 images (seed 65 in the binary column encoding); it does not +replay the predecessor's endpoint search or CNOT/data-circuit invoice. + +## Reproduction and evidence limits + +From the repository root, standard-library CPython 3.12: + +```sh +python3.12 -I -W error -B research/a5-affine-address-minimum/verify.py +python3.12 -I -O -W error -B research/a5-affine-address-minimum/verify.py +python3.12 -B scripts/research_package.py --package research/a5-affine-address-minimum +``` + +Expected marker: `PASS_A5_AFFINE_ADDRESS_MINIMUM bits=8`. Each direct check +takes a few seconds locally; the registered caps are 120 seconds +per mode. Direct verification works without Git when the two pinned +predecessor inputs are present. Ordinary verification is read-only; explicit +`--write-result` regenerates the deterministic receipt. + +The replay checks the algebra quotient and J powers, both universal group +actions, all kernel witnesses, and the corner formula. For each module, 256 +small P/Q cases also check the actual equivariant subquotient map at 44,032 +domain points, including rank-deficient P and Q; these corroborate the general +written reduction. The regular-orbit positive fixture and 14 rejection +controls are retained. Wrong generator alignment, a corrupted image rank or +group product, the identity asserted to annihilate, a missing witness term, +the zero witness, a wrong extension corner, a supposedly fixed bottom +complement, and a falsely vanishing norm on the upper construction all reject. These +finite checks support the written reduction; they are not a proof-kernel +formalization or independent human acceptance. No physical caller or full +multiplication theorem is verified. + +## Sources, coordination and value check + +Fresh base: `20a1e31bc6009b9b3f4d084bbaadc6350e34fcba`, priority revision 7. +The selected-record source/metadata orientation passed before research; +no historical supplier suite was run. The task picker seed was +`868e7503946f9a08f9e795c7cdf8df97`. The `bit-new-register-model` scope is changed +from a paid-word proposal to this unresolved address-realization minimum. +Current priorities explicitly allow scoped interface obstructions. + +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5131) +takes #5114's explicit open question after its construction reservation was +released. #1166 was checked first. Before claiming, the complete overlap +snapshot covered 314 open PRs, 4,282 Discussion records, 4,406 closed PRs and +6,884 main-tree notes; targeted live searches and this account's recent +claims found no same-scope minimum result. Unpublished work and arbitrary +diffs remain outside that coverage. This adds the universal lower bound; +neither the existing upper construction nor its four-bit check is presented +as a new contribution. + +Exact source blobs and SHA256 values are in [SOURCES.json](SOURCES.json). +The predecessor's README and result at #5114 head +`d165f73e8af63e8621e4e8a279f58b54079e48c5` are retained unchanged and hash-checked. +Only this new package is modified. + +## Open next questions + +The minimum question is closed within the stated affine contract. The useful +next task remains #5114's first question: bind **one actual BIT caller** to +the necessary eight-bit carrier, including its rank-one-projector operation, +frames, owners, arbitrary dirty inputs, restoration and complete movement +and scalar bill. Start from that pinned carrier and a named chronological +caller; stop if its full bill loses the direct implementation. No physical +ABI or tariff is supplied here, and this follow-up is not reserved. + +## Credit + +Krzysztof Wojt, with substantial OpenAI Codex assistance, including a separately +implemented finite-algebra checker. Apache-2.0. Nick Petalas retains the +eight-bit construction and the open minimum question (#5114). Wentao Li +retains the any-register formal endpoint result (#4089); Cinna Davis retains +the A5 word and additive-caller obstruction (#2246/#3914). The natural A5, +SL2(F4), permutation-module and group-algebra methods are classical; their +literature priority is not claimed. The retained register-model lineage, +including eumemic and Ali Romman, keeps its credit. The contribution here is +the universal extension/subquotient obstruction and its application to the +repository's exact affine minimum, with explicit exact finite certificates. diff --git a/research/a5-affine-address-minimum/RESULT.json b/research/a5-affine-address-minimum/RESULT.json new file mode 100644 index 0000000000..136e1cd736 --- /dev/null +++ b/research/a5-affine-address-minimum/RESULT.json @@ -0,0 +1,1131 @@ +{ + "controls": [ + "natural:identity-is-not-zero", + "natural:missing-witness-term", + "natural:zero-witness", + "natural:wrong-extension-corner", + "natural:bottom-complement-is-not-a-fixed-summand", + "augmentation:identity-is-not-zero", + "augmentation:missing-witness-term", + "augmentation:zero-witness", + "augmentation:wrong-extension-corner", + "augmentation:bottom-complement-is-not-a-fixed-summand", + "eight-bit-norm-does-not-vanish" + ], + "group_basis_permutations": [ + [ + 0, + 1, + 2, + 3, + 4 + ], + [ + 1, + 0, + 3, + 2, + 4 + ], + [ + 2, + 1, + 4, + 3, + 0 + ], + [ + 1, + 2, + 3, + 4, + 0 + ], + [ + 3, + 0, + 4, + 2, + 1 + ], + [ + 4, + 1, + 0, + 3, + 2 + ], + [ + 0, + 3, + 2, + 4, + 1 + ], + [ + 1, + 4, + 3, + 0, + 2 + ], + [ + 3, + 2, + 0, + 4, + 1 + ], + [ + 4, + 0, + 1, + 2, + 3 + ], + [ + 2, + 3, + 4, + 0, + 1 + ], + [ + 0, + 4, + 2, + 1, + 3 + ], + [ + 2, + 3, + 1, + 4, + 0 + ], + [ + 3, + 4, + 2, + 0, + 1 + ], + [ + 0, + 2, + 1, + 4, + 3 + ], + [ + 3, + 2, + 4, + 1, + 0 + ], + [ + 4, + 3, + 0, + 2, + 1 + ], + [ + 2, + 0, + 4, + 1, + 3 + ], + [ + 4, + 3, + 1, + 0, + 2 + ], + [ + 2, + 4, + 3, + 1, + 0 + ], + [ + 1, + 3, + 0, + 4, + 2 + ], + [ + 2, + 4, + 1, + 0, + 3 + ], + [ + 3, + 4, + 0, + 1, + 2 + ], + [ + 4, + 2, + 1, + 3, + 0 + ], + [ + 3, + 1, + 4, + 0, + 2 + ], + [ + 4, + 2, + 0, + 1, + 3 + ], + [ + 0, + 3, + 1, + 2, + 4 + ], + [ + 4, + 0, + 3, + 1, + 2 + ], + [ + 1, + 3, + 2, + 0, + 4 + ], + [ + 3, + 0, + 2, + 1, + 4 + ], + [ + 0, + 4, + 1, + 3, + 2 + ], + [ + 3, + 1, + 0, + 2, + 4 + ], + [ + 1, + 2, + 0, + 3, + 4 + ], + [ + 4, + 1, + 2, + 0, + 3 + ], + [ + 0, + 2, + 3, + 1, + 4 + ], + [ + 1, + 3, + 4, + 2, + 0 + ], + [ + 2, + 1, + 3, + 0, + 4 + ], + [ + 1, + 4, + 0, + 2, + 3 + ], + [ + 2, + 0, + 1, + 3, + 4 + ], + [ + 3, + 1, + 2, + 4, + 0 + ], + [ + 1, + 4, + 2, + 3, + 0 + ], + [ + 0, + 1, + 4, + 2, + 3 + ], + [ + 0, + 2, + 4, + 3, + 1 + ], + [ + 4, + 1, + 3, + 2, + 0 + ], + [ + 1, + 0, + 2, + 4, + 3 + ], + [ + 2, + 0, + 3, + 4, + 1 + ], + [ + 0, + 4, + 3, + 2, + 1 + ], + [ + 1, + 0, + 4, + 3, + 2 + ], + [ + 2, + 1, + 0, + 4, + 3 + ], + [ + 2, + 4, + 0, + 3, + 1 + ], + [ + 4, + 0, + 2, + 3, + 1 + ], + [ + 0, + 1, + 3, + 4, + 2 + ], + [ + 1, + 2, + 4, + 0, + 3 + ], + [ + 4, + 2, + 3, + 0, + 1 + ], + [ + 3, + 0, + 1, + 4, + 2 + ], + [ + 3, + 4, + 1, + 2, + 0 + ], + [ + 0, + 3, + 4, + 1, + 2 + ], + [ + 4, + 3, + 2, + 1, + 0 + ], + [ + 3, + 2, + 1, + 0, + 4 + ], + [ + 2, + 3, + 0, + 1, + 4 + ] + ], + "group_order": 60, + "minimum_affine_bits": 8, + "schema": "a5-affine-address-minimum/v1", + "simple_module_coordinate_binding": { + "augmentation": [ + 0, + 1, + 2, + 3 + ], + "natural": [ + 0, + 2, + 1, + 3 + ] + }, + "simple_quotient": { + "algebra_map": { + "ambient_binary_target_dimension": 33, + "block_dimensions": { + "End_F2_F2^4": 16, + "End_F4_F4^2": 8, + "F2": 1 + }, + "declared_target_dimension": 25, + "domain_dimension": 60, + "kernel_basis_sha256": "100bcaafe029bf5bb35d766d48e6ec741c5925a10e301efc73a9f743bc9b545a", + "kernel_dimension": 35, + "kernel_power_dimensions": [ + 35, + 27, + 17, + 9, + 0 + ], + "nilpotence_index": 5, + "rank": 25, + "two_sided_ideal_checked": true + }, + "checks": { + "all_3600_group_products_checked": true, + "all_60_even_permutations_aligned": true, + "corrupted_image_matrix_rank_rejected": true, + "corrupted_multiplication_table_rejected": true, + "target_image_homomorphism_checked": true, + "wrong_generator_alignment_rejected": true + }, + "group": { + "group_basis_sha256": "fd70055d6c507f8d5971a7ce9ea0b968176cfd69bf0adffbc447b5200424189c", + "name": "A5", + "order": 60, + "permutation_convention": "p*q = p after q; images are one-based", + "x_images": [ + 2, + 1, + 4, + 3, + 5 + ], + "y_images": [ + 3, + 2, + 5, + 4, + 1 + ] + }, + "modules": { + "augmentation_subspace": { + "X_matrix": [ + [ + 0, + 1, + 0, + 0 + ], + [ + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 1, + 0 + ] + ], + "Y_matrix": [ + [ + 1, + 1, + 1, + 1 + ], + [ + 0, + 1, + 0, + 0 + ], + [ + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1 + ] + ], + "description": "even-parity subspace of F2^5, basis e_i+e_4 for i=0,...,3", + "dimension_over_F2": 4, + "group_image_span_rank": 16 + }, + "natural": { + "X_F4": [ + [ + "1", + "1" + ], + [ + "0", + "1" + ] + ], + "X_as_F2_matrix": [ + [ + 1, + 1, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 1, + 1 + ], + [ + 0, + 0, + 0, + 1 + ] + ], + "Y_F4": [ + [ + "0", + "w" + ], + [ + "w^2", + "1" + ] + ], + "Y_as_F2_matrix": [ + [ + 0, + 0, + 0, + 1 + ], + [ + 1, + 1, + 1, + 0 + ], + [ + 0, + 1, + 0, + 1 + ], + [ + 1, + 0, + 0, + 1 + ] + ], + "dimension_over_F2": 4, + "dimension_over_F4": 2, + "field": "F2[w]/(w^2+w+1)", + "group_image_span_rank": 8 + } + }, + "result": "PASS_A5_SIMPLE_QUOTIENT", + "scope": "finite algebra checks only; no theorem beyond these checks is asserted" + }, + "source_sha256": { + "research/a5-eight-bit-carrier/README.md": "b6de9f9cdf6da13fb5e7d9b7b145c9fbf5dcf9a96a1c53f5308d846e9107ce18", + "research/a5-eight-bit-carrier/RESULT.json": "6c71f9e7c6a14b484523b80a505b2d539c307713c581c26538cf040098d05f9e" + }, + "universal_extensions": { + "augmentation": { + "bilinear_corner_cases": 256, + "first_witness_permutations": [ + [ + 2, + 1, + 4, + 3, + 0 + ], + [ + 1, + 2, + 3, + 4, + 0 + ], + [ + 3, + 0, + 4, + 2, + 1 + ], + [ + 4, + 1, + 0, + 3, + 2 + ], + [ + 0, + 3, + 2, + 4, + 1 + ], + [ + 1, + 4, + 3, + 0, + 2 + ], + [ + 3, + 2, + 0, + 4, + 1 + ], + [ + 4, + 0, + 1, + 2, + 3 + ], + [ + 2, + 3, + 4, + 0, + 1 + ], + [ + 0, + 4, + 2, + 1, + 3 + ], + [ + 2, + 3, + 1, + 4, + 0 + ], + [ + 3, + 2, + 4, + 1, + 0 + ], + [ + 4, + 3, + 1, + 0, + 2 + ], + [ + 2, + 4, + 1, + 0, + 3 + ], + [ + 3, + 4, + 0, + 1, + 2 + ], + [ + 4, + 2, + 0, + 1, + 3 + ] + ], + "fixed_columns_basis": [ + 3, + 12 + ], + "fixed_rows_basis": [ + 3, + 12 + ], + "kernel_basis_hex": [ + "000000002649ffc", + "000000024476fa3", + "00000041078e45f", + "00000081c2e681f", + "000001101dc055f", + "0000022499b6aa3", + "000004081e38ea3", + "0000080c4e0b210", + "000040311445b74", + "0000900d8464a0f", + "000120049ddb55f", + "0002003c811e124", + "000410209f34aa3", + "00082030c68b76b", + "00103011c7afd61", + "00203009c4f629d", + "0040102d0a7d5f3", + "0080203453cb76b", + "010030155e3ddc2", + "0200300451bf89d", + "0400302109bee1d", + "080030295dc20be", + "1000302598beebd", + "20003024d9afabd", + "4000302543bfc1d", + "800030255a096e2" + ], + "orbit_size_histogram": { + "1": 16, + "5": 16, + "10": 16 + }, + "permutation_algebra_rank": 34, + "simple_x_columns": [ + 2, + 1, + 8, + 4 + ], + "simple_y_columns": [ + 5, + 3, + 1, + 9 + ], + "subquotient_domain_points_checked": 44032, + "universal_x_columns": [ + 1, + 2, + 9, + 5, + 34, + 18, + 77, + 178 + ], + "universal_y_columns": [ + 1, + 2, + 20, + 12, + 4, + 36, + 64, + 128 + ] + }, + "natural": { + "bilinear_corner_cases": 256, + "first_witness_permutations": [ + [ + 2, + 1, + 4, + 3, + 0 + ], + [ + 1, + 2, + 3, + 4, + 0 + ], + [ + 3, + 0, + 4, + 2, + 1 + ], + [ + 4, + 1, + 0, + 3, + 2 + ], + [ + 0, + 3, + 2, + 4, + 1 + ], + [ + 1, + 4, + 3, + 0, + 2 + ], + [ + 4, + 0, + 1, + 2, + 3 + ], + [ + 2, + 3, + 4, + 0, + 1 + ], + [ + 0, + 4, + 2, + 1, + 3 + ], + [ + 2, + 3, + 1, + 4, + 0 + ], + [ + 3, + 4, + 2, + 0, + 1 + ], + [ + 0, + 2, + 1, + 4, + 3 + ], + [ + 3, + 4, + 0, + 1, + 2 + ], + [ + 4, + 2, + 1, + 3, + 0 + ], + [ + 3, + 1, + 4, + 0, + 2 + ], + [ + 4, + 2, + 0, + 1, + 3 + ], + [ + 0, + 3, + 1, + 2, + 4 + ], + [ + 4, + 0, + 3, + 1, + 2 + ], + [ + 1, + 3, + 2, + 0, + 4 + ], + [ + 3, + 0, + 2, + 1, + 4 + ], + [ + 3, + 1, + 0, + 2, + 4 + ], + [ + 1, + 2, + 0, + 3, + 4 + ], + [ + 0, + 2, + 3, + 1, + 4 + ], + [ + 1, + 3, + 4, + 2, + 0 + ], + [ + 2, + 1, + 3, + 0, + 4 + ], + [ + 1, + 4, + 0, + 2, + 3 + ], + [ + 2, + 0, + 1, + 3, + 4 + ], + [ + 4, + 1, + 3, + 2, + 0 + ], + [ + 1, + 0, + 2, + 4, + 3 + ], + [ + 2, + 0, + 3, + 4, + 1 + ], + [ + 0, + 4, + 3, + 2, + 1 + ], + [ + 1, + 0, + 4, + 3, + 2 + ] + ], + "fixed_columns_basis": [ + 1, + 2 + ], + "fixed_rows_basis": [ + 4, + 8 + ], + "kernel_basis_hex": [ + "000f87dbfc07efc", + "00377a5a00a891f", + "00c07d7f43f8bfc", + "0343e5a1480564f", + "0c41e721effc1d7", + "3007327e3ee747b", + "4546e7e2ad53d8d", + "90575e7456da72e" + ], + "orbit_size_histogram": { + "1": 4, + "12": 6, + "15": 4, + "20": 6 + }, + "permutation_algebra_rank": 52, + "simple_x_columns": [ + 1, + 2, + 5, + 10 + ], + "simple_y_columns": [ + 12, + 4, + 6, + 11 + ], + "subquotient_domain_points_checked": 44032, + "universal_x_columns": [ + 1, + 2, + 4, + 8, + 21, + 42, + 70, + 139 + ], + "universal_y_columns": [ + 1, + 2, + 48, + 16, + 24, + 44, + 64, + 128 + ] + } + }, + "upper_regular_seed": 65 +} diff --git a/research/a5-affine-address-minimum/SOURCES.json b/research/a5-affine-address-minimum/SOURCES.json new file mode 100644 index 0000000000..cbeca36534 --- /dev/null +++ b/research/a5-affine-address-minimum/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "20a1e31bc6009b9b3f4d084bbaadc6350e34fcba", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/a5-eight-bit-carrier/README.md", + "usage": "input", + "git_blob": "aa13ba0a0bc41a88cf2c72b27e9f56933ded6603", + "sha256": "b6de9f9cdf6da13fb5e7d9b7b145c9fbf5dcf9a96a1c53f5308d846e9107ce18" + }, + { + "path": "research/a5-eight-bit-carrier/RESULT.json", + "usage": "input", + "git_blob": "3c87bf8767fa42a2d3ed64a561e48d77a1928ade", + "sha256": "6c71f9e7c6a14b484523b80a505b2d539c307713c581c26538cf040098d05f9e" + } + ] +} diff --git a/research/a5-affine-address-minimum/TASK.json b/research/a5-affine-address-minimum/TASK.json new file mode 100644 index 0000000000..48cfbb3d63 --- /dev/null +++ b/research/a5-affine-address-minimum/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "20a1e31bc6009b9b3f4d084bbaadc6350e34fcba", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the minimum number of binary address bits for an affine A5 action whose extension to the full F2[A5] algebra is injective. Covers all affine representations, including nonsplit modules and actions without a fixed point.", + "scope_change_reason": "Take the unclaimed Open next question 2 of Nick Petalas's PR5114, after its eight-bit construction claim was completed and released. This is a universal address-realization obstruction, not another paid-word search or a replay of the predecessor's construction.", + "bottleneck_link": "The theorem rules out reducing the existing carrier's 256-address footprint by choosing another binary affine representation. It is a scoped interface result; no physical tariff, native supplier or kappa gain follows.", + "budget_minutes": 240, + "stop_rule": "Stop at the first complete minimum theorem or smaller construction; if the small-module completeness reduction fails, record the precise gap without claiming a universal minimum. No word search, physical caller campaign or frontier change.", + "outcome": "negative-result", + "evidence": "README proof reduces every relevant module to two explicit universal extensions. Independent finite algebra implementation certifies the quotient F2 x M2(F4) x M4(F2), rank25, and radical power dimensions 35,27,17,9,0. Exact permutation-action ranks52 and34 yield nonzero annihilators. Their preservation through subquotients and affine homogenization proves the seven-bit obstruction; PR5114 supplies the matching eight-bit regular orbit. Author-checked, no independent human or proof-kernel acceptance.", + "author": "Krzysztof Wojt with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for derivation, implementation, verification and writing; a Luna worker independently implemented the finite group-algebra quotient checker and supported overlap/proof-gap review. The primary agent reviewed and reran its finite evidence and retains responsibility for the complete proof.", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5131", + "assignment_seed": "868e7503946f9a08f9e795c7cdf8df97", + "predecessors": [ + {"pr": 5114, "author": "Nick Petalas", "head": "d165f73e8af63e8621e4e8a279f58b54079e48c5", "credit": "Eight-bit algebra-faithful affine carrier and explicit open minimum question"}, + {"pr": 4089, "author": "Wentao Li", "credit": "Any-register formal A5 endpoint theorem"}, + {"pr": 2246, "author": "Cinna Davis", "credit": "A5 conjugate target and dirty-register word"}, + {"pr": 3914, "author": "Cinna Davis", "credit": "Additive caller obstruction and nonabelian escape route"} + ], + "open_questions": [ + { + "question": "Can one actual BIT caller use the now-proved necessary eight-bit carrier with a favorable complete physical bill?", + "why_it_matters": "An address-algebra embedding and its minimum do not establish a useful native recursive supplier.", + "first_step": "Take PR5114's pinned carrier and specify one chronological rank-one-projector call, retaining frames, independent owners, dirty restoration, scalar changes and all address movement; compare the complete direct implementation.", + "blocked_by": "No source-bound physical ABI or full tariff is supplied. This is the predecessor's remaining caller question and is not reserved by this package." + } + ] +} diff --git a/research/a5-affine-address-minimum/VERIFY.json b/research/a5-affine-address-minimum/VERIFY.json new file mode 100644 index 0000000000..ce074c7bf1 --- /dev/null +++ b/research/a5-affine-address-minimum/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/a5-eight-bit-carrier/README.md", + "research/a5-eight-bit-carrier/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete simple quotient with nilpotent kernel; both universal extension actions and every annihilator; bilinear corner formula; eight-bit regular-orbit fixture; rejecting controls; pinned inputs and deterministic receipt" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the exact finite proof ingredients and all rejecting controls with assertions disabled" + } + ] +} diff --git a/research/a5-affine-address-minimum/check_algebra.py b/research/a5-affine-address-minimum/check_algebra.py new file mode 100644 index 0000000000..e020229ca0 --- /dev/null +++ b/research/a5-affine-address-minimum/check_algebra.py @@ -0,0 +1,630 @@ +#!/usr/bin/env python3 +"""Exact finite check for the proposed A5 semisimple quotient. + +This is deliberately self-contained: it uses only Python's standard library, +represents F2/F4 and finite group-algebra elements by small integers, and uses +explicit runtime checks rather than ``assert`` (so ``python -O`` is equivalent). + +The output certifies only the computations it performs: the combined action +map has rank 25, its kernel is a two-sided ideal, and the computed powers of +that ideal reach zero. +""" + +from __future__ import annotations + +import hashlib +import json +from collections import deque +from itertools import permutations +from typing import Callable, Iterable, Sequence + + +class CheckFailure(RuntimeError): + """Raised when an exact finite check does not meet its expected result.""" + + +Permutation = tuple[int, int, int, int, int] +F4Matrix = tuple[tuple[int, int], tuple[int, int]] +BinaryMatrix = tuple[int, ...] # row masks, least significant bit is column 0 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise CheckFailure(message) + + +def compose(p: Permutation, q: Permutation) -> Permutation: + """Return p*q = p after q, matching left column-vector actions.""" + return tuple(p[q[i]] for i in range(5)) # type: ignore[return-value] + + +def permutation_parity(p: Permutation) -> int: + inversions = sum(p[i] > p[j] for i in range(5) for j in range(i + 1, 5)) + return inversions & 1 + + +IDENTITY_PERM: Permutation = (0, 1, 2, 3, 4) +X_PERM: Permutation = (1, 0, 3, 2, 4) # (12)(34) +Y_PERM: Permutation = (2, 1, 4, 3, 0) # (135) + + +def f4_add(a: int, b: int) -> int: + return a ^ b + + +def f4_mul(a: int, b: int) -> int: + """Multiply codes a,b in F2[w]/(w^2+w+1), with w=2 and w^2=3.""" + product = 0 + for i in range(2): + if (a >> i) & 1: + for j in range(2): + if (b >> j) & 1: + degree = i + j + product ^= (1 << degree) if degree < 2 else 3 + return product + + +def f4_matrix_mul(a: F4Matrix, b: F4Matrix) -> F4Matrix: + return tuple( + tuple( + f4_add(f4_mul(a[i][0], b[0][j]), f4_mul(a[i][1], b[1][j])) + for j in range(2) + ) + for i in range(2) + ) # type: ignore[return-value] + + +F4_IDENTITY: F4Matrix = ((1, 0), (0, 1)) +X_F4: F4Matrix = ((1, 1), (0, 1)) +Y_F4: F4Matrix = ((0, 2), (3, 1)) + + +def f4_matrix_power(a: F4Matrix, exponent: int) -> F4Matrix: + result = F4_IDENTITY + for _ in range(exponent): + result = f4_matrix_mul(result, a) + return result + + +def binary_matrix_mul(a: BinaryMatrix, b: BinaryMatrix) -> BinaryMatrix: + """Multiply square F2 matrices stored as row masks.""" + n = len(a) + require(len(b) == n, "binary matrix dimensions differ") + rows: list[int] = [] + for row in a: + value = 0 + for k in range(n): + if (row >> k) & 1: + value ^= b[k] + rows.append(value) + return tuple(rows) + + +def binary_identity(n: int) -> BinaryMatrix: + return tuple(1 << i for i in range(n)) + + +def f4_vector_to_binary(u: int, v: int) -> int: + """Encode (u,v) in the F2 basis (1,0),(0,1),(w,0),(0,w).""" + return (u & 1) | ((v & 1) << 1) | ((u & 2) << 1) | ((v & 2) << 2) + + +def f4_matrix_to_binary(a: F4Matrix) -> BinaryMatrix: + """View an F4-linear 2x2 map as a 4x4 binary linear map.""" + basis = ((1, 0), (0, 1), (2, 0), (0, 2)) + columns: list[int] = [] + for u, v in basis: + out_u = f4_add(f4_mul(a[0][0], u), f4_mul(a[0][1], v)) + out_v = f4_add(f4_mul(a[1][0], u), f4_mul(a[1][1], v)) + columns.append(f4_vector_to_binary(out_u, out_v)) + return tuple( + sum(((columns[col] >> row) & 1) << col for col in range(4)) + for row in range(4) + ) + + +def augmentation_matrix(p: Permutation) -> BinaryMatrix: + """Action on even-parity vectors, in basis e_i+e_4 for i=0,...,3.""" + columns: list[int] = [] + for j in range(4): + column = 0 + for i in range(4): + bit = (p[j] == i) ^ (p[4] == i) + column |= int(bit) << i + columns.append(column) + return tuple( + sum(((columns[col] >> row) & 1) << col for col in range(4)) + for row in range(4) + ) + + +def binary_matrix_mask(matrix: BinaryMatrix) -> int: + n = len(matrix) + return sum( + ((matrix[row] >> col) & 1) << (row * n + col) + for row in range(n) + for col in range(n) + ) + + +def binary_matrix_from_mask(mask: int, n: int) -> BinaryMatrix: + return tuple( + sum(((mask >> (row * n + col)) & 1) << col for col in range(n)) + for row in range(n) + ) + + +def target_image(natural: F4Matrix, augmentation: BinaryMatrix) -> int: + natural_bits = binary_matrix_mask(f4_matrix_to_binary(natural)) + augmentation_bits = binary_matrix_mask(augmentation) + return 1 | (natural_bits << 1) | (augmentation_bits << 17) + + +def target_identity_mask() -> int: + identity4 = binary_matrix_mask(binary_identity(4)) + return 1 | (identity4 << 1) | (identity4 << 17) + + +def target_multiply(a: int, b: int) -> int: + scalar = (a & 1) & (b & 1) + natural_a = binary_matrix_from_mask((a >> 1) & 0xFFFF, 4) + natural_b = binary_matrix_from_mask((b >> 1) & 0xFFFF, 4) + augmentation_a = binary_matrix_from_mask((a >> 17) & 0xFFFF, 4) + augmentation_b = binary_matrix_from_mask((b >> 17) & 0xFFFF, 4) + return ( + scalar + | (binary_matrix_mask(binary_matrix_mul(natural_a, natural_b)) << 1) + | (binary_matrix_mask(binary_matrix_mul(augmentation_a, augmentation_b)) << 17) + ) + + +def check_f4() -> None: + require(f4_mul(2, 2) == 3, "F4 relation w^2=w+1 failed") + require(f4_mul(1, 2) == 2 and f4_mul(1, 3) == 3, "F4 identity failed") + for a in range(4): + for b in range(4): + require(f4_mul(a, b) == f4_mul(b, a), "F4 multiplication is not commutative") + for c in range(4): + require( + f4_mul(f4_mul(a, b), c) == f4_mul(a, f4_mul(b, c)), + "F4 multiplication is not associative", + ) + + +def check_generator_relations( + x_natural: F4Matrix, + y_natural: F4Matrix, + x_augmentation: BinaryMatrix, + y_augmentation: BinaryMatrix, +) -> None: + require(compose(X_PERM, X_PERM) == IDENTITY_PERM, "x^2 != 1 in permutations") + require(compose(compose(Y_PERM, Y_PERM), Y_PERM) == IDENTITY_PERM, "y^3 != 1 in permutations") + xy_perm = compose(X_PERM, Y_PERM) + xy5 = IDENTITY_PERM + for _ in range(5): + xy5 = compose(xy5, xy_perm) + require(xy5 == IDENTITY_PERM, "(xy)^5 != 1 in permutations") + + require(f4_matrix_power(x_natural, 2) == F4_IDENTITY, "x^2 != 1 in natural module") + require(f4_matrix_power(y_natural, 3) == F4_IDENTITY, "y^3 != 1 in natural module") + xy_natural = f4_matrix_mul(x_natural, y_natural) + require(f4_matrix_power(xy_natural, 5) == F4_IDENTITY, "(xy)^5 != 1 in natural module") + + id4 = binary_identity(4) + require(binary_matrix_mul(x_augmentation, x_augmentation) == id4, "x^2 != 1 in augmentation module") + y3 = binary_matrix_mul(binary_matrix_mul(y_augmentation, y_augmentation), y_augmentation) + require(y3 == id4, "y^3 != 1 in augmentation module") + xy_augmentation = binary_matrix_mul(x_augmentation, y_augmentation) + xy5_augmentation = id4 + for _ in range(5): + xy5_augmentation = binary_matrix_mul(xy5_augmentation, xy_augmentation) + require(xy5_augmentation == id4, "(xy)^5 != 1 in augmentation module") + + +def build_group() -> tuple[list[Permutation], dict[Permutation, tuple[F4Matrix, BinaryMatrix]]]: + x_aug = augmentation_matrix(X_PERM) + y_aug = augmentation_matrix(Y_PERM) + check_generator_relations(X_F4, Y_F4, x_aug, y_aug) + + generator_data = ( + (X_PERM, X_F4, x_aug), + (Y_PERM, Y_F4, y_aug), + ) + representations: dict[Permutation, tuple[F4Matrix, BinaryMatrix]] = { + IDENTITY_PERM: (F4_IDENTITY, binary_identity(4)) + } + queue: deque[Permutation] = deque([IDENTITY_PERM]) + while queue: + p = queue.popleft() + natural, augmentation = representations[p] + for generator, natural_generator, augmentation_generator in generator_data: + product = compose(p, generator) + product_rep = ( + f4_matrix_mul(natural, natural_generator), + binary_matrix_mul(augmentation, augmentation_generator), + ) + if product in representations: + require( + representations[product] == product_rep, + "generator words give inconsistent module matrices", + ) + else: + representations[product] = product_rep + queue.append(product) + + group = sorted(representations) + even_permutations = sorted(p for p in permutations(range(5)) if permutation_parity(p) == 0) + require(len(group) == 60, f"generated group has order {len(group)}, expected 60") + require(group == even_permutations, "generator closure differs from all even permutations") + return group, representations + + +def build_multiplication_table( + group: Sequence[Permutation], +) -> tuple[tuple[int, ...], ...]: + index = {p: i for i, p in enumerate(group)} + require(len(index) == len(group), "group list contains duplicate permutations") + table = tuple( + tuple(index[compose(p, q)] for q in group) + for p in group + ) + identity_index = index[IDENTITY_PERM] + require( + all(table[identity_index][i] == i and table[i][identity_index] == i for i in range(len(group))), + "multiplication table has an incorrect identity row or column", + ) + return table + + +def check_representations_and_table( + group: Sequence[Permutation], + representations: dict[Permutation, tuple[F4Matrix, BinaryMatrix]], + table: Sequence[Sequence[int]], +) -> None: + for i, p in enumerate(group): + natural_p, augmentation_p = representations[p] + for j, q in enumerate(group): + natural_q, augmentation_q = representations[q] + product_index = table[i][j] + natural_product, augmentation_product = representations[group[product_index]] + require( + f4_matrix_mul(natural_p, natural_q) == natural_product, + "natural module disagrees with permutation multiplication", + ) + require( + binary_matrix_mul(augmentation_p, augmentation_q) == augmentation_product, + "augmentation module disagrees with permutation multiplication", + ) + + +def rank_of_masks(values: Iterable[int]) -> int: + pivots: dict[int, int] = {} + for original in values: + value = original + while value: + pivot = value.bit_length() - 1 + if pivot in pivots: + value ^= pivots[pivot] + else: + pivots[pivot] = value + break + return len(pivots) + + +def nullspace_basis(columns: Sequence[int], domain_dimension: int) -> tuple[int, list[int]]: + """Return rank and a basis of column dependencies as domain bit masks.""" + pivots: dict[int, tuple[int, int]] = {} + kernel: list[int] = [] + for i, original in enumerate(columns): + value = original + coefficients = 1 << i + while value: + pivot = value.bit_length() - 1 + if pivot in pivots: + pivot_value, pivot_coefficients = pivots[pivot] + value ^= pivot_value + coefficients ^= pivot_coefficients + else: + pivots[pivot] = (value, coefficients) + break + if value == 0: + kernel.append(coefficients) + require(len(columns) == domain_dimension, "domain dimension does not match column count") + return len(pivots), kernel + + +def independent_basis(values: Iterable[int]) -> list[int]: + pivots: dict[int, int] = {} + basis: list[int] = [] + for original in values: + value = original + while value: + pivot = value.bit_length() - 1 + if pivot in pivots: + value ^= pivots[pivot] + else: + pivots[pivot] = value + basis.append(value) + break + return basis + + +def in_span(value: int, basis: Sequence[int]) -> bool: + pivots: dict[int, int] = {} + for vector in basis: + residual = vector + while residual: + pivot = residual.bit_length() - 1 + if pivot in pivots: + residual ^= pivots[pivot] + else: + pivots[pivot] = residual + break + while value: + pivot = value.bit_length() - 1 + if pivot not in pivots: + return False + value ^= pivots[pivot] + return True + + +def algebra_mask_image(mask: int, images: Sequence[int]) -> int: + result = 0 + while mask: + bit = mask & -mask + index = bit.bit_length() - 1 + result ^= images[index] + mask ^= bit + return result + + +def multiply_algebra_masks( + left: int, + right: int, + table: Sequence[Sequence[int]], +) -> int: + result = 0 + left_bits = left + while left_bits: + left_bit = left_bits & -left_bits + i = left_bit.bit_length() - 1 + right_bits = right + while right_bits: + right_bit = right_bits & -right_bits + j = right_bit.bit_length() - 1 + result ^= 1 << table[i][j] + right_bits ^= right_bit + left_bits ^= left_bit + return result + + +def multiply_by_group_basis( + value: int, + group_index: int, + table: Sequence[Sequence[int]], + group_on_left: bool, +) -> int: + result = 0 + bits = value + while bits: + bit = bits & -bits + j = bit.bit_length() - 1 + product_index = table[group_index][j] if group_on_left else table[j][group_index] + result ^= 1 << product_index + bits ^= bit + return result + + +def check_group_table( + group: Sequence[Permutation], + table: Sequence[Sequence[int]], +) -> None: + index = {p: i for i, p in enumerate(group)} + for i, p in enumerate(group): + for j, q in enumerate(group): + require(table[i][j] == index[compose(p, q)], "multiplication table entry is corrupted") + + +def check_image_homomorphism(images: Sequence[int], table: Sequence[Sequence[int]]) -> None: + require(len(images) == len(table), "group-image count mismatch") + require(images[0] == target_identity_mask(), "identity image is not the target identity") + for i, left in enumerate(images): + for j, right in enumerate(images): + require( + images[table[i][j]] == target_multiply(left, right), + "group-basis images fail multiplication consistency", + ) + + +def expect_rejected(label: str, check: Callable[[], None]) -> None: + try: + check() + except CheckFailure: + return + raise CheckFailure(f"negative control was not rejected: {label}") + + +def run_negative_controls( + group: Sequence[Permutation], + table: Sequence[Sequence[int]], + images: Sequence[int], + actual_rank: int, +) -> dict[str, bool]: + x_aug = augmentation_matrix(X_PERM) + y_aug = augmentation_matrix(Y_PERM) + expect_rejected( + "wrong generator alignment", + lambda: check_generator_relations(Y_F4, X_F4, x_aug, y_aug), + ) + + corrupted_images = list(images) + corrupted_images[0] ^= 1 << 33 # add a spurious, independent target coordinate + corrupted_rank = rank_of_masks(corrupted_images) + require(corrupted_rank == actual_rank + 1, "rank-corruption control did not raise rank by one") + expect_rejected( + "corrupted image matrix rank", + lambda: require(corrupted_rank == 25, "combined map rank is not 25"), + ) + + corrupted_table = [list(row) for row in table] + corrupted_table[0][0] = (corrupted_table[0][0] + 1) % len(group) + expect_rejected( + "corrupted multiplication table", + lambda: check_group_table(group, corrupted_table), + ) + return { + "wrong_generator_alignment_rejected": True, + "corrupted_image_matrix_rank_rejected": True, + "corrupted_multiplication_table_rejected": True, + } + + +def hash_json(value: object) -> str: + encoded = json.dumps(value, separators=(",", ":"), sort_keys=True).encode("utf-8") + return hashlib.sha256(encoded).hexdigest() + + +def matrix_as_lists(matrix: BinaryMatrix) -> list[list[int]]: + n = len(matrix) + return [[(matrix[row] >> col) & 1 for col in range(n)] for row in range(n)] + + +def run_checks() -> dict[str, object]: + check_f4() + + group, representations = build_group() + table = build_multiplication_table(group) + check_representations_and_table(group, representations, table) + + natural_images: list[int] = [] + augmentation_images: list[int] = [] + combined_images: list[int] = [] + for p in group: + natural, augmentation = representations[p] + natural_bits = binary_matrix_mask(f4_matrix_to_binary(natural)) + augmentation_bits = binary_matrix_mask(augmentation) + natural_images.append(natural_bits) + augmentation_images.append(augmentation_bits) + combined_images.append(1 | (natural_bits << 1) | (augmentation_bits << 17)) + + check_image_homomorphism(combined_images, table) + natural_rank = rank_of_masks(natural_images) + augmentation_rank = rank_of_masks(augmentation_images) + combined_rank, kernel = nullspace_basis(combined_images, domain_dimension=60) + require(natural_rank == 8, f"natural F4 block rank is {natural_rank}, expected 8") + require(augmentation_rank == 16, f"augmentation block rank is {augmentation_rank}, expected 16") + require(combined_rank == 25, f"combined map rank is {combined_rank}, expected 25") + require(len(kernel) == 35, f"kernel dimension is {len(kernel)}, expected 35") + require(all(algebra_mask_image(v, combined_images) == 0 for v in kernel), "kernel basis image is nonzero") + + ideal_basis = independent_basis(kernel) + require(len(ideal_basis) == 35, "computed kernel basis is not independent") + for j in ideal_basis: + for g in range(60): + left = multiply_by_group_basis(j, g, table, group_on_left=True) + right = multiply_by_group_basis(j, g, table, group_on_left=False) + require(algebra_mask_image(left, combined_images) == 0, "kernel is not left-stable") + require(algebra_mask_image(right, combined_images) == 0, "kernel is not right-stable") + require(in_span(left, ideal_basis), "left product escaped the kernel span") + require(in_span(right, ideal_basis), "right product escaped the kernel span") + + powers = [ideal_basis] + power_dimensions = [len(ideal_basis)] + for _ in range(60): + current = powers[-1] + next_basis = independent_basis( + multiply_algebra_masks(a, b, table) + for a in current + for b in ideal_basis + ) + power_dimensions.append(len(next_basis)) + require( + all(in_span(v, current) for v in next_basis), + "computed ideal powers are not descending", + ) + if not next_basis: + powers.append([]) + break + require( + len(next_basis) < len(current), + "a nonzero computed ideal power failed to decrease", + ) + powers.append(next_basis) + else: + raise CheckFailure("kernel powers did not reach zero within 60 steps") + require(power_dimensions[-1] == 0, "last kernel power is not zero") + require( + power_dimensions == [35, 27, 17, 9, 0], + f"kernel power dimensions are {power_dimensions}, expected [35, 27, 17, 9, 0]", + ) + + controls = run_negative_controls(group, table, combined_images, combined_rank) + group_digest = hash_json([list(p) for p in group]) + kernel_digest = hash_json([f"{v:015x}" for v in kernel]) + x_aug = augmentation_matrix(X_PERM) + y_aug = augmentation_matrix(Y_PERM) + f4_names = {0: "0", 1: "1", 2: "w", 3: "w^2"} + return { + "result": "PASS_A5_SIMPLE_QUOTIENT", + "scope": "finite algebra checks only; no theorem beyond these checks is asserted", + "group": { + "name": "A5", + "order": len(group), + "permutation_convention": "p*q = p after q; images are one-based", + "x_images": [i + 1 for i in X_PERM], + "y_images": [i + 1 for i in Y_PERM], + "group_basis_sha256": group_digest, + }, + "modules": { + "natural": { + "field": "F2[w]/(w^2+w+1)", + "dimension_over_F4": 2, + "dimension_over_F2": 4, + "X_F4": [[f4_names[v] for v in row] for row in X_F4], + "Y_F4": [[f4_names[v] for v in row] for row in Y_F4], + "X_as_F2_matrix": matrix_as_lists(f4_matrix_to_binary(X_F4)), + "Y_as_F2_matrix": matrix_as_lists(f4_matrix_to_binary(Y_F4)), + "group_image_span_rank": natural_rank, + }, + "augmentation_subspace": { + "description": "even-parity subspace of F2^5, basis e_i+e_4 for i=0,...,3", + "dimension_over_F2": 4, + "X_matrix": matrix_as_lists(x_aug), + "Y_matrix": matrix_as_lists(y_aug), + "group_image_span_rank": augmentation_rank, + }, + }, + "algebra_map": { + "domain_dimension": 60, + "ambient_binary_target_dimension": 33, + "declared_target_dimension": 25, + "block_dimensions": {"F2": 1, "End_F4_F4^2": 8, "End_F2_F2^4": 16}, + "rank": combined_rank, + "kernel_dimension": len(kernel), + "kernel_basis_sha256": kernel_digest, + "two_sided_ideal_checked": True, + "kernel_power_dimensions": power_dimensions, + "nilpotence_index": len(power_dimensions), + }, + "checks": { + "all_60_even_permutations_aligned": True, + "all_3600_group_products_checked": True, + "target_image_homomorphism_checked": True, + **controls, + }, + } + + +def main() -> int: + try: + result = run_checks() + except CheckFailure as exc: + print(json.dumps({"result": "FAIL_A5_SIMPLE_QUOTIENT", "error": str(exc)}, sort_keys=True)) + return 1 + print(json.dumps(result, sort_keys=True, separators=(",", ":"))) + print("PASS_A5_SIMPLE_QUOTIENT") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/a5-affine-address-minimum/verify.py b/research/a5-affine-address-minimum/verify.py new file mode 100644 index 0000000000..931449b985 --- /dev/null +++ b/research/a5-affine-address-minimum/verify.py @@ -0,0 +1,374 @@ +#!/usr/bin/env python3 +"""Exact finite ingredients of the affine A5 minimum proof (Apache-2.0). + +Krzysztof Wojt, with substantial OpenAI Codex assistance. +The completeness argument is in README.md; a finite rank test alone is not it. +All matrices use binary column encoding and act on the left. +""" + +from __future__ import annotations + +import argparse +from collections import Counter +import hashlib +from itertools import product +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def identity(n: int) -> tuple[int, ...]: + return tuple(1 << i for i in range(n)) + + +def act(matrix: tuple[int, ...], vector: int) -> int: + out = 0 + while vector: + bit = vector & -vector + out ^= matrix[bit.bit_length() - 1] + vector ^= bit + return out + + +def compose(left: tuple[int, ...], right: tuple[int, ...]) -> tuple[int, ...]: + return tuple(act(left, column) for column in right) + + +def power(matrix: tuple[int, ...], exponent: int) -> tuple[int, ...]: + out = identity(len(matrix)) + for _ in range(exponent): + out = compose(matrix, out) + return out + + +def f4_multiply(a: int, b: int) -> int: + polynomial = (a if b & 1 else 0) ^ (a << 1 if b & 2 else 0) + return polynomial ^ (7 if polynomial & 4 else 0) + + +def binary_natural(matrix: tuple[int, ...]) -> tuple[int, ...]: + out = [] + for v in (1, 2, 4, 8): + lo = f4_multiply(matrix[0], v & 3) ^ f4_multiply(matrix[1], v >> 2) + hi = f4_multiply(matrix[2], v & 3) ^ f4_multiply(matrix[3], v >> 2) + out.append(lo | (hi << 2)) + return tuple(out) + + +def perm_compose(left: tuple[int, ...], right: tuple[int, ...]) -> tuple[int, ...]: + return tuple(left[right[i]] for i in range(5)) + + +def parity_action(permutation: tuple[int, ...]) -> tuple[int, ...]: + # Coordinates v0,...,v3 represent (v0,...,v3,sum(vi)) in F2^5. + return tuple(((1 << permutation[i]) ^ (1 << permutation[4])) & 15 + for i in range(4)) + + +def group_model() -> tuple[list[tuple[int, ...]], list[tuple[int, ...]], + dict[str, tuple[tuple[int, ...], tuple[int, ...]]]]: + x, y = (1, 0, 3, 2, 4), (2, 1, 4, 3, 0) + permutations = [tuple(range(5))] + words: list[tuple[int, ...]] = [()] + lookup = {permutations[0]: 0} + for p, word in zip(permutations, words): + for k, generator in enumerate((x, y)): + q = perm_compose(generator, p) + if q not in lookup: + lookup[q] = len(permutations) + permutations.append(q) + words.append(word + (k,)) + require(len(permutations) == 60, "A5 order") + modules = { + "natural": (binary_natural((1, 1, 0, 1)), binary_natural((0, 2, 3, 1))), + "augmentation": (parity_action(x), parity_action(y)), + } + return permutations, words, modules + + +def evaluate_word(generators: tuple[tuple[int, ...], tuple[int, ...]], + word: tuple[int, ...]) -> tuple[int, ...]: + out = identity(len(generators[0])) + for letter in word: + out = compose(generators[letter], out) + return out + + +def check_representation(permutations: list[tuple[int, ...]], + words: list[tuple[int, ...]], + generators: tuple[tuple[int, ...], tuple[int, ...]]) -> list[tuple[int, ...]]: + images = [evaluate_word(generators, w) for w in words] + lookup = {p: i for i, p in enumerate(permutations)} + for i, p in enumerate(permutations): + for j, q in enumerate(permutations): + require(compose(images[i], images[j]) == images[lookup[perm_compose(p, q)]], + "representation multiplication") + require(len(set(images)) == 60, "group faithfulness") + return images + + +def independent_basis(vectors: list[int]) -> list[int]: + pivots: dict[int, int] = {} + for value in vectors: + while value: + pivot = value.bit_length() - 1 + if pivot in pivots: + value ^= pivots[pivot] + else: + pivots[pivot] = value + break + return list(pivots.values()) + + +def permutation_kernel(images: list[tuple[int, ...]]) -> tuple[int, list[int]]: + size = 1 << len(images[0]) + pivots: dict[int, tuple[int, int]] = {} + kernel = [] + for i, matrix in enumerate(images): + column = sum(1 << (v * size + act(matrix, v)) for v in range(size)) + combination = 1 << i + while column: + pivot = column.bit_length() - 1 + if pivot in pivots: + old_column, old_combination = pivots[pivot] + column ^= old_column + combination ^= old_combination + else: + pivots[pivot] = (column, combination) + break + if not column: + require(combination != 0, "nonzero dependence") + kernel.append(combination) + require(len(independent_basis(kernel)) == len(kernel), "independent kernel witnesses") + require(len(pivots) + len(kernel) == 60, "rank-nullity") + return len(pivots), kernel + + +def check_annihilator(images: list[tuple[int, ...]], mask: int) -> None: + require(0 < mask < (1 << len(images)), "nonzero valid group-algebra witness") + selected = [matrix for i, matrix in enumerate(images) if mask >> i & 1] + # Independent of the flattened-matrix rank calculation: cancel actual output + # basis vectors, for every input basis vector of the permutation module. + for v in range(1 << len(images[0])): + outputs: set[int] = set() + for matrix in selected: + w = act(matrix, v) + if w in outputs: + outputs.remove(w) + else: + outputs.add(w) + require(not outputs, "annihilator acts nontrivially") + + +def extension(rx: tuple[int, ...], ry: tuple[int, ...], + rows: tuple[int, ...], columns: tuple[int, ...]) -> tuple[tuple[int, ...], tuple[int, ...]]: + a, b = len(rows), len(columns) + n = a + 4 + b + unit = identity(n) + x, y = list(unit), list(unit) + for j in range(4): + x[a + j] = (rx[j] << a) | sum(((r >> j) & 1) << i for i, r in enumerate(rows)) + y[a + j] = ry[j] << a + for j, column in enumerate(columns): + x[a + 4 + j] ^= column << a + defect = power(compose(tuple(x), tuple(y)), 5) + require(all(defect[j] == unit[j] for j in range(a + 4)), "fifth-power defect outside corner") + for j in range(b): + delta = defect[a + 4 + j] ^ unit[a + 4 + j] + require(delta < (1 << a), "fifth-power defect outside corner") + x[a + 4 + j] ^= delta + result = tuple(x), tuple(y) + d = compose(rx, ry) + d3 = power(d, 3) + corner_map = compose(ry, tuple(u ^ v for u, v in zip(d, d3))) + for j, column in enumerate(columns): + middle = act(corner_map, column) + formula = sum(((r & middle).bit_count() % 2) << i for i, r in enumerate(rows)) + require(result[0][a + 4 + j] & ((1 << a) - 1) == formula, + "explicit corner C=A Ry(D+D^3)B") + require(power(result[0], 2) == unit, "extension x-square") + require(power(result[1], 3) == unit, "extension y-cube") + require(power(compose(*result), 5) == unit, "extension xy-fifth") + return result + + +def orbit_sizes(images: list[tuple[int, ...]]) -> list[int]: + unseen = set(range(1 << len(images[0]))) + sizes = [] + while unseen: + orbit = {act(g, min(unseen)) for g in images} + require(orbit <= unseen, "disjoint complete orbits") + sizes.append(len(orbit)) + unseen -= orbit + return sorted(sizes) + + +def rejected(call, label: str) -> str: + try: + call() + except ValueError: + return label + raise ValueError("negative control accepted: " + label) + + +def check_subquotient(core: tuple[tuple[int, ...], tuple[int, ...]], + target: tuple[tuple[int, ...], tuple[int, ...]], + p: tuple[int, ...], q: tuple[int, ...]) -> int: + # P is row-encoded, Q column-encoded. Take an actual section of Q, + # rather than treating a bottom vector-space complement as fixed. + section = {} + for v in range(4): + section.setdefault(act(q, v), v) + + def map_point(v: int) -> int: + t, m, z = v & 3, v >> 2 & 15, v >> 6 + pt = sum(((r & t).bit_count() % 2) << i for i, r in enumerate(p)) + return pt | (m << 2) | (section[z] << 6) + + domain = [v for v in range(256) if v >> 6 in section] + image = {map_point(v) for v in domain} + p_image = {sum(((r & t).bit_count() % 2) << i for i, r in enumerate(p)) for t in range(4)} + require(len(image) == len(p_image) * 16 * len(section), "subquotient core size") + for v in domain: + for g, h in zip(core, target): + require(map_point(act(g, v)) == act(h, map_point(v)), "subquotient equivariance") + if map_point(v) == 0: + require(v < 4 and all((r & v).bit_count() % 2 == 0 for r in p), + "subquotient kernel outside top ker(P)") + return len(domain) + + +def core_checks() -> dict: + permutations, words, modules = group_model() + results = {} + controls = [] + for name, (rx, ry) in modules.items(): + check_representation(permutations, words, (rx, ry)) + delta = tuple(c ^ (1 << j) for j, c in enumerate(rx)) + require(len(independent_basis(list(delta))) == 2, "rank(x-I)=2") + ker = [v for v in range(16) if act(rx, v) == v] + coker = [r for r in range(16) if all((r & c).bit_count() % 2 == (r >> j & 1) + for j, c in enumerate(rx))] + rows, columns = tuple(independent_basis(coker)), tuple(independent_basis(ker)) + require(len(rows) == len(columns) == 2, "two-dimensional extension spaces") + require(all((r & c).bit_count() % 2 == 0 for r in rows for c in columns), "AB=0") + xy = compose(rx, ry) + require(power(xy, 5) == identity(4), "order-five simple action") + require(all(act(xy, v) != v for v in range(1, 16)), "no xy-fixed vector") + core = extension(rx, ry, rows, columns) + images = check_representation(permutations, words, core) + rank, kernel = permutation_kernel(images) + require(rank < 60, "universal extension must have a nonzero algebra kernel") + for mask in kernel: + check_annihilator(images, mask) + controls.append(rejected(lambda: check_annihilator(images, 1), name + ":identity-is-not-zero")) + missing_term = kernel[0] ^ (kernel[0] & -kernel[0]) + controls.append(rejected(lambda: check_annihilator(images, missing_term), name + ":missing-witness-term")) + controls.append(rejected(lambda: check_annihilator(images, 0), name + ":zero-witness")) + wrong_corner = list(core[0]) + wrong_corner[6] ^= 1 + controls.append(rejected( + lambda: check_representation(permutations, words, (tuple(wrong_corner), core[1])), + name + ":wrong-extension-corner")) + controls.append(rejected( + lambda: require(act(core[0], 64) == 64, "bottom complement is not fixed"), + name + ":bottom-complement-is-not-a-fixed-summand")) + + # Check C(P A0,B0 Q) = P C0 Q for every binary 2x2 P,Q. + # This finite bilinearity check corroborates the all-size block proof. + corner_checks = 0 + subquotient_points = 0 + for p, q in product(product(range(4), repeat=2), repeat=2): + new_rows = tuple(act(rows, r) for r in p) + new_columns = tuple(act(columns, c) for c in q) + built_x, built_y = extension(rx, ry, new_rows, new_columns) + for j in range(2): + old_corner = act(tuple(core[0][6 + k] & 3 for k in range(2)), q[j]) + predicted = sum(((r & old_corner).bit_count() % 2) << i for i, r in enumerate(p)) + require(built_x[6 + j] & 3 == predicted, "corner bilinearity") + subquotient_points += check_subquotient(core, (built_x, built_y), p, q) + corner_checks += 1 + results[name] = { + "simple_x_columns": list(rx), "simple_y_columns": list(ry), + "fixed_columns_basis": list(columns), "fixed_rows_basis": list(rows), + "universal_x_columns": list(core[0]), "universal_y_columns": list(core[1]), + "permutation_algebra_rank": rank, + "kernel_basis_hex": [f"{m:015x}" for m in kernel], + "orbit_size_histogram": dict(sorted(Counter(orbit_sizes(images)).items())), + "bilinear_corner_cases": corner_checks, + "subquotient_domain_points_checked": subquotient_points, + "first_witness_permutations": [list(p) for i, p in enumerate(permutations) if kernel[0] >> i & 1], + } + # The predecessor's upper bound needs only one regular orbit, not a rerun of + # its CNOT/data programs or predecessor endpoint searches. + nx, ny = modules["natural"] + doubled = tuple(tuple(g) + tuple(c << 4 for c in g) for g in (nx, ny)) + images = check_representation(permutations, words, doubled) + regular_seed = 1 | (4 << 4) + require(len({act(g, regular_seed) for g in images}) == 60, "eight-bit regular orbit") + controls.append(rejected(lambda: check_annihilator(images, (1 << 60) - 1), "eight-bit-norm-does-not-vanish")) + return {"schema": "a5-affine-address-minimum/v1", "minimum_affine_bits": 8, + "group_order": 60, "group_basis_permutations": [list(p) for p in permutations], + "universal_extensions": results, "upper_regular_seed": regular_seed, + "controls": controls} + + +def calculate() -> dict: + # -I deliberately removes the script directory; load only this explicitly + # selected sibling source, with no third-party or predecessor imports. + import runpy + algebra = runpy.run_path(str(HERE / "check_algebra.py"))["run_checks"]() + result = core_checks() + for name, x_key, y_key, algebra_name in ( + ("natural", "X_as_F2_matrix", "Y_as_F2_matrix", "natural"), + ("augmentation", "X_matrix", "Y_matrix", "augmentation_subspace"), + ): + for key, letter in ((x_key, "x"), (y_key, "y")): + columns = result["universal_extensions"][name][f"simple_{letter}_columns"] + rows = [[column >> i & 1 for column in columns] for i in range(4)] + # The independent checker orders the natural basis as + # (1,0),(0,1),(w,0),(0,w); this file groups each F4 coordinate. + order = (0, 2, 1, 3) if name == "natural" else (0, 1, 2, 3) + rows = [[rows[i][j] for j in order] for i in order] + require(rows == algebra["modules"][algebra_name][key], "independent simple-module binding") + result["simple_module_coordinate_binding"] = {"natural": [0, 2, 1, 3], "augmentation": [0, 1, 2, 3]} + result["simple_quotient"] = algebra + root = HERE.parent.parent + source_rows = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"] + bound_inputs = {} + for row in source_rows: + if row["usage"] == "input": + digest = hashlib.sha256((root / row["path"]).read_bytes()).hexdigest() + require(digest == row["sha256"], "source hash: " + row["path"]) + bound_inputs[row["path"]] = digest + require(len(bound_inputs) == 2, "both predecessor inputs bound") + predecessor = json.loads((root / "research/a5-eight-bit-carrier/RESULT.json").read_text(encoding="utf-8")) + require(predecessor["result"]["group_order"] == 60, "predecessor group order") + require(predecessor["result"]["faithful_formal_basis_columns"] == 60, "predecessor upper-bound scope") + result["source_sha256"] = bound_inputs + return result + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--write-result", action="store_true", help="explicitly regenerate RESULT.json") + args = parser.parse_args() + result = calculate() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.write_result: + (HERE / "RESULT.json").write_text(encoded, encoding="utf-8") + else: + expected = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + require(json.loads(encoded) == expected, "committed result mismatch") + print("PASS_A5_AFFINE_ADDRESS_MINIMUM bits=8 result_sha256=" + hashlib.sha256(encoded.encode()).hexdigest()) + + +if __name__ == "__main__": + main()