Bound once-rounded rational gate temporaries by B+4C+2 bits (no κ)

research/integer-rounded-gate/PROOF.md

@@ -0,0 +1,152 @@
+# A smaller arithmetic width for once-rounded rational gates
+
+This scoped construction and proof were produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let B>=2 and C>=1 be integers. Four signed input grid numerators X_j satisfy
+
+    -2^(B-1) <= X_j < 2^(B-1),  0<=j<4.
+
+A rational row has coefficients p_j/d_j, with integer p_j and d_j such that
+
+    |p_j| < 2^C,  1 <= d_j < 2^C.
+
+The coefficients need not be reduced. There is a constant-word arithmetic
+program that computes
+
+    floor(sum_j (p_j/d_j) X_j + 1/2)
+
+with every signed data-arithmetic temporary fitting
+
+    W = B + 4C + 2 bits.                                      (1)
+
+The program uses shifts, bit tests, addition, subtraction and comparisons.
+Multiplication and division below are implemented by bounded binary loops.
+They are not assumed machine instructions. Four applications to saved inputs
+implement any two-coordinate Gaussian rational matrix gate, rounding each
+real and imaginary output once with ties toward positive infinity.
+
+This is an upper bound, not a minimum-width theorem. It concerns arithmetic
+words after coefficients and input data are supplied. No reversible circuit,
+bit-tape running time, memory layout or coefficient-preparation bound follows.
+
+## Common-denominator accumulation
+
+Set
+
+    D = product_j d_j,
+    N_j = p_j X_j product_(k!=j) d_k,
+    S = sum_j N_j.
+
+Compute D by four successive products starting from one. Compute each N_j
+from p_j X_j and then the three other denominators. Accumulate its exact
+integer value before proceeding to the next term. No product is rounded.
+
+We have
+
+    1 <= D < 2^(4C),
+    |N_j| < 2^(B+4C-1),
+    |sum_(j in J) N_j| < 4 * 2^(B+4C-1) = 2^(W-1)           (2)
+
+for every partial sum occurring in this fixed four-term order. The bound
+uses |X_j|<=2^(B-1), including the most negative B-bit input. Strictness
+comes from the four coefficient numerator/denominator factors, each strictly
+below 2^C. Signs and cancellation are unrestricted.
+
+Each nonzero partial product has magnitude at most the corresponding full
+product: every remaining denominator is at least one. A zero numerator
+remains zero. All these intermediate values fit (1), by (2). D and its
+partial products fit as well. The exact rational row value is S/D.
+
+For signed multiplication, retain the result sign and use unsigned
+magnitudes. Scan the multiplier's binary digits from low to high, adding
+the shifted multiplicand when a digit is one. Every shifted multiplicand
+and every partial sum is at most the full magnitude product. Hence the
+same word bound applies to the shift/add implementation, including its
+positive magnitude words. None of these constructed products is the most
+negative W-bit integer, so taking its absolute value is safe.
+
+## Division and signed ties
+
+Put t=|S|. Binary long division scans exactly W-1 positions of t, from
+most significant to least significant. Maintain a quotient prefix q and
+remainder r. At each position with digit b, replace
+
+    r by 2r+b,
+    q by 2q,
+    if r>=D, subtract D from r and add one to q.
+
+The ordinary prefix-division induction proves that the final pair satisfies
+t=qD+r and 0<=r<D. Before conditional subtraction, the remainder is below
+2D, which is below 2^(4C+1). Since B>=2, this is below 2^(W-1).
+Each quotient prefix is at most the final quotient, which is at most t.
+The shifted quotient prefix before its next digit is no larger than the
+next completed quotient prefix. Thus every quotient and remainder word
+fits (1). The Python helper enforces the sufficient additional contract
+D<2^(W-2), which holds here by the stronger D<2^(4C).
+
+The final rounded integer is
+
+    q + [2r>=D],     if S>=0,
+    -q - [2r>D],     if S<0.                               (3)
+
+For S>=0, this is floor(q+r/D+1/2). For S<0, it is
+floor(-q-r/D+1/2). The strict inequality in the negative branch is
+essential: -1/2 rounds to zero. The positive halfway value 1/2 rounds to
+one. The word 2r is below 2D, so its comparison is also safe.
+
+If D=1, r=0 and rounding changes nothing. If D>=2 and t>=1, the rounded
+result's magnitude is at most q+1<=t. At t=0 it is zero. Therefore the
+final result also fits W signed bits. Equations (2) and (3), rather than
+finite extrapolation, prove the all-B, all-C construction.
+
+## Complex gates, input snapshots and the cited allowance
+
+For a complex row a_0 z_0+a_1 z_1, expand its real and imaginary parts
+using the four real input coordinates. Each real row has exactly four
+rational coefficients, with signs but no increased component height.
+If the inputs are 2^-F X_j, multiplying a rounded output by 2^F gives
+exactly the integer expression above. The arithmetic bound depends on
+B=F+I, not separately on F. The input grid cancels before arithmetic.
+
+Save all four inputs, compute all four output integers, then overwrite
+the four stored coordinates. This gives the same saved-input,
+exact-local-sum, once-per-output rounding contract as Jose Manuel's
+`rational-unitary-fft/exact.py:apply`. Armin Pourshafeie's PR5240 asks for
+such a concrete arithmetic implementation. Its layer and stored-state
+theorems are cited premises, not re-proved or audited here.
+
+The same source's `engine.py:certificate` and FULL-PROOF.md use the
+conservative temporary allowance
+
+    2F + 8C + 2I + 32 = 2B + 8C + 32.
+
+The new arithmetic construction uses
+
+    B + 4C + 2 = (2B + 8C + 32)/2 - 14.                     (4)
+
+This reduces a sufficient maximum arithmetic-word width. It does not
+establish a reduction in total live bits, elapsed time or a complete
+caller's allocation. Output data still need that caller's independent
+amplitude bound before they can be stored back in B bits. The kernel
+permits W-bit outputs and makes no unconditional B-bit output claim.
+
+## One source-produced butterfly
+
+The verifier calls the retained `Phases(4, source)` and
+`Builder.butterfly` with the exact phase i. They produce
+
+    [ 13575/19193,   13568 i/19193 ]
+    [ 13568/19193,  -13575 i/19193 ].
+
+The maximum component height is C=15. For B=18, the new bound is 80 bits.
+Evaluating the cited allowance at these same parameters gives 188 bits.
+This comparison does not assert that a complete source caller selected
+C=15 or allocated an 188-bit word. It is a same-parameter comparison of
+two sufficient formulas. Actual coefficient production is used to supply
+this finite fixture; its approximation theorem is not an audit target.
+
+The independent Fraction oracle, source executor comparisons, large-height
+fixtures and controls corroborate the implementation. They do not replace
+the proof or establish any physical supplier or multiplication theorem.

