[petalas]

Summary

Scoped mathematical proof with exact finite corroboration. For a uniform source in F_q^d and a rank-r target delivered after its last-read cut,

Pr[correct output AND exact workspace restoration] <= q^(-r)
output error probability + restoration failure probability >= 1-q^(-r)

The contract requires an earlier-input-independent cut output and an injective workspace continuation that does not read outputs or the earlier source. All persistent control/history belongs to the state. Two explicit logical programs and independent mixtures attain every point on the error boundary, on arbitrary incoming dirt and output values. For linear computation over any field, the deferred target rank is at most the final workspace's dependence rank on the earlier input.

exact restoration fixes at most one cut state
correct delivery then confines inputs to one target fibre

This original interface obstruction was produced by Nick Petalas. Elementary injectivity, counting and rank facts are classical. No new kappa or selected-frontier change is claimed. The advance CLAIM predicted this scope; it has not changed.

Evidence

Before: a proposed one-pass deferred helper can leave its restoration mechanism unspecified. After: PROOF.md gives the sharp error boundary and explicit controls showing which changed hypotheses escape it. No predecessor theorem, fixture or count is rechecked as this contribution.

Local Darwin 27.0.0 arm64, CPython 3.12.15, standard library only:

• Complete finite enumeration of 6,649,846 protocol/initial-state cases and 26,245,090 literal input executions on three specified domains.
• Six finite-field gate fixtures cover 81,162 input/dirt/output triples, five four-outcome mixtures each, four changed-premise escapes and complete omitted-log debt.
• All 316,464 2x2 linear matrix triples over F2/F3 pass, with an independent image-cardinality rank oracle. Ten invalid domains reject.
• Warning-strict normal and optimized direct commands pass in 5.00 and 5.11 seconds locally, below their 120-second limits. Generated hash-bound receipts agree. Both registered commands, metadata and whitespace checks pass. No timing improvement is claimed.

From the worktree root, reproduce with the recorded interpreter or another CPython 3.12 executable:

/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 --check-modes

Expected markers: PASS_LAST_READ_RESTORATION_BOUND, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. The standalone verifier writes nothing and binds its generated receipt to all six package files. Exact six-file committed bytes, execute modes and declared-source ancestry pass at 7839e2a5b964312aab6d5f1a6bd720b623fc9003. The official export and input-coverage check pass. Normal and optimized replay from a read-only, Git-free export with empty PATH passes with identical receipts and unchanged bytes/modes on all seven exported files, including the export manifest.

Limitations and unrun obligations

No existing selected P104 schedule is asserted to satisfy this excluded interface. Source rereads, output feedback, early accumulation, noninjective work and explicitly retained history require their own contracts; the theorem excludes none of those alternatives. The random tape and future inputs are independent of the earlier source. Finite replay corroborates the written proof, without proving its universal quantifiers by enumeration.

No physical/native realization, complete paid/target invoice, compiler/ownership/precision/stock/tape/outer admission or complete multiplication theorem is supplied. The selected cold replay, Lean and Docker were unrun. All five selected framework assumptions remain. Independent human and formal proof-kernel review are unclaimed.

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 named late target, implement its feedback map on arbitrary inputs with legal frames and owned lifetimes, then charge its complete signed invoice. The physical interface and favorable bill are missing.

Related open work

No open PR studying this declared last-read restoration/error quantity was found in the complete 431-body open snapshot and the live submission refresh. Sparse notes, arbitrary historical diffs and unpublished work remain coverage limits. Merged PR1203 supplies a different dirty wrapper using both a source and its inverse; merged PR6015 concerns finite-menu exact endpoints; merged PR6134 concerns random query cost versus mean-square error. Those results are context, not the target or replayed premises.

The completion refresh inspected this account's 16 open PRs created since the advance CLAIM, including this PR. None of the fifteen others studies this declared last-read joint-success quantity. No common-instance numerical disagreement was identified, and no extra computation checked another contribution.

• PR6496 is adjacent error-interface work: it bounds deterministic perturbations of a bounded-dirty QQ16 producer. This package bounds joint delivery/restoration probability in an abstract finite-field last-read contract and computes no QQ16 precision quantity.

CI notes

Both hosted checks passed at exact head 7839e2a5b964312aab6d5f1a6bd720b623fc9003 in Registered research packages run 41556104563: plan and replay (research/last-read-restoration-bound). The completed checks were read once with gh pr checks; both report pass and the published head matches.

Hosted CI executes the registered normal/optimized finite checks and source metadata validation. It does not establish independent mathematical or formal proof-kernel acceptance of the universal written proof. All local checks listed above also passed; physical implementation and the five selected framework assumptions retain their stated status.

Merge danger

Door: two-way. Blast radius: package. Six new files in research/last-read-restoration-bound; shared code, frozen sources and selected records are unchanged.