diff --git a/research/division-free-dual-exchange/PROOF.md b/research/division-free-dual-exchange/PROOF.md new file mode 100644 index 0000000000..ef845be379 --- /dev/null +++ b/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. diff --git a/research/division-free-dual-exchange/README.md b/research/division-free-dual-exchange/README.md new file mode 100644 index 0000000000..5cf1073ede --- /dev/null +++ b/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. diff --git a/research/division-free-dual-exchange/RESULT.json b/research/division-free-dual-exchange/RESULT.json new file mode 100644 index 0000000000..f0005d53eb --- /dev/null +++ b/research/division-free-dual-exchange/RESULT.json @@ -0,0 +1,83 @@ +{ + "counts": { + "boundary_pairs": 3, + "controls_rejected": 19, + "dyadic_pairs": 64, + "field_consumers": 9, + "integer_pairs": 116 + }, + "fixture": { + "a": [ + 3, + 5 + ], + "b": [ + 2, + -1 + ], + "legacy_allowance": 134, + "legacy_gates": 20, + "new_allowance": 64, + "new_gates": 7, + "new_program": [ + [ + "ADD", + 0, + 2, + "2" + ], + [ + "ADD", + 1, + 2, + "-1" + ], + [ + "ADD", + 2, + 0, + "-3" + ], + [ + "ADD", + 2, + 1, + "-5" + ], + [ + "ADD", + 0, + 2, + "2" + ], + [ + "ADD", + 1, + 2, + "-1" + ], + [ + "SCALE", + 2, + 2, + "-1" + ] + ], + "roles": 3 + }, + "package_sha256": { + "PROOF.md": "84973fa811181824228610fdaf95504d915a4e98a594bfb0591acb963f354079", + "README.md": "c7f6c03990f858c85fd199babdc927f79af25de4421681d9a488c9f8d231ce09", + "SOURCES.json": "a6369cb59d3e9f1071b4610ea913deb6b36f3118c6d6f70caebe500fb43cbba5", + "TASK.json": "af2acab866adf771dfcbf884c96a260c78fb469e926a00fa1b84273e37f9f9d3", + "VERIFY.json": "3e19489d7511cf4861570ceb433a5dd190073e4f341afdaae0e6518abbf42261", + "compiler.py": "9d7b71ed4da90360f8a0f15b7a89599340efbb4eb1ff40054e11e621f85df5bf", + "verify.py": "17d41e20eb84a0f0f965ff4ff0515fcff996ea6f70bddd60bf217baf72eaca5d" + }, + "schema": "division-free-dual-exchange/1", + "source_sha256": { + "research/dyadic-helper-basis-completion/PROOF.md": "a909d7b909edffb5babec3e937a3d13052aeaf87852ec73a37dac9802b6d9734", + "research/dyadic-helper-basis-completion/basis.py": "f4d097783dd775d434994f1903eb20006cc03933f428bf3edec463437185daf7", + "research/p104-coupled-helper-bases/local.py": "5f0678c768544517780d3511995faf0d7062748e7e780c0adb5c4d9c2749a925" + } +} diff --git a/research/division-free-dual-exchange/SOURCES.json b/research/division-free-dual-exchange/SOURCES.json new file mode 100644 index 0000000000..ee140e2f9e --- /dev/null +++ b/research/division-free-dual-exchange/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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/dyadic-helper-basis-completion/PROOF.md", + "usage": "input", + "git_blob": "8c51201534aaab80b2cefe1ef12c3a1048ce3f36", + "sha256": "a909d7b909edffb5babec3e937a3d13052aeaf87852ec73a37dac9802b6d9734" + }, + { + "path": "research/dyadic-helper-basis-completion/basis.py", + "usage": "input", + "git_blob": "6b2bcbbb7c578376bf7a2e72e52cd815c12ebbc9", + "sha256": "f4d097783dd775d434994f1903eb20006cc03933f428bf3edec463437185daf7" + }, + { + "path": "research/p104-coupled-helper-bases/local.py", + "usage": "input", + "git_blob": "9556e86744e18efdd76263a36664830c695f1c0f", + "sha256": "5f0678c768544517780d3511995faf0d7062748e7e780c0adb5c4d9c2749a925" + } + ] +} diff --git a/research/division-free-dual-exchange/TASK.json b/research/division-free-dual-exchange/TASK.json new file mode 100644 index 0000000000..54efa22a25 --- /dev/null +++ b/research/division-free-dual-exchange/TASK.json @@ -0,0 +1,125 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "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/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/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": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "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": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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": "Division-free dyadic dual-pair exchange with an arbitrary common-chart spare, exact scalar tariff, three-block lower bound and dirty-spare return consumer.", + "scope_change_reason": "The target changes from finding a physical helper split to an enabling basis construction with one explicit spare coordinate. No complete supplier or new productive target is claimed.", + "bottleneck_link": "Nonunit dyadic pairings can require costly Euclidean preparation. This coefficient-preserving alternative bounds emitted work when a compatible spare is physically available; delivery and the complete signed invoice remain open.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified emitted-program improvement; do not extend to a physical cut search.", + "outcome": "completed", + "evidence": "PROOF.md; compiler.py; independent dense interpreter and tariff in verify.py; generated source-bound RESULT.json", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is an arbitrary spare physically available at the required charts of a current helper boundary?", + "why_it_matters": "Determines whether the enabling compiler can be installed without losing its scalar benefit.", + "first_step": "Pin one exact word, cut, dual pair and spare lifetime, and price every transport and target debit.", + "blocked_by": "No current-word spare allocation or complete signed invoice is supplied." + }, + { + "question": "Can a legal G and the full S/G/S consumer improve a matched complete bill?", + "why_it_matters": "The algebraic single-call consumer alone does not imply a supplier saving.", + "first_step": "Specify one actual G, its chart/routing/precision contract and the full consumer bill.", + "blocked_by": "No physical source/consumer match or rounded implementation is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294890", + "claim_type": "scoped constructive proof with exact finite corroboration" +} diff --git a/research/division-free-dual-exchange/VERIFY.json b/research/division-free-dual-exchange/VERIFY.json new file mode 100644 index 0000000000..1ca81e21f8 --- /dev/null +++ b/research/division-free-dual-exchange/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/dyadic-helper-basis-completion/PROOF.md", + "research/dyadic-helper-basis-completion/basis.py", + "research/p104-coupled-helper-bases/local.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Full dual-pair/involution matrices, scalar prefixes, both tariffs, arbitrary dirty-spare consumer, named emitted-program comparison and rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete finite evidence with optimized Python and all exception-based checks retained." + } + ] +} diff --git a/research/division-free-dual-exchange/compiler.py b/research/division-free-dual-exchange/compiler.py new file mode 100644 index 0000000000..9ead98d573 --- /dev/null +++ b/research/division-free-dual-exchange/compiler.py @@ -0,0 +1,73 @@ +"""Division-free dual-pair exchange, produced by Nick Petalas; Apache-2.0.""" + +from fractions import Fraction + +MAX_DIMENSION = 16 +MAX_NUMERATOR_BITS = 64 +MAX_DENOMINATOR_BITS = 33 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def pair(a, b): + """Validate a bounded dyadic dual pair at the public compiler boundary.""" + need(type(a) in (list, tuple) and type(b) in (list, tuple), "Vector containers") + need(1 <= len(a) == len(b) <= MAX_DIMENSION, "Matching bounded dimensions") + need(all(type(q) in (int, Fraction) for q in (*a, *b)), "Exact coefficients") + a, b = tuple(map(Fraction, a)), tuple(map(Fraction, b)) + for q in (*a, *b): + need(abs(q.numerator).bit_length() <= MAX_NUMERATOR_BITS, "Numerator bound") + d = q.denominator + need(d.bit_length() <= MAX_DENOMINATOR_BITS and d & (d - 1) == 0, + "Bounded dyadic denominator") + need(sum(x * y for x, y in zip(a, b)) == 1, "Dual pairing equals one") + return a, b + + +def addition_cost(q): + """PR5602's real scalar ADD allowance for a nonzero dyadic coefficient.""" + q = Fraction(q) + n, d = abs(q.numerator), q.denominator + need(n > 0 and d & (d - 1) == 0, "Nonzero dyadic ADD") + return 2 * (3 + n.bit_length() - 1 + n.bit_count() + d.bit_length() - 1) + + +def allowance(operations): + """Price this compiler's ADDs and its one sign SCALE.""" + need(len(operations) <= 3 * MAX_DIMENSION + 1, "Exchange operation bound") + total = 0 + for op, destination, source, q in operations: + if op == "ADD": + need(destination != source, "Distinct ADD roles") + total += addition_cost(q) + else: + need(op == "SCALE" and destination == source and q == -1, + "Only sign SCALE") + total += 2 + return total + + +def compile_exchange(a, b, repeat="cheapest"): + """Emit S=[[I-ba,b],[a,0]] on n data roles and arbitrary spare role n. + + 'cheapest' minimizes the declared tariff among these two factorizations. + It does not solve unrestricted circuit optimization. + """ + a, b = pair(a, b) + need(repeat in ("a", "b", "cheapest"), "Known factorization") + if repeat == "cheapest": + a_cost = sum(addition_cost(q) for q in a if q) + b_cost = sum(addition_cost(q) for q in b if q) + repeat = "a" if a_cost < b_cost else "b" + spare = len(a) + upper = [("ADD", i, spare, q) for i, q in enumerate(b) if q] + lower = [("ADD", spare, i, q) for i, q in enumerate(a) if q] + sign = [("SCALE", spare, spare, Fraction(-1))] + if repeat == "b": + negative = [(op, r, s, -q) for op, r, s, q in lower] + return upper + negative + upper + sign + negative = [(op, r, s, -q) for op, r, s, q in upper] + return sign + lower + negative + lower diff --git a/research/division-free-dual-exchange/verify.py b/research/division-free-dual-exchange/verify.py new file mode 100644 index 0000000000..311a8c0c5b --- /dev/null +++ b/research/division-free-dual-exchange/verify.py @@ -0,0 +1,224 @@ +"""Exact finite corroboration, produced by Nick Petalas; Apache-2.0.""" + +import argparse +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +from itertools import product +import json +from pathlib import Path + +import compiler as C + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +LIMIT = 128 * 1024 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def digest(path): + need(path.stat().st_size <= LIMIT, "Bounded file size") + return sha256(path.read_bytes()).hexdigest() + + +def bindings(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + inputs = [r for r in manifest["files"] if r["usage"] == "input"] + need(len(inputs) == 3, "Three declared source inputs") + for row in inputs: + need(digest(ROOT / row["path"]) == row["sha256"], "Source hash " + row["path"]) + return {row["path"]: row["sha256"] for row in inputs} + + +def identity(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def multiply(a, b): + n = len(a) + return [[sum(a[i][k] * b[k][j] for k in range(n)) + for j in range(n)] for i in range(n)] + + +def expected(a, b): + n = len(a) + return [[Q(i == j) - b[i] * a[j] for j in range(n)] + [b[i]] + for i in range(n)] + [list(a) + [Q(0)]] + + +def interpret(operations, n, growth=None): + rows = identity(n) + for op, r, s, q in operations: + need(0 <= r < n and 0 <= s < n and q != 0, "Instruction indices") + if op == "ADD": + need(r != s, "Distinct row update") + rows[r] = [x + q * y for x, y in zip(rows[r], rows[s])] + else: + need(op == "SCALE" and r == s and q == -1, "Sign instruction") + rows[r] = [q * x for x in rows[r]] + if growth is not None: + need(max(sum(map(abs, row)) for row in rows) <= growth, + "Every scalar prefix respects the height envelope") + return rows + + +def independent_cost(operations): + cost = 0 + for op, _, _, q in operations: + if op == "SCALE": + need(q == -1, "Priced sign") + cost += 2 + else: + numerator = bin(abs(q.numerator))[2:] + exponent = q.denominator.bit_length() - 1 + cost += 2 * (len(numerator) + numerator.count("1") + exponent + 2) + return cost + + +def check_pair(a, b): + a, b = tuple(map(Q, a)), tuple(map(Q, b)) + n, s = len(a), expected(a, b) + prices = [] + for repeat in ("a", "b"): + ops = C.compile_exchange(a, b, repeat) + alpha, beta = 1 + sum(map(abs, a)), 1 + sum(map(abs, b)) + bound = alpha * alpha * beta if repeat == "a" else alpha * beta * beta + matrix = interpret(ops, n + 1, bound) + need(matrix == s and multiply(matrix, matrix) == identity(n + 1), + "Complete exchange and arbitrary-input involution") + repeated, single = (a, b) if repeat == "a" else (b, a) + count = 2 * sum(q != 0 for q in repeated) + sum(q != 0 for q in single) + 1 + need(len(ops) == count, "Exact scalar gate count") + permitted = {Q(-1)} | set(a) | set(b) | {-q for q in (*a, *b)} + need(all(q in permitted for _, _, _, q in ops), "No new coefficients") + prices.append(independent_cost(ops)) + need(C.allowance(ops) == prices[-1], "Independent scalar tariff") + chosen = C.compile_exchange(a, b) + need(independent_cost(chosen) == min(prices), "Cheaper displayed factorization") + return len(chosen) + + +def consumer(a, b): + """Check every dirty-input column with a non-scalar two-coordinate G.""" + n = len(a) + scalar = interpret(C.compile_exchange(a, b), n + 1) + whole = [[scalar[i // 2][j // 2] * Q(i % 2 == j % 2) + for j in range(2 * n + 2)] for i in range(2 * n + 2)] + g = [[Q(2), Q(1)], [Q(1), Q(1)]] + use = identity(2 * n + 2) + for i in range(2): + for j in range(2): + use[2 * n + i][2 * n + j] = g[i][j] + actual = multiply(whole, multiply(use, whole)) + target = identity(2 * n + 2) + for i in range(n): + for j in range(n): + for r in range(2): + for s in range(2): + target[2 * i + r][2 * j + s] += b[i] * a[j] * (g[r][s] - Q(r == s)) + need(actual == target, "Full field consumer, arbitrary spare return and no leakage") + + +def legacy_fixture(): + path = ROOT / "research/dyadic-helper-basis-completion/basis.py" + spec = importlib.util.spec_from_file_location("pinned_legacy_basis", path) + need(spec is not None and spec.loader is not None, "Pinned comparison loader") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + old = module.compile_basis([3, 5, 0], [2, -1, 0], 2) + new = C.compile_exchange([3, 5], [2, -1]) + old_cost = 0 + for op, _, _, q in old: + if op == "ADD": + old_cost += independent_cost([(op, 0, 1, q)]) + else: + n, d = abs(q.numerator), q.denominator + old_cost += 2 * (abs(n.bit_length() - d.bit_length()) + int(q < 0)) + need((len(old), old_cost, len(new), independent_cost(new)) == (20, 134, 7, 64), + "Named emitted-program improvement") + return {"a": [3, 5], "b": [2, -1], "roles": 3, + "legacy_gates": len(old), "legacy_allowance": old_cost, + "new_gates": len(new), "new_allowance": independent_cost(new), + "new_program": [[op, r, s, str(q)] for op, r, s, q in new]} + + +def rejects(action): + try: + action() + except ValueError: + return 1 + raise ValueError("Expected rejection did not occur") + + +def controls(): + invalid = [([], []), ([1], [1, 0]), ([1], [0]), ([Q(1, 3)], [3]), + ([1.0], [1]), ([True], [1]), ([2**65], [Q(1, 2**65)]), + ([Q(1, 2**33)], [2**33]), ([1] * 17, [1] + [0] * 16)] + count = sum(rejects(lambda a=a, b=b: C.compile_exchange(a, b)) for a, b in invalid) + count += rejects(lambda: C.compile_exchange([1], [1], "unknown")) + good = C.compile_exchange([3, 5], [2, -1], "b") + target = expected([Q(3), Q(5)], [Q(2), Q(-1)]) + for index in range(len(good)): + altered = good[:index] + good[index + 1:] + count += rejects(lambda altered=altered: need(interpret(altered, 3) == target, + "Omitted operation detected")) + bad = good[:] + op, r, s, q = bad[2] + bad[2] = (op, r, s, -q) + count += rejects(lambda: need(interpret(bad, 3) == target, "Wrong sign detected")) + count += rejects(lambda: need(interpret(list(reversed(good)), 3) == target, + "Wrong chronological order detected")) + return count + + +def evidence(): + counts = {"integer_pairs": 0, "dyadic_pairs": 0, "field_consumers": 0, + "boundary_pairs": 0} + for x, y, u, v in product(range(-3, 4), repeat=4): + if x * u + y * v == 1: + check_pair([x, y], [u, v]) + counts["integer_pairs"] += 1 + for n in range(1, 9): + for k in range(8): + b = [Q(1)] + [Q((i + k) % 5 - 2, 2**(k % 4)) for i in range(1, n)] + a = [Q(0)] + [Q((2 * i + k) % 7 - 3, 2**((k + 1) % 4)) for i in range(1, n)] + a[0] = 1 - sum(a[i] * b[i] for i in range(1, n)) + check_pair(a, b) + counts["dyadic_pairs"] += 1 + if k == 0: + consumer(a, b) + counts["field_consumers"] += 1 + check_pair([3, 5], [2, -1]) + for a, b in [([1] + [0] * 15, [1] + [0] * 15), + ([2**63, 1], [0, 1]), ([Q(1, 2**32)], [2**32])]: + check_pair(a, b) + counts["boundary_pairs"] += 1 + consumer(list(map(Q, [3, 5])), list(map(Q, [2, -1]))) + counts["field_consumers"] += 1 + counts["controls_rejected"] = controls() + return {"schema": "division-free-dual-exchange/1", "counts": counts, + "fixture": legacy_fixture(), "source_sha256": bindings()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="Regenerate the retained result") + args = parser.parse_args() + bindings() + result = evidence() + files = ["compiler.py", "verify.py", "PROOF.md", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json"] + result["package_sha256"] = {name: digest(HERE / name) for name in files} + target = HERE / "RESULT.json" + if args.write: + target.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + need(result == json.loads(target.read_text()), "Generated result and source bindings") + print("PASS_DIVISION_FREE_DUAL_EXCHANGE " + json.dumps(result["counts"], sort_keys=True)) + + +if __name__ == "__main__": + main()