research/integer-rounded-gate/README.md

@@ -0,0 +1,131 @@
+# Once-rounded rational gates with smaller arithmetic words
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped arithmetic construction and written proof with exact
+finite corroboration. A two-coordinate Gaussian rational gate can compute
+each output with one final nearest rounding, using signed arithmetic words
+of width B+4C+2. Here B is the signed input-numerator width, and C bounds
+the bit length of every coefficient component's numerator magnitude and
+positive denominator. B>=2 and C>=1; the input fractional grid is arbitrary.
+
+The cited rational FFT/Full allowance is 2B+8C+32. The new sufficient width
+is half that allowance minus fourteen bits. [PROOF.md](PROOF.md) proves the
+all-width bound by four-term common-denominator accumulation and bounded
+binary multiplication/division. [kernel.py](kernel.py) implements it with
+integer shifts, tests, additions, subtraction and comparisons. It uses no
+machine multiplication/division instruction or intermediate rounding.
+All four real inputs are saved before output writes.
+
+This answers the arithmetic question left open by Armin Pourshafeie in
+[PR5240](https://github.com/CrocSwap/integer-mult-bounds/pull/5240).
+The result is a new implementation and resource bound, not an audit of the
+predecessor's rounded-layer theorem. No new kappa or selected-frontier
+change is claimed. The bound is sufficient, not proved minimal.
+
+## Evidence and reproduction
+
+The exact finite checks cover 50,625 four-term rows, 3,600 two-term rows,
+31,744 binary divisions, 50 large-height rows and 768 complete complex-gate
+cases. Eight semantic checks distinguish signed ties, product rounding and
+input overwrite. Seventeen invalid-domain/overflow requests reject.
+The largest tested data/coefficient widths are 2048 and 256 bits.
+The word observer checks arithmetic intermediates at each operation.
+
+The retained phase factory at precision four supplies an actual butterfly
+with component height fifteen. For B=18, our construction uses 80-bit
+temporaries; the cited formula evaluated at those same parameters gives
+188 bits. This does not assert a particular full caller allocated 188 bits.
+The verifier compares all four rounded output components with the retained
+saved-input executor, on three grids and all 256 stated input combinations.
+
+From the repository root, standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/integer-rounded-gate/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/integer-rounded-gate/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/integer-rounded-gate
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/integer-rounded-gate --check-source-history --check-modes
+```
+
+Other machines can substitute their CPython 3.12 path. Both registered
+commands have a 120-second cap. The direct marker is
+`PASS_INTEGER_ROUNDED_GATE`. Its generated stdout receipt binds every
+package file by SHA256. Verification writes no package files. No receipt
+is handwritten or committed. Source pins and the complete originating
+card are in [SOURCES.json](SOURCES.json) and [TASK.json](TASK.json).
+
+## Scope and credit
+
+The theorem concerns arithmetic data words, given supplied coefficients.
+The executable accepts 2<=B<=2048 and 1<=C<=256. Its word observer uses
+host arithmetic to detect overflow; it is not a physical machine emitter.
+Output values fit W=B+4C+2 bits. Returning them to B-bit data storage still
+requires the caller's separate amplitude contract. No total-live-storage,
+runtime or bit-tape improvement is claimed.
+
+Coefficient preparation, its local temporaries, reversible cleanup, actual
+instruction encoding, tape movement, all-size compiler funding and supplier
+admission remain open. All five selected framework assumptions remain.
+No selected scientific replay, native/Lean/Docker build, independent human
+review or proof-kernel acceptance is claimed.
+
+Credit Armin Pourshafeie / apoursh for PR5240's explicit arithmetic seam;
+Jose Manuel / jmbarrancoml for the rational executor, phase producer and
+coefficient/temporary contracts; Vlado Vojdanovski for the schedule;
+Chafik Boukhalfa for phases; Brian / JoyboyBrian and James Reed for the
+retained cut/allocator work; Cinna Davis and the numerical/compiler lineage.
+Common-denominator arithmetic, long multiplication/division and nearest
+rounding are classical. Nick Petalas's PR5940 concerns conditioned operator
+interpolation; that theorem and its follow-up question are not extended.
+Predecessor files and their credit lines remain unchanged.
+
+Base is canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a,
+priority revision eight, selected PR6030. The source-binding baseline passed.
+The supplier-boundary-audit card explicitly changes to this constructive
+arithmetic side result, because a missing local kernel separates stored-state
+bounds from an implementation. This does not change a supplier family or
+admit a new one. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361639)
+reserves the same scope.
+
+Live claims, local reservations, open/account PRs, main formula/object
+searches, merged searches and the cached card report were checked. The
+cache covered 370 open PRs and 6,284 Discussion records, with complete
+remote pagination. Its sparse local corpus covered 115 of 8,917 notes;
+relevant packages were materialized and main README searches supplemented
+it. Arbitrary historical diffs and unpublished work remain coverage limits.
+
+## Open next questions
+
+Bind this kernel to one complete Full allocation and charge its exact live
+word count, source snapshots, output staging, bit operations, cleanup and
+tape movement. Start from one emitted two-wire call and its proved input
+and output amplitude bounds. A physical arithmetic/ownership contract and
+the complete caller invoice remain missing. The present maximum word width
+does not settle those costs. No further optimization is reserved.
+
+## Code constraints
+
+Foundational Thinking fixes grid numerators and coefficient pairs before
+arithmetic. Build the Lever supplies the retained kernel and independent
+Fraction oracle. Prove It Works requires actual source-produced gate
+conformance, overflow checks and rejection controls.
+
+All new functions fit sixty lines. There is no recursion or generated code
+in the new kernel. Each multiplication scans at most W-1 multiplier bits;
+each division scans exactly W-1 positions; W<=3074. Gate loops have four
+iterations. Fixed finite verification domains bound all other loops.
+Explicit exceptions retain checks under optimized Python.
+
+Power of Ten rule 3 deviation: CPython allocates integers and containers
+during this bounded reference execution. Fixed B,C limits, four-coordinate
+state and one current row bound the kernel's live collections. A static
+memory backend is needed before a fixed-allocation claim. The width
+observer's capacity and operation counters are verification metadata outside the
+claimed data-word program. Rule 8/9 fixture deviation: the unchanged phase
+factory executes its authenticated interval source; imports and dispatch
+are limited to the five declared inputs and their standard-library imports.
+Its preparation is outside the arithmetic-width theorem. The 120-second
+registered timeout also bounds this finite fixture. Warning-strict normal
+and optimized replay and AST/function-size checks supply local diagnostics;
+no separate type analyzer or linter is claimed.

research/integer-rounded-gate/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "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"
+    },
+    {
+      "path": "research/cubic-cyclic-inverse/vendor/interval_kernel.py",
+      "usage": "input",
+      "git_blob": "1182175a55cb871481de0f56ea9ae56e474705fe",
+      "sha256": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe"
+    },
+    {
+      "path": "research/matching-layer-rounding/README.md",
+      "usage": "input",
+      "git_blob": "99f648abd626c91312ae03dffc41bf307a33176a",
+      "sha256": "ba0225a7af7aa7547d719831f3122c02af09bd56ae32eb45aecccb2e66d8cbdb"
+    },
+    {
+      "path": "research/rational-unitary-fft/FULL-PROOF.md",
+      "usage": "input",
+      "git_blob": "e650f46863115f810e27b403f916dd7f79b37786",
+      "sha256": "acf8c596d91b5efd35a286735d6867ff8afce64354a13f680c2fae3dab824410"
+    },
+    {
+      "path": "research/rational-unitary-fft/engine.py",
+      "usage": "input",
+      "git_blob": "e9f2f2b08dc2bc4c646e47dca92059351ca89384",
+      "sha256": "9e36aee0835e6b1b62997433581f88b5a434ccab8ae43e5c25d1deaaf1ebf653"
+    },
+    {
+      "path": "research/rational-unitary-fft/exact.py",
+      "usage": "input",
+      "git_blob": "aae41e6acfb2e5a4fafdd85727891eb746b57b42",
+      "sha256": "c9b89d7357210af69865690ba12e695366961f8b501a8fab9d0fefe3fb30c479"
+    }
+  ]
+}