Add division-free dual-pair exchange: 134 to 64 scalar units (no κ)

research/division-free-dual-exchange/PROOF.md

@@ -0,0 +1,190 @@
+# Division-free exchange of a dual pair
+
+This scoped construction and its compiler application were produced by Nick
+Petalas. Elementary block shears, stabilized unimodular completion and
+compute/use/uncompute are classical. No general linear-algebra priority is
+claimed. The contribution is a coefficient-preserving alternative for the
+dyadic helper interface, its explicit scalar tariff and the emitted-program
+improvement below.
+
+## Boundary contract
+
+Let D = Z[1/2], let a be a row in D^n and b a column in D^n with ab = 1.
+There are n data fields x and one spare field z, all at one common linear
+chart. Every incoming value, including z, is arbitrary. No zero initialization,
+erasure, odd inverse or change of chart is available inside the exchange.
+
+The desired basis map on these n+1 fields is
+
+```text
+S(x,z) = ((I-ba)x + bz, ax).
+S = [[I-ba, b], [a, 0]].
+```
+
+The extended pair is (a,0), (b,0), and the pivot is the spare coordinate.
+Then (a,0)S = e_z^T and S e_z = (b,0)^T, exactly the row/column equations
+of Ali Romman's [PR5611](https://github.com/CrocSwap/integer-mult-bounds/pull/5611).
+This changes the resource contract by requiring a spare coordinate. It does
+not replace a no-spare completion and does not assert that the spare exists
+in a particular P104 cut. During S alone, z becomes ax; it is not restored
+at that intermediate boundary.
+
+## Two literal factorizations
+
+Define common-chart block shears and a sign operation by
+
+```text
+U_b(x,z) = (x+bz,z)
+L_a(x,z) = (x,z+ax)
+D(x,z)   = (x,-z).
+```
+
+Operations below are written in chronological order. The first program is
+
+```text
+U_b; L_(-a); U_b; D.
+```
+
+After the middle block, the spare is
+z-a(x+bz) = -ax, using ab=1. After the last upper block and sign, the
+result is ((I-ba)x+bz,ax). The second program is
+
+```text
+D; L_a; U_(-b); L_a.
+```
+
+Its first lower block gives ax-z. Its upper block gives (I-ba)x+bz.
+Its last lower block gives ax-z+a(I-ba)x+abz = ax. Thus both programs
+are S. Every upper block is one ADD per nonzero b_i; every lower block
+is one ADD per nonzero a_i. Within each block the ADDs commute, but blocks
+cannot be reordered freely. Only the sign SCALE is used. Every emitted
+coefficient belongs to {+a_i,-a_i,+b_i,-b_i,-1}; no Euclidean quotient,
+new denominator, native operation, INIT or CLEAR is introduced.
+
+Put s_a=nnz(a), s_b=nnz(b). The two exact gate counts are
+2s_b+s_a+1 and 2s_a+s_b+1. In particular a completion exists with
+min(2s_b+s_a,2s_a+s_b)+1 gates. Selecting the cheaper scalar tariff can
+select a different factorization than selecting the smaller gate count.
+
+Because ab=1, (ba)^2=ba and (I-ba)b=0=a(I-ba). Direct multiplication
+therefore gives S^2=I. S fixes ker(a) and swaps the directions (b,0) and
+(0,1), so its determinant is -1. It uses no additional field beyond the
+stated spare. Its n-dimensional top-left block is singular, with kernel
+exactly Db.
+
+## A sharp block count, within a stated alphabet
+
+Three off-diagonal block shears are necessary for this S, even allowing
+arbitrary invertible block-diagonal operations for free. This statement
+counts entire U and L blocks, not individual ADDs, and is not a lower bound
+for unrestricted scalar circuits.
+
+Move each block-diagonal factor through an adjacent shear by conjugation.
+Conjugation preserves whether the shear is upper or lower. The resulting
+outer block-diagonal factors preserve invertibility of each principal
+block. Two upper shears combine, as do two lower shears. A product UL has
+invertible lower-right block; a product LU has invertible top-left block.
+The same is true of zero or one shear. S has lower-right block zero and
+singular top-left block I-ba. Hence at most two shears cannot realize S.
+The displayed programs attain three. The argument applies over D by
+embedding into Q. The constructive identities themselves hold over any
+commutative ring with ab=1.
+
+## Full scalar bill and intermediate growth
+
+Use the retained PR5602 real scalar tariff, as defined in its pinned
+`local.py`. For reduced nonzero q=u/2^v, define
+
+```text
+A(q) = 2(3 + bitlength(|u|)-1 + popcount(|u|) + v),
+A_a = sum_(a_i != 0) A(a_i),
+A_b = sum_(b_i != 0) A(b_i).
+```
+
+The sign SCALE costs 2. The cheaper of the two displayed factorizations
+therefore has exact allowance
+
+```text
+B = 2 + min(2 A_a + A_b, A_a + 2 A_b).
+```
+
+This is an exact bill for emitted scalar work, not a proof of global scalar
+optimality. The source caller additionally limits coefficient magnitudes;
+that limit must still be checked for each installation. The named example
+below satisfies it. The general bounded compiler is an algebraic tool and
+does not widen the source caller's admissible coefficients.
+
+For a magnitude bound put alpha=||a||_1 and beta=||b||_1. Every scalar
+prefix of a lower block has infinity-operator norm at most 1+alpha, and
+every scalar prefix of an upper block at most 1+beta. D has norm one.
+Submultiplicativity bounds every intermediate by
+(1+alpha)^2(1+beta) times the input infinity norm for the a-repeated
+program, and (1+alpha)(1+beta)^2 for the b-repeated program. This includes
+partial accumulation inside each block; cancellation only at the end of
+a block is not used as an intermediate bound.
+
+## An arbitrary dirty spare returns in the complete consumer
+
+Let G be a D-linear endomorphism of the field value space. Scalar
+coefficients commute with G. Apply S, then G on the spare alone, then S
+again. Since S^2=I, the complete map is
+
+```text
+x -> x + b(G-I)ax
+z -> z.
+```
+
+One direct calculation starts after the first S with
+x'=(I-ba)x+bz and z'=ax. The last S sends the data to
+(I-ba)x'+bGz'=(I-ba)x+bGax, and sends the spare to ax'=z.
+There is no initial-zero premise or dirty-spare contribution to the data.
+The fully charged displayed consumer uses two exchanges, allowance 2B,
+and one application of G. G's own cost, representation, physical delivery,
+any required chart changes and allocation are additional obligations.
+This is not an independence certificate for new productive helper targets.
+
+## First emitted-program improvement
+
+For a=(3,5), b=(2,-1), ab=1 and neither entry of a is a dyadic unit.
+Use the same three roles and spare pivot 2 in both constructions. The
+unmodified PR5611 compiler, called on (3,5,0), (2,-1,0), pivot 2, emits
+20 gates with scalar allowance 134. The new compiler emits
+
+```text
+x_0 += 2 z
+x_1 -= z
+z   -= 3 x_0
+z   -= 5 x_1
+x_0 += 2 z
+x_1 -= z
+z   *= -1.
+```
+
+This has seven gates and allowance 64. Both programs satisfy the same
+dual-pair equations on the same three-role resource contract. Their full
+matrices need not agree on the complementary subspace. The numerical
+comparison concerns the predecessor's actual emitted program, not an
+optimal predecessor algorithm or all possible three-role completions.
+Only that one source invocation is used for the comparison. Its scientific
+suite is not replayed or claimed as this contribution.
+
+The corresponding displayed consumer has fourteen scalar gates and
+allowance 128, plus G. No claim is made that this consumer bill or its sign
+operations are minimal. This first small compiler improvement is the
+deliverable; no larger physical search is included.
+
+## Evidence and remaining obligations
+
+The written algebra proves the quantified result. Exact finite replays
+corroborate the emitted code, full matrices, all scalar prefixes, tariff,
+and dirty-spare return for a nonscalar two-coordinate G. Deliberate
+omission, sign, ordering and invalid-input controls must reject. Tests
+alone are not an all-input proof or formal-kernel acceptance.
+
+This package finds no actual P104 cut, physical native supplier, rounded
+precision allocation, favorable complete paid/target invoice or new kappa.
+All five selected framework assumptions remain. Classical stabilized
+completion has a broad literature; for historical context see M. Roitman,
+[Completing unimodular rows to invertible matrices, 1977](https://doi.org/10.1016/0021-8693(77)90280-0).
+That citation is background, not a claim that this elementary block identity
+or the notion of completion is new.

research/division-free-dual-exchange/README.md

@@ -0,0 +1,140 @@
+# Division-free dyadic dual-pair exchange
+
+One arbitrary common-chart spare role gives a coefficient-preserving
+alternative to Euclidean dual-pair preparation. For the nonunit pair
+a=(3,5), b=(2,-1), the emitted basis program falls from twenty gates and
+scalar allowance 134 to seven gates and allowance 64, on the same three
+roles. This is a scoped constructive proof and compiler improvement,
+produced by Nick Petalas. No new kappa is claimed.
+
+Given ab=1, the compiler realizes
+
+```text
+S = [[I-ba,b],[a,0]],    S^2 = I,
+(a,0) S = e_spare^T,    S e_spare = (b,0)^T.
+```
+
+It uses three off-diagonal block shears and one sign SCALE. Every ADD
+coefficient is a signed input coefficient. There is no Euclidean quotient,
+odd division, INIT, CLEAR or change of chart. Three block shears are
+necessary for this particular exchange, even with free invertible
+block-diagonal operations. This restricted block count does not establish
+optimality among arbitrary scalar circuits.
+
+For A_a and A_b equal to the summed retained ADD tariffs of the row and
+column, the cheaper displayed factorization has exact scalar allowance
+`2 + min(2 A_a + A_b, A_a + 2 A_b)`. Its gate count is either
+`2 nnz(a)+nnz(b)+1` or `nnz(a)+2 nnz(b)+1`; minimizing the tariff can
+differ from minimizing the gate count.
+
+Applying S, a D-linear G on the spare, and S again gives
+`x -> x+b(G-I)ax`, `z -> z`, for arbitrary incoming z. This complete
+consumer has scalar allowance twice the exchange bill, plus the separate
+cost of G. During the basis exchange alone, the spare contains ax and is
+not restored. Availability of a physical spare is an explicit hypothesis.
+
+[PROOF.md](PROOF.md) gives the complete algebra, block-count obstruction,
+prefix growth envelope, coefficient tariff and dirty-spare calculation.
+[compiler.py](compiler.py) emits either factorization and selects the
+cheaper of these two by default. [verify.py](verify.py) uses a separate
+dense Fraction interpreter, full dirty-input columns and an independently
+written tariff calculation. [RESULT.json](RESULT.json) is generated and
+bound to all package implementation/documentation files and live sources.
+
+## Reproduction
+
+Use CPython 3.12 and the standard library, from the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/division-free-dual-exchange/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/division-free-dual-exchange/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/division-free-dual-exchange
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/division-free-dual-exchange --check-source-history
+```
+
+Any CPython 3.12 path can replace the interpreter shown. Expected scientific
+marker: `PASS_DIVISION_FREE_DUAL_EXCHANGE`. Expected registered marker:
+`PASS_REGISTERED_RESEARCH_PACKAGE`. `verify.py --write` explicitly
+regenerates RESULT.json; default replay is read-only. The source comparator
+is called only on the one named padded pair, to measure its emitted
+program. No predecessor scientific suite is run.
+
+The finite replay passes 116 integer dual pairs with both vectors in
+[-3,3]^2 for both factorizations, 64 dyadic pairs through dimension eight,
+three valid compiler-boundary cases, nine complete two-coordinate-field
+consumers and nineteen rejecting controls. Every
+scalar prefix is checked against its proved magnitude envelope. Both
+direct warning-strict normal/optimized commands completed in under one
+second locally on CPython 3.12. These durations describe the bounded
+checks; no execution-speed comparison is claimed.
+
+## Scope, provenance and credit
+
+Base `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8.
+The selected record at that base has conditional kappa .003125804 and five
+retained framework assumptions. The binding-only first example passed.
+This changes the `p104-side-correction` card to an enabling scalar-boundary
+construction; it does not meet that card's complete supplier acceptance gate.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294890)
+is the canonical investigation. The first emitted-program improvement is
+packaged without a larger construction search.
+
+Ali Romman supplies [PR5611](https://github.com/CrocSwap/integer-mult-bounds/pull/5611)'s
+dual-pair specification and complete Euclidean compiler, and
+[PR5602](https://github.com/CrocSwap/integer-mult-bounds/pull/5602)'s
+helper handoff and scalar tariff, following
+[PR5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599).
+All retained P104, native, controller and compiler contributors keep their
+credit. Nick Petalas's
+[PR5115](https://github.com/CrocSwap/integer-mult-bounds/pull/5115)
+is earlier source-only borrowing with no spare and a different shear
+contract. The two-role conditioning question in PR6016 is not extended
+here. Elementary stabilized completion and block-shear identities are
+classical; the new claim is this explicit coefficient-preserving compiler
+application and its stated bill, not historical priority for the algebra.
+Apache-2.0. Independent human and formal proof-kernel review are unclaimed.
+
+Live handoffs, active Discussions, open PRs, recent account contributions,
+main README formulas/objects and merged searches were checked before the
+claim. The cached overlap report has sparse local-note coverage. Those
+bounded checks do not cover unpublished work or prove global novelty.
+
+This package constructs no physical P104 handoff, productive target split,
+native supplier, rounded implementation or favorable complete invoice.
+Chart access, spare allocation/lifetimes, G's cost and legality,
+precision/storage, compiler closure and outer funding remain obligations.
+The source caller's coefficient-magnitude cap remains applicable to an
+installation. Selected scientific replay, Lean and a complete multiplication
+theorem are outside this result.
+
+## Open next questions
+
+1. Is there a current helper boundary with an available arbitrary spare at
+   every chart needed by this exchange and its return? This determines
+   whether the compiler can help an actual supplier. First identify one
+   exact word, cut, dual pair and spare lifetime, then charge every required
+   transport and target debit. Physical availability and the complete
+   signed invoice are the blockers.
+2. Can a physically legal use of G improve the complete consumer bill after
+   chart changes and precision are charged? First price one exact G and its
+   full S/G/S macro. The algebraic one-call count alone is insufficient;
+   no such source/consumer match is supplied here.
+
+## Executable bounds
+
+Build the Lever led to the retained compiler and executable evidence.
+Prove It Works led to full matrix checks, including every arbitrary spare
+column. Power of Ten inspection found no recursion in the new code and
+kept functions below sixty physical lines. Compiler inputs have at most
+sixteen coordinates, 64 numerator bits and 32 fractional bits. Its output
+has at most 49 scalar operations. Every loop in the finite verifier has an
+explicit fixed dimension or enumeration bound. Checks use exceptions,
+so optimized Python preserves them.
+
+Managed Python allocation is a rule 3 deviation bounded by these offline
+input, file and enumeration limits; no steady service is provided. Loading
+one authenticated predecessor module for the single comparison is a
+restricted rule 8/9 deviation with one fixed target. No source-level
+dynamic generation or network call occurs. Warning-strict normal and
+optimized execution provide diagnostics. No shared lint configuration,
+predecessor source, pinned evidence or selected record is changed.