From 4cc9b9719fdab59f0f33243b9c323fe4d69346f5 Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 12:57:03 -0700 Subject: [PATCH] research: certify batched R437 Count quotient tradeoff --- research/r437-batched-high-quotient/README.md | 114 ++ .../r437-batched-high-quotient/RESULT.json | 1301 +++++++++++++++++ .../r437-batched-high-quotient/SOURCES.json | 150 ++ research/r437-batched-high-quotient/TASK.json | 91 ++ .../r437-batched-high-quotient/VERIFY.json | 54 + .../r437-batched-high-quotient/adapter.py | 41 + research/r437-batched-high-quotient/verify.py | 111 ++ 7 files changed, 1862 insertions(+) create mode 100644 research/r437-batched-high-quotient/README.md create mode 100644 research/r437-batched-high-quotient/RESULT.json create mode 100644 research/r437-batched-high-quotient/SOURCES.json create mode 100644 research/r437-batched-high-quotient/TASK.json create mode 100644 research/r437-batched-high-quotient/VERIFY.json create mode 100644 research/r437-batched-high-quotient/adapter.py create mode 100644 research/r437-batched-high-quotient/verify.py diff --git a/research/r437-batched-high-quotient/README.md b/research/r437-batched-high-quotient/README.md new file mode 100644 index 0000000000..65ea601dbe --- /dev/null +++ b/research/r437-batched-high-quotient/README.md @@ -0,0 +1,114 @@ +# Batched high-factor binary Count quotient: a scoped tradeoff + +This opt-in adapter refines the actual `fresh_rows.quotient` on **valid fixed +contexts**: prime q, dimension m≥1, encoded modulus q^w with w≥1, positive family +factor F and GL low count G. It replaces m² traversals of the encoded radix +iterator and m²(w−1) divisions by q with one radix traversal and w−1 divisions by +the compiled constant C=q^(m²). It retains binary Count inputs and outputs and +never decodes runtime w. The actual four-statement `Machine.node` quotient/save/ +stock guard and its real `save_count`/`commit` bodies are executed unchanged. + +**This is a finite execution and fixed-context refinement, not an unconditional +physical speedup.** C has 6,493 bits already at q=3,m=64, with C possible remainder +states. The compile/setup and wide arithmetic bill cannot be treated as free. +The default backend, frozen caller and selected frontier remain unchanged. + +## Refinement and ownership + +After the identical F and G divisions, let N be the remaining positive Count. +The original accepts the high part iff q^(m²(w−1)) divides N. Successive exact +q-divisions and successive exact C-divisions have the same final quotient, +because C^(w−1)=q^(m²(w−1)); a first failing intermediate division in either +implementation implies failure of the same aggregate divisibility. Both use the +same `complete fresh high factor` error class. For w=1 both do no high division, +though the original still traverses the radix iterator m² times. Positivity and +F/G checks are unchanged. The literal local guard then accepts exactly when the +returned quotient is divisible by the same stock_multiple; that does not claim +the node has executed its payload or later recursion. + +The adapter closes its owned Count on ValueError. Both original and adapted +paths preserve the borrowed Count and restore numeric live sets on valid +contexts, including rejected fresh/F/G/high/local-stock inputs. The harness +copies the source AST for only the four quotient/guard statements and the two +save helpers, not full Machine.node. Ordinary Count-backed record tapes are +used; `Lease=()` disables the unrelated Lease-return branch of commit. The +same actual code consumes the candidate and baseline outputs. + +The malformed-modulus control (8 in a purported q3,w2 context) is deliberately +**outside this theorem**. The unchanged `radix_power` need-failure leaks two +numeric slots in both versions before its normal frees. The receipt explicitly +records numeric_restored=false and two leaked slots; the harness performs +`arena.rollback` solely to clean its diagnostic fixture. This is not a runtime +repair or successful cleanup claim for invalid contexts. + +## Complete bill and what the measurements mean + +For each actual Count division the external observer records input bit width, +divisor width, and the number of possible remainder states (hashed integer +receipt). It calls the unchanged `Natural.divide_small`. After each input bit, +that source doubles/adds a bit, compares with the divisor, and conditionally +subtracts it. The pre-subtraction temporary is below 2C. Thus C states require +ceil(log2 C) bits, and transient control needs at most one additional bit. The +receipt's `B*(4*b+8)` is a diagnostic linear-bit-work proxy for B input bits +and a b-bit divisor. The four-linear-scan coefficient is an accounting choice, +not a proved binary-Turing-machine step bound. The source arithmetic admits an +O(Bb) bitwise implementation once its ripple primitives and storage are fixed; +this package does not supply that implementation. The proxy is **not a measured +host-operation count** or a calibrated physical-tape implementation. Count normalization and head +movement remain separately charged in the exact tape meters. The already-large +G division and the final stock_multiple division are included in both invoices. + +Constant construction uses an explicit square-and-multiply sequence. The +receipt lists every multiplication's operand widths, multiplication count, +Σ operand-width products (schoolbook bit-product units), and stored divisor +width. This provides an implementable construction bill; native Python big-int +multiplication is not charged as a unit-time physical operation. At m64 it takes +13 products with 14,066,186 schoolbook bit products and stores 6,493 bits. A +finite-state implementation that literally compiles all remainders has C states, +not merely 6,493 states. A binary-state implementation must implement and charge +its comparisons/subtractions instead. Neither representation is free. + +At m64,w1 the observed Count record bill is identical (755,782 actions), while +residue actions fall from 4,808,704 to 1,174. However, an unamortized charge of one +unit per stated schoolbook bit product already exceeds that saving. This is a +concrete setup/scan tradeoff, not a net improvement claim. Compile-once reuse +may amortize setup, but still must pay the wide divider's runtime implementation. +A conditional saving requires saved tape/encoded-radix cost to exceed the extra +compile, storage/control and wide arithmetic cost in one explicitly chosen +machine model. This package does not prove that inequality uniformly. + +Matched physical replays cover m2,w1/2/3; m4,w2; and real m64,w1. A candidate-only +real m64,w2 execution uses R=9475*(28416*|GL64(F3)|*3^4096)^2 and returns R/A, +then passes the actual local 9475 guard. The original m64,w2 full replay is not +run; equality there follows from the scoped arithmetic refinement, not a measured +baseline. Full receipts include all divisions and separate record/residue lanes. +No field payload, production rows, root admission or supplier budget is run. + +## Sources, reproduction and credit + +The actual quotient/Count code is David Arias's PR2753 predecessor; ToikY's +`source-directory-setup-cost` identified repeated high-power/radix traversal +costs. #4757 (5dba1acc2ef67e65e6a40e963f727b01edc5e132) covers sharp host entry +and explicitly leaves real binary Count execution open; the present work does +not repeat the 9475 factor proof or change that entry guard. NickPetalas #3246, +Tekalign #3264, Mihir #4685, and codyw912 #4734 retain predecessor credit for the +stock invariant and adapters. All 23 declared inputs are SHA256/git-blob bound +at canonical base 624de9dc66858af0945e5f8a0942488d62280d43 and checked before imports. +The new adapter and harness are Brian (JoyboyBrian), substantial OpenAI Codex +assistance, Apache-2.0. No frozen source was edited. + +Run `python3.12 -I -B research/r437-batched-high-quotient/verify.py`, also with +`-O`; both are registered in VERIFY.json. Explicit checks survive optimization, +and JSON typed receipt equality distinguishes booleans from integers. Results +are author-checked; no formal-kernel or hosted-CI acceptance is asserted. + +## Open next questions + +1. Implement and meter a binary large-constant divider or explicitly priced + finite controller, then determine the setup-amortization crossover. +2. Compare this batch with a shared radix traversal that retains q-divisions, + which may avoid large-controller setup while preserving residue savings. +3. Fix the inherited out-of-domain radix iterator cleanup in a separate scoped + package, preserving its accepted-domain and rejection behavior. +4. Join the encoded quotient to admitted root rows and full caller payload before + claiming complete R437 supplier admission. diff --git a/research/r437-batched-high-quotient/RESULT.json b/research/r437-batched-high-quotient/RESULT.json new file mode 100644 index 0000000000..8f399e2cc5 --- /dev/null +++ b/research/r437-batched-high-quotient/RESULT.json @@ -0,0 +1,1301 @@ +{ + "cases": [ + { + "candidate_count_high_passes": 0, + "candidate_radix_traversals": 1, + "construction": { + "multiplications": 3, + "operand_bit_pairs": [ + [ + 2, + 2 + ], + [ + 4, + 4 + ], + [ + 1, + 7 + ] + ], + "schoolbook_bit_products": 27, + "stored_divisor_bits": 7 + }, + "dimension": 2, + "high_factor_bits": 7, + "high_remainder_bits": 7, + "old_q_remainder_bits": 2, + "q": 3, + "results": [ + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 1072, + "divisions": [ + { + "divisor_bits": 3, + "input_bits": 18, + "linear_bit_proxy": 360, + "remainder_states": { + "bits": 3, + "sha256": "e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71" + } + }, + { + "divisor_bits": 6, + "input_bits": 16, + "linear_bit_proxy": 512, + "remainder_states": { + "bits": 6, + "sha256": "5feceb66ffc86f38d952786c6d696c79c2dbc239dd4e91b46729d73a27fb57e9" + } + }, + { + "divisor_bits": 3, + "input_bits": 10, + "linear_bit_proxy": 200, + "remainder_states": { + "bits": 3, + "sha256": "e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 10, + "sha256": "1f5c65186bd477aaa4180428209a0367735b83a7f227bf9beaa943d366ef8abc" + }, + "record": { + "moves": 522, + "reads": 573, + "writes": 125 + }, + "residue": { + "moves": 2224, + "reads": 2092, + "writes": 380 + }, + "temporary_backing_erased": true, + "version": "original" + }, + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 1072, + "divisions": [ + { + "divisor_bits": 3, + "input_bits": 18, + "linear_bit_proxy": 360, + "remainder_states": { + "bits": 3, + "sha256": "e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71" + } + }, + { + "divisor_bits": 6, + "input_bits": 16, + "linear_bit_proxy": 512, + "remainder_states": { + "bits": 6, + "sha256": "5feceb66ffc86f38d952786c6d696c79c2dbc239dd4e91b46729d73a27fb57e9" + } + }, + { + "divisor_bits": 3, + "input_bits": 10, + "linear_bit_proxy": 200, + "remainder_states": { + "bits": 3, + "sha256": "e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 10, + "sha256": "1f5c65186bd477aaa4180428209a0367735b83a7f227bf9beaa943d366ef8abc" + }, + "record": { + "moves": 522, + "reads": 573, + "writes": 125 + }, + "residue": { + "moves": 556, + "reads": 523, + "writes": 95 + }, + "temporary_backing_erased": true, + "version": "batched" + } + ], + "rows": { + "bits": 18, + "sha256": "3efefa0fb21db8b6674639d4f693b0c73b028305904be8048b2f46e75326deab" + }, + "source_count_high_passes": 0, + "source_radix_traversals": 4, + "w": 1 + }, + { + "candidate_count_high_passes": 1, + "candidate_radix_traversals": 1, + "construction": { + "multiplications": 3, + "operand_bit_pairs": [ + [ + 2, + 2 + ], + [ + 4, + 4 + ], + [ + 1, + 7 + ] + ], + "schoolbook_bit_products": 27, + "stored_divisor_bits": 7 + }, + "dimension": 2, + "high_factor_bits": 7, + "high_remainder_bits": 7, + "old_q_remainder_bits": 2, + "q": 3, + "results": [ + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 3216, + "divisions": [ + { + "divisor_bits": 3, + "input_bits": 31, + "linear_bit_proxy": 620, + "remainder_states": { + "bits": 3, + "sha256": "e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71" + } + }, + { + "divisor_bits": 6, + "input_bits": 29, + "linear_bit_proxy": 928, + "remainder_states": { + "bits": 6, + "sha256": "5feceb66ffc86f38d952786c6d696c79c2dbc239dd4e91b46729d73a27fb57e9" + } + }, + { + "divisor_bits": 2, + "input_bits": 23, + "linear_bit_proxy": 368, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 22, + "linear_bit_proxy": 352, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 20, + "linear_bit_proxy": 320, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 18, + "linear_bit_proxy": 288, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 3, + "input_bits": 17, + "linear_bit_proxy": 340, + "remainder_states": { + "bits": 3, + "sha256": "e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 17, + "sha256": "f4a83119b7579e106465ea81c9c9cdb2f555787fe7386e630b001b98c7d523dd" + }, + "record": { + "moves": 1206, + "reads": 1382, + "writes": 295 + }, + "residue": { + "moves": 7456, + "reads": 7256, + "writes": 1376 + }, + "temporary_backing_erased": true, + "version": "original" + }, + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 2716, + "divisions": [ + { + "divisor_bits": 3, + "input_bits": 31, + "linear_bit_proxy": 620, + "remainder_states": { + "bits": 3, + "sha256": "e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71" + } + }, + { + "divisor_bits": 6, + "input_bits": 29, + "linear_bit_proxy": 928, + "remainder_states": { + "bits": 6, + "sha256": "5feceb66ffc86f38d952786c6d696c79c2dbc239dd4e91b46729d73a27fb57e9" + } + }, + { + "divisor_bits": 7, + "input_bits": 23, + "linear_bit_proxy": 828, + "remainder_states": { + "bits": 7, + "sha256": "4ae81572f06e1b88fd5ced7a1a000945432e83e1551e6f721ee9c00b8cc33260" + } + }, + { + "divisor_bits": 3, + "input_bits": 17, + "linear_bit_proxy": 340, + "remainder_states": { + "bits": 3, + "sha256": "e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 17, + "sha256": "f4a83119b7579e106465ea81c9c9cdb2f555787fe7386e630b001b98c7d523dd" + }, + "record": { + "moves": 942, + "reads": 1061, + "writes": 235 + }, + "residue": { + "moves": 1864, + "reads": 1814, + "writes": 344 + }, + "temporary_backing_erased": true, + "version": "batched" + } + ], + "rows": { + "bits": 31, + "sha256": "edb904ff4ce0beba26ed31b4d7bafd949aa510fe400dbdffc2a02b5e312668d9" + }, + "source_count_high_passes": 4, + "source_radix_traversals": 4, + "w": 2 + }, + { + "candidate_count_high_passes": 2, + "candidate_radix_traversals": 1, + "construction": { + "multiplications": 3, + "operand_bit_pairs": [ + [ + 2, + 2 + ], + [ + 4, + 4 + ], + [ + 1, + 7 + ] + ], + "schoolbook_bit_products": 27, + "stored_divisor_bits": 7 + }, + "dimension": 2, + "high_factor_bits": 7, + "high_remainder_bits": 7, + "old_q_remainder_bits": 2, + "q": 3, + "results": [ + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 6504, + "divisions": [ + { + "divisor_bits": 3, + "input_bits": 43, + "linear_bit_proxy": 860, + "remainder_states": { + "bits": 3, + "sha256": "e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71" + } + }, + { + "divisor_bits": 6, + "input_bits": 41, + "linear_bit_proxy": 1312, + "remainder_states": { + "bits": 6, + "sha256": "5feceb66ffc86f38d952786c6d696c79c2dbc239dd4e91b46729d73a27fb57e9" + } + }, + { + "divisor_bits": 2, + "input_bits": 36, + "linear_bit_proxy": 576, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 34, + "linear_bit_proxy": 544, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 33, + "linear_bit_proxy": 528, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 31, + "linear_bit_proxy": 496, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 29, + "linear_bit_proxy": 464, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 28, + "linear_bit_proxy": 448, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 26, + "linear_bit_proxy": 416, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 25, + "linear_bit_proxy": 400, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 3, + "input_bits": 23, + "linear_bit_proxy": 460, + "remainder_states": { + "bits": 3, + "sha256": "e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 23, + "sha256": "1e415600c1879d39ff812f3f0d87b980dc3be3cf1e18d0b155ed3a0817ca830c" + }, + "record": { + "moves": 2162, + "reads": 2537, + "writes": 531 + }, + "residue": { + "moves": 13936, + "reads": 13708, + "writes": 2632 + }, + "temporary_backing_erased": true, + "version": "original" + }, + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 4972, + "divisions": [ + { + "divisor_bits": 3, + "input_bits": 43, + "linear_bit_proxy": 860, + "remainder_states": { + "bits": 3, + "sha256": "e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71" + } + }, + { + "divisor_bits": 6, + "input_bits": 41, + "linear_bit_proxy": 1312, + "remainder_states": { + "bits": 6, + "sha256": "5feceb66ffc86f38d952786c6d696c79c2dbc239dd4e91b46729d73a27fb57e9" + } + }, + { + "divisor_bits": 7, + "input_bits": 36, + "linear_bit_proxy": 1296, + "remainder_states": { + "bits": 7, + "sha256": "4ae81572f06e1b88fd5ced7a1a000945432e83e1551e6f721ee9c00b8cc33260" + } + }, + { + "divisor_bits": 7, + "input_bits": 29, + "linear_bit_proxy": 1044, + "remainder_states": { + "bits": 7, + "sha256": "4ae81572f06e1b88fd5ced7a1a000945432e83e1551e6f721ee9c00b8cc33260" + } + }, + { + "divisor_bits": 3, + "input_bits": 23, + "linear_bit_proxy": 460, + "remainder_states": { + "bits": 3, + "sha256": "e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 23, + "sha256": "1e415600c1879d39ff812f3f0d87b980dc3be3cf1e18d0b155ed3a0817ca830c" + }, + "record": { + "moves": 1406, + "reads": 1610, + "writes": 354 + }, + "residue": { + "moves": 3484, + "reads": 3427, + "writes": 658 + }, + "temporary_backing_erased": true, + "version": "batched" + } + ], + "rows": { + "bits": 43, + "sha256": "1f2c2e7c1c307ab6d50b9280cbea466cd2e9164a2d4f8f4f073b82373bffc33f" + }, + "source_count_high_passes": 8, + "source_radix_traversals": 4, + "w": 3 + }, + { + "candidate_count_high_passes": 1, + "candidate_radix_traversals": 1, + "construction": { + "multiplications": 5, + "operand_bit_pairs": [ + [ + 2, + 2 + ], + [ + 4, + 4 + ], + [ + 7, + 7 + ], + [ + 13, + 13 + ], + [ + 1, + 26 + ] + ], + "schoolbook_bit_products": 264, + "stored_divisor_bits": 26 + }, + "dimension": 4, + "high_factor_bits": 26, + "high_remainder_bits": 26, + "old_q_remainder_bits": 2, + "q": 3, + "results": [ + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 32020, + "divisions": [ + { + "divisor_bits": 3, + "input_bits": 107, + "linear_bit_proxy": 2140, + "remainder_states": { + "bits": 3, + "sha256": "e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71" + } + }, + { + "divisor_bits": 25, + "input_bits": 105, + "linear_bit_proxy": 11340, + "remainder_states": { + "bits": 25, + "sha256": "3e040209cbb4d446987f5a0e07ffdf6af5b347bdb6af584830860b3c53a2cc2d" + } + }, + { + "divisor_bits": 2, + "input_bits": 80, + "linear_bit_proxy": 1280, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 78, + "linear_bit_proxy": 1248, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 77, + "linear_bit_proxy": 1232, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 75, + "linear_bit_proxy": 1200, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 74, + "linear_bit_proxy": 1184, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 72, + "linear_bit_proxy": 1152, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 71, + "linear_bit_proxy": 1136, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 69, + "linear_bit_proxy": 1104, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 67, + "linear_bit_proxy": 1072, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 66, + "linear_bit_proxy": 1056, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 64, + "linear_bit_proxy": 1024, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 63, + "linear_bit_proxy": 1008, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 61, + "linear_bit_proxy": 976, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 59, + "linear_bit_proxy": 944, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 58, + "linear_bit_proxy": 928, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 2, + "input_bits": 56, + "linear_bit_proxy": 896, + "remainder_states": { + "bits": 2, + "sha256": "084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5" + } + }, + { + "divisor_bits": 3, + "input_bits": 55, + "linear_bit_proxy": 1100, + "remainder_states": { + "bits": 3, + "sha256": "e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 55, + "sha256": "3554d245b7d952d1ed7f5cec26b890070fc00d716fa7c34c957372fa7cd6335b" + }, + "record": { + "moves": 7154, + "reads": 8591, + "writes": 1796 + }, + "residue": { + "moves": 29824, + "reads": 29024, + "writes": 5504 + }, + "temporary_backing_erased": true, + "version": "original" + }, + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 23540, + "divisions": [ + { + "divisor_bits": 3, + "input_bits": 107, + "linear_bit_proxy": 2140, + "remainder_states": { + "bits": 3, + "sha256": "e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71" + } + }, + { + "divisor_bits": 25, + "input_bits": 105, + "linear_bit_proxy": 11340, + "remainder_states": { + "bits": 25, + "sha256": "3e040209cbb4d446987f5a0e07ffdf6af5b347bdb6af584830860b3c53a2cc2d" + } + }, + { + "divisor_bits": 26, + "input_bits": 80, + "linear_bit_proxy": 8960, + "remainder_states": { + "bits": 26, + "sha256": "fd8f53b18ebc9d389f52d5db4daa64694c8c924946acde84d1141705a5362d20" + } + }, + { + "divisor_bits": 3, + "input_bits": 55, + "linear_bit_proxy": 1100, + "remainder_states": { + "bits": 3, + "sha256": "e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 55, + "sha256": "3554d245b7d952d1ed7f5cec26b890070fc00d716fa7c34c957372fa7cd6335b" + }, + "record": { + "moves": 2994, + "reads": 3436, + "writes": 786 + }, + "residue": { + "moves": 1864, + "reads": 1814, + "writes": 344 + }, + "temporary_backing_erased": true, + "version": "batched" + } + ], + "rows": { + "bits": 107, + "sha256": "e39510b869f30d4092aefd3c7503e75fa8004bc335f7057f417a86caaf013e91" + }, + "source_count_high_passes": 16, + "source_radix_traversals": 16, + "w": 2 + }, + { + "candidate_count_high_passes": 0, + "candidate_radix_traversals": 1, + "construction": { + "multiplications": 13, + "operand_bit_pairs": [ + [ + 2, + 2 + ], + [ + 4, + 4 + ], + [ + 7, + 7 + ], + [ + 13, + 13 + ], + [ + 26, + 26 + ], + [ + 51, + 51 + ], + [ + 102, + 102 + ], + [ + 203, + 203 + ], + [ + 406, + 406 + ], + [ + 812, + 812 + ], + [ + 1624, + 1624 + ], + [ + 3247, + 3247 + ], + [ + 1, + 6493 + ] + ], + "schoolbook_bit_products": 14066186, + "stored_divisor_bits": 6493 + }, + "dimension": 64, + "high_factor_bits": 6493, + "high_remainder_bits": 6493, + "old_q_remainder_bits": 2, + "q": 3, + "results": [ + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 339276784, + "divisions": [ + { + "divisor_bits": 15, + "input_bits": 13026, + "linear_bit_proxy": 885768, + "remainder_states": { + "bits": 15, + "sha256": "3541e98bd04b5587b9c1918d8abed88bded9328de3fedd36e856d151cb05383e" + } + }, + { + "divisor_bits": 6492, + "input_bits": 13011, + "linear_bit_proxy": 337973736, + "remainder_states": { + "bits": 6492, + "sha256": "d57ec5ba42197bb1d323c42204a8463632fe05ad622f12102f775248b120103b" + } + }, + { + "divisor_bits": 14, + "input_bits": 6520, + "linear_bit_proxy": 417280, + "remainder_states": { + "bits": 14, + "sha256": "b184d29a1c103b5269165d679d2460bdc54ed484d57a4716800bfba78ae036ff" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 6520, + "sha256": "b4b2fab41fd0a7ab8f92729e4049ab786f2b7de7db4938ba58754e3ce4c38be3" + }, + "record": { + "moves": 312758, + "reads": 358330, + "writes": 84694 + }, + "residue": { + "moves": 2277376, + "reads": 2142208, + "writes": 389120 + }, + "temporary_backing_erased": true, + "version": "original" + }, + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 339276784, + "divisions": [ + { + "divisor_bits": 15, + "input_bits": 13026, + "linear_bit_proxy": 885768, + "remainder_states": { + "bits": 15, + "sha256": "3541e98bd04b5587b9c1918d8abed88bded9328de3fedd36e856d151cb05383e" + } + }, + { + "divisor_bits": 6492, + "input_bits": 13011, + "linear_bit_proxy": 337973736, + "remainder_states": { + "bits": 6492, + "sha256": "d57ec5ba42197bb1d323c42204a8463632fe05ad622f12102f775248b120103b" + } + }, + { + "divisor_bits": 14, + "input_bits": 6520, + "linear_bit_proxy": 417280, + "remainder_states": { + "bits": 14, + "sha256": "b184d29a1c103b5269165d679d2460bdc54ed484d57a4716800bfba78ae036ff" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 6520, + "sha256": "b4b2fab41fd0a7ab8f92729e4049ab786f2b7de7db4938ba58754e3ce4c38be3" + }, + "record": { + "moves": 312758, + "reads": 358330, + "writes": 84694 + }, + "residue": { + "moves": 556, + "reads": 523, + "writes": 95 + }, + "temporary_backing_erased": true, + "version": "batched" + } + ], + "rows": { + "bits": 13026, + "sha256": "f6486467b3786a1ede2b2b53d2347c31871ee6d2ccaa2b22dda1d07c82d03d30" + }, + "source_count_high_passes": 0, + "source_radix_traversals": 4096, + "w": 1 + }, + { + "candidate_count_high_passes": 1, + "candidate_radix_traversals": 1, + "construction": { + "multiplications": 13, + "operand_bit_pairs": [ + [ + 2, + 2 + ], + [ + 4, + 4 + ], + [ + 7, + 7 + ], + [ + 13, + 13 + ], + [ + 26, + 26 + ], + [ + 51, + 51 + ], + [ + 102, + 102 + ], + [ + 203, + 203 + ], + [ + 406, + 406 + ], + [ + 812, + 812 + ], + [ + 1624, + 1624 + ], + [ + 3247, + 3247 + ], + [ + 1, + 6493 + ] + ], + "schoolbook_bit_products": 14066186, + "stored_divisor_bits": 6493 + }, + "dimension": 64, + "high_factor_bits": 6493, + "high_remainder_bits": 6493, + "old_q_remainder_bits": 2, + "q": 3, + "results": [ + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 1184561488, + "divisions": [ + { + "divisor_bits": 15, + "input_bits": 26010, + "linear_bit_proxy": 1768680, + "remainder_states": { + "bits": 15, + "sha256": "3541e98bd04b5587b9c1918d8abed88bded9328de3fedd36e856d151cb05383e" + } + }, + { + "divisor_bits": 6492, + "input_bits": 25995, + "linear_bit_proxy": 675246120, + "remainder_states": { + "bits": 6492, + "sha256": "d57ec5ba42197bb1d323c42204a8463632fe05ad622f12102f775248b120103b" + } + }, + { + "divisor_bits": 6493, + "input_bits": 19504, + "linear_bit_proxy": 506713920, + "remainder_states": { + "bits": 6493, + "sha256": "4acde110321e89dc1be1c4b81709f91e8298a1bbff8c80d0d86adaf5b112eac2" + } + }, + { + "divisor_bits": 14, + "input_bits": 13012, + "linear_bit_proxy": 832768, + "remainder_states": { + "bits": 14, + "sha256": "b184d29a1c103b5269165d679d2460bdc54ed484d57a4716800bfba78ae036ff" + } + } + ], + "error": null, + "invalid_context_leaked_slots": 0, + "numeric_restored": true, + "quotient": { + "bits": 13012, + "sha256": "f1ea55a14de9636ab49aada28027a2a4152a6a40fe00771060867a36f1a30e31" + }, + "record": { + "moves": 702398, + "reads": 812917, + "writes": 188594 + }, + "residue": { + "moves": 1864, + "reads": 1814, + "writes": 344 + }, + "temporary_backing_erased": true, + "version": "batched" + } + ], + "rows": { + "bits": 26010, + "sha256": "fb854591452036d2cbacbaad05d441a36f7f0f8434c7b8f185c9b877811d15b2" + }, + "source_count_high_passes": 4096, + "source_radix_traversals": 4096, + "w": 2 + } + ], + "live_inputs": 23, + "node_guard_ast_sha256": "84d9ed7a1cdd5678fc3e419aac9a5710b9407181127e69ae22000de0d9716c27", + "rejections": [ + { + "error": "independent positive cardinality tape", + "name": "zero" + }, + { + "error": "complete fresh family factor", + "name": "family" + }, + { + "error": "complete fresh GL low factor", + "name": "GL" + }, + { + "error": "complete fresh high factor", + "name": "high" + }, + { + "error": "compatible fresh stock factor", + "name": "local_stock" + }, + { + "error": "compatible fresh stock factor", + "name": "missing_9475" + }, + { + "error": "cardinality prime-power context", + "harness_rollback": true, + "name": "non_power_modulus", + "outside_theorem": true, + "results": [ + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 1548, + "divisions": [ + { + "divisor_bits": 3, + "input_bits": 31, + "linear_bit_proxy": 620, + "remainder_states": { + "bits": 3, + "sha256": "e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71" + } + }, + { + "divisor_bits": 6, + "input_bits": 29, + "linear_bit_proxy": 928, + "remainder_states": { + "bits": 6, + "sha256": "5feceb66ffc86f38d952786c6d696c79c2dbc239dd4e91b46729d73a27fb57e9" + } + } + ], + "error": "cardinality prime-power context", + "invalid_context_leaked_slots": 2, + "numeric_restored": false, + "quotient": null, + "record": { + "moves": 526, + "reads": 596, + "writes": 132 + }, + "residue": { + "moves": 910, + "reads": 880, + "writes": 179 + }, + "temporary_backing_erased": true, + "version": "original" + }, + { + "borrowed_preserved": true, + "division_linear_bit_proxy": 1548, + "divisions": [ + { + "divisor_bits": 3, + "input_bits": 31, + "linear_bit_proxy": 620, + "remainder_states": { + "bits": 3, + "sha256": "e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71" + } + }, + { + "divisor_bits": 6, + "input_bits": 29, + "linear_bit_proxy": 928, + "remainder_states": { + "bits": 6, + "sha256": "5feceb66ffc86f38d952786c6d696c79c2dbc239dd4e91b46729d73a27fb57e9" + } + } + ], + "error": "cardinality prime-power context", + "invalid_context_leaked_slots": 2, + "numeric_restored": false, + "quotient": null, + "record": { + "moves": 526, + "reads": 596, + "writes": 132 + }, + "residue": { + "moves": 910, + "reads": 880, + "writes": 179 + }, + "temporary_backing_erased": true, + "version": "batched" + } + ] + } + ], + "scope": "Fixed-context binary Count refinement and lane invoice; enlarged finite control charged separately; no uniform time or supplier admission.", + "status": "PASS_R437_BATCHED_HIGH_QUOTIENT" +} diff --git a/research/r437-batched-high-quotient/SOURCES.json b/research/r437-batched-high-quotient/SOURCES.json new file mode 100644 index 0000000000..31dd6b354d --- /dev/null +++ b/research/r437-batched-high-quotient/SOURCES.json @@ -0,0 +1,150 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/cardinal_counts.py", + "usage": "input", + "git_blob": "6a14feac45094ae9156e8c2c982d6727544f180e", + "sha256": "59ddeac102a0cc51fa49b15aae6aeb68cd68ed217fa974ce916372a177d2ec8f" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/fresh_rows.py", + "usage": "input", + "git_blob": "aa3a327604308d3a5c7a27b65f5e631d430ab093", + "sha256": "e4ae08fbd658add630eb7754ebe0cbcb42c6f39cf4128f9cb92e27fcf5213a7d" + }, + { + "path": "research/selected-bit-physical-caller/PROOF.md", + "usage": "input", + "git_blob": "548ecff3ef79a32c14bafc7f2309781181d3c23d", + "sha256": "e5a827e93fe313ba9bf4a2e300bae01b58b28004aa8a8ee119cf6d950edd9f93" + }, + { + "path": "research/selected-bit-physical-caller/macro_binding.py", + "usage": "input", + "git_blob": "c197eb6458be9374cb4684c654bfc99e619dcaf0", + "sha256": "9ef31765d03d2c54fad9296f2ff0707a190ce169e44de4f0f45214e3c410c01a" + }, + { + "path": "research/selected-bit-physical-caller/macro_machine.py", + "usage": "input", + "git_blob": "5a032e8923f7f8b22bb98f3e39b804beb9906c16", + "sha256": "7bc6e42072a09a08ac961e05c3da01cde012d740d4b4c605f298d994f2ad7c5a" + }, + { + "path": "research/selected-bit-recursive-caller/PROOF.md", + "usage": "input", + "git_blob": "1a08e57eac2a37764066d31baa3ecd3769759158", + "sha256": "552fa306d5cc228f4d8d8553f8ac5fc6a738ef2b66a2cb765ba0638cd229794d" + }, + { + "path": "research/selected-bit-recursive-caller/driver.py", + "usage": "input", + "git_blob": "5b7846a70aada53d87480b337e1c04217118771b", + "sha256": "ceaf8f75de9810a05ebf8f65780b6f8bd7599a5768401d5e4386182afe615cdf" + }, + { + "path": "research/selected-bit-recursive-caller/node.py", + "usage": "input", + "git_blob": "28c98a3573b458f7a055678d70b602b80e6e959e", + "sha256": "0bd4f640cafb5c8f070c161d86445910f77578a672bf5886936ed89e7f6bd21b" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/cardinal_counts.py", + "usage": "input", + "git_blob": "6a14feac45094ae9156e8c2c982d6727544f180e", + "sha256": "59ddeac102a0cc51fa49b15aae6aeb68cd68ed217fa974ce916372a177d2ec8f" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/fresh_rows.py", + "usage": "input", + "git_blob": "aa3a327604308d3a5c7a27b65f5e631d430ab093", + "sha256": "e4ae08fbd658add630eb7754ebe0cbcb42c6f39cf4128f9cb92e27fcf5213a7d" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/vendor/bitstream.py", + "usage": "input", + "git_blob": "4d1fd4abb0f2aabe833e5cbc9efb51039739e7ca", + "sha256": "f78bac9641007dbd8824984edcac057274fe016ce78bd9cb512d0c0913274783" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/vendor/cardinality.py", + "usage": "input", + "git_blob": "b8ba857e32c5903408e1e61ff916300848b4a208", + "sha256": "505d5e560c5a507e6184edcc19a87cf1fed243eb34a5cb21fbe1e4fe017e7f22" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/vendor/counts.py", + "usage": "input", + "git_blob": "81b48940ce222290a40d4fb349ce827f4788469d", + "sha256": "00b476dbda0e8cc99886bf794439e1cb9e775f435f599a3557e99321fe084069" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/vendor/directory.py", + "usage": "input", + "git_blob": "c74cacf5ce809c0561d374f137a52df0992b4226", + "sha256": "4270e370b2bfe38ef73aadcd97d1b3496b56bd582115d74331eb9e5ceb90bec7" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/vendor/matrices.py", + "usage": "input", + "git_blob": "5d497353efbb9eeaaf4facd96ab40ffb0f3aa20d", + "sha256": "00b687434039b54529ee092e34f9435cfcd66e0816eb3bd2a6688c73f4e01459" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/vendor/oracle.py", + "usage": "input", + "git_blob": "244f131466698a3ace10b657242fe1f65c07fd1f", + "sha256": "7bd18089e32ce48085b5e3a75159f6a82cdb2649ec682c53db05e399d97aef67" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/vendor/records.py", + "usage": "input", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/vendor/routes.py", + "usage": "input", + "git_blob": "35531201dc349a811dfabc6f1f6e64697d665194", + "sha256": "ed7dc3679451696ab1dd841146b215c9515a3eec5e4ff3763f33c315f1696ada" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/vendor/stream.py", + "usage": "input", + "git_blob": "5e5a4bb0f98971447043e25d4dd6991bfc070389", + "sha256": "c7dc7da5b00f27016982ada4c0416f8328568b00df16d97012f33d4b372d79b5" + }, + { + "path": "research/selected-bit-recursive-caller/predecessor/vendor/words.py", + "usage": "input", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9" + }, + { + "path": "research/selected-bit-recursive-caller/recursive_call.py", + "usage": "input", + "git_blob": "6d33224145aa04f7fbaf7b6cda7c9c164311a402", + "sha256": "157deaa5972557893d43494a81151483bdc46373448ec677cb6a738c9b7e6f1e" + }, + { + "path": "research/selected-live-row-divisor/README.md", + "usage": "input", + "git_blob": "a0303f03ebdf8427445fc5b4ae3083e762e18f98", + "sha256": "361424cba2b70d82e7d96a094db9051a11bbea2fa7484990e2ca07292c5daead" + }, + { + "path": "research/selected-live-row-divisor/sources/pr2234/NOTICE.md", + "usage": "input", + "git_blob": "a5ccfbecbd225d4b63d9ce85edb2fac90f37147c", + "sha256": "c144e34c24470ca53df77527b9687ae9b345a4d88a506d839312ca26584cfe79" + } + ] +} diff --git a/research/r437-batched-high-quotient/TASK.json b/research/r437-batched-high-quotient/TASK.json new file mode 100644 index 0000000000..d499541857 --- /dev/null +++ b/research/r437-batched-high-quotient/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "r437-carrier-integration", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "r437-carrier-integration", + "question": "Can the paid R437 two-window carrier improvement be admitted by the actual pooled compiler and physical caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/r437-two-window-carrier/README.md", + "research/r437-reverse-row-coefficient/README.md" + ], + "methods": [ + "Close one compiler/request, caller or precision/stock implication for the pinned paid exchange.", + "Falsify that exact interface with an arbitrary-dirty-state or chronology counterexample." + ], + "acceptance_gate": "Pin the complete source and destination contracts, exact paid and scalar deltas, and all remaining assumptions. A local moment gain is not a physical or all-size supplier admission.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4067 paid profile and open integration obligations; #4147 covers the reverse row coefficient. Three additional ADDs per call and all helpers remain charged. This is not a selected supplier.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Choose one unclaimed obligation: pooled compiler codebook/request alignment, actual physical caller, or precision/stock envelope using the already reported reverse coefficient. Pin the input and receiver, preserve dirty/source windows, and test one binding with a rejection control. Stop at unresolved dependencies; do not rederive the coefficient or quote the local moment as a completed bound.", + "bottleneck_link": "The exchange changes the paid profile; integration must establish that its gain survives the complete caller.", + "allowed_variations": [ + "One compiler rebind, one actual caller boundary, or one precision/stock implication." + ], + "scope_change_triggers": [ + "Ignoring added ADDs, retaining an obsolete reverse coefficient, or declaring global admission from the local histogram." + ], + "overlap_terms": [ + "R437", + "two-window carrier", + "4067", + "4147", + "pooled compiler", + "request alignment", + "reverse row coefficient" + ], + "existing_checks": [ + { + "scope": "PR #4067: source-bound two-window carrier with (2,2) to (1,3) paid exchange and fixed OQ4 host.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Pooled compiler/request rebind, physical caller and precision/stock admission.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4147: reverse row coefficient follow-up.", + "evidence": "research/r437-reverse-row-coefficient/README.md", + "remaining": "Use the exact coefficient in a caller-bound precision/stock proof rather than repeat the arithmetic.", + "status": "author-checked", + "source_commit": "72e7bb797adf82aeb525a399f56ab8adbab8e93c", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Batched high-factor fresh_rows quotient on actual binary Counts, exact accepted-domain refinement and separate finite-control/tape invoice.", + "scope_change_reason": "Follow the original-root entry handoff with a new executable binary-stock quotient rather than repeat host admission.", + "bottleneck_link": "Close one source-bound R437 caller admission interface without changing the selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop at fixed-context quotient/stock guard with honest finite-control cost; no default backend or uniform supplier improvement.", + "outcome": "partial", + "evidence": "RESULT.json", + "author": "Brian (JoyboyBrian)", + "ai_assistance": "Substantial OpenAI Codex assistance. Author-checked finite evidence; not formal-kernel verification.", + "open_questions": [ + { + "question": "When does a physically priced batched divider beat shared-radix q division?", + "why_it_matters": "Fewer Count scans may lose to large-controller setup and state.", + "first_step": "Implement and meter binary large-constant division plus setup amortization.", + "blocked_by": "A specified primitive model and full physical divider." + } + ], + "freshness": { + "canonical_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "entry_utc": "2026-10-22T19:39:00Z", + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4682#discussioncomment-19131462", + "overlap_coverage": "299 open PRs; 3695 Discussion records; 5860 local notes. Remote pagination complete; local inventory at b58ad9ef (guidance unchanged at refreshed 624de9dc); closed code/diffs not exhaustive." + } +} diff --git a/research/r437-batched-high-quotient/VERIFY.json b/research/r437-batched-high-quotient/VERIFY.json new file mode 100644 index 0000000000..3819ed846e --- /dev/null +++ b/research/r437-batched-high-quotient/VERIFY.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/cardinal_counts.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/fresh_rows.py", + "research/selected-bit-physical-caller/PROOF.md", + "research/selected-bit-physical-caller/macro_binding.py", + "research/selected-bit-physical-caller/macro_machine.py", + "research/selected-bit-recursive-caller/PROOF.md", + "research/selected-bit-recursive-caller/driver.py", + "research/selected-bit-recursive-caller/node.py", + "research/selected-bit-recursive-caller/predecessor/cardinal_counts.py", + "research/selected-bit-recursive-caller/predecessor/fresh_rows.py", + "research/selected-bit-recursive-caller/predecessor/vendor/bitstream.py", + "research/selected-bit-recursive-caller/predecessor/vendor/cardinality.py", + "research/selected-bit-recursive-caller/predecessor/vendor/counts.py", + "research/selected-bit-recursive-caller/predecessor/vendor/directory.py", + "research/selected-bit-recursive-caller/predecessor/vendor/matrices.py", + "research/selected-bit-recursive-caller/predecessor/vendor/oracle.py", + "research/selected-bit-recursive-caller/predecessor/vendor/records.py", + "research/selected-bit-recursive-caller/predecessor/vendor/routes.py", + "research/selected-bit-recursive-caller/predecessor/vendor/stream.py", + "research/selected-bit-recursive-caller/predecessor/vendor/words.py", + "research/selected-bit-recursive-caller/recursive_call.py", + "research/selected-live-row-divisor/README.md", + "research/selected-live-row-divisor/sources/pr2234/NOTICE.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Binary Count quotient, NODE guard, lane costs and failures." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Same explicit checks under optimized Python." + } + ] +} diff --git a/research/r437-batched-high-quotient/adapter.py b/research/r437-batched-high-quotient/adapter.py new file mode 100644 index 0000000000..37674d1744 --- /dev/null +++ b/research/r437-batched-high-quotient/adapter.py @@ -0,0 +1,41 @@ +"""Opt-in fixed-context quotient; enlarged finite control is part of its cost. + +Brian (JoyboyBrian), substantial OpenAI Codex assistance. Apache-2.0. +Based on David Arias's PR2753 fresh_rows quotient and ToikY's shared radix idea. +""" + +def compile_quotient(q,dimension): + from cardinal_counts import Count,positive + from cardinality import radix_power + from words import need + need(type(q) is int and q>=2 and type(dimension) is int and dimension>0,'compiled radix/dimension') + # Explicit square-and-multiply construction; all operands are fixed context. + power=dimension*dimension; factor=q; high_factor=1; products=[] + def product(a,b): + products.append((a.bit_length(),b.bit_length())) + return a*b + while power: + if power&1:high_factor=product(high_factor,factor) + power//=2 + if power:factor=product(factor,factor) + construction=dict(multiplications=len(products),operand_bit_pairs=products, + schoolbook_bit_products=sum(a*b for a,b in products), + stored_divisor_bits=high_factor.bit_length()) + def quotient(fresh,context,families): + need((context.q,context.dimension)==(q,dimension),'matching compiled high divisor') + positive(fresh) + unused=Count(fresh) + try: + need(unused.divide_small(families)==0,'complete fresh family factor') + need(unused.divide_small(context.codes.size)==0,'complete fresh GL low factor') + first=True + for _ in radix_power(context.ring,q): + if first:first=False + else:need(unused.divide_small(high_factor)==0,'complete fresh high factor') + need(not unused.zero(),'nonempty unused row quotient') + return unused + except ValueError: + unused.close() + raise + quotient.construction=construction + return quotient,high_factor diff --git a/research/r437-batched-high-quotient/verify.py b/research/r437-batched-high-quotient/verify.py new file mode 100644 index 0000000000..4611310b2e --- /dev/null +++ b/research/r437-batched-high-quotient/verify.py @@ -0,0 +1,111 @@ +#!/usr/bin/env python3 +"""Actual Count high-factor quotient refinement; no default-backend change.""" +import argparse,ast,hashlib,importlib,json,math,sys +from pathlib import Path +from types import SimpleNamespace as NS +HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1] +PREFIX='research/selected-bit-recursive-caller/predecessor' + +def need(ok,message): + if not ok:raise ValueError(message) + +def sha(data):return hashlib.sha256(data).hexdigest() +def receipt(x):return dict(bits=x.bit_length(),sha256=sha(x.to_bytes(max(1,(x.bit_length()+7)//8),'big'))) +def authenticate(): + manifest=json.loads((HERE/'SOURCES.json').read_text()) + for row in manifest['files']: + if row['usage']!='input':continue + path=ROOT/row['path'];need(path.is_file() and not path.is_symlink() and sha(path.read_bytes())==row['sha256'],'source hash '+row['path']) + return sum(r['usage']=='input' for r in manifest['files']) + +def run(): + inputs=authenticate();sys.path[:0]=[str(HERE),str(ROOT/PREFIX),str(ROOT/PREFIX/'vendor')] + import cardinal_counts,cardinality,fresh_rows,words,records,directory + from adapter import compile_quotient + Count=cardinal_counts.Count + for name in ('fresh_rows','cardinal_counts','cardinality','counts','words','records','directory','stream','oracle','matrices','bitstream','routes'): + module=importlib.import_module(name);need(str(Path(module.__file__).resolve()).startswith(str(ROOT/PREFIX)),'bound module '+name) + tree=ast.parse((ROOT/'research/selected-bit-physical-caller/macro_machine.py').read_text()) + machine=next(x for x in tree.body if isinstance(x,ast.ClassDef) and x.name=='Machine') + node=next(x for x in machine.body if isinstance(x,ast.FunctionDef) and x.name=='node') + start=next(i for i,x in enumerate(node.body) if isinstance(x,ast.Assign) and isinstance(x.targets[0],ast.Name) and x.targets[0].id=='unused') + block=node.body[start:start+4] + need([type(x).__name__ for x in block]==['Assign','Expr','Assign','Try'],'literal NODE stock guard shape') + save=next(x for x in machine.body if isinstance(x,ast.FunctionDef) and x.name=='save_count') + commit=next(x for x in machine.body if isinstance(x,ast.FunctionDef) and x.name=='commit') + env=dict(directory=directory,append_tape=directory.append_tape,Lease=(),Count=Count,need=words.need) + exec(compile(ast.Module(body=[save,commit],type_ignores=[]),'','exec'),env) + code=compile(ast.Module(body=block,type_ignores=[]),'','exec') + def value(count): + cells=count.tape.cells[1:];at=cells.index(words.RIGHT) + need(all(x in (0,1) for x in cells[:at]),'binary observer') + return sum(x<