Prove sharp deferred-delivery restoration/error boundary (no κ)

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.

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 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
+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.

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"
+    }
+  ]
+}