Prove the all-size unit-price one-clean checkpoint optimum (no κ)

research/one-clean-unit-optimum/PROOF.md

@@ -0,0 +1,158 @@
+# One reusable clean checkpoint has no unit-price count advantage
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## Contract and predecessor results
+
+Use Stephen Shore / nightangelflowerwin-ops's ordered binary,
+reserved-connector class from [PR788](https://github.com/CrocSwap/integer-mult-bounds/pull/788).
+There are `s >= 1` scratch arrays, exactly one supplied initially zero and
+the others arbitrary. A connector remains reserved throughout its node's
+invocation. Each child restores its scratch before the next invocation.
+Every signed leaf invocation costs one. Factor order is fixed.
+
+A dirty connector invokes its left and right children twice each. A clean
+connector invokes its left child twice and its right child once. Reserving
+the clean connector leaves only dirty scratch to its children. Reserving
+a dirty connector permits both sequential children to reuse the same clean
+array. These are the predecessor's interface and restoration identities.
+They are premises here, not new identities or newly audited implementations.
+
+Let `D_s(n)` be the minimum with `s` all-dirty arrays. Let `C_s(n)` be the
+minimum with one clean and `s-1` dirty arrays. A leaf costs one. A nonleaf
+obeys the exact class recurrences
+
+```
+D_s(n) = min_(a+b=n) 2 D_(s-1)(a) + 2 D_(s-1)(b),
+C_s(n) = min_(a+b=n) {
+    2 D_(s-1)(a) + D_(s-1)(b),
+    2 C_(s-1)(a) + 2 C_(s-1)(b)    if s >= 2.
+}
+```
+
+The second line is the extra reuse freedom. PR788 supplies its exact
+interval/weighted formulation and a strict weighted improvement. FanPUYen's
+[PR714](https://github.com/CrocSwap/integer-mult-bounds/pull/714) supplies the
+clean-root formula below with balanced dirty children. The new step proves
+that the full reuse freedom cannot improve that formula at unit prices,
+for any `n` or admitting scratch cap.
+
+## The theorem
+
+There is no admissible binary tree when `n > 2^s`. Otherwise
+
+```
+C_s(1) = 1,
+C_s(2) = 3,
+C_s(n) = F(n) = 6q(n-2q)       for n >= 3,
+```
+
+where `q` is the unique power of two with `3q <= n < 6q`.
+The value is independent of `s` throughout the feasible range. A clean
+root with balanced all-dirty children attains it using only
+`ceil(log2(n))` scratch arrays for `n >= 2`.
+
+This is optimality within this binary grammar. It is neither a general
+reversible-program lower bound nor an optimal physical work invoice.
+
+## All-dirty envelope and clean-root lower bound
+
+Write
+
+```
+D(n) = p(3n-2p),        p = 2^floor(log2(n)), n >= 1.
+```
+
+This is the balanced all-dirty leaf count used by the predecessors.
+For completeness, its discrete increment is
+`D(j+1)-D(j) = 3*2^floor(log2(j))`, so `D` is discretely convex.
+Consequently the minimum of `D(a)+D(n-a)` occurs at the two most balanced
+integer arguments. Direct substitution gives
+`D(2m)=4D(m)` and `D(2m+1)=2D(m)+2D(m+1)`.
+Induction in the dirty recurrence proves that every dirty tree costs at
+least `D(n)` and a balanced tree attains it whenever its height fits.
+
+Fix `n >= 3` and its `q`. The affine pieces of the convex function `D`
+give supporting lines valid at every positive integer `x`:
+
+```
+D(x) >= 3q x - 2q^2,
+D(x) >= 6q x - 8q^2.
+```
+
+Their equality intervals are `[q,2q]` and `[2q,4q]`, respectively. Thus
+
+```
+2D(a) + D(b) >= 6q(a+b) - 12q^2 = F(n).
+```
+
+Equality holds for the familiar PR714 interval
+`max(q,n-4q) <= a <= min(2q,n-2q)`. In particular choose
+`a = min(2q,n-2q)` and `b=n-a`. For `3q <= n <= 4q`, the larger child is
+`2q`, half the least power of two admitting `n`. For `4q < n < 6q`, the
+larger child is `n-2q < 4q`, also at most half that admitting power.
+Balanced dirty children therefore fit in `ceil(log2(n))-1` arrays.
+For `n=2`, the two singleton children cost three and fit under one clean
+connector. These facts establish an attaining clean-root tree for every
+feasible `n >= 2`.
+
+## The new reuse inequality
+
+Extend the notation by `F(1)=1` and `F(2)=3`.
+Its first differences are `2,3`, followed by `6q` at every integer
+`3q <= j < 6q`. They never decrease. Hence `F` is discretely convex,
+and for every positive `a+b=n`,
+
+```
+2F(a)+2F(b) >= 2F(floor(n/2))+2F(ceil(n/2)).
+```
+
+For `n >= 4`, the right side equals `F(n)`. To see this without an
+asymptotic argument, linearly interpolate `F` on `[2,infinity)`.
+On `[2,3]` it is `3x-3`, and thereafter its successive pieces are
+`6q(x-2q)` on `[3q,6q]`. All breakpoints are integers and doubling an
+argument multiplies its interpolated value by four. The interpolation
+is affine between the two consecutive integers surrounding `n/2`.
+Therefore its doubled midpoint identity is exactly the displayed equality.
+The remaining cases give `2F(1)+2F(1)=4>F(2)` and
+`2F(1)+2F(2)=8>F(3)`.
+
+It follows for every `a,b >= 1` that
+
+```
+2F(a)+2F(b) >= F(a+b).
+```
+
+Now induct on factor count in the full one-clean recurrence. A clean
+root costs at least `F(n)` by the preceding all-dirty bound. A dirty
+root costs at least `2F(a)+2F(b)`, because each child has fewer factors;
+the reuse inequality bounds that by `F(n)`. The attaining clean-root
+tree proves equality. This includes arbitrarily many opportunities to
+reuse the clean array at successive dirty nodes, not only a single
+root comparison.
+
+Finally, every root-to-leaf path reserves at most `s` distinct connectors.
+Its depth is at most `s`, so a binary tree has at most `2^s` leaves.
+This proves infeasibility above capacity independently of prices.
+
+## Evidence and limits
+
+The verifier exhausts the full clean/dirty recurrence for `n <= 256` and
+caps `1..10`, and checks both root inequalities at every split through
+256. Large exact integer fixtures test scaling, convexity and balanced
+identities near dyadic breakpoints. The written proof, not their finite
+range, establishes the theorem for all positive factor counts.
+
+An independently written iterative emitter and dense coefficient interpreter
+execute attaining words and their literal inverses. Every source, target
+and dirty-input column is tracked under noncommuting two-dimensional
+integer factors. The clean entry is exactly zero. This checks these new
+attaining words; it executes no predecessor code and supplies no new
+rounded leaf or physical interface theorem.
+
+Unequal leaf prices are excluded: PR788 already gives a strict weighted
+gain. Two clean arrays are excluded: Better-Call-Paul's PR829 treats that
+changed resource. Higher arity, nonreserved lifetimes, phase scans,
+dispatch, clean provisioning, routing, precision, native implementation,
+hosting, all-size compilation and outer admission remain outside the
+count optimum. No selected frontier or kappa changes.

research/one-clean-unit-optimum/README.md

@@ -0,0 +1,112 @@
+# Exact unit-price optimum with one reusable clean checkpoint
+
+One reusable clean array never reduces the unit-price signed-leaf count
+beyond a clean root in the ordered binary, reserved-connector class.
+For `s >= 1` scratch arrays and `n <= 2^s` factors, the exact minimum is
+
+```
+F(1)=1, F(2)=3,
+F(n)=6q(n-2q),    3q <= n < 6q, q a power of two, n >= 3.
+```
+
+Above `2^s` factors the class is infeasible. The value is independent of
+the admitting scratch cap. A clean root and balanced dirty children
+attain it using the least possible cap `ceil(log2(n))` for `n >= 2`.
+
+Claim type: scoped written proof with exact finite corroboration. No new
+kappa, physical supplier or complete multiplication theorem is claimed.
+This contribution was produced by Nick Petalas. Independent human and
+formal proof-kernel review are unclaimed.
+
+Stephen Shore / nightangelflowerwin-ops's [PR788](https://github.com/CrocSwap/integer-mult-bounds/pull/788)
+gives the reusable-array grammar, a strict unequal-price improvement and
+the equality at 54 unit-price factors. FanPUYen's
+[PR714](https://github.com/CrocSwap/integer-mult-bounds/pull/714) gives the
+displayed clean-root formula. The new result is its optimality under
+arbitrary clean-array reuse for every factor count and cap. Neither the
+formula nor the numerical value `F(54)=2112` is claimed as new.
+
+[PROOF.md](PROOF.md) proves the root inequalities and the all-tree lower
+bound. [verify.py](verify.py) evaluates the full clean/dirty recurrence
+without importing or running predecessor code. The receipt emitted to
+stdout binds all six package source files by SHA256. It is generated on
+each replay; there is no handwritten receipt.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/one-clean-unit-optimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/one-clean-unit-optimum --check-source-history
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/one-clean-unit-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/one-clean-unit-optimum/verify.py
+```
+
+Each direct run prints a generated JSON receipt and
+`PASS_ONE_CLEAN_UNIT_OPTIMUM`. The registered hook runs both direct modes
+under separate 60-second limits. Direct replay needs only this package;
+Git, network, numerical libraries and predecessor scripts are unnecessary.
+Source metadata uses the exact Git provenance in [SOURCES.json](SOURCES.json).
+Those four predecessor documents are proof provenance, not executable
+inputs. Their original attribution remains unchanged.
+
+The finite checks cover all factor counts through 256 and caps `1..10`,
+every root split through 256, and large integer identities near dyadic
+breakpoints. An iterative emitter checks attaining words at factors
+`2..32,54,63,128`. Dense coefficient execution tracks every arbitrary
+source, target and dirty-input column under noncommuting integer factors,
+including literal inverse restoration. Ten controls cover omitted cleanup,
+a dirty purported clean entry, reversed factor order, a wrong sign,
+aliasing and invalid factor counts. The receipt enumerates the actual
+coverage; finite tests support the written all-n proof.
+
+## Scope and engineering limits
+
+The `p104-side-correction` card changes scope to a recursive helper's clean
+storage assumption. This is a side result about schedule count, not a
+profitable P104 split. The current source-binding first example passed on
+canonical base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8,
+selected PR6030. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19380579)
+records the question and overlap limits. The selected frontier is unchanged.
+
+Unequal prices, two clean arrays, higher arity and nonreserved lifetimes
+are excluded. Dispatch, provisioning, admission scans, routing, precision,
+native implementation, hosting, compiler and outer costs remain payable.
+The PR628 rounded leaves, selected scientific cold replay, Lean and Docker
+were not run. No complete multiplication assumption is discharged.
+
+The new verifier has no recursion. Its tables are bounded by 11 by 257
+entries, its integer input helpers reject values with more than 1024 bits,
+and emitted words are bounded by the 256-factor formula. Python allocates
+managed objects during execution; fixed-allocation compliance is not
+claimed. The control helper's indirect call has only the two explicit
+targets `optimum` and `execute`. All acceptance checks use exceptions and
+remain active under `-O`. Package replay is the available recurring
+diagnostic; warning-as-error execution is registered. No additional Python
+static analyzer was available on PATH.
+
+## Open next questions
+
+- Which unequal-price sequences still have a clean-root optimum? The
+  theorem settles equal prices, while PR788 shows that arbitrary unequal
+  prices can benefit from reuse. Start with monotone price sequences and
+  the predecessor's weighted recurrence. A useful criterion must retain
+  ordered factors and the scratch cap; no such criterion is supplied here.
+- Can a source-bound caller supply the one clean array at a cost that
+  survives its complete signed invoice? Start with one actual lifetime,
+  including initialization, admission and cleanup. No physical occurrence
+  or positive complete supplier margin is established here.
+
+The structured versions are in [TASK.json](TASK.json). Following the first
+proved result, neither question was pursued in this contribution.
+
+## Credit
+
+The new all-n reuse lower bound and its checker were produced by Nick Petalas.
+Credit Stephen Shore / nightangelflowerwin-ops for PR788's grammar and
+weighted construction, FanPUYen for PR714's clean-root formula, Chafik
+Boukhalfa / chafreaky for PR628, 0xkilgore for PR663, androolloyd for PR673,
+and the retained reversible-echo lineage. Better-Call-Paul's PR829 studies
+the separate two-clean resource. Convexity and binary-tree induction are
+classical. No predecessor file or credit line is changed. Apache-2.0.

research/one-clean-unit-optimum/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "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": "research/clean-checkpoint/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "363edd94ac5f3ae381885eb272e7bcc32873dc18",
+      "sha256": "99afa18845fc7686c1a0ebaf376bf475b3773960e76a5dec4295a843c38a7a0a"
+    },
+    {
+      "path": "research/clean-checkpoint/README.md",
+      "usage": "provenance",
+      "git_blob": "5ea5a92dd8547e72d91ee797b024e7da2135304c",
+      "sha256": "51212b539d5992b827eb77708622ad3bcddae25b1c654db0bc473222fee3ac2c"
+    },
+    {
+      "path": "research/reusable-clean-checkpoint/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "17d2fc0761a9453698832232f7c8761f3547cea3",
+      "sha256": "ac24b3753aba8edf9de07bf061846f14237ee6ca233da4df21111a3e47c4ec36"
+    },
+    {
+      "path": "research/reusable-clean-checkpoint/README.md",
+      "usage": "provenance",
+      "git_blob": "48b0e5b281c6f473cfad600ddfc17edb7bbf06e2",
+      "sha256": "4a2eb2754c9f83dba2cee604eb13841f7d79c6bc0714fa2604fe01be6b559580"
+    }
+  ]
+}