Prove a ten-product dyadic S3 convolution floor (no new κ)

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[<a>] 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.

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.

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."
+    }
+  ]
+}