Count exact nonzero carries for every reduced rational shear (no κ)

research/rational-shear-carry-density/PROOF.md

@@ -0,0 +1,151 @@
+# Exact canonical carry frequency for a rational shear
+
+## Contract and result
+
+Fix a nonzero reduced rational coefficient `c=a/h`, where `a` is an integer,
+`h>=1`, and `gcd(|a|,h)=1`. Let `q>=2` be an integer with `gcd(q,h)=1`.
+The low input is the ordered pair `(x,y)` in `{0,...,q-1}^2`. Apply the shear
+
+```text
+(x,y) -> (x+c*y,y).
+x' = the canonical residue of x+c*y modulo q.
+C(x,y) = (x+c*y-x')/q.
+```
+
+Rational residues use the inverse of `h`. The exact rational `C` has denominator
+dividing `h`. This is the elementary instance of the carry contract in Ali
+Romman's [PR #5841](https://github.com/CrocSwap/integer-mult-bounds/pull/5841).
+That package counts potential final correction sites and explicitly permits
+additional zero corrections on particular low rows. Its source binding and
+whole-word fusion are predecessor results, not conclusions of this package.
+
+Write `A=|a|`, `H=max(A,h)` and `m=floor((q-1)/H)`. The exact number of zero
+carries is
+
+```text
+Z(a,h,q) = (m+1)*q - A*m*(m+1)/2.
+```
+
+Consequently exactly `q^2-Z` low pairs have a nonzero exact carry. Both signs
+of the coefficient have the same count. No primality assumption on `q` is
+needed for this scalar result.
+
+## Counting proof
+
+Suppose first that `a>0`. The equation `C=0` says `x'=x+a*y/h` as a rational
+equality. In particular `h` divides `a*y`, and reducedness implies `y=h*t`.
+Conversely, for such a `y` the exact carry is zero precisely when
+
+```text
+0 <= t <= floor((q-1)/h),
+0 <= x <= q-1-a*t.
+```
+
+There are `q-a*t` choices of `x` when `a*t<=q-1`, and none otherwise. Thus
+the permitted values of `t` are exactly `0,...,m`. Summing the arithmetic
+progression gives the displayed formula.
+
+For `a<0`, write `A=-a`. The same integrality condition gives `y=h*t`, and
+the no-wrap interval is `A*t<=x<=q-1`. It again has `q-A*t` entries. This
+proves the sign symmetry and the entire formula.
+
+## Exact carries versus high-digit translations
+
+For width `w>=2`, put `M=q^(w-1)`. The actual high-digit correction is the
+residue of `C` modulo `M`, rather than the rational number `C` itself.
+Writing arbitrary full inputs as `x+q*hx` and `y+q*hy`, the high output is
+
+```text
+hx + c*hy + C(x,y) modulo M.
+```
+
+These two notions of a zero correction agree whenever `q>=A+h`. Indeed
+
+```text
+h*C = (h*(x-x') + a*y)/q
+```
+
+is an integer, and `|h*C| < A+h <= q <= M`. Since `h` is a unit modulo `M`,
+the residue of `C` vanishes exactly when `M` divides `h*C`. In that strict
+interval it can do so only when `C=0`. Under this sufficient radix bound,
+`q^2-Z` therefore counts nonidentity high translations at every width `w>=2`.
+The proof does not assert that this sufficient bound is necessary.
+
+The distinction matters outside that bound. For `q=3`, `w=2`, `c=4`, and
+`(x,y)=(1,2)`, one has `x'=0` and exact `C=3`, but its high residue modulo
+three is zero. At width one there is no nontrivial high ring at all.
+
+## Conditioning on an invertible low matrix
+
+Let now `q` be prime and `n>=2`. Choose a matrix uniformly from `GL_n(F_q)`
+and take two specified distinct coordinates in one specified row. Let
+
+```text
+B_n(q) = product over j=1,...,n-1 of (q^n-q^j).
+```
+
+Every nonzero row has exactly `B_n(q)` invertible completions. To see this,
+successively choose each remaining row outside the span of its predecessors.
+The numbers of choices are `q^n-q`, `q^n-q^2`, and so on.
+
+For every nonzero coordinate pair `(x,y)`, exactly `q^(n-2)` nonzero rows
+project onto it. The pair `(0,0)` has one fewer such row. It always has zero
+carry, so it contributes nothing to the nonzero-carry count. It follows that
+the exact number of invertible matrices with nonzero exact carry is
+
+```text
+(q^2-Z(a,h,q)) * q^(n-2) * B_n(q),
+```
+
+and their proportion is
+
+```text
+(q^2-Z(a,h,q)) * q^(n-2) / (q^n-1).
+```
+
+Under `q>=A+h` these also count nonidentity high translations for every
+`w>=2`. The matrix must be uniform over the complete stated general linear
+group. This law is not asserted for an arbitrary subset of admissible matrices,
+correlated invocations, composite-radix general linear groups, or a selected
+construction's actual execution distribution.
+
+## Smaller coefficients can have more carry events
+
+For fixed `a,h`, the scalar nonzero-carry proportion tends, as the radix grows
+through integers coprime to `h`, to
+
+```text
+1 - 1/H + A/(2*H^2),  H=max(A,h).
+```
+
+This follows by dividing the exact formula by `q^2` and using `m/q -> 1/H`.
+In particular coefficients `1`, `1/2`, and `1/4` have limiting proportions
+`1/2`, `5/8`, and `25/32`, respectively. More generally `c=1/2^s` has limit
+
+```text
+1 - 2^(-s) + 2^(-2*s-1),
+```
+
+which increases strictly to one. For successive denominators `h` and `2h`,
+the increase is `(4*h-3)/(8*h^2)>0`. This is a scoped obstruction to using
+coefficient magnitude alone as a predictor of carry sparsity. It is not a
+lower bound on a complete physical circuit's cost.
+
+## Scope and credit
+
+This is a scoped written counting proof with finite corroboration. It adds an
+exact per-input law to the cited potential-site contract. It neither audits
+that source nor certifies its complete G20 word. Exact uniform frequencies
+do not improve a worst-case recursive invoice without a legal skipping or
+amortization argument. Computing the predicate, retaining low data, preparation,
+cache erasure, physical movement, restoration and full supplier admission remain
+separate obligations. All selected framework assumptions remain open at their
+previous status. No new kappa or complete multiplication theorem is claimed.
+
+Credit Ali Romman #5841 for the question's source and fused carry contract,
+Nick Petalas's earlier elementary carry identity, ToikY #5801/#5805,
+Tekalign #3343/#4000, JoyboyBrian and the retained G20/native/ROW lineage.
+Arithmetic-progression counting and uniform general-linear-group row counting
+are classical. The new formula, consequences and verifier were produced by
+Nick Petalas. Apache-2.0. Independent human and formal proof-kernel review are
+unclaimed.

