From 29e4d3a25225a219f97c3a2815ed3a5a8fd9b891 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:04:17 +0100 Subject: [PATCH] feat(research): prove semilocal right-vector cost formula --- research/right-vector-semilocal/PROOF.md | 161 ++++++++++ research/right-vector-semilocal/README.md | 107 +++++++ research/right-vector-semilocal/SOURCES.json | 30 ++ research/right-vector-semilocal/TASK.json | 70 +++++ research/right-vector-semilocal/VERIFY.json | 35 +++ research/right-vector-semilocal/verify.py | 290 +++++++++++++++++++ 6 files changed, 693 insertions(+) create mode 100644 research/right-vector-semilocal/PROOF.md create mode 100644 research/right-vector-semilocal/README.md create mode 100644 research/right-vector-semilocal/SOURCES.json create mode 100644 research/right-vector-semilocal/TASK.json create mode 100644 research/right-vector-semilocal/VERIFY.json create mode 100644 research/right-vector-semilocal/verify.py diff --git a/research/right-vector-semilocal/PROOF.md b/research/right-vector-semilocal/PROOF.md new file mode 100644 index 0000000000..3cd62bfe98 --- /dev/null +++ b/research/right-vector-semilocal/PROOF.md @@ -0,0 +1,161 @@ +# The semilocal two-role theorem + +Let `K` be a field in the centre of an associative unital algebra `R`. +The paid alphabet is `I+u y^T`, with `u in R^2` and `y in K^2`, and free maps +are common `GL_2(K)` maps. Cost and delta have the meanings of +[#4276](../right-vector-two-factor-criterion/PROOF.md). In particular, + +`delta_R(M) = min_{T in GL_2(K)} dim_K (MT-I)K^2`. + +Assume `R` is semilocal: its Jacobson radical `J` has quotient +`R/J = product_i M_{d_i}(D_i)`, for finitely many division rings `D_i`. +This includes every finite-dimensional `K`-algebra. The quotient contains +the same central field `K`. The zero algebra is excluded. + +## The new statement + +For every `M in GL_2(R)`: + +1. Three paid factors suffice, with the fixed right vectors `e1,e2,e1`. + No free map is needed for this upper bound. +2. `cost_R(M)<=2` holds exactly when `cost_{R/J}(Mbar)<=2`. +3. `cost_R(M)=max(delta_R(M),cost_{R/J}(Mbar))<=3`. + +This settles the semilocal matrix-block question in #4601. That predecessor +proves the formula for products of local algebras. ToikY's #4334 proves the +field-product case and supplies its three-factor construction. The new step +here allows arbitrary matrix blocks in the semisimple quotient and does not +require `R` itself to split as a product of local algebras. The one/two-factor +criteria and delta lower bound are inputs from #4276/#4243/#4099. + +The unit-completion argument below is the classical stable-range-one +argument, included to specify sides and coefficient types. Stable range and +ordinary ring-matrix elimination are not claimed as new. For historical +context see Ara, Pedersen and Perera, [*An infinite analogue of rings with +stable rank one*, introduction](https://arxiv.org/abs/math/9910131v2). +The contribution is its application to this restricted-right-vector cost +question and its exact radical consequence. + +## 1. Units and one-sided inverses + +An element of `R` is a unit exactly when its image modulo `J` is a unit. +Indeed, lift an inverse to `y`, so `xy=1+j` and `yx=1+k` for `j,k in J`. +The elements `1+j` and `1+k` are units by the Jacobson-radical property. +Thus `y(1+j)^(-1)` is a right inverse of `x`, and `(1+k)^(-1)y` is a left +inverse. A left and a right inverse agree. The converse follows by projection. + +Every right-invertible element in `R` is a unit. Project a right inverse to +each finite matrix ring over a division ring, where a right inverse is an +inverse by finite-dimensional linear algebra, and use the preceding paragraph. + +## 2. Complete a unimodular block row to a unit + +Suppose `aR+bR=R`. We prove that some `f in R` makes `a-bf` a unit. +Work first in one quotient block `M_d(D)`, acting on the right vector space +`V=D^d`. Since `aR+bR=R`, `im(a)+im(b)=V`. + +Choose a complement `U` of `ker(a)` in the domain. Then `a` maps `U` +isomorphically onto `im(a)`, and +`dim ker(a)=dim V/im(a)`. The map induced by `b` onto `V/im(a)` is onto. +Choose a right-linear map `f` on `ker(a)` so that `b f`, followed by the +quotient map, is an isomorphism `ker(a) -> V/im(a)`. Extend `f` by zero on +`U`. On `U`, `a-bf=a` has image `im(a)` and is injective. On `ker(a)`, its +image projects isomorphically onto the quotient. Therefore `a-bf` is bijective. + +Make these choices independently in every quotient block. Lift the resulting +element `fbar` to `R`. The lifted `a-bf` has unit residue, so it is a unit by +section 1. In particular, no idempotent lifting or splitting of `R` is assumed. +The coefficient `f` is algebra-valued. Restricting it to `K` is unjustified. + +## 3. Three factors with base-field right vectors + +Write `M=[[a,b],[c,d]]`. Its first block row is right unimodular, because +the first column of `M^(-1)` gives `ax+by=1`. Choose `f` as above and put + +```text +e = a-bf, +g = (c-df)e^(-1), +h = d-gb. + +F1 = [[1,0],[g,1]] = I + (0,g)^T e1^T, +F2 = [[1,b],[0,h]] = I + (b,h-1)^T e2^T, +F3 = [[e,0],[f,1]] = I + (e-1,f)^T e1^T. +``` + +Multiplication in the indicated algebraic order gives + +```text +F1 F2 F3 = [[e+bf,b],[ge+(gb+h)f,gb+h]] + = [[a,b],[c,d]] = M. +``` + +All three right vectors are in `K^2`; the algebra coefficients occur only on +the left. `F1` and `F3` are invertible, since `e` is a unit. Therefore +`F2=F1^(-1) M F3^(-1)` is invertible, which also proves that `h` is a unit. +Every prefix in either product or execution order is invertible. A column +execution applies `F3`, then `F2`, then `F1`. There is no scratch register and +the identity holds on arbitrary input data. + +## 4. The two-factor threshold and radical formula + +By #4276, `cost_R(M)<=2` exactly when some `G,H in GL_2(K)` give `N=GMH` +with `N12 in N11 R`. For an invertible `N`, its first row is right unimodular. +Writing `N12=N11 z` shows that `N11` is right-invertible, hence a unit by +section 1. Conversely, a unit `N11` gives the required ideal membership. +Thus the threshold is equivalent to + +`there are G,H in GL_2(K) for which (GMH)11 is a unit`. + +Equivalently, some common nonzero base-field row `phi` and column `t` have +`phi M t` a unit. Every nonzero row and column extends to an invertible +base-field matrix. The word "common" is essential across quotient blocks. + +Units lift and descend through `J`, and the same `G,H` work on both sides. +This proves item 2. Projection also gives +`cost_R(M)>=cost_{R/J}(Mbar)`. The column bound gives +`cost_R(M)>=delta_R(M)`. + +If the residue cost is 3, the three-factor upper bound proves item 3. +Otherwise item 2 gives `cost_R(M)<=2`. If `delta_R(M)<=1`, #4276's one-factor +theorem gives `cost_R(M)=delta_R(M)`; projection makes the residue cost no +larger. If `delta_R(M)=2`, both sides of item 3 equal 2. These exhaust the +possibilities, since `delta_R(M)<=2`. + +## 5. A matrix-block family attaining three + +Take `R0=M_2(F_2)` and the established #4265/#4276 sharp target + +```text +a=E11, b=E01, c=E10, d=E00, +``` + +where indices are 0,1. The flattened 4x4 matrix exchanges coordinates 0 and 3. +All nine common base-field row/column pivots are singular. For example, +`a-bf` is singular for both scalar choices `f=0,I`, whereas `f=E10` gives +`a-bf=I`. This is a fixture distinguishing the matrix-block +completion from a scalar-only pivot choice. Its sharp residue cost is +predecessor credit, not a new counterexample. + +Now take the new lifting family `R=M_2(F_2[e]/e^2)`. For every +`X in M_4(F_2)`, let `M_X=M_0+eX`, viewed as a 2x2 matrix over `R`. +Its residue `M_0` is invertible. Explicitly + +`M_X^(-1)=M_0^(-1)-e M_0^(-1)X M_0^(-1)`. + +All `2^16=65,536` targets are distinct and invertible. Items 1 and 2 prove +that every one costs exactly 3. The verifier enumerates each lift, checks +every common pivot, constructs its actual three-factor word using the lifted +pivot inverse, and checks its action on all eight binary basis coordinates. +It also constructs words for all 20,160 elements of `GL_4(F_2)` in the +matrix-block residue ring. These are finite corroborations of the written +theorem; they do not establish an unbounded theorem by enumeration. + +## Limits + +The target must be invertible, the role count is two, and `R` is semilocal. +This does not settle the singular-target question of #4276/#4601. The +construction is a formal alphabet with unpriced algebra-valued left vectors +and common free base-field maps. Preparation, conversion, routing, control, +precision, restoration and stock costs for a native implementation are unknown. +No supplier admission, new kappa or complete multiplication theorem follows. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/right-vector-semilocal/README.md b/research/right-vector-semilocal/README.md new file mode 100644 index 0000000000..66f8077f44 --- /dev/null +++ b/research/right-vector-semilocal/README.md @@ -0,0 +1,107 @@ +# Three right-vector factors suffice over every semilocal algebra + +Claim type: scoped proof, with finite constructive certificates. No new kappa. + +For every semilocal associative algebra `R` over a central field `K`, and every +invertible two-role target `M`, the right-vector alphabet has + +```text +cost_R(M) = max(delta_R(M), cost_(R/J)(Mbar)) <= 3, +``` + +where `J` is the Jacobson radical. In particular, the two-factor threshold is +unchanged modulo `J`. This includes every finite-dimensional algebra, with +arbitrary matrix blocks in its semisimple quotient. Three factors with right +vectors `e1,e2,e1` suffice without using a free map. + +This answers Open next question 1 of +[PR4601](https://github.com/CrocSwap/integer-mult-bounds/pull/4601), at head +`4b2322fc5bd30a129507c2eee69aa275527b69ac`. That result covers products of +local algebras. The present proof removes that restriction. It does not +recheck its enumeration. The complete argument and explicit word are in +[PROOF.md](PROOF.md). + +## Model and evidence + +Paid factors are `I+u y^T`, with `u in R^2` and `y in K^2`; common +`GL_2(K)` maps are free. There are two data roles and no scratch roles. +The unit completion uses an algebra-valued left coefficient. The right +vectors and free charts remain base-field-valued and common across blocks. + +The new constructor is checked on: + +- Every one of the 20,160 invertible targets over `M_2(F_2)`. +- All 65,536 radical lifts of one fixed sharp residue target to + `M_2(F_2[e]/e^2)`. Every lift has exact cost 3, from the cited two-factor + criterion and the new attaining word. +- Each word both as block-ring multiplication and as an independent action + on all eight binary basis coordinates. Seven negative controls cover scalar + completion, word order, an omitted factor, residue-only substitution, + an uncorrected residue inverse, a singular input and the sign over `F_3`. + +A separate 96-target binary dual-number compatibility control gives cost +histogram `[6,54,36,0]`, agreeing numerically with the shared control reported +by open #4601 and #4613. It evaluates the formula on scalar matrices embedded +in the matrix-block algebra. It does not replay either predecessor's engines. + +The universal claim is a written proof. The finite certificates corroborate +its construction and do not replace it. The verifier imports no predecessor +code, writes no files, checks the two pinned source documents, and prints a +fresh receipt bound to every package file and the regenerated word digests. + +## Reproduce + +From the repository root, using the Python 3.12 standard library: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-semilocal/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-semilocal/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-semilocal +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-semilocal --check-source-history +``` + +Expected marker: `PASS_RIGHT_VECTOR_SEMILOCAL`, with residue `targets=20160` +and radical `targets=exact_cost_three=65536`. Both registered commands retain +checks under optimized Python. + +## Limitations + +The theorem requires invertible targets, two roles and a semilocal algebra. +It does not classify singular targets or algebras outside that class. +Native preparation, conversion, routing, control, precision, restoration and +stock costs remain unknown. No supplier, selected-frontier change or complete +multiplication theorem is claimed. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker and the selected operator replay are not +part of this result. + +The verifier uses managed Python allocation. Its tables contain 65,536 ring +products and 256 inverse entries. Every census streams at most 65,536 targets, +with eight-coordinate matrices and constant-size digests. All loops have +fixed bounds, no recursion or dynamic code is used, functions are below +60 lines, and warnings are errors in both registered commands. A fixed-memory +implementation would be needed only if this verifier were moved into a runtime +that forbids allocation; no native real-time guarantee is made here. + +## Open next questions + +1. Classify reachable singular targets over matrix-block radical extensions. + This would extend the exact cost decision beyond invertible targets. + First test the three-factor image over `M_2(F_2[e]/e^2)` on a named singular + residue family. The unit-pivot argument used here does not apply. The + square-zero local singular-target question is separately claimed; check live + overlap before starting. +2. Bind one such word to a literal native producer and consumer. First state + and price how its algebra-valued left coefficients are prepared. All physical + costs listed above are blockers, so this theorem does not authorize a larger + construction campaign. + +## Credit + +This contribution was produced by Nick Petalas. Nick Petalas's #4601 supplies +the local-product theorem and explicit semilocal question; #4276 supplies the +one/two-factor criteria, following #4265/#4243. ToikY's #4334 supplies the +field-product three-factor theorem and its construction. Wentao Li's #4099 +supplies the alphabet and column bound, building on #2513. The stable-range +unit completion and ordinary ring-matrix elimination are classical. Their +application to the semilocal restricted-right-vector cost formula is proved +here. Apache-2.0. diff --git a/research/right-vector-semilocal/SOURCES.json b/research/right-vector-semilocal/SOURCES.json new file mode 100644 index 0000000000..1af6a7cdfc --- /dev/null +++ b/research/right-vector-semilocal/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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/right-vector-commutative-products/PROOF.md", + "usage": "input", + "git_blob": "f149515c1684ac16bcb1ef0fd014b98d6f92f5db", + "sha256": "b401a15bc3a11e2040cdde9d99d4a5b8ec7b4f92643eac547f21b7c667fbf408" + }, + { + "path": "research/right-vector-two-factor-criterion/PROOF.md", + "usage": "input", + "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c", + "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895" + } + ] +} diff --git a/research/right-vector-semilocal/TASK.json b/research/right-vector-semilocal/TASK.json new file mode 100644 index 0000000000..1283d3d2ad --- /dev/null +++ b/research/right-vector-semilocal/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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 three-factor upper bound and radical cost formula for invertible two-role right-vector targets over every semilocal central K-algebra.", + "scope_change_reason": "Take the explicit semilocal matrix-block question of PR4601. This is a formal-alphabet algebraic side result, with no native supplier implementation or larger-register construction.", + "bottleneck_link": "Side result: it settles a formal right-vector interface question. Native left-coefficient preparation and all physical supplier costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved semilocal extension and bounded constructive check; do not pursue a new supplier or singular-target classification.", + "outcome": "completed", + "evidence": "PROOF.md gives the universal argument. verify.py constructs words on all 20160 invertible M2(F2) targets and all 65536 radical lifts of one sharp target, with independent faithful actions and seven negative controls. The shared 96-target binary dual-number compatibility histogram [6,54,36,0] agrees with PR4601 and PR4613.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Classify reachable singular targets over matrix-block radical extensions.", + "why_it_matters": "The current exact cost formula assumes invertibility.", + "first_step": "After live overlap checks, choose one singular residue family over M2(F2[e]/e^2) and describe its three-factor image.", + "blocked_by": "No unit completion follows for a singular first block row; the square-zero local singular question is already separately claimed." + }, + { + "question": "Realize an algebra-valued left coefficient in a literal native caller.", + "why_it_matters": "Formal factors alone do not change a paid supplier invoice.", + "first_step": "Specify and price coefficient preparation for one producer/consumer pair.", + "blocked_by": "Preparation, conversion, routing, control, precision, restoration and stock are all unpriced." + } + ] +} diff --git a/research/right-vector-semilocal/VERIFY.json b/research/right-vector-semilocal/VERIFY.json new file mode 100644 index 0000000000..89a3efd519 --- /dev/null +++ b/research/right-vector-semilocal/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/right-vector-commutative-products/PROOF.md", + "research/right-vector-two-factor-criterion/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 20160 GL4(F2) words, all 65536 sharp radical lifts with nine-pivot lower bounds and independent eight-coordinate actions, and seven negative controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete checks remain active under optimized Python." + } + ] +} diff --git a/research/right-vector-semilocal/verify.py b/research/right-vector-semilocal/verify.py new file mode 100644 index 0000000000..4d34a6ffd8 --- /dev/null +++ b/research/right-vector-semilocal/verify.py @@ -0,0 +1,290 @@ +#!/usr/bin/env python3 +"""Construct semilocal three-factor words on finite matrix-block fixtures. + +Produced by Nick Petalas. Apache-2.0. +This checks this package's new construction, not a predecessor's census. +""" + +from hashlib import sha256 +import json +from pathlib import Path + + +ONE = 9 # I_2 in row-major binary coordinates. +SHARP = (8, 2, 4, 1) # The 4x4 permutation exchanging coordinates 0 and 3. + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def binary_product(a, b): + """Multiply two 2x2 binary matrices encoded in four bits.""" + return sum( + (sum(((a >> (2*i+k)) & 1) * ((b >> (2*k+j)) & 1) + for k in range(2)) % 2) << (2*i+j) + for i in range(2) for j in range(2) + ) + + +def tables(): + """R=M_2(F_2[e]/e^2): low nibble is residue, high is e coefficient.""" + base = tuple(tuple(binary_product(a, b) for b in range(16)) + for a in range(16)) + inverse = [-1] * 256 + for a in range(16): + for b in range(16): + if base[a][b] == base[b][a] == ONE: + for radical in range(16): + inverse[a | (radical << 4)] = ( + b | (base[base[b][radical]][b] << 4)) + multiplication = tuple(tuple( + base[x & 15][y & 15] + | ((base[x & 15][y >> 4] ^ base[x >> 4][y & 15]) << 4) + for y in range(256)) for x in range(256)) + for x in range(256): + if inverse[x] >= 0: + require(multiplication[x][inverse[x]] == ONE + and multiplication[inverse[x]][x] == ONE, "unit inverse") + return multiplication, tuple(inverse) + + +def product(a, b, mul): + return ( + mul[a[0]][b[0]] ^ mul[a[1]][b[2]], + mul[a[0]][b[1]] ^ mul[a[1]][b[3]], + mul[a[2]][b[0]] ^ mul[a[3]][b[2]], + mul[a[2]][b[1]] ^ mul[a[3]][b[3]], + ) + + +def factors(target, mul, inverse): + """Use the residue completion f and the actual lifted pivot inverse.""" + a, b, c, d = target + for f in range(16): + pivot = a ^ mul[b][f] + if inverse[pivot] >= 0: + lower = mul[c ^ mul[d][f]][inverse[pivot]] + last = d ^ mul[lower][b] + require(inverse[last] >= 0, "Schur remainder must be a unit") + return ((ONE, 0, lower, ONE), (ONE, b, 0, last), + (pivot, 0, f, ONE)) + raise ValueError("no unit completion in the residue algebra") + + +def flatten(matrix): + """Independent faithful action on eight binary coordinates, x0 then e*x1.""" + rows = [0] * 8 + for i in range(4): + for j in range(4): + block = matrix[2*(i//2) + j//2] + offset = 2*(i % 2) + j % 2 + residue = (block >> offset) & 1 + radical = (block >> (4+offset)) & 1 + rows[i] |= residue << j + rows[i+4] |= (radical << j) | (residue << (j+4)) + return tuple(rows) + + +def compose_rows(a, b): + rows = [0] * 8 + for i in range(8): + for j in range(8): + if (a[i] >> j) & 1: + rows[i] ^= b[j] + return tuple(rows) + + +def check_word(target, word, mul): + f1, f2, f3 = word + require(f1[0:2] == (ONE, 0) and f1[3] == ONE, "first e1 factor") + require(f2[0] == ONE and f2[2] == 0, "middle e2 factor") + require(f3[1] == 0 and f3[3] == ONE, "last e1 factor") + require(product(product(f1, f2, mul), f3, mul) == target, "block endpoint") + independent = compose_rows(compose_rows(flatten(f1), flatten(f2)), flatten(f3)) + require(independent == flatten(target), "all eight binary basis columns") + + +def invertible_rows(code): + rows = [(code >> (4*i)) & 15 for i in range(4)] + pivot = 0 + for col in range(4): + found = next((i for i in range(pivot, 4) if (rows[i] >> col) & 1), None) + if found is not None: + rows[pivot], rows[found] = rows[found], rows[pivot] + for i in range(4): + if i != pivot and (rows[i] >> col) & 1: + rows[i] ^= rows[pivot] + pivot += 1 + return pivot == 4 + + +def blocks(code): + out = [0] * 4 + for i in range(4): + for j in range(4): + bit = (code >> (4*i+j)) & 1 + out[2*(i//2)+j//2] |= bit << (2*(i % 2)+j % 2) + return tuple(out) + + +def unit_pivots(target, inverse): + """All nine common nonzero F2 rows/columns from the cited criterion.""" + count = 0 + for row in range(1, 4): + for column in range(1, 4): + entry = 0 + for i in range(2): + for j in range(2): + if ((row >> i) & 1) and ((column >> j) & 1): + entry ^= target[2*i+j] + count += inverse[entry] >= 0 + return count + + +def residue_census(mul, inverse): + count = 0 + digest = sha256() + for code in range(1 << 16): + if invertible_rows(code): + target = blocks(code) + word = factors(target, mul, inverse) + check_word(target, word, mul) + digest.update(bytes(target + sum(word, ()))) + count += 1 + require(count == 20160, "complete GL4(F2) enumeration") + return {"targets": count, "word_sha256": digest.hexdigest()} + + +def radical_census(mul, inverse): + count = 0 + digest = sha256() + for code in range(1 << 16): + target = tuple(SHARP[i] | (((code >> (4*i)) & 15) << 4) + for i in range(4)) + require(unit_pivots(target, inverse) == 0, "cost-three lift lower bound") + word = factors(target, mul, inverse) + check_word(target, word, mul) + digest.update(bytes(target + sum(word, ()))) + count += 1 + require(count == 65536, "every radical lift of the fixed sharp target") + return {"targets": count, "exact_cost_three": count, + "word_sha256": digest.hexdigest()} + + +def shared_local_control(mul, inverse): + """Tiny numeric overlap with #4601/#4613; not a replay of their engines.""" + scalars = (0, ONE, ONE << 4, ONE | (ONE << 4)) + charts = tuple(tuple(ONE if (code >> i) & 1 else 0 for i in range(4)) + for code in range(16) + if inverse[code] >= 0) + require(len(charts) == 6, "common GL2(F2) charts") + histogram = [0] * 4 + for code in range(256): + coefficients = tuple((code >> (2*i)) & 3 for i in range(4)) + a, b, c, d = tuple(x & 1 for x in coefficients) + if (a*d) ^ (b*c) != 1: + continue + target = tuple(scalars[x] for x in coefficients) + delta = 2 + for chart in charts: + n = product(target, chart, mul) + col1, col2 = (n[0] ^ ONE, n[2]), (n[1], n[3] ^ ONE) + rank = 0 if col1 == col2 == (0, 0) else ( + 1 if col1 == (0, 0) or col2 == (0, 0) or col1 == col2 else 2) + delta = min(delta, rank) + cost = delta if delta <= 1 else (2 if unit_pivots(target, inverse) else 3) + histogram[cost] += 1 + require(histogram == [6, 54, 36, 0], "shared binary dual-number count") + return {"targets": sum(histogram), "cost_histogram": histogram} + + +def odd_characteristic_control(): + """The displayed identity, with genuine subtraction, in M2(F3).""" + def mm(a, b): + return tuple(sum(a[2*i+k]*b[2*k+j] for k in range(2)) % 3 + for i in range(2) for j in range(2)) + + def add(a, b, sign=1): + return tuple((a[i]+sign*b[i]) % 3 for i in range(4)) + + def block_mm(a, b): + return tuple(add(mm(a[2*i], b[j]), mm(a[2*i+1], b[2+j])) + for i in range(2) for j in range(2)) + + zero, one = (0, 0, 0, 0), (1, 0, 0, 1) + a, b, c, d = (0, 0, 0, 1), (0, 1, 0, 0), (0, 0, 1, 0), (1, 0, 0, 0) + f = c + pivot = add(a, mm(b, f), -1) + pivot_inverse = (2, 0, 0, 1) + require(mm(pivot, pivot_inverse) == one, "ternary inverse") + lower = mm(add(c, mm(d, f), -1), pivot_inverse) + last = add(d, mm(lower, b), -1) + word = ((one, zero, lower, one), (one, b, zero, last), (pivot, zero, f, one)) + require(block_mm(block_mm(word[0], word[1]), word[2]) == (a, b, c, d), + "odd-characteristic endpoint") + wrong = (add(a, mm(b, f)), zero, f, one) + require(block_mm(block_mm(word[0], word[1]), wrong) != (a, b, c, d), + "wrong-sign control must differ") + + +def controls(mul, inverse): + require(not any(inverse[SHARP[0] ^ mul[SHARP[1]][f]] >= 0 + for f in (0, ONE)), "base-field-only completion must fail") + word = factors(SHARP, mul, inverse) + order_target = (1, 6, 6, 0) + order_word = factors(order_target, mul, inverse) + require(product(product(order_word[2], order_word[1], mul), order_word[0], mul) + != order_target, + "reversed word must differ") + require(product(word[0], word[1], mul) != SHARP, "dropped factor must differ") + lifted = tuple(SHARP[i] ^ (ONE << 4) for i in range(4)) + lifted_word = factors(lifted, mul, inverse) + require(product(product(word[0], word[1], mul), word[2], mul) != lifted, + "residue word cannot stand in for the lift") + f = lifted_word[2][2] + pivot = lifted_word[2][0] + wrong_lower = mul[lifted[2] ^ mul[lifted[3]][f]][inverse[pivot & 15]] + wrong_word = ((ONE, 0, wrong_lower, ONE), + (ONE, lifted[1], 0, lifted[3] ^ mul[wrong_lower][lifted[1]]), + lifted_word[2]) + require(product(product(wrong_word[0], wrong_word[1], mul), wrong_word[2], mul) + != lifted, "uncorrected residue inverse must differ") + try: + factors((0, 0, 0, 0), mul, inverse) + except ValueError as exc: + require(str(exc) == "no unit completion in the residue algebra", "failure reason") + else: + raise ValueError("singular target must be rejected by this construction") + odd_characteristic_control() + return 7 + + +def source_hashes(): + package = Path(__file__).resolve().parent + root = package.parents[1] + manifest = json.loads((package / "SOURCES.json").read_text()) + require(len(manifest["files"]) == 4, "source inventory size") + for row in manifest["files"]: + if row["usage"] == "input": + require(sha256((root / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "source bytes: " + row["path"]) + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + return {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + + +def main(): + hashes = source_hashes() + mul, inverse = tables() + result = {"residue": residue_census(mul, inverse), + "radical": radical_census(mul, inverse), + "shared_local_control": shared_local_control(mul, inverse), + "negative_controls": controls(mul, inverse), "files": hashes} + receipt = sha256(json.dumps(result, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + print("PASS_RIGHT_VECTOR_SEMILOCAL", json.dumps(result, sort_keys=True), + "receipt=" + receipt, "no_new_kappa") + + +if __name__ == "__main__": + main()