diff --git a/research/one-clean-unit-optimum/PROOF.md b/research/one-clean-unit-optimum/PROOF.md new file mode 100644 index 0000000000..b05fd8defd --- /dev/null +++ b/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. diff --git a/research/one-clean-unit-optimum/README.md b/research/one-clean-unit-optimum/README.md new file mode 100644 index 0000000000..99bba0033d --- /dev/null +++ b/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. diff --git a/research/one-clean-unit-optimum/SOURCES.json b/research/one-clean-unit-optimum/SOURCES.json new file mode 100644 index 0000000000..3f2906af2a --- /dev/null +++ b/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" + } + ] +} diff --git a/research/one-clean-unit-optimum/TASK.json b/research/one-clean-unit-optimum/TASK.json new file mode 100644 index 0000000000..da87f18fc8 --- /dev/null +++ b/research/one-clean-unit-optimum/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "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", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.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": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "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": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "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": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "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": "changed", + "actual_scope": "Prove the exact all-n unit-price optimum with one reusable clean checkpoint in PR788's ordered binary reserved-connector grammar, for every scratch cap.", + "scope_change_reason": "A side result changes the card's producer/storage premise to a supplied clean array. The new question is whether arbitrary reuse improves the known clean-root count, not a source-bound P104 target split.", + "bottleneck_link": "A recursive helper mechanism must price any clean storage assumption. This result rules out unit-leaf-count gains from recycling one supplied clean checkpoint in the stated class; no complete supplier gain follows.", + "budget_minutes": 60, + "stop_rule": "Publish the first all-n optimum or counterexample; do not extend to unequal prices or additional clean arrays.", + "outcome": "completed", + "evidence": "PROOF.md establishes the all-n lower bound and attainer. verify.py checks full clean/dirty recurrences, both root inequalities, large integer identities, all dirty-input columns of emitted words, and ten controls. Its stdout is a generated source-hash-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which unequal-price sequences still have a clean-root optimum?", + "why_it_matters": "PR788 proves a weighted reuse advantage, whereas this theorem settles equal prices.", + "first_step": "Apply the ordered weighted recurrence to monotone price sequences with explicit scratch caps.", + "blocked_by": "No structural criterion is supplied; arbitrary unequal prices already have counterexamples." + }, + { + "question": "Can an actual native caller supply the clean array cheaply enough?", + "why_it_matters": "Clean storage is a paid input contract and leaf counts alone do not improve the complete signed supplier invoice.", + "first_step": "Name one actual source-bound lifetime and price initialization, admission and cleanup against the complete caller.", + "blocked_by": "No physical occurrence or positive complete supplier margin is established here." + } + ] +} diff --git a/research/one-clean-unit-optimum/VERIFY.json b/research/one-clean-unit-optimum/VERIFY.json new file mode 100644 index 0000000000..fa4c6274e9 --- /dev/null +++ b/research/one-clean-unit-optimum/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": 60, + "checks": "Full clean/dirty recurrence, root inequalities, attaining words and inverse basis coefficients, ten controls, generated source-hash-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same complete exact checks with assertions disabled." + } + ] +} diff --git a/research/one-clean-unit-optimum/verify.py b/research/one-clean-unit-optimum/verify.py new file mode 100644 index 0000000000..426ab8a156 --- /dev/null +++ b/research/one-clean-unit-optimum/verify.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +"""Check the all-n one-clean theorem without executing predecessor code. + +Produced by Nick Petalas. Apache-2.0. +""" + +import hashlib +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +LIMIT = 256 +CAP = 10 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def positive_integer(n): + require(type(n) is int and 1 <= n < (1 << 1024), "invalid factor count") + + +def dirty(n): + positive_integer(n) + p = 1 << (n.bit_length() - 1) + return p * (3 * n - 2 * p) + + +def optimum(n): + positive_integer(n) + if n <= 2: + return 2 * n - 1 + q = 1 << ((n // 3).bit_length() - 1) + require(3 * q <= n < 6 * q, "wrong dyadic interval") + return 6 * q * (n - 2 * q) + + +def root_split(n): + require(type(n) is int and 2 <= n <= LIMIT, "invalid emitted size") + if n == 2: + return 1 + q = 1 << ((n // 3).bit_length() - 1) + return min(2 * q, n - 2 * q) + + +def minima(values): + return min(values) if values else None + + +def dynamic_program(): + """Exhaust every split and clean/dirty root, with exact scratch caps.""" + ds = [[None] * (LIMIT + 1) for _ in range(CAP + 1)] + cs = [[None] * (LIMIT + 1) for _ in range(CAP + 1)] + ds[0][1] = 1 + for s in range(1, CAP + 1): + ds[s][1] = cs[s][1] = 1 + for n in range(2, min(LIMIT, 1 << s) + 1): + dv, cv = [], [] + for k in range(1, n): + a, b = ds[s - 1][k], ds[s - 1][n - k] + if a is not None and b is not None: + dv.append(2 * a + 2 * b) + cv.append(2 * a + b) + a, b = cs[s - 1][k], cs[s - 1][n - k] + if s >= 2 and a is not None and b is not None: + cv.append(2 * a + 2 * b) + ds[s][n], cs[s][n] = minima(dv), minima(cv) + return ds, cs + + +def check_recurrences(): + ds, cs = dynamic_program() + admitted, excluded = 0, 0 + for s in range(1, CAP + 1): + for n in range(1, LIMIT + 1): + if n <= 1 << s: + require(ds[s][n] == dirty(n), "all-dirty minimum mismatch") + require(cs[s][n] == optimum(n), "one-clean minimum mismatch") + admitted += 1 + else: + require(ds[s][n] is None and cs[s][n] is None, "capacity leak") + excluded += 1 + splits = 0 + for n in range(2, LIMIT + 1): + for k in range(1, n): + require(2 * dirty(k) + dirty(n - k) >= optimum(n), "clean-root bound") + require(2 * optimum(k) + 2 * optimum(n - k) >= optimum(n), + "dirty-root bound") + splits += 1 + k = root_split(n) + require(2 * dirty(k) + dirty(n - k) == optimum(n), "unattained optimum") + require(max(k, n - k) <= 1 << ((n - 1).bit_length() - 1), + "attainer exceeds minimum scratch cap") + return {"admitted_n_cap_pairs": admitted, "excluded_n_cap_pairs": excluded, + "all_root_splits": splits} + + +def check_large_identities(): + cases = 0 + for h in range(1, 257): + q = 1 << h + for n in (3 * q - 1, 3 * q, 3 * q + 1, 4 * q, 6 * q - 1): + require(optimum(2 * n) == 4 * optimum(n), "scaling identity") + m = n // 2 + require(optimum(n) == 2 * optimum(m) + 2 * optimum(n - m), + "balanced dirty-root identity") + require(optimum(n + 1) - optimum(n) >= optimum(n) - optimum(n - 1), + "convexity identity") + cases += 1 + return cases + + +def emit(n): + """Emit a clean root and balanced dirty children using an explicit stack.""" + require(type(n) is int and 2 <= n <= LIMIT, "invalid emitted size") + s = (n - 1).bit_length() + # Tasks are (first factor, count, source, target, available roles, sign, clean). + stack = [(0, n, 0, 1, tuple(range(2, s + 2)), 1, True)] + word = [] + for _ in range(2 * optimum(n)): + if not stack: + require(len(word) == optimum(n), "wrong emitted call count") + return word, s + 2 + first, size, source, target, pool, sign, clean = stack.pop() + if size == 1: + word.append((first, source, target, sign)) + continue + require(bool(pool), "emitter exhausted scratch") + connector, rest = pool[0], pool[1:] + k = root_split(size) if clean else size // 2 + left = (first, k, source, connector, rest) + right = (first + k, size - k, connector, target, rest) + calls = [(left, 1), (right, 1), (left, -1)] + if not clean: + calls.append((right, -1)) + if sign == -1: + calls = [(task, -direction) for task, direction in reversed(calls)] + stack.extend((*task, direction, False) for task, direction in reversed(calls)) + raise ValueError("emitter exceeded its node bound") + + +def factor(j): + # The two orientations fail to commute, so order errors are observable. + a = j % 3 + 1 + return ((1, a), (0, 1)) if j % 2 == 0 else ((1, 0), (a, 1)) + + +def multiply(a, b): + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(2)) + for j in range(2)) for i in range(2)) + + +def initial_state(roles, clean=True): + width = 2 * roles + state = [[[int(j == 2 * r + i) for j in range(width)] + for i in range(2)] for r in range(roles)] + if clean: + state[2] = [[0] * width for _ in range(2)] + return state + + +def execute(word, roles, clean=True): + require(3 <= roles <= CAP + 2, "invalid register inventory") + state = initial_state(roles, clean) + require(len(word) <= 2 * optimum(LIMIT), "word too long") + for j, source, target, sign in word: + require(0 <= j < LIMIT and 0 <= source < roles and 0 <= target < roles, + "invalid instruction index") + require(source != target and sign in (-1, 1), "invalid instruction alias/sign") + a = factor(j) + original = state[source] + state[target] = [[x + sign * sum(a[i][k] * original[k][col] for k in range(2)) + for col, x in enumerate(state[target][i])] for i in range(2)] + return state + + +def endpoint(word, n, roles, sign=1, clean=True): + state = execute(word, roles, clean) + expected = initial_state(roles, clean) + product = ((1, 0), (0, 1)) + for j in range(n): + product = multiply(factor(j), product) + for i in range(2): + for j in range(2): + expected[1][i][j] += sign * product[i][j] + return state == expected + + +def expect_rejection(function, *args): + try: + function(*args) + except ValueError: + return + raise ValueError("invalid input was accepted") + + +def check_words(): + calls, runs = 0, 0 + sizes = list(range(2, 33)) + [54, 63, 128] + for n in sizes: + word, roles = emit(n) + inverse = [(j, source, target, -sign) + for j, source, target, sign in reversed(word)] + require(endpoint(word, n, roles), "forward endpoint/restoration failure") + require(endpoint(inverse, n, roles, -1), "inverse endpoint/restoration failure") + require(execute(word + inverse, roles) == initial_state(roles), "literal inverse") + calls += len(word) + runs += 3 + word, roles = emit(6) + require(not endpoint(word[:-1], 6, roles), "omitted cleanup escaped") + require(not endpoint(word, 6, roles, clean=False), "dirty clean-slot escaped") + wrong = [(5 - j, source, target, sign) for j, source, target, sign in word] + require(not endpoint(wrong, 6, roles), "factor reversal escaped") + wrong = list(word) + j, source, target, sign = wrong[0] + wrong[0] = (j, source, target, -sign) + require(not endpoint(wrong, 6, roles), "sign corruption escaped") + expect_rejection(execute, [(0, 0, 0, 1)], 4) + for n in (0, -1, True, 1.5, 1 << 1024): + expect_rejection(optimum, n) + return {"factor_counts": sizes, "basis_word_runs": runs, + "forward_calls_enumerated": calls, "controls": 10} + + +def receipt(): + result = {"schema": "one-clean-unit-optimum/1", "claim_type": "scoped proof", + "recurrences": check_recurrences(), + "large_identity_cases": check_large_identities(), "words": check_words(), + "examples": {str(n): optimum(n) for n in (2, 3, 4, 50, 54, 63, 128, 256)}} + result["source_sha256"] = { + name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() + for name in ("verify.py", "PROOF.md", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json")} + return result + + +def main(): + require(len(sys.argv) == 1, "this verifier takes no arguments") + print(json.dumps(receipt(), indent=2, sort_keys=True)) + print("PASS_ONE_CLEAN_UNIT_OPTIMUM") + + +if __name__ == "__main__": + main()