diff --git a/research/rational-shear-carry-density/PROOF.md b/research/rational-shear-carry-density/PROOF.md new file mode 100644 index 0000000000..00cc960817 --- /dev/null +++ b/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. diff --git a/research/rational-shear-carry-density/README.md b/research/rational-shear-carry-density/README.md new file mode 100644 index 0000000000..11490731f6 --- /dev/null +++ b/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. diff --git a/research/rational-shear-carry-density/SOURCES.json b/research/rational-shear-carry-density/SOURCES.json new file mode 100644 index 0000000000..23c38508db --- /dev/null +++ b/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." + } + ] +} diff --git a/research/rational-shear-carry-density/TASK.json b/research/rational-shear-carry-density/TASK.json new file mode 100644 index 0000000000..6c483063db --- /dev/null +++ b/research/rational-shear-carry-density/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact number of canonical low pairs with nonzero carry for a reduced rational shear; distinguish high-residue cancellation and give the prime-field invertible-matrix law.", + "scope_change_reason": "The selected helper-contract question is narrowed away from a changed productive target. PR5841 explicitly leaves per-input zero carries outside its potential correction-site count. This is a self-contained carry-sparsity side result, not a complete physical caller.", + "bottleneck_link": "Low-cache preparation and coefficient-specific translations remain paid obligations. Exact sparsity tests whether smaller coefficients can justify fewer carry events; no worst-case invoice saving follows without a priced skipping program.", + "budget_minutes": 60, + "stop_rule": "Ship the first closed-form count once literal scalar, full-width and complete small GL enumerations pass. Do not extend to fused words or physical execution.", + "outcome": "completed", + "evidence": "PROOF.md supplies the written all-radix counting proof; verify.py supplies finite literal modular and complete small GL corroboration and a generated hash-bound stdout receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a physically legal carry-skipping program beat unconditional translation after paying for the predicate and low-cache lifecycle?", + "why_it_matters": "The exact frequency does not itself lower a worst-case supplier invoice.", + "first_step": "Take one released quarter-shear leaf, price a zero-carry branch and its cache preparation/erasure on the literal tape interface.", + "blocked_by": "No complete branch implementation or compatible amortization contract is supplied here." + }, + { + "question": "What is the joint zero-carry count for one complete fused G20 route?", + "why_it_matters": "Single-shear marginals cannot price correlated fused corrections.", + "first_step": "Choose one exact PR5841 two-coordinate restriction and count its complete simultaneous carry-zero equations.", + "blocked_by": "The full route has multiple coefficients and correlated low coordinates; this theorem treats one shear only." + } + ], + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "system": "Darwin", + "machine": "arm64", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216892", + "upstream_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "checked_at_utc": "2026-10-27T12:37:00Z" + } +} diff --git a/research/rational-shear-carry-density/VERIFY.json b/research/rational-shear-carry-density/VERIFY.json new file mode 100644 index 0000000000..68ca8c902e --- /dev/null +++ b/research/rational-shear-carry-density/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-X", + "dev", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact scalar carry counts, independent full-width translations, complete small GL matrix enumeration, arbitrary-high identity, asymptotic fixtures and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same finite coverage with optimization and isolated imports; all acceptance checks use explicit exceptions." + } + ] +} diff --git a/research/rational-shear-carry-density/inputs/PR5841-PROOF.md b/research/rational-shear-carry-density/inputs/PR5841-PROOF.md new file mode 100644 index 0000000000..30170cf866 --- /dev/null +++ b/research/rational-shear-carry-density/inputs/PR5841-PROOF.md @@ -0,0 +1,106 @@ +# Whole-word carry identity and complete G20 binding + +Let q>1 be coprime to12, w>=1, and M=q^(w-1). Let S be one exact rational +RIGHT product from either released PR5820 catalogue. Both S and its inverse +have dyadic coefficients and determinant a signed power of two. Thus S is +invertible modulo q and modulo q^w. The stronger source modulus guard is kept. +The argument also applies to any rational matrix whose denominators and +determinant are units modulo q, with the corresponding denominator bounds. + +Write a row uniquely as x=l+q*h, with canonical low digits0<=l_i (l', h*S+C_S(l) mod M). + +Indeed l*S=l'+q*C_S(l), so rejoining the displayed output gives x*S modulo +q^w. At w=1 the high ring has one value and the same formula applies. This +integer identity proves the all-width assertion; finite checks are evidence +for the emitted source binding and implementations. + +## Composition and final correction + +For a second admissible matrix T, with l'=l*S mod q, direct substitution gives + + C_(S*T)(l) = C_S(l)*T + C_T(l'). + +The final canonical low digit is the same on both sides. Thus all carries of +a complete elementary word can be transported through its remaining linear +suffix and added once at the end. Execute the original high-digit linear word +without intermediate carries, then add C_S(l). Compute that vector from the +saved entry low row and commit the final low row l'. This is an explicit +algorithm; it does not use a table of q^8 low rows or depend on w. + +If a column of S is a positive coordinate unit, its carry is identically zero +and needs no translation. The verifier omits exactly those columns. Every +other column has one possible final correction site. The count is an upper +bound: a particular low row can have additional zero carries. No minimum over +all physical circuits, correlated translations or alternative low sections is +claimed. The source linear words and all their ADD/SCALE charges remain. + +The two complete source catalogues contain444 directed routes. Every port and +direction occurs34 times in the actual7,548-marker stream. Their per-marker +potential correction counts sum to28,492 for either basis. The factor-by-factor +construction has74,460 sites for the tree and53,448 for the shear basis. After +N=127f lifting these count differences are5,837,936f^2 and3,169,412f^2 named +correction calls. Each correction has a positive coefficient-specific physical +tariff. Changing coefficients or adding cache work can change the total cost; +these counts alone do not prove a physical saving. + +## Inverse, high fibers and fields + +Put T=S^-1. The composition law gives + + C_T(l') = -C_S(l)*T. + +The inverse must read the committed low row l', not a stale entry cache. It +then restores both low and high digits exactly for every input. For each fixed +low row, h -> h*S+C_S(l) is a bijection of all M^8 high rows. For an N by N +cover and a fixed low matrix, the tensor embedding is a bijection of all +M^(N^2) high completions. If the low matrix is invertible, all its high lifts +are invertible: a matrix over Z/q^w is invertible exactly when its determinant +is a unit modulo q. This also holds for the tested composite radix. No fresh +stock values are filtered out. + +The18 actual stages have nonconsecutive numeric labels. Give the k-th source +stage, k=0..17, axes0 and1+7k through7+7k, as in the retained cover convention. +For row r and lane t, addresses are r*N+axis*f+t, where N=127f. They are distinct. +Each row has f disjoint active eight-entry blocks. The map is the identity on +all other columns. It reads no ancestor, role, head/data or unused-descendant +field, so it is the identity on those product factors for arbitrary values. +The chosen compatible axis convention is not a proved physical head layout. + +ENTRY uses the inverse word and RETURN the forward word under the retained +single-cover convention h=gS. The checker rebuilds every marker index, stage, +owner bank, port and phase from the frozen call intervals. This binds the new +carry program to the exact source incidence. The physical reflected pairing +and native port action remain the source's proved contract; no second cover +or factor-of-two bill is introduced here. + +## Verification and remaining obligations + +The dense oracle multiplies full-width residues by S without splitting digits +or using a carry routine. The separate elementary interpreter uses integer +carry numerators at each factor. Both agree with the fused interpreter over +all emitted routes. A noncommuting next matrix tests the general cocycle, +not only inverse round trips. Full cover fixtures check source stage ordinals, +all rows and lanes, inactive coordinates and exact inverse restoration. +Controls reject missing carry, stale low type, wrong order, an omitted nonzero +correction, wrong owner and an ineligible modulus. + +The algorithm is an exact row-index implementation. Low cache, type commit, +translation, preparation and cache erasure are not assumed free. Literal ROW +heads, tape execution, padding, borrowed-child return, physical coefficient +tariffs and the complete current caller binding remain separate obligations. +No selected framework assumption is discharged and no kappa change is claimed. diff --git a/research/rational-shear-carry-density/inputs/PR5841-README.md b/research/rational-shear-carry-density/inputs/PR5841-README.md new file mode 100644 index 0000000000..063b52f21a --- /dev/null +++ b/research/rational-shear-carry-density/inputs/PR5841-README.md @@ -0,0 +1,59 @@ +# Complete G20 routes with fused q-adic carries + +All 111 sparse port routes now have an exact low/high implementation at every +width, for both directions and both released bases. The construction combines +all elementary carries into one final dyadic translation per affected output +column. For the 7,548 actual source markers, the tree needs at most 28,492 +translation sites instead of 74,460, a reduction of 61.7%. The scale-free basis +needs 28,492 instead of 53,448, a reduction of 46.7%. The linear words stay fixed. +These are carry-site counts. Their physical tariffs need not be equal, and this +is not a runtime or full supplier saving. + +The proof gives a width-independent carry, its exact composition law, its +inverse, dyadic denominator and height bounds, and complete high-fiber +preservation. It includes canonical low-type commit. The stage-to-axis map uses +the source stage ordinal, not its numeric stage label. A full N=127f cover uses +127f^2 independent eight-entry row/lane blocks. Other columns, ancestor fields, +roles and unused descendant stock stay fixed. See [PROOF.md](PROOF.md). + +The checker authenticates PR5820 head +`04b5db84b4b02bdc17e1c6287dfcf8b9c04199d4`, reconstructs each rational product, +checks the same line/complement interface and exact marker owners, and compares +22,200 complete full-width cases with a separate dense modular oracle and an +elementary carry interpreter. It checks 2,220 noncommuting rational cocycles, +3,100 exhaustive two-coordinate inputs, complete first/last-stage cover +fixtures, inverse restoration and six semantic rejection controls. The tested +moduli include a composite and an89-bit integer; the written identity has no +width cap. Every exact count and digest is in RESULT.json. + +Run `python3 -B scripts/research_package.py --package research/g20-fused-qadic-carries`. +Python3.12 and the standard library suffice. The direct command is +`python3 -B research/g20-fused-qadic-carries/verify.py`. + +Physical head placement, low-cache preparation and erasure, coefficient-specific +ROW/tape tariffs, padding, borrowed return, final compiler and compatible outer +admission remain open. The source native interface and all five framework +assumptions retain their status. No new kappa or selected-frontier change follows. +This package does not implement PR5836's physical unit-scale tariff or repeat +the current controller optimization. + +## Open next questions + +Bind one complete fused eight-axis route to the retained physical affine-stream +kernels, including low-cache commit and erasure. Compare the total tariff with +the unfused route; fewer named translations alone do not establish that result. +Then install the route in the exact current caller with its actual head map. + +Credit PR5820 for the two bases, ToikY PR5801/5805 for words and marker contracts, +Nick Petalas's selected-bit-qadic-route for the elementary carry identity, +Tekalign PR3343/4000 for physical carry and dyadic affine stream work, +JoyboyBrian and all retained G20/native/ROW authors in inputs/NOTICE. +The new contribution is the complete G20 binding and whole-word carry fusion. +Ali Romman with substantial OpenAI Codex assistance; no subagents. Apache-2.0. +Independent scientific acceptance remains open. + +The source manifest pins replay inputs to copies in this publication history. +Its `retained_predecessors` records keep each original head, path, blob and +SHA256, plus its exact retained file or archive member. Each source was checked +byte-for-byte before this rebind. This removes an unavailable side-commit +dependency from clean CI; no source bytes or scientific checks are changed. diff --git a/research/rational-shear-carry-density/verify.py b/research/rational-shear-carry-density/verify.py new file mode 100644 index 0000000000..86706b10cf --- /dev/null +++ b/research/rational-shear-carry-density/verify.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the rational-shear carry-count theorem.""" + +from fractions import Fraction +from hashlib import sha1, sha256 +from itertools import product +import json +from math import gcd, prod +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +MAX_RADIX = (1 << 127) - 1 +MAX_COMPONENT = 1 << 16 + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def validate(a, h, q): + if any(type(value) is not int for value in (a, h, q)): + raise ValueError("coefficient components and radix must be integers") + if not 0 < abs(a) <= MAX_COMPONENT or not 1 <= h <= MAX_COMPONENT: + raise ValueError("nonzero reduced coefficient exceeds checker bounds") + if not 2 <= q <= MAX_RADIX: + raise ValueError("radix exceeds checker bounds") + if gcd(abs(a), h) != 1 or gcd(h, q) != 1: + raise ValueError("coefficient must be reduced and denominator a radix unit") + + +def zero_count(a, h, q): + """Return the exact count; the written theorem has no checker-size cap.""" + validate(a, h, q) + magnitude = abs(a) + last = (q - 1) // max(magnitude, h) + result = (last + 1) * q - magnitude * last * (last + 1) // 2 + require(q <= result <= q * q, "zero count is outside its feasible range") + return result + + +def carry_numerator(a, h, q, x, y): + """Return h*C from the literal canonical low modular product.""" + low = (x + a * y * pow(h, -1, q)) % q + numerator = h * (x - low) + a * y + require(numerator % q == 0, "carry numerator must be divisible by the radix") + return numerator // q + + +def limit_density(a, h): + height = max(abs(a), h) + return 1 - Fraction(1, height) + Fraction(abs(a), 2 * height * height) + + +def coefficients(bound): + return tuple((a, h) for h in range(1, bound + 1) + for a in range(-bound, bound + 1) + if a and gcd(abs(a), h) == 1) + + +def check_scalar_counts(): + fixtures = pairs = 0 + for q in range(2, 32): + for a, h in coefficients(12): + if gcd(h, q) != 1: + continue + observed = 0 + for x, y in product(range(q), repeat=2): + observed += carry_numerator(a, h, q, x, y) == 0 + pairs += 1 + require(observed == zero_count(a, h, q), "literal scalar count differs") + require(observed == zero_count(-a, h, q), "sign symmetry differs") + fixtures += 1 + return {"scalar_fixtures": fixtures, "scalar_low_pairs": pairs} + + +def check_high_translations(): + fixtures = pairs = 0 + for q in range(2, 20): + for a, h in coefficients(6): + if gcd(h, q) != 1: + continue + for width in (2, 3): + full_modulus = q ** width + high_modulus = q ** (width - 1) + inverse = pow(h, -1, full_modulus) + observed = 0 + for x, y in product(range(q), repeat=2): + full = ((h * x + a * y) * inverse) % full_modulus + numerator = carry_numerator(a, h, q, x, y) + high = numerator * pow(h, -1, high_modulus) % high_modulus + require(full % q == (x + a * y * pow(h, -1, q)) % q, + "full product has the wrong low digit") + require(full // q == high, "carry fails the full-width oracle") + if q >= abs(a) + h: + require((full < q) == (numerator == 0), + "large-radix exact/residue equivalence differs") + observed += full < q + pairs += 1 + if q >= abs(a) + h: + require(observed == zero_count(a, h, q), "translation count differs") + fixtures += 1 + # The sufficient large-radix premise cannot simply be omitted. + numerator = carry_numerator(4, 1, 3, 1, 2) + require(numerator == 3 and (1 + 4 * 2) % 9 == 0, + "small-radix cancellation control disappeared") + return {"high_fixtures": fixtures, "full_width_low_pairs": pairs, + "small_radix_cancellation_controls": 1} + + +def determinant(entries, n, q): + if n == 2: + return (entries[0] * entries[3] - entries[1] * entries[2]) % q + require(n == 3 and len(entries) == 9, "only finite 2/3-dimensional oracles exist") + a, b, c, d, e, f, g, h, i = entries + return (a * (e * i - f * h) - b * (d * i - f * g) + + c * (d * h - e * g)) % q + + +def check_matrix_counts(): + candidates = invertible = fixtures = 0 + for n, q in ((2, 2), (2, 3), (2, 5), (2, 7), (3, 2), (3, 3)): + menu = tuple((a, h) for a, h in coefficients(4) if gcd(h, q) == 1) + row_counts = [0] * (q * q) + actual_group = 0 + for entries in product(range(q), repeat=n * n): + candidates += 1 + if determinant(entries, n, q) != 0: + row_counts[q * entries[0] + entries[1]] += 1 + actual_group += 1 + invertible += 1 + completions = prod(q ** n - q ** j for j in range(1, n)) + require(actual_group == (q ** n - 1) * completions, "GL size differs") + for a, h in menu: + observed = sum(row_counts[q * x + y] + for x, y in product(range(q), repeat=2) + if carry_numerator(a, h, q, x, y) != 0) + expected = (q * q - zero_count(a, h, q)) * q ** (n - 2) * completions + require(observed == expected, "complete GL carry count differs") + fixtures += 1 + return {"matrix_candidates": candidates, "invertible_matrices": invertible, + "matrix_coefficient_fixtures": fixtures} + + +def check_payload_identity(): + cases = 0 + for q in (3, 5, 7): + for a, h in coefficients(4): + if gcd(h, q) != 1: + continue + for width in (2, 3): + full_modulus, high_modulus = q ** width, q ** (width - 1) + for x, y, hx, hy in product(range(q), range(q), (0, 1), (0, 1)): + low = (x + a * y * pow(h, -1, q)) % q + k = carry_numerator(a, h, q, x, y) + high = (hx + (a * hy + k) * pow(h, -1, high_modulus)) % high_modulus + full = (x + q * hx + a * (y + q * hy) + * pow(h, -1, full_modulus)) % full_modulus + require(low + q * high == full, "arbitrary-high affine identity differs") + cases += 1 + return {"arbitrary_high_cases": cases} + + +def check_limits_and_controls(): + expected = ((1, 1, Fraction(1, 2)), (1, 2, Fraction(5, 8)), + (1, 4, Fraction(25, 32)), (3, 2, Fraction(5, 6)), + (4, 1, Fraction(7, 8))) + for a, h, density in expected: + require(limit_density(a, h) == density, "displayed limiting density differs") + for exponent in range(1, 17): + h = 1 << exponent + require(limit_density(1, h) > limit_density(1, h // 2), + "reciprocal dyadic carries must become more frequent") + invalid = ((0, 1, 5), (2, 4, 5), (1, 0, 5), (1, -2, 5), + (1, 2, 4), (1, 1, 1), (True, 1, 5), (1, True, 5), + (1, 1, False), (1.0, 1, 5), (MAX_COMPONENT + 1, 1, 5), + (1, MAX_COMPONENT + 1, 5), (1, 1, MAX_RADIX + 1)) + for args in invalid: + try: + zero_count(*args) + except ValueError: + continue + raise RuntimeError("invalid coefficient or radix was accepted") + # Named semantic mutations have explicit separating fixtures. + require(zero_count(1, 4, 5) != zero_count(1, 1, 5), "lost denominator control") + require(zero_count(3, 2, 7) != 7 * 7 - zero_count(3, 2, 7), + "zero/nonzero complement control") + gl_probability = Fraction((25 - zero_count(1, 4, 5)), 24) + scalar_probability = Fraction((25 - zero_count(1, 4, 5)), 25) + require(gl_probability != scalar_probability, "GL conditioning control") + return {"limit_fixtures": len(expected), "dyadic_monotonicity_cases": 16, + "invalid_inputs_rejected": len(invalid), "semantic_controls": 3} + + +def source_and_package_hashes(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + for source in sources["retained_predecessors"]: + payload = (PACKAGE / source["retained_path"]).read_bytes() + require(sha256(payload).hexdigest() == source["sha256"], "retained source SHA256 differs") + header = b"blob " + str(len(payload)).encode("ascii") + b"\0" + require(sha1(header + payload).hexdigest() == source["git_blob"], + "retained source Git blob differs") + paths = sorted(path for path in PACKAGE.rglob("*") if path.is_file()) + require(len(paths) <= 16, "unexpected package files or generated leftovers") + return {str(path.relative_to(PACKAGE)): sha256(path.read_bytes()).hexdigest() + for path in paths} + + +def main(): + counts = {} + counts.update(check_scalar_counts()) + counts.update(check_high_translations()) + counts.update(check_matrix_counts()) + counts.update(check_payload_identity()) + counts.update(check_limits_and_controls()) + receipt = {"status": "PASS_RATIONAL_SHEAR_CARRY_DENSITY", + "claim_type": "scoped written proof with finite corroboration", + "counts": counts, "package_sha256": source_and_package_hashes(), + "no_new_kappa": True} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()