Prove exact mixed-direction Clifford batching criteria (no new κ)

research/mixed-clifford-dyadic-imbalance/PROOF.md

@@ -0,0 +1,159 @@
+# Mixed Clifford lanes at widths congruent to two
+
+This contribution is produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Work over a characteristic-zero field containing i, where i^2=-1. Put
+
+```
+C = ((1+i) I + (1-i) X)/2,  X = [[0,1],[1,0]],  C_f = C tensor ... tensor C.
+```
+
+Fix f>0 with f=2 modulo 4, nonnegative integers a,b with q=a+b>0,
+and delta=a-b. The independent payload operator is
+
+```
+T = (I_a tensor C_f) direct-sum (I_b tensor C_f^-1).
+```
+
+All q 2^f coordinates are arbitrary independent inputs. Identity complements
+also hold arbitrary dirty data. Allow any invertible square encoder E and its
+exact inverse as decoder. One candidate child has operator
+H=lambda (C_h tensor I_t), with h,t positive integers and nonzero lambda.
+
+There is a full-space identity
+
+```
+T direct-sum I_d = E^-1 (H direct-sum I_e) E
+```
+
+if and only if d=e and there is an integer j>=0 such that
+
+```
+q = 2^j |delta|,   4^j divides q,
+h = f+2j,         t = q/4^j,
+lambda = sign(delta) i^(-j).
+```
+
+In particular, delta cannot be zero. These conditions determine the candidate
+uniquely. They classify a forward child; allowing an inverse child adds no
+widths because C_h^-1 is similar to (-i)^h C_h, as in Arham Tahir's PR1920.
+The theorem does not classify other congruence classes of f.
+
+## Necessity
+
+The source facts used here are PR1920's reciprocal full-space contract,
+Walsh eigenbasis and trace method. Their application to arbitrary directional
+multiplicities, and the resulting integer conditions, are the new step.
+
+Since C has eigenvalues 1,i, all payload eigenvalues are fourth roots of
+unity. Taking fourth powers of the identity forces lambda^4=1 on the
+nonempty child operand. Therefore lambda belongs to {1,i,-1,-i}.
+The traces of C_f^2 and C_h^2 are zero, since they are positive tensor powers
+of the traceless X. The square traces of the two full operators are d and e,
+so d=e. Dimension equality then gives
+
+```
+q 2^f = t 2^h.                                      (1)
+```
+
+Write z=(1+i)^f. Since f=2 modulo 4, its Gaussian conjugate is -z. After
+subtracting the equal complement traces, the first trace identity becomes
+
+```
+delta z = t lambda (1+i)^h.                         (2)
+```
+
+The right side is nonzero, so delta is nonzero. Taking the algebraic Gaussian
+norm of this equality gives
+
+```
+delta^2 2^f = t^2 2^h.
+```
+
+Combine this with (1) to obtain q^2/delta^2=2^(h-f). Because |delta|<=q,
+h>=f. A rational square that is a power of two has an even exponent, by
+the exponent of the prime 2 in its numerator and denominator. Thus h-f=2j
+for an integer j>=0, and q=2^j |delta|. Equation (1) now gives t=q/4^j;
+its required positive integrality is exactly 4^j dividing q. Finally,
+(1+i)^(f+2j)=z (2i)^j in (2) gives the asserted lambda, including its sign.
+
+No positivity, ordering or analytic norm on the ambient field was used.
+The norm calculation is in its embedded copy of Q(i).
+
+## Sufficiency and explicit basis
+
+Assume the displayed integer conditions. The dimensions agree. Substitution
+shows the first traces agree, since
+
+```
+(q/4^j) sign(delta) i^(-j) z (2i)^j = delta z.
+```
+
+The square traces vanish. The third traces are the Gaussian conjugates of
+the first traces, so they agree as well. The zeroth traces are dimensions.
+The four-point Fourier matrix recovers eigenvalue multiplicities from these
+four traces. Since x^4-1 has distinct roots in characteristic zero, both
+operators are diagonalizable and equal multiplicities suffice for similarity.
+
+This is constructive with rational dyadic matrices. Let
+W_f[x,y]=(-1)^popcount(x&y). Its column y has C_f eigenvalue
+i^popcount(y), and W_f^-1=2^-f W_f^T. Let U be the direct sum of q copies
+of W_f, retaining the inverse direction in the eigenvalue list for the last
+b copies. Let V be W_h tensor I_t, with columns reordered to match U's
+eigenvalues after multiplication by lambda. Equal multiplicities guarantee
+this matching. Then
+
+```
+E = V U^T / 2^f,    E^-1 = U V^T / 2^h,
+H E = E T.
+```
+
+Both products of the unscaled encoding and decoding numerators equal
+2^(f+h) I. Extend E by I_d to retain any dirty complement. Thus the identity
+holds for every input column, including arbitrary independent dirty data.
+This construction does not require that E itself be a native operation.
+
+## First new identity and sharp minimum batch
+
+Taking f=2, a=3, b=1 gives q=4, delta=2 and j=1. Therefore
+
+```
+C_2 direct-sum C_2 direct-sum C_2 direct-sum C_2^-1
+    = E^-1 (-i C_4) E.
+```
+
+This is a 16-coordinate identity. PR1920's balanced opposite pair has zero
+first trace at f=2 and cannot do this. Any proper width upgrade in the
+present model has j>=1 and hence q>=4^j>=4. The four-lane batch is minimal.
+More generally the conditions give a minimum q=4^j for a width increase 2j,
+attained by a=(4^j+2^j)/2 and b=(4^j-2^j)/2 for every j>=1.
+This minimum is an algebraic batch size, not an operation-cost claim.
+
+## Cost and applicability limit
+
+Under the inherited PR679 expression A V f^sigma per full lane, with
+A,V>0 and 0<sigma<1, the q separate lanes have expression q A V f^sigma.
+The joined child occupies all qV coordinates and has expression
+q A V (f+2j)^sigma before encoding, decoding and every other extra cost.
+For j>0 its ratio is (1+2j/f)^sigma>1. This is a comparison of available
+upper expressions, not a lower bound on optimal runtime. The identity
+does not establish the card's favorable complete-invoice gate.
+
+The congruence condition applies to the literal tensor width f. An operation
+whose literal width varies with a column parameter would need an implementation
+for every required width. This package supplies no such uniform supplier,
+native encoding, physical placement, scalar-read tariff, precision/tape proof,
+restoration schedule for the encoder, new kappa or multiplication theorem.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Proof versus finite corroboration
+
+The preceding argument proves the quantified statement. The standalone
+verifier independently compares its integer classification with literal
+binomial eigenspace counts, and constructs four dense rational encoders.
+It checks both inverse orders and every coefficient of H E=E T using
+Gaussian integer tensor coefficients, including identity complements.
+Those finite checks corroborate the proof; they are not extrapolated to
+unbounded widths or converted into physical costs.

