From 028527eecad4fd191f8d26811c7df2a2acf92df3 Mon Sep 17 00:00:00 2001 From: zxv Date: Wed, 28 Oct 2026 01:24:29 -0400 Subject: [PATCH 1/2] Prove a 76-bit retained-information floor for the stochastic prefix --- .../COLLISIONS.json | 765 ++++++++++++++++++ .../PREDECESSOR.json | 9 + .../stochastic-restoration-memory/PROOF.md | 49 ++ .../stochastic-restoration-memory/README.md | 30 + .../stochastic-restoration-memory/RESULT.json | 39 + .../SOURCES.json | 24 + .../stochastic-restoration-memory/TASK.json | 89 ++ .../stochastic-restoration-memory/VERIFY.json | 32 + .../predecessor/PR6066-README.md | 203 +++++ .../stochastic-restoration-memory/verify.py | 193 +++++ 10 files changed, 1433 insertions(+) create mode 100644 research/stochastic-restoration-memory/COLLISIONS.json create mode 100644 research/stochastic-restoration-memory/PREDECESSOR.json create mode 100644 research/stochastic-restoration-memory/PROOF.md create mode 100644 research/stochastic-restoration-memory/README.md create mode 100644 research/stochastic-restoration-memory/RESULT.json create mode 100644 research/stochastic-restoration-memory/SOURCES.json create mode 100644 research/stochastic-restoration-memory/TASK.json create mode 100644 research/stochastic-restoration-memory/VERIFY.json create mode 100644 research/stochastic-restoration-memory/predecessor/PR6066-README.md create mode 100644 research/stochastic-restoration-memory/verify.py diff --git a/research/stochastic-restoration-memory/COLLISIONS.json b/research/stochastic-restoration-memory/COLLISIONS.json new file mode 100644 index 0000000000..254935b4a4 --- /dev/null +++ b/research/stochastic-restoration-memory/COLLISIONS.json @@ -0,0 +1,765 @@ +{ + "coin_choice": "Every noninteger event uses u=0.", + "blocks": [ + { + "block": 0, + "input_preimages": [ + [ + 39, + -36, + -91, + 61, + 68, + 58, + -91, + 30, + -82, + -98, + 19, + -8, + -53, + -6, + -24, + 80 + ], + [ + 39, + -36, + -91, + 61, + 68, + 59, + -91, + 30, + -82, + -99, + 19, + -9, + -54, + -7, + -24, + 80 + ], + [ + 38, + -37, + -92, + 61, + 67, + 58, + -91, + 30, + -82, + -98, + 19, + -8, + -53, + -6, + -24, + 80 + ], + [ + 38, + -37, + -92, + 61, + 67, + 59, + -91, + 30, + -82, + -99, + 19, + -9, + -54, + -7, + -24, + 80 + ] + ], + "output": [ + -79, + -2, + 38, + 2, + -54, + 105, + -47, + -48, + 62, + -50, + -50, + 40, + -43, + 4, + -114, + -10 + ] + }, + { + "block": 1, + "input_preimages": [ + [ + 6, + 64, + 2, + -37, + -62, + 70, + -26, + -4, + 6, + -14, + -45, + -66, + -32, + -46, + -35, + 26 + ], + [ + 6, + 64, + 2, + -37, + -62, + 71, + -26, + -4, + 6, + -15, + -45, + -67, + -33, + -47, + -35, + 26 + ], + [ + 5, + 63, + 1, + -37, + -63, + 70, + -26, + -4, + 6, + -14, + -45, + -66, + -32, + -46, + -35, + 26 + ], + [ + 5, + 63, + 1, + -37, + -63, + 71, + -26, + -4, + 6, + -15, + -45, + -67, + -33, + -47, + -35, + 26 + ] + ], + "output": [ + 69, + -20, + 19, + -32, + -75, + -139, + 47, + -31, + -76, + -66, + -24, + -76, + 48, + 34, + -33, + 28 + ] + }, + { + "block": 2, + "input_preimages": [ + [ + 53, + 40, + -29, + -31, + -42, + -18, + -48, + 30, + 41, + 73, + 22, + -89, + 13, + -26, + -88, + -67 + ], + [ + 53, + 40, + -29, + -31, + -42, + -17, + -48, + 30, + 41, + 72, + 22, + -90, + 12, + -27, + -88, + -67 + ], + [ + 52, + 39, + -30, + -31, + -43, + -18, + -48, + 30, + 41, + 73, + 22, + -89, + 13, + -26, + -88, + -67 + ], + [ + 52, + 39, + -30, + -31, + -43, + -17, + -48, + 30, + 41, + 72, + 22, + -90, + 12, + -27, + -88, + -67 + ] + ], + "output": [ + 51, + -63, + 11, + 26, + -27, + -40, + 151, + -59, + 8, + 19, + 86, + -76, + -18, + -57, + -48, + -27 + ] + }, + { + "block": 3, + "input_preimages": [ + [ + 99, + 71, + -1, + -77, + 1, + -49, + 64, + -66, + -40, + -63, + -93, + 98, + 53, + 78, + -100, + -55 + ], + [ + 99, + 71, + -1, + -77, + 1, + -48, + 64, + -66, + -40, + -64, + -93, + 97, + 52, + 77, + -100, + -55 + ], + [ + 98, + 70, + -2, + -77, + 0, + -49, + 64, + -66, + -40, + -63, + -93, + 98, + 53, + 78, + -100, + -55 + ], + [ + 98, + 70, + -2, + -77, + 0, + -48, + 64, + -66, + -40, + -64, + -93, + 97, + 52, + 77, + -100, + -55 + ] + ], + "output": [ + 112, + 132, + 62, + 157, + -129, + -127, + -202, + 23, + -118, + -92, + -180, + -19, + 122, + 147, + 1, + 46 + ] + }, + { + "block": 4, + "input_preimages": [ + [ + 33, + -98, + 63, + -80, + -47, + 50, + -53, + -4, + -99, + 38, + -90, + 45, + 38, + 96, + 7, + 16 + ], + [ + 33, + -98, + 63, + -80, + -47, + 51, + -53, + -4, + -99, + 37, + -90, + 44, + 37, + 95, + 7, + 16 + ], + [ + 32, + -99, + 62, + -80, + -48, + 50, + -53, + -4, + -99, + 38, + -90, + 45, + 38, + 96, + 7, + 16 + ], + [ + 32, + -99, + 62, + -80, + -48, + 51, + -53, + -4, + -99, + 37, + -90, + 44, + 37, + 95, + 7, + 16 + ] + ], + "output": [ + 30, + -21, + 89, + 172, + 23, + -87, + -135, + -181, + -108, + -203, + -26, + -19, + 153, + 211, + 61, + 70 + ] + }, + { + "block": 5, + "input_preimages": [ + [ + 58, + -80, + -41, + 63, + 47, + -66, + -7, + -31, + -86, + -37, + 12, + 84, + -71, + -47, + 50, + -38 + ], + [ + 58, + -80, + -41, + 63, + 47, + -65, + -7, + -31, + -86, + -38, + 12, + 83, + -72, + -48, + 50, + -38 + ], + [ + 57, + -81, + -42, + 63, + 46, + -66, + -7, + -31, + -86, + -37, + 12, + 84, + -71, + -47, + 50, + -38 + ], + [ + 57, + -81, + -42, + 63, + 46, + -65, + -7, + -31, + -86, + -38, + 12, + 83, + -72, + -48, + 50, + -38 + ] + ], + "output": [ + -104, + 27, + -38, + 86, + 12, + 100, + -97, + 17, + 66, + 11, + -57, + 64, + -116, + -92, + 19, + -69 + ] + }, + { + "block": 6, + "input_preimages": [ + [ + 74, + 8, + 99, + -88, + 98, + -34, + -14, + 67, + -55, + 59, + 72, + 36, + -81, + -67, + 37, + -1 + ], + [ + 74, + 8, + 99, + -88, + 98, + -33, + -14, + 67, + -55, + 58, + 72, + 35, + -82, + -68, + 37, + -1 + ], + [ + 73, + 7, + 98, + -88, + 97, + -34, + -14, + 67, + -55, + 59, + 72, + 36, + -81, + -67, + 37, + -1 + ], + [ + 73, + 7, + 98, + -88, + 97, + -33, + -14, + 67, + -55, + 58, + 72, + 35, + -82, + -68, + 37, + -1 + ] + ], + "output": [ + 91, + 194, + -58, + -2, + 168, + 167, + -60, + -97, + -3, + -125, + 115, + 92, + -170, + -156, + 141, + 103 + ] + }, + { + "block": 7, + "input_preimages": [ + [ + 3, + 25, + -41, + 77, + 96, + -97, + 78, + 77, + -37, + 53, + -5, + -47, + 73, + 30, + -29, + -28 + ], + [ + 3, + 25, + -41, + 77, + 96, + -96, + 78, + 77, + -37, + 52, + -5, + -48, + 72, + 29, + -29, + -28 + ], + [ + 2, + 24, + -42, + 77, + 95, + -97, + 78, + 77, + -37, + 53, + -5, + -47, + 73, + 30, + -29, + -28 + ], + [ + 2, + 24, + -42, + 77, + 95, + -96, + 78, + 77, + -37, + 52, + -5, + -48, + 72, + 29, + -29, + -28 + ] + ], + "output": [ + -65, + -142, + -70, + -5, + -58, + 79, + 190, + 168, + 203, + 89, + 0, + -100, + 29, + -14, + -58, + -57 + ] + } + ] +} diff --git a/research/stochastic-restoration-memory/PREDECESSOR.json b/research/stochastic-restoration-memory/PREDECESSOR.json new file mode 100644 index 0000000000..73a4931b9a --- /dev/null +++ b/research/stochastic-restoration-memory/PREDECESSOR.json @@ -0,0 +1,9 @@ +{ + "source_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6066", + "head": "2711ca28367c5bbbb54ce9601928e885d87ca165", + "source_path": "research/reversible-stochastic-shears/README.md", + "retained_path": "predecessor/PR6066-README.md", + "sha256": "bb6cee79d80fad16278141d1f0a42f348ec291eba288ee00668cdd59d5aab3d7", + "license": "Apache-2.0", + "credit": "https://github.com/zxv" +} diff --git a/research/stochastic-restoration-memory/PROOF.md b/research/stochastic-restoration-memory/PROOF.md new file mode 100644 index 0000000000..ce7e8b4796 --- /dev/null +++ b/research/stochastic-restoration-memory/PROOF.md @@ -0,0 +1,49 @@ +# A 2^76 fiber in the exact PR6066 forward map + +This proof concerns the historical 748-role, 9,589-event scalar prefix used by [PR6066](https://github.com/CrocSwap/integer-mult-bounds/pull/6066). It does not transfer the result to the different selected PR6030 word. All incoming integer values are arbitrary dirty data. Fix every forward coin to zero; this is a permitted finite tape with positive probability under the fresh-coin model. The tape is retained unchanged. + +## 1. A surjective prefix with exactly 2^60 preimages per state + +For a dyadic denominator d and fixed u, write S(n,d,u)=floor((n+d-1-u)/d). An ADD x_r += S(n*x_s,d,u), with r != s, is a bijection of the full integer state: subtract the same function of the unchanged source. A sign SCALE is also a bijection. + +A signed half SCALE is exactly two-to-one and surjective. For sign s in {-1,1}, output y, and u in {0,1}, its two distinct preimages are + + x = s * (2y + (2u-1)r), r in {0,1}. + +The first 8,411 source events contain 60 signed half SCALEs, no doubling, and otherwise only ADDs and sign SCALEs. Composition of a surjective a-to-one map and a surjective b-to-one map is surjective and ab-to-one. Therefore, for **every** fixed tape and every prescribed state after event 8410, this prefix has exactly 2^60 distinct original input states. The choice bits in the reverse interpreter give an explicit parametrization of them. + +Counting all 84 halvings alone would be invalid: the later program has 32 doublings, and double followed by stochastic half is injective. This is why chronology and the tail need separate checks. + +## 2. Eight independent four-preimage tail blocks + +The next 1,121 events partition into eight consecutive programs on the disjoint role sets 272..287, 288..303, ..., 384..399. The first three blocks have 137 events each; the last five have 142 each. No block reads or writes outside its own sixteen roles. Each has three signed halvings and four doublings. + +[COLLISIONS.json](COLLISIONS.json) supplies four distinct 16-integer preimages and their common output for each literal source block, with every coin zero. The verifier replays all 32 input vectors directly against the authenticated source events. It also runs an independently structured reverse branch interpreter: each halving branches into its two preimages and each inverse doubling rejects odd values. For the nominated output it checks that the complete surviving fiber is exactly the four committed vectors. This checks particular finite fibers; it does **not** prove four is a global maximum for other outputs or tapes. + +Take the Cartesian product of these eight four-element sets, fixing all other coordinates to zero at the start of the middle program. Disjoint support proves that its 4^8 = 2^16 distinct states have one identical complete 748-role output. Every following event is deterministic with the fixed tape, so the final 57 ADDs preserve this collision. + +## 3. Lift through the first prefix + +Every one of those 2^16 middle input states has exactly 2^60 distinct original preimages by section 1. The preimage sets of distinct middle states are disjoint. Hence the complete forward map F_0 has a fiber of cardinality at least + + 2^16 * 2^60 = 2^76. + +This large cardinality is proved by composition; the verifier does not claim to enumerate 2^76 inputs. It checks the complete small fibers that generate the product, all 516 signed-half identities over the stated finite corroboration range, and 86 complete lifted source executions. The latter cover all-zero/all-one/unit choice patterns for the sixty early residues and each of the other three choices in each tail block. They all reach the same full endpoint. + +The witnesses are finite integers. A conservative reverse interval bound starts with the largest absolute middle-collision coordinate. In reverse, an ADD increases the global magnitude bound B by at most ceil(|n|B/d), a signed half changes it to at most 2B+1, and a sign leaves it fixed. Applying this to all 8,411 events gives a bound with 4,563 magnitude bits. Eight additional bits cover the sign and scalar numerator/addition guards. Thus the collision proof also applies to sufficiently wide finite implementations (the supplied conservative sufficient width is 4,571 bits); it is not a lower bound for every tiny fixed-width or restricted-input variant. The 86 executed fixtures actually stay within ten magnitude bits. The guard calculation is deliberately an upper bound, not an optimized precision requirement. + +## 4. Consequence for retained information + +Suppose the exact forward stage of a pathwise restorable implementation has the boundary + + (x, U, 0) -> (F_U(x), U, A(x,U)). + +All additional state capable of distinguishing inputs is included in A: logs, temporary registers left live, control state, or head-position information. Fix U=0 and restrict x to the proven 2^76-point fiber. The first two output components are identical on that set. Injectivity, necessary to restore arbitrary dirty x, therefore requires at least 2^76 distinguishable values of A. An auxiliary capacity below 76 bits is impossible. Copying F_U(x) to a disjoint accumulator with the same initial value does not distinguish these inputs. + +This is a **worst-case** bound for exact pathwise restoration and the same forward map/tape. It does not bound average compressed length or prove that every tape needs 76 bits. It does not cover a changed rounding law, bounded-error restoration, restricted reached input set, or a different forward interface that leaves further input information in other outputs. Such extra information is payable and cannot be called clean scratch. + +PR6066 supplies an 84-bit residue log. This lower bound leaves at most eight bits of possible worst-case log reduction under this boundary. It does not construct a 76-bit log, prove the block fibers never exceed four, or price a physical compression/cleanup routine. Working scratch, integer arithmetic, tape movement, the next native MOVE and complete supplier costs remain open. No new kappa or selected change follows. + +## Credit + +Prepared by [zxv](https://github.com/zxv), with substantial OpenAI Codex assistance. [Nick Petalas](https://github.com/petalas)'s [PR6026](https://github.com/CrocSwap/integer-mult-bounds/pull/6026) supplies the stochastic prefix and error context. [Ali Romman](https://github.com/aliromman)'s [PR5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599) and the retained P104 lineage supply the source word. The round-and-restore ABI is PR6066's. Fiber counting and injectivity are classical; the contribution is this source-bound 2^76 collision and its exact restoration implication. Apache-2.0. No independent human or formal proof-kernel review is claimed. diff --git a/research/stochastic-restoration-memory/README.md b/research/stochastic-restoration-memory/README.md new file mode 100644 index 0000000000..cfd540e052 --- /dev/null +++ b/research/stochastic-restoration-memory/README.md @@ -0,0 +1,30 @@ +# The PR6066 stochastic prefix needs at least 76 retained bits + +For the exact integer-grid forward map in [PR6066](https://github.com/CrocSwap/integer-mult-bounds/pull/6066), with its random tape unchanged, exact dirty restoration needs auxiliary information with at least **76 bits of worst-case capacity**. The existing 84-bit parity log can therefore save at most eight bits under the same boundary. No matching compression algorithm or new kappa is claimed. + +The authenticated historical 9,589-event prefix has 60 halvings before any doubling. Its first 8,411 events are surjective and exactly 2^60-to-one on arbitrary integer data. Eight disjoint later 16-role blocks each have a verified four-preimage collision for one all-zero coin tape. Their product and the surjective prefix give a 2^76-point fiber of the full rounded forward map. [PROOF.md](PROOF.md) gives the quantifiers, finite-width guard and limits; [COLLISIONS.json](COLLISIONS.json) provides the small exact witnesses. + +## Significance for researchers + +This resolves a substantial part of PR6066's question about reducing its 84 parity bits. The 32 later doublings do not imply a 52-bit log is sufficient: chronology and source-bound collisions force at least 76 bits at the forward boundary. A smaller log would require proving and implementing a compression within the remaining eight-bit gap, or changing the forward/restoration contract. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/stochastic-restoration-memory +python3.12 -B scripts/check_research_commit.py --package research/stochastic-restoration-memory +``` + +The standard-library verifier authenticates the historical word and retained PR6066 statement, checks all 32 small collision preimages with exact integer arithmetic, exhausts each nominated block fiber, verifies disjoint literal source domains, and checks 86 complete lifted source executions plus signed-half and invalid-counting controls. The written composition proof supplies the 2^76 quantifier; this many inputs are not enumerated. Normal and optimized registered checks compare RESULT.json. + +## Open next questions + +Are all fibers of each tail block bounded by four, for every output and coin tape? Start with its eight exact inverse branches; a proof could close the remaining eight-bit information gap. Finite probes are not an all-tape proof. + +Can a smaller retained log be computed and erased under the actual physical caller at a favorable total cost? First distinguish retained information from working scratch, charge compression and random-tape movement, and keep every arbitrary dirty input. The native MOVE and full error/cost contracts remain blockers. + +## Scope and credit + +This uses the historical PR5599 prefix used by PR6066, not the different selected PR6030 word. The 76-bit floor is worst-case for exact pathwise restoration with arbitrary integer inputs and unchanged tape. It does not assert an average-length lower bound, a matching 76-bit implementation, a complete physical resource optimum, or a result for every small fixed width. A conservative 4,571-bit signed/guard width suffices for the entire collision family; executed representative fixtures need only ten magnitude bits. No native/selected cold replay or new kappa is claimed. + +Prepared by [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance. Credit [Nick Petalas](https://github.com/petalas)'s [PR6026](https://github.com/CrocSwap/integer-mult-bounds/pull/6026), [Ali Romman](https://github.com/aliromman)'s [PR5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599), and the retained source lineage. The pending PR6066 statement is retained verbatim with exact head/hash. Apache-2.0. No independent human review or proof-kernel acceptance is claimed. diff --git a/research/stochastic-restoration-memory/RESULT.json b/research/stochastic-restoration-memory/RESULT.json new file mode 100644 index 0000000000..7a3c1724d1 --- /dev/null +++ b/research/stochastic-restoration-memory/RESULT.json @@ -0,0 +1,39 @@ +{ + "block_fiber_sizes": [ + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4 + ], + "block_program_sha256": [ + "5988600462f2d31f19ee57ba6bb211a1e09d4487f8f072304602bf583aae6085", + "5988600462f2d31f19ee57ba6bb211a1e09d4487f8f072304602bf583aae6085", + "5988600462f2d31f19ee57ba6bb211a1e09d4487f8f072304602bf583aae6085", + "310fd43088b4f8d64285d0df3e0bee2a2eeafe4fb1aab6e06c4a5590de1a3c28", + "310fd43088b4f8d64285d0df3e0bee2a2eeafe4fb1aab6e06c4a5590de1a3c28", + "310fd43088b4f8d64285d0df3e0bee2a2eeafe4fb1aab6e06c4a5590de1a3c28", + "310fd43088b4f8d64285d0df3e0bee2a2eeafe4fb1aab6e06c4a5590de1a3c28", + "310fd43088b4f8d64285d0df3e0bee2a2eeafe4fb1aab6e06c4a5590de1a3c28" + ], + "conservative_signed_guard_bits": 4571, + "events": 9589, + "fixture_peak_magnitude_bits": 10, + "full_fiber_power_lower": 76, + "full_word_lifts_checked": 86, + "half_lemma_checks": 516, + "independent_blocks": 8, + "lift_bound_magnitude_bits": 4563, + "maximum_possible_bit_saving": 8, + "prefix_fiber_power": 60, + "public_integer_roles": 748, + "scope": "Worst-case retained information for the exact PR6066 forward map and unchanged tape; no matching upper bound or new kappa.", + "source_doubles": 32, + "source_halves": 84, + "source_log_bits": 84, + "status": "PASS_STOCHASTIC_RESTORATION_MEMORY", + "surjective_prefix_events": 8411 +} diff --git a/research/stochastic-restoration-memory/SOURCES.json b/research/stochastic-restoration-memory/SOURCES.json new file mode 100644 index 0000000000..34b0d2454b --- /dev/null +++ b/research/stochastic-restoration-memory/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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-helper-subspace-splits/WORD.json.gz", + "usage": "input", + "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb", + "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099" + } + ] +} diff --git a/research/stochastic-restoration-memory/TASK.json b/research/stochastic-restoration-memory/TASK.json new file mode 100644 index 0000000000..5570c3880e --- /dev/null +++ b/research/stochastic-restoration-memory/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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": "refined", + "actual_scope": "Investigate PR6066 chronological restoration-log compression by constructing a source-bound large fiber of its exact forward rounded map.", + "scope_change_reason": "Explicit assignment starts with recent zxv PRs; this addresses PR6066 open question on the 84 retained parity bits.", + "bottleneck_link": "Bounds the possible storage improvement before paying for a new reversible numerical interface; no direct exponent gain is inferred.", + "budget_minutes": 30, + "stop_rule": "Stop at a proved source-bound memory floor and bounded exact replay. Treat a matching compression and all-tape block upper bound as separate tasks.", + "outcome": "negative-result", + "evidence": "PROOF.md; COLLISIONS.json; RESULT.json: 86 whole-prefix lifts, 32 block collision inputs, complete nominated fibers and 516 signed-half checks.", + "author": "zxv", + "ai_assistance": "Substantial OpenAI Codex assistance in source review, proof, exact search, implementation and verification; no subagents or independent human/formal review.", + "open_questions": [ + { + "question": "Is every tail-block fiber at most four for arbitrary outputs and fixed tapes?", + "why_it_matters": "Could close the remaining eight-bit information gap.", + "first_step": "Analyze the eight exact inverse branches for each of the two source templates.", + "blocked_by": "A universal upper bound is unproved; finite probes are insufficient." + }, + { + "question": "Can a smaller retained log be compressed and erased under the actual native caller?", + "why_it_matters": "Information capacity alone does not pay for scratch, tape access or cleanup.", + "first_step": "Give the exact forward boundary, reversible algorithm and total physical bill.", + "blocked_by": "Full physical/native/error interface remains open." + } + ] +} diff --git a/research/stochastic-restoration-memory/VERIFY.json b/research/stochastic-restoration-memory/VERIFY.json new file mode 100644 index 0000000000..94838e0636 --- /dev/null +++ b/research/stochastic-restoration-memory/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper-subspace-splits/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source-bound product collisions, complete nominated block fibers, lifted source executions and controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks with Python optimization" + } + ] +} diff --git a/research/stochastic-restoration-memory/predecessor/PR6066-README.md b/research/stochastic-restoration-memory/predecessor/PR6066-README.md new file mode 100644 index 0000000000..829b3ebf4b --- /dev/null +++ b/research/stochastic-restoration-memory/predecessor/PR6066-README.md @@ -0,0 +1,203 @@ +# Stochastic scalar prefixes can restore dirty inputs with a parity log + +A grid-valued stochastic ADD is an exactly invertible shear when its inverse +uses the complemented coin. A rounded signed halving instead needs one parity +bit; keeping that bit suffices, and recomputing it during reversal clears it. +Together these give a compute–accumulate–uncompute interface for the exact +9,589-event scalar prefix studied by +[Nick Petalas](https://github.com/petalas)'s +[PR #6026](https://github.com/CrocSwap/integer-mult-bounds/pull/6026). + +The source has 84 signed halvings. The protocol uses **84 clean residue bits +and 11,713 read-only random bits per real stream sample**, restores all 748 +arbitrary dirty working values, returns the residue log to zero, and leaves +the random tape unchanged. Its forward arithmetic law is exactly the source's +fresh stochastic rounding law. Thus its source-relative forward error bound +is retained under the source's assumptions; that concentration result is cited, +not independently replayed or strengthened here. + +This is a logical scalar-grid ABI, not a native rounded supplier, physically +reversible bit-level implementation, complete caller invoice or new κ. Physical +random-bit preparation/access, guard widths, integer arithmetic, temporary +cleanup and the later native MOVE remain payable and unimplemented. + +## Exact stochastic rounding and an inverse shear + +Normalize the grid spacing to one. For an integer numerator $n$, dyadic +denominator $d=2^q$, and a fixed coin integer $0\leq U 0 and d & (d-1) == 0 and 0 <= u < d, 'dyadic coin') + return (n+d-1-u)//d + + +def event(e): + q = Q(e[-2]) + return e[0], e[1], e[2] if e[0] == 'ADD' else None, q.numerator, q.denominator + + +def forward(initial, events): + x = list(initial) + peak = max(map(abs,x), default=0) + for op,r,s,n,d in events: + x[r] = x[r]+sr(n*x[s],d) if op == 'ADD' else sr(n*x[r],d) + peak = max(peak,abs(x[r])) + return x, peak + + +def inverse_prefix(output, events, bits): + """All-zero coins; each signed halving has two distinct exact preimages.""" + x = list(output) + it = iter(bits) + for op,r,s,n,d in reversed(events): + if op == 'ADD': + x[r] -= sr(n*x[s],d) + elif d == 2: + x[r] = n*(2*x[r]-next(it)) + else: + need(n == -1 and d == 1, 'no doubling in surjective prefix') + x[r] = -x[r] + need(next(it,None) is None, 'all prefix choice bits consumed') + return x + + +def inverse_bound(output_bound, events): + bound = output_bound + for op,r,s,n,d in reversed(events): + if op == 'ADD': + bound += (abs(n)*bound+d-1)//d + elif d == 2: + bound = 2*bound+1 + else: + need(n == -1 and d == 1, 'prefix SCALE domain') + return bound + + +def source(): + for pin in json.loads((HERE/'SOURCES.json').read_text())['files']: + if pin['usage'] == 'input': + need(sha256((ROOT/pin['path']).read_bytes()).hexdigest() == pin['sha256'], + 'source bytes: '+pin['path']) + p = json.loads((HERE/'PREDECESSOR.json').read_text()) + need(sha256((HERE/p['retained_path']).read_bytes()).hexdigest() == p['sha256'], + 'retained PR6066 statement') + w = json.loads(gzip.decompress((ROOT/WORD).read_bytes())) + cut = next(i for i,e in enumerate(w['program']) if e[0] == 'MOVE') + need(w['public'] == 748 and cut == 9589 and w['frames'][3] == [], 'historical source ABI') + prefix = w['program'][:cut] + need(all(e[0] in ('ADD','SCALE') and e[-1] == 3 for e in prefix), 'common empty-chart scalar block') + events = [event(e) for e in prefix] + for op,r,s,n,d in events: + need(0 <= r < 748 and (op != 'ADD' or 0 <= s < 748 and r != s), 'public indices') + need(d in (1,2,4) and abs(Q(n,d)) <= 16, 'coefficient domain') + if op == 'SCALE': + need(Q(n,d) in (Q(-1),Q(2),Q(1,2),Q(-1,2)), 'SCALE domain') + return events + + +def calculate(): + events = source() + pre, tail = events[:8411], events[9532:] + halves = sum(op == 'SCALE' and d == 2 for op,r,s,n,d in events) + doubles = sum(op == 'SCALE' and n == 2 and d == 1 for op,r,s,n,d in events) + need(halves == 84 and doubles == 32, 'source half/double ledger') + need(sum(op == 'SCALE' and d == 2 for op,r,s,n,d in pre) == 60, 'sixty prefix losses') + need(all(op == 'ADD' or n == -1 or d == 2 for op,r,s,n,d in pre), 'surjective prefix') + need(len(tail) == 57 and all(op == 'ADD' for op,r,s,n,d in tail), 'bijective trailing shears') + fixture = json.loads((HERE/'COLLISIONS.json').read_text()) + need(len(fixture['blocks']) == 8, 'eight collision blocks') + blocks, cursor, signatures, bound = [], 8411, [], 0 + for b, row in enumerate(fixture['blocks']): + lo = 272+16*b + size = 137 if b < 3 else 142 + es = events[cursor:cursor+size] + need(row['block'] == b and all(lo <= r < lo+16 and + (s is None or lo <= s < lo+16) for op,r,s,n,d in es), 'independent literal block') + local = [(op,r-lo,None if s is None else s-lo,n,d) for op,r,s,n,d in es] + xs = row['input_preimages'] + need(len(xs) == 4 and len({tuple(x) for x in xs}) == 4 and + all(len(x) == 16 and all(type(v) is int for v in x) for x in xs), 'four distinct preimages') + for x in xs: + y, peak = forward(x,local) + need(y == row['output'], 'literal all-zero-tape collision') + bound = max(bound,max(map(abs,x))) + # Three halvings leave only eight possible inverse branches. Enumerate them + # to check the fixture's complete fiber, without relying on search output. + states = [list(row['output'])] + for op,r,s,n,d in reversed(local): + new = [] + for old in states: + x = list(old) + if op == 'ADD': + x[r] -= sr(n*x[s],d); new.append(x) + elif d == 2: + for bit in (0,1): + xx = list(x); xx[r] = n*(2*x[r]-bit); new.append(xx) + elif n == 2: + if x[r] % 2 == 0: + x[r] //= 2; new.append(x) + else: + x[r] = -x[r]; new.append(x) + states = new + need({tuple(x) for x in states} == {tuple(x) for x in xs}, 'complete exact four-point block fiber') + signatures.append(sha256(json.dumps(local,separators=(',',':')).encode()).hexdigest()) + blocks.append((lo,local,xs)) + cursor += size + need(cursor == 9532, 'complete middle coverage') + need(all(not 272 <= r < 400 and (s is None or not 272 <= s < 400) + for op,r,s,n,d in tail), 'trailing shears separate from collision blocks') + final, start = [0]*748, [0]*748 + for b,(lo,es,xs) in enumerate(blocks): + start[lo:lo+16] = xs[0] + final, _ = forward(start,events[8411:]) + patterns = [[0]*60,[1]*60] + [[int(i == j) for i in range(60)] for j in range(60)] + checked, peak = 0, 0 + for bits in patterns: + x = inverse_prefix(start,pre,bits) + actual, size = forward(x,events) + need(actual == final, 'complete prefix lift and full endpoint') + checked += 1; peak = max(peak,size.bit_length()) + for b,(lo,es,xs) in enumerate(blocks): + for xlocal in xs[1:]: + state = list(start); state[lo:lo+16] = xlocal + x = inverse_prefix(state,pre,[0]*60) + actual,size = forward(x,events) + need(actual == final, 'independent block lift reaches common full endpoint') + checked += 1; peak = max(peak,size.bit_length()) + # The written product proof supplies the unenumerated 2^76 quantifier. + upper = inverse_bound(bound,pre) + local_checks = 0 + for y,n,u in product(range(-64,65),(-1,1),(0,1)): + xs = [n*(2*y+(2*u-1)*r) for r in (0,1)] + need(xs[0] != xs[1] and all(sr(n*x,2,u) == y for x in xs), 'two-to-one half lemma') + local_checks += 1 + need([sr(2*x,2,0) for x in range(-5,6)] == list(range(-5,6)), + 'double-then-half is injective: raw half counts alone do not suffice') + # Altered output and a deleted collision state must invalidate the certificate. + try: + need(forward(fixture['blocks'][0]['input_preimages'][0],blocks[0][1])[0] == + [x+int(i == 0) for i,x in enumerate(fixture['blocks'][0]['output'])], 'wrong output') + except ValueError: + pass + else: + raise ValueError('wrong collision output accepted') + need(60+sum(2 for block in blocks) == 76 and 84-76 == 8, 'retention floor and possible headroom') + return dict(status='PASS_STOCHASTIC_RESTORATION_MEMORY',events=9589, + public_integer_roles=748,source_halves=halves,source_doubles=doubles, + surjective_prefix_events=8411,prefix_fiber_power=60, + independent_blocks=8,block_fiber_sizes=[4]*8,block_program_sha256=signatures, + full_fiber_power_lower=76,source_log_bits=84,maximum_possible_bit_saving=8, + full_word_lifts_checked=checked,half_lemma_checks=local_checks, + lift_bound_magnitude_bits=upper.bit_length(),fixture_peak_magnitude_bits=peak, + conservative_signed_guard_bits=upper.bit_length()+8, + scope='Worst-case retained information for the exact PR6066 forward map and unchanged tape; no matching upper bound or new kappa.') + + +def main(): + result = calculate() + need(result == json.loads((HERE/'RESULT.json').read_text()), 'committed semantic receipt') + print(json.dumps(result,sort_keys=True)) + + +if __name__ == '__main__': + main() From 57d183c60dddb18e1c44b15e5c39f3f3a6daaab7 Mon Sep 17 00:00:00 2001 From: zxv Date: Wed, 28 Oct 2026 01:32:05 -0400 Subject: [PATCH 2/2] Recover eight source residues and match the 76-bit lower bound --- .../PREDECESSOR.json | 7 +- .../stochastic-restoration-memory/PROOF.md | 30 ++- .../stochastic-restoration-memory/README.md | 20 +- .../stochastic-restoration-memory/RESULT.json | 46 ++++- .../stochastic-restoration-memory/TASK.json | 24 +-- .../stochastic-restoration-memory/VERIFY.json | 2 +- .../compressed.py | 175 ++++++++++++++++++ .../predecessor/PR6066-verify.py | 164 ++++++++++++++++ .../stochastic-restoration-memory/verify.py | 17 +- 9 files changed, 453 insertions(+), 32 deletions(-) create mode 100644 research/stochastic-restoration-memory/compressed.py create mode 100644 research/stochastic-restoration-memory/predecessor/PR6066-verify.py diff --git a/research/stochastic-restoration-memory/PREDECESSOR.json b/research/stochastic-restoration-memory/PREDECESSOR.json index 73a4931b9a..55bb045b6d 100644 --- a/research/stochastic-restoration-memory/PREDECESSOR.json +++ b/research/stochastic-restoration-memory/PREDECESSOR.json @@ -5,5 +5,10 @@ "retained_path": "predecessor/PR6066-README.md", "sha256": "bb6cee79d80fad16278141d1f0a42f348ec291eba288ee00668cdd59d5aab3d7", "license": "Apache-2.0", - "credit": "https://github.com/zxv" + "credit": "https://github.com/zxv", + "retained_verifier": { + "source_path": "research/reversible-stochastic-shears/verify.py", + "retained_path": "predecessor/PR6066-verify.py", + "sha256": "7e7a203f6c8f82443d7fd036c36d1659c3d2ffdbbc7f86aebeda49e6642af73c" + } } diff --git a/research/stochastic-restoration-memory/PROOF.md b/research/stochastic-restoration-memory/PROOF.md index ce7e8b4796..e5dd86052e 100644 --- a/research/stochastic-restoration-memory/PROOF.md +++ b/research/stochastic-restoration-memory/PROOF.md @@ -1,4 +1,4 @@ -# A 2^76 fiber in the exact PR6066 forward map +# An optimal 76-bit retained log for the exact PR6066 forward map This proof concerns the historical 748-role, 9,589-event scalar prefix used by [PR6066](https://github.com/CrocSwap/integer-mult-bounds/pull/6066). It does not transfer the result to the different selected PR6030 word. All incoming integer values are arbitrary dirty data. Fix every forward coin to zero; this is a permitted finite tape with positive probability under the fresh-coin model. The tape is retained unchanged. @@ -18,7 +18,7 @@ Counting all 84 halvings alone would be invalid: the later program has 32 doubli The next 1,121 events partition into eight consecutive programs on the disjoint role sets 272..287, 288..303, ..., 384..399. The first three blocks have 137 events each; the last five have 142 each. No block reads or writes outside its own sixteen roles. Each has three signed halvings and four doublings. -[COLLISIONS.json](COLLISIONS.json) supplies four distinct 16-integer preimages and their common output for each literal source block, with every coin zero. The verifier replays all 32 input vectors directly against the authenticated source events. It also runs an independently structured reverse branch interpreter: each halving branches into its two preimages and each inverse doubling rejects odd values. For the nominated output it checks that the complete surviving fiber is exactly the four committed vectors. This checks particular finite fibers; it does **not** prove four is a global maximum for other outputs or tapes. +[COLLISIONS.json](COLLISIONS.json) supplies four distinct 16-integer preimages and their common output for each literal source block, with every coin zero. The verifier replays all 32 input vectors directly against the authenticated source events. It also runs an independently structured reverse branch interpreter: each halving branches into its two preimages and each inverse doubling rejects odd values. For the nominated output it checks that the complete surviving fiber is exactly the four committed vectors. These are finite lower-bound witnesses. Section 5 independently proves a four-preimage upper bound for every output and tape by recovering one of each block's three residues. Take the Cartesian product of these eight four-element sets, fixing all other coordinates to zero at the start of the middle program. Disjoint support proves that its 4^8 = 2^16 distinct states have one identical complete 748-role output. Every following event is deterministic with the fixed tape, so the final 57 ADDs preserve this collision. @@ -42,7 +42,31 @@ All additional state capable of distinguishing inputs is included in A: logs, te This is a **worst-case** bound for exact pathwise restoration and the same forward map/tape. It does not bound average compressed length or prove that every tape needs 76 bits. It does not cover a changed rounding law, bounded-error restoration, restricted reached input set, or a different forward interface that leaves further input information in other outputs. Such extra information is payable and cannot be called clean scratch. -PR6066 supplies an 84-bit residue log. This lower bound leaves at most eight bits of possible worst-case log reduction under this boundary. It does not construct a 76-bit log, prove the block fibers never exceed four, or price a physical compression/cleanup routine. Working scratch, integer arithmetic, tape movement, the next native MOVE and complete supplier costs remain open. No new kappa or selected change follows. +## 5. Recover eight residues instead of retaining them + +Number a block's local roles x0,...,x15. Its first half acts on x9, after a twelve-ADD phase whose only source is x9. The source has two block templates. Immediately before this phase they satisfy, for arbitrary incoming integers and every fixed tape, + + first three blocks: x15 = 0 (mod 2), + last five blocks: x10 + x15 = 0 (mod 2). + +These are literal source invariants. The verifier derives them by propagating integer parity rows through the pre-phase program. Each fractional ADD is replaced by an entirely arbitrary independent integer contribution to its target. This enlarges the possible states, so any relation annihilating all original bits and all these extra noise bits holds for the actual rounded word. The derived annihilators are masks 0x8000 and 0x8400, respectively. Every coefficient column is checked. + +In the following twelve-ADD phase, x15 receives x9 exactly once with coefficient +1; x10 is unchanged. None of the fractional ADDs targets a parity holder. The holders do not include x9. Therefore, immediately after the signed half of x9, its discarded input parity is exactly + + first three blocks: x15 mod 2, + last five blocks: (x10 + x15) mod 2. + +The relation is independent of the rounding coins and of the magnitude of the data. In reverse, all later block events have already been undone when this half is reached. The displayed parity is consequently available from the current state. Recover it, apply the usual matched-coin inverse half, and continue. No retained bit is required for these eight particular halves. + +The other 76 signed halves use PR6066's original retained parity and cleanup rule. Forward arithmetic and every coin are unchanged; forward processing merely omits eight log writes. Reverse processing infers those eight bits using thirteen existing-value parity reads. All retained bits are cleared after reconstruction, as in the predecessor. The complete logical boundary is + + (x, y, U, 0^76) -> (x, y + F_U(x), U, 0^76). + +The intermediate forward boundary retains F_U(x), U and exactly 76 residue bits, with no additional input-dependent retained payload. This supplies a computable inverse on the reached image. Together with section 4 it proves **76 is the minimum worst-case retained information capacity at this logical boundary**. Equivalently, every fixed-tape fiber has size at most 2^76, and section 3 attains that size on the all-zero tape. Each tail block has at most four preimages: only its other two half residues can vary after the first is inferred. + +The source-bound checker compares the new forward endpoint with the exact unmodified PR6066 interpreter on 64 full protocols, using all-zero, all-maximum and independently generated mixed tapes and arbitrary signed dirty values. It checks exact restoration, all 76 cleaned residues, unchanged tape, and the same dirty accumulator update. A wrong parity-holder control fails on an actually reached state. The symbolic parity invariant, rather than these finite protocols, supplies the all-input/all-tape proof. + +This is an eight-bit reduction from the original 84-bit retained log (2/21, about 9.52%). It does not bound total physical working memory or execution time. Temporary integer scratch and its reversible cleanup, finite guards for arbitrary callers, tape access, the next native MOVE and the full supplier bill remain unpriced. Fewer retained bits do not alone imply a runtime improvement, new kappa, or a complete rounded multiplier. ## Credit diff --git a/research/stochastic-restoration-memory/README.md b/research/stochastic-restoration-memory/README.md index cfd540e052..b097e2e383 100644 --- a/research/stochastic-restoration-memory/README.md +++ b/research/stochastic-restoration-memory/README.md @@ -1,12 +1,14 @@ -# The PR6066 stochastic prefix needs at least 76 retained bits +# PR6066 stochastic restoration needs exactly 76 retained residue bits -For the exact integer-grid forward map in [PR6066](https://github.com/CrocSwap/integer-mult-bounds/pull/6066), with its random tape unchanged, exact dirty restoration needs auxiliary information with at least **76 bits of worst-case capacity**. The existing 84-bit parity log can therefore save at most eight bits under the same boundary. No matching compression algorithm or new kappa is claimed. +The historical [PR6066](https://github.com/CrocSwap/integer-mult-bounds/pull/6066) integer-grid protocol's retained log falls from **84 to 76 bits**, with the same stochastic forward map, unchanged random tape and exact arbitrary-dirty restoration. A matching 2^76-point collision proves 76 is optimal for retained information at this logical boundary. This saves eight bits (about 9.52%); physical working scratch and tape costs remain open. No new kappa is claimed. -The authenticated historical 9,589-event prefix has 60 halvings before any doubling. Its first 8,411 events are surjective and exactly 2^60-to-one on arbitrary integer data. Eight disjoint later 16-role blocks each have a verified four-preimage collision for one all-zero coin tape. Their product and the surjective prefix give a 2^76-point fiber of the full rounded forward map. [PROOF.md](PROOF.md) gives the quantifiers, finite-width guard and limits; [COLLISIONS.json](COLLISIONS.json) provides the small exact witnesses. +One residue in each of eight independent tail blocks can be inferred from current data when the inverse reaches it. For the first three blocks its input parity is one current role's parity; for the last five it is the sum of two roles' parities. A symbolic source-bound invariant proves these rules for every integer input and coin tape, including the fractional ADDs. No rounding event or coin changes. The other 76 residues follow the predecessor's original save/reconstruct/clear lifecycle. + +The lower bound uses 60 early halvings before any doubling, followed by eight disjoint four-preimage tail collisions. Their product gives exactly the retained-state requirement. [PROOF.md](PROOF.md) supplies both proofs and the exact source scope; [COLLISIONS.json](COLLISIONS.json) contains the small witnesses. The matching inverse is in compressed.py. ## Significance for researchers -This resolves a substantial part of PR6066's question about reducing its 84 parity bits. The 32 later doublings do not imply a 52-bit log is sufficient: chronology and source-bound collisions force at least 76 bits at the forward boundary. A smaller log would require proving and implementing a compression within the remaining eight-bit gap, or changing the forward/restoration contract. +This resolves PR6066's question about chronological reduction of the 84 parity bits at its logical boundary. The 32 later doublings do not make a 52-bit log possible; exact collisions force 76. The constructive upper bound also shows that keeping all 84 local residues was unnecessary. Next work can price the actual 76-bit interface instead of searching further for a smaller retained log under the same map. ## Reproduce @@ -15,16 +17,16 @@ python3.12 -B scripts/research_package.py --package research/stochastic-restorat python3.12 -B scripts/check_research_commit.py --package research/stochastic-restoration-memory ``` -The standard-library verifier authenticates the historical word and retained PR6066 statement, checks all 32 small collision preimages with exact integer arithmetic, exhausts each nominated block fiber, verifies disjoint literal source domains, and checks 86 complete lifted source executions plus signed-half and invalid-counting controls. The written composition proof supplies the 2^76 quantifier; this many inputs are not enumerated. Normal and optimized registered checks compare RESULT.json. +The standard-library checks authenticate the historical word and retained predecessor, verify all 32 small collision inputs and complete nominated fibers, derive both symbolic parity invariants, execute 86 whole-prefix collision lifts, and compare 64 full restored protocols against the unmodified predecessor interpreter. Signed-half and wrong-holder controls remain active under optimization. The written product proof supplies the 2^76 quantifier; that many inputs are not enumerated. RESULT.json is compared with the recomputation. ## Open next questions -Are all fibers of each tail block bounded by four, for every output and coin tape? Start with its eight exact inverse branches; a proof could close the remaining eight-bit information gap. Finite probes are not an all-tape proof. +Can the 76-bit protocol be lowered to a reversible integer/tape implementation with a favorable total cost? Start with the eight inferred-parity sites, thirteen existing-value parity reads and the complete scratch/cleanup ledger. Retained-log optimality does not price working memory or tape movement. -Can a smaller retained log be computed and erased under the actual physical caller at a favorable total cost? First distinguish retained information from working scratch, charge compression and random-tape movement, and keep every arbitrary dirty input. The native MOVE and full error/cost contracts remain blockers. +Can one actual native MOVE accept the resulting copied-output error and guard contract? Pin its source operands and completed error bound before composing the caller. The predecessor's stochastic error estimate and the complete native/caller costs remain separate obligations. ## Scope and credit -This uses the historical PR5599 prefix used by PR6066, not the different selected PR6030 word. The 76-bit floor is worst-case for exact pathwise restoration with arbitrary integer inputs and unchanged tape. It does not assert an average-length lower bound, a matching 76-bit implementation, a complete physical resource optimum, or a result for every small fixed width. A conservative 4,571-bit signed/guard width suffices for the entire collision family; executed representative fixtures need only ten magnitude bits. No native/selected cold replay or new kappa is claimed. +This uses the historical PR5599 prefix used by PR6066, not the different selected PR6030 word. Optimality concerns worst-case retained information for exact pathwise restoration with arbitrary integer data and unchanged tape. It does not assert an average-code-length lower bound or a total physical resource optimum. A conservative 4,571-bit signed/guard width suffices for the entire collision family; executed representative collision fixtures use ten magnitude bits. No selected/native cold replay, independent human review, proof-kernel acceptance or new kappa is claimed. -Prepared by [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance. Credit [Nick Petalas](https://github.com/petalas)'s [PR6026](https://github.com/CrocSwap/integer-mult-bounds/pull/6026), [Ali Romman](https://github.com/aliromman)'s [PR5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599), and the retained source lineage. The pending PR6066 statement is retained verbatim with exact head/hash. Apache-2.0. No independent human review or proof-kernel acceptance is claimed. +Prepared by [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance. Credit [Nick Petalas](https://github.com/petalas)'s [PR6026](https://github.com/CrocSwap/integer-mult-bounds/pull/6026), [Ali Romman](https://github.com/aliromman)'s [PR5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599), PR6066's restoration ABI and the retained P104 lineage. The pending predecessor statement and interpreter are retained verbatim with exact head/hash. Apache-2.0. diff --git a/research/stochastic-restoration-memory/RESULT.json b/research/stochastic-restoration-memory/RESULT.json index 7a3c1724d1..5f1b281fc6 100644 --- a/research/stochastic-restoration-memory/RESULT.json +++ b/research/stochastic-restoration-memory/RESULT.json @@ -20,6 +20,45 @@ "310fd43088b4f8d64285d0df3e0bee2a2eeafe4fb1aab6e06c4a5590de1a3c28" ], "conservative_signed_guard_bits": 4571, + "construction": { + "existing_value_parity_reads": 13, + "forward_law": "Byte-identical predecessor opcodes, coefficients and fresh tape; only residue retention changes.", + "full_tape_protocols": 64, + "omitted_parity_logs": 8, + "physical_scratch_and_movement": "Not priced; 76 counts retained residue capacity at the logical boundary.", + "recovery": { + "8460": [ + 287 + ], + "8597": [ + 303 + ], + "8734": [ + 319 + ], + "8877": [ + 330, + 335 + ], + "9019": [ + 346, + 351 + ], + "9161": [ + 362, + 367 + ], + "9303": [ + 378, + 383 + ], + "9445": [ + 394, + 399 + ] + }, + "retained_bits": 76 + }, "events": 9589, "fixture_peak_magnitude_bits": 10, "full_fiber_power_lower": 76, @@ -27,13 +66,14 @@ "half_lemma_checks": 516, "independent_blocks": 8, "lift_bound_magnitude_bits": 4563, - "maximum_possible_bit_saving": 8, + "optimal_retained_log_bits": 76, "prefix_fiber_power": 60, "public_integer_roles": 748, - "scope": "Worst-case retained information for the exact PR6066 forward map and unchanged tape; no matching upper bound or new kappa.", + "saved_log_bits": 8, + "scope": "Optimal retained residue capacity for the exact PR6066 logical boundary and unchanged tape; physical working scratch and full native costs remain open; no new kappa.", "source_doubles": 32, "source_halves": 84, "source_log_bits": 84, - "status": "PASS_STOCHASTIC_RESTORATION_MEMORY", + "status": "PASS_OPTIMAL_STOCHASTIC_RETAINED_LOG", "surjective_prefix_events": 8411 } diff --git a/research/stochastic-restoration-memory/TASK.json b/research/stochastic-restoration-memory/TASK.json index 5570c3880e..013f55e767 100644 --- a/research/stochastic-restoration-memory/TASK.json +++ b/research/stochastic-restoration-memory/TASK.json @@ -63,27 +63,27 @@ ] }, "scope_status": "refined", - "actual_scope": "Investigate PR6066 chronological restoration-log compression by constructing a source-bound large fiber of its exact forward rounded map.", + "actual_scope": "Construct and prove an optimal 76-bit retained residue log for the exact PR6066 forward map, including a matching 2^76 collision lower bound and source-derived parity recovery.", "scope_change_reason": "Explicit assignment starts with recent zxv PRs; this addresses PR6066 open question on the 84 retained parity bits.", "bottleneck_link": "Bounds the possible storage improvement before paying for a new reversible numerical interface; no direct exponent gain is inferred.", "budget_minutes": 30, - "stop_rule": "Stop at a proved source-bound memory floor and bounded exact replay. Treat a matching compression and all-tape block upper bound as separate tasks.", - "outcome": "negative-result", - "evidence": "PROOF.md; COLLISIONS.json; RESULT.json: 86 whole-prefix lifts, 32 block collision inputs, complete nominated fibers and 516 signed-half checks.", + "stop_rule": "Stop at a matching logical lower/upper bound and bounded exact replay. Total physical working scratch, guard widths and native caller pricing remain separate.", + "outcome": "completed", + "evidence": "PROOF.md; COLLISIONS.json; compressed.py; RESULT.json: symbolic all-tape parity certificates, 86 collision lifts and 64 full protocols compared with the literal predecessor.", "author": "zxv", "ai_assistance": "Substantial OpenAI Codex assistance in source review, proof, exact search, implementation and verification; no subagents or independent human/formal review.", "open_questions": [ { - "question": "Is every tail-block fiber at most four for arbitrary outputs and fixed tapes?", - "why_it_matters": "Could close the remaining eight-bit information gap.", - "first_step": "Analyze the eight exact inverse branches for each of the two source templates.", - "blocked_by": "A universal upper bound is unproved; finite probes are insufficient." + "question": "Can the 76-bit retained log be implemented with a favorable complete reversible integer/tape bill?", + "why_it_matters": "Retained information capacity is not total working memory or runtime.", + "first_step": "Lower the eight inference sites, thirteen current-value parity reads and all scratch cleanup.", + "blocked_by": "No physical tape/arithmetic implementation or complete fee supplied." }, { - "question": "Can a smaller retained log be compressed and erased under the actual native caller?", - "why_it_matters": "Information capacity alone does not pay for scratch, tape access or cleanup.", - "first_step": "Give the exact forward boundary, reversible algorithm and total physical bill.", - "blocked_by": "Full physical/native/error interface remains open." + "question": "Can the next native MOVE use this copied-output error/guard boundary?", + "why_it_matters": "Needed before the stochastic prefix can become a complete supplier.", + "first_step": "Pin actual operands, full approximation error and restored endpoint.", + "blocked_by": "Native and complete caller/precision contract remain open." } ] } diff --git a/research/stochastic-restoration-memory/VERIFY.json b/research/stochastic-restoration-memory/VERIFY.json index 94838e0636..456da8097a 100644 --- a/research/stochastic-restoration-memory/VERIFY.json +++ b/research/stochastic-restoration-memory/VERIFY.json @@ -15,7 +15,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Exact source-bound product collisions, complete nominated block fibers, lifted source executions and controls" + "checks": "Exact lower-bound collisions, symbolic all-tape parity recovery, 76-bit protocols against literal predecessor and controls" }, { "argv": [ diff --git a/research/stochastic-restoration-memory/compressed.py b/research/stochastic-restoration-memory/compressed.py new file mode 100644 index 0000000000..6288e89be0 --- /dev/null +++ b/research/stochastic-restoration-memory/compressed.py @@ -0,0 +1,175 @@ +"""Exact 76-bit retained log; physical integer/tape scratch remains unpriced.""" +from itertools import product +from random import Random + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def nullspace(rows, columns): + rows = list(rows) + pivots, rank = [], 0 + for j in range(columns): + i = next((i for i in range(rank,len(rows)) if rows[i] >> j & 1), None) + if i is None: + continue + rows[rank], rows[i] = rows[i], rows[rank] + for i in range(len(rows)): + if i != rank and rows[i] >> j & 1: + rows[i] ^= rows[rank] + pivots.append(j) + rank += 1 + basis = [] + for j in range(columns): + if j in pivots: + continue + mask = 1 << j + for i,col in enumerate(pivots): + if rows[i] >> j & 1: + mask ^= 1 << col + basis.append(mask) + return basis + + +def plan(events): + cursor, result = 8411, {} + for b in range(8): + lo, size = 272+16*b, 137 if b < 3 else 142 + es = events[cursor:cursor+size] + half = next(i for i,e in enumerate(es) if e[0] == 'SCALE' and e[-1] == 2) + target = es[half][1] + start = half + while start and es[start-1][0] == 'ADD' and es[start-1][2] == target: + start -= 1 + need(half-start == 12 and es[half][3:] == (1,2), 'literal first-half phase') + # Parity rows over the original 16 bits and independent fresh noise bits + # for every fractional shear. This grants more possible states than the + # true rounded map and makes the relation valid for every input and tape. + rows, variables = [1 << j for j in range(16)], 16 + for op,r,s,n,d in es[:start]: + r -= lo + if op == 'ADD': + if d > 1: + rows[r] ^= 1 << variables + variables += 1 + elif n & 1: + rows[r] ^= rows[s-lo] + else: + need(d == 1 and n in (-1,2), 'integer pre-phase SCALE') + if not n & 1: + rows[r] = 0 + transpose = [sum(((rows[r] >> j) & 1) << r for r in range(16)) + for j in range(variables)] + basis = nullspace(transpose,16) + candidates = [] + for bits in product((0,1),repeat=len(basis)): + mask = 0 + for bit,v in zip(bits,basis): + if bit: + mask ^= v + if mask >> (target-lo) & 1: + continue + phase = es[start:half] + if any(d > 1 and mask >> (r-lo) & 1 for op,r,s,n,d in phase): + continue + if sum(n for op,r,s,n,d in phase if mask >> (r-lo) & 1) % 2: + candidates.append(mask) + need(candidates, 'recoverable half parity') + mask = min(candidates) + need(all((mask & row).bit_count() % 2 == 0 for row in transpose), + 'complete pre-phase parity relation') + holders = tuple(lo+j for j in range(16) if mask >> j & 1) + need(holders == ((lo+15,) if b < 3 else (lo+10,lo+15)), + 'literal recovery holders') + result[cursor+half] = holders + cursor += size + return result + + +def rounded(n,d,u): + q,r = divmod(n,d) + return q+int(u < r) + + +def forward(initial,events,tape,recovery): + x, logs = list(initial), [] + for i,((op,r,s,n,d),u) in enumerate(zip(events,tape)): + if op == 'ADD': + x[r] += rounded(n*x[s],d,u) + else: + if d == 2 and i not in recovery: + logs.append((n*x[r]) % 2) + x[r] = rounded(n*x[r],d,u) + return x,logs + + +def backward(current,events,tape,logs,recovery): + x, logs = list(current), list(logs) + index = len(logs) + for i in range(len(events)-1,-1,-1): + op,r,s,n,d = events[i] + u = tape[i] + if op == 'ADD': + x[r] -= rounded(n*x[s],d,u) + elif d == 2: + if i in recovery: + bit = sum(x[j] for j in recovery[i]) % 2 + else: + index -= 1 + need(index >= 0, 'retained residue available') + bit = logs[index] + x[r] = n*(2*x[r]-2*int(u < bit)+bit) + if i not in recovery: + logs[index] ^= (n*x[r]) % 2 + need(logs[index] == 0, 'retained residue cleaned') + elif n == 2: + need(x[r] % 2 == 0, 'reached doubled image') + x[r] //= 2 + else: + x[r] = -x[r] + need(index == 0 and not any(logs), 'all 76 residue bits cleaned') + return x,logs + + +def verify(events,old): + recovery = plan(events) + need(len(recovery) == 8 and sum(map(len,recovery.values())) == 13, + 'eight recovered residues from thirteen existing parity reads') + rng = Random(606676) + count = 0 + broken = dict(recovery) + broken[min(broken)] = () + rejected = False + for case in range(64): + initial = ([0]*748 if case == 0 else + [((j*73)%251)-125 for j in range(748)] if case == 1 else + [rng.randrange(-(1<<30),1<<30) for _ in range(748)]) + tape = tuple(0 if case%4 == 0 else d-1 if case%4 == 1 else rng.randrange(d) + for op,r,s,n,d in events) + saved = tuple(tape) + expected,old_logs = old.forward(initial,events,tape) + actual,logs = forward(initial,events,tape,recovery) + need(actual == expected and len(old_logs) == 84 and len(logs) == 76, + 'unchanged literal predecessor forward map') + restored,clean = backward(actual,events,tape,logs,recovery) + need(restored == initial and clean == [0]*76 and tape == saved, + 'exact dirty restoration and unchanged tape') + # Copying the same forward value to a dirty accumulator has the same ABI. + accumulator = [17*j-12345 for j in range(748)] + need([a+x for a,x in zip(accumulator,actual)] == + [a+x for a,x in zip(accumulator,expected)], 'same compute-accumulate endpoint') + if not rejected: + try: + bad,_ = backward(actual,events,tape,logs,broken) + rejected = bad != initial + except ValueError: + rejected = True + count += 1 + # A false zero-parity replacement must fail on a reached input/tape. + need(rejected, 'wrong parity holder rejected on a full reached state') + return dict(retained_bits=76,omitted_parity_logs=8,existing_value_parity_reads=13, + full_tape_protocols=count,recovery={str(i):list(v) for i,v in recovery.items()}, + forward_law='Byte-identical predecessor opcodes, coefficients and fresh tape; only residue retention changes.', + physical_scratch_and_movement='Not priced; 76 counts retained residue capacity at the logical boundary.') diff --git a/research/stochastic-restoration-memory/predecessor/PR6066-verify.py b/research/stochastic-restoration-memory/predecessor/PR6066-verify.py new file mode 100644 index 0000000000..94106a084e --- /dev/null +++ b/research/stochastic-restoration-memory/predecessor/PR6066-verify.py @@ -0,0 +1,164 @@ +"""Source-bound stochastic compute/accumulate/uncompute on an integer grid.""" +from fractions import Fraction as Q +from itertools import product +from pathlib import Path +from random import Random +import gzip +import hashlib +import json + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +WORD='research/p104-helper-subspace-splits/WORD.json.gz' + + +def need(ok,msg): + if not ok:raise ValueError(msg) + + +def sr(n,d,u): + need(d>0 and d&(d-1)==0 and 0<=u1 for _,_,_,_,d in events) + need(ops=={'ADD':9358,'SCALE':231} and bits==11713 and h==84 and rounded==7421,'source ledger') + rng=Random(6026) + fixtures=[[0]*748,[((i*73)%251)-125 for i in range(748)], + [(-1 if i%2 else 1)*((1<<30)+104729*i) for i in range(748)], + [rng.randrange(-10**6,10**6) for _ in range(748)]] + full=peak=0 + for initial in fixtures: + target=[i*17-12345 for i in range(748)] + for mode in range(4): + tape=tuple(0 if mode==0 else d-1 if mode==1 else i%d if mode==2 + else hashlib.sha256(str(i).encode()).digest()[0]%d + for i,(_,_,_,_,d) in enumerate(events)) + _,size=protocol(initial,target,events,tape);peak=max(peak,size);full+=1 + # Same uncomplemented coin is an actual failing inverse, not a guarantee. + y=sr(1,2,0);bad=y+sr(-1,2,0) + need(bad!=0,'uncomplemented-coin counterexample') + reused=sum(sr(sr(1,2,u),2,u) for u in (0,1)) + fresh=sum(sr(sr(1,2,u),2,v) for u,v in product((0,1),repeat=2)) + need(Q(reused,2)==Q(1,2) and Q(fresh,4)==Q(1,4), + 'restored tape is not fresh for an adaptive second shear') + need(sr(0,2,1)==sr(1,2,1),'one side bit necessary for local halving') + rejected(lambda:need(2*sr(1,2,0)==1,'discarded half residue')) + es=[('SCALE',0,None,1,2)];y,log=forward([1],es,(0,));log[0]=0 + rejected(lambda:need(backward(y,es,(0,),log)[0]==[1],'corrupt residue')) + rejected(lambda:sr(1,3,0)) + rejected(lambda:sr(1,2,2)) + rejected(lambda:forward([1],[],(0,))) + print(json.dumps(dict(status='PASS_REVERSIBLE_STOCHASTIC_PREFIX',local_coin_identities=identities, + signed_halves=halves,tiny_protocols=tiny_cases,full_prefix_protocols=full, + events=9589,random_bits=bits,clean_residue_bits=h, + forward_reverse_and_copy_macros=2*len(events)+748, + peak_fixture_value_bits=peak, + scope='logical scalar-grid ABI; physical sampler/native costs open; no new kappa'),sort_keys=True)) + + +if __name__=='__main__':main() diff --git a/research/stochastic-restoration-memory/verify.py b/research/stochastic-restoration-memory/verify.py index c4661d9aab..e86112d3e5 100644 --- a/research/stochastic-restoration-memory/verify.py +++ b/research/stochastic-restoration-memory/verify.py @@ -5,6 +5,7 @@ from pathlib import Path import gzip import json +import types HERE = Path(__file__).resolve().parent ROOT = HERE.parents[1] @@ -172,15 +173,25 @@ def calculate(): else: raise ValueError('wrong collision output accepted') need(60+sum(2 for block in blocks) == 76 and 84-76 == 8, 'retention floor and possible headroom') - return dict(status='PASS_STOCHASTIC_RESTORATION_MEMORY',events=9589, + p = json.loads((HERE/'PREDECESSOR.json').read_text())['retained_verifier'] + raw = (HERE/p['retained_path']).read_bytes() + need(sha256(raw).hexdigest() == p['sha256'], 'literal predecessor verifier') + old = types.ModuleType('retained_pr6066') + old.__file__ = str(HERE/p['retained_path']) + exec(compile(raw,old.__file__,'exec'),old.__dict__) + compressed = types.ModuleType('compressed_source') + exec(compile((HERE/'compressed.py').read_bytes(),str(HERE/'compressed.py'),'exec'),compressed.__dict__) + construction = compressed.verify(events,old) + return dict(status='PASS_OPTIMAL_STOCHASTIC_RETAINED_LOG',events=9589, public_integer_roles=748,source_halves=halves,source_doubles=doubles, surjective_prefix_events=8411,prefix_fiber_power=60, independent_blocks=8,block_fiber_sizes=[4]*8,block_program_sha256=signatures, - full_fiber_power_lower=76,source_log_bits=84,maximum_possible_bit_saving=8, + full_fiber_power_lower=76,source_log_bits=84,optimal_retained_log_bits=76, + saved_log_bits=8,construction=construction, full_word_lifts_checked=checked,half_lemma_checks=local_checks, lift_bound_magnitude_bits=upper.bit_length(),fixture_peak_magnitude_bits=peak, conservative_signed_guard_bits=upper.bit_length()+8, - scope='Worst-case retained information for the exact PR6066 forward map and unchanged tape; no matching upper bound or new kappa.') + scope='Optimal retained residue capacity for the exact PR6066 logical boundary and unchanged tape; physical working scratch and full native costs remain open; no new kappa.') def main():