[petalas]

Summary

Prove the exact unit-price optimum for every factor count and scratch cap in PR788's ordered binary, reserved-connector grammar with one reusable clean array. Claim type: scoped written proof with exact finite corroboration. No new kappa.

- PR714: clean-root formula; PR788: equality at 54 unit-price factors
+ arbitrary reuse cannot improve that formula, for every n and admitting cap

For s >= 1 scratch arrays, capacity is n <= 2^s. The minimum is F(1)=1, F(2)=3, and F(n)=6q(n-2q) for n>=3, where q is the power of two with 3q<=n<6q. It is independent of the admitting cap and attained at a clean root with balanced dirty children. The new step is the all-tree reuse lower bound, not the predecessor formula or the known value F(54)=2112.

This contribution was produced by Nick Petalas. Credit Stephen Shore / nightangelflowerwin-ops for PR788's reusable-array grammar and weighted construction, FanPUYen for PR714's root formula, chafreaky / PR628, 0xkilgore / PR663, androolloyd / PR673 and their retained reversible-echo lineage. Convexity and binary-tree induction are classical. No predecessor code or scientific replay is executed as this contribution.

Evidence

Before, the reusable-array package demonstrates a weighted improvement and the 54-factor unit-price equality. After, PROOF.md supplies a lower bound and attainer for every feasible factor count and cap.

Local CPython 3.12.15 on Darwin arm64, standard library only, passes:

• All 1,022 feasible and 1,538 infeasible factor-count/cap pairs through 256 factors and caps 1..10.
• All 32,640 root splits through 256, plus 1,280 large exact-integer identity fixtures near dyadic breakpoints.
• 102 dense coefficient word executions at 34 factor counts, with every source, target and dirty-input column, ordered noncommuting factors and literal inverses; 25,659 forward leaf occurrences enumerated.
• Ten semantic/input controls. Normal and optimized direct receipts agree byte for byte and bind all six package sources by SHA256.
• Both registered commands, timed locally at 0.660 and 0.715 seconds for direct normal and optimized replay, below their separate 60-second limits. These are bounded replay durations, not performance gains.
• Metadata/source pins, in-memory syntax/AST inspection, staged whitespace checks, exact committed bytes/modes and declared source ancestry.
• Official committed export/integrity check and read-only Git-free normal/optimized replay with empty PATH. Export receipts match local receipts and every exported file retains bytes and modes.

From the worktree root:

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

Use another CPython 3.12 executable elsewhere. Expected markers are PASS_ONE_CLEAN_UNIT_OPTIMUM, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES.

Canonical base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, selected PR6030. The current binding-only example passed. The P104 card explicitly changes scope to a recursive helper's clean-storage premise. Main, live claims, local reservations, merged formula/object searches and a complete 627-open-PR body snapshot were checked before commitment. Sparse notes, arbitrary historical diffs and unpublished work remain coverage limits. Advance CLAIM.

Limitations

Unit leaf prices and exactly one supplied clean array are essential. Unequal prices, additional clean arrays, higher arity, nonreserved lifetimes and arbitrary reversible circuits are outside the theorem. Dispatch, provisioning, admission scans, routing, precision, native implementation, hosting, compiler and outer costs remain payable. The result is not a complete signed supplier invoice. All selected framework assumptions remain. PR628 rounded-leaf replay, the selected scientific cold replay, Lean, Docker, independent human and formal proof-kernel review were not run.

Open next questions

• Which unequal-price sequences retain a clean-root optimum? Start with monotone sequences and the ordered weighted recurrence. PR788 already excludes a claim covering all positive price sequences.
• Can an actual native caller supply the clean array cheaply enough? Start with one named lifetime, including initialization, admission and cleanup, and its complete signed invoice. No physical occurrence or positive complete margin is supplied here.

Related open work

• Prove exact distinguished-factor tariffs for dirty echo trees (no κ) #6450 gives a distinguished-factor tariff for static all-dirty echo trees, including higher arity. This theorem changes the storage model to one clean array and optimizes total unit-price binary count; no marked-factor value is recomputed.
• Prove exact source-injection tariffs for completed partial echoes #6411 prices source injections across completed partial echo observations. This proof keeps the parent connector reserved and optimizes a composition tree, rather than that observation contract.
• Use one clean carry for the complete selected P104 scalar layer #6511 supplies a one-bit clean carry for the actual selected scalar layer. Its bit-circuit contract and gate bill are separate from a clean payload array in this abstract product schedule.
• Certify cheaper physical control routes for all selected P104 scalars #6513 prices physical control routes for that scalar layer, retaining its clean carry. This package supplies no tape-route or scalar-layer gate comparison.

Merged #714/#788 are the cited predecessors. Closed #829 studies two clean checkpoints and is a different resource contract.

The completion refresh inspected all 212 open account PRs and the seven other open contributions created since the advance CLAIM: #6676, #6677, #6678, #6680, #6681, #6682 and #6683. None studies this one-clean, unit-price reserved-connector optimum or computes a conflicting value. No additional scientific computation was run to check those contributions.

CI notes

Hosted CI did not certify this result. At head ed0043fa12735b80ff56c53b07d37353bfe4ad55, run 41693024798 was cancelled by the workflow's 10-minute timeout while the repository-wide Onboarding helper tests step was running. The plan job ran from 18:21:31Z to 18:31:33Z on 2026-11-03, before package selection; the package replay was skipped. Run metadata confirms the matching head and cancelled conclusion. This is a CI infrastructure timeout, not a reported package-check failure.

Validation evidence is limited to the local checks listed above: normal and optimized exact checks, both registered replay commands, metadata/source pins, committed bytes/modes/source ancestry, and read-only Git-free export replay. No hosted package pass is claimed. A separate recent run 41693750102 also had its plan cancelled after about ten minutes and skipped replay; its onboarding step was skipped, so the cancellation is not attributed to that step. No commit was pushed and no workflow was rerun to retrigger CI.

Merge Danger

Door: two-way. This adds one isolated research package.

Blast Radius: package. No selected record, shared code or predecessor file changes.