[petalas]

Summary

Prove the exact per-input carry count for every nonzero reduced rational shear x <- x + (a/h)y, with canonical low digits in {0,...,q-1} and gcd(h,q)=1.

A = |a|, H = max(A,h), m = floor((q-1)/H)
zero exact carries Z = (m+1)q - A*m*(m+1)/2
nonzero exact carries = q^2-Z

Claim type: scoped written mathematical proof with finite corroboration. Both signs have the same count. At q>=|a|+h, the count also gives nonidentity high translations at every width w>=2. The package gives the separate exact prime-field GL_n conditioning law and a small-radix cancellation counterexample.

The limiting nonzero-carry proportions for coefficients 1, 1/2 and 1/4 are 1/2, 5/8 and 25/32. More generally, the proportion for 1/2^s increases to one. Smaller coefficients alone therefore do not imply fewer carry events.

This extends the per-input zero-correction boundary explicitly left outside Ali Romman's #5841 potential-site count. Credit #5841, Nick Petalas's earlier elementary carry identity, ToikY #5801/#5805, Tekalign #3343/#4000, JoyboyBrian and the retained G20/native/ROW lineage. Their source documents remain unchanged; no predecessor mathematical verifier is imported or replayed. Classical arithmetic-progression and general-linear-group row counting retain their credit. The new contribution was produced by Nick Petalas. Apache-2.0.

Advance CLAIM. Canonical main remains de5ec2e7a6074068452f45b1a191b5c72832df4a, priority revision 8. The helper-contract card is explicitly changed to this carry-sparsity side result.

Evidence

Before, #5841 allows input-dependent zero corrections without counting them. After, the written proof gives the closed form, sign symmetry, exact/high-residue distinction and invertible-matrix law.

Local CPython 3.12.15 on macOS arm64 passes:

• Warning-strict normal and isolated optimized direct checks, timed separately at 0.42s and 0.31s. Both print PASS_RATIONAL_SHEAR_CARRY_DENSITY with generated receipts binding all eight package files.
• 3,848 scalar fixtures and all 1,353,470 low pairs; 1,188 full-width fixtures and 168,044 low pairs against a direct full-modulus oracle; 14,176 arbitrary-high input cases.
• All 23,318 matrices in the six complete small domains, including 13,950 invertible matrices and 104 coefficient/domain combinations. These are GL2 at primes 2,3,5,7 and GL3 at primes 2,3.
• Five limiting fixtures, sixteen dyadic monotonicity cases, thirteen invalid-input rejections, three semantic separating controls and the small-radix cancellation control.
• Both registered VERIFY commands, metadata/provenance validation, AST parsing, in-memory compilation and staged whitespace checks.
• Exact committed bytes and declared-source ancestry at 91900a57a9378586d02cf2c3609873175441d558; official package export/integrity; a read-only, empty-PATH, Git-free optimized export replay; deliberate retained-source corruption rejection.

Exact reproduction from the repository root:

/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. Only the standard library is required. Pending source documents are retained with original head/blob/SHA256 records; replay needs no unmerged predecessor Git objects.

Limitations and unrun obligations

The main count concerns exact rational carries. Its high-translation interpretation has the stated sufficient radix bound and excludes width one. The GL law assumes a uniform complete general linear group over a prime field, not an arbitrary selected admissible subset or execution distribution. One-shear marginals do not determine correlated fused-route counts.

No physical predicate, low-cache preparation/erasure, carry-skipping program, amortization contract, total tape bill or actual G20 caller distribution is supplied. Uniform frequencies do not by themselves reduce a worst-case recursive invoice. Source native/tape suites, the selected cold replay and a formal proof-kernel run are unrun. All five framework assumptions retain their status. No new kappa, selected-frontier change, supplier admission or complete multiplication theorem is claimed. Independent human and formal proof-kernel review are unclaimed.

Open next questions

1. Can one legal zero-carry branch beat unconditional translation after its predicate and full cache lifecycle are paid? Start with a released quarter-shear leaf and the literal tape interface; the branch and amortization contract are missing.
2. What is the joint zero-carry count for one complete fused route? Start with one exact two-coordinate restriction from Lower all sparse G20 routes with exact whole-word q-adic carries #5841; coordinate correlation prevents multiplying these scalar marginals.

Related open work

• Lower all sparse G20 routes with exact whole-word q-adic carries #5841 supplies fused G20 carry algebra and potential sites; this result counts actual zero/nonzero events for a single elementary shear.
• Complete runtime G20 quarter-carry rotation with tight physical bounds #5849 implements a rotation from a supplied quarter-carry packet; this result does not implement its missing producer or change its physical bounds.
• Complete all G20 rational shear leaves with paid literal coefficient preparation #5846 supplies paid rational-coefficient preparation and shear leaves; the new count supplies no replacement leaf or tariff.
• Complete original-owner execution of the full runtime affine shear #5842 installs affine-shear output in its original owner; this result concerns the correction coefficient before that execution interface.
• Cut G20 port route words by 73% with exact sparse bases #5820 constructs sparse G20 port bases; this theorem neither resynthesizes nor physically realizes its routes.
• Construct dyadic words for all 111 G20 port normalizers #5801 constructs dyadic normalizer words; this theorem counts scalar carry events without changing those words.
• Bind all 7,548 G20 route markers to conditional ROW cover words #5805 binds actual markers to ROW words; this result supplies no cache/carry/commit implementation or physical marker binding.
• Install the shorter G20 word in all 18 physical calls with fresh source records #5834 installs a shorter complete global G20 caller while retaining carry obligations; its endpoint and invoice are not recomputed here.
• Halve G20 boundary work with equal-target bases and a complete physical caller #5840 simplifies G20 boundary words while retaining cache/carry obligations; this result gives no new bank-exchange synthesis or complete caller bill.
• Prove exact retained state for serialized rational-shear carries #5913 counts distinguishable response functions for a serialized rational-shear packet producer; this result counts low input pairs with a nonzero correction, a different quantity.
• Prove exact nearest-even shear history from binary code weight #5912 classifies retained history for nearest-even rounded shears; this theorem uses exact modular arithmetic and computes none of its history costs.

The completion refresh inspected the nine other open account PRs created since the CLAIM: #5909 through #5914 and #5916 through #5918. The same-object entries are #5912 and #5913, already distinguished above. The remaining submissions concern partition fees, batching, sector workspace, cyclic quotients, tensor phase recovery, tree degree and XOR synthesis. None computes the same carry-frequency quantity; no additional computations were run to compare their results.

CI notes

Hosted CI has not certified this package. At commit 91900a57a9378586d02cf2c3609873175441d558, run 40506445146 finished with plan failed; replay skipped.

The only failed step was Onboarding helper tests. All ten failure/error entries are in unchanged tests/test_research_current_assignment.py, ending FAILED (failures=8, errors=2, skipped=22). The two errors are KeyError: 'follow_up_steps' and KeyError: 'catalog_first_step'. The eight assertion failures concern frozen-card/current-command routing (0 != 16), missing current/historical references (ValueError not raised, five entries), and sparse omission lists (two entries).

All ten failure/error headers and the final summary match PR #5913's plan log exactly; both logs were inspected. This confirms the shared onboarding failure on main de5ec2e7a6074068452f45b1a191b5c72832df4a. Maintainers will repair it. No package, shared source, workflow or onboarding test was changed in response.

The package replay was skipped. Hosted replay has not certified the package; only the local checks listed above have run. No hosted scientific pass or package-specific failure is claimed.

Merge danger

Reversible package-only addition. Eight files under research/rational-shear-carry-density/; no shared code, selected record, review ledger, frozen source or upstream changes.