Give native output prefixes optimal unbiased variance (no κ)

research/native-prefix-balanced-coarsening/ORIGIN.json

@@ -0,0 +1,9 @@
+{
+  "author": "Ali Romman",
+  "url": "https://github.com/aliromman/integer-mult-bounds/blob/5f7c893b6af9a75cb19ad22c6db06ed22eea6f54/research/native-coarse-grid-residue-codec/PROOF.md",
+  "pr": 6540,
+  "head": "5f7c893b6af9a75cb19ad22c6db06ed22eea6f54",
+  "path": "research/native-coarse-grid-residue-codec/PROOF.md",
+  "sha256": "2322e9b613004aa4278ba6cdefea2bf68df01fcd5eb502208928539b36dfa1c7",
+  "usage": "Cited Gaussian quotient and native-grid premises; no predecessor executable is invoked."
+}

research/native-prefix-balanced-coarsening/PROOF.md

@@ -0,0 +1,151 @@
+# Prefix-balanced native coarsening
+
+This is a scoped mathematical proof of a changed numerical interface. The new
+step is the compatibility of cumulative stochastic rounding with the native
+coarse-period codec, including simultaneous optimal prefix variances and the
+extra scan cost. It is not a complete multiplication theorem.
+
+## Premises and credit
+
+Use Ali Romman's [PR6540](https://github.com/CrocSwap/integer-mult-bounds/pull/6540)
+at `5f7c893b6af9a75cb19ad22c6db06ed22eea6f54` for the Gaussian operator and
+quotient premises below. Its exact proof is retained in
+[inputs/PR6540-PROOF.md](inputs/PR6540-PROOF.md), with origin and hash in
+[ORIGIN.json](ORIGIN.json). Its scientific executable is not invoked. Gaussian
+Smith coordinates and the earlier native/compiler lineage keep their credit.
+
+Cumulative rounding is classical. Knuth's
+[two-way rounding](https://arxiv.org/abs/math/9504228) and Doerr, Friedrich,
+Klein and Osbild's [unbiased matrix rounding](https://arxiv.org/abs/cs/0604068)
+give broader controlled-rounding context. Neither cumulative rounding nor the
+scalar unbiased-variance inequality is claimed as new here.
+
+Let A=L C_r R be the predecessor's Gaussian-unit monomial native recipe at
+tensor width f>=1. Write N=512^f, a=r*f, d=ceil(a/2), m=2^k, k>=d and
+D=2^(k+d). Its central pair is
+
+```text
+C = [[1+i,1-i],[1-i,1+i]]/2.
+```
+
+For every x in Z[i]^N the vector n=2^d A x is integral Gaussian, and
+B=m A^-1 is integral Gaussian. The lattice quotient Z[i]^N / B Z[i]^N
+has exactly 2^(2kN) elements. The predecessor supplies a label ell(x) with
+2kN bits and a representative x0(ell), with x-x0 in B Z[i]^N. These are cited
+premises, not new quotient or source-admission claims.
+
+Fix an order of the 2N real components after applying A. The input and order
+are fixed before drawing a fresh uniform u in {0,...,D-1}, conditionally on
+the entire incoming state and history. Physical values use input unit h/m
+and output unit h, for h>0. No initial component of x is assumed zero.
+
+## The new quantizer
+
+Flatten n into n_1,...,n_t, t=2N. Set S_j=sum_(i<=j) n_i, S_0=0, and
+
+```text
+q_j = floor((S_j+u)/D) - floor((S_(j-1)+u)/D).
+```
+
+Equivalently, keep c_0=u and compute
+
+```text
+(q_j,c_j) = divmod(n_j+c_(j-1),D),   0 <= c_j < D.
+```
+
+The invariant D*sum_(i<=j) q_i+c_j=S_j+u proves the equivalence even for
+negative inputs. For a fixed j, c_(j-1)=(S_(j-1)+u) mod D is uniform on the
+D residues. Consequently q_j is an adjacent-integer unbiased rounding of
+n_j/D. Every individual coordinate retains the predecessor's pointwise
+minimum mean squared error. In particular the total Euclidean mean squared
+error remains at most N*h^2/2.
+
+More strongly, each prefix sum is exactly floor((S_j+u)/D). If
+t_j=S_j mod D, then
+
+```text
+E[h*sum_(i<=j) q_i | x] = h*S_j/D,
+Var[h*sum_(i<=j) q_i | x] = h^2*t_j*(D-t_j)/D^2 <= h^2/4.
+```
+
+Its absolute error is less than h for every seed, and it is exact whenever
+S_j/D is integral. All these statements hold simultaneously for every prefix
+in the fixed order. For any integer-valued unbiased output with mean b+p,
+0<=p<1, the inequality (Z-b)*(Z-b-1)>=0 gives Var(Z)>=p*(1-p).
+Thus each displayed prefix variance is the least possible among all unbiased
+grid-valued vector outputs, without any reversibility assumption.
+
+## Translation and the exact inverse
+
+For any integer real vector z, replacing n by n+D*z increases q_j by z_j
+and leaves every carry unchanged. In Gaussian coordinates this proves
+
+```text
+Q_u(x+B*z) = Q_u(x)+z.
+```
+
+Use exactly the cited label ell. Encode x as (Q_u(x),ell(x)). Given any
+coarse q and label ell, compute
+
+```text
+x0 = x0(ell),
+z = q-Q_u(x0),
+x = x0+B*z.
+```
+
+Translation gives Q_u(x)=q, and addition of B*z preserves ell. Conversely,
+an original x differs from its representative by a unique B*z, and this
+formula recovers it. Hence this is a two-sided bijection for each retained
+seed. It changes neither the 2kN-bit label nor the k+d-bit uniform seed.
+The predecessor's full-grid capacity and fixed-fair-bit lower bounds apply
+to the same input domain and means. No better capacity bound is claimed.
+
+The finite reference instantiates the canonical C axes and their Gaussian
+Smith coordinates. The written translation proof applies also to the cited
+L,R phases/permutations and arbitrary tensor widths. The finite program's
+size/payload guards are not an all-width physical implementation.
+
+## A strict native improvement and sharpness
+
+For the canonical unphased native operator at N=512, r=8, k=5, take every
+Gaussian input component equal to 16+16i. C and all its tensor powers fix
+constant vectors, so all 1024 real output means are 1/2. The predecessor's
+common-coordinate threshold makes the entire sum either 0 or 1024 with equal
+probability. Its error variance is 512^2*h^2=262144*h^2.
+
+The new total is identically 512, so its error variance is zero on this same
+input. Both constructions have the same coordinate marginals, 5120-bit
+residue capacity and nine-bit seed. This is a comparison for this fixed
+reader and input, not a new Euclidean-error optimum or caller kappa.
+
+The new uniform quarter-variance bound is sharp for this native family.
+Take x_0=16 and every other Gaussian input zero. Column sums of C and its
+tensor powers are one, so the full real-component sum has ideal value 1/2.
+Its rounded sum is an unbiased Bernoulli output and has variance h^2/4.
+
+## Complete cost change and remaining obligations
+
+Keep the predecessor's native evaluations, Gaussian quotient transforms,
+digit extraction/reconstruction, routing and retained-label costs. Each of
+the two quantizer passes in an encode/decode round trip visits 2N real
+coordinates. Each visit still adds one offset and takes a floor quotient,
+and now also computes its remainder modulo D. The added work is exactly
+4N remainder extractions, plus two carry initializations from the retained
+seed. The carry has k+d bits and can be reused between the sequential passes.
+It introduces a serial dependence along the chosen output order.
+
+Because D is a power of two, a remainder is the low k+d bits, including for
+negative integers under floor division. The carry never grows with N. If a
+numerator has magnitude below 2^W, adding c<D needs at most max(W,k+d)+2
+signed bits. There is no full prefix-sum accumulator in this implementation.
+The added indexed bit work is O(N*(W+k+d)) and the added live carry capacity
+is k+d bits. These are ordinary integer-reference costs. No reversible gate,
+dirty-temporary cleanup, seed sampler, fixed-tape schedule or recursive
+tariff is supplied by calling a remainder extraction free.
+
+A selected consumer must actually use the declared ordered prefix readers
+before this numerical bound can improve its precision budget. An arbitrary
+later linear reader need not benefit. Adaptive seed reuse, a changed order
+chosen after seeing u, whole-word accumulated errors, native supplier admission,
+precision/stock/tape/compiler/outer closure and all five selected framework
+assumptions remain unresolved. No new kappa or frontier change follows.

research/native-prefix-balanced-coarsening/README.md

@@ -0,0 +1,115 @@
+# Prefix-balanced native coarsening
+
+This contribution was produced by Nick Petalas.
+
+Claim type: scoped mathematical proof with exact finite corroboration. Replacing
+PR6540's shared coordinate threshold with a cumulative carry gives every fixed
+output prefix its minimum unbiased grid variance, at most `h^2/4`. Coordinate
+marginals and their minimum Euclidean mean squared error remain the same.
+The Gaussian native codec keeps its `2kN`-bit residue and `k+ceil(rf/2)`-bit
+fresh seed, with an exact two-sided inverse for arbitrary fine-grid inputs.
+
+The new result is the native codec substitution, translation proof, simultaneous
+prefix optimum and explicit extra scan cost. Cumulative rounding, scalar
+variance inequalities and Gaussian Smith coordinates are credited prior work.
+See [PROOF.md](PROOF.md) for the proof and full limitations.
+
+On a canonical 512-coordinate rank-eight native example, the full sum of real
+components has error variance `262144*h^2` with the shared threshold and zero
+with the carry. A second input attains the new uniform `h^2/4` bound. This is
+a fixed-reader precision improvement, with no new kappa or selected-frontier
+change. Investigation stopped at this first verified improvement.
+
+## Evidence and reproduction
+
+The exact standard-library verifier checks:
+
+- 5,050 complete small residue vectors through length four, with signed integer
+  translates, 38,860 seed vectors and 10,100 translation cases.
+- 3,264 arbitrary coarse-output/label/seed endpoints of the new two-sided codec.
+- All 1,920 seeds for eight canonical 512-coordinate native ranks, and 48
+  additional fine/coarse codec round trips.
+- The strict-improvement and sharpness examples, nine rejected domains, a
+  reset-carry mutant, a missing-seed mutant and a missing-residue collision.
+
+From the repository root, with CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/native-prefix-balanced-coarsening/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/native-prefix-balanced-coarsening/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/native-prefix-balanced-coarsening
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/native-prefix-balanced-coarsening --check-source-history
+```
+
+Any CPython 3.12 path can substitute. Expected scientific marker:
+`PASS_NATIVE_PREFIX_BALANCED_COARSENING`. Optional `--receipt /absolute/path.json`
+writes a generated receipt outside the package, binding every package file hash
+to the computed counts. The verifier writes no checkout artifacts by default.
+Normal and optimized modes use the same executable contracts.
+
+## Sources, scope and costs
+
+Ali Romman's [PR6540](https://github.com/CrocSwap/integer-mult-bounds/pull/6540),
+head `5f7c893b6af9a75cb19ad22c6db06ed22eea6f54`, supplies the native grid and
+Gaussian quotient premises. Its exact proof and attribution are retained with
+a hash in [ORIGIN.json](ORIGIN.json). No predecessor scientific executable or
+selected cold replay is run. The new finite reference instantiates canonical C
+axes; the written proof applies to the cited monomial recipes at every width.
+Knuth and Doerr, Friedrich, Klein and Osbild retain the controlled-rounding
+credit linked in the proof. The quotient lineage includes Dugongue's PR5815,
+Ali Romman's PR5821 and Nick Petalas's PR5880. Cinna Davis's native interfaces,
+DreamingOfClouds's selected word and the retained Gaussian/native/compiler
+lineage keep their credit. No general literature-priority claim is made.
+
+An encode/decode round trip adds `4N` remainder extractions and two carry
+initializations. The added live carry needs `k+ceil(rf/2)` bits. Native
+evaluations, quotient transforms and label digits retain their existing costs.
+The scan is serial in the chosen output order. Reversible temporary cleanup,
+seed sampling, storage lifetimes, physical routing and the complete tape and
+recursive invoice remain unpriced.
+
+The original `centre-path-sharing` card is changed to a numerical boundary side
+result. It supplies no selected consumer or eliminated paid operation. Arbitrary
+later linear readers, an order chosen after observing the seed, adaptive seed
+reuse and complete accumulated caller error are outside the result. All five
+selected framework assumptions remain. Lean, Docker, complete native admission,
+independent human review and formal proof-kernel review are unrun or unclaimed.
+
+The package is based on canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8 and selected
+PR6030. The live selected binding command passed. Main/merged searches, account
+contributions, open PRs, handoffs and local reservations were checked. The
+overlap cache covered 521 open PRs and 6,527 Discussion records; local sparse
+notes, arbitrary historical diffs and unpublished work remain coverage limits.
+
+## Open next questions
+
+1. Can a selected native consumer use the declared fixed prefix order? Pin one
+   event and enumerate its actual readers. A source-bound consumer and complete
+   error/precision invoice are missing.
+2. Can the carry scan and residue codec fit a physical caller budget? Start with
+   one 512-coordinate round trip, including its 2,048 added remainder steps,
+   seed/residue lifetimes and temporary cleanup. Physical routing, reversible
+   gates and a complete paid invoice remain blockers.
+
+The structured questions are in [TASK.json](TASK.json).
+
+## Implementation bounds
+
+The exact reference permits at most 512 complex coordinates, eight active
+axes, precision at most 16 and integer payloads at most 4,096 bits. There is
+no recursion. Functions are at most 31 lines; all loops have bounds from these
+limits or the fixed verification fixtures. Explicit `require` contracts remain
+active under optimized Python.
+
+Power-of-Ten rule 3 has a managed-runtime deviation in `model.py` and
+`verify.py`: Python allocates tuples and arbitrary-precision integers during
+operation. Finite shapes and payload guards bound live data. Verification uses
+at most 1,024-component moment accumulators and a 16,384-bit residue label.
+No hard allocator or hardware memory bound is claimed. A physical fixed-buffer
+implementation is the follow-up when a consumer contract is selected.
+Warning-strict normal/optimized replay and in-memory syntax compilation are
+the available diagnostics; no standalone type checker is required by this
+standard-library package.
+
+Apache-2.0, under the repository license.

research/native-prefix-balanced-coarsening/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}