From 2937b10487f67e3e9b1f4f873a6b87b4c9754ef5 Mon Sep 17 00:00:00 2001 From: Thiago Maceno Rocha Goulart Date: Wed, 14 Oct 2026 01:19:27 -0300 Subject: [PATCH] Prove nine-call bound with arbitrary dirty registers for identical targets --- .../CERTIFICATE.json | 956 ++++++++++++++++++ .../PROOF.md | 345 +++++++ .../README.md | 161 +++ .../SOURCES.json | 36 + .../TASK.json | 109 ++ .../VERIFY.json | 33 + .../independent.py | 170 ++++ .../verify.py | 191 ++++ 8 files changed, 2001 insertions(+) create mode 100644 research/bit-identical-three-targets-dirty/CERTIFICATE.json create mode 100644 research/bit-identical-three-targets-dirty/PROOF.md create mode 100644 research/bit-identical-three-targets-dirty/README.md create mode 100644 research/bit-identical-three-targets-dirty/SOURCES.json create mode 100644 research/bit-identical-three-targets-dirty/TASK.json create mode 100644 research/bit-identical-three-targets-dirty/VERIFY.json create mode 100644 research/bit-identical-three-targets-dirty/independent.py create mode 100644 research/bit-identical-three-targets-dirty/verify.py diff --git a/research/bit-identical-three-targets-dirty/CERTIFICATE.json b/research/bit-identical-three-targets-dirty/CERTIFICATE.json new file mode 100644 index 0000000000..dcf08b21ac --- /dev/null +++ b/research/bit-identical-three-targets-dirty/CERTIFICATE.json @@ -0,0 +1,956 @@ +{ + "call_partitions_checked_with_multiplicity": 144, + "canonical_payload_sha256": "e4f823f34841541723da5326f0d025963f2d2f72faa4ead9aff6217871a6540c", + "cases": [ + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 3, + "u": 1, + "v": 1 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 1, + "v": 3 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 1, + "v": 5 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 1, + "v": 7 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 1, + "v": 9 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 1, + "v": 11 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 1, + "v": 13 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 1, + "v": 15 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 3, + "u": 2, + "v": 2 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 2, + "v": 3 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 2, + "v": 6 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 2, + "v": 7 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 2, + "v": 10 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 2, + "v": 11 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 2, + "v": 14 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 2, + "v": 15 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 3, + "v": 1 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 3, + "v": 2 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 3, + "v": 5 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 3, + "v": 6 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 3, + "v": 9 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 3, + "v": 10 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 3, + "v": 13 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 3, + "v": 14 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 3, + "u": 4, + "v": 4 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 4, + "v": 5 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 4, + "v": 6 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 4, + "v": 7 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 4, + "v": 12 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 4, + "v": 13 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 4, + "v": 14 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 4, + "v": 15 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 5, + "v": 1 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 5, + "v": 3 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 5, + "v": 4 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 5, + "v": 6 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 5, + "v": 9 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 5, + "v": 11 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 5, + "v": 12 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 5, + "v": 14 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 6, + "v": 2 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 6, + "v": 3 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 5, + "u": 6, + "v": 4 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 6, + "v": 5 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 6, + "v": 10 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 6, + "v": 11 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 6, + "v": 12 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 6, + "v": 13 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 7, + "v": 1 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 7, + "v": 2 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 7, + "v": 4 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 7, + "v": 7 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 7, + "v": 9 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 7, + "v": 10 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 7, + "v": 12 + }, + { + "case": "active_image", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 7, + "v": 15 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 8, + "v": 8 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 1, + 2, + 3 + ], + "rank_one_members": 4, + "u": 8, + "v": 9 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 8, + "v": 10 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 1, + 2, + 3 + ], + "rank_one_members": 4, + "u": 8, + "v": 11 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 8, + "v": 12 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 1, + 2, + 3 + ], + "rank_one_members": 4, + "u": 8, + "v": 13 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 8, + "v": 14 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 1, + 2, + 3 + ], + "rank_one_members": 4, + "u": 8, + "v": 15 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 9, + "v": 1 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 9, + "v": 3 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 9, + "v": 5 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 9, + "v": 7 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 9, + "v": 8 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 9, + "v": 10 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 9, + "v": 12 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 9, + "v": 14 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 10, + "v": 2 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 10, + "v": 3 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 10, + "v": 6 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 10, + "v": 7 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 10, + "v": 8 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 1, + 2, + 3 + ], + "rank_one_members": 4, + "u": 10, + "v": 9 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 10, + "v": 12 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 1, + 2, + 3 + ], + "rank_one_members": 4, + "u": 10, + "v": 13 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 11, + "v": 1 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 11, + "v": 2 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 11, + "v": 5 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 11, + "v": 6 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 11, + "v": 8 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 2 + ], + "rank_one_members": 4, + "u": 11, + "v": 11 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 11, + "v": 12 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 0, + 1, + 3 + ], + "rank_one_members": 4, + "u": 11, + "v": 15 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 12, + "v": 4 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 12, + "v": 5 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 12, + "v": 6 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 12, + "v": 7 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 12, + "v": 8 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 1, + 2, + 3 + ], + "rank_one_members": 4, + "u": 12, + "v": 9 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 12, + "v": 10 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 1, + 2, + 3 + ], + "rank_one_members": 4, + "u": 12, + "v": 11 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 13, + "v": 1 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 13, + "v": 3 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 13, + "v": 4 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 13, + "v": 6 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 13, + "v": 8 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 13, + "v": 10 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 1 + ], + "rank_one_members": 4, + "u": 13, + "v": 13 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 0, + 2, + 3 + ], + "rank_one_members": 4, + "u": 13, + "v": 15 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 14, + "v": 2 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 14, + "v": 3 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 14, + "v": 4 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 14, + "v": 5 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 14, + "v": 8 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 1, + 2, + 3 + ], + "rank_one_members": 4, + "u": 14, + "v": 9 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 14, + "v": 14 + }, + { + "case": "active_hyperplane", + "invariant_coordinates": [ + 1, + 2, + 3 + ], + "rank_one_members": 4, + "u": 14, + "v": 15 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 15, + "v": 1 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 15, + "v": 2 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 15, + "v": 4 + }, + { + "case": "dirty_common_kernel", + "invariant_coordinates": null, + "rank_one_members": 4, + "u": 15, + "v": 7 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 15, + "v": 8 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 2 + ], + "rank_one_members": 4, + "u": 15, + "v": 11 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 1 + ], + "rank_one_members": 4, + "u": 15, + "v": 13 + }, + { + "case": "active_line", + "invariant_coordinates": [ + 0 + ], + "rank_one_members": 4, + "u": 15, + "v": 14 + } + ], + "effective_extra_projector_cases": { + "active_hyperplane": 12, + "active_image": 56, + "active_line": 24, + "dirty_common_kernel": 28 + }, + "forbidden_controls_rejected": [ + "rank_one_nilpotent", + "rank_two_projector" + ], + "idempotents": 120, + "rank_one_span_members_checked_with_multiplicity": 489, + "rank_three_projector_decompositions": 28, + "status": "FINITE_CORROBORATION_OF_WRITTEN_SCALAR_REDUCTION" +} diff --git a/research/bit-identical-three-targets-dirty/PROOF.md b/research/bit-identical-three-targets-dirty/PROOF.md new file mode 100644 index 0000000000..eae8424c3b --- /dev/null +++ b/research/bit-identical-three-targets-dirty/PROOF.md @@ -0,0 +1,345 @@ +# Nine-call minimum for three identical invertible targets with dirty workspace + +This is a written proof in a formal abelian register model. It relies on +the named retained theorems below; the new finite controls do not replay +their full proofs or establish a multiplication theorem. + +## 1. Statement, normalization and existing inputs + +Let T be an invertible rational 3-by-3 matrix and let P be a rank-three +idempotent over F2 on any finite R-dimensional scalar register space, +where R >= 3. For a nonzero rank-one rational 3-by-3 matrix A and a binary +rank-one idempotent N, set + +```text +D_N([A]) = I + ([A] - 1) N. +``` + +The symbols belong to the group algebra over F2 of additive rational +matrices, so `[A][B] = [A+B]`. We prove that + +```text +product_j D_Nj([Aj]) = I + ([T] - 1) P (1) +``` + +requires at least nine factors, and that nine suffice. A basis adapted to +P gives the diagonal endpoint `[T], [T], [T], 1, ..., 1`. Thus arbitrary +dirty roles are restored, not assumed zero. Scalar conjugations preserve +the paid alphabet. Common rational left multiplication `A -> T^-1 A` is +an additive automorphism preserving rank and reduces the common target to +I3 when needed. + +We use the following published statements, with their separate scopes: + +1. **Three-register theorem.** Ali Romman's PR468, retained in + `research/bit-three-register-lower-bound/README.md`, sections 1 and 10, + excludes eight calls for three invertible lower-triangular targets on + exactly three scalar registers. It applies to three identical + invertible T after the common normalization above. Its proof includes + a completed finite calculation; that calculation is not rerun here. +2. **At most one rational relation, arbitrary scalar registers.** + woklerx's PR1456, head + `83b6ad2ace819a96128131a3600ee914a66dd0dd`, proves that if k paid + rank-one frames have rational span at least `k-1`, the sum of the + rational ranks of diagonal target frames is at most k. Zero frames + on restored dirty roles are explicitly allowed. No common triangular + target flag is needed for that theorem. + +The low-span and span-four projection arguments used below come from +section 3 of the retained PR468 proof and its eumemic PR288 / huxint +PR203 lineage. We give their needed identical-target/dirty-role forms +explicitly, including the block normalization step. + +## 2. Projection tools and low frame span + +All arguments can be restricted to the subgroup generated by the finitely +many paid frames. This group is finitely generated and torsion-free, so it +is free abelian. Its group algebra is a Laurent polynomial domain and has +a fraction field. + +Write `N_j = x_j y_j^T`. For k nontrivial factors over that fraction field, +the ordered product has the form + +```text +product_j (I + a_j x_j y_j^T) = I + X L Y^T, +X = (x_1 ... x_k), Y = (y_1 ... y_k), +``` + +where L is upper triangular with nonzero diagonal `a_1,...,a_k`. +Consequently, if the product equals I, Sylvester's inequality gives + +```text +rank(X) + rank(Y) <= k. (2) +``` + +More generally, a product-minus-identity of rank W requires both active +scalar spans to have dimension at least W. Rational linear projections +of the paid frames induce group-algebra homomorphisms, so these bounds +remain available after any such projection. + +**Low-span lemma with dirty roles.** In address dimension m, suppose the +paid rank-one frame span has dimension at most m and the endpoint has W +invertible m-by-m targets plus any number of zero targets. Then at least +mW calls are necessary. + +Every target frame occurs as a positional subset sum in the formal +product, hence belongs to the paid span. A span of fewer than m rank-one +basis matrices cannot contain an invertible target. At dimension m, +choose a basis `B_i = u_i v_i^T` from actual paid frames and write one +invertible target as `sum_i c_i B_i`. Its invertibility implies that both +the left and right factor matrices are invertible and that every c_i is +nonzero. Common rational left and right basis changes make the frame +span diagonal. Each nonzero paid rank-one frame then lies on exactly one +coordinate line. Every invertible target has a nonzero coefficient on +every line. Projection to one coefficient gives product-minus-identity +of scalar rank W, requiring at least W calls on that line. The m line +assignments are disjoint. Zero target frames add no rank. + +**Two identical targets.** Two active copies of an invertible rational +3-by-3 T require six calls, even with arbitrary dirty workspace. It +suffices to exclude five: splitting a frame as `A/2 + A/2` with the same +idempotent pads every shorter positive-length word to five. If the +rational frame span d is at most three, the low-span lemma gives six. +If d is at least four, five calls have at most one rational relation, so +PR1456 gives the same bound. Zero calls cannot give the target. + +On a one-dimensional scalar block, one active copy of T costs at least +three calls: every surviving scalar idempotent is 1, the target exponent +is the sum of its paid frames, and rational rank subadditivity applies. + +## 3. Frame span at most four, with identical targets and dirty roles + +Suppose a word has W copies of the same invertible rational 3-by-3 +target and any number of zero targets. We show that rational paid-frame +span at most four forces at least 3W calls. The low-span lemma treats +span at most three. + +At dimension four, choose a basis of rank-one paid matrices. The +determinant of a linear combination is nonzero for some coefficients. +Its nonzero terms use three distinct rank-one basis matrices: a repeated +rank-one summand contributes zero to a determinant. Therefore three +basis matrices have independent left factors and independent right +factors. Common invertible rational left and right maps send them to +`E11,E22,E33`. The fourth basis matrix becomes `B = u v^T`, and the +span consists of `D + t B` with D diagonal. + +These maps also send the common target to an invertible matrix C. They +do **not** in general preserve the target I3; we retain C explicitly. + +If every coordinate of u and v is nonzero, consider distinct i,k,l. The +minor of `D+tB` on rows i,k and columns i,l equals `D_ii t u_k v_l`. +Hence any rank-one matrix with nonzero t has D=0. Every paid rank-one +matrix lies on one of the four independent basis lines. Projecting to +one line requires W calls if C uses that line and zero otherwise. By +rank subadditivity an invertible C uses at least three lines. The sum +of these disjoint call requirements is at least 3W. + +Otherwise u or v has a zero coordinate. Every vertex in a directed +cycle of the graph of B belongs to `supp(u) intersect supp(v)`, whose +size is at most two. Permuting coordinates therefore puts the whole +span into block upper triangular form with diagonal block sizes at +most two. A rank-one matrix in this form has at most one nonzero +diagonal block: nonzero entries in two diagonal blocks would force a +nonzero entry in the lower intervening block. Assign each paid call +to its nonzero diagonal block, if it has one. Calls with all diagonal +blocks zero contribute to none of the following projected words. + +The common target C lies in this block upper triangular span, and +each of its diagonal blocks C_b is invertible. Project to one diagonal +address block, then multiply every projected paid frame and target on +the left by `C_b^-1`. This is an additive automorphism of that block, +preserves each nonzero projected frame's rank one, and changes the +common block target to I_b. It does not alter the disjoint assignment +of original calls to address blocks. + +A one-dimensional address block needs W calls by scalar target rank. +For a two-dimensional block, let E count its assigned calls and U the +number whose normalized upper entry is nonzero. Projecting onto that +upper entry gives the identity endpoint, since the normalized target +is I2. Let r_X and r_Y be the scalar column and row ranks of those U +calls. Equation (2) gives `r_X+r_Y <= U`. For diagonal coordinate i, +let l_i count lower-triangular rank-one frames with nonzero ith +diagonal entry. The diagonal projection's product-minus-identity has +scalar rank W, so + +```text +W <= r_X + l_i, W <= r_Y + l_i. +``` + +A lower-triangular rank-one frame has at most one nonzero diagonal +entry, so `l_1+l_2 <= E-U`. Adding all four inequalities gives + +```text +4W <= 2(r_X+r_Y+l_1+l_2) <= 2E. +``` + +Thus a two-dimensional address block needs 2W calls. Block dimensions +sum to three and assigned calls are disjoint, giving 3W in total. +This argument uses arbitrary scalar matrix size and permits all +restored dirty roles. + +## 4. First-order augmentation bounds the scalar projector span + +Suppose an eight-call word satisfies (1), and let H be the additive +subgroup generated by its eight paid frames. Its free-abelian rank d +is the rational dimension of their frame span. The nonzero formal +coefficient P at `[T]` shows that T belongs to H: at least one +positional subset in the expanded product has sum T. + +Let `V = H/2H`, let a_j be the image of A_j in V, and let t be the image +of T. The a_j span the d-dimensional binary space V. For the +augmentation ideal I of F2[H], `I/I^2` identifies with V. Taking degree +one in (1) gives the exact tensor identity + +```text +sum_j a_j tensor N_j = t tensor P. (3) +``` + +This uses the actual finitely generated H. Applying augmentation to +the divisible ambient rational group, or reducing rational matrix +entries modulo two, would not justify this step. + +Set `S = span_F2{N_1,...,N_8}`. If t=0, every functional on V gives a +relation among the N_j. The surjection `F2^8 -> V` has injective dual, +so the d such relations are independent. Hence + +```text +dim S <= 8-d. (4) +``` + +If t is nonzero, applying a functional taking t to one shows that P +belongs to S. The `(d-1)`-dimensional annihilator of t yields independent +relations in the same way, so + +```text +P in S, dim S <= 9-d. (5) +``` + +Repeated frames and repeated projectors are permitted throughout. + +## 5. A scalar span of dimension at most three compresses to three registers + +Choose a basis of S from actual paid rank-one projectors, and let U +be the span of their image lines. Every N_j has image contained in U, +so every factor acts trivially on the quotient by U. In particular +the formal coefficient P of product-minus-identity has image in U. +Thus + +```text +im P <= U, 3 <= dim U <= dim S <= 3. +``` + +It follows that `U = im P`. Restrict every factor to U. Each projector +retains rank one: its nonzero image vector belongs to U and is fixed +by the idempotent. The restricted endpoint is `[T] I3`, contradicting +the retained three-register theorem. This does not assume clean +workspace or a simultaneously invariant complementary subspace. + +## 6. A four-dimensional scalar span containing P is reducible enough + +Assume `dim S = 4` and `P in S`. Select a basis `N_1,...,N_4` of S +from actual rank-one idempotents. Their binary traces are one, while +`trace(P) = 3 mod 2 = 1`. P's expansion in this basis therefore has +odd Hamming weight. Weight one is impossible because P has rank +three. Relabel so that + +```text +P = N_1 + N_2 + N_3. +``` + +Write `N_i = x_i y_i^T` for i=1,2,3, and set +`X = (x_1 x_2 x_3)` and `Y^T = (y_1^T; y_2^T; y_3^T)`. +Since `P = X Y^T` has rank three, X and Y^T have full column and row +rank. From `P^2 = P`, multiplication by a left inverse of X and a +right inverse of Y^T gives `Y^T X = I3`. Hence these first three +projectors are mutually orthogonal coordinate projectors on im P +and annihilate ker P. + +Write `Q = N_4 = x y^T` and set `U = im P + span{x}`. Every paid +projector has image in U, preserves U, and retains rank one on U. +If U has dimension three, the previous section applies. Otherwise +choose coordinates on U with the first three vectors x_1,x_2,x_3 +and fourth vector `(I-P)x`, which is nonzero and lies in ker P. In +these coordinates + +```text +P = diag(1,1,1,0), +x = (a,1), y^T = (b^T,c), +a dot b + c = 1, a,b in F2^3, c in F2. +``` + +If c=0, the fourth coordinate line is annihilated by Q and by all +three coordinate projectors, and therefore by every paid projector. +Quotienting by that line gives the endpoint `[T] I3`. Each quotient +projector remains rank one. Otherwise its image would lie in the +common annihilated line, making its square zero, contrary to its +being a nonzero idempotent. The retained three-register theorem +again excludes eight calls. + +If c=1, `a dot b = 0`. Because there are three active coordinates, +some i satisfies `a_i b_i = 0`. If `b_i = 0`, the coordinate line +`span(e_i)` is invariant under Q and the coordinate projectors. If +`a_i = 0`, the complementary coordinate hyperplane is invariant. +Thus every paid projector preserves one of these subspaces. The +restriction and quotient endpoints consist of one copy of `[T]` +and two copies of `[T]` plus one dirty identity role, in one order +or the other. + +A rank-one idempotent preserving a subspace induces a rank-one +idempotent on exactly one of restriction and quotient and zero on +the other. Both diagonal blocks are idempotent and their ranks +sum to at most one. They cannot both be zero, since the resulting +strict block triangular matrix would square to zero. Therefore the +eight original calls partition between the two induced words. +Section 2 requires at least `3+6 = 9` calls in total, a contradiction. + +## 7. Exhaustion of cases, shorter words and attainment + +For an eight-call word with rational frame span d, section 3 excludes +`d <= 4` with W=3 active targets. For `d >= 5`, if t=0, (4) gives +`dim S <= 3`, and section 5 applies. If t is nonzero, (5) gives +`P in S` and `dim S <= 4`. Section 5 treats dimension at most three; +section 6 treats dimension four. This covers all rational frames +and every finite amount of restored dirty workspace. + +Every shorter positive-length word can be padded to eight because + +```text +D_N([A]) = D_N([A/2]) D_N([A/2]) +``` + +for an idempotent N; both new frames remain nonzero and rank one. +The zero-length word does not realize (1). Therefore fewer than +nine calls are impossible. + +For attainment, decompose T into its three column matrices +`T = sum_i (T e_i) e_i^T`. Each is nonzero rank one because T is +invertible. Apply these three frames on each of three active scalar +coordinate projectors, fixing every dirty coordinate. The nine +factors give three copies of `[T]`. A binary conjugation gives (1) +for every rank-three idempotent P. + +## 8. Scope, attribution and remaining obligations + +The theorem permits all rational rank-one paid frames, all finite +scalar register counts, arbitrary dirty inputs restored exactly, +and free binary scalar basis changes. It retains the formal +torsion-free abelian address model, binary rank-one idempotent paid +projectors, and three identical invertible dimension-three targets. +It does not prove the corresponding statement for different +targets, four active targets, another address dimension, higher-rank +paid projectors, nonabelian address operations or nonlinear gates. + +The proof depends on Ali Romman's PR468 three-register theorem and +woklerx's PR1456 one-relation theorem. The low-span, flag and Laurent +tools retain the eumemic PR288 / huxint PR203 / Ali Romman lineage. +Tuafo's PR1604 supplies the preceding finite dyadic ternary case; +its alphabet census is not an input to this unrestricted-rational +argument. The new step is the augmentation/scalar-span reduction +and the rank-three idempotent analysis with arbitrary dirty roles. + +This package provides a written extension and finite corroborating +checks, not a fresh full replay of PR468, a Lean proof, physical +supplier admission, a new kappa, or a complete multiplication theorem. +Prepared for Tuafo with substantial OpenAI Codex assistance, +including GPT-6 Astra at maximum reasoning. Apache-2.0. diff --git a/research/bit-identical-three-targets-dirty/README.md b/research/bit-identical-three-targets-dirty/README.md new file mode 100644 index 0000000000..e07ca2f021 --- /dev/null +++ b/research/bit-identical-three-targets-dirty/README.md @@ -0,0 +1,161 @@ +# Three identical rational targets still need nine calls with arbitrary dirty workspace + +**Written extension of a retained computer-assisted theorem. No new kappa or +supplier admission.** In the formal abelian rank-one call model below, three +copies of any invertible rational 3-by-3 target require exactly nine paid +calls, even with any finite number of arbitrary dirty registers that must be +restored. The rational paid frames are unrestricted: no finite alphabet, +numerator bound or denominator bound is imposed. + +This removes the finite-alphabet restriction from the three-identical-target +case of [PR1604](https://github.com/CrocSwap/integer-mult-bounds/pull/1604). +It does not extend the retained theorem to three *different* targets with +dirty workspace. The positive construction search must therefore change +another premise, such as the number of active targets or the address model. + +## Exact statement and model + +Use the group algebra over F2 of the additive group of rational 3-by-3 +matrices. Its formal symbols satisfy `[A][B] = [A+B]`. A paid factor is + +```text +D_N([A]) = I + ([A] - 1) N, +rank_Q(A) = 1, +N in M_R(F2), rank_F2(N) = 1, N^2 = N. +``` + +For every finite `R >= 3`, invertible `T in M_3(Q)`, and rank-three +idempotent `P in M_R(F2)`, the minimum number of factors for + +```text +product_j D_Nj([Aj]) = I + ([T] - 1) P +``` + +is **nine**. In a binary basis adapted to P, this endpoint has three +diagonal copies of `[T]` and `R-3` identity entries. Those additional roles +have arbitrary initial contents and are restored exactly. Equality means +equality of every formal coefficient, not equality after one finite +specialization. Free scalar GL changes are represented by conjugating the +projectors; arbitrary free address maps between calls are outside the model. + +## Proof and predecessor boundary + +[PROOF.md](PROOF.md) supplies the written argument. It uses two named +published inputs, with source pins recorded in [SOURCES.json](SOURCES.json): + +- Ali Romman's [PR468](https://github.com/CrocSwap/integer-mult-bounds/pull/468), + retained in [bit-three-register-lower-bound](../bit-three-register-lower-bound/README.md), + excludes eight calls on exactly three scalar registers. Common rational + left multiplication reduces an identical invertible target T to I3. +- woklerx's [PR1456](https://github.com/CrocSwap/integer-mult-bounds/pull/1456) + at `83b6ad2ace819a96128131a3600ee914a66dd0dd` bounds the sum of target + ranks when the paid frames have at most one rational relation. Its + statement explicitly permits arbitrary register count and zero targets + on restored dirty roles. Together with the low-frame-span argument, it + proves that two active copies of T still need six calls with arbitrary + dirty workspace. + +David Govea’s [PR720](https://github.com/CrocSwap/integer-mult-bounds/pull/720), +at `a942c0ae1b463710ca535c1fba1b07b6431b5a86`, removes target triangularity +for exactly three registers. It does not admit extra dirty registers and is +not a dependency of this identical-target extension. + +The new reduction applies the augmentation ideal to the actual finitely +generated subgroup H of paid frames. It does not reduce rational matrix +entries modulo two or use the augmentation of the divisible ambient group. +For a hypothetical eight-call word with rational frame span d, it gives +`dim span(N_j) <= 8-d` when `T = 0 in H/2H`; otherwise P is in that scalar +span and its dimension is at most `9-d`. + +Low frame spans `d <= 4` are excluded by an explicitly restated extension +of the predecessor's projection argument. For `d >= 5`, only scalar spans +of dimension at most four remain. A scalar span of dimension at most three +restricts to the three-dimensional image of P. In dimension four, P is the +sum of three mutually orthogonal rank-one projectors. The fourth projector +then gives either a three-register quotient or an invariant split into one +active target and two active targets with dirty workspace. The disjoint +call requirements are respectively nine or `3+6`. + +Nine calls attain the bound: write T as its three rank-one column matrices, +and apply all three on each active coordinate role. A binary change of +basis gives the construction for every rank-three P. + +## Evidence and reproduction + +The new proof is a written theorem relying on the two named inputs. The +package's finite checks corroborate its new algebraic reductions and the +nine-call construction; they are not an enumeration of rational frames or +a machine-checked proof of the universal statement. + +```sh +python3.12 -B scripts/research_package.py --package research/bit-identical-three-targets-dirty +python3 -I -O -B research/bit-identical-three-targets-dirty/verify.py +python3 -I -O -B research/bit-identical-three-targets-dirty/independent.py +``` + +The primary checker classifies all 120 binary rank-one idempotents on +four coordinates: 56 active-image cases, 28 common-dirty-kernel cases, +24 invariant-line cases and 12 invariant-hyperplane cases. It checks +28 rank-three projector decompositions, 489 rank-one span members with +multiplicity and 144 induced call partitions. Forbidden rank-one +nilpotent and rank-two paid-projector controls reject. + +The separate checker enumerates all 65,536 binary 4-by-4 matrices and +reproduces those cases, counts and decompositions without importing the +primary implementation. It also replays the full formal nine-call word +at register counts 3, 4 and 7 for a nondiagonal integer target with +determinant 25, including scalar conjugations that mix active and dirty +coordinates. All three omitted-call controls reject, as does a corrupted +case-count fixture. The certificate records the complete finite cases; +verification requires no network fetch. + +Consult the checker output and registered replay receipt for execution +details. This package does not rerun PR468's 21,317,520-order +computer-assisted theorem, the selected supplier's cold replay, native +physical admission, or a Lean proof. Separate proof review and separate +finite implementations were performed by AI agents, not independent human +reviewers. [TASK.json](TASK.json) records the research scope. + +For the proposed three-target dimension-three kernel, even the ideal +overhead-free normalized moment is + +```text +9 * (1/3)^(1-a) / 3 = 3^a. +``` + +It cannot be below one for positive a. Extra restoration, routing or +precision costs cannot rescue this particular route. This is a statement +about the declared kernel model, not a lower bound for integer +multiplication or for other supplier contracts. + +## Open next questions + +- **Four identical targets in eleven calls.** A four-target construction + would escape the three-target theorem and has favorable ideal moment + `(11/12) * 3^a`. A first bounded step is an exact formal search with + four active roles and a specified scalar alphabet containing at least + two noncoordinate projectors, followed by a full paid invoice for + any witness. The three-target argument fails at a + precise point: four active coordinates can have `a_i b_i = 1` for every + i while `a dot b = 0`, so it no longer forces an invariant coordinate + line or complementary hyperplane. No eleven-call construction or + physical admission is asserted here. +- **Different three-dimensional targets with dirty workspace.** The + augmentation identity has several target exponent classes instead of + one tensor `t tensor P`. A first step is to derive the corresponding + scalar-span restriction. The present identical-target reduction does + not establish that case. + +## Credit and license + +Ali Romman's PR468 supplies the retained three-register theorem and the +projection/rank tools. Its model and flag-method lineage is credited to +eumemic's [PR288](https://github.com/CrocSwap/integer-mult-bounds/pull/288) +and huxint's [PR203](https://github.com/CrocSwap/integer-mult-bounds/pull/203). +woklerx's PR1456 supplies the arbitrary-register one-relation theorem. +Tuafo's PR1604, head `c5f5bef84f6648d5573f801c283e01a333ea5f89`, is the +preceding finite dyadic ternary-frame result and remains separately +credited; its finite census is not reused as an unrestricted-rational +proof. Prepared for Tuafo with substantial OpenAI Codex assistance, +including GPT-6 Astra at maximum reasoning for derivation, independent +implementation and proof review. New material is Apache-2.0. diff --git a/research/bit-identical-three-targets-dirty/SOURCES.json b/research/bit-identical-three-targets-dirty/SOURCES.json new file mode 100644 index 0000000000..1540017721 --- /dev/null +++ b/research/bit-identical-three-targets-dirty/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "81e81af67714bdc8d1693b0bf5c29468b92f62ff", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ], + "external_theorems": [ + { + "pr": 1456, + "author": "woklerx", + "commit": "83b6ad2ace819a96128131a3600ee914a66dd0dd", + "path": "research/bit-one-relation-any-registers/PROOF.md", + "git_blob": "9b42c6cd2e93514bd8c5247e2ef2d516d6603ae6", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/83b6ad2ace819a96128131a3600ee914a66dd0dd/research/bit-one-relation-any-registers/PROOF.md", + "use": "At most one rational frame relation, arbitrary scalar register count and zero target frames for restored dirty roles.", + "validation": "Exact pinned text read and independently scope-audited; not fetched or replayed by the offline finite verifier." + } + ] +} diff --git a/research/bit-identical-three-targets-dirty/TASK.json b/research/bit-identical-three-targets-dirty/TASK.json new file mode 100644 index 0000000000..bf406e6999 --- /dev/null +++ b/research/bit-identical-three-targets-dirty/TASK.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "81e81af67714bdc8d1693b0bf5c29468b92f62ff", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "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.", + "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": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "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." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "Prove the sharp nine-call minimum for three identical invertible rational 3-by-3 targets with any finite number of arbitrary restored dirty scalar registers, arbitrary nonzero rational rank-one frames, and binary rank-one idempotent couplings in the formal additive group algebra.", + "scope_change_reason": "Remove the three-register restriction while retaining the abelian operation alphabet and specializing to identical invertible targets. This generalizes the finite ternary half-integral domain in PR1604; it is a structural side result, not a positive supplier.", + "bottleneck_link": "An eight-call collective would have optimistic moment (8/9)*3^a before native realization costs. The theorem rules out that route for every rational rank-one alphabet and every finite dirty workspace, directing positive search toward distinct targets, more active targets or changed paid primitives.", + "budget_minutes": null, + "stop_rule": "Complete a proof covering every rational frame-span dimension and every finite dirty space; require a separate proof audit, independent finite scalar replay, full formal nine-call attainability controls and explicit predecessor scope. Do not claim a positive supplier or kappa change.", + "outcome": "negative-result", + "evidence": "PROOF.md is the arbitrary-domain mathematical argument, using the retained three-register theorem and pinned PR1456. verify.py and independent.py separately check 120 effective projectors, 28 rank-three decompositions, 489 rank-one span members and 144 disjoint call partitions. independent.py also checks formal nine-call endpoints in 3,4,7 registers and rejects omitted calls. These finite checks corroborate the new scalar reduction; they do not replace the written proof or replay the full inherited theorem.", + "author": "Tuafo", + "ai_assistance": "Prepared for Tuafo with substantial OpenAI Codex GPT-6 and GPT-6 Astra assistance in derivation, independent proof review, exact implementations and source audit.", + "open_questions": [ + { + "question": "Can distinct invertible lower-triangular targets use eight calls with restored dirty registers?", + "why_it_matters": "The common rank-three target projector is essential to the new four-dimensional scalar-space reduction.", + "first_step": "Specify three unequal targets and one dirty register, then search a bounded scalar alphabet after a full native adaptation and moment budget.", + "blocked_by": "A formal exact word and a complete implementation of its per-role target adapters are missing." + }, + { + "question": "Can four identical targets use eleven rank-one calls with restored dirt?", + "why_it_matters": "The odd rank-three trace and parity step does not directly generalize to four active targets.", + "first_step": "Derive scalar-space constraints and reject alphabets with separating dirty contrast rows before relation-space search.", + "blocked_by": "No exact improving word or native admission certificate is established." + } + ], + "coordination": { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1594#discussioncomment-18914574", + "finite_predecessor_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/1604", + "note": "New general theorem; finite predecessor preserved. No priority claim for inherited low-span or one-relation lemmas." + }, + "overlap": { + "snapshot_utc": "2026-10-14T04:16:52.056461+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T04:15:42.416510+00:00", + "complete_pagination": true, + "records": 733 + }, + "discussions": { + "fetched_at": "2026-10-14T04:16:51.943976+00:00", + "complete_pagination": true, + "records": 259 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "nearest_work": [ + { + "pr": 468, + "scope": "Retained exactly-three-register theorem; used as named dependency." + }, + { + "pr": 1456, + "head": "83b6ad2ace819a96128131a3600ee914a66dd0dd", + "scope": "At most one rational frame relation, arbitrary registers; used as named dependency." + }, + { + "pr": 1604, + "head": "c5f5bef84f6648d5573f801c283e01a333ea5f89", + "scope": "Finite half-integral ternary alphabet; preceding result now generalized." + }, + { + "pr": 720, + "head": "a942c0ae1b463710ca535c1fba1b07b6431b5a86", + "scope": "Arbitrary invertible targets on exactly three registers; does not add arbitrary dirty space." + } + ] + } +} diff --git a/research/bit-identical-three-targets-dirty/VERIFY.json b/research/bit-identical-three-targets-dirty/VERIFY.json new file mode 100644 index 0000000000..00f807355c --- /dev/null +++ b/research/bit-identical-three-targets-dirty/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact finite scalar-reduction census, immutable receipt equality and forbidden rank/projector controls; written theorem is not replaced by this finite check." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Code-disjoint enumeration of all 2^16 binary matrices, scalar cases, coefficientwise formal nine-call endpoints in 3/4/7 roles and omitted-call controls." + } + ] +} diff --git a/research/bit-identical-three-targets-dirty/independent.py b/research/bit-identical-three-targets-dirty/independent.py new file mode 100644 index 0000000000..193877a06e --- /dev/null +++ b/research/bit-identical-three-targets-dirty/independent.py @@ -0,0 +1,170 @@ +"""Separate tuple-matrix check of the scalar reduction and nine-call endpoint. + +Enumerates all 2^16 binary matrices rather than outer-product parameters. +No primary-checker import. Finite corroboration, not a proof of all rational words. +Prepared for Tuafo with substantial OpenAI assistance. Apache-2.0. +""" +import itertools +import json +from pathlib import Path + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def zero(n): + return tuple(tuple(0 for _ in range(n)) for _ in range(n)) + + +def identity(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def plus(a, b): + return tuple(tuple(x ^ y for x, y in zip(r, s)) for r, s in zip(a, b)) + + +def times(a, b): + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(len(b))) % 2 + for j in range(len(b))) for i in range(len(a))) + + +def dimension(a): + rows = [list(r) for r in a] + pivot = 0 + for j in range(len(rows[0]) if rows else 0): + found = next((i for i in range(pivot, len(rows)) if rows[i][j]), None) + if found is None: + continue + rows[pivot], rows[found] = rows[found], rows[pivot] + for i in range(pivot + 1, len(rows)): + if rows[i][j]: + rows[i] = [x ^ y for x, y in zip(rows[i], rows[pivot])] + pivot += 1 + return pivot + + +def submatrix(a, ids): + return tuple(tuple(a[i][j] for j in ids) for i in ids) + + +def rank_one_projection(a): + return dimension(a) == 1 and times(a, a) == a + + +def check_scalar(): + z = zero(4) + p = tuple(tuple(int(i == j and i < 3) for j in range(4)) for i in range(4)) + axes = [tuple(tuple(int(i == j == k) for j in range(4)) for i in range(4)) for k in range(3)] + alphabet = [] + for entries in itertools.product((0, 1), repeat=16): + a = tuple(tuple(entries[4*i:4*i+4]) for i in range(4)) + nonzero = {row for row in a if any(row)} + if len(nonzero) == 1 and sum(a[i][i] for i in range(4)) % 2: + need(rank_one_projection(a), 'Alphabet membership') + alphabet.append(a) + need(len(alphabet) == 120, 'Complete binary matrix census') + index = {a: i for i, a in enumerate(alphabet)} + triples = 0 + for i, a in enumerate(alphabet): + for j in range(i+1, len(alphabet)): + b = alphabet[j] + c = plus(p, plus(a, b)) + if c not in index or index[c] <= j: + continue + for x in (a, b, c): + for y in (a, b, c): + need(times(x, y) == (x if x == y else z), 'Orthogonal decomposition') + triples += 1 + need(triples == 28, 'Rank-three decomposition count') + records = [] + checked = partitioned = 0 + for q in alphabet: + first = next(row for row in q if any(row)) + u = sum(int(any(row)) << i for i, row in enumerate(q)) + v = sum(x << i for i, x in enumerate(first)) + pool = set() + for bits in itertools.product((0, 1), repeat=4): + a = z + for enabled, b in zip(bits, axes+[q]): + if enabled: + a = plus(a, b) + if rank_one_projection(a): + pool.add(a) + checked += len(pool) + if not any(q[3]): + kind, ids = 'active_image', None + for a in pool: + need(not any(a[3]) and rank_one_projection(submatrix(a, [0,1,2])), 'Active restriction') + elif all(q[i][3] == 0 for i in range(4)): + kind, ids = 'dirty_common_kernel', None + for a in pool: + need(all(a[i][3] == 0 for i in range(4)), 'Common kernel') + need(rank_one_projection(submatrix(a, [0,1,2])), 'Quotient projector') + else: + i = next(i for i in range(3) if q[i][i] == 0) + if first[i] == 0: + kind, ids = 'active_line', [i] + else: + kind, ids = 'active_hyperplane', [j for j in range(4) if j != i] + rest = [j for j in range(4) if j not in ids] + need(sorted([dimension(submatrix(p, ids)), dimension(submatrix(p, rest))]) == [1,2], 'Target partition') + for a in pool: + need(all(a[r][c] == 0 for r in rest for c in ids), 'Invariant subspace') + b, c = submatrix(a, ids), submatrix(a, rest) + need(times(b,b) == b and times(c,c) == c, 'Induced idempotents') + need(sorted([dimension(b),dimension(c)]) == [0,1], 'Disjoint call partition') + partitioned += 1 + records.append(dict(u=u, v=v, case=kind, rank_one_members=len(pool), invariant_coordinates=ids)) + receipt = json.loads(Path(__file__).with_name('CERTIFICATE.json').read_text(encoding='utf-8')) + need(sorted(records, key=lambda r:(r['u'],r['v'])) == receipt['cases'], 'Exact case receipt comparison') + need(checked == 489 and partitioned == 144, 'All member counts') + altered = [dict(r) for r in receipt['cases']] + altered[0]['rank_one_members'] += 1 + need(sorted(records, key=lambda r:(r['u'],r['v'])) != altered, 'Count corruption not detected') + return dict(idempotents=120, decompositions=triples, span_members=checked, call_partitions=partitioned) + + +def formal_word(n, factors): + origin = (0,)*9 + result = {origin: identity(n)} + for address, projector in factors: + new = {} + for exponent, coefficient in result.items(): + for offset, local in ((origin,plus(identity(n),projector)), (address,projector)): + key = tuple(x+y for x,y in zip(exponent,offset)) + new[key] = plus(new.get(key,zero(n)), times(coefficient,local)) + result = {k:v for k,v in new.items() if any(any(row) for row in v)} + return result + + +def check_attainment(): + # This integer target has determinant25 and is not diagonal. + target = (1,2,0, 0,1,3, 4,0,1) + need(target[0]*(target[4]*target[8]-target[5]*target[7])-target[1]*(target[3]*target[8]-target[5]*target[6])+target[2]*(target[3]*target[7]-target[4]*target[6]) == 25, 'Invertible target') + columns = [tuple(target[3*i+j] if j == k else 0 for i in range(3) for j in range(3)) for k in range(3)] + for n in (3,4,7): + # Involutory scalar basis change, mixing active and dirty coordinates. + s = [list(r) for r in identity(n)] + for j in range(1,n): + s[0][j] = 1 + s = tuple(map(tuple,s)) + need(times(s,s) == identity(n), 'Conjugating basis') + factors, p = [], zero(n) + for active in range(3): + e = tuple(tuple(int(i == j == active) for j in range(n)) for i in range(n)) + q = times(times(s,e),s) + need(rank_one_projection(q), 'Paid projector') + p = plus(p,q) + factors.extend((a,q) for a in columns) + expected = {(0,)*9:plus(identity(n),p), target:p} + expected = {k:v for k,v in expected.items() if any(any(row) for row in v)} + need(formal_word(n,factors) == expected, 'Full formal nine-call endpoint') + need(formal_word(n,factors[:-1]) != expected, 'Omitted-call control') + return dict(nine_call_register_counts=[3,4,7], exact_formal_non_diagonal_target=True, omitted_call_controls=3) + + +if __name__ == '__main__': + print('PASS_INDEPENDENT_IDENTICAL_THREE_DIRTY ' + json.dumps(dict(scalar=check_scalar(), attainment=check_attainment()), sort_keys=True)) diff --git a/research/bit-identical-three-targets-dirty/verify.py b/research/bit-identical-three-targets-dirty/verify.py new file mode 100644 index 0000000000..679e95341a --- /dev/null +++ b/research/bit-identical-three-targets-dirty/verify.py @@ -0,0 +1,191 @@ +"""Exact finite corroboration of IDENTICAL-TARGET-LEMMA's new scalar step. + +This checks every effective four-dimensional extra rank-one idempotent, +every rank-one element in each resulting scalar span, and every rank-three +projector decomposition in the fixed P chart. It is not a finite proof of +the arbitrary-register or unrestricted-rational theorem by itself. +Standard library only. Prepared with substantial OpenAI Codex assistance. +""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def outer(u, v, n): + return tuple(v if u >> i & 1 else 0 for i in range(n)) + + +def add(*matrices): + return tuple(__import__("functools").reduce(int.__xor__, row, 0) + for row in zip(*matrices)) + + +def mul(a, b): + return tuple(__import__("functools").reduce( + int.__xor__, (b[j] for j in range(len(b)) if row >> j & 1), 0) + for row in a) + + +def rank(rows): + basis = {} + for row in rows: + while row: + p = row.bit_length() - 1 + if p in basis: + row ^= basis[p] + else: + basis[p] = row + break + return len(basis) + + +def apply(matrix, vector): + return sum(((row & vector).bit_count() & 1) << i + for i, row in enumerate(matrix)) + + +def projector(matrix): + return rank(matrix) == 1 and mul(matrix, matrix) == matrix + + +def span(matrices): + result = {tuple(0 for _ in matrices[0])} + for matrix in matrices: + result |= {add(current, matrix) for current in tuple(result)} + return sorted(result) + + +def block(matrix, coordinates): + return tuple(sum(((matrix[i] >> j) & 1) << k + for k, j in enumerate(coordinates)) + for i in coordinates) + + +def invariant_coordinate_set(matrix, coordinates): + allowed = set(coordinates) + return all(not (matrix[i] >> j & 1) + for j in coordinates for i in range(len(matrix)) + if i not in allowed) + + +def check(): + n = 4 + zero = (0,) * n + active = (1, 2, 4, 0) + axes = [outer(1 << i, 1 << i, n) for i in range(3)] + factors = [(u, v, outer(u, v, n)) for u in range(1, 16) + for v in range(1, 16) if (u & v).bit_count() & 1] + require(len(factors) == 120, "Wrong complete idempotent alphabet") + require(len({m for _, _, m in factors}) == 120, "Duplicate factorization") + require(all(projector(m) for _, _, m in factors), "Invalid alphabet") + + decompositions = [] + matrices = [m for _, _, m in factors] + for ids in itertools.combinations(range(120), 3): + triple = [matrices[i] for i in ids] + if add(*triple) != active: + continue + for i, a in enumerate(triple): + require(mul(active, a) == a and mul(a, active) == a, + "Rank-three decomposition escaped active support") + for j, b in enumerate(triple): + require(mul(a, b) == (a if i == j else zero), + "Rank-three decomposition is not orthogonal") + decompositions.append(ids) + require(len(decompositions) == 28, "Unexpected decomposition count") + + counts = {"active_image": 0, "dirty_common_kernel": 0, + "active_line": 0, "active_hyperplane": 0} + cases = [] + checked_members = 0 + partitioned_members = 0 + for u, v, extra in factors: + pool = [m for m in span(axes + [extra]) if projector(m)] + checked_members += len(pool) + if not (u & 8): + case = "active_image" + for m in pool: + require(m[3] == 0, "Image leaves active subspace") + require(projector(block(m, [0, 1, 2])), + "Active restriction lost rank-one idempotence") + witness = None + elif not (v & 8): + case = "dirty_common_kernel" + for m in pool: + require(apply(m, 8) == 0, "Dirty line is not common kernel") + require(projector(block(m, [0, 1, 2])), + "Common-kernel quotient lost idempotence") + witness = None + else: + require(((u & v) & 7).bit_count() % 2 == 0, + "Active overlap must have even parity") + i = next(j for j in range(3) if not (u & v & (1 << j))) + if not (v & (1 << i)): + case = "active_line" + coords = [i] + else: + case = "active_hyperplane" + coords = [j for j in range(4) if j != i] + rest = [j for j in range(4) if j not in coords] + require(sorted([rank(block(active, coords)), + rank(block(active, rest))]) == [1, 2], + "Target split is not one plus two") + for m in pool: + require(invariant_coordinate_set(m, coords), + "Selected flag is not invariant for whole scalar span") + left, right = block(m, coords), block(m, rest) + require(mul(left, left) == left and mul(right, right) == right, + "Diagonal block idempotence failed") + require(sorted([rank(left), rank(right)]) == [0, 1], + "Paid factor does not partition between blocks") + partitioned_members += 1 + witness = coords + counts[case] += 1 + cases.append({"u": u, "v": v, "case": case, + "rank_one_members": len(pool), "invariant_coordinates": witness}) + + # This one forbidden nilpotent would destroy the parity inference: + # J4 has all three active overlaps equal to one, but has trace zero. + nilpotent = outer(15, 15, 4) + require(rank(nilpotent) == 1 and mul(nilpotent, nilpotent) == zero, + "Nilpotent mutation fixture is wrong") + require(not projector(nilpotent), "Nilpotent mutation accepted") + # A rank-two paid projector cannot use the one-call partition rule. + rank_two = add(axes[0], axes[1]) + require(rank(rank_two) == 2 and not projector(rank_two), + "Rank-two paid-call mutation accepted") + + receipt = { + "status": "FINITE_CORROBORATION_OF_WRITTEN_SCALAR_REDUCTION", + "idempotents": len(factors), + "rank_three_projector_decompositions": len(decompositions), + "effective_extra_projector_cases": counts, + "rank_one_span_members_checked_with_multiplicity": checked_members, + "call_partitions_checked_with_multiplicity": partitioned_members, + "forbidden_controls_rejected": ["rank_one_nilpotent", "rank_two_projector"], + "cases": cases, + } + canonical = json.dumps(receipt, sort_keys=True, separators=(",", ":")) + receipt["canonical_payload_sha256"] = hashlib.sha256(canonical.encode()).hexdigest() + return receipt + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="Regenerate the explicit finite receipt") + args = parser.parse_args() + result = check() + output = Path(__file__).with_name("CERTIFICATE.json") + if args.write: + output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8", newline="\n") + else: + require(json.loads(output.read_text(encoding="utf-8")) == result, "Finite receipt differs from exact recomputation") + print("PASS_IDENTICAL_THREE_DIRTY_FINITE_CHECK " + json.dumps({k: v for k, v in result.items() if k != "cases"}, sort_keys=True))