research/rational-shear-carry-density/README.md

@@ -0,0 +1,109 @@
+# Exact nonzero-carry frequency for rational shears
+
+For a nonzero reduced coefficient `a/h`, canonical low digits `x,y` in
+`{0,...,q-1}`, and `gcd(h,q)=1`, the exact zero-carry count is
+
+```text
+A = |a|, H = max(A,h), m = floor((q-1)/H)
+Z = (m+1)q - A*m*(m+1)/2
+nonzero exact carries = q^2 - Z
+```
+
+This is a scoped written proof with finite corroboration. Both coefficient
+signs have the same count. For `q>=|a|+h` and every width `w>=2`, the formula
+also counts nonidentity high-digit translations. Smaller radices can have
+nonzero exact carries whose high residues vanish; an explicit example and
+the separate prime-field `GL_n` law are in [PROOF.md](PROOF.md).
+
+The limiting nonzero proportions for coefficients `1`, `1/2` and `1/4` are
+`1/2`, `5/8` and `25/32`. For `1/2^s` the limit increases strictly to one
+as `s` grows. Smaller coefficient magnitude alone therefore does not establish
+sparser carries. This is a new per-input count, building on Ali Romman's
+[#5841](https://github.com/CrocSwap/integer-mult-bounds/pull/5841) carry
+contract and its explicit allowance for zero corrections at particular inputs.
+No predecessor verifier is imported or replayed.
+
+The helper-contract card is changed to this local carry-sparsity question.
+Exact uniform frequencies need a priced skipping or amortization argument
+before they can reduce a worst-case supplier invoice. This package does not
+supply that program, a complete G20 route, a physical caller, a new kappa or a
+complete multiplication theorem. The selected frontier and its five framework
+assumptions retain their previous status.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and only its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -X dev -W error -B research/rational-shear-carry-density/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rational-shear-carry-density/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rational-shear-carry-density
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rational-shear-carry-density --check-source-history
+```
+
+An equivalent CPython 3.12 path works. The direct verifier prints
+`PASS_RATIONAL_SHEAR_CARRY_DENSITY` inside a generated JSON receipt bound to
+every package file's SHA256. It never writes a receipt or bytecode cache.
+Both registered commands run the same coverage under normal and optimized
+Python. Explicit exceptions enforce acceptance in both modes.
+
+The finite checker enumerates 3,848 scalar fixtures and all 1,353,470 low
+pairs in those domains. It compares 168,044 full-width low-pair cases with a
+separate direct modular product, including small-radix cancellation, and
+checks 14,176 arbitrary-high inputs. The matrix oracle enumerates all 23,318
+matrices in its six domains, including 13,950 invertible matrices, and checks
+104 coefficient/domain combinations. The domains are `GL_2` at primes
+2, 3, 5 and 7, and `GL_3` at primes 2 and 3. Five exact limiting fixtures,
+sixteen dyadic monotonicity cases, thirteen invalid-input rejections and three
+semantic separating controls are also checked. These finite domains corroborate
+the written proof; they do not replace its universal quantifiers.
+
+[SOURCES.json](SOURCES.json) pins the historical catalogue and selected record
+in reachable base history. It also records the original head, Git blobs and
+SHA256 hashes for two unchanged source documents retained under `inputs/`.
+Those documents preserve attribution and the precise question boundary. No
+pending predecessor Git object or external package is needed for replay.
+[TASK.json](TASK.json) records scope, environment and structured next questions.
+
+## Implementation limits
+
+The public count evaluator rejects coefficient components above `2^16` and radices
+above `2^127-1`. These are checker bounds, not theorem restrictions. The
+enumeration domains are fixed in the source. There is no recursion, subprocess,
+network access, mutable global state or search that stops on a hoped-for answer.
+Every function is shorter than sixty lines. All arithmetic is exact.
+
+Power-of-Ten rule 3 requires a managed-runtime deviation for Python's integer,
+tuple and dictionary allocations. Only bounded finite menus and matrix sizes
+are kept live; matrix enumeration streams its candidates, retaining at most
+`q^2` counters with `q<=7`. Scalar enumeration keeps constant-size state, and
+the evaluator's public numeric limits bound integer sizes. The fixed package
+has eight files; its receipt rejects an inventory exceeding sixteen. A native
+fixed-capacity implementation is the follow-up if the checker becomes a
+runtime component. Warning-strict normal and optimized replay, AST parsing and
+compilation are the available diagnostics; no repository-wide diagnostic
+configuration is changed.
+
+No selected cold replay, source native/tape suite, formal proof-kernel run,
+physical skipping implementation or complete supplier admission is performed.
+Independent human review is unclaimed.
+
+## Open next questions
+
+1. Can a legal zero-carry branch beat unconditional translation after its
+   predicate, retained cache and erasure are paid? Start with one released
+   quarter-shear leaf and the literal tape interface. The missing branch
+   implementation and amortization contract prevent a supplier-cost claim.
+2. What is the joint zero-carry count for one complete fused route? Begin with
+   one exact two-coordinate restriction in #5841. Correlated coordinates and
+   multiple coefficients prevent multiplication of these one-shear marginals.
+
+## Credit
+
+The new proof, count and verifier were produced by Nick Petalas. Credit Ali
+Romman #5841 for the fused carry contract and per-input boundary, Nick Petalas's
+earlier elementary carry identity, ToikY #5801/#5805, Tekalign #3343/#4000,
+JoyboyBrian and all retained G20/native/ROW contributors. Their unchanged source
+notices remain in `inputs/`. Arithmetic progressions and uniform general linear
+group row counting are classical. Apache-2.0. Independent human and formal
+proof-kernel review are unclaimed.

research/rational-shear-carry-density/SOURCES.json

@@ -0,0 +1,40 @@
+{
+  "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"
+    }
+  ],
+  "retained_predecessors": [
+    {
+      "repository": "CrocSwap/integer-mult-bounds",
+      "pr": 5841,
+      "head": "58a032ffafc2c5d08b8f53c2e98657b75c48379d",
+      "original_path": "research/g20-fused-qadic-carries/PROOF.md",
+      "retained_path": "inputs/PR5841-PROOF.md",
+      "git_blob": "30170cf866c4e7be4fa20544087bb0b3f056af1f",
+      "sha256": "09790822ea0cb8fd2bc6db2ba9d5c1c616dc162486083bca79026be61d7f5757",
+      "usage": "Attribution and exact statement of the per-input zero-carry boundary. No predecessor code is executed; the new proof is self-contained."
+    },
+    {
+      "repository": "CrocSwap/integer-mult-bounds",
+      "pr": 5841,
+      "head": "58a032ffafc2c5d08b8f53c2e98657b75c48379d",
+      "original_path": "research/g20-fused-qadic-carries/README.md",
+      "retained_path": "inputs/PR5841-README.md",
+      "git_blob": "063b52f21ac661884540f10c5894ac30151a7766",
+      "sha256": "b957a53d9f9a1e6ba3cbd9151a2e5fea071cecbcc6cf0d00f6efa520ccc62f83",
+      "usage": "Attribution and exact statement of the per-input zero-carry boundary. No predecessor code is executed; the new proof is self-contained."
+    }
+  ]
+}