research/mixed-clifford-dyadic-imbalance/README.md

@@ -0,0 +1,140 @@
+# Exact directional imbalance for mixed Clifford lanes
+
+This contribution is produced by Nick Petalas. Apache-2.0.
+
+Scoped algebraic proof with finite corroboration. For literal tensor widths
+f=2 modulo 4, an unbalanced collection of forward and inverse Clifford lanes
+can sometimes be one wider child under an arbitrary reciprocal linear
+encoding. The first new identity uses three forward width-two lanes and one
+inverse lane on 16 coordinates:
+
+```
+C_2 direct-sum C_2 direct-sum C_2 direct-sum C_2^-1 = E^-1 (-i C_4) E.
+```
+
+Four lanes are necessary and sufficient for a proper width upgrade in this
+model. This differs from Arham Tahir's PR1920 balanced-pair result, which
+excludes an opposite width-two pair. The spectral and Walsh methods are
+inherited; the arbitrary directional multiplicities and exact integer
+classification are the new contribution. No literature priority is claimed
+for elementary spectral similarity or prime valuations.
+
+## Exact classification
+
+Let a,b be the forward/inverse counts, q=a+b>0, and delta=a-b. With the
+convention C=((1+i)I+(1-i)X)/2 and C_f=C tensor ... tensor C, a single
+forward child lambda (C_h tensor I_t) is similar to the independent lanes
+exactly when, for an integer j>=0,
+
+```
+q = 2^j |delta|,    4^j divides q,
+h = f+2j,          t = q/4^j,
+lambda = sign(delta) i^(-j).
+```
+
+In particular a=b never works at these widths. The smallest batch for an
+increase 2j is q=4^j. All payload coordinates are independent arbitrary
+inputs. Arbitrary restored dirty complements can be mixed by the encoder;
+they cannot increase the active child volume. [PROOF.md](PROOF.md) gives
+necessity, sufficiency, explicit rational dyadic encoding/decoding, the exact
+complement statement and the inherited volume-cost limitation.
+
+This is an algebraic interface identity. The joined child loses the inherited
+PR679 full-volume upper expression even with free adapters. Physical/native
+encoding, frame conversion, reads, storage, routing, precision, restoration
+and every complete consumer cost remain unpaid. Widths in other congruence
+classes and a uniform implementation at every column multiplicity are outside
+this theorem. No supplier admission, new kappa or multiplication theorem is
+claimed. Independent human and formal proof-kernel review are unclaimed.
+
+## Reproduce
+
+From the repository root, using the standard library and CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mixed-clifford-dyadic-imbalance
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/mixed-clifford-dyadic-imbalance/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/mixed-clifford-dyadic-imbalance/verify.py
+```
+
+The interpreter path is local; reviewers elsewhere can substitute their
+CPython 3.12 executable. The verifier is read-only and also works in a
+Git-free package export. Its JSON receipt is generated, includes file SHA256
+hashes, and is printed to stdout. No saved receipt is a proof input.
+
+The finite sweep enumerates every a,b with 1<=a+b<=64 at widths
+f=2,6,...,30. It checks 17,152 target multiplicity lists against 1,170,400
+dimension-compatible phased candidates. There are 1,360 matches, of which
+336 are proper width upgrades. The uniform boundary cases are controls,
+not predecessor results claimed anew. A separate cyclic recurrence checks
+all 37 binomial spectrum lists used in the sweep.
+
+Four dense rational witnesses cover both imbalance signs, a nontrivial
+spectator factor, a four-width increase, and arbitrary dirty identity
+complements. They check 5,870 entries of H E=E T, plus both inverse products
+for every fixture. Exact Gaussian tensor coefficients are constructed
+separately from the Walsh eigenbasis. Controls reject a wrong phase,
+direction, encoder, dirty output, balanced batch, nondyadic imbalance and
+nonintegral spectator count, plus four invalid domains. All checks remain
+enabled under optimized Python.
+
+The written proof establishes the quantified result. Finite enumeration
+alone is not an unbounded proof. No predecessor verifier, selected cold
+replay, native implementation, Lean or Docker build is run for this result.
+
+## Scope and overlap
+
+Base canonical main is `624de9dc66858af0945e5f8a0942488d62280d43`, priority
+revision 7. [The advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133741)
+states the delivered target. [TASK.json](TASK.json) records the changed scope
+from physical synthesis to an exact prerequisite classification and the
+bounded stop rule. The current selected source-binding orientation passed.
+The card's historical ceiling command failed with `KeyError: complex_profile`
+against the changed selected schema; it supplies no evidence here.
+
+Overlap checks read current open PRs, this account's recent work, recent
+handoffs, active Discussions, targeted merged PRs and distinctive terms in
+all main READMEs. The cached search covers 379 open PRs and 3,853 Discussion
+records, but only 101 of 6,319 local-main notes were materialized. This does
+not cover unpublished work or every code diff. Exact predecessor READMEs are
+historical provenance in [SOURCES.json](SOURCES.json); no predecessor code is
+imported or copied. The standalone verifier has no external proof input.
+
+The implementation has no recursion or background work. The entrypoint fixes
+every finite enumeration range; dense matrices have at most 67 rows and
+columns. Python allocates integers and collections dynamically, a managed
+runtime deviation from fixed allocation. Live matrices are bounded by those
+fixture caps. Functions stay below 60 physical lines. Warning-strict normal
+and optimized execution are the registered diagnostics; no static type or
+native-code analysis is claimed.
+
+## Credit
+
+Arham Tahir, PR1920, supplied the reciprocal full-space contract, equal-width
+uniform and balanced-pair results, trace invariants and Walsh construction.
+Adam Gall, PR1946, classified two unequal-width equal-volume lanes, a
+different multiplicity contract. The exact correction-rank work by ywz65
+concerns an additional nonreciprocal adapter, which this theorem does not
+allow. Greer Guthrie, PR679, and Ross Richardson's diagonal-child contract
+audit supplied the inherited volume-aware scope and tariff. ToikY, PR1924,
+and Douglas Colkitt, PR665, supplied distinct clean-injection/spectral
+interfaces. Jose Manuel/jmbarrancoml with Cinna Davis/1337isnot1337, PR1779,
+and Josie Elliston, PR1817, supplied the batching motivation and retiming
+context. Credit icekylinx, DreamingOfClouds, Rohan Arun, Jeremy Kothe,
+Hao Yan and the retained native-kernel/construction lineage. Their original
+credit and source files remain unchanged.
+
+## Open next questions
+
+- Can a real three-forward/one-inverse width-two caller support a different,
+  favorable fully paid operation or volume contract? First name its actual
+  charts, inputs, outputs and complete adapter ledger. No such physical
+  caller or cheaper tariff is supplied here.
+- Can a uniform supplier exploit this exception while supporting every
+  required literal width? First pin one caller's column parameter, derive
+  its admissible congruences, and price a legal fallback. An actual caller
+  and all-size cost contract remain missing.
+
+The structured questions in TASK.json give their relevance, first steps and
+blockers. Further reciprocal basis searches under the same losing tariff
+are not justified by this algebraic identity.

research/mixed-clifford-dyadic-imbalance/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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/clifford-reciprocal-basis-obstruction/README.md",
+      "usage": "provenance",
+      "git_blob": "6aff66509d3748445d33847e90a0abbafca14263",
+      "sha256": "ecef2b644bfb28083d9220f56aed2903c778c96851d5c6daa749bd974bbbdf24"
+    },
+    {
+      "path": "research/complex-heterogeneous-child-interface/README.md",
+      "usage": "provenance",
+      "git_blob": "72f125c320ee6f0ccfeff4c6373d1b5081361e2e",
+      "sha256": "de40ae7874788a3f4875d41e9a294c3a1a78f4fec1f1f0b7677e60cdd5eed670"
+    },
+    {
+      "path": "research/clifford-sharp-correction-rank/README.md",
+      "usage": "provenance",
+      "git_blob": "457263eece572398f3ddadd87793d0a189413f93",
+      "sha256": "767b6d8c72561026cf6dea31db5d5ef86dfb7b35c33d66fe4366b71ae744bfe3"
+    }
+  ]
+}