From f4979f2cf14625c65424fe09d48545efb6f261e1 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 20:58:59 -0700 Subject: [PATCH 1/3] Implement source-bound rounded C0 and C2 completed-call contracts --- .../PROOF.md | 177 +++++++++++++++++ .../README.md | 54 ++++++ .../RESULT.json | 151 +++++++++++++++ .../SOURCES.json | 42 ++++ .../TASK.json | 80 ++++++++ .../VERIFY.json | 34 ++++ .../rounded.py | 119 ++++++++++++ .../source/CHANNELS.md | 94 +++++++++ .../source/FULL-INPUT-PORT.md | 86 +++++++++ .../source/QQ16-ROUNDING.md | 181 ++++++++++++++++++ .../source/channels.py | 167 ++++++++++++++++ .../source/pins.json | 6 + .../verify.py | 110 +++++++++++ 13 files changed, 1301 insertions(+) create mode 100644 research/native-rounded-butterfly-contract/PROOF.md create mode 100644 research/native-rounded-butterfly-contract/README.md create mode 100644 research/native-rounded-butterfly-contract/RESULT.json create mode 100644 research/native-rounded-butterfly-contract/SOURCES.json create mode 100644 research/native-rounded-butterfly-contract/TASK.json create mode 100644 research/native-rounded-butterfly-contract/VERIFY.json create mode 100644 research/native-rounded-butterfly-contract/rounded.py create mode 100644 research/native-rounded-butterfly-contract/source/CHANNELS.md create mode 100644 research/native-rounded-butterfly-contract/source/FULL-INPUT-PORT.md create mode 100644 research/native-rounded-butterfly-contract/source/QQ16-ROUNDING.md create mode 100644 research/native-rounded-butterfly-contract/source/channels.py create mode 100644 research/native-rounded-butterfly-contract/source/pins.json create mode 100644 research/native-rounded-butterfly-contract/verify.py diff --git a/research/native-rounded-butterfly-contract/PROOF.md b/research/native-rounded-butterfly-contract/PROOF.md new file mode 100644 index 0000000000..b5040dc9b0 --- /dev/null +++ b/research/native-rounded-butterfly-contract/PROOF.md @@ -0,0 +1,177 @@ +# A concrete fixed-grid completed-call contract for C0 and C2 + +JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0. + +## Scope and existing work + +PR4743 supplies the literal two- and three-call triangular ports, their inverse +schedules and arbitrary dirty-bank interpretation. `native-error-channel-amplification` +already proves source-ordered completed-call error amplification. That result +assumes an implementation returns its exact Gaussian transform of its **actual +stored input** within a requested complex-coordinate radius. This package +constructs one such implementation, including internal range and direct work. + +This is not the first deterministic native rounding example. Arham Tahir's +PR3036 and the retained `qq16-native-rounded-components` implement pair-first +native Gaussian interiors with floating significands and prove a whole-F0 +failure. We reuse its conventional butterfly lowering and signed ties-to-even +method as credited precedent. Our new scope is a uniform fixed-grid accuracy +service for the actual C0/C2 tensor letters, with a completed-call theorem and +all four PR4743 port schedules. We do not rerun or claim novelty for full F0. + +## Actual arithmetic ABI and operation order + +Let h=2^-g. Store each real/imaginary component as a signed integer times h. +All inputs to a call have this form. The Cj base letter is + + Cj = ((1+i) I + (1-i) Xj)/2. + +On a complex pair `(a+ib,c+id)` of grid integers, form EXACT integer values + + sr=a+c; si=b+d; dr=a-c; di=b-d; + n0=sr-di; n1=si+dr; n2=sr+di; n3=si-dr. + +Store nearest-even(n0/2),...,nearest-even(n3/2). For the adjoint use +`sr+di, si-dr, sr-di, si+dr`. Overflow checks precede every numerator storage. +For every signed integer n, put q=n>>1 with arithmetic right shift (floor), and + + nearest_even(n/2) = q + ((n & 1) & (q & 1)). + +For even n this is exact. For odd n the two nearest integers are q and q+1; +the expression selects the even one, also when n<0. This is an explicit +arithmetic-shift ABI, not a division-free claim for a machine lacking that +instruction. No floating exponent, division oracle or unbounded-word primitive +is used. Pair sums are exact on the grid, so intermediate rounding at those +sums would do nothing; rounding occurs at the four final halves. + +On N=8^f entries apply this butterfly on bit positions3k+j for k=0,...,f-1, +in that declared order, j=0 or2. These commuting exact coordinate factors +produce Cj^tensor f before rounding; the rounded factors need not commute. +`rounded.call` executes the stated order and charges all fN/2 butterflies. + +## Uniform completed-call defect and internal range + +For one butterfly, each real component error has absolute value at most h/2, +so each complex coordinate has error at most h/sqrt2. The coordinate infinity +norm of one exact Gaussian factor is sqrt2. If delta_k is the maximum error +versus the exact first k factors applied to the actual stored input, then + + delta_0=0; + delta_(k+1) <= sqrt2 delta_k + h/sqrt2. + +Thus for every f>=1, both axes and both adjoint choices, + + delta_f <= eta_f h, + eta_f = (2^(f/2)-1)/(2-sqrt2) < 2 * 2^(f/2). + +This is a sufficient bound; no sharpness of eta_f for deterministic arithmetic +is claimed. The proof uses actual errors on actual perturbed inputs, not a +promise valid only at an ideal input. Correlations cannot invalidate the upper +bound. If the call's stored input has complex magnitude at most U, after k +stages it is at most `2^(k/2) U + eta_k h < 2^(k/2)(U+2h)`. +Each integer numerator formed at the next stage is at most four times the +component bound divided by h. These are explicit internal cuts, not merely +endpoint conditioning. + +To meet a requested completed-call tolerance rho=2^-q choose + + g = q + ceil(f/2) + 1. + +Then `eta_f 2^-g < rho`. Nearest-even input quantization at the same grid has +complex error at most h/sqrt2 < rho. This does not require extra free fault +variables or independence between the actual roundings. + +## Source-ordered port substitution and sufficient widths + +Retain the actual P=S U S,Q=S V01 S,W=Z0 Z2,M=Z1 V01 monomials and their global +phases. The three-call forward order is A on x; the two separately conjugated +P and Q additions into y; A on y; W on y; C2 on y; M on y. The reverse order +is M^-1,C2^-1,W^-1,A^-1 on y; subtract the two monomial terms from retained x; +then A^-1 on x. Two-call variants omit the extra C2/M/W layer. Each free update +really maps x, adds to y, then restores x. Integer scaling by2 is a left shift. +These monomial/integer operations are exact on the common grid and checked +against word bounds. The completed C2 defect is before M, not after it. + +The predecessor's proved external tolerance for final error2^-P is2^-q with: + +| schedule | q | +|---|---| +| two-call forward |P+f+3| +| three-call forward |P+ceil(3f/2)+3| +| two-call reverse |P+ceil(f/2)+2| +| three-call reverse |P+f+2| + +Choose g=q+ceil(f/2)+1 as above. Every completed call satisfies that tolerance, +and so does initial quantization. Substitution into the credited source-ordered +error-channel proof gives final complex-coordinate error at most2^-P on both +banks, for every f>=1 and P>=0. Independence of actual defects is unnecessary: +the predecessor bound holds for every choice in the enclosing balls. There is +no new proof of its sharp external constant or claim that our implementation +attains it. + +For original complex coordinate magnitudes at most2^H, H>=0, the predecessor's +port-entry/internal-between-call allowance2^(H+2f+4) remains valid since each +new completed-call defect is below its requested rho<=1/8. Put U equal to that +allowance. Since h<=1 and U>=1, the call-internal prefix is below2^(ceil(f/2))(U+2h) +<=3*2^(ceil(f/2))*U. Numerators are less than12 times that binary U factor. +Consequently the conservative signed component width + + w = H + g + 2f + ceil(f/2) + 9 + +suffices for all exact pair sums, differences, numerators, rounded outputs, +integer mix intermediates and phase negations. The extra fixed margin covers +sign and the factor12; no wraparound is allowed. For f,H,P=O(log n), this width +is O(log n); it is not a numerical constant independent of the input size. +The verifier actively rejects insufficient width at a numerator before rounding. + +## Costs, workspace and restoration + +Each butterfly uses8 signed additions/subtractions and four half-even operations. +Each half uses one arithmetic shift, three ANDs and one ADD:28 elementary +integer operations per butterfly, plus4 real reads and4 real writes. One call +therefore costs14 f N integer operations and2 f N real reads plus2 f N writes, +before bounded loop/address overhead. It uses eight real scratch words and +constant loop indices; the arrays are updated in place. Both forward and inverse +call cost this same direct bound. This is O(fN) work, NOT the recursive rank-one +child's advertised accelerated tariff. All calls in both port directions are +counted. The implementation is a sufficient accuracy backend and control, not +an admissible faster multiplication supplier. + +The executable monomial backend builds N address/phase records in O(fN) bounded +word work, traverses cycles with N owned visited bytes and two held complex +values, then explicitly zeros the route/visited fields. This is O(N) owned +control workspace, not a clean independent productive bank. Metadata, +allocation, initialization, clearing, sign operations and mixing retain their +O(fN)/O(N) costs. Source/native O(N) monomial implementations may replace this +conservative backend only with their own source-bound proof. The reference +oracle and optional verifier cut snapshots allocate extra arrays as proof +instrumentation; they are not claimed production scratch or included in the +small-workspace algorithm. No actual caller dirty array is cleared or borrowed. +Only owned work is initialized/cleared; approximate forward/reverse composition +need not restore arbitrary numerical input exactly. + +## Realizable defects are more constrained than independent balls + +For one pair, all four numerator parities equal a+b+c+d modulo2. Therefore +all four real rounding defects are zero together, or all four have magnitude +h/2. An isolated one-real-component defect is permitted by an independent-ball +relaxation but impossible at this cut. The grid input `(1,0),(0,0)` rounds to +zero on both output coordinates, while the exact C0 image is nonzero: a concrete +reachable half-grid loss, with no injected fault. This is compatible with the +sufficient error bound; it is not a failure at the guarded requested tolerance. +The parity argument is uniform over every integer input; the625-case census +corroborates it and does not establish it by extrapolation. + +## Evidence and limitations + +The source-authenticated exact sparse-matrix engine is retained from +`native-error-channel-amplification`, credited rather than claimed new. Production +monomial/rounding code imports none of it. Exact tensor matrices independently +check actual C0/C2/adjoint output errors on nonzero-rounding inputs through f=3; +all twelve complete port cases compare against exact rational trajectories, +including an off-grid original input quantized to the stored grid. Every paid +cut is compared to the exact transform of its actual stored input. Signed tie, +wrong-axis, adjoint, overflow and domain controls reject. The all-f theorem is +the recurrence proof above, not the finite checks. Complete recursive substitution, +fast Gaussian call implementation, fixed tapes, native supplier/outer admission, +and selected5413 reproduction remain outside scope. diff --git a/research/native-rounded-butterfly-contract/README.md b/research/native-rounded-butterfly-contract/README.md new file mode 100644 index 0000000000..3a6543be1b --- /dev/null +++ b/research/native-rounded-butterfly-contract/README.md @@ -0,0 +1,54 @@ +# Concrete rounded C0/C2 completed-call service + +For the literal PR4743 tensor calls, an explicit nearest-even fixed-grid +butterfly implementation meets a requested completed-call tolerance rho=2^-q +with grid bits **g=q+ceil(f/2)+1**. The proof includes every internal numerator, +actual stored inputs, adjoints, two arbitrary dirty banks, all four forward/reverse +ports and a conservative signed-word width. No freely chosen error is injected. + +[PROOF.md](PROOF.md) supplies the all-width recurrence, source-ordered substitution, +work/storage bill and limits. This direct backend costs O(f8^f), including every +paid-call butterfly; it does not inherit an accelerated recursive tariff and +makes no new κ or selected-frontier claim. + +``` +python3 -I -W error -B research/native-rounded-butterfly-contract/verify.py +python3 -I -W error -O -B research/native-rounded-butterfly-contract/verify.py +python3 -B scripts/research_package.py --package research/native-rounded-butterfly-contract +``` + +The verifier uses authenticated predecessor sparse-matrix arithmetic as an exact +oracle, and a new integer production path with literal phases and rounding. It +checks C0/C2 in both directions at widths1/2/3, all twelve actual port cases, +input quantization, every completed-call defect against actual stored inputs, +signed ties, nonzero rounding and overflow/axis/adjoint controls. RESULT is +recomputed and compared. The explicit half-grid unit-input loss also shows why +abstract independent error balls need not describe realizable rounding patterns. + +This answers the concrete implementation question left by our +`native-error-channel-amplification`; it does not repeat its sharp external norm +calculation. It differs from the already completed QQ16 F0 native rounding +witness, which uses significand rounding on a different complete word. + +Canonical source base32890bc5de034ab8fc93ac88ead7279a6a416d04, priority7; +[Discussion5475](https://github.com/CrocSwap/integer-mult-bounds/discussions/5475). +The retained selected5413 frontier is unchanged. Root coordinated fresh live +handoff/PR/Discussion overlap before assignment. + +## Open next questions + +- Can a source-compatible accelerated recursive Gaussian implementation satisfy + the same internal contract with a better full work/precision bill? Begin with + one actual recursive child, preserving every rounded cut and scratch return. + The direct O(fN) algorithm here supplies accuracy, not that acceleration. +- Which sharp external fault patterns can actually be generated by deterministic + rounded whole ports? Start from the proved one-butterfly parity constraint. + The independent-ball upper bound does not establish attainability. + +Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0. +Credit Dugongue PR4743 for the actual arbitrary-input ports, Nick Petalas PR4828 +for endpoint conditioning, JoyboyBrian's preceding error-channel analysis, +Arham Tahir PR3036 and `qq16-native-rounded-components` for actual pair-first +rounding precedent, and Yiyang/Lyy-iiis PR4710, lee-phys PR4688, Jacob Alan Sussman +PR4628 and the full lineage retained in source/FULL-INPUT-PORT.md. No independent +human or formal-kernel acceptance is claimed. diff --git a/research/native-rounded-butterfly-contract/RESULT.json b/research/native-rounded-butterfly-contract/RESULT.json new file mode 100644 index 0000000000..cd0c8687a6 --- /dev/null +++ b/research/native-rounded-butterfly-contract/RESULT.json @@ -0,0 +1,151 @@ +{ + "status": "PASS_NATIVE_ROUNDED_BUTTERFLY_CONTRACT", + "half_rounding_cases": 20003, + "completed_calls": 36, + "nonzero_call_roundings": 14976, + "port_cases": [ + { + "input_quantized_max_error_squared_grid": "221/18", + "f": 1, + "kind": 2, + "reverse": false, + "grid_bits": 10, + "signed_bits": 23, + "rounding_events": 20, + "max_error_squared_grid": "13/2", + "butterflies": 8 + }, + { + "input_quantized_max_error_squared_grid": "73/18", + "f": 1, + "kind": 2, + "reverse": true, + "grid_bits": 9, + "signed_bits": 22, + "rounding_events": 28, + "max_error_squared_grid": "1/2", + "butterflies": 8 + }, + { + "input_quantized_max_error_squared_grid": "289/18", + "f": 1, + "kind": 3, + "reverse": false, + "grid_bits": 11, + "signed_bits": 24, + "rounding_events": 20, + "max_error_squared_grid": "25/2", + "butterflies": 12 + }, + { + "input_quantized_max_error_squared_grid": "32/9", + "f": 1, + "kind": 3, + "reverse": true, + "grid_bits": 9, + "signed_bits": 22, + "rounding_events": 12, + "max_error_squared_grid": "1/2", + "butterflies": 12 + }, + { + "input_quantized_max_error_squared_grid": "3233/144", + "f": 2, + "kind": 2, + "reverse": false, + "grid_bits": 11, + "signed_bits": 26, + "rounding_events": 300, + "max_error_squared_grid": "241/16", + "butterflies": 128 + }, + { + "input_quantized_max_error_squared_grid": "73/18", + "f": 2, + "kind": 2, + "reverse": true, + "grid_bits": 9, + "signed_bits": 24, + "rounding_events": 300, + "max_error_squared_grid": "5/4", + "butterflies": 128 + }, + { + "input_quantized_max_error_squared_grid": "4717/144", + "f": 2, + "kind": 3, + "reverse": false, + "grid_bits": 12, + "signed_bits": 27, + "rounding_events": 428, + "max_error_squared_grid": "613/16", + "butterflies": 192 + }, + { + "input_quantized_max_error_squared_grid": "32/9", + "f": 2, + "kind": 3, + "reverse": true, + "grid_bits": 10, + "signed_bits": 25, + "rounding_events": 172, + "max_error_squared_grid": "5/4", + "butterflies": 192 + }, + { + "input_quantized_max_error_squared_grid": "30553/576", + "f": 3, + "kind": 2, + "reverse": false, + "grid_bits": 13, + "signed_bits": 31, + "rounding_events": 2740, + "max_error_squared_grid": "81/2", + "butterflies": 1536 + }, + { + "input_quantized_max_error_squared_grid": "73/18", + "f": 3, + "kind": 2, + "reverse": true, + "grid_bits": 11, + "signed_bits": 29, + "rounding_events": 2388, + "max_error_squared_grid": "9/4", + "butterflies": 1536 + }, + { + "input_quantized_max_error_squared_grid": "145769/1152", + "f": 3, + "kind": 3, + "reverse": false, + "grid_bits": 15, + "signed_bits": 33, + "rounding_events": 3684, + "max_error_squared_grid": "17153/128", + "butterflies": 2304 + }, + { + "input_quantized_max_error_squared_grid": "32/9", + "f": 3, + "kind": 3, + "reverse": true, + "grid_bits": 12, + "signed_bits": 30, + "rounding_events": 1364, + "max_error_squared_grid": "9/4", + "butterflies": 2304 + } + ], + "one_butterfly_error_patterns": 9, + "controls": [ + "floor differs at -1", + "floor differs at 3", + "wrong_axis", + "wrong_adjoint", + "internal_numerator_overflow", + "domain", + "domain", + "domain" + ] +} diff --git a/research/native-rounded-butterfly-contract/SOURCES.json b/research/native-rounded-butterfly-contract/SOURCES.json new file mode 100644 index 0000000000..2b2b210a17 --- /dev/null +++ b/research/native-rounded-butterfly-contract/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/complex-prefix-native-ports/FULL-INPUT-PORT.md", + "usage": "provenance", + "git_blob": "39a461f2fbf2e009423cd784f56de121d190d842", + "sha256": "52b8462e28f9e87925ccfea27872630e2b2da23f19fd3d2265c2654bc016088c" + }, + { + "path": "research/native-error-channel-amplification/README.md", + "usage": "provenance", + "git_blob": "9e2b0550888c563ae6a0ad42403d45721694b382", + "sha256": "dd32e4ce8d8ca27e72ed55c67fbe6803fbce4bd5f2c848b0219197927db6f02d" + }, + { + "path": "research/native-error-channel-amplification/channels.py", + "usage": "provenance", + "git_blob": "57817c6715c5094583be188b80b6224cf1efd7ed", + "sha256": "a5a9471a2c3061d0e1c88f9633acc50e67922ba4a0577b4063f9a54e049534ce" + }, + { + "path": "research/qq16-native-rounded-components/README.md", + "usage": "provenance", + "git_blob": "5a894aaaa464406b122bf0e183bc6441c207cf70", + "sha256": "0c7c3c6ea4832f08a8006175079b53413285ae516a0c31ade2e696f05bddbe9e" + } + ] +} diff --git a/research/native-rounded-butterfly-contract/TASK.json b/research/native-rounded-butterfly-contract/TASK.json new file mode 100644 index 0000000000..eddf9f7ece --- /dev/null +++ b/research/native-rounded-butterfly-contract/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Concrete fixed-grid C0/C2 rounded completed-call contract and internal range for literal PR4743 forward/reverse ports.", + "scope_change_reason": "Explicit open implementation obligation of the existing source-ordered error-channel analysis; not a new whole-framework audit.", + "bottleneck_link": "Replaces an abstract completed-call tolerance with a constructive internal arithmetic service and explicit nonaccelerated cost.", + "budget_minutes": 60, + "stop_rule": "Complete one uniform rounded backend and source-ordered substitution; do not claim its direct work has the recursive supplier tariff.", + "outcome": "completed", + "evidence": "PROOF.md all-width recurrence and signed width; RESULT.json actual nonzero-rounding calls and all twelve port cases.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation and tests; no independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can an accelerated recursive call satisfy this internal contract?", + "why_it_matters": "The direct O(fN) accuracy backend does not establish an improved multiplication tariff.", + "first_step": "Trace one actual recursive child and all internal rounded cuts.", + "blocked_by": "Accelerated source and complete precision/work contract absent." + }, + { + "question": "Which external sharp fault patterns are realizable?", + "why_it_matters": "Independent defect balls can overstate deterministic attainable error.", + "first_step": "Propagate the exact one-butterfly parity constraint through one complete rounded port.", + "blocked_by": "Full correlated rounding characterization not provided." + } + ] +} diff --git a/research/native-rounded-butterfly-contract/VERIFY.json b/research/native-rounded-butterfly-contract/VERIFY.json new file mode 100644 index 0000000000..fe725ffc98 --- /dev/null +++ b/research/native-rounded-butterfly-contract/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Actual rounded Gaussian calls, complete forward/reverse source ports, internal word checks and deterministic ties against authenticated exact matrix oracle." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Actual rounded Gaussian calls, complete forward/reverse source ports, internal word checks and deterministic ties against authenticated exact matrix oracle." + } + ] +} diff --git a/research/native-rounded-butterfly-contract/rounded.py b/research/native-rounded-butterfly-contract/rounded.py new file mode 100644 index 0000000000..7950580ff7 --- /dev/null +++ b/research/native-rounded-butterfly-contract/rounded.py @@ -0,0 +1,119 @@ +"""Fixed-grid Gaussian calls and literal ports; JoyboyBrian, Codex assistance.""" + + +def need(ok,why): + if not ok:raise ValueError(why) + + +def half_even(n): + q=n>>1 + return q+((n&1)&(q&1)) + + +def checkword(n,width): + need(type(n) is int and -(1<<(width-1))<=n<(1<<(width-1)),'signed word overflow') + return n + + +def call(v,f,axis,width,adjoint=False,trace=None): + need(type(f) is int and f>=1 and axis in (0,2) and len(v)==8**f,'literal Gaussian call dimensions') + need(type(width) is int and width>=2,'word width') + for z in v: + need(len(z)==2,'complex pair') + for value in z:checkword(value,width) + trace=trace if trace is not None else {} + for j in range(f): + bit=3*j+axis; step=1<>1) + if name=='P':y=x^(4 if x&1 else 0); q=x.bit_count()+y.bit_count() + elif name=='Q':y=swap;q=x.bit_count()+y.bit_count() + elif name=='W':y=x;q=2*((x&5).bit_count()%2) + else:y=swap;q=2*((y>>1)&1) + perm.append(y);phase.append(q%4) + return perm,phase + + +def rotate(z,q): + a,b=z + return ((a,b),(-b,a),(-a,-b),(b,-a))[q] + + +def route(name,f,inverse=False): + p,q=letters(name) + if inverse: + back=[0]*8;ph=[0]*8 + for x,y in enumerate(p):back[y]=x;ph[y]=-q[x]%4 + p,q=back,ph + out=[] + for x in range(8**f): + y=z=0 + for j in range(f): + a=(x>>(3*j))&7;y|=p[a]<<(3*j);z+=q[a] + out.append((y,z%4)) + return out + + +def monomial(v,name,f,width,inverse=False): + routing=route(name,f,inverse); seen=bytearray(len(v)) + for start in range(len(v)): + if seen[start]:continue + x=start;saved=v[x] + while True: + seen[x]=1;y,q=routing[x];following=v[y] + v[y]=tuple(checkword(z,width) for z in rotate(saved,q));x=y;saved=following + if x==start:break + # These are owned control fields, explicitly returned zero after use. + for i in range(len(seen)):seen[i]=0;routing[i]=(0,0) + + +def mix(t,y,f,width,sign): + for name,coefficient in [('P',1),('Q',2)]: + monomial(t,name,f,width) + for i,((a,b),(c,d)) in enumerate(zip(t,y)): + ca=checkword(a if coefficient==1 else a<<1,width);cb=checkword(b if coefficient==1 else b<<1,width) + y[i]=(checkword(c+sign*ca,width),checkword(d+sign*cb,width)) + monomial(t,name,f,width,True) + + +def port(x,y,f,kind,reverse,width): + need(kind in (2,3),'two or three calls');x=list(x);y=list(y);trace={};cuts=[] + def paid(v,axis,adj=False): + before=list(v);call(v,f,axis,width,adj,trace);cuts.append((axis,adj,before,list(v))) + if reverse: + if kind==3: + monomial(y,'M',f,width,True);paid(y,2,True);monomial(y,'W',f,width,True) + paid(y,0,True);mix(x,y,f,width,-1);paid(x,0,True) + else: + paid(x,0);mix(x,y,f,width,1);paid(y,0) + if kind==3:monomial(y,'W',f,width);paid(y,2);monomial(y,'M',f,width) + return x,y,trace,cuts + + +def request_bits(P,f,kind,reverse): + need(type(P) is int and P>=0 and type(f) is int and f>=1 and kind in (2,3),'accuracy domain') + if reverse:external=(f+1)//2+2 if kind==2 else f+2 + else:external=f+3 if kind==2 else (3*f+1)//2+3 + return P+external+(f+1)//2+1 + + +def signed_width(H,P,f,kind,reverse): + need(type(H) is int and H>=0,'magnitude domain') + return H+request_bits(P,f,kind,reverse)+2*f+(f+1)//2+9 diff --git a/research/native-rounded-butterfly-contract/source/CHANNELS.md b/research/native-rounded-butterfly-contract/source/CHANNELS.md new file mode 100644 index 0000000000..9e2b055088 --- /dev/null +++ b/research/native-rounded-butterfly-contract/source/CHANNELS.md @@ -0,0 +1,94 @@ +# Sharp source-ordered native-port error channels + +Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. + +## Result and exact interface + +This answers [PR4828](https://github.com/CrocSwap/integer-mult-bounds/pull/4828)'s Open next question2 for the literal [PR4743](https://github.com/CrocSwap/integer-mult-bounds/pull/4743) full-input ports. Sharp Euclidean endpoint conditioning and coordinatewise chronological error propagation are different quantities. Keep every individual tensorized phase letter, two arbitrary independent input banks, and every forward/reverse paid call. Write `L=2^(f/2)` for every integer f>=1. + +Assume independent initial input-coordinate perturbations and an additive complex-coordinate defect after each completed paid call, each of modulus at most rho on that call's actual stored input. Monomial updates, integer mixing and their reverses are exact on the common grid. Then the **exact largest output-coordinate error**, over those abstract independent defect balls and both output banks, is bounded by `E rho`, with these sharp constants: + +| Literal schedule | E(f) | Sufficient completed-call/input tolerance for output2^-P | +| --- | --- | --- | +| two-call forward | `3L^2+4L+1` | `rho=2^(-P-f-3)` | +| three-call forward | `2L^3+4L^2+2L+1` | `rho=2^(-P-ceil(3f/2)-3)` | +| two-call reverse | `L+4` | `rho=2^(-P-ceil(f/2)-2)` | +| three-call reverse | `L^2+L+4` | `rho=2^(-P-f-2)` | + +The original sufficient tolerance `2^(-P-2f-6)` remains valid. These are improved **external completed-call accuracy requests**, not measured word/time savings from a new Gaussian implementation. The abstract independent defects need not all be attainable errors of one concrete rounded algorithm. Sharpness is a property of this explicitly stated error contract; it is not a lower bound on every numerical realization. No paid calls are removed and no new κ is claimed. + +## Actual chronology and defect maps + +Use source `A=C0`, `P=S U S`, `Q=S V01 S`, `W=Z0 Z2`, `M=Z1 V01`, `J=M C2`, `D=J W A`; each subscript f tensors the individual base matrix before addition. In this section suppress f. Source order is + +``` +t = A(x+dx)+e1; +s = A((y+dy)+P t+2Q t)+e2; +u = M(C2 W s+e3) # three-call variant only +``` + +The third defect is immediately after C2 and before M. It cannot be replaced by an identity channel when checking the actual vector error, even though M has coordinate norm1. With `F=A P A+2 A Q A`, `B=D P A+2 D Q A`, the lower-bank maps of the independent error variables are + +| schedule | dx | dy | e1 | e2 | e3 | +| --- | --- | --- | --- | --- | --- | +| forward2 | F | A | `A P+2 A Q` | I | absent | +| forward3 | B | D | `D P+2 D Q` | `J W` | M | + +The upper bank has error `A dx+e1`. There are no products between defects: the maps are linear and every paid-call error is defined against its actual perturbed input. Using a defect guarantee only at an ideal input would change the premise. + +For the reverse3 program, apply M^-1 then C2^-1 to the second input, insert its first defect, apply W^-1 then A^-1 and insert its second defect. Subtract P t and2Q t using the retained first input **before** its final A^-1 call. That last call's defect reaches only the first output. Reverse2 omits the first C2 stage. Thus the lower output channels are + +| schedule | first-input quantization | second-input quantization | first paid defect | second paid defect | third paid defect | +| --- | --- | --- | --- | --- | --- | +| reverse2 | `-(P+2Q)` | A^-1 | I | zero | absent | +| reverse3 | `-(P+2Q)` | D^-1 | `A^-1 W^-1` | I | zero | + +The upper bank is `A^-1 dt+e_last`. An inverse paid call can use the source's forward-call-plus-X realization; its exact monomial merely transports the defect ball and preserves its coordinate tolerance. No optional odd division by15 is executed in these schedules. + +## Uniform norms and sharpness + +For a finite row r of a complex matrix, the induced complex-coordinate norm is `sum_j |r_j|`. Tensor products multiply row1-norms. The following exact eight-coordinate facts follow by multiplying the literal Gaussian-rational source letters. The verifier binds the source declarations and independently reconstructs those matrices; it imports no predecessor checker. + +* A,A^-1,JW,A^-1 W^-1 have flat rows of1-norm sqrt2; D,D^-1 have flat rows of1-norm2; P,Q,M are monomial. +* The two separately tensorized branches of F have flat row1-norm2, those of AP+2AQ have flat branch norm sqrt2, those of DP+2DQ have flat branch norm2, and those of P+2Q have flat branch norm1. +* B's first branch `D P A` has flat row norm sqrt2; its second branch `D Q A` has flat row norm sqrt8, as checked directly from the literal matrices. The source residual identity names another monomial M; it differs from this note's post-call `M=Z1 V01` and is not substituted here. Neither branch statement tensors the sum B. +* In base row0, every overlapping nonzero entry of each listed branch pair has the same complex phase: `x_j conjugate(y_j)` is positive real. This includes B's unequal-magnitude branches. + +The triangle inequality therefore gives the uniform upper bounds + +``` +||F_f||inf=3L^2, ||A_f P_f+2A_f Q_f||inf=3L, +||B_f||inf=2L^3+L, ||D_f P_f+2D_f Q_f||inf=3L^2, +||P_f+2Q_f||inf=3. +``` + +The equalities are attained by row `(0,...,0)`: entrywise same-phase overlap is preserved by products under tensorization, including support intersections, so the triangle inequality is exact there for every f. All the other single-unitary channels have their stated flat row norm. The proof is an application of explicit finite base identities and tensor functoriality, not extrapolation from the later width1/2/3 tests. + +For independent coordinate errors, concatenate all channel matrices horizontally. Its induced norm is the maximum, over output rows, of the sum of all channel row1-norms. Every channel above attains its own bound at the same row0, so summing gives the asserted E. For a sharpness witness, independently set each error coordinate to rho times the conjugate phase of its channel's row0 entry (zero entries may receive0). Every summand then points along the positive real axis and attains E rho. The two banks' upper error constant is only L+1, smaller than the lower-bank total. The mathematical witnesses can use eighth roots of unity; the finite execution tests use exact Gaussian-rational perturbations and do not claim that a dyadic quantizer necessarily generates every sharpness witness. + +## Guard consequence and retained costs + +Since f>=1, L>=sqrt2. Dividing forward2/forward3 constants by L^2/L^3 gives respectively at most `7/2+2sqrt2<8` and `3+(9/4)sqrt2<8`. Reverse2/reverse3 divided by L/L^2 are at most `1+2sqrt2<4` and `3+1/sqrt2<4`. Rounding the exponent upward yields the four stated dyadic tolerances with strict output margin. The checker uses rational squared comparisons, not floating logarithms. These guards are sufficient; the exact minimal dyadic guard can instead be selected by the explicit E table, and no optimality of the integer constants3/2 is claimed. + +The original conservative intermediate allowance `2^(H+2f+4)` for inputs of magnitude2^H remains sufficient: at most three Gaussian stages contribute at most L^3, the one mixed update contributes total coefficient3, and all new tolerances are at most1/8 for H,P>=0. Writing M0=2^H, the forward stages are bounded by `(3L^3+L^2)M0+(3L^3+4L^2+L+1)rho` and the reverse stages by `(L^2+3)M0+(L^2+L+4)rho` (the smaller two-call cases fit these envelopes). Each is below `8L^3 M0 <= 2^(H+2f+3)`. The looser original allowance therefore accommodates the perturbed states. Exact free monomial/scalar passes and their existing owned address workspace remain charged as in #4743. The Gaussian implementation's internal-prefix guard, internal error guarantee and execution cost are additional; this package neither installs nor prices one. It also does not price complete recursive substitution, general nonunitary encodings, full supplier/outer transfer or physical tapes. + +Research decision: stop at the actual error interface. Inherited paid/source/ownership/native contracts keep their status; source-ordered amplification and a sharper completed-call tolerance are established here; physical implementation and recursive consequences remain open. This is a focused precision obligation and does not reopen a fixed-word paid-saving search. + +## Evidence and reproduction + +Generated `RESULT.json` records12cases (two/three calls, forward/reverse, f1/2/3),54exact dirty perturbed trajectories and144independent impulse columns at width1. Exact row norms and row0 sharpness are checked at every row of the bounded lifted matrices. A separately executed chronological vector program agrees with the independent error maps. Six controls reject unsupported width, wrong phase family, wrong defect order, a false cap, dropping the third defect's post-call monomial and unsupported entry-angle assumptions. Complete typed receipt comparison rejects altered fields and bool/int substitutions. Normal and optimized commands use only CPython3.12 standard library. + +``` +python3.12 -B scripts/research_package.py --package research/native-error-channel-amplification +python3 -B scripts/check_research_commit.py --package research/native-error-channel-amplification --check-source-history +``` + +The official committed export can execute `verify.py` directly with `-I -W error -B`, and separately `-O`, without Git/network. `--emit NEW_PATH` writes a new deterministic receipt and refuses overwrite. Source pins bind the exact base and retained source bytes. Hosted CI is unverified at publication. + +Base canonical main `bee95ce88f9f19802f0613f92838895cd0e14a1f`, priority7, selected conditional κ0.00302015 unchanged. Entry overlap at06:05–06:06UTC October23 covered310openPRs,4096Discussion records and6690base notes with complete reported pagination/inventory. Related #4828/#4743, shared-port/cascade and later compensated-port work were distinguished. Coverage is advisory, not novelty proof; arbitrary diffs and unpublished work remain outside it. Canonical claim: https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19139368. + +Credit Nick Petalas #4828 for sharp endpoint conditioning and the explicit error-channel question; Dugongue #4743 for literal all-input schedules and conservative precision contract; Yiyang/Lyy-iiis #4710 for repaired phases; lee-phys #4688, Jacob Alan Sussman #4628, eumemic, Swapnil Jain and all notices retained in those packages. No source archive is modified or reissued. No independent human or formal proof-kernel acceptance is claimed. + +## Open next questions + +Can one concrete rounded Cj_f implementation meet these completed-call tolerances on each actual stored input with its internal range, data-grid, movement and time costs retained? Begin with one nonzero-rounding invocation and compare its actual radius/tolerance to the table. The sharp external contract supplies no internal Gaussian guarantee. Complete recursive substitution requires its own error-channel composition and is outside this package. Structured question: TASK.json. diff --git a/research/native-rounded-butterfly-contract/source/FULL-INPUT-PORT.md b/research/native-rounded-butterfly-contract/source/FULL-INPUT-PORT.md new file mode 100644 index 0000000000..bc713d82db --- /dev/null +++ b/research/native-rounded-butterfly-contract/source/FULL-INPUT-PORT.md @@ -0,0 +1,86 @@ +# Reversible two-call and three-call full-input triangular ports + +Prepared for Dugongue with substantial OpenAI Codex assistance. This is an exact, all-width native building block on two arbitrary independent input arrays. It does not claim an improved complete supplier or multiplication exponent. + +## Leading two-call theorem + +Let A_f = C0_f and L_f = P_f + 2 Q_f, with the individually tensorized phase letters pinned below. For two arbitrary independent initial registers (x,y), execute + + t <- A_f x, + y <- y + P_f t + 2 Q_f t, + s <- A_f y. + +Only the first and last lines are paid calls. The complete output is + + (t,s) = (A_f x, A_f y + A_f L_f A_f x). + +This is an actual dirty-target extension of the predecessor prefix: replace its initial copy by additive injection into the existing target. To implement a term P_f t using only per-register maps and ordinary mixing, apply P_f to t, add it into y, and restore t using P_f inverse; do the same for Q_f. No original y value is overwritten and no hidden clean copy is needed. + +The exact two-call block and its inverse are + + F_f = A_f L_f A_f, + U_f = [[A_f, 0], [F_f, A_f]], + U_f inverse = [[A_f inverse, 0], [-L_f, A_f inverse]]. + +The reverse program applies A_f inverse to s, subtracts the two separately applied monomial terms using retained t, and applies A_f inverse to t. Thus it costs exactly two inverse paid calls, each equivalent to one forward paid call plus a free X0_f. Both block multiplication orders verify the inverse. This result is valid for arbitrary x and y and every positive f. + +There is also an explicit free inverse for the coupling L_f. Set R_f = P_f inverse Q_f. The actual predecessor letters satisfy R^4 = I, hence R_f^4 = I. Then + + L_f inverse = -(I - 2 R_f + 4 R_f^2 - 8 R_f^3) P_f inverse / 15. + +Multiplying by P_f(I + 2 R_f) proves the formula. Every summand is applied separately; the four-term sum is never tensorized as one letter. The fixed denominator 15 requires explicitly charged fixed-precision scalar arithmetic for numerical execution. Since R_f is unitary with fourth-root-of-unity spectrum, L_f has singular values between 1 and 3. In addition, every R_f power times P_f inverse is monomial, so the explicit formula gives infinity norm(L_f inverse) <= (1 + 2 + 4 + 8)/15 = 1 uniformly in f. The forward and reverse two/three-call schedules do not execute this division by 15; it is an optional coupling inverse. If that optional inverse is used numerically, its fixed odd division and rounding must be charged explicitly, for example by ordinary bounded-word DIV with a sufficient common-grid guard. This well-conditioned free coupling is concrete controller material, rather than an unknown gadget or an inverse asserted from a numerical rank. + +The two-call block is a product of unitary layers and the shear (t,y) -> (t,y + L_f t). Its norm and inverse norm are at most 4, so its condition number is at most 16 uniformly in f. The three-call block below is this same block followed by another unitary layer, and inherits the identical bound. + +## Constructive full-input theorem + +Use the actual base letters and phases of the pinned PR #4710 residual identity, with notation as in SECTOR-COMPLETION.md. At every positive width f, each individual letter G_f means G raised to its f-fold tensor power. Put + + A_f = C0_f, + L_f = P_f + 2 Q_f, + D_f = J_f W_f C0_f, + B_f = M_f C2_f + 2 K_f a_f. + +For arbitrary independent complex arrays x and y of length N = 8^f, the following exact program uses three paid rank-one calls: + +1. Replace x by t = C0_f x. This is the first paid call. +2. Add P_f t and 2 Q_f t into the existing y register, obtaining y + L_f t. Each summand is a separately applied free monomial. The original y is retained additively; no zero-scratch precondition is used. +3. Apply C0_f to the second register. This is the second paid call. +4. Apply W_f and J_f to that register. Only the C2_f inside J is paid, giving the third call. + +The resulting two-register output is exactly + + (t,u) = (C0_f x, D_f y + B_f x). + +Indeed u = D_f y + J_f W_f C0_f (P_f + 2 Q_f) C0_f x, and the pinned predecessor identities, tensorized separately before addition, identify the two x summands with M_f C2_f x and 2 K_f a_f x. Nothing tensors the sum P + 2 Q as a single matrix. Absolute Pauli phases remain those of the source. + +The three-call map is invertible at every width. Its explicit reverse schedule is: apply J_f inverse, W_f inverse and C0_f inverse to u, subtract P_f t and 2 Q_f t, and apply C0_f inverse to t. This recovers exactly (x,y), with no borrowed copy. Each inverse Cj_f uses one forward paid call followed by Xj_f, since Cj inverse = Xj Cj on the actual base letters. Thus the reverse also uses three paid calls. In block form the forward and inverse are + + [[A_f, 0], [D_f L_f A_f, D_f]] + and [[A_f inverse, 0], [-L_f, D_f inverse]]. + +Both multiplication orders give the identity by literal block multiplication. This is a sufficient all-input implementation, not a rank-only test or a subspace assertion. + +## Conditioning, native work and precision + +Each paid Gaussian letter and each free monomial is unitary. The whole program is a product of unitary block-diagonal layers and the shear + + S_f(t,y) = (t, y + L_f t). + +As the two free terms in L_f have unitary Euclidean norm, norm(L_f) <= 3. Writing S_f = I + N_f, with N_f squared zero, gives norm(S_f) <= 4 and norm(S_f inverse) <= 4. Consequently both the complete forward operator and its inverse have Euclidean operator norm at most 4, and their condition number is at most 16, independently of f. This statement concerns the complete two-bank map, without discarding either output. + +For an explicit coordinatewise native error budget, let complex input magnitudes be at most 2^H and request coordinate error at most 2^(-P), where H,P >= 0. Let each charged Gaussian call return its exact transform of the stored input with error at most rho per coordinate, and quantize the original inputs with error at most rho. Set L = 2^(f/2), bounding the infinity norm of any Cj_f. Free monomials, integer scalings, copies and additions can be exact on the common grid. The first call's error contributes at most 3 L^2 rho to u, the second at most L rho, and the third at most rho. Initial input errors contribute at most (3 L^3 + L^2) rho to u. Thus the conservative bound 10 L^3 rho covers both output arrays. Taking rho = 2^(-(P + 2 f + 6)) gives error below 2^(-P), since L^3 <= 2^(2 f) and 10/64 < 1. Any chosen Gaussian implementation's internal guard and time costs are separately charged; this theorem does not assume an unproved fast oracle. + +Intermediate magnitudes are below 2^(H + 2 f + 4), including these errors. P + H + 4 f + 12 signed bits per real or imaginary coordinate suffice for the displayed arithmetic. If f = O(log p), H,P = O(p) and p = Theta(log n), this occupies a fixed number of ordinary C log n-bit words, for sufficiently large fixed C. No unbounded-word multiplication or whole-array unit instruction is used. + +The address/phase odometer and explicit in-place permutation implementation in SECTOR-COMPLETION.md implement every displayed free map and mixed update in O(N) ordinary word operations. O(N) owned address workspace, or one separately owned work field, is initialized and restored in O(N) stores. These are charged native resources, not additional independent productive inputs. The theorem therefore supplies three paid calls plus O(N) native work, with two arbitrary input banks and explicitly accounted workspace. + +## How to use the port without changing its claim + +A controller may now wire this full-input block into a larger exact block identity, preserving both diagonal channels and the actual rank-three off-diagonal term. This differs from the clean-prefix presentation because the second initial array is arbitrary and its D_f y contribution is explicit. A claimed complete saving must show the actual subsequent block operations, canonical independent outputs, restored owners and total paid calls. This port alone has diagonal ranks one and two and does not establish a three-rank target for both independent arrays. Discarding D_f y, assuming it is initially zero, or counting B_f x as an independent additional Gaussian job would change the theorem. + +## Evidence and predecessor credit + +verify_full_input_port.py uses the pinned exact Gaussian-rational engine to verify both predecessor word identities, both full-input triangular blocks, both inverse multiplication identities, the order-four free coupling inverse and the one-call implementation of paid inverses. It rejects the false claim that the second output is independent of an arbitrary y. Separately tensorized word algebra proves all widths; the finite checks do not infer universal correctness from a few dimensions. + +Credit Yiyang / Lyy-iiis, PR #4710 (b0d5192390af493d626054b060921895df3c94d2), for the repaired phase prefix and residual identity; lee-phys, PR #4688 (264c4b3cb13c82d171de352ecf60486dfb8d2bd4), for the original prefix and rank engine; and Jacob Alan Sussman, PR #4628 (ee4fd87f064017c23e5a86fc1dcfe0a5237caed3), for the complex engine model and small-unit problem. Retain their notices and earlier attribution. This full-input additive schedule, reverse interface and uniform norm bound are the present extension. No worldwide novelty or independent human review is claimed. Exact source URLs and SHA-256 pins appear in SOURCE-PINS.json. diff --git a/research/native-rounded-butterfly-contract/source/QQ16-ROUNDING.md b/research/native-rounded-butterfly-contract/source/QQ16-ROUNDING.md new file mode 100644 index 0000000000..5a894aaaa4 --- /dev/null +++ b/research/native-rounded-butterfly-contract/source/QQ16-ROUNDING.md @@ -0,0 +1,181 @@ +# Concrete component rounding in the native QQ16 F0 reference + +Arham Tahir's [PR3036](https://github.com/CrocSwap/integer-mult-bounds/pull/3036) +leaves open whether its two deterministic scalar rounding errors survive the +physical native maps. **They do for the finite reference lowering specified +below.** All 480 borrowed helpers restore as numerical values, yet a unit data +input is lost. No freely chosen fault is injected. + +The new evidence includes the native butterfly interiors, adapters, residual +wrappers and all eight additional native lines. The source's recursive child +tariff is not assigned to this direct finite implementation. There is no new +supplier or kappa claim. + +## Finite statement and operation order + +Use the pinned joint-query `programs.F_0`, including the literal forward core, +on 712 fields of 512 complex coordinates. Let `1` be the unnormalized real +constant payload. Initialize + +``` +L112 = Y0 = 1; L224 = 2^65 * 1; all other fields = 0. +``` + +Here L0..L111 are X, L112..L223 are Y, L224..L703 are dirty helpers, +and C0..C7 are private fields. L224 has ordinary frame endpoints `(0,1)`. +The exact reference returns this entry unchanged. + +Each real component uses binary round-to-nearest, ties-to-even, with 53 +significand bits. Scalar ADD means **separate rounded multiplication and ADD**. +Scalar coefficients are checked to be exactly representable. A native recipe +is its serialized right monomial, coordinate Gaussian lines in increasing +axis order, then its left monomial, including global phase. Monomials perform +signed coordinate permutations and real/imaginary exchanges. Phase tags in +the event stream are control labels, following the source semantics. + +For each disjoint complex pair `(a+ib,c+id)`, a positive Gaussian line uses +this pair-first real lowering, rounding each displayed sum/difference: + +``` +rp = RN(a+c); ip = RN(b+d); rd = RN(a-c); id = RN(b-d) +out0 = (RN(rp-id)/2, RN(ip+rd)/2) +out1 = (RN(rp+id)/2, RN(ip-rd)/2) +``` + +Division by two is exact on this execution. The operation order is part of +the claim. CLEAR applies only to owned private fields. Zero-valued child +inputs may be skipped by the interpreter because every primitive maps zero +exactly to zero; this is an execution shortcut, not a cost saving claim. + +Under this lowering the final numerical values are + +``` +Y0 = 0 +Y2 = Y25 = Y78 = Y99 = -1/2 * 1 +L224 = 2^65 * 1 +all other outputs = 0. +``` + +The maximum data-field Hilbert error is `sqrt(512)`, equal to the entry +data-field norm. Every physical helper returns its entry value and every +private output is zero. Signed-zero bit patterns are not compared. + +Exactly two completed scalar ADD sites round, at unfiltered zero-based +expanded events **3887 and 4060**, each on 512 real components. At both cuts +the actual native target/source vectors are `(1/2 * 1, 2^65 * 1)` and the +coefficient is `-1/2`. Thus each real component rounds +`-2^64 + 1/2` to `-2^64`, losing `1/2`. These are deterministic arithmetic +decisions. Every native butterfly's internal operation and every scalar +multiplication is exact on the resulting trajectory. + +## Evidence and source binding + +[RESULT.json](RESULT.json) is recomputed by a shared-exponent integer-vector +interpreter. Rounding discards low significand bits with an explicit signed +nearest-even decision; dyadic denominators are exact and exponents unbounded. +All observed nonzero primitive binary exponents lie in `[-2,67]`, checked +inside the normal finite binary64 range. This witness needs neither underflow +nor overflow. + +A second engine uses actual Python binary64 scalar multiplication/ADD and +separately written float Gaussian butterflies and complex phase rotations. +The engines agree at **all 26,089 changed-field cuts** of the complete +26,099-event program and all **364,544 complex endpoint amplitudes**. The +cut comparison uses canonical exact dyadic-vector hashes; the complete final +vectors and both marked operand pairs are compared directly. Both engines +share the source event dispatcher and the credited monomial index table. +This is arithmetic corroboration, not an independent audit of every source +recipe or its Clifford theorem. + +Exact arithmetic, 65-bit precision on the same dirty input, and removal of +the dirty input all recover the correct native endpoint with no rounding. +The wider control is a sufficient escape for this input, not a general +precision bound or minimum. + +Seven behavioral groups check 36,882 decisions against an enumerated finite +binary system, 5,008 integer decisions against hardware binary64, Gaussian +basis columns, a changed literal ADD, a used native global-phase mutation, +and scientific-input, receipt and primitive-source corruption. Both positive +fixtures and actual failing variants are exercised. + +Source commits, Git blobs, archive-member hashes and the unchanged vendored +primitive evaluator are recorded in [SOURCES.json](SOURCES.json). The two +external scientific inputs are declared for invalidation in +[VERIFY.json](VERIFY.json). The selected record and catalogue are historical +provenance. Frozen predecessor packages and the selected frontier are unchanged. + +## Reproduce + +From the repository root, with standard-library Python 3.12: + +```sh +python3.12 -Werror -I -B scripts/research_package.py \ + --package research/qq16-native-rounded-components +``` + +Expected marker: `PASS_QQ16_NATIVE_ROUNDED_COMPONENTS`, seven passing +behavioral groups, then `PASS_REGISTERED_RESEARCH_PACKAGE`. Replay is read-only; +`verify.py --write PATH` only creates an absent receipt. Direct `verify.py` and +`test_verify.py` also work in a source export containing the package and its +two declared inputs. See TASK.json for the actual task and verification status. + +## Consequence and limits + +The scalar-rounding handoff is resolved for one explicit finite native +lowering. Exact dirty restoration alone still does not imply data accuracy, +even when the errors come from actual correctly rounded component operations. +[PR2965](https://github.com/CrocSwap/integer-mult-bounds/pull/2965)'s conditional +completed-output transfer remains unchanged; producer tolerances are its premises. + +This checks the retained 512-coordinate native recipes under their inherited +local chart/access interpretation. It proves no all-depth tensor statement, +arbitrary-input error estimate, child-tariff implementation, exact signed-zero +restoration, owner routing or physical machine/tape/storage bound. It neither +audits B1/the decoder nor supplies a paid consumer, complete supplier, selected +cold replay, formal-kernel proof or multiplication theorem. Other numerical +lowerings and common grids can avoid the loss. + +Family decision: **narrow and stop** after this local numerical implication. +The direct finite numerical bill is not a favorable complete recursive invoice. +Native recursive cost, physical movement/storage, dirty-range policy, B1, +consumer and supplier admission remain additional or unknown; unknowns are +not assigned zero cost. No downstream implementation campaign is proposed. + +## Open next questions + +Can a pinned finite native producer meet the required completed-output tolerance +with an explicit dirty-input bound and grid/precision policy? Start by deriving +its all-cut component magnitudes and exact-cancellation rules, then charge the +native children, layout/movement, workspace/restoration and actual consumer. +This matters because the output-error theorem assumes producer accuracy; the +missing complete numerical/physical caller contract blocks supplier adoption. +The structured handoff is in [TASK.json](TASK.json). Local registered replay +on Linux / CPython 3.12.14 passes; hosted CI is separate. + +## Credit + +Prepared by **Sricharan Vagvala (@theon199), with substantial OpenAI Codex +assistance**. New interpreter, audit, controls and prose are Apache-2.0. No +independent human review, hosted CI pass or formal-kernel review is claimed. + +Credit **Arham Tahir / PR3036** at `3717c1e684553c57bc73300410df65438a9ef095` +for the concrete scalar witness, two sites and numerical-conjugacy handoff; +**Tekalign (@tekuuu) / PR3017** at `0f493f4c264fbc70ee14364b68af260d858c143c` +for the native semantics, exact vector primitives and member pins. The +180-line [vendor/native.py](vendor/native.py) is reused byte-for-byte with its +author/license retained; it is a working dependency, not new independent +native-semantic evidence. Credit Nick Petalas / PR2965, Arham Tahir / PR2995, +Ali Romman and the QQ16 team, Sagar Thakrar, DLamdata, ywz65, starship-s, +Ross Richardson, Douglas Colkitt and the retained supplier/native/scalar lineage +in the [original notice](../joint-query/NOTICE.md). + +## Publication handoff + +The verified numerical code and receipt are public at fork commit +[`946a399d6ae1667236bb395d21c33c749e000877`](https://github.com/theon199/integer-mult-bounds/commit/946a399d6ae1667236bb395d21c33c749e000877). +The [contribution branch](https://github.com/theon199/integer-mult-bounds/tree/research/qq16-native-rounded-audit) +may add publication-status documentation only. GitHub denied both PR creation +and Discussion posting with `Resource not accessible by integration`; no PR +or public CLAIM was created. The result is complete for its stated finite +scope and released. A maintainer can review the public artifact or open the +[fork comparison](https://github.com/CrocSwap/integer-mult-bounds/compare/main...theon199:research/qq16-native-rounded-audit?expand=1). diff --git a/research/native-rounded-butterfly-contract/source/channels.py b/research/native-rounded-butterfly-contract/source/channels.py new file mode 100644 index 0000000000..57817c6715 --- /dev/null +++ b/research/native-rounded-butterfly-contract/source/channels.py @@ -0,0 +1,167 @@ +"""Exact source-ordered defect maps; independent Gaussian-rational arithmetic. + +JoyboyBrian, substantial OpenAI Codex assistance; Apache-2.0. +""" +from fractions import Fraction as Q + +ZERO=(Q(0),Q(0)); ONE=(Q(1),Q(0)); PHASES=(ONE,(Q(0),Q(1)),(-Q(1),Q(0)),(Q(0),-Q(1))) + + +def need(ok, why): + if not ok: raise ValueError(why) + + +def add(a,b): return a[0]+b[0],a[1]+b[1] +def mul(a,b): return a[0]*b[0]-a[1]*b[1],a[0]*b[1]+a[1]*b[0] +def scale(c,a): return c*a[0],c*a[1] +def conj(a): return a[0],-a[1] + + +def eye(n=8): return [{i:ONE} for i in range(n)] + + +def put(row,j,z): + z=add(row.get(j,ZERO),z) + if z==ZERO: row.pop(j,None) + else: row[j]=z + + +def plus(a,b,c=1): + out=[dict(row) for row in a] + for row,source in zip(out,b): + for j,z in source.items(): put(row,j,scale(c,z)) + return out + + +def product(a,b): + out=[{} for row in a] + for i,row in enumerate(a): + for k,x in row.items(): + for j,y in b[k].items(): put(out[i],j,mul(x,y)) + return out + + +def word(*matrices): + out=eye(len(matrices[0])) + for a in matrices: out=product(out,a) + return out + + +def adjoint(a): + out=[{} for row in a] + for i,row in enumerate(a): + for j,z in row.items(): out[j][i]=conj(z) + return out + + +def monomial(perm,phases=None): + phases=phases or [0]*len(perm) + need(sorted(perm)==list(range(len(perm))),'monomial bijection') + out=[{} for i in perm] + for j,i in enumerate(perm): out[i][j]=PHASES[phases[j]%4] + return out + + +def pauli(x,z): + return monomial([j^x for j in range(8)],[(x&z).bit_count()+2*(j&z).bit_count() for j in range(8)]) + + +def letters(): + C=[plus([{i:(Q(1,2),Q(1,2))} for i in range(8)], + [{i^(1<=0 and y>=0: return True + if x<=0 and y<=0: return x==y==0 + return x*x>=2*y*y if x>=0 else 2*y*y>=x*x + + +def Lpower(k): + return (Q(1<< (k//2)),Q(0)) if k%2==0 else (Q(0),Q(1<<(k//2))) + + +def pair_sum(*parts): return tuple(sum(z[i] for z in parts) for i in (0,1)) +def pair_scale(c,a): return c*a[0],c*a[1] + + +def maps(base,f,kind,reverse=False): + A,P,T,D,J,W,M,I=(base[k] for k in ('A','P','Q','D','J','W','M','I')) + def lifted(*terms): + out=[{} for i in range(8**f)] + for c,a in terms: out=plus(out,power(a,f),c) + return out + if reverse: + cols=[lifted((-1,P),(-2,T)),lifted((1,adjoint(A if kind==2 else D)))] + cols += ([lifted((1,I))] if kind==2 else + [lifted((1,word(adjoint(A),adjoint(W)))),lifted((1,I))]) + cols.append(None) + return cols + B=A if kind==2 else D + cols=[lifted((1,word(B,P,A)),(2,word(B,T,A))),lifted((1,B)), + lifted((1,word(B,P)),(2,word(B,T)))] + cols.append(lifted((1,I if kind==2 else word(J,W)))) + if kind==3: cols.append(lifted((1,M))) + return cols + + +def schedule(base,f,kind,reverse,x,y,defects): + lifted={k:power(v,f) for k,v in base.items()} + A,P,T,W,M,C2=(lifted[k] for k in ('A','P','Q','W','M','C2')) + dx,dy,*e=defects; x=vplus(x,dx); y=vplus(y,dy) + if not reverse: + t=vplus(apply(A,x),e[0]); z=vplus(y,apply(P,t)); z=vplus(z,apply(T,t),2) + out=vplus(apply(A,z),e[1]) + if kind==3: out=apply(M,vplus(apply(C2,apply(W,out)),e[2])) + return t,out + if kind==3: + out=vplus(apply(adjoint(C2),apply(adjoint(M),y)),e[0]) + out=vplus(apply(adjoint(A),apply(adjoint(W),out)),e[1]) + else: out=vplus(apply(adjoint(A),y),e[0]) + out=vplus(vplus(out,apply(P,x),-1),apply(T,x),-2) + return vplus(apply(adjoint(A),x),e[-1]),out diff --git a/research/native-rounded-butterfly-contract/source/pins.json b/research/native-rounded-butterfly-contract/source/pins.json new file mode 100644 index 0000000000..a8623f18fd --- /dev/null +++ b/research/native-rounded-butterfly-contract/source/pins.json @@ -0,0 +1,6 @@ +{ + "CHANNELS.md": "dd32e4ce8d8ca27e72ed55c67fbe6803fbce4bd5f2c848b0219197927db6f02d", + "channels.py": "a5a9471a2c3061d0e1c88f9633acc50e67922ba4a0577b4063f9a54e049534ce", + "FULL-INPUT-PORT.md": "52b8462e28f9e87925ccfea27872630e2b2da23f19fd3d2265c2654bc016088c", + "QQ16-ROUNDING.md": "0c7c3c6ea4832f08a8006175079b53413285ae516a0c31ade2e696f05bddbe9e" +} diff --git a/research/native-rounded-butterfly-contract/verify.py b/research/native-rounded-butterfly-contract/verify.py new file mode 100644 index 0000000000..0c1bf1ac41 --- /dev/null +++ b/research/native-rounded-butterfly-contract/verify.py @@ -0,0 +1,110 @@ +"""Source-authenticated rounded execution against retained exact matrix arithmetic.""" +import hashlib,itertools,json,sys +from fractions import Fraction as Q +from pathlib import Path +P=Path(__file__).resolve().parent +sys.path.insert(0,str(P));sys.path.insert(0,str(P/'source')) +import rounded as r +c=None + + +def norm2(z):return z[0]*z[0]+z[1]*z[1] + + +def error2(a,b):return max(norm2(c.add(x,c.scale(-1,y)))for x,y in zip(a,b)) + + +def reference(x,y,f,kind,reverse): + letters={k:c.power(v,f)for k,v in c.letters().items()} + A,C2,Pm,Qm,W,M=(letters[k] for k in ('A','C2','P','Q','W','M')) + if reverse: + if kind==3:y=c.apply(c.adjoint(M),y);y=c.apply(c.adjoint(C2),y);y=c.apply(c.adjoint(W),y) + y=c.apply(c.adjoint(A),y);y=c.vplus(y,c.apply(Pm,x),-1);y=c.vplus(y,c.apply(Qm,x),-2);x=c.apply(c.adjoint(A),x) + else: + x=c.apply(A,x);y=c.vplus(y,c.apply(Pm,x));y=c.vplus(y,c.apply(Qm,x),2);y=c.apply(A,y) + if kind==3:y=c.apply(W,y);y=c.apply(C2,y);y=c.apply(M,y) + return x,y + + +def oracle_round_half(n): + value=Q(n,2);lower=value.numerator//value.denominator;upper=lower+1 + return min((lower,upper),key=lambda a:(abs(Q(a)-value),a%2)) + + +def verify(): + pins=json.loads((P/'source/pins.json').read_text()) + for name,h in pins.items():r.need(hashlib.sha256((P/'source'/name).read_bytes()).hexdigest()==h,'source hash '+name) + for n in range(-10001,10002):r.need(r.half_even(n)==oracle_round_half(n),'signed nearest-even half') + global c + import channels as c + base=c.letters() + for name in ('P','Q','W','M'): + p,q=r.letters(name);r.need(c.monomial(p,q)==base[name],'source monomial phase') + rounding=0;cases=[];calls=0 + for f in (1,2,3): + N=8**f + for axis in (0,2): + for adj in (False,True): + mat=c.power(base['A' if axis==0 else 'C2'],f) + if adj:mat=c.adjoint(mat) + for seed in range(3): + src=[((17*i+seed)%23-11,(7*i+3*seed)%19-9)for i in range(N)] + out=list(src);tr={};r.call(out,f,axis,32,adj,tr) + exact=c.apply(mat,[(Q(a),Q(b))for a,b in src]) + # eta_f < 2*2^(f/2) grid units, proved in PROOF. + r.need(error2(out,exact)<4*(2**f),'actual completed-call defect bound') + r.need(tr['butterflies']==f*N//2,'literal paid-call work') + rounding+=tr['rounding_events'];calls+=1 + for kind in (2,3): + for reverse in (False,True): + precision=4;g=r.request_bits(precision,f,kind,reverse);width=r.signed_width(1,precision,f,kind,reverse) + # Tiny grid-residue plus a macroscopic dirty component exercises nonzero rounding. + x=[((i%5-2)*(1<<(g-2))+(i%3), (i%7-3)*(1<<(g-3))+1)for i in range(N)] + y=[((i%3-1)*(1<<(g-2))+1,(i%5-2)*(1<<(g-3))-(i%2))for i in range(N)] + a,b,tr,cuts=r.port(x,y,f,kind,reverse,width) + exact=reference([(Q(s),Q(t))for s,t in x],[(Q(s),Q(t))for s,t in y],f,kind,reverse) + err=max(error2(a,exact[0]),error2(b,exact[1])) + r.need(err<=Q(1<<(2*g),1<<(2*precision)),'full port target on actual rounded execution') + for axis,adj,before,after in cuts: + mat=c.power(base['A' if axis==0 else 'C2'],f) + if adj:mat=c.adjoint(mat) + r.need(error2(after,c.apply(mat,before))<4*2**f,'defect against actual stored input') + original_x=[(Q(s)+Q(1,3),Q(t)-Q(1,3)) for s,t in x] + original_y=[(Q(s)-Q(1,3),Q(t)+Q(1,3)) for s,t in y] + ideal=reference(original_x,original_y,f,kind,reverse) + err_original=max(error2(a,ideal[0]),error2(b,ideal[1])) + r.need(err_original<=Q(1<<(2*g),1<<(2*precision)),'input quantization plus actual call defects') + cases.append(dict(input_quantized_max_error_squared_grid=str(err_original),f=f,kind=kind,reverse=reverse,grid_bits=g,signed_bits=width,rounding_events=tr['rounding_events'],max_error_squared_grid=str(err),butterflies=tr['butterflies'])) + # First exact reachable rounding defect and a non-independent error-channel constraint. + unit=[(0,0)]*8;unit[0]=(1,0);lost=list(unit);r.call(lost,1,0,8) + r.need(lost==[(0,0)]*8,'deterministic half-grid loss witness') + patterns=set() + for a,b,d,e in itertools.product(range(-2,3),repeat=4): + v=[(0,0)]*8;v[0]=(a,b);v[1]=(d,e);out=list(v);r.call(out,1,0,8) + exact=c.apply(base['A'],[(Q(x),Q(y))for x,y in v]) + defect=tuple(2*(Q(out[j][k])-exact[j][k])for j in (0,1)for k in (0,1)) + patterns.add(defect) + r.need(all(z==0 for z in defect) or all(abs(z)==1 for z in defect),'four component ties share parity') + # A coordinate error in only one real component is admitted by a ball but impossible here. + r.need((Q(1),Q(0),Q(0),Q(0)) not in patterns,'independent fault not realizable') + controls=[] + for n in (-3,-1,1,3): + if (n>>1)!=r.half_even(n):controls.append('floor differs at '+str(n)) + v=[(0,0)]*8;v[0]=(2,1);a=list(v);b=list(v);r.call(a,1,0,16);r.call(b,1,2,16) + r.need(a!=b,'wrong actual C2 axis rejected');controls.append('wrong_axis') + b=list(v);r.call(b,1,0,16,True);r.need(a!=b,'wrong adjoint rejected');controls.append('wrong_adjoint') + try:r.call([(7,7)]*8,1,0,4) + except ValueError:controls.append('internal_numerator_overflow') + else:raise ValueError('overflow accepted') + for args in [(0,0,2,False),(-1,1,2,False),(0,1,4,False)]: + try:r.request_bits(*args) + except ValueError:controls.append('domain') + else:raise ValueError('invalid precision contract accepted') + r.need(rounding>0 and all(x['rounding_events']>0 for x in cases),'nonzero rounding coverage') + return dict(status='PASS_NATIVE_ROUNDED_BUTTERFLY_CONTRACT',half_rounding_cases=20003,completed_calls=calls,nonzero_call_roundings=rounding,port_cases=cases,one_butterfly_error_patterns=len(patterns),controls=controls) + +if __name__=='__main__': + result=verify() + if '--write' in sys.argv:(P/'RESULT.json').write_text(json.dumps(result,indent=2)+'\n') + else:r.need(json.dumps(result,sort_keys=True)==json.dumps(json.loads((P/'RESULT.json').read_text()),sort_keys=True),'receipt mismatch') + print(result['status']) From 3dbf6040fe28684cd98798624843865ae40a9f2a Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 21:00:19 -0700 Subject: [PATCH 2/3] Verify in-place rounded execution and cold mutation rejection --- .../.gitattributes | 1 + .../PROOF.md | 11 ++++++++++ .../VALIDATION.md | 19 +++++++++++++++++ .../VERIFY.json | 12 +++++++++++ .../rounded.py | 10 ++++++--- .../test_package.py | 21 +++++++++++++++++++ .../verify.py | 5 ++++- 7 files changed, 75 insertions(+), 4 deletions(-) create mode 100644 research/native-rounded-butterfly-contract/.gitattributes create mode 100644 research/native-rounded-butterfly-contract/VALIDATION.md create mode 100644 research/native-rounded-butterfly-contract/test_package.py diff --git a/research/native-rounded-butterfly-contract/.gitattributes b/research/native-rounded-butterfly-contract/.gitattributes new file mode 100644 index 0000000000..d4b4746d86 --- /dev/null +++ b/research/native-rounded-butterfly-contract/.gitattributes @@ -0,0 +1 @@ +source/FULL-INPUT-PORT.md -text diff --git a/research/native-rounded-butterfly-contract/PROOF.md b/research/native-rounded-butterfly-contract/PROOF.md index b5040dc9b0..071e067de0 100644 --- a/research/native-rounded-butterfly-contract/PROOF.md +++ b/research/native-rounded-butterfly-contract/PROOF.md @@ -175,3 +175,14 @@ wrong-axis, adjoint, overflow and domain controls reject. The all-f theorem is the recurrence proof above, not the finite checks. Complete recursive substitution, fast Gaussian call implementation, fixed tapes, native supplier/outer admission, and selected5413 reproduction remain outside scope. + +## Register allocation and instrumentation distinction + +The eight-word butterfly allocation is an explicit overwrite schedule: load +a,b,c,d into slots0..3; place sr,si,dr,di in slots4..7; overwrite0..3 with the +four numerators; round/store those four slots. Python retains extra named +intermediate objects as a semantic reference and is not the register allocator. +`port` defaults to in-place operation with no cut snapshots. Only the verifier +requests `capture=True`, making copied inputs and per-call before/after arrays +for independent checks. The verifier separately requires the production default +to return the identical objects, outputs and trace with no captured arrays. diff --git a/research/native-rounded-butterfly-contract/VALIDATION.md b/research/native-rounded-butterfly-contract/VALIDATION.md new file mode 100644 index 0000000000..328edbbd7f --- /dev/null +++ b/research/native-rounded-butterfly-contract/VALIDATION.md @@ -0,0 +1,19 @@ +# Validation scope + +Canonical base32890bc5de034ab8fc93ac88ead7279a6a416d04; Darwin, standard-library +Python3.12 registered replay. The registered normal and optimized scientific +checks and optimized Git-free subprocess mutation controls passed. Each mutation +changes an actual copied file: authenticated source bytes, the scientific receipt, +and the implementation's central phase/rounding rule. Positive replay precedes +mutations. No network or Git executable is available in these copied-package runs. +Source-history and committed-byte preflight plus official export/cold replay are +reported in the publication handoff after the final commit, separately from this +working-science evidence. Transport hashes do not authenticate mathematical truth. + +The initial generic python3 registered command was rejected because this host's +python3 is3.14 and the manifest requires3.12; the corrected python3.12 command +passed. Direct scientific execution also passed on3.14 before registration. +No Lean, Docker, hosted CI, selected-frontier or unrelated historical suite ran. + +A separate OpenAI Codex peer reviewed the mathematical/implementation interface. +This is additional AI review, not independent human or formal-kernel acceptance. diff --git a/research/native-rounded-butterfly-contract/VERIFY.json b/research/native-rounded-butterfly-contract/VERIFY.json index fe725ffc98..68f75c8697 100644 --- a/research/native-rounded-butterfly-contract/VERIFY.json +++ b/research/native-rounded-butterfly-contract/VERIFY.json @@ -29,6 +29,18 @@ ], "timeout_seconds": 120, "checks": "Actual rounded Gaussian calls, complete forward/reverse source ports, internal word checks and deterministic ties against authenticated exact matrix oracle." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Optimized Git-free positive replay, then actual damaged source, receipt and scientific code rejection controls." } ] } diff --git a/research/native-rounded-butterfly-contract/rounded.py b/research/native-rounded-butterfly-contract/rounded.py index 7950580ff7..8ae18373f2 100644 --- a/research/native-rounded-butterfly-contract/rounded.py +++ b/research/native-rounded-butterfly-contract/rounded.py @@ -93,10 +93,14 @@ def mix(t,y,f,width,sign): monomial(t,name,f,width,True) -def port(x,y,f,kind,reverse,width): - need(kind in (2,3),'two or three calls');x=list(x);y=list(y);trace={};cuts=[] +def port(x,y,f,kind,reverse,width,capture=False): + need(kind in (2,3),'two or three calls') + if capture:x=list(x);y=list(y) + trace={};cuts=[] def paid(v,axis,adj=False): - before=list(v);call(v,f,axis,width,adj,trace);cuts.append((axis,adj,before,list(v))) + before=list(v) if capture else None + call(v,f,axis,width,adj,trace) + if capture:cuts.append((axis,adj,before,list(v))) if reverse: if kind==3: monomial(y,'M',f,width,True);paid(y,2,True);monomial(y,'W',f,width,True) diff --git a/research/native-rounded-butterfly-contract/test_package.py b/research/native-rounded-butterfly-contract/test_package.py new file mode 100644 index 0000000000..63bb4c485b --- /dev/null +++ b/research/native-rounded-butterfly-contract/test_package.py @@ -0,0 +1,21 @@ +"""Optimized Git-free replay and actual on-disk rejection controls.""" +import json,os,shutil,subprocess,sys,tempfile +from pathlib import Path +P=Path(__file__).resolve().parent + +def run(p,accept): + env=dict(os.environ,PATH='',PYTHONDONTWRITEBYTECODE='1') + out=subprocess.run([sys.executable,'-I','-O','-B',str(p/'verify.py')],cwd=p.parent,env=env,capture_output=True,text=True,timeout=30) + if (out.returncode==0)!=accept:raise ValueError(out.stdout+out.stderr) + +def main(): + with tempfile.TemporaryDirectory() as temp: + q=Path(temp)/'package';shutil.copytree(P,q,ignore=shutil.ignore_patterns('__pycache__')) + run(q,True) + path=q/'source'/'CHANNELS.md';raw=path.read_bytes();path.write_bytes(raw+b'\n');run(q,False);path.write_bytes(raw) + path=q/'RESULT.json';raw=path.read_bytes();record=json.loads(raw);record['status']=False;path.write_text(json.dumps(record));run(q,False);path.write_bytes(raw) + path=q/'rounded.py';raw=path.read_text() + if raw.count('return q+((n&1)&(q&1))')!=1:raise ValueError('science mutation anchor') + path.write_text(raw.replace('return q+((n&1)&(q&1))','return q'));run(q,False) + print('PASS_PACKAGE_GITFREE_MUTATIONS controls=3 optimized_git_free=true') +if __name__=='__main__':main() diff --git a/research/native-rounded-butterfly-contract/verify.py b/research/native-rounded-butterfly-contract/verify.py index 0c1bf1ac41..11ecf1f80c 100644 --- a/research/native-rounded-butterfly-contract/verify.py +++ b/research/native-rounded-butterfly-contract/verify.py @@ -61,7 +61,10 @@ def verify(): # Tiny grid-residue plus a macroscopic dirty component exercises nonzero rounding. x=[((i%5-2)*(1<<(g-2))+(i%3), (i%7-3)*(1<<(g-3))+1)for i in range(N)] y=[((i%3-1)*(1<<(g-2))+1,(i%5-2)*(1<<(g-3))-(i%2))for i in range(N)] - a,b,tr,cuts=r.port(x,y,f,kind,reverse,width) + a,b,tr,cuts=r.port(x,y,f,kind,reverse,width,capture=True) + xx,yy=list(x),list(y) + direct_a,direct_b,direct_trace,no_cuts=r.port(xx,yy,f,kind,reverse,width) + r.need(direct_a is xx and direct_b is yy and no_cuts==[] and (direct_a,direct_b,direct_trace)==(a,b,tr),'production in-place and optional cut instrumentation') exact=reference([(Q(s),Q(t))for s,t in x],[(Q(s),Q(t))for s,t in y],f,kind,reverse) err=max(error2(a,exact[0]),error2(b,exact[1])) r.need(err<=Q(1<<(2*g),1<<(2*precision)),'full port target on actual rounded execution') From 47c4e95f2aad7b33637aca3ac0dde0a0a2a9ebfe Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 21:00:33 -0700 Subject: [PATCH 3/3] Retain exact CRLF bytes of the pinned native port source --- .../source/FULL-INPUT-PORT.md | 172 +++++++++--------- 1 file changed, 86 insertions(+), 86 deletions(-) diff --git a/research/native-rounded-butterfly-contract/source/FULL-INPUT-PORT.md b/research/native-rounded-butterfly-contract/source/FULL-INPUT-PORT.md index bc713d82db..39a461f2fb 100644 --- a/research/native-rounded-butterfly-contract/source/FULL-INPUT-PORT.md +++ b/research/native-rounded-butterfly-contract/source/FULL-INPUT-PORT.md @@ -1,86 +1,86 @@ -# Reversible two-call and three-call full-input triangular ports - -Prepared for Dugongue with substantial OpenAI Codex assistance. This is an exact, all-width native building block on two arbitrary independent input arrays. It does not claim an improved complete supplier or multiplication exponent. - -## Leading two-call theorem - -Let A_f = C0_f and L_f = P_f + 2 Q_f, with the individually tensorized phase letters pinned below. For two arbitrary independent initial registers (x,y), execute - - t <- A_f x, - y <- y + P_f t + 2 Q_f t, - s <- A_f y. - -Only the first and last lines are paid calls. The complete output is - - (t,s) = (A_f x, A_f y + A_f L_f A_f x). - -This is an actual dirty-target extension of the predecessor prefix: replace its initial copy by additive injection into the existing target. To implement a term P_f t using only per-register maps and ordinary mixing, apply P_f to t, add it into y, and restore t using P_f inverse; do the same for Q_f. No original y value is overwritten and no hidden clean copy is needed. - -The exact two-call block and its inverse are - - F_f = A_f L_f A_f, - U_f = [[A_f, 0], [F_f, A_f]], - U_f inverse = [[A_f inverse, 0], [-L_f, A_f inverse]]. - -The reverse program applies A_f inverse to s, subtracts the two separately applied monomial terms using retained t, and applies A_f inverse to t. Thus it costs exactly two inverse paid calls, each equivalent to one forward paid call plus a free X0_f. Both block multiplication orders verify the inverse. This result is valid for arbitrary x and y and every positive f. - -There is also an explicit free inverse for the coupling L_f. Set R_f = P_f inverse Q_f. The actual predecessor letters satisfy R^4 = I, hence R_f^4 = I. Then - - L_f inverse = -(I - 2 R_f + 4 R_f^2 - 8 R_f^3) P_f inverse / 15. - -Multiplying by P_f(I + 2 R_f) proves the formula. Every summand is applied separately; the four-term sum is never tensorized as one letter. The fixed denominator 15 requires explicitly charged fixed-precision scalar arithmetic for numerical execution. Since R_f is unitary with fourth-root-of-unity spectrum, L_f has singular values between 1 and 3. In addition, every R_f power times P_f inverse is monomial, so the explicit formula gives infinity norm(L_f inverse) <= (1 + 2 + 4 + 8)/15 = 1 uniformly in f. The forward and reverse two/three-call schedules do not execute this division by 15; it is an optional coupling inverse. If that optional inverse is used numerically, its fixed odd division and rounding must be charged explicitly, for example by ordinary bounded-word DIV with a sufficient common-grid guard. This well-conditioned free coupling is concrete controller material, rather than an unknown gadget or an inverse asserted from a numerical rank. - -The two-call block is a product of unitary layers and the shear (t,y) -> (t,y + L_f t). Its norm and inverse norm are at most 4, so its condition number is at most 16 uniformly in f. The three-call block below is this same block followed by another unitary layer, and inherits the identical bound. - -## Constructive full-input theorem - -Use the actual base letters and phases of the pinned PR #4710 residual identity, with notation as in SECTOR-COMPLETION.md. At every positive width f, each individual letter G_f means G raised to its f-fold tensor power. Put - - A_f = C0_f, - L_f = P_f + 2 Q_f, - D_f = J_f W_f C0_f, - B_f = M_f C2_f + 2 K_f a_f. - -For arbitrary independent complex arrays x and y of length N = 8^f, the following exact program uses three paid rank-one calls: - -1. Replace x by t = C0_f x. This is the first paid call. -2. Add P_f t and 2 Q_f t into the existing y register, obtaining y + L_f t. Each summand is a separately applied free monomial. The original y is retained additively; no zero-scratch precondition is used. -3. Apply C0_f to the second register. This is the second paid call. -4. Apply W_f and J_f to that register. Only the C2_f inside J is paid, giving the third call. - -The resulting two-register output is exactly - - (t,u) = (C0_f x, D_f y + B_f x). - -Indeed u = D_f y + J_f W_f C0_f (P_f + 2 Q_f) C0_f x, and the pinned predecessor identities, tensorized separately before addition, identify the two x summands with M_f C2_f x and 2 K_f a_f x. Nothing tensors the sum P + 2 Q as a single matrix. Absolute Pauli phases remain those of the source. - -The three-call map is invertible at every width. Its explicit reverse schedule is: apply J_f inverse, W_f inverse and C0_f inverse to u, subtract P_f t and 2 Q_f t, and apply C0_f inverse to t. This recovers exactly (x,y), with no borrowed copy. Each inverse Cj_f uses one forward paid call followed by Xj_f, since Cj inverse = Xj Cj on the actual base letters. Thus the reverse also uses three paid calls. In block form the forward and inverse are - - [[A_f, 0], [D_f L_f A_f, D_f]] - and [[A_f inverse, 0], [-L_f, D_f inverse]]. - -Both multiplication orders give the identity by literal block multiplication. This is a sufficient all-input implementation, not a rank-only test or a subspace assertion. - -## Conditioning, native work and precision - -Each paid Gaussian letter and each free monomial is unitary. The whole program is a product of unitary block-diagonal layers and the shear - - S_f(t,y) = (t, y + L_f t). - -As the two free terms in L_f have unitary Euclidean norm, norm(L_f) <= 3. Writing S_f = I + N_f, with N_f squared zero, gives norm(S_f) <= 4 and norm(S_f inverse) <= 4. Consequently both the complete forward operator and its inverse have Euclidean operator norm at most 4, and their condition number is at most 16, independently of f. This statement concerns the complete two-bank map, without discarding either output. - -For an explicit coordinatewise native error budget, let complex input magnitudes be at most 2^H and request coordinate error at most 2^(-P), where H,P >= 0. Let each charged Gaussian call return its exact transform of the stored input with error at most rho per coordinate, and quantize the original inputs with error at most rho. Set L = 2^(f/2), bounding the infinity norm of any Cj_f. Free monomials, integer scalings, copies and additions can be exact on the common grid. The first call's error contributes at most 3 L^2 rho to u, the second at most L rho, and the third at most rho. Initial input errors contribute at most (3 L^3 + L^2) rho to u. Thus the conservative bound 10 L^3 rho covers both output arrays. Taking rho = 2^(-(P + 2 f + 6)) gives error below 2^(-P), since L^3 <= 2^(2 f) and 10/64 < 1. Any chosen Gaussian implementation's internal guard and time costs are separately charged; this theorem does not assume an unproved fast oracle. - -Intermediate magnitudes are below 2^(H + 2 f + 4), including these errors. P + H + 4 f + 12 signed bits per real or imaginary coordinate suffice for the displayed arithmetic. If f = O(log p), H,P = O(p) and p = Theta(log n), this occupies a fixed number of ordinary C log n-bit words, for sufficiently large fixed C. No unbounded-word multiplication or whole-array unit instruction is used. - -The address/phase odometer and explicit in-place permutation implementation in SECTOR-COMPLETION.md implement every displayed free map and mixed update in O(N) ordinary word operations. O(N) owned address workspace, or one separately owned work field, is initialized and restored in O(N) stores. These are charged native resources, not additional independent productive inputs. The theorem therefore supplies three paid calls plus O(N) native work, with two arbitrary input banks and explicitly accounted workspace. - -## How to use the port without changing its claim - -A controller may now wire this full-input block into a larger exact block identity, preserving both diagonal channels and the actual rank-three off-diagonal term. This differs from the clean-prefix presentation because the second initial array is arbitrary and its D_f y contribution is explicit. A claimed complete saving must show the actual subsequent block operations, canonical independent outputs, restored owners and total paid calls. This port alone has diagonal ranks one and two and does not establish a three-rank target for both independent arrays. Discarding D_f y, assuming it is initially zero, or counting B_f x as an independent additional Gaussian job would change the theorem. - -## Evidence and predecessor credit - -verify_full_input_port.py uses the pinned exact Gaussian-rational engine to verify both predecessor word identities, both full-input triangular blocks, both inverse multiplication identities, the order-four free coupling inverse and the one-call implementation of paid inverses. It rejects the false claim that the second output is independent of an arbitrary y. Separately tensorized word algebra proves all widths; the finite checks do not infer universal correctness from a few dimensions. - -Credit Yiyang / Lyy-iiis, PR #4710 (b0d5192390af493d626054b060921895df3c94d2), for the repaired phase prefix and residual identity; lee-phys, PR #4688 (264c4b3cb13c82d171de352ecf60486dfb8d2bd4), for the original prefix and rank engine; and Jacob Alan Sussman, PR #4628 (ee4fd87f064017c23e5a86fc1dcfe0a5237caed3), for the complex engine model and small-unit problem. Retain their notices and earlier attribution. This full-input additive schedule, reverse interface and uniform norm bound are the present extension. No worldwide novelty or independent human review is claimed. Exact source URLs and SHA-256 pins appear in SOURCE-PINS.json. +# Reversible two-call and three-call full-input triangular ports + +Prepared for Dugongue with substantial OpenAI Codex assistance. This is an exact, all-width native building block on two arbitrary independent input arrays. It does not claim an improved complete supplier or multiplication exponent. + +## Leading two-call theorem + +Let A_f = C0_f and L_f = P_f + 2 Q_f, with the individually tensorized phase letters pinned below. For two arbitrary independent initial registers (x,y), execute + + t <- A_f x, + y <- y + P_f t + 2 Q_f t, + s <- A_f y. + +Only the first and last lines are paid calls. The complete output is + + (t,s) = (A_f x, A_f y + A_f L_f A_f x). + +This is an actual dirty-target extension of the predecessor prefix: replace its initial copy by additive injection into the existing target. To implement a term P_f t using only per-register maps and ordinary mixing, apply P_f to t, add it into y, and restore t using P_f inverse; do the same for Q_f. No original y value is overwritten and no hidden clean copy is needed. + +The exact two-call block and its inverse are + + F_f = A_f L_f A_f, + U_f = [[A_f, 0], [F_f, A_f]], + U_f inverse = [[A_f inverse, 0], [-L_f, A_f inverse]]. + +The reverse program applies A_f inverse to s, subtracts the two separately applied monomial terms using retained t, and applies A_f inverse to t. Thus it costs exactly two inverse paid calls, each equivalent to one forward paid call plus a free X0_f. Both block multiplication orders verify the inverse. This result is valid for arbitrary x and y and every positive f. + +There is also an explicit free inverse for the coupling L_f. Set R_f = P_f inverse Q_f. The actual predecessor letters satisfy R^4 = I, hence R_f^4 = I. Then + + L_f inverse = -(I - 2 R_f + 4 R_f^2 - 8 R_f^3) P_f inverse / 15. + +Multiplying by P_f(I + 2 R_f) proves the formula. Every summand is applied separately; the four-term sum is never tensorized as one letter. The fixed denominator 15 requires explicitly charged fixed-precision scalar arithmetic for numerical execution. Since R_f is unitary with fourth-root-of-unity spectrum, L_f has singular values between 1 and 3. In addition, every R_f power times P_f inverse is monomial, so the explicit formula gives infinity norm(L_f inverse) <= (1 + 2 + 4 + 8)/15 = 1 uniformly in f. The forward and reverse two/three-call schedules do not execute this division by 15; it is an optional coupling inverse. If that optional inverse is used numerically, its fixed odd division and rounding must be charged explicitly, for example by ordinary bounded-word DIV with a sufficient common-grid guard. This well-conditioned free coupling is concrete controller material, rather than an unknown gadget or an inverse asserted from a numerical rank. + +The two-call block is a product of unitary layers and the shear (t,y) -> (t,y + L_f t). Its norm and inverse norm are at most 4, so its condition number is at most 16 uniformly in f. The three-call block below is this same block followed by another unitary layer, and inherits the identical bound. + +## Constructive full-input theorem + +Use the actual base letters and phases of the pinned PR #4710 residual identity, with notation as in SECTOR-COMPLETION.md. At every positive width f, each individual letter G_f means G raised to its f-fold tensor power. Put + + A_f = C0_f, + L_f = P_f + 2 Q_f, + D_f = J_f W_f C0_f, + B_f = M_f C2_f + 2 K_f a_f. + +For arbitrary independent complex arrays x and y of length N = 8^f, the following exact program uses three paid rank-one calls: + +1. Replace x by t = C0_f x. This is the first paid call. +2. Add P_f t and 2 Q_f t into the existing y register, obtaining y + L_f t. Each summand is a separately applied free monomial. The original y is retained additively; no zero-scratch precondition is used. +3. Apply C0_f to the second register. This is the second paid call. +4. Apply W_f and J_f to that register. Only the C2_f inside J is paid, giving the third call. + +The resulting two-register output is exactly + + (t,u) = (C0_f x, D_f y + B_f x). + +Indeed u = D_f y + J_f W_f C0_f (P_f + 2 Q_f) C0_f x, and the pinned predecessor identities, tensorized separately before addition, identify the two x summands with M_f C2_f x and 2 K_f a_f x. Nothing tensors the sum P + 2 Q as a single matrix. Absolute Pauli phases remain those of the source. + +The three-call map is invertible at every width. Its explicit reverse schedule is: apply J_f inverse, W_f inverse and C0_f inverse to u, subtract P_f t and 2 Q_f t, and apply C0_f inverse to t. This recovers exactly (x,y), with no borrowed copy. Each inverse Cj_f uses one forward paid call followed by Xj_f, since Cj inverse = Xj Cj on the actual base letters. Thus the reverse also uses three paid calls. In block form the forward and inverse are + + [[A_f, 0], [D_f L_f A_f, D_f]] + and [[A_f inverse, 0], [-L_f, D_f inverse]]. + +Both multiplication orders give the identity by literal block multiplication. This is a sufficient all-input implementation, not a rank-only test or a subspace assertion. + +## Conditioning, native work and precision + +Each paid Gaussian letter and each free monomial is unitary. The whole program is a product of unitary block-diagonal layers and the shear + + S_f(t,y) = (t, y + L_f t). + +As the two free terms in L_f have unitary Euclidean norm, norm(L_f) <= 3. Writing S_f = I + N_f, with N_f squared zero, gives norm(S_f) <= 4 and norm(S_f inverse) <= 4. Consequently both the complete forward operator and its inverse have Euclidean operator norm at most 4, and their condition number is at most 16, independently of f. This statement concerns the complete two-bank map, without discarding either output. + +For an explicit coordinatewise native error budget, let complex input magnitudes be at most 2^H and request coordinate error at most 2^(-P), where H,P >= 0. Let each charged Gaussian call return its exact transform of the stored input with error at most rho per coordinate, and quantize the original inputs with error at most rho. Set L = 2^(f/2), bounding the infinity norm of any Cj_f. Free monomials, integer scalings, copies and additions can be exact on the common grid. The first call's error contributes at most 3 L^2 rho to u, the second at most L rho, and the third at most rho. Initial input errors contribute at most (3 L^3 + L^2) rho to u. Thus the conservative bound 10 L^3 rho covers both output arrays. Taking rho = 2^(-(P + 2 f + 6)) gives error below 2^(-P), since L^3 <= 2^(2 f) and 10/64 < 1. Any chosen Gaussian implementation's internal guard and time costs are separately charged; this theorem does not assume an unproved fast oracle. + +Intermediate magnitudes are below 2^(H + 2 f + 4), including these errors. P + H + 4 f + 12 signed bits per real or imaginary coordinate suffice for the displayed arithmetic. If f = O(log p), H,P = O(p) and p = Theta(log n), this occupies a fixed number of ordinary C log n-bit words, for sufficiently large fixed C. No unbounded-word multiplication or whole-array unit instruction is used. + +The address/phase odometer and explicit in-place permutation implementation in SECTOR-COMPLETION.md implement every displayed free map and mixed update in O(N) ordinary word operations. O(N) owned address workspace, or one separately owned work field, is initialized and restored in O(N) stores. These are charged native resources, not additional independent productive inputs. The theorem therefore supplies three paid calls plus O(N) native work, with two arbitrary input banks and explicitly accounted workspace. + +## How to use the port without changing its claim + +A controller may now wire this full-input block into a larger exact block identity, preserving both diagonal channels and the actual rank-three off-diagonal term. This differs from the clean-prefix presentation because the second initial array is arbitrary and its D_f y contribution is explicit. A claimed complete saving must show the actual subsequent block operations, canonical independent outputs, restored owners and total paid calls. This port alone has diagonal ranks one and two and does not establish a three-rank target for both independent arrays. Discarding D_f y, assuming it is initially zero, or counting B_f x as an independent additional Gaussian job would change the theorem. + +## Evidence and predecessor credit + +verify_full_input_port.py uses the pinned exact Gaussian-rational engine to verify both predecessor word identities, both full-input triangular blocks, both inverse multiplication identities, the order-four free coupling inverse and the one-call implementation of paid inverses. It rejects the false claim that the second output is independent of an arbitrary y. Separately tensorized word algebra proves all widths; the finite checks do not infer universal correctness from a few dimensions. + +Credit Yiyang / Lyy-iiis, PR #4710 (b0d5192390af493d626054b060921895df3c94d2), for the repaired phase prefix and residual identity; lee-phys, PR #4688 (264c4b3cb13c82d171de352ecf60486dfb8d2bd4), for the original prefix and rank engine; and Jacob Alan Sussman, PR #4628 (ee4fd87f064017c23e5a86fc1dcfe0a5237caed3), for the complex engine model and small-unit problem. Retain their notices and earlier attribution. This full-input additive schedule, reverse interface and uniform norm bound are the present extension. No worldwide novelty or independent human review is claimed. Exact source URLs and SHA-256 pins appear in SOURCE-PINS.json.