diff --git a/research/s3-three-local-obstruction/PROOF.md b/research/s3-three-local-obstruction/PROOF.md new file mode 100644 index 0000000000..4b6b94c744 --- /dev/null +++ b/research/s3-three-local-obstruction/PROOF.md @@ -0,0 +1,173 @@ +# A characteristic-three obstruction to nine-product S3 convolution + +This contribution was produced by Nick Petalas. It is a scoped proof using a +classical tensor-rank theorem, with finite exact corroboration. Independent +human and formal proof-kernel review are unclaimed. + +## 1. Boundary and result + +Let S3 be the symmetric group on three letters. Let R be a commutative unital +ring admitting a unital homomorphism to a field K of characteristic three. +For b >= 1, consider b independent, unrestricted S3 convolutions over R. +Their input and output spaces each have dimension 6b. A bilinear formula +of length r means + + xy = sum(j=1..r) u_j(x) v_j(y) w_j, + +where u_j and v_j are R-linear scalar forms on the complete respective +input spaces and w_j is an output vector over R. Forms and outputs may mix +different blocks freely. Only the r scalar products are counted; all linear +preprocessing, postprocessing and finite linear scratch are free in this +model. The product xy here is componentwise multiplication in R[S3]^b, +not convolution between the different blocks. + +**Theorem. Every such formula has r >= 10b.** In particular, no nine-product +formula exists over Z[1/2], over Z[1/2,i], or over Z[1/2,zeta_8]. Joint +formulas cannot amortize this floor below ten products per block. + +**Rational consequence.** Any rational bilinear formula for b such blocks +with fewer than 10b products must have at least one coefficient with reduced +denominator divisible by three. This includes its input forms and output +vectors. Thus the nine-product construction of Cinna Davis's +[PR #2224](https://github.com/CrocSwap/integer-mult-bounds/pull/2224) cannot +be replaced at the same product count by a formula using only coefficients +regular at three. This is a new application of a classical bound to that +package's exact-division question; it does not question its rational identity. + +## 2. Classical theorem used + +For a finite-dimensional associative unital algebra A over a field, let t(A) +be its number of maximal two-sided ideals. The Alder--Strassen bound gives + + rank(multiplication in A) >= 2 dim(A) - t(A). + +This is a cited mathematical input, not a theorem established by this verifier. +See A. Alder and V. Strassen, *On the algorithmic complexity of associative +algebras*, Theoretical Computer Science 15 (1981), 201--211, +[DOI](https://doi.org/10.1016/0304-3975(81)90070-0). +The same bound and definition of t are stated in the abstract of Markus +Bläser's *A Complete Characterization of the Algebras of Minimal Bilinear +Complexity*, [SIAM publication](https://epubs.siam.org/doi/10.1137/S0097539703438277). +The bound and modular specialization are classical. No priority for either +method, or for the representation theory of S3, is claimed. + +## 3. The characteristic-three algebra + +Write a=(123), s=(12), so a^3=s^2=1 and sas=a^-1. Put B=K[] and +u=a-1. In characteristic three, + + B = K[u]/(u^3), + A = K[S3] = B direct-sum B s. + +Let I=uB be the augmentation ideal of B. Conjugation by s preserves I, +because s u s = a^-1-1 = -u+u^2. Therefore + + J = I direct-sum I s + +is a two-sided ideal of A. More explicitly, if c,d are in I^j and e,f +are in I^k, every B-coefficient of (c+d s)(e+f s) lies in I^(j+k). +It follows that J^3=0. Its dimension is four, with basis u,u^2,u s,u^2 s. + +Modulo J, a becomes 1 and s remains an involution. Consequently + + A/J = K[C2] = K[t]/(t^2-1) = K x K, + +because 2 is invertible in characteristic three. The last isomorphism is +evaluation at t=1 and t=-1. Equivalently, the quotient map consists of the +trivial and sign characters on S3. Their images on 1 and s are (1,1) and +(1,-1), with determinant -2 != 0, so the map is surjective. + +Every maximal two-sided ideal contains J: its image in a simple quotient +is a nilpotent two-sided ideal, which must be zero. Maximal two-sided ideals +therefore correspond to those of K x K, of which there are exactly two. +Thus t(A)=2. This argument works over every characteristic-three field; +no finite-field enumeration or algebraic-closure assumption enters it. + +For b independent blocks the algebra is A^b. Its nilpotent ideal is J^b +(direct product, with componentwise multiplication), its quotient is +K^(2b), and its dimension is 6b. Hence t(A^b)=2b, and the cited theorem gives + + rank(A^b) >= 2(6b) - 2b = 10b. + +This applies directly to joint formulas, including cross-block linear forms. +It does not invoke any general tensor-rank direct-sum additivity conjecture. + +## 4. Specialization of coefficients + +Apply R -> K to every coefficient in a proposed length-r formula. Its tensor +identity remains valid, since it is an equality of the integer structure +constants of S3 multiplication. Some product terms may become zero, so the +specialized formula has length at most r. Section 3 forces r >= 10b. + +For rational coefficients whose reduced denominators avoid three, all +coefficients lie in the local ring + + Z_(3) = {m/n in Q : 3 does not divide n}. + +Reduction m/n -> (m mod 3)(n mod 3)^-1 maps this ring to F3. Contraposition +proves the rational consequence. Invertible changes of input/output basis +over this ring cannot evade it: after specialization they remain invertible, +or one can simply absorb them into the linear forms and output vectors. + +The complex examples also have characteristic-three specializations. In +F9 = F3[j]/(j^2+1), use + + 1/2 -> 2, i -> j, zeta_8 -> 1+j. + +The polynomial X^2+1 has no root in F3, so F9 is a field. The image of i +satisfies its defining equation. Further, (1+j)^2=2j and (1+j)^4=-1, so +the eighth-root relation is preserved. These assignments define maps from +the respective coefficient rings. In particular, allowing binary Fourier +normalizations does not evade the result: sqrt(2)=zeta_8+zeta_8^-1 and its +inverse belong to Z[1/2,zeta_8]. This is an exact-coefficient statement; +arbitrary complex coefficients need not admit such a specialization. + +Free linear scratch does not change the displayed formula class. With +arbitrary dirty auxiliary inputs and outputs, set the auxiliary inputs and +the initial accumulated output to zero and retain only the required data +outputs. Any formula that handles those arbitrary inputs also handles this +restriction, with no additional scalar products. Likewise, affine constants +in the separate input forms cannot evade the bound: extracting bidegree +(1,1) gives the same number of bilinear product terms. These observations +do not cover products whose two factors both mix the two input families, +nor arbitrary nonlinear straight-line algorithms. + +## 5. Exact finite evidence and its limits + +The verifier constructs S3 independently as permutations and as the normal +forms a^i s^e, and compares all 36 basis products. Over F3 it constructs a +four-vector basis for the common kernel of the trivial and sign characters, +checks two-sided closure, checks the quotient on all 36 products, and checks +all 16 radical basis products and 64 triple products. The resulting dimensions +are dim J=4, dim J^2=2 and J^3=0. + +As a separate finite corroboration, it enumerates all 729 algebra elements, +computes the rank of each six-by-six left-multiplication matrix, and checks +that invertibility agrees with both characters being nonzero. It obtains +324 units. The theoretical count is (3-1)^2 3^4, since every fiber of the +two-character quotient has 3^4 elements and units lift across a nilpotent ideal. + +Eight rejection controls cover a missing radical direction, transplanting the +radical to characteristic five, three invalid coefficient specializations, +two underpriced one-/eight-block claims, and an incorrect quotient dimension. +The product-floor controls exercise the arithmetic application of the cited +theorem; they are not exhaustive searches over tensor decompositions. + +All checks remain active with Python optimization. A generated optional +receipt binds all six package source files by SHA256. It contains measured +finite evidence, not a proof-kernel certificate of the theorem above. + +## 6. Research decision and remaining obligations + +Stop at this obstruction. Ten is a lower bound, not a proved attainable +dyadic rank. The rational formula, its numerator divisibility, and the old +conditional ceiling are not replayed or re-certified here. No current +selected-word placement, signed invoice, recursive child implementation, +rounding, tape, native map or complete multiplication theorem is supplied. + +A division by three that is known exact on restricted intermediate inputs +lies outside the coefficient ring model and remains a possible route. This +result gives neither its physical cost nor an impossibility for it. It also +does not exclude a changed convolution, restricted input space, approximate +or border-rank construction, or a different decoder mechanism. The selected +frontier and its five framework assumptions are unchanged. diff --git a/research/s3-three-local-obstruction/README.md b/research/s3-three-local-obstruction/README.md new file mode 100644 index 0000000000..504e871ba3 --- /dev/null +++ b/research/s3-three-local-obstruction/README.md @@ -0,0 +1,109 @@ +# Nine-product S3 convolution needs a characteristic-three denominator + +**Scoped proof; no new kappa.** A bilinear formula for b independent, +unrestricted S3 convolutions needs at least **10b scalar products** whenever +its coefficient ring admits a map to a characteristic-three field. This +includes dyadic, dyadic-Gaussian and eighth-root dyadic coefficients. Joint +formulas may mix all blocks; the lower bound still applies. + +Consequently every rational formula using fewer than 10b products has a +coefficient whose reduced denominator is divisible by three. Cinna Davis's +[nine-product construction (#2224)](https://github.com/CrocSwap/integer-mult-bounds/pull/2224) +therefore cannot keep its product count through a denominator-free or purely +dyadic bilinear replacement. Its rational identity is cited, not audited. +This answers one branch of its exact-division implementation question. + +The [proof](PROOF.md) computes a four-dimensional nilpotent ideal in K[S3], +with quotient K x K, in characteristic three. The classical +[Alder--Strassen bound](https://doi.org/10.1016/0304-3975(81)90070-0) +then gives 2(6b)-2b=10b. The new contribution is this source-specific +denominator obstruction and its implication for jointly batched S3 blocks. +The lower-bound theorem, modular specialization and group-algebra structure +are classical; no mathematical priority for those ingredients is claimed. + +## Evidence and reproduction + +The standard-library verifier constructs the new modular certificate and +enumerates every one of the 729 elements of F3[S3]. It finds 324 units, +checks radical dimensions (4,2,0), all 36 basis products, all 64 radical +triple products, and eight rejection controls. It imports no predecessor +verifier and does not replay the rational nine-product formula or its ceiling. + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/s3-three-local-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/s3-three-local-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/s3-three-local-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/s3-three-local-obstruction --check-source-history +``` + +Direct replay prints `PASS_S3_THREE_LOCAL_OBSTRUCTION` in its JSON output; +the registered runner prints `PASS_REGISTERED_RESEARCH_PACKAGE`. An optional +`--receipt /absolute/path/outside/the/checkout.json` writes generated evidence +bound to all six package files by SHA256. No receipt is hand-written. + +The written proof applies for every b and every characteristic-three field. +The finite checks corroborate its algebraic certificate; they do not prove +the cited general tensor-rank theorem or constitute proof-kernel verification. + +## Scope and sources + +The formula model is a sum of products of a linear form in the left inputs +and a linear form in the right inputs, followed by arbitrary linear output +maps. All blocks may share these forms and products. Linear scratch and +arbitrary dirty inputs cannot remove the lower bound: set auxiliary inputs +and initial accumulated outputs to zero and retain the required data outputs. +Invertible input/output basis changes over the coefficient ring are included. + +Ten is a lower bound; no ten-product dyadic construction is claimed. Exact +division by three on restricted intermediate values, nonlinear algorithms, +approximation and arbitrary complex coefficients remain outside this model. +No provider placement, complete signed bill, precision/tape schedule, supplier +admission, selected-frontier change or complete multiplication theorem is claimed. + +The base is canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`, +priority revision 8. The selected source-binding baseline passed before work. +The current coframe card is changed to the arithmetic boundary of #2224; +this is a scoped mechanism obstruction, not a current supplier optimization. +See [TASK.json](TASK.json) and [SOURCES.json](SOURCES.json) for the exact card, +scope and source pins. The advance +[CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228557) +records the question. The live overlap search covered 393 open PRs and 5,638 +Discussion records; sparse local-note coverage was incomplete. Whole-main +README searches and separate merged-PR searches supplied additional coverage. +No novelty claim rests on a lack of search matches. + +Credit Cinna Davis / 1337isnot1337's #2224 at +`b767ef166b6871c6965dce9b463432c665130024` for the rational S3 mechanism, +its division question and retained Strassen/representation-theory lineage. +Nick Petalas's older [#3336](https://github.com/CrocSwap/integer-mult-bounds/pull/3336) +excludes a literal affine-data placement; it is a separate obstruction and +is not extended or rechecked here. Credit Alder, Strassen and Bläser for +the cited algebra-complexity results. Predecessor files and credits remain intact. + +This contribution was produced by Nick Petalas. Independent human and formal +proof-kernel review are unclaimed. New work is Apache-2.0. + +## Verification bounds + +The verifier has no recursion, dynamic code execution or mutable shared state. +Matrices have at most 36 rows and exactly six columns; the largest +enumeration has 729 elements. Each function is under 60 physical lines. +Checks use explicit exceptions and survive optimization. Receipt I/O failures +propagate. Managed Python allocation is the rule-3 deviation: small fixed +dimensions bound live data, while Python integers and temporary collections +allocate during replay. No Python static analyzer is configured; registered +commands enable warning errors. There are no callback control dispatchers. + +## Open next questions + +1. What is the exact bilinear rank over Z[1/2] of this six-coordinate tensor? + Start by constructing a ten-product formula or proving a stronger floor + in characteristic three. The present argument does not prove attainability. +2. Can a known-exact division-by-three implementation retain nine rational + products within a fully charged physical invoice? Start with #2224's + numerator schedule and its intermediate divisibility invariant. Actual + source placement, quotient cost, storage, precision and restoration are open. + +Structured questions are in TASK.json. Neither follow-on is reserved here. diff --git a/research/s3-three-local-obstruction/SOURCES.json b/research/s3-three-local-obstruction/SOURCES.json new file mode 100644 index 0000000000..21c21a262b --- /dev/null +++ b/research/s3-three-local-obstruction/SOURCES.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/complex-s3-convolution-seed8b17/README.md", + "usage": "provenance", + "git_blob": "f935b2085d1bfe7622829e6e83ff94684ff7aa39", + "sha256": "809d0af838da2f5c4fe1029af7095371cbcd045bd7fb9937b010be57540b06a4" + }, + { + "path": "research/complex-s3-convolution-seed8b17/TASK.json", + "usage": "provenance", + "git_blob": "f84ad32fc86332c0ac779e51d9f2b3b7478a4bc4", + "sha256": "0034e31306aaa6c76b42d1235381063217a2e2ed8563b001ce2d3c9018257da8" + }, + { + "path": "research/s3-selected-affine-boundary/README.md", + "usage": "provenance", + "git_blob": "ee710975b75d67134a399e2ef9f2306527153b4a", + "sha256": "18f040656fd2e42118749012a6060f2739441ac52cb643bac3dc5fa6360ca83f" + } + ], + "external_mathematical_inputs": [ + { + "name": "Alder--Strassen bound", + "doi": "10.1016/0304-3975(81)90070-0", + "statement": "For an associative unital finite-dimensional field algebra A, R(A) >= 2 dim(A) - t(A), with t the number of maximal two-sided ideals.", + "confirmation": "https://epubs.siam.org/doi/10.1137/S0097539703438277", + "coverage": "Cited theorem; not computer-proved by this package." + } + ] +} diff --git a/research/s3-three-local-obstruction/TASK.json b/research/s3-three-local-obstruction/TASK.json new file mode 100644 index 0000000000..ac8471b079 --- /dev/null +++ b/research/s3-three-local-obstruction/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove that b unrestricted S3 convolutions need at least 10b bilinear scalar products over any coefficient ring admitting specialization to a characteristic-three field. Deduce unavoidable factors of three in denominators of rational formulas below that length, including the nine-product mechanism of PR2224.", + "scope_change_reason": "Changes the current coframe/card experiment to the exact-coefficient admission boundary of the published nonabelian convolution mechanism. This is a new scoped denominator obstruction, not a selected-word search, audit or supplier claim.", + "bottleneck_link": "PR2224 proposes a nine-product nonabelian rank-shape mechanism but leaves division by six unpaid. The obstruction rules out keeping nine products with purely dyadic or binary-Fourier exact coefficients, including joint block formulas. Exact division or more products must be priced before any physical gain.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved denominator obstruction after exact modular corroboration; do not seek an optimal dyadic construction or price a hypothetical selected supplier.", + "outcome": "negative-result", + "evidence": "Written specialization proof using the classical Alder--Strassen bound and a characteristic-three nilpotent ideal with quotient K x K. The self-contained verifier checks dimensions (4,2,0), 36 basis products, 64 radical triple products, all 729 F3[S3] elements (324 units), coefficient residue maps and eight rejection controls. No predecessor scientific replay.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact bilinear rank of S3 convolution over Z[1/2]?", + "why_it_matters": "The lower bound ten does not say how many dyadic products a physical implementation needs.", + "first_step": "Construct a ten-product formula or prove a stronger characteristic-three obstruction.", + "blocked_by": "No attaining dyadic formula or matching exact-rank theorem is supplied." + }, + { + "question": "Can exact division by three retain the nine rational products with a complete physical invoice?", + "why_it_matters": "Known-divisible restricted intermediates evade the coefficient-ring hypothesis and remain an implementation route.", + "first_step": "Derive the divisibility invariant for the PR2224 numerator schedule, then price the exact quotient and storage.", + "blocked_by": "Provider placement, quotient/tape cost, precision and restoration remain unresolved." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228557", + "claim_type": "scoped proof using a cited classical theorem, with finite exact corroboration" +} diff --git a/research/s3-three-local-obstruction/VERIFY.json b/research/s3-three-local-obstruction/VERIFY.json new file mode 100644 index 0000000000..87da965ead --- /dev/null +++ b/research/s3-three-local-obstruction/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact modular radical/quotient certificate, all 729 algebra elements, residue maps and eight rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same finite evidence with Python optimization; acceptance checks must remain active." + } + ] +} diff --git a/research/s3-three-local-obstruction/verify.py b/research/s3-three-local-obstruction/verify.py new file mode 100644 index 0000000000..89e854001e --- /dev/null +++ b/research/s3-three-local-obstruction/verify.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written characteristic-three obstruction.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows, modulus): + require(modulus in (3, 5), "unsupported modulus") + require(len(rows) <= 36, "row capacity") + require(all(len(row) == 6 for row in rows), "six coordinates required") + work = [[value % modulus for value in row] for row in rows] + pivot = 0 + for column in range(6): + candidates = [i for i in range(pivot, len(work)) if work[i][column]] + if not candidates: + continue + chosen = candidates[0] + work[pivot], work[chosen] = work[chosen], work[pivot] + inverse = pow(work[pivot][column], -1, modulus) + work[pivot] = [(value * inverse) % modulus for value in work[pivot]] + for i in range(len(work)): + if i != pivot: + factor = work[i][column] + work[i] = [(x - factor * y) % modulus + for x, y in zip(work[i], work[pivot], strict=True)] + pivot += 1 + return pivot + + +def group_data(): + permutations = tuple(itertools.permutations(range(3))) + table = tuple(tuple(permutations.index(tuple(p[q[i]] for i in range(3))) + for q in permutations) for p in permutations) + signs = tuple((-1) ** sum(p[i] > p[j] for i in range(3) + for j in range(i + 1, 3)) for p in permutations) + basis = tuple(tuple(int(i == j) for j in range(6)) for i in range(6)) + return permutations, table, signs, basis + + +def multiply(left, right, table): + output = [0] * 6 + for i in range(6): + for j in range(6): + output[table[i][j]] += left[i] * right[j] + return tuple(output) + + +def characters(vector, signs, modulus): + return (sum(vector) % modulus, + sum(x * sign for x, sign in zip(vector, signs, strict=True)) % modulus) + + +def radical_basis(signs): + vectors = [] + for sign in (1, -1): + indices = [i for i in range(6) if signs[i] == sign] + for i in indices[1:]: + vector = [0] * 6 + vector[i], vector[indices[0]] = 1, -1 + vectors.append(tuple(vector)) + return tuple(vectors) + + +def check_radical(table, signs, basis, radical, modulus): + require(rank(radical, modulus) == 4, "radical dimension") + require(all(characters(v, signs, modulus) == (0, 0) for v in radical), + "radical lies in quotient kernel") + for u in basis: + for v in basis: + image = characters(multiply(u, v, table), signs, modulus) + a, b = characters(u, signs, modulus), characters(v, signs, modulus) + require(image == tuple(x * y % modulus for x, y in zip(a, b, strict=True)), + "quotient multiplicativity") + for u in basis: + for v in radical: + for product in (multiply(u, v, table), multiply(v, u, table)): + require(rank((*radical, product), modulus) == 4, "two-sided ideal") + products = tuple(multiply(u, v, table) for u in radical for v in radical) + require(rank(products, modulus) == 2, "radical-square dimension") + for uv in products: + for w in radical: + require(all(x % modulus == 0 for x in multiply(uv, w, table)), + "radical cube must vanish") + return {"radical_dimension": 4, "radical_square_dimension": 2, + "radical_cube_dimension": 0, "quotient_dimension": 2, + "basis_products": 36, "radical_pair_products": len(products), + "radical_triple_products": len(products) * len(radical)} + + +def check_units(table, signs, basis): + units = 0 + for vector in itertools.product(range(3), repeat=6): + columns = tuple(multiply(vector, e, table) for e in basis) + invertible = rank(tuple(zip(*columns, strict=True)), 3) == 6 + predicted = all(characters(vector, signs, 3)) + require(invertible == predicted, "unit criterion") + units += invertible + require(units == (3 - 1) ** 2 * 3 ** 4, "unit count") + return {"elements_enumerated": 3 ** 6, "units": units} + + +def f9_multiply(x, y): + a, b = x + c, d = y + return ((a * c - b * d) % 3, (a * d + b * c) % 3) + + +def check_residue_maps(half, imaginary, zeta): + require(tuple(2 * x % 3 for x in half) == (1, 0), "half relation") + require(f9_multiply(imaginary, imaginary) == (2, 0), "Gaussian relation") + square = f9_multiply(zeta, zeta) + require(f9_multiply(square, square) == (2, 0), "eighth-root relation") + require(zeta != (0, 0), "unit eighth root") + + +def check_tensor_count(dimension, quotient_dimension, blocks, products): + require(dimension == 6 * blocks, "direct-product dimension") + require(quotient_dimension == 2 * blocks, "split quotient dimension") + # The inequality itself is the cited Alder--Strassen theorem, not a + # computer-proved tensor-rank theorem. PROOF.md supplies its hypotheses. + require(products >= 2 * dimension - quotient_dimension, + "Alder--Strassen product floor") + + +def rejected_controls(table, signs, basis, radical): + controls = 0 + try: + check_radical(table, signs, basis, radical[:-1], 3) + except ValueError as error: + require(str(error) == "radical dimension", "wrong control failure") + controls += 1 + else: + raise ValueError("missing radical direction accepted") + try: + check_radical(table, signs, basis, radical, 5) + except ValueError as error: + require(str(error) in ("radical-square dimension", "radical cube must vanish"), + "wrong characteristic control failure") + controls += 1 + else: + raise ValueError("characteristic-five radical accepted") + for half, imaginary, zeta in ( + ((1, 0), (0, 1), (1, 1)), + ((2, 0), (1, 0), (1, 1)), + ((2, 0), (0, 1), (0, 1))): + try: + check_residue_maps(half, imaginary, zeta) + except ValueError: + controls += 1 + else: + raise ValueError("false residue map accepted") + for blocks, quotient, products in ((1, 2, 9), (8, 16, 79), (1, 3, 9)): + try: + check_tensor_count(6 * blocks, quotient, blocks, products) + except ValueError: + controls += 1 + else: + raise ValueError("false product floor accepted") + return controls + + +def evidence(): + permutations, table, signs, basis = group_data() + require(len(set(permutations)) == 6, "group size") + # An independent normal-form product: a^i s^e a^j s^f. + a, s = (1, 2, 0), (1, 0, 2) + normal = [] + for i in range(3): + power = (0, 1, 2) + for _ in range(i): + power = tuple(a[power[k]] for k in range(3)) + for e in range(2): + normal.append(tuple(power[s[k]] for k in range(3)) if e else power) + require(len(set(normal)) == 6, "normal-form basis") + for i, p in enumerate(normal): + for j, q in enumerate(normal): + target = 2 * ((i // 2 + (-1) ** (i % 2) * (j // 2)) % 3) + target += (i % 2 + j % 2) % 2 + require(permutations[table[permutations.index(p)][permutations.index(q)]] + == normal[target], "independent group multiplication") + radical = radical_basis(signs) + result = check_radical(table, signs, basis, radical, 3) + result.update(check_units(table, signs, basis)) + # The two quotient images of e and s have determinant -2, a unit mod 3. + require(characters(basis[0], signs, 3) == (1, 1), "identity character") + require(characters(basis[permutations.index(s)], signs, 3) == (1, 2), + "surjective split quotient") + check_residue_maps((2, 0), (0, 1), (1, 1)) + for blocks in range(1, 9): + check_tensor_count(6 * blocks, 2 * blocks, blocks, 10 * blocks) + result["rejected_controls"] = rejected_controls(table, signs, basis, radical) + result["radical_basis"] = radical + result["lower_bound_per_block_using_cited_theorem"] = 10 + result["rational_predecessor_products_per_block"] = 9 + result["status"] = "PASS_S3_THREE_LOCAL_OBSTRUCTION" + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + package = Path(__file__).resolve().parent + if args.receipt is not None: + receipt = args.receipt.resolve() + require(args.receipt.is_absolute(), "receipt path must be absolute") + require(not receipt.is_relative_to(package.parent.parent), + "receipt must stay outside the checkout") + result = evidence() + files = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result["source_sha256"] = { + name: hashlib.sha256((package / name).read_bytes()).hexdigest() for name in files} + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.receipt is not None: + args.receipt.write_text(encoded, encoding="utf-8") + print(encoded, end="") + + +if __name__ == "__main__": + main()