diff --git a/research/selected-native-unbiased-rounding/NOTICE b/research/selected-native-unbiased-rounding/NOTICE new file mode 100644 index 0000000000..d0ac2391f6 --- /dev/null +++ b/research/selected-native-unbiased-rounding/NOTICE @@ -0,0 +1,37 @@ +New work: Ali Romman with substantial OpenAI Codex assistance. No subagents. +Apache-2.0. + +DreamingOfClouds, PR6030, supplies the selected word and its retained P104 +lineage through PR5907, PR5827, PR5811, PR5786 and earlier work. +https://github.com/CrocSwap/integer-mult-bounds/pull/6030 + +Ali Romman with OpenAI Codex assistance, PR6509, supplies the deterministic +conserved-sum center family, phase-covariant choice and nearest-grid proof. +The new package randomizes opposite centers and binds a stochastic interface. +https://github.com/CrocSwap/integer-mult-bounds/pull/6509 + +Nick Petalas, PR6438, supplies the prior ensemble question and a different +optimal planar construction. PR6418 gives the adaptive-reuse bound; zxv's +PR6066 supplies the earlier reuse warning. Ali Romman's PR6526 supplies the +whole-word relative stochastic contract not met by this fixed-grid map. +https://github.com/CrocSwap/integer-mult-bounds/pull/6438 +https://github.com/CrocSwap/integer-mult-bounds/pull/6418 +https://github.com/CrocSwap/integer-mult-bounds/pull/6066 +https://github.com/CrocSwap/integer-mult-bounds/pull/6526 + +Cinna Davis, 1337isnot1337, PR4088 and PR2226, supplies the consumed exact +native representations. All source notices remain unchanged. The native +compiler retains the work of icekylinx, DreamingOfClouds, vendor531, +Rohan Arun and the preceding Gaussian lineage. +https://github.com/CrocSwap/integer-mult-bounds/pull/4088 +https://github.com/CrocSwap/integer-mult-bounds/pull/2226 + +Tekalign's reversible lifting, JoyboyBrian's rounded ports, Arham Tahir's +numerical work and the PR4743/PR5485 lineage are predecessors of PR6509. +Chris R / Clear1nsight and the credited PR4017 contributors supply a different +source-bound deterministic native circuit with dirty scratch. +https://github.com/CrocSwap/integer-mult-bounds/pull/5485 +https://github.com/CrocSwap/integer-mult-bounds/pull/4017 + +Lattice parity, nearest-grid error and conditional martingale orthogonality +are established mathematics. No global literature priority is claimed. diff --git a/research/selected-native-unbiased-rounding/PROOF.md b/research/selected-native-unbiased-rounding/PROOF.md new file mode 100644 index 0000000000..7a31e82281 --- /dev/null +++ b/research/selected-native-unbiased-rounding/PROOF.md @@ -0,0 +1,175 @@ +# A retained-seed native Gaussian interface + +This is an all-integer construction with a finite source check. It does not +change kappa. It supplies zero conditional mean error, bounded absolute error +and exact data return with retained seeds. It does not supply a reversible bit +circuit, a tape bill or a uniform relative error coefficient below one. + +## Source and new scope + +The selected PR6030 word has 22,803 events. Its first MOVE is zero-based event +9896, `["MOVE",236,3,7,false]`. Frame 3 is empty; frame 7 has basis [21]. +The Boolean is a private-field flag. The native map at width one is the +canonical frame T_[21] on 512 complex coordinates. The unchanged Clifford +compiler produces a rank-one recipe L C R. The separate coordinate oracle +checks all 512 columns, including global phase. SOURCES.json pins both sources +and the word. Source assertions remain enabled in both registered modes. + +The deterministic conserved-sum center family and nearest-grid property are +prior work in [PR6509](https://github.com/CrocSwap/integer-mult-bounds/pull/6509). +The new interface randomizes opposite centers, uses one fresh bit per complete +layer, binds the map to this selected MOVE, and proves its conditional moments, +tensor bound, seed cost and reachable relative-error limit. +[PR6438](https://github.com/CrocSwap/integer-mult-bounds/pull/6438) gives the prior +question of optimal unbiased reversible ensembles for other rational operators. + +## Pair map + +Use units of a positive grid spacing h. Let x,y be Gaussian integers, s=x+y, +d=x-y. Choose c(s)=0 when Re(s)+Im(s) is even. Otherwise choose the sign of +Re(s) when Re(s) is odd, or i times the sign of Im(s) when Im(s) is odd. +The sign is never taken at zero. Then Re(c)+Im(c) has the parity of +Re(s)+Im(s), and c(is)=i*c(s). For sigma in {-1,+1}, define + +```text +d' = i*(d-sigma*c(s)) + sigma*c(s) +F_sigma(x,y) = ((s+d')/2, (s-d')/2). +``` + +The numerators are even Gaussian integers: d and s agree componentwise +modulo two, and rotation exchanges the components of d-sigma*c. The parity +condition gives d'=s modulo two. The complex sum s is preserved exactly. +The inverse uses the same s, seed and center, with -i in place of i. Thus +each fixed seed gives a bijection of the entire Gaussian integer pair lattice +with an exact two-sided inverse. No input-size bound is needed. + +Multiplication of both inputs by i multiplies s,d,c,d' by i. Every fixed-seed +map and inverse therefore commute with all four Gaussian unit phases. These +properties retain the prior conserved-sum mechanism; they are not claimed new. + +## Exact stochastic optimum and one-bit cost + +The ideal pair operator is `C=[[1+i,1-i],[1-i,1+i]]/2`. It sends d to i*d. +The local error is `sigma*((1-i)c/2,-(1-i)c/2)`. A fair seed independent of +the complete past therefore gives conditional mean zero. Its squared Hilbert +norm is h^2*|c|^2: zero for even total parity and h^2 for odd total parity. +The inverse ensemble has the same mean and error statement for an input +independent of its seed. Inversion of the seed-dependent forward output is +used for exact return, not as a fresh-noise step. + +For odd total parity, all four real components of the ideal output are +half-integers. Every grid-valued output has squared error at least +4*(h/2)^2=h^2. Both outcomes attain this lower bound. For even parity the +ideal output is integral and both outcomes are exact. The construction is +therefore pointwise optimal among all unbiased grid-valued random outputs, +including nonreversible ones. This is an error optimum, not a machine-cost +optimum. + +For N/2 disjoint pairs, use the SAME fresh bit on the entire layer. Given +the input, each error still has mean zero. Disjoint coordinate support gives +exact squared error k*h^2 for each seed, where k is the number of odd pairs. +This is the pointwise minimum total error. The pair errors need not be +independent; they can be fully correlated. + +When k>0, any distribution attaining the minimum has support on nearest +grid points. One half-integral real component must take its two neighboring +integers with probabilities one half. Output entropy is at least one bit. +A seed that deterministically produces it has entropy at least one bit. +The construction attains this lower bound for a layer. No minimum of f bits +is claimed for an arbitrary complete f-stage implementation. + +## Actual native map and tensor stages + +The source monomials L,R are Gaussian-unit signed permutations. They preserve +the grid and norm. Use L F_sigma R and the literal inverse +R^-1 F_sigma^-1 L^-1. Its mean is LCR; its squared error is k*h^2, with k +measured after R. Sum preservation is in the transformed coordinates: +S L^-1 y = S R x, where S adds each pair. Arbitrary physical-coordinate pair +sums are not asserted invariant. + +For f>=1 and N=512^f, apply a native stage on each address digit, with a fresh +independent fair bit at each stage. Keep the f bits and reverse the actual +stage order for inversion. The exact stage operators A_j are deterministic +unitaries. For each completed stage error delta_j, + +```text +E(delta_j | all earlier data and seeds) = 0, +||delta_j||^2 <= (N/2)*h^2. +``` + +The final error is the sum of these defects transported by the later ideal +unitaries. Conditional mean zero makes distinct summands orthogonal in L2. +This requires no independence of their values. Hence + +```text +E(output | input) = (T_[21])^(tensor f) input, +E(||output-ideal||^2 | input) <= f*N*h^2/2, +||output-ideal|| <= f*h*sqrt(N/2) for every seed word. +``` + +The proof holds at every finite width. The second-moment upper bound is not +claimed sharp for the complete tensor map. A full 512^2 input and all four +two-stage seed words are also checked against a Kronecker product of the +independent source oracle. Finite checks corroborate, but do not replace, +the universal argument. + +Freshness is required. RESULT.json gives a four-coordinate example where +reusing a seed across two rounded axes changes the mean. Literal inversion +intentionally reuses the retained seeds; it is not a new stochastic forward +invocation. General adaptive reuse bias retains its prior credit in +[PR6418](https://github.com/CrocSwap/integer-mult-bounds/pull/6418). + +## Reachable relative-error boundary + +Input h*R^-1 e_0 is a single Gaussian unit grid entry with norm h. After R, +exactly one pair has odd parity. Every same-grid output has error at least h. +Thus no same-grid rule, randomized or otherwise, can have +`||delta|| <= u*||input||` for all such inputs when u<1. The constructed +stage attains equality. It satisfies coefficient one for every grid input: +k odd pairs require input squared norm at least k*h^2, and its error is +exactly k*h^2. + +This witness is reachable at the actual source boundary. A reverse scalar +row and a separate forward replay of all 9896 preceding events show that +setting only public input 236 to this vector produces the same vector at +the first MOVE. That public input starts in the empty frame. RESULT.json +records the maximum prefix denominator and magnitude. The scalar prefix can +therefore be exact on the corresponding finer grid. No earlier native error +is needed. This does not assert one common grid at every cut of the whole word. + +The stage does not discharge the relative premise in +[PR6526](https://github.com/CrocSwap/integer-mult-bounds/pull/6526). +An absolute-error caller analysis, changed grid or changed encoding is needed. +No impossibility is claimed for those other interfaces. + +## Complete direct bill and remaining obligations + +The supplied integer algorithm uses f*N/2 pair calls, 2*f monomial passes +and f retained bits. A pair uses at most 13 additions/subtractions, four +exact half shifts, three sign changes and a constant number of parity, sign +and seed selections. Each monomial pass moves N complex coordinates and uses +at most 2*N real sign changes. The two 512-entry route tables are built by +the displayed nine-bit quadratic formulas, with setup included. Inversion +has the same counts; a forward/inverse round trip doubles them. + +If input component magnitudes are at most M, pair outputs have magnitude at +most 2*M+1 and temporaries at most 4*M+2. After j stages the component bound +is 2^j*(M+1)-1. With M<=2^(w-1)-1, w+f signed bits suffice for stored outputs, +and w+f+1 for pair temporaries. Gaussian unit permutations preserve these +bounds. These are sufficient, not optimal, widths. + +Direct indexed work is O(f*N) bounded-word operations, including data movement, +buffer initialization and routes. Addresses use 9*f bits. Arithmetic and +address operations give O(f*N*(w+f)) bit work in this indexed model. There +are at most two working arrays of N Gaussian entries in addition to the live +input, constant pair scratch, route tables and f retained bits. This is not +an in-place bit circuit, minimum-space construction or fixed multitape +schedule. Sampling, random-tape access, entropy recovery, physical cleanup +and accelerated recursive-child pricing remain open. + +Nonlinearity remains. Data inversion does not imply additivity, native-graph +flatness, dirty compensation after intervening arithmetic or whole-word +restoration. Only this MOVE and its stated tensor powers are bound. All five +framework assumptions and the selected frontier remain unchanged. Selected +cold replay, complete supplier/caller implementation, native builds, +independent human acceptance and formal proof-kernel review are unclaimed. diff --git a/research/selected-native-unbiased-rounding/README.md b/research/selected-native-unbiased-rounding/README.md new file mode 100644 index 0000000000..2a335164c4 --- /dev/null +++ b/research/selected-native-unbiased-rounding/README.md @@ -0,0 +1,85 @@ +# Unbiased reversible rounding at the selected first native MOVE + +The selected PR6030 word's first native MOVE now has a source-bound integer +grid map with exact retained-seed inversion and zero conditional mean error. +One fresh fair bit serves every pair in a complete butterfly layer. Its +pointwise squared error is the minimum possible grid error: h^2 for each +odd-parity pair and zero otherwise. Each seed preserves the complex pair +sum and Gaussian phase covariance in the native pair coordinates. + +For N=512^f and f fresh stage bits, the completed tensor map has exact mean +T_[21]^(tensor f), mean squared error at most f*N*h^2/2, and an exact literal +inverse with the retained bits in reverse stage order. This is a construction +and proof with finite corroboration, not a new kappa. + +A reachable first-MOVE input has error/input norm ratio at least one under +every same-grid rule. Thus this map cannot fill a uniform relative allowance +u<1. The absolute-error caller join remains open. The [proof](PROOF.md), +[generated receipt](RESULT.json), [source pins](SOURCES.json) and +[scope record](TASK.json) state the contracts and limits. + +## Source and evidence + +Canonical base: 7c49fe32c55de02c2c873655c804b16e4c3fef0a; priority revision 8; +selected PR6030. Event 9896 is MOVE field 236 from empty frame 3 to frame 7 +with basis [21]. The unchanged compiler and independent coordinate oracle +agree on all 512 columns. The new interpreter checks real and imaginary basis +inputs, signed dense inputs and every seed of a full 512^2 tensor input. +A separate reverse row and literal scalar replay check the first-MOVE witness. + +The verifier checks all pairs with real components from -4 through 4, both +directions, all Gaussian unit phases and signed inputs including 2^1024-scale values. +It checks seed reuse bias, a wrong inverse seed, a biased fixed seed, +deterministic floor, a non-covariant center, invalid seeds, the relative-error +counterexample and source corruption. RESULT.json gives the exact counts. + +## Reproduce + +Use CPython 3.12 and the declared NumPy 2.3.4 dependency: + +```sh +python3.12 -B scripts/research_package.py --package research/selected-native-unbiased-rounding +``` + +Both registered commands use isolated, warning-strict normal and optimized +modes. Expected markers: `PASS_SELECTED_NATIVE_UNBIASED_ROUNDING` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. The source compiler and coordinate oracle +require assertions, so each mode runs them in an unchanged normal subprocess. +The new verifier's checks remain active under optimization. + +## Complete scope and remaining work + +The direct implementation uses f*N/2 pair calls, 2*f monomial passes and f +retained bits. The proof includes setup, arithmetic, routing, sufficient +integer widths, data movement and O(N) buffer storage. This is an indexed +integer implementation, not a reversible bit circuit or fixed multitape +schedule. Sampling, random-tape access, entropy recovery, physical cleanup, +accelerated recursive tariffs and full caller propagation are unpriced. +Data inversion does not prove additivity, graph consistency or cleanup after +arbitrary intervening arithmetic. All five assumptions remain open. + +Selected cold replay, predecessor full scientific suites, native builds, +independent human review and proof-kernel review are unrun. See the PR for +publication and hosted status. A hosted pass verifies the registered commands, +not acceptance of the universal proof. + +## Open next questions + +The next question is a full absolute-error caller join with finite scalar +records and owned fresh randomness. First bind its completed native defects +to the selected suffix transfers. A physical supplier and full tape invoice +are the blockers. No next scope is reserved. + +## Attribution and overlap + +Prepared by Ali Romman with substantial OpenAI Codex assistance; no subagents. +[NOTICE](NOTICE) separates the prior deterministic center family in PR6509, +Nick Petalas's ensemble and reuse results, the selected word, and the consumed +native compiler/oracle lineage. Their sources remain unchanged. + +Public open/closed PR and Discussion metadata was refreshed before the claim. +A second exact-main README/TASK search found no matching unbiased Gaussian or +butterfly description. Related PR6509, PR6438, PR6418, PR4017, PR6499 and PR6526 +were inspected. This construction has a different numerical contract and an +actual selected native binding. Arbitrary diffs and unpublished work remain +search limits. No novelty certificate is claimed. diff --git a/research/selected-native-unbiased-rounding/RESULT.json b/research/selected-native-unbiased-rounding/RESULT.json new file mode 100644 index 0000000000..41ebc06899 --- /dev/null +++ b/research/selected-native-unbiased-rounding/RESULT.json @@ -0,0 +1,161 @@ +{ + "source": { + "event_index": 9896, + "event": [ + "MOVE", + 236, + 3, + 7, + false + ], + "frames": [ + [], + [ + 21 + ] + ], + "word_events": 22803, + "recipe": { + "rank": 1, + "left": { + "matrix_rows": [ + 3, + 4, + 9, + 16, + 1, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 21, + 17, + 2, + 20, + 8, + 32, + 64, + 128, + 256 + ], + "offset": 1, + "quadratic_rows": [ + 5, + 0, + 5, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 3, + 0, + 3, + 0, + 2, + 0, + 0, + 0, + 0 + ], + "phase": 1 + } + }, + "assertions_enabled": true, + "oracle_columns": 512 + }, + "kernel": { + "pair_directions": 26244, + "phase_checks": 104976, + "wide_pairs": 128 + }, + "native": { + "native_basis_inputs": 1024, + "native_signed_inputs": 8, + "tensor_seed_words": 4, + "tensor_coordinates": 262144, + "tensor_mse": "78276", + "native_output_sha256": "207f9ca2eb94799790838d71ae54018c0926126104437013cc60d9fe2b529c2f", + "relative_witness": [ + { + "coordinate": 21, + "value": [ + 0, + 1 + ] + } + ] + }, + "prefix_witness": { + "input_field": 236, + "input_scalar": "1", + "coefficient": "1", + "row_support": 2, + "prefix_events": 9896, + "max_prefix_denominator": 2, + "max_prefix_absolute": "1" + }, + "controls": { + "semantic_controls": 7, + "reused_seed_witness": { + "input": [ + -1, + -1, + -1, + 0 + ], + "fresh_mean": [ + "-1", + "-1/2", + "-1/2", + "0", + "-1/2", + "0", + "-1", + "1/2" + ], + "reused_mean": [ + "-1", + "-1/2", + "-1", + "0", + "-1/2", + "0", + "-1/2", + "1/2" + ] + } + }, + "source_corruption_controls": 3 +} diff --git a/research/selected-native-unbiased-rounding/SOURCES.json b/research/selected-native-unbiased-rounding/SOURCES.json new file mode 100644 index 0000000000..dc4e6683f6 --- /dev/null +++ b/research/selected-native-unbiased-rounding/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/staged544-mixed-fourth-entry/native/vendor/native/new/code/borrow/bw_gauss.py", + "usage": "input", + "git_blob": "1ff29dfb244e2114de8e586a450ae9fb70308d58", + "sha256": "0884b14d6d77cde419a3c773ad9b21d0d18de1e6e20e6b6d5add458ed32ba4cb" + }, + { + "path": "research/staged544-mixed-fourth-entry/native/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/selected-native-unbiased-rounding/TASK.json b/research/selected-native-unbiased-rounding/TASK.json new file mode 100644 index 0000000000..b387d5756a --- /dev/null +++ b/research/selected-native-unbiased-rounding/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Bind an optimal unbiased reversible Gaussian grid map to the first native MOVE of the selected PR6030 word. Prove the tensor error and retained-seed interface, and its fixed-grid relative-error limit.", + "scope_change_reason": "The current native precision obligation has no supplied stochastic implementation. This result supplies a source-bound absolute-error interface and records the failed uniform relative substitution.", + "bottleneck_link": "The selected native_all_columns and precision_tape assumptions need a concrete numerical contract. This local map has zero conditional mean error with fresh bits, but cannot meet a uniform relative coefficient below one on a fixed grid. It is not supplier admission or a kappa change.", + "budget_minutes": 60, + "stop_rule": "Stop at one source-bound construction with a proof, complete source-column checks and counterexamples to stronger contracts.", + "outcome": "completed", + "evidence": "PROOF.md and generated RESULT.json. Exact pair and native checks, complete two-stage tensor expectation and inversion, scalar-prefix witness, and semantic/source controls. See README.md for checks and limits.", + "author": "Ali Romman", + "ai_assistance": "Ali Romman with substantial OpenAI Codex assistance. No subagents.", + "open_questions": [ + { + "question": "Can a full selected caller use absolute stochastic native errors with bounded scalar grids and retained random bits?", + "why_it_matters": "The relative stochastic premise is not met by this fixed-grid native map.", + "first_step": "Join the absolute native error and fresh-seed ownership to a complete scalar-record and suffix-transfer invoice.", + "blocked_by": "A complete supplier, fixed-tape schedule, sampling and restoration cost, and caller error propagation are not supplied here." + } + ] +} diff --git a/research/selected-native-unbiased-rounding/VERIFY.json b/research/selected-native-unbiased-rounding/VERIFY.json new file mode 100644 index 0000000000..1c1ebec8d2 --- /dev/null +++ b/research/selected-native-unbiased-rounding/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.3.4" + ], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/staged544-mixed-fourth-entry/native/vendor/native/new/code/borrow/bw_gauss.py", + "research/staged544-mixed-fourth-entry/native/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Source-bound native operator; exact pair and tensor moments, inverse and range; prefix witness; semantic and source controls. The unchanged source compiler runs in a normal subprocess with assertions enabled." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Source-bound native operator; exact pair and tensor moments, inverse and range; prefix witness; semantic and source controls. The unchanged source compiler runs in a normal subprocess with assertions enabled." + } + ] +} diff --git a/research/selected-native-unbiased-rounding/kernel.py b/research/selected-native-unbiased-rounding/kernel.py new file mode 100644 index 0000000000..ef6e720b09 --- /dev/null +++ b/research/selected-native-unbiased-rounding/kernel.py @@ -0,0 +1,102 @@ +"""Apply the retained-seed Gaussian map with exact integer operations.""" + + +def center(sr, si): + if (sr + si) % 2 == 0: + return 0, 0 + if sr % 2: + return (1 if sr > 0 else -1), 0 + return 0, (1 if si > 0 else -1) + + +def pair(x, y, seed, inverse=False): + if seed not in (-1, 1): + raise ValueError("seed must be -1 or 1") + a, b = x + c, d = y + sr, si, dr, di = a + c, b + d, a - c, b - d + cr, ci = center(sr, si) + cr, ci = seed * cr, seed * ci + dr, di = dr - cr, di - ci + dr, di = (di, -dr) if inverse else (-di, dr) + dr, di = dr + cr, di + ci + numerators = (sr + dr, si + di, sr - dr, si - di) + if any(v % 2 for v in numerators): + raise ArithmeticError("pair output is not on the integer grid") + a, b, c, d = (v // 2 for v in numerators) + return (a, b), (c, d) + + +def phase(z, p): + a, b = z + p %= 4 + if p == 0: + return a, b + if p == 1: + return -b, a + if p == 2: + return -a, -b + return b, -a + + +def route(recipe): + n = len(recipe["matrix_rows"]) + mapping, phases = [], [] + for x in range(1 << n): + y = sum(((row & x).bit_count() % 2) << j + for j, row in enumerate(recipe["matrix_rows"])) ^ recipe["offset"] + p = recipe["phase"] + for j in range(n): + if x >> j & 1: + p += recipe["linear_Z4"][j] + p += 2 * (((recipe["quadratic_rows"][j] >> (j + 1)) + & (x >> (j + 1))).bit_count() % 2) + mapping.append(y) + phases.append(p % 4) + if sorted(mapping) != list(range(1 << n)): + raise ValueError("monomial route is not a permutation") + return mapping, phases + + +def monomial(values, routing, axis, inverse=False): + mapping, phases = routing + radix = len(mapping) + stride = radix ** axis + out = [None] * len(values) + for start in range(0, len(values), radix * stride): + for digit, dest in enumerate(mapping): + p = phases[digit] + for low in range(stride): + src, dst = start + digit * stride + low, start + dest * stride + low + if inverse: + out[src] = phase(values[dst], -p) + else: + out[dst] = phase(values[src], p) + return out + + +def layer(values, seed, stride=1, inverse=False): + out = [None] * len(values) + for start in range(0, len(values), 2 * stride): + for low in range(stride): + a, b = start + low, start + stride + low + out[a], out[b] = pair(values[a], values[b], seed, inverse) + return out + + +def native(values, recipes, seeds, inverse=False): + if not seeds or len(values) != 512 ** len(seeds): + raise ValueError("native shape must be 512**len(seeds)") + left, right = (route(recipes[key]) for key in ("left", "right")) + out = list(values) + axes = reversed(range(len(seeds))) if inverse else range(len(seeds)) + for axis in axes: + if inverse: + out = monomial(out, left, axis, True) + out = layer(out, seeds[axis], 512 ** axis, True) + out = monomial(out, right, axis, True) + else: + out = monomial(out, right, axis) + out = layer(out, seeds[axis], 512 ** axis) + out = monomial(out, left, axis) + return out diff --git a/research/selected-native-unbiased-rounding/produce.py b/research/selected-native-unbiased-rounding/produce.py new file mode 100644 index 0000000000..e654dba2a4 --- /dev/null +++ b/research/selected-native-unbiased-rounding/produce.py @@ -0,0 +1,53 @@ +"""Read the source word and run both unchanged native representations.""" + +import gzip +import hashlib +import json +import sys +from pathlib import Path + +import numpy as np + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def main(): + if not __debug__: + raise RuntimeError("source assertions must remain enabled") + for item in json.loads((HERE / "SOURCES.json").read_text())["files"]: + if item["usage"] == "input": + if hashlib.sha256((ROOT / item["path"]).read_bytes()).hexdigest() != item["sha256"]: + raise ValueError("source mismatch: " + item["path"]) + word = json.loads(gzip.decompress((ROOT / "research/p104-helper470-twin-rung-removal/WORD.json.gz").read_bytes())) + first = next((j, e) for j, e in enumerate(word["program"]) if e[0] == "MOVE") + if first != (9896, ["MOVE", 236, 3, 7, False]) or word["frames"][3] != [] or word["frames"][7] != [21]: + raise ValueError("selected native boundary changed") + source = ROOT / "research/staged544-mixed-fourth-entry/native/vendor/native/new/code/borrow" + sys.path.insert(0, str(source)) + sys.path.insert(0, str(source / "vendor/clifford")) + import bw_gauss + from clifford_exact import canonical_frame, lower_child + recipe, compiled = lower_child(canonical_frame(9, [21])) + if recipe["rank"] != 1: + raise ValueError("the selected MOVE is not rank one") + real, imag, exponent = bw_gauss.frame(bw_gauss.eye(9), [21], 9) + if exponent != 1: + raise ValueError("unexpected oracle denominator") + for j in range(512): + values, exp = compiled.zero_state(j) + if any((a * 2 != int(real[i, j]) * (1 << exp) or + b * 2 != int(imag[i, j]) * (1 << exp)) + for i, (a, b) in enumerate(values)): + raise ValueError("compiler and coordinate oracle disagree") + out = Path(sys.argv[1]) + np.savez(out / "oracle.npz", real=real, imag=imag) + (out / "source.json").write_text(json.dumps({ + "event_index": first[0], "event": first[1], "frames": [[], [21]], + "word_events": len(word["program"]), "recipe": recipe, + "assertions_enabled": __debug__, "oracle_columns": 512, + }, indent=2) + "\n") + + +if __name__ == "__main__": + main() diff --git a/research/selected-native-unbiased-rounding/verify.py b/research/selected-native-unbiased-rounding/verify.py new file mode 100644 index 0000000000..e52983f296 --- /dev/null +++ b/research/selected-native-unbiased-rounding/verify.py @@ -0,0 +1,248 @@ +"""Check the stochastic native interface and its stated limits.""" + +import gzip +import hashlib +import itertools +import json +import subprocess +import sys +import tempfile +from fractions import Fraction +from pathlib import Path + +import numpy as np + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from kernel import center, layer, monomial, native, pair, phase, route + +M = ((1, -1, 1, 1), (1, 1, -1, 1), (1, 1, 1, -1), (-1, 1, 1, 1)) + + +def need(ok, label): + if not ok: + raise ValueError(label) + + +def flatten(values): + return tuple(v for z in values for v in z) + + +def ideal_pair(values, inverse=False): + x = flatten(values) + matrix = tuple(zip(*M)) if inverse else M + return tuple(sum(a * b for a, b in zip(row, x)) for row in matrix) + + +def squared_error4(y, twice_exact): + return sum((2 * a - b) ** 2 for a, b in zip(flatten(y), twice_exact)) + + +def kernel_checks(): + count = phases = 0 + for x in itertools.product(range(-4, 5), repeat=4): + values = (x[:2], x[2:]) + p = sum(x) % 2 + for inv in (False, True): + ys = [pair(*values, s, inv) for s in (-1, 1)] + oracle = ideal_pair(values, inv) + need(tuple(a + b for a, b in zip(flatten(ys[0]), flatten(ys[1]))) == oracle, + "exact two-seed expectation") + for s, y in zip((-1, 1), ys): + need(pair(*y, s, not inv) == values, "literal two-sided inverse") + need(squared_error4(y, oracle) == 4 * p, "pointwise grid minimum") + need(tuple(y[0][j] + y[1][j] for j in (0, 1)) == + tuple(values[0][j] + values[1][j] for j in (0, 1)), "complex sum") + for unit in range(4): + need(pair(*(phase(z, unit) for z in values), s, inv) == + tuple(phase(z, unit) for z in y), "Gaussian phase covariance") + phases += 1 + count += 1 + wide = 0 + for bits in (16, 64, 257, 1024): + for signs in itertools.product((-1, 1), repeat=4): + x = tuple(s * ((1 << bits) + j) for j, s in enumerate(signs)) + for seed in (-1, 1): + values = (x[:2], x[2:]) + y = pair(*values, seed) + need(pair(*y, seed, True) == values, "wide signed inverse") + need(max(abs(a) for a in flatten(y)) <= 2 * max(map(abs, x)) + 1, "range") + wide += 1 + return {"pair_directions": count, "phase_checks": phases, "wide_pairs": wide} + + +def prefix_witness(word): + prefix = word["program"][:9896] + row = {236: Fraction(1)} + for e in reversed(prefix): + op, r = e[:2] + if op == "ADD": + row[e[2]] = row.get(e[2], Fraction(0)) + Fraction(e[3]) * row.get(r, Fraction(0)) + elif op == "SCALE": + row[r] = row.get(r, Fraction(0)) * Fraction(e[2]) + elif op in ("INIT", "CLEAR"): + row.pop(r, None) + elif op == "COPY": + value = row.pop(r, Fraction(0)) + row[e[2]] = row.get(e[2], Fraction(0)) + Fraction(e[3]) * value + else: + raise ValueError("unexpected prefix operation") + row = {r: q for r, q in row.items() if q} + source, coeff = next(iter(sorted(row.items()))) + values = {r: Fraction(0) for r in range(word["public"])} + need(source in values, "witness input is public") + need(word["initial"][source] == 3, "witness input starts in the empty frame") + values[source] = 1 / coeff + max_denominator = values[source].denominator + max_absolute = abs(values[source]) + for e in prefix: + op, r = e[:2] + if op in ("INIT", "CLEAR"): + values[r] = Fraction(0) + elif op == "ADD": + values[r] += Fraction(e[3]) * values[e[2]] + elif op == "SCALE": + values[r] *= Fraction(e[2]) + elif op == "COPY": + values[r] = Fraction(e[3]) * values[e[2]] + max_denominator = max(max_denominator, values[r].denominator) + max_absolute = max(max_absolute, abs(values[r])) + need(values[236] == 1, "reverse row agrees with literal forward prefix") + return {"input_field": source, "input_scalar": str(1 / coeff), + "coefficient": str(coeff), "row_support": len(row), "prefix_events": len(prefix), + "max_prefix_denominator": max_denominator, "max_prefix_absolute": str(max_absolute)} + + +def matrix_vector(real, imag, values): + out = [] + for r, im in zip(real, imag): + out.append((sum(int(a) * x - int(b) * y for a, b, (x, y) in zip(r, im, values)), + sum(int(a) * y + int(b) * x for a, b, (x, y) in zip(r, im, values)))) + return out + + +def native_checks(source, real, imag): + recipes = source["recipe"] + counts = {"native_basis_inputs": 0, "native_signed_inputs": 0, "tensor_seed_words": 0} + sums = hashlib.sha256() + for j in range(512): + for unit in (0, 1): + x = [(0, 0)] * 512 + x[j] = phase((1, 0), unit) + ys = [native(x, recipes, (s,)) for s in (-1, 1)] + exact = [phase((int(real[i, j]), int(imag[i, j])), unit) for i in range(512)] + need([(a + c, b + d) for (a, b), (c, d) in zip(*ys)] == exact, + "source column expectation") + for s, y in zip((-1, 1), ys): + need(native(y, recipes, (s,), True) == x, "source basis inverse") + counts["native_basis_inputs"] += 1 + for k in range(8): + x = [(((i * 17 + k) % 23 - 11) * (1 << (9 * k)), + ((i * i + 3 * k) % 19 - 9) * (1 << (5 * k))) for i in range(512)] + exact = matrix_vector(real, imag, x) + ys = [native(x, recipes, (s,)) for s in (-1, 1)] + need([(a + c, b + d) for (a, b), (c, d) in zip(*ys)] == exact, "dense native expectation") + right = monomial(x, route(recipes["right"]), 0) + odd = sum(sum(flatten(right[j:j + 2])) % 2 for j in range(0, 512, 2)) + for s, y in zip((-1, 1), ys): + need(native(y, recipes, (s,), True) == x, "dense native inverse") + need(sum((2 * a - c) ** 2 + (2 * b - d) ** 2 + for (a, b), (c, d) in zip(y, exact)) == 4 * odd, "native exact error") + sums.update(json.dumps(ys, separators=(",", ":")).encode()) + counts["native_signed_inputs"] += 1 + # A full 512**2 tensor input; the independent oracle uses a Kronecker product. + u = [((j % 5) - 2, 0) for j in range(512)] + v = [((j % 7) - 3, (j % 3) - 1) for j in range(512)] + x = [(a * c - b * d, a * d + b * c) for c, d in v for a, b in u] + au, av = matrix_vector(real, imag, u), matrix_vector(real, imag, v) + exact4 = [(a * c - b * d, a * d + b * c) for c, d in av for a, b in au] + total = [(0, 0)] * len(x) + mse16_sum = 0 + for seeds in itertools.product((-1, 1), repeat=2): + y = native(x, recipes, seeds) + need(native(y, recipes, seeds, True) == x, "full tensor inverse") + total = [(a + c, b + d) for (a, b), (c, d) in zip(total, y)] + mse16_sum += sum((4 * a - c) ** 2 + (4 * b - d) ** 2 + for (a, b), (c, d) in zip(y, exact4)) + counts["tensor_seed_words"] += 1 + need(total == exact4, "full tensor expectation") + need(mse16_sum <= 64 * len(x), "two-stage martingale second moment") + counts.update(tensor_coordinates=len(x), tensor_mse=str(Fraction(mse16_sum, 64)), + native_output_sha256=sums.hexdigest()) + unit = [(1, 0)] + [(0, 0)] * 511 + x = monomial(unit, route(recipes["right"]), 0, True) + exact = matrix_vector(real, imag, x) + need(sum(a * a + b * b for a, b in x) == 1, "native relative witness has unit norm") + for seed in (-1, 1): + y = native(x, recipes, (seed,)) + need(sum((2 * a - c) ** 2 + (2 * b - d) ** 2 + for (a, b), (c, d) in zip(y, exact)) == 4, + "actual native relative witness has unit error") + counts["relative_witness"] = [{"coordinate": j, "value": list(z)} + for j, z in enumerate(x) if z != (0, 0)] + return counts + + +def controls(): + x = ((1, 0), (0, 0)) + y = pair(*x, 1) + need(pair(*y, -1, True) != x, "wrong retained seed must fail") + need(flatten(y) != tuple(Fraction(v, 2) for v in ideal_pair(x)), "one fixed seed is biased") + exact = ideal_pair(x) + floor = tuple(v // 2 for v in exact) + need(tuple(2 * v for v in floor) != exact, "deterministic floor is not unbiased") + need(squared_error4(y, exact) == 4 and sum(v * v for v in flatten(x)) == 1, + "relative error u<1 fails on a unit grid input") + fixed_center_at_i = ((0, 0), (0, 1)) + need(fixed_center_at_i != tuple(phase(z, 1) for z in y), + "a fixed real center fails phase covariance on (i,0)") + try: + pair(*x, 0) + except ValueError: + pass + else: + raise ValueError("invalid seed accepted") + # Independent coins are enumerated before a search for a reuse witness. + witness = None + for reals in itertools.product(range(-1, 2), repeat=4): + values = [(a, 0) for a in reals] + ys = [layer(layer(values, s), t, 2) for s, t in itertools.product((-1, 1), repeat=2)] + fresh4 = [tuple(sum(z[j][c] for z in ys) for c in (0, 1)) for j in range(4)] + reused2 = [tuple(ys[0][j][c] + ys[3][j][c] for c in (0, 1)) for j in range(4)] + if any(2 * a != b for a, b in zip(flatten(reused2), flatten(fresh4))): + witness = {"input": list(reals), "fresh_mean": [str(Fraction(a, 4)) for a in flatten(fresh4)], + "reused_mean": [str(Fraction(a, 2)) for a in flatten(reused2)]} + break + need(witness is not None, "seed-reuse control needs an actual witness") + return {"semantic_controls": 7, "reused_seed_witness": witness} + + +def main(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + inputs = [x for x in sources["files"] if x["usage"] == "input"] + for item in inputs: + data = (ROOT / item["path"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == item["sha256"], "input source hash") + need(hashlib.sha256(data + b"!").hexdigest() != item["sha256"], "source corruption control") + with tempfile.TemporaryDirectory(prefix="selected-native-unbiased-") as tmp: + subprocess.run([sys.executable, "-I", "-W", "error", "-B", str(HERE / "produce.py"), tmp], + check=True, capture_output=True, text=True, timeout=120) + source = json.loads((Path(tmp) / "source.json").read_text()) + with np.load(Path(tmp) / "oracle.npz") as arrays: + real, imag = arrays["real"], arrays["imag"] + word = json.loads(gzip.decompress((ROOT / inputs[0]["path"]).read_bytes())) + result = {"source": source, "kernel": kernel_checks(), + "native": native_checks(source, real, imag), "prefix_witness": prefix_witness(word), + "controls": controls(), "source_corruption_controls": len(inputs)} + if "--write-result" in sys.argv: + (HERE / "RESULT.json").write_text(json.dumps(result, indent=2) + "\n") + else: + need(result == json.loads((HERE / "RESULT.json").read_text()), "committed result differs") + print("PASS_SELECTED_NATIVE_UNBIASED_ROUNDING") + print(json.dumps({"kernel": result["kernel"], "native": result["native"], + "prefix_witness": result["prefix_witness"], "controls": result["controls"]}, sort_keys=True)) + + +if __name__ == "__main__": + main()