From a6f54b6048db1b6d49fdecba2ad5e28827a620c4 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 00:51:38 +0000 Subject: [PATCH 1/2] feat(research): prove a deferred-delivery restoration bound --- research/last-read-restoration-bound/PROOF.md | 132 +++++++++ .../last-read-restoration-bound/README.md | 136 +++++++++ .../last-read-restoration-bound/SOURCES.json | 30 ++ .../last-read-restoration-bound/TASK.json | 98 +++++++ .../last-read-restoration-bound/VERIFY.json | 34 +++ .../last-read-restoration-bound/verify.py | 257 ++++++++++++++++++ 6 files changed, 687 insertions(+) create mode 100644 research/last-read-restoration-bound/PROOF.md create mode 100644 research/last-read-restoration-bound/README.md create mode 100644 research/last-read-restoration-bound/SOURCES.json create mode 100644 research/last-read-restoration-bound/TASK.json create mode 100644 research/last-read-restoration-bound/VERIFY.json create mode 100644 research/last-read-restoration-bound/verify.py diff --git a/research/last-read-restoration-bound/PROOF.md b/research/last-read-restoration-bound/PROOF.md new file mode 100644 index 0000000000..87fdd3bc68 --- /dev/null +++ b/research/last-read-restoration-bound/PROOF.md @@ -0,0 +1,132 @@ +# Deferred delivery and exact workspace restoration + +This proof and its finite corroboration were produced by Nick Petalas. +Apache-2.0. Claim type: scoped mathematical proof. Injectivity, counting and +matrix-rank facts are classical; no literature-priority claim is made for them. + +## 1. Contract at a last-read cut + +Fix the initial workspace w0, initial output y0, future sources z and an +entire random tape rho. The earlier source is x. The complete workspace at +the cut is c(x) in a set W, of any size or alphabet. Include persistent +heads, control, transcripts and any other state affecting the continuation. + +The cut output a is independent of x under these fixed conditions. It can +depend on w0, y0, z and rho. This permits pre-cancellation of incoming dirt, +but forbids delivering an x-dependent part of this output early. After the cut: + +1. No further read of x is allowed, including an omitted x-dependent choice + of continuation. +2. The final workspace is s(c(x)), where s: W -> W is injective. Invertible + workspace updates independent of output contents suffice. +3. The final output is a+d(c(x)), with outputs in an abelian group and d + arbitrary. Outputs supply no information back to the workspace. The + theorem also holds for an arbitrary final-output function of c. + +The intended endpoint is workspace w0 and output y0+F(x). The required +deferred increment f(x)=y0+F(x)-a has the same fibre sizes as F. No linearity, +fixed workspace dimension or bounded computation is needed below. + +This is a proposed interface, not a description of a selected word. +Reversibility of the combined workspace/output map alone does not imply +item 2. Output feedback is an explicit escape in section 5. + +## 2. Sharp joint-success theorem + +Let X have any finite distribution mu, independent of the fixed initial +state, future sources and random tape. Put p_max=max_v Pr[F(X)=v]. Then + +`Pr[output correct AND workspace restored] <= p_max`. (1) + +Injectivity implies that at most one cut state u satisfies s(u)=w0. If none +exists, joint success is empty. Otherwise every jointly successful x has +c(x)=u, hence f(x)=d(u). These inputs lie in one fibre of f, of mass at most +p_max. This proves (1). Conditioning on each independent random tape proves +the same bound for randomized protocols, including nonlinear ones. The +argument is valid for each fixed future input and arbitrary fixed dirt. + +Let e_out be the final output error probability and e_work the probability +that the complete final workspace differs from w0. By the union bound, + +`e_out + e_work >= 1-p_max`. (2) + +For uniform X in F_q^d and F(x)=Lx of rank r, every fibre has q^(d-r) points. +For every finite field, therefore, + +`Pr[correct AND restored] <= q^(-r)`, +`e_out + e_work >= 1-q^(-r)`. (3) + +Any nonzero deferred linear target prevents simultaneous zero-error delivery +and exact restoration in this contract. More workspace cannot remove this +obstruction. A single nonzero binary target forces the sum of the two error +probabilities to be at least 1/2. For r=0 the bound is zero. + +## 3. Attainment on the whole error boundary + +For any finite field and any rank-r map L with codomain F_q^t, take distinct +workspace and output registers w,y in F_q^t with arbitrary initial values. +Execute: + +```text +before cut: y -= w +before cut: w += Lx # the only read of x +after cut: y += w +``` + +At the cut y=y0-w0, independent of x. The output is always y0+Lx. The final +workspace w0+Lx is restored exactly on ker L, with probability q^(-r). The +suffix workspace map is the identity. This attains +`(e_out,e_work)=(0,1-q^(-r))` on arbitrary incoming dirt and output values. + +Leaving both registers unchanged instead attains `(1-q^(-r),0)`. An +independent coin choosing between the two programs attains every point on +`e_out+e_work=1-q^(-r)` in the nonnegative quadrant. Thus (3) is the sharp +lower boundary of this error pair. These are logical state transitions; +no native realization, free operation or favorable paid invoice is asserted. + +## 4. Rank obstruction over every field + +For a linear computation let the cut workspace be Bx+b. Since the cut output +has zero x coefficient, the final output's x coefficient is L=CB for some +C. The final workspace's x coefficient is E=AB with A invertible. Thus + +`rank L <= rank B = rank E`. (4) + +E measures dependence on x, not on incoming dirt. Exact restoration requires +E=0, forcing L=0. This holds over infinite fields too. The program in section +3 has B=L and A=C=I, attaining equality for every rank. + +## 5. Changed-premise controls + +The first four programs change a hypothesis and deliver/restore exactly. +The last control exposes omitted state. None is a counterexample to (1). + +* Read x again after section 3's delivery and execute w-=Lx. This pays a + second source-dependent operation, the usual missing inverse call. +* With clean initial workspace, load Lx, deliver it and erase workspace to + zero. The suffix workspace map is not injective. Erasure/history costs + need their own implementation and cannot be treated as zero. +* Allow output feedback. Before the cut swap w and y, then add Lx to w. + At the cut y=w0, independent of x. After the cut swap w and y again. + The endpoint is `(w,y)=(w0,y0+Lx)` for arbitrary incoming values. This is + reversible on the combined pair, but the suffix workspace is not a + function of workspace alone. No ADD decomposition of SWAP is claimed. +* Deliver y+=Lx before the cut and leave workspace untouched. Delivery is + no longer deferred. +* Leave a source-dependent log outside the reported workspace. Apparent + restoration can leave that log dirty; including it restores the boundary. + +This excludes no construction using source rereads, readable outputs, paid +irreversibility, early accumulation or retained history. It is a rejection +test for a declared one-pass deferred helper interface, not a universal +network, compiler or multiplication lower bound. No new kappa follows. + +## 6. Finite evidence + +The verifier exhausts literal prefix maps, suffix permutations and output +maps on three declared small domains. It scores each input directly, without +using a rank/fibre bound to compute the score. Separate finite-field gate +executions check attainment and changed-premise escapes on arbitrary dirty +workspace and output values. Elimination checks (4) on separate matrices. +All checks remain active under optimized Python. The finite evidence +corroborates the written proof; it does not extrapolate it from sample fields. diff --git a/research/last-read-restoration-bound/README.md b/research/last-read-restoration-bound/README.md new file mode 100644 index 0000000000..017b63f9d4 --- /dev/null +++ b/research/last-read-restoration-bound/README.md @@ -0,0 +1,136 @@ +# Sharp error boundary for deferred delivery through restored workspace + +This contribution was produced by Nick Petalas. Apache-2.0. + +A helper cannot retain an earlier input after its last read, deliver a +nonzero target later, and restore all workspace under the following contract: +the output at the cut contains no earlier-input dependence, the continuation +reads no earlier input, and its workspace map is injective and independent +of output contents. This includes arbitrary nonlinear workspace computation +and independent randomness, with every persistent control/log included. + +For a uniform source in F_q^d and a rank-r deferred target, the sharp law is + +```text +Pr[correct output AND exact workspace restoration] <= q^(-r) +output error probability + restoration failure probability >= 1-q^(-r) +``` + +Every point on the lower boundary is attainable by mixing two explicit +logical programs. One delivers the target exactly and leaves a rank-r +workspace defect; the other restores exactly and guesses the zero target. +Over any field, a linear implementation has +`rank(deferred target) <= rank(final workspace dependence on earlier input)`. +For a general finite source distribution and arbitrary target F, replace +q^(-r) by the largest probability of a fibre of F. + +Claim type: scoped written mathematical proof with finite corroboration. +[PROOF.md](PROOF.md) gives the contract, argument, attaining programs and +explicit escapes. Elementary counting, injectivity and rank facts are +classical. The contribution is their sharp application to this declared +causal/restoration interface, with its exact error frontier and controls. +No literature-priority claim is made for the underlying facts. + +## Evidence and reproduction + +From the repository root, using the recorded interpreter or another CPython +3.12 installation with the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/last-read-restoration-bound/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/last-read-restoration-bound/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/last-read-restoration-bound +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/last-read-restoration-bound --check-source-history +``` + +The direct marker is `PASS_LAST_READ_RESTORATION_BOUND`. The verifier writes +nothing and emits a generated JSON receipt bound to all six package files. +It exhausts prefix functions, suffix permutations, output functions and +initial states on the declared domains. It separately executes the attaining +programs, independent four-outcome coin mixtures, and changed-premise escapes +on finite-field inputs with arbitrary dirt and output values. Rationally +stated probabilities are checked by integer counts. Matrix elimination checks +the rank inequality on every 2x2 cut/readout matrix and invertible suffix over +F2 and F3. Explicit requirements stay active under optimization. + +The universal result rests on the written proof. The finite checks certify +their enumerated domains. Hosted execution and independent mathematical +acceptance are separate. + +Local warning-strict normal and optimized direct checks passed. The three +abstract scans enumerate 6,649,846 protocol/initial-state cases and 26,245,090 +input executions: all target functions on 4/2/2 and 3/3/3 source/work/output +alphabets, and the identity target on 4/4/4. Six finite-field gate fixtures +enumerate 81,162 input/dirt/output triples and five four-outcome coin mixtures +each. All 316,464 linear matrix triples pass, with a separate image-cardinality +rank oracle. Ten invalid domains reject. Four changed-premise escapes and +the complete hidden-log debt are checked. Each registered command was +timed locally below six seconds against its 120-second limit; no runtime +improvement is claimed. + +## Scope and connection to the bottleneck + +This is an original changed-scope result under `coverage-law-change` at main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected PR6030. +The selected metadata orientation passed. The selected supplier's complete +signed bill remains the binding question; this package changes neither that +bill nor any selected record. + +A proposed one-pass helper cannot omit its inverse input operation while +silently assuming deferred delivery and full restoration under this contract. +Source rereads, readable outputs, early accumulation, noninjective workspace +steps or a retained transcript change the conclusion. The verifier exhibits +these escapes. In particular, whole-program reversibility does not imply an +injective workspace-only suffix when outputs feed back into workspace. + +No existing selected schedule is asserted to satisfy the excluded contract. +There is no physical/native implementation, complete paid/target invoice, +compiler closure, ownership, precision, stock, tape, outer recovery or new +kappa result. All five selected framework assumptions remain. Selected cold +replay, Lean and Docker were unrun. Independent human and formal proof-kernel +review are unclaimed. Family decision: finish this scoped obstruction; a +physical expansion needs a named feedback/reread contract and complete bill. + +## Related work and credit + +The current construction and its historical contributors retain their credit +through the selected record. No predecessor executable, fixture, count or +proof is replayed as the result. PR1203's dirty-state wrapper uses both a +source call and its inverse; that explicit reread is outside the excluded +contract. PR6015 concerns exact finite-menu endpoint choices, and PR6134 +concerns random observation cost/error tradeoffs. Neither is being audited +or extended as the question's source. The local source pins are historical +orientation provenance only. No mathematical input is imported. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363385) +records this original target. Main README/general-form searches, merged +searches, live open PRs and the last hour of handoff posts were checked. +Sparse local notes, arbitrary historical diffs and unpublished work remain +coverage limits; an absence of matches is not a novelty proof. + +## Open next questions + +Can one actual helper/caller use output feedback to avoid the second source +call at a favorable complete cost? Start with one concrete late target and +implement its two swaps or another feedback map with all arbitrary inputs, +legal frames, owned lifetimes and the complete signed invoice. The missing +physical interface and favorable bill block a supplier claim. The structured +question is in TASK.json. This package stops at its first proved result. + +## Verifier constraints + +The standalone verifier has fixed domains: source/work/output cardinalities +at most four for the abstract scan; q in {2,3,5}, ranks one/two for the literal +gates; 2x2 matrices over F2/F3 for the linear scan. Loops have explicit bounds, +there is no recursion, subprocess, source import, dynamic code or file write, +and all functions are below sixty lines. Reads are confined to the six local +files, each capped at one MiB, for the output receipt. Failures propagate +without a success marker. + +Power of Ten rule 3 deviation: CPython allocates tuples, integers and Counter +entries during replay. Fixed fixture domains bound live collections; the +largest materialized function table has 256 entries and protocols are scored +one at a time. No fixed-allocation runtime is claimed. Revisit storage before +accepting arbitrary sizes or production use. Warning-strict normal/optimized +replay and in-memory syntax compilation provide the available diagnostics; +no separate static analyzer or production backend is claimed. diff --git a/research/last-read-restoration-bound/SOURCES.json b/research/last-read-restoration-bound/SOURCES.json new file mode 100644 index 0000000000..d48e7c3a03 --- /dev/null +++ b/research/last-read-restoration-bound/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "docs/research/bottleneck-brief.md", + "usage": "provenance", + "git_blob": "df5b2001ceedde599cf18d7362cebe3bf7c7e00b", + "sha256": "d4b6c3d7f354ab9227e0e2e723b31d2e8d3a5b2151c18d51688efd06393f3117" + }, + { + "path": "docs/research/current-priorities.md", + "usage": "provenance", + "git_blob": "6f5d40d13d8f3bdc12ce7954c8c3eb4ab1f8be91", + "sha256": "70f61c8d140ae6e892f2b8f065bba4eae3e76f7a8f55f632fd4e2f9f34039bdc" + } + ] +} diff --git a/research/last-read-restoration-bound/TASK.json b/research/last-read-restoration-bound/TASK.json new file mode 100644 index 0000000000..4a0b618e9a --- /dev/null +++ b/research/last-read-restoration-bound/TASK.json @@ -0,0 +1,98 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "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": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp joint output-error/restoration-error boundary for a last-read cut with deferred delivery and an injective output-independent workspace continuation; nonlinear finite-state and all-field linear statements.", + "scope_change_reason": "Investigate an original causal helper contract directly. The result is an interface obstruction, not the card's complete paid/productive supplier gate.", + "bottleneck_link": "A proposed helper split cannot omit its inverse source call by retaining past input in restored workspace under this declared streaming contract. Any escape must expose source rereads, output feedback, early delivery, noninjective work or a retained log, and price it. No selected word is asserted to satisfy the excluded contract.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved sharp obstruction and its finite corroboration; do not optimize a physical implementation or expand the model.", + "outcome": "completed", + "evidence": "PROOF.md and the read-only verify.py generated hash-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual helper/caller use output feedback to avoid the second source call at a favorable complete cost?", + "why_it_matters": "The output-feedback control escapes the theorem, but a cheaper logical contract is not a paid supplier.", + "first_step": "Locate one concrete late target and implement its two swaps or another feedback map with all dirty inputs, legal frames, owned lifetimes and the full signed invoice.", + "blocked_by": "No source-bound physical feedback interface or favorable complete bill is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363385", + "scientific_claim_type": "scoped proof with finite corroboration", + "overlap": { + "checked_at_utc": "2026-11-03T00:43:00Z", + "source": "original", + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "coverage": "Main README/general-form and targeted merged searches; complete 431-open-PR / 6406-Discussion cache with pagination at 2026-11-03 00:42-00:43 UTC; live precommit open PRs and handoff claims. Local cache notes covered 126 of 8917 HEAD note records, supplemented by targeted Git searches. Unpublished work and arbitrary historical diffs remain limits.", + "nearest_context": [ + "PR1203: source/inverse-source dirty wrapper; no predecessor replay", + "PR6015: finite-menu exact endpoint adaptivity; different contract", + "PR6134: random observation cost/error frontier; different contract" + ] + }, + "engineering_playbook": "autonomous local run", + "verification_environment": { + "python": "Python 3.12.15", + "dependencies": "standard library only", + "unrun": [ + "selected cold replay", + "native/tape implementation", + "Lean", + "Docker", + "independent human or formal proof-kernel review" + ] + } +} diff --git a/research/last-read-restoration-bound/VERIFY.json b/research/last-read-restoration-bound/VERIFY.json new file mode 100644 index 0000000000..f1ab58adaa --- /dev/null +++ b/research/last-read-restoration-bound/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete finite-state enumeration, literal dirty gate programs and five mixtures, changed-premise controls, all 2x2 linear rank cases over F2/F3, explicit invalid-domain rejection." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete checks under optimized Python, with all explicit requirements active." + } + ] +} diff --git a/research/last-read-restoration-bound/verify.py b/research/last-read-restoration-bound/verify.py new file mode 100644 index 0000000000..051b96b09c --- /dev/null +++ b/research/last-read-restoration-bound/verify.py @@ -0,0 +1,257 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Finite corroboration produced by Nick Petalas. Writes no files.""" + +from collections import Counter +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def finite_case(source_size, work_size, output_size, all_targets): + require(1 <= source_size <= 4, "source size bound") + require(1 <= work_size <= 4 and 1 <= output_size <= 4, "state size bounds") + targets = tuple(product(range(output_size), repeat=source_size)) + if not all_targets: + require(source_size == output_size, "identity target domain") + targets = (tuple(range(source_size)),) + suffixes = tuple(permutations(range(work_size))) + outputs = tuple(product(range(output_size), repeat=work_size)) + counts = Counter() + maxima = [] + for target in targets: + maximum = 0 + bound = max(Counter(target).values()) + for prefix in product(range(work_size), repeat=source_size): + for suffix in suffixes: + final = tuple(suffix[w] for w in prefix) + for readout in outputs: + delivered = tuple(readout[w] for w in prefix) + for initial in range(work_size): + score = sum(final[x] == initial and delivered[x] == target[x] + for x in range(source_size)) + require(score <= bound, "literal joint-success bound") + maximum = max(maximum, score) + counts[score] += 1 + require(maximum == bound, "sharp bound for every target") + maxima.append(maximum) + return {"source_size": source_size, "workspace_size": work_size, + "output_size": output_size, "targets": len(targets), + "protocols": sum(counts.values()), "input_runs": source_size * sum(counts.values()), + "joint_success_histogram": dict(sorted(counts.items())), "attaining_maxima": maxima} + + +def add(left, right, q, sign=1): + require(len(left) == len(right), "equal vector lengths") + return tuple((a + sign * b) % q for a, b in zip(left, right)) + + +def target_value(x, rank, q): + require(len(x) == rank + 1 and 1 <= rank <= 2, "target shape") + return tuple((x[j] + (j + 1) * x[-1]) % q for j in range(rank)) + + +def execute(kind, x, initial_work, initial_output, q): + """Literal logical updates; return cut output, final work and output.""" + rank = len(initial_work) + value = target_value(x, rank, q) + work, out = initial_work, initial_output + if kind == "guess": + return out, work, out + if kind == "early": + out = add(out, value, q) + return out, work, out + if kind == "feedback": + work, out = out, work + work = add(work, value, q) + cut = out + work, out = out, work + return cut, work, out + require(kind in ("deferred", "reread", "erase"), "known program") + out = add(out, work, q, -1) + work = add(work, value, q) + cut = out + out = add(out, work, q) + if kind == "reread": + work = add(work, target_value(x, rank, q), q, -1) + if kind == "erase": + require(not any(initial_work), "erasure control has clean initial work") + work = (0,) * rank + return cut, work, out + + +def gate_case(q, rank): + require(q in (2, 3, 5) and rank in (1, 2), "fixed prime-field domain") + inputs = tuple(product(range(q), repeat=rank + 1)) + states = tuple(product(range(q), repeat=rank)) + outcomes = {name: Counter() for name in ("deferred", "guess", "reread", "feedback", "early")} + mixtures = [Counter() for _ in range(5)] + clean_erasure = Counter() + hidden_log = Counter() + for work, out in product(states, repeat=2): + for x in inputs: + expected = add(out, target_value(x, rank, q), q) + for name, counts in outcomes.items(): + cut, final_work, final_out = execute(name, x, work, out, q) + if name != "early": + wanted_cut = work if name == "feedback" else out + if name in ("deferred", "reread"): + wanted_cut = add(out, work, q, -1) + require(cut == wanted_cut, "no source dependence at deferred cut") + counts[(final_out == expected, final_work == work)] += 1 + for numerator in range(5): + for coin in range(4): + name = "deferred" if coin < numerator else "guess" + _, final_work, final_out = execute(name, x, work, out, q) + mixtures[numerator][(final_out == expected, final_work == work)] += 1 + if not any(work): + _, end_work, end_out = execute("erase", x, work, out, q) + clean_erasure[(end_out == expected, end_work == work)] += 1 + initial_log = (0,) * rank + log = add(initial_log, target_value(x, rank, q), q) + logged_out = add(out, log, q) + visible_work = work + hidden_log[(logged_out == expected, (visible_work, log) == (work, initial_log))] += 1 + return check_gate_counts(q, rank, len(inputs), len(states), outcomes, + mixtures, clean_erasure, hidden_log) + + +def encoded_counts(counts): + return {f"output_{int(a)}_workspace_{int(b)}": n for (a, b), n in sorted(counts.items())} + + +def check_gate_counts(q, rank, input_count, state_count, outcomes, mixtures, erased, log): + total = input_count * state_count**2 + joint = total // q**rank + require(total % q**rank == 0, "integral fibre count") + require(outcomes["deferred"] == {(True, True): joint, (True, False): total - joint}, + "exact-output attaining program") + require(outcomes["guess"] == {(True, True): joint, (False, True): total - joint}, + "exact-restoration attaining program") + for name in ("reread", "feedback", "early"): + require(outcomes[name] == {(True, True): total}, "changed-premise escape: " + name) + require(erased == {(True, True): input_count * state_count}, "noninjective escape") + require(log == {(True, True): joint, (True, False): total - joint}, "complete hidden log debt") + for numerator, counts in enumerate(mixtures): + require(sum(counts.values()) == 4 * total, "four actual coin outcomes") + require(counts[(True, True)] == 4 * joint, "mixture joint boundary") + require(counts[(False, True)] == (4 - numerator) * (total - joint), "output error frontier") + require(counts[(True, False)] == numerator * (total - joint), "workspace error frontier") + require(not counts[(False, False)], "no unnecessary double failure") + require(outcomes["deferred"][(True, True)] * q**(rank + 1) > total, + "attaining program rejects a one-digit stronger bound") + return {"q": q, "rank": rank, "source_dimension": rank + 1, + "dirty_output_input_cases": total, + "programs": {n: encoded_counts(c) for n, c in outcomes.items()}, + "mixtures": [encoded_counts(c) for c in mixtures], + "clean_erasure": encoded_counts(erased), "complete_log": encoded_counts(log)} + + +def matrix_rank(matrix, q): + require(matrix and len(matrix) <= 3, "bounded rank rows") + columns = len(matrix[0]) + require(1 <= columns <= 3 and all(len(row) == columns for row in matrix), "bounded rank columns") + rows = [list(row) for row in matrix] + rank = 0 + for column in range(columns): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column] % q), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + inverse = pow(rows[rank][column] % q, -1, q) + rows[rank] = [v * inverse % q for v in rows[rank]] + for i in range(len(rows)): + if i != rank: + coefficient = rows[i][column] % q + rows[i] = [(a - coefficient * b) % q for a, b in zip(rows[i], rows[rank])] + rank += 1 + return rank + + +def multiply(left, right, q): + require(len(left[0]) == len(right), "product shape") + return tuple(tuple(sum(a * b for a, b in zip(row, column)) % q for column in zip(*right)) + for row in left) + + +def linear_cases(): + histograms = {} + for q in (2, 3): + matrices = tuple((v[:2], v[2:]) for v in product(range(q), repeat=4)) + for matrix in matrices: + images = {tuple(sum(a * b for a, b in zip(row, x)) % q for row in matrix) + for x in product(range(q), repeat=2)} + require(len(images) == q**matrix_rank(matrix, q), "independent image-size rank oracle") + invertible = tuple(a for a in matrices if matrix_rank(a, q) == 2) + counts = Counter() + for suffix in invertible: + for cut in matrices: + residual = multiply(suffix, cut, q) + residual_rank = matrix_rank(residual, q) + require(residual_rank == matrix_rank(cut, q), "invertible suffix preserves cut rank") + for readout in matrices: + demand = multiply(readout, cut, q) + demand_rank = matrix_rank(demand, q) + require(demand_rank <= residual_rank, "deferred target rank versus final debt") + counts[(demand_rank, residual_rank)] += 1 + histograms[str(q)] = {f"target_{a}_debt_{b}": n for (a, b), n in sorted(counts.items())} + return histograms + + +def rejection_controls(): + rejected = 0 + for args in ((0, 2, 2, True), (5, 2, 2, True), (2, 0, 2, True), + (2, 5, 2, True), (2, 2, 0, True), (2, 2, 5, True), (2, 2, 3, False)): + try: + finite_case(*args) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid finite domain accepted") + for q, rank in ((4, 1), (2, 0), (2, 3)): + try: + gate_case(q, rank) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid gate domain accepted") + require(rejected == 10, "all invalid domains rejected") + return rejected + + +def package_hashes(here): + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = here / name + require(path.is_file() and not path.is_symlink(), "regular local package file") + with path.open("rb") as source: + raw = source.read(1024 * 1024 + 1) + require(0 < len(raw) <= 1024 * 1024, "package file byte bound") + hashes[name] = sha256(raw).hexdigest() + return hashes + + +def main(): + require(len(sys.argv) == 1, "no command-line arguments are accepted") + finite = [finite_case(4, 2, 2, True), finite_case(3, 3, 3, True), + finite_case(4, 4, 4, False)] + gates = [gate_case(q, r) for q in (2, 3, 5) for r in (1, 2)] + result = {"claim_type": "scoped_proof_with_finite_corroboration", + "finite_state_domains": finite, "gate_domains": gates, + "linear_rank_histograms": linear_cases(), + "invalid_domain_rejections": rejection_controls(), "no_new_kappa": True} + result["package_sha256"] = package_hashes(Path(__file__).resolve().parent) + print(json.dumps(result, sort_keys=True)) + print("PASS_LAST_READ_RESTORATION_BOUND") + + +if __name__ == "__main__": + main() From 7839e2a5b964312aab6d5f1a6bd720b623fc9003 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 00:52:36 +0000 Subject: [PATCH 2/2] docs(research): specify the linear target in the opening claim --- research/last-read-restoration-bound/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/last-read-restoration-bound/README.md b/research/last-read-restoration-bound/README.md index 017b63f9d4..1b3269ebff 100644 --- a/research/last-read-restoration-bound/README.md +++ b/research/last-read-restoration-bound/README.md @@ -3,7 +3,7 @@ This contribution was produced by Nick Petalas. Apache-2.0. A helper cannot retain an earlier input after its last read, deliver a -nonzero target later, and restore all workspace under the following contract: +nonzero linear target later, and restore all workspace under this contract: the output at the cut contains no earlier-input dependence, the continuation reads no earlier input, and its workspace map is injective and independent of output contents. This includes arbitrary nonlinear workspace computation