Prove exact optimal ordering of heterogeneous Smith axes (no κ)

research/smith-axis-order/PROOF.md

@@ -0,0 +1,172 @@
+# Optimal axis order for heterogeneous Smith tensors
+
+This contribution was produced by Nick Petalas. New material is Apache-2.0.
+Credit Dugongue / David Ganz, PR [#5815](https://github.com/CrocSwap/integer-mult-bounds/pull/5815)
+at `f0fcda576df410dc15cd5b8183d4f74d284eba2b`, for the Gaussian integral
+Smith word and its complete two-pass addition-precision accounting, especially
+consumer-construction.md C2–C8. Tensor products, valuation arithmetic and
+adjacent-exchange proofs are classical. No literature-wide priority is claimed.
+
+## 1. Changed premise and exact tariff
+
+Put pi=1+i, and fix n>=1 nonnegative integers a_1,...,a_n. Define
+
+```text
+S = [[i,0],[1,1]],       T = [[1,-i],[0,1]],
+C_a = S diag(1,pi^a) T = [[i,1],[1,pi^a-i]],
+F_a = tensor_j C_(a_j),  N=2^n.
+```
+
+The Gaussian factor in #5815 is C_2. We allow unequal gaps a_j. This changes
+the tensor being computed; we do not claim an order improvement for its
+identical C_2 axes. Input coordinates are arbitrary Gaussian integers. The
+endpoint is every coordinate of F_a x modulo pi^P, for an integer P>=0.
+Normalization by pi^-B instead gives the same calculation with raw modulus
+P=p+B, whenever this raw modulus is nonnegative.
+
+We permit independent axis permutations sigma for the T gather and tau for
+the S delivery, at fixed coordinate indices. There are no axis swaps of the
+data. Each scalar ADD performed at q residue digits costs exactly q in this
+tariff, including q=0. The theorem minimizes the sum of this mass over **both**
+passes. It does not minimize shifts, phases, routing, allocation, truncation,
+cleanup, bit time, or all implementations of F_a.
+
+## 2. A legal modular word for every pair of orders
+
+Work in an owned copy of the input, initially reduced modulo pi^P. After
+gathering a set A of axes, a coordinate u has precision
+
+```text
+q(u,A) = (P - sum_(j in A) a_j u_j)_+.
+```
+
+For the next axis j, a low/high pair differs only at bit j and has common
+current precision q. Execute
+
+```text
+low  <- low - i*high mod pi^q
+high <- high mod pi^(q-a_j)_+
+```
+
+The subtraction precedes truncation. Later T axes do not change the already
+processed bits. Therefore each discarded error, on reaching the diagonal
+tensor factor, receives at least the valuation sum that paid for its loss.
+If that sum is >=P, the entire coordinate may be replaced by zero. This
+proves the gather invariant and correctness of truncation by induction.
+
+After all T axes, a coordinate represents pi^e z, where
+e=sum_j a_j u_j and z is known modulo pi^(P-e)_+. We need not physically
+multiply all diagonal entries into a common-precision array.
+
+During delivery let B be the remaining axes. A pair at axis j in B has tags
+e and e+a_j, where e=sum_(h in B minus {j}) a_h u_h. Its represented values
+are pi^e z_0 and pi^(e+a_j) z_1. With q=(P-e)_+, execute
+
+```text
+z_1 <- z_0 + pi^a_j * z_1 mod pi^q
+z_0 <- i*z_0 mod pi^q
+give both coordinates tag e and precision q.
+```
+
+These are precisely S applied to the represented pair. The old z_1 needs
+only (q-a_j)_+ digits. When q-a_j<0, its missing contribution is already
+zero modulo pi^q. The new z_0 phase follows the addition. At the end all
+tags are zero and all precisions are P. Thus this word computes every
+required output for arbitrary inputs, for every sigma and tau. Original
+inputs are preserved. This ordinary modular word uses the declared owned
+truncation/erasure contract; it is not a reversible implementation.
+
+## 3. Exact mass formula
+
+For a set A of axes define the rational average
+
+```text
+H(A) = 2^(-|A|) sum_(U subset A) (P - sum_(j in U) a_j)_+.
+```
+
+For a gather order sigma, let A_m contain its first m axes, including A_0
+empty. Among its N/2 pairs at the next stage, each processed bit pattern
+occurs equally often, so
+
+```text
+M_T(sigma) = (N/2) sum_(m=0)^(n-1) H(A_m).
+```
+
+For delivery order tau, the ADD at a stage depends only on axes remaining
+after that stage. Their sets, read backwards, are the prefixes of reverse(tau).
+The same counting gives the exact identity
+
+```text
+M_S(tau) = M_T(reverse(tau)).
+```
+
+All actual stage masses are integers: a stage uses at most n-1 averaging
+bits, which are paid by the factor N/2. The formula counts every scalar pair
+of both passes, rather than only the diagonal bank or one pass.
+
+## 4. Adjacent exchange and all equality cases
+
+Take adjacent gather axes with gaps a,b after an arbitrary prefix A. Let
+X=sum_(j in A) a_j U_j, where U_j are independent uniform binary bits, and
+write f(t)=max(t,0). The first stage cost is unchanged by the exchange;
+every later stage has the same prefix set. The difference of the two
+normalized gather sums is exactly
+
+```text
+D(a,b | A) = (1/2) E[ f(P-X-a) - f(P-X-b) ].
+```
+
+If a>=b, every summand is <=0. If a>b and P>b, the event with all prefix
+bits zero has positive probability and gives a strictly negative summand.
+If P<=b, both summands vanish for every X>=0. Hence for a>b the exchange
+is strict exactly when P>b.
+
+Define clipped gaps b_j=min(a_j,P). An order has minimum gather mass **if
+and only if** its clipped gaps are nonincreasing. Sufficiency follows by
+sorting all adjacent inversions; swaps within a clipped tie have zero cost.
+For necessity, any sequence that is not nonincreasing has an adjacent
+increase in its clipped gaps. Swapping that pair strictly decreases cost,
+by the preceding calculation. This includes P=0 and arbitrary zero gaps.
+
+The exact delivery minimizers are the orders with clipped gaps
+nondecreasing, by Section 3. The two order choices are independent, so
+these conditions characterize every minimizing pair (sigma,tau).
+
+In particular, sort the actual gaps descending for gather and ascending
+for delivery. If a_[1]>=...>=a_[n] is that sorted list, the exact optimum is
+
+```text
+M_min = N sum_(m=0)^(n-1)
+          2^(-m) sum_(U subset {1,...,m}) (P-sum_(j in U) a_[j])_+.
+```
+
+Once the orders are chosen, this is an explicit finite formula, with no
+search over permutations. The written theorem has no executable size limit.
+
+## 5. First strict improvement
+
+For gaps (1,4) and P=3, use the same fixed four-coordinate target throughout.
+
+```text
+gather gaps (1,4), delivery gaps (4,1): 11+11 = 22
+gather gaps (4,1), delivery gaps (1,4):  9+ 9 = 18
+```
+
+Both words have eight nominal scalar ADD positions; a zero-precision ADD
+contributes zero mass. The optimized word saves four residue-digit ADD
+units. Its literal modular execution and independent dense tensor outputs
+agree. This is an exact component-work comparison, not a runtime speedup.
+
+Equal gaps make every order tie. More generally, gaps >=P are all tied even
+if their actual values differ. Ordering heterogeneous physical axes can
+change movement costs, which this theorem does not absorb into its tariff.
+
+## 6. Evidence boundary
+
+The verifier exhausts its declared small profiles and orders, separately
+enumerates actual stage pairs, checks the exchange identity and all equality
+cases, and compares the new heterogeneous modular word with direct dense
+tensor multiplication. Odd moduli are checked through their Gaussian parity
+lattice. These checks corroborate this written proof. No predecessor result
+or verifier is replayed or audited. No selected source, supplier admission,
+five framework assumption, or complete multiplication theorem is changed.

research/smith-axis-order/README.md

@@ -0,0 +1,114 @@
+# Exact optimal ordering of heterogeneous Smith axes
+
+This contribution was produced by Nick Petalas. New material is Apache-2.0.
+
+**Scoped proof with finite corroboration; no new kappa.** For a tensor of
+integral factors `C_a = [[i,1],[1,(1+i)^a-i]]`, arbitrary Gaussian-integer
+inputs, and every raw residue precision P>=0, the minimum complete two-pass
+addition-precision mass is attained by descending valuation gaps in the
+triangular gather and ascending gaps in delivery. Every optimal order is
+classified by sorting the clipped gaps `min(a,P)` in those directions.
+
+The first strict example has gaps (1,4) and P=3: the same four-coordinate
+tensor costs **18 instead of 22** residue-digit ADD units. Both words have
+eight nominal ADD positions. This is an exact arithmetic-work comparison,
+not a measured runtime or an admitted supplier.
+
+[PROOF.md](PROOF.md) gives the all-size modular word, full two-pass formula,
+adjacent-exchange identity, equality cases and proof. [circuit.py](circuit.py)
+implements the new heterogeneous circuit and ordering; [verify.py](verify.py)
+uses independent coordinate-pair accounting, dense tensor multiplication and
+Gaussian parity-lattice congruence checks. It imports no predecessor code.
+
+## Relation to the source and current priorities
+
+Credit Dugongue / David Ganz's [PR #5815](https://github.com/CrocSwap/integer-mult-bounds/pull/5815),
+exact head `f0fcda576df410dc15cd5b8183d4f74d284eba2b`, for the integral Gaussian
+Smith circuit, propagated moduli, complete two-pass accounting, and the
+parameter-efficiency continuation. In particular, consumer-construction.md
+C2–C8 supplies the starting word. Tensor factorization, valuation arithmetic
+and adjacent exchanges are classical; no literature-wide priority is claimed.
+
+The new step changes identical Gaussian gaps a=2 to **unequal supplied
+gaps** and optimizes the entire order class, including delivery. Identical
+Gaussian gaps tie, so this adds no ordering gain to #5815's existing word.
+No earlier implementation or mathematical result was audited or replayed.
+
+This is a declared side result from the formal-interface-lemma card, rather
+than a formal-kernel or selected-caller proof. It can guide a heterogeneous
+ordinary tensor backend once such a backend's complete physical bill is
+supplied. The selected .00310045 result and five assumptions retain their
+status. Main was refreshed at `de5ec2e7a6074068452f45b1a191b5c72832df4a`,
+priority revision 8. The source limitations and live overlap searches are in
+[TASK.json](TASK.json) and [SOURCES.json](SOURCES.json).
+
+## Reproduce
+
+From the worktree root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/smith-axis-order/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/smith-axis-order
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/smith-axis-order --check-source-history
+```
+
+Any CPython 3.12 path may replace the shown interpreter. The direct verifier
+ends `PASS_SMITH_AXIS_ORDER`; registered verification also runs optimized
+Python. To save a generated, package-hash-bound receipt, pass
+`--receipt /path/outside-the-checkout/receipt.json` to the direct verifier.
+Default execution writes no files. Counts are printed from actual enumeration.
+
+## Local evidence
+
+- All 153,405 physical-axis orders across 2,259 profile/precision cases pass;
+  all 593,730 adjacent-exchange identities pass. Profiles are nondecreasing
+  multisets of 1–5 gaps in 0–4, precisions 0–8, with every physical-axis
+  permutation including repeated-gap permutations.
+- 18,648 basis endpoints and 4,320 arbitrary-input endpoints agree with a
+  direct dense tensor oracle: all ordered profiles in 0–2 through four axes,
+  precisions 0–5, and the optimal/opposite order pairings.
+- 357 complete finite-ring input cases cover gaps 0,1,2,4 in one axis and
+  (1,4) in two axes, at precisions 0–2. Thirteen malformed inputs reject;
+  six semantic controls cover strictness, clipped ties, corrupted output,
+  early truncation and omitted delivery.
+
+The counts are finite corroboration of the separate written proof. These are
+not independent human review or formal proof-kernel results.
+
+## Limits and engineering inspection
+
+The executable accepts 1–8 axes, gaps and precision in 0–64, and Gaussian
+input components of height at most 10^6. The proof covers all finite n and
+nonnegative integer gaps and precisions. Finite tests cover smaller ranges;
+they do not establish the universal theorem by themselves.
+
+The tariff is the sum of operand precision for all ADDs in both declared
+triangular passes. Phase, scale, truncation, owned storage, cleanup, access,
+physical layout and full compiler costs remain separate. Axis scheduling
+does not permute coordinates in this indexed circuit, but a physical tape
+host still needs its access bill. Owned truncation is permitted; reversible
+truncation is a different contract. No Lean, Docker, supplier cold replay or
+complete rounded multiplier was run. Independent human and formal
+proof-kernel review are unclaimed.
+
+All loops have finite bounds from at most eight axes and 256 coordinates;
+verification domains are fixed. There is no recursion or network dependency.
+Python allocation and arbitrary-precision integers are explicit managed-runtime
+deviations from fixed allocation: live arrays are bounded by 256 coordinates,
+and tensor valuation exponents by 512. The verifier's largest dense matrix
+has 256 Gaussian entries. Local module loading and the sorting key are bounded
+dispatch deviations. Relevant diagnostics, ordinary and optimized replays,
+boundary rejections and committed-byte checks are recorded in the PR.
+
+## Open next questions
+
+1. **Unequal per-axis ADD prices.** Which order minimizes the bill when axes
+   have different physical prices? It matters when routing or coefficient
+   work varies by axis. Start with the two-axis exchange formula, now weighted
+   by those prices, and look for context-dependent comparisons. A universal
+   sorting rule is unproved.
+2. **One actual heterogeneous backend.** Does an existing caller produce
+   unequal Smith gaps whose complete physical bill benefits from this order?
+   Start with one explicitly supplied tensor factorization and source-bound
+   input/output grids. Actual routing, scales, truncation, cleanup and consumer
+   costs block a supplier or kappa conclusion.

research/smith-axis-order/SOURCES.json

@@ -0,0 +1,28 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "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"
+    }
+  ],
+  "external_context": [
+    {
+      "repository": "CrocSwap/integer-mult-bounds",
+      "pull_request": 5815,
+      "head": "f0fcda576df410dc15cd5b8183d4f74d284eba2b",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5815",
+      "path": "research/gaussian-exceptional-correction/consumer-construction.md",
+      "usage": "Bibliographic context only; C2-C8 cited, no code import, replay or source-byte acceptance dependency. The new factor, word and proof are fully restated in PROOF.md."
+    }
+  ]
+}