From 4b2322fc5bd30a129507c2eee69aa275527b69ac Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 10:23:46 +0100 Subject: [PATCH] feat(research): prove exact right-vector costs over local products --- research/right-vector-local-products/PROOF.md | 158 +++++++++++++ .../right-vector-local-products/README.md | 125 +++++++++++ .../right-vector-local-products/SOURCES.json | 30 +++ .../right-vector-local-products/TASK.json | 70 ++++++ .../right-vector-local-products/VERIFY.json | 37 ++++ .../right-vector-local-products/verify.py | 209 ++++++++++++++++++ 6 files changed, 629 insertions(+) create mode 100644 research/right-vector-local-products/PROOF.md create mode 100644 research/right-vector-local-products/README.md create mode 100644 research/right-vector-local-products/SOURCES.json create mode 100644 research/right-vector-local-products/TASK.json create mode 100644 research/right-vector-local-products/VERIFY.json create mode 100644 research/right-vector-local-products/verify.py diff --git a/research/right-vector-local-products/PROOF.md b/research/right-vector-local-products/PROOF.md new file mode 100644 index 0000000000..7230a0e7bb --- /dev/null +++ b/research/right-vector-local-products/PROOF.md @@ -0,0 +1,158 @@ +# Radical reduction for invertible right-vector targets + +Let `K` be a field. Let `R = R_1 x ... x R_k`, with `1 <= k < infinity`, +where each `R_i` is an associative unital `K`-algebra whose non-units form +a proper two-sided ideal `J_i`. This is the local-algebra hypothesis used +by Nick Petalas's #4276. Put `J = product J_i` and `D = R/J`. Each +`D_i = R_i/J_i` is a division algebra with the induced central copy of `K`. +No commutativity, finite-dimensionality or nilpotence hypothesis is needed. + +Use the retained two-role alphabet + +```text +P(u,y) = I + u y^T, u in R^2, y in K^2, +free maps GL_2(K), usable anywhere, +delta_R(M) = min_{T in GL_2(K)} dim_K ((MT-I)K^2). +``` + +The cost is the least number of paid factors. A bar denotes reduction +modulo `J`. The target `M` is assumed invertible throughout. + +## The result + +```text +cost_R(M) <= 2 iff cost_D(Mbar) <= 2, +cost_R(M) = max(delta_R(M), cost_D(Mbar)) <= 3. +``` + +Thus local radicals cannot create or remove a three-factor obstruction +on invertible targets. They can increase a zero- or one-factor residue +cost, and `delta_R` measures precisely that remaining increase. + +For finite `K` of size `q`, every invertible target costs at most two when +`k <= q`. For each fixed product with `k >= q+1`, there is an invertible +target of cost three and `delta_R = 2`. For infinite `K`, every invertible +target in a finite product costs at most two. The finite-field component +threshold therefore extends #4334 from field products to these local +products, including noncommutative local algebras. + +## 1. Units and the common pivot + +An element of `R_i` is a unit exactly when its image in `D_i` is nonzero. +Indeed, the zero coset is `J_i`, the set of non-units by hypothesis. The +quotient is a division algebra since every nonzero coset has a unit +representative. Units in a finite product are exactly the tuples of units. + +For any invertible `N` over `R`, the first row `(A,B)` is right unimodular. +Writing `(x,z)^T` for the first column of `N^{-1}` gives `Ax+Bz=1`. +If `B=AC`, this becomes `A(x+Cz)=1`. In each component a non-unit `A_i` +would make the left side belong to the proper ideal `J_i`. Consequently +`A` must be a unit. Conversely, a unit `A` always gives `B in AR`. + +By #4276, Theorem B, two paid factors suffice exactly when some +`G,H in GL_2(K)` make `N=GMH` satisfy `N12 in N11 R`. The preceding +paragraph reduces this, on invertible targets, to `N11` being a unit. +Every nonzero `K` row `phi` can be the first row of `G`, and every nonzero +`K` column `t` can be the first column of `H`. Therefore + +```text +cost_R(M) <= 2 +iff some common nonzero phi,t over K make phi M_i t a unit for every i +iff some common nonzero phi,t over K make phi Mbar_i t nonzero for every i +iff cost_D(Mbar) <= 2. +``` + +The same argument applies to `D`, since a division algebra is local with +zero non-unit ideal. This proves radical invariance of the two-factor set. +It does not assume componentwise free maps or componentwise right vectors. + +## 2. Three paid factors always suffice + +This extends ToikY's #4334, Section 3, with the order of every product kept +as written. Write `M=[[a,b],[c,d]]`. In each component its second column +is left unimodular. If `d_i` is a non-unit, then `b_i` is a unit, since +otherwise both entries and all their left linear combinations lie in +`J_i`, contradicting the second row of `M_i^{-1}` applied to that column. + +Choose the element `r in R` by `r_i=0` if `d_i` is a unit and `r_i=1` +otherwise. Set + +```text +D0 = d-rb, +f = D0^{-1}(c-ra), +e = a-bf. +``` + +Each `D0_i` is a unit. In the second case its residue is `-bbar_i != 0`; +in the first case it is `d_i`. Hence the inverse in the formula exists. +Direct multiplication, without interchanging any ring factors, gives + +```text +M = [[1,0],[r,1]] [[1,b],[0,D0]] [[e,0],[f,1]] + = P((0,r)^T,e1) P((b,D0-1)^T,e2) P((e-1,f)^T,e1). +``` + +The four entries of this product are `e+bf=a`, `b`, +`r(e+bf)+D0 f=ra+c-ra=c`, and `rb+D0=d`. This uses three allowed factors +with the common right-vector sequence `e1,e2,e1` and no free map. +The componentwise coefficient choice belongs to the allowed left vector. +It does not make the right vectors or free maps componentwise. + +## 3. The exact cost formula + +By the predecessor column bound and quotient functoriality, + +```text +cost_R(M) >= delta_R(M), +cost_R(M) >= cost_D(Mbar). +``` + +Both costs are at most three by Section 2. If `cost_D(Mbar)=3`, these +bounds force `cost_R(M)=3`, while `delta_R(M)<=2`. Otherwise Section 1 +gives `cost_R(M)<=2`. Theorem A of #4276 gives exact cost `delta_R` +when `delta_R<=1`. If `delta_R=2`, the column bound forces cost two. +Thus `cost_R=delta_R` in this second case, and the quotient lower bound +also gives `cost_D(Mbar)<=delta_R`. The stated maximum formula follows. + +For example, over the single local algebra `F2[e]/e^2`, the targets +`diag(1+e,1)` and `diag(1+e,1+e)` reduce to the free identity but cost +one and two respectively. For the first, `T=I` gives dimension one and +the target is not free. For the second, a binary kernel vector `v` of +`(1+e)T-I` must satisfy both `(T-I)v=0` and `Tv=0`, hence `v=0`. +So every free endpoint gives dimension two. The exact formula applies. + +## 4. The sharp component threshold + +Fix a nonzero `t in K^2`. Each `Mbar_i t` is nonzero in `D_i^2`. +At most one projective `K` row can annihilate it. If two distinct +projective rows did so, they would form a `K` basis of the row space, +forcing both entries of this vector to vanish. For finite `K`, there +are `q+1` projective rows. When `k<=q` some row is not forbidden. +For infinite `K`, a finite union of these singleton forbidden sets +also leaves a row. Section 1 supplies the two-factor word in each case. + +For sharpness when `K` is finite and `k>=q+1`, take the `q+1` scalar +matrices in `GL_2(K)` constructed in #4334, Section 4, from the +projective representatives of a quadratic extension. Place these in +the first `q+1` components, using the central copy of `K` in each `R_i`, +and put identities in extra components. For every nonzero `phi,t`, +one of these component pivots is literally zero, so it is not a unit. +Section 1 excludes two factors; Section 2 supplies three. Theorem A +then forces `delta_R=2`. The extension-field construction and its +projective covering property are credited to #4334, not reproved here. + +## Scope and credit + +This is a scoped algebraic proof in the formal alphabet. It supplies no +native implementation, frame conversion, routing, precision, restoration, +stock bound, supplier admission or multiplication theorem. These physical +costs remain unknown. Singular targets are excluded. Independent human +and formal proof-kernel review are unclaimed. + +Produced by Nick Petalas. The new result is the local-product reduction +and exact lift formula. ToikY's #4334 supplies the field-product result, +the three-factor formula being extended, and the sharp scalar examples. +Nick Petalas's #4276 supplies the one- and two-factor criteria, following +#4265 and #4243. Wentao Li's #4099 supplies the right-vector alphabet and +column bound, building on #2513. Source bytes and commits are pinned in +SOURCES.json. Apache-2.0. diff --git a/research/right-vector-local-products/README.md b/research/right-vector-local-products/README.md new file mode 100644 index 0000000000..e7886eba30 --- /dev/null +++ b/research/right-vector-local-products/README.md @@ -0,0 +1,125 @@ +# Local radicals preserve the three-factor right-vector obstruction + +**Scoped proof with exhaustive finite controls. No new kappa.** This takes +Open next question 1 of ToikY's [#4334](https://github.com/CrocSwap/integer-mult-bounds/pull/4334), +which proves the field-product case and leaves local products open. + +Let `R=R_1 x ... x R_k` be a finite product of associative local +`K`-algebras. In each component the non-units must form a proper two-sided +ideal `J_i`. Set `J=product J_i`. Use two roles, paid factors +`I+u y^T` with `u in R^2`, `y in K^2`, and common free `GL_2(K)` maps. +For every invertible target `M`, [PROOF.md](PROOF.md) proves + +```text +cost_R(M) <= 2 iff cost_(R/J)(Mbar) <= 2, +cost_R(M) = max(delta_R(M), cost_(R/J)(Mbar)) <= 3, +delta_R(M) = min_{T in GL_2(K)} dim_K ((MT-I)K^2). +``` + +Local radicals therefore preserve exactly which invertible targets need +three factors. They can increase smaller residue costs. Over `F2[e]/e^2`, +`diag(1+e,1)` and `diag(1+e,1+e)` both reduce to the free identity but +cost one and two respectively. + +The proof reduces the predecessor right-ideal criterion to a common unit +pivot, then reduces that pivot modulo each component ideal. It extends +#4334's three-factor word with the ring multiplications in their stated +order. It applies to noncommutative local algebras as well. In particular, +for finite `K=F_q`, the sharp component threshold remains `k=q+1`: +all invertible targets cost at most two for `k<=q`, and every such product +with `k>=q+1` has a cost-three target. For infinite `K`, all invertible +targets in a finite product cost at most two. + +## Finite evidence + +`verify.py` imports no predecessor code. It enumerates literal words of +cost zero, one and two over `A^k`, where `A=F2[e]/e^2`, for `k=1,2,3`. +All common right-vector pairs and all six common free endpoints are +included. Each local factor coefficient is independent across components. +For an invertible endpoint, filtering to invertible paid factors is sound +because determinants multiply in these commutative finite rings. + +For each common pair and endpoint, it computes the local reachable set +and its complete `k`-fold Cartesian power. Their union is the exact +two-factor set, without using the pivot criterion. Separately, it computes +all six literal binary column ranks for delta. The explicit three-factor +formula is checked on all 96 local invertible matrices; its common +right-vector sequence makes the construction valid on every product tuple. + +| Components | Invertible targets | Cost 0 | Cost 1 | Cost 2 | Cost 3 | +|---:|---:|---:|---:|---:|---:| +| 1 | 96 | 6 | 54 | 36 | 0 | +| 2 | 9,216 | 6 | 558 | 8,652 | 0 | +| 3 | 884,736 | 6 | 4,590 | 830,988 | 49,152 | + +The maximum formula and radical invariance hold on all **894,048** targets. +The three-component residue cost-three count is 12, agreeing with #4334; +each residue target has `16^3=4096` lifts, all of cost three. The printed +receipt also records every residue-cost/lift-cost count and hashes every +complete cost table. It binds the results to the package's file hashes. +There is no handwritten receipt. + +Controls detect changing an attaining factor, reversing a product, +allowing separate free charts, dropping an obstruction component, and +equating cost with residue cost while ignoring nilpotent contributions. +Checks remain active under Python optimization. + +## Reproduce + +From the repository root, with CPython 3.12 and NumPy 2.5.4: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-local-products/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-local-products/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-local-products +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-local-products --check-source-history +``` + +The verifier writes nothing and ends with +`PASS_RIGHT_VECTOR_LOCAL_PRODUCTS targets=894048 cost3=49152 formula=exact`, +followed by its generated digest and `no_new_kappa`. Each registered check +has a 120-second limit. Source commits, blobs and SHA256 pins are in +[SOURCES.json](SOURCES.json). Its catalogue and selected record are historical +provenance. The two predecessor proof files are live pinned inputs. + +## Limits and engineering notes + +The proof concerns invertible two-role targets in the formal alphabet. +Finite evidence covers the binary dual-number products only; it does not +enumerate noncommutative local algebras. Native preparation, conversion, +routing, precision, restoration and stock costs remain unknown. No supplier +is admitted and no multiplication theorem or frontier changes. Independent +human and formal proof-kernel review are unclaimed. No Lean, Docker or +selected construction replay is needed for this isolated result or claimed. + +The verifier uses bounded ranges, no recursion, local immutable matrix +tuples, explicit checks and functions below 60 lines. Python and NumPy +allocate dynamically; live memory is bounded by arrays over at most +`96^3` targets and a fixed number of temporaries. This is the managed-runtime +deviation from static allocation. No shared code changes are included. + +The orientation command `scripts/research_baseline.py` fails at this base +with `KeyError: 'bit_lower'` because it expects the earlier certificate +schema. The selected record's source-binding check succeeds after sparse +inputs are materialized. This package does not depend on the baseline helper. + +## Open next questions + +1. Does the two-factor radical reduction extend to all semilocal algebras? + Start with a quotient having one `M_2(K)` block. This would separate + radical lifting from noncommutative matrix-block effects, but the + present non-unit-ideal argument does not apply to matrix algebras. +2. Which singular targets over local products are reachable, and do the + reachable ones always cost at most three? Begin with the three-factor + image over `F2[x,y]/(x,y)^2`. The current unit-pivot and upper-word + arguments both use invertibility. + +## Credit + +This contribution was produced by Nick Petalas. ToikY's #4334 supplies the +field-product theorem, the three-factor formula extended here, and the +sharp scalar examples. Nick Petalas's #4276 supplies the one- and +two-factor criteria, following #4265 and #4243. Wentao Li's #4099 supplies +the alphabet and column bound, building on #2513. The new claims are the +local-product radical reduction, exact lift formula and their stated +consequences. Apache-2.0. diff --git a/research/right-vector-local-products/SOURCES.json b/research/right-vector-local-products/SOURCES.json new file mode 100644 index 0000000000..473c4b9fd3 --- /dev/null +++ b/research/right-vector-local-products/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "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-local-products/TASK.json b/research/right-vector-local-products/TASK.json new file mode 100644 index 0000000000..abcb8fef26 --- /dev/null +++ b/research/right-vector-local-products/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "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": "Exact cost of invertible two-role right-vector targets over finite products of associative local K-algebras: radical invariance of the two-factor set, cost_R(M)=max(delta_R(M),cost_(R/J)(Mbar))<=3, and the sharp field-size component threshold. Literal exhaustive finite controls over (F2[e]/e^2)^k for k=1,2,3.", + "scope_change_reason": "Takes Open next question 1 of ToikY #4334 rather than a new native register construction. The result separates radical effects from common residue charts; this is a formal-alphabet side result.", + "bottleneck_link": "Side result for a formal two-role alphabet; it settles the effect of local radicals on exact factor counts. Native conversion, physical caller and complete supplier costs remain unknown, and no kappa changes.", + "budget_minutes": 60, + "stop_rule": "Stop after the radical-reduction proof and first complete binary dual-number product controls; package the result without a larger construction or search campaign.", + "outcome": "completed", + "evidence": "PROOF.md gives the scoped proof. verify.py enumerates literal words with zero, one and two paid factors and an explicit three-factor upper witness. All 894048 invertible targets over one, two and three binary dual-number factors satisfy the maximum formula; exactly 49152 of the three-component targets cost three. No predecessor verifier is imported or replayed.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does radical invariance of the two-factor set extend from products of local algebras to all semilocal K-algebras?", + "why_it_matters": "Matrix blocks in the semisimple quotient allow nontrivial ranks and fall outside the local division-residue proof.", + "first_step": "Specify the two-factor unit-pivot criterion and an explicit three-factor construction when R/J has one M2(K) block; separate radical lifting from the block obstruction.", + "blocked_by": "The present proof uses the component ideal of non-units; matrix algebras do not satisfy that hypothesis." + }, + { + "question": "Which singular targets over local products have finite cost, and is three always sufficient for the reachable ones?", + "why_it_matters": "Invertibility is used both in the unit-pivot reduction and in choosing the three-factor word; singular radical targets can be unreachable.", + "first_step": "Characterise the three-factor image over F2[x,y]/(x,y)^2 before attempting a general theorem.", + "blocked_by": "No unit-pivot reduction or general reachability theorem for singular targets is proved here." + } + ] +} diff --git a/research/right-vector-local-products/VERIFY.json b/research/right-vector-local-products/VERIFY.json new file mode 100644 index 0000000000..72887bddfd --- /dev/null +++ b/research/right-vector-local-products/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.5.4" + ], + "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": "Literal zero/one/two-factor sets on every invertible target of (F2[e]/e^2)^k for k=1,2,3 (894048 targets), explicit three-factor upper words, exact binary delta, radical maximum formula, unit-pivot equivalence and changed-factor/order/common-chart/dropped-component/nilpotent controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the complete exact census with Python optimization and explicit checks that remain active; print the deterministic hash-bound receipt for comparison with the normal run." + } + ] +} diff --git a/research/right-vector-local-products/verify.py b/research/right-vector-local-products/verify.py new file mode 100644 index 0000000000..6f15d651a6 --- /dev/null +++ b/research/right-vector-local-products/verify.py @@ -0,0 +1,209 @@ +#!/usr/bin/env python3 +"""Exact literal words over binary dual-number products. Apache-2.0.""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +import numpy as np + + +IDENTITY = (1, 0, 0, 1) +LINES = ((1, 0), (0, 1), (1, 1)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(a, b): + """(a0+a1 e)(b0+b1 e) with e^2=0; restrict to 0,1 for F2.""" + return (a & b & 1) | ((((a & 1) * (b >> 1)) ^ + ((a >> 1) * (b & 1))) << 1) + + +def matrix_product(a, b): + return tuple(multiply(a[2 * i], b[j]) ^ + multiply(a[2 * i + 1], b[2 + j]) + for i in range(2) for j in range(2)) + + +def invertible(a): + return (multiply(a[0], a[3]) ^ multiply(a[1], a[2])) & 1 + + +def paid(u, y): + return tuple(IDENTITY[2 * i + j] ^ multiply(u[i], y[j]) + for i in range(2) for j in range(2)) + + +def alphabet(size): + require(size in (2, 4), "only F2 and F2[e]/e^2 are supported") + matrices = tuple(a for a in product(range(size), repeat=4) if invertible(a)) + free = tuple(a for a in product(range(2), repeat=4) if invertible(a)) + factors = tuple(tuple(sorted({paid(u, y) for u in product(range(size), repeat=2) + if invertible(paid(u, y))})) for y in LINES) + require(len(matrices) == (6 if size == 2 else 96), "GL2 inventory") + require(all(len(f) == (2 if size == 2 else 8) for f in factors), "paid inventory") + return matrices, free, factors + + +def literal_costs(size, components): + """Union Cartesian boxes for every common y1,y2,S, without a pivot test.""" + require(1 <= components <= 3, "component bound") + matrices, free, factors = alphabet(size) + index = {a: i for i, a in enumerate(matrices)} + costs = np.full((len(matrices),) * components, 3, dtype=np.uint8) + for s, f1, f2 in product(free, factors, factors): + endpoints = sorted({index[matrix_product(matrix_product(a, b), s)] + for a, b in product(f1, f2)}) + costs[np.ix_(*([endpoints] * components))] = 2 + for s, f1 in product(free, factors): + endpoints = sorted({index[matrix_product(a, s)] for a in f1}) + costs[np.ix_(*([endpoints] * components))] = 1 + for s in free: + costs[(index[s],) * components] = 0 + return matrices, costs + + +def delta_values(matrices, components): + """Literal binary ranks of the two common-input columns for every free T.""" + _, free, _ = alphabet(2) + shape = (len(matrices),) * components + delta = np.full(shape, 2, dtype=np.uint8) + for t in free: + columns = [matrix_product(a, t) for a in matrices] + c1 = np.zeros(shape, dtype=np.uint16) + c2 = np.zeros(shape, dtype=np.uint16) + for i in range(components): + view = [1] * components + view[i] = len(matrices) + left = np.array([(a[0] ^ 1) | (a[2] << 2) for a in columns], np.uint16) + right = np.array([a[1] | ((a[3] ^ 1) << 2) for a in columns], np.uint16) + c1 |= left.reshape(view) << (4 * i) + c2 |= right.reshape(view) << (4 * i) + rank = np.where((c1 == 0) & (c2 == 0), 0, + np.where((c1 == 0) | (c2 == 0) | (c1 == c2), 1, 2)) + np.minimum(delta, rank, out=delta, casting="unsafe") + return delta + + +def pivot_mask(matrices, components): + """Independent unit-pivot predicate, not used to construct literal costs.""" + mask = np.zeros((len(matrices),) * components, dtype=bool) + for phi, t in product(LINES, repeat=2): + good = [] + for a in matrices: + value = 0 + for i, j in product(range(2), repeat=2): + value ^= multiply(phi[i], multiply(a[2 * i + j], t[j])) + good.append(bool(value & 1)) + indices = np.flatnonzero(good) + mask[np.ix_(*([indices] * components))] = True + return mask + + +def three_factor_words(matrices): + """Check the noncommutative-order formula on each local GL2 element.""" + reversed_failures = 0 + for a, b, c, d in matrices: + r = 0 if d & 1 else 1 + big_d = d ^ multiply(r, b) + require(big_d & 1, "D must be a unit") + inverse = next(x for x in range(4) if multiply(big_d, x) == 1) + f = multiply(inverse, c ^ multiply(r, a)) + e = a ^ multiply(b, f) + first = paid((0, r), (1, 0)) + second = paid((b, big_d ^ 1), (0, 1)) + third = paid((e ^ 1, f), (1, 0)) + target = (a, b, c, d) + require(matrix_product(matrix_product(first, second), third) == target, + "three-factor witness") + changed = (third[0] ^ 1, *third[1:]) + require(matrix_product(matrix_product(first, second), changed) != target, + "changed-factor control") + reversed_failures += matrix_product(matrix_product(third, second), first) != target + require(reversed_failures > 0, "word-order control") + return reversed_failures + + +def check_arithmetic(): + for a, b, c in product(range(4), repeat=3): + require(multiply(a, b) == multiply(b, a), "commutativity") + require(multiply(multiply(a, b), c) == multiply(a, multiply(b, c)), + "associativity") + require(multiply(a, b ^ c) == multiply(a, b) ^ multiply(a, c), + "distributivity") + require((multiply(a, b) & 1) == ((a & 1) * (b & 1)), "residue map") + require(multiply(2, 2) == 0 and multiply(2, 1) == 2, "nonzero nilpotent") + + +def check_case(components): + matrices, costs = literal_costs(4, components) + residue_matrices, residue_costs = literal_costs(2, components) + residue_index = {a: i for i, a in enumerate(residue_matrices)} + projection = np.array([residue_index[tuple(x & 1 for x in a)] for a in matrices]) + reduced = residue_costs[np.ix_(*([projection] * components))] + delta = delta_values(matrices, components) + require(np.array_equal(costs, np.maximum(delta, reduced)), "exact cost formula") + require(np.array_equal(costs <= 2, reduced <= 2), "radical invariance") + require(np.array_equal(costs <= 2, pivot_mask(matrices, components)), "unit pivots") + require(np.all(costs >= delta), "column lower bound") + histogram = [int(np.count_nonzero(costs == i)) for i in range(4)] + require(sum(histogram) == 96 ** components, "all invertible targets counted") + failures = int(np.count_nonzero(costs == 3)) + require(failures == (49152 if components == 3 else 0), "sharp binary threshold") + transitions = [[int(np.count_nonzero((reduced == i) & (costs == j))) + for j in range(4)] for i in range(4)] + return {"components": components, "targets": costs.size, "cost_histogram": histogram, + "residue_to_lift_cost": transitions, + "cost_bytes_sha256": sha256(costs.tobytes()).hexdigest()} + + +def check_controls(): + matrices, costs = literal_costs(4, 1) + index = {a: i for i, a in enumerate(matrices)} + require(int(costs[index[(3, 0, 0, 1)]]) == 1, "one nilpotent diagonal") + require(int(costs[index[(3, 0, 0, 3)]]) == 2, "two nilpotent diagonals") + binary, quotient_costs = literal_costs(2, 3) + bi = {a: i for i, a in enumerate(binary)} + obstruction = (IDENTITY, (0, 1, 1, 1), (1, 1, 1, 0)) + require(int(quotient_costs[tuple(bi[a] for a in obstruction)]) == 3, + "known residue obstruction") + require(not np.all(pivot_mask(binary, 3)), "common-chart control") + _, two_costs = literal_costs(2, 2) + require(np.all(two_costs <= 2), "dropped-component control") + require(all(a in bi for a in obstruction), "each component separately free") + + +def source_binding(): + package = Path(__file__).resolve().parent + root = package.parents[1] + sources = json.loads((package / "SOURCES.json").read_text()) + for entry in sources["files"]: + if entry["usage"] == "input": + raw = (root / entry["path"]).read_bytes() + require(sha256(raw).hexdigest() == entry["sha256"], "source changed") + names = ("verify.py", "PROOF.md", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json") + return {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + + +def main(): + check_arithmetic() + matrices, _, _ = alphabet(4) + reversed_failures = three_factor_words(matrices) + check_controls() + results = [check_case(k) for k in range(1, 4)] + receipt = {"sources": source_binding(), "cases": results, + "reversed_word_failures": reversed_failures} + encoded = json.dumps(receipt, sort_keys=True, separators=(",", ":")) + print(json.dumps(receipt, sort_keys=True)) + print("PASS_RIGHT_VECTOR_LOCAL_PRODUCTS targets=" + + str(sum(r["targets"] for r in results)) + + " cost3=49152 formula=exact receipt=" + sha256(encoded.encode()).hexdigest() + + " no_new_kappa") + + +if __name__ == "__main__": + main()