Prove exact weighted pending-capacity fanout tariffs (no κ)

research/weighted-pending-fanout/PROOF.md

@@ -0,0 +1,201 @@
+# Exact weighted pending-capacity tariff
+
+This scoped written proof was produced by Nick Petalas. Apache-2.0.
+
+## Contract
+
+Retain Sagar Thakrar's PR1168 common-source fanout alphabet. Arrays
+`x,z,y_1,...,y_k` start arbitrarily and are distinct. Exact characteristic-zero
+linear maps `B,A_1,...,A_k` need not commute. A fixed word must universally
+realize
+
+```text
+x unchanged, z unchanged, y_i += A_i B x for every i.
+```
+
+The only paid root queries, with `s` equal to `+1` or `-1`, are
+
+```text
+B^s:   z += s B x
+A_i^s: y_i += s A_i z.
+```
+
+Each is a complete source-preserving, spectator-preserving, private-work
+restoring, head-returning query. Their implementations and complete prices
+are premises. Inverse queries have the same positive fixed price as forward
+queries. There is no direct product query, combined output query, free copy,
+output-to-output query, changing source, frame change or overwritten helper.
+Universality over the admissible maps is essential to the lower bound.
+Special zero maps or relations among maps can admit shorter words.
+
+An output is unfinished from its first readout query until its permanent
+commit. Commit requires the correct all-input value. No later query may
+touch it. Unstarted and committed outputs do not count toward the pending
+capacity; they remain reserved arrays and are not reusable child scratch.
+
+The new hypothesis is that output i has positive integer reservation weight
+`w_i`, and at every query boundary
+
+```text
+sum_(i unfinished) w_i <= C,
+```
+
+where C is a positive integer. A commit can occur at a complete-query return.
+Weights are declared lifetime reservations. Unequal physical payload widths
+or a memory-saving theorem do not follow from this abstract contract.
+
+## Theorem
+
+Let `b(w,C)` be the smallest number of bins partitioning the outputs, with
+total weight at most C in each bin; put `b(empty,C)=0`. If every `w_i<=C`,
+the coordinatewise simultaneous minimum query counts are
+
+```text
+N_Ai = 2 for every i,
+N_B  = 2 ceil(b(w,C)/2).
+```
+
+Consequently every positive fixed sign-symmetric complete query price gives
+
+```text
+Q_min = 2 sum_i c_Ai + 2 ceil(b(w,C)/2) c_B.
+```
+
+If an output has `w_i>C`, no universally correct word exists: it cannot even
+be opened. The empty problem has the empty optimum. The theorem is uncapped;
+the reference implementation deliberately accepts at most ten outputs.
+
+## Lower bound for arbitrary words
+
+Use Ross Richardson's PR938 coefficient state, as retained by PR1168:
+
+```text
+z   = z_initial + q B x,
+y_i = y_i_initial + e_i A_i z_initial + f_i A_i B x.
+```
+
+Initially `q=e_i=f_i=0`. A signed B query changes q by s. A signed A_i query
+changes `(e_i,f_i)` by `(s,s*q)`. Universal correctness implies final
+`q=0,e_i=0,f_i=1`. Necessity already follows by specializing all maps to the
+scalar identity and varying initial x and z independently. These coefficient
+facts and summation by parts are credited premises, not new audit claims.
+
+Since each readout changes e_i by a unit, and f_i must change, at least two
+readouts of each output are necessary. Since q starts and ends at zero,
+the number of B queries is even.
+
+The discrete product rule gives, for each output,
+
+```text
+1 = f_i(final) = - sum_(B queries) e_i(before query) * delta(q).
+```
+
+Indeed, an A_i query contributes `q delta(e_i)` both to `delta(e_i q)` and
+to `delta(f_i)`, while a B query contributes `e_i delta(q)` only to the
+former. The endpoint product is zero. Thus every output has nonzero e_i
+immediately before at least one B query. Such an output is unfinished:
+before its first readout e_i is zero, and a correct permanent commit has
+e_i zero with no later changes.
+
+Assign each output to one such B query, for example the earliest one. The
+outputs assigned to a single event are a subset of its unfinished outputs,
+so their total weight is at most C. Nonempty assigned sets partition all
+outputs into at most N_B feasible bins. Hence `b(w,C)<=N_B`. Combining this
+with evenness gives the stated B lower bound. This argument permits extra
+readouts, arbitrary integer excursions of q and e_i, overlapping lifetimes,
+idle intervals and any commit order. It does not assume the emitted word.
+
+## Attainment
+
+Choose any optimal bin partition `G_0,...,G_(b-1)`. Start with q=0 and, for
+bin j, set `s=(-1)^j` and emit
+
+```text
+for i in G_j: A_i^(-s)
+B^s
+for i in G_j: A_i^s; commit i
+```
+
+Let z_before be the connector immediately before the B query. Output i
+receives exactly
+
+```text
+-s A_i z_before + s A_i(z_before+s Bx) = A_i Bx.
+```
+
+Only that bin's outputs are unfinished during this block. Every one commits
+before the next bin opens. The capacity is legal, all readout counts equal
+two, and q alternates between zero and one. If b is odd, append one B^(-1)
+after all commits. Otherwise nothing is appended. The connector returns
+exactly and the B count is `b+(b mod 2)`. This attains every lower bound
+simultaneously, and therefore every declared positive complete price.
+
+## A strict obstruction to total-weight pricing
+
+Take `w=(3,3,3,3,3,1)` and `C=5`. The five weight-three outputs must occupy
+different bins, and the weight-one output can join any one. Therefore b=5
+and exactly six B calls are needed, together with twelve readouts. The
+total-weight relaxation gives only four B calls, since total weight is 16
+and `2 ceil(ceil(16/5)/2)=4`.
+
+For declared complete prices `c_B=52` and `c_Ai=1`, the correct optimum is
+324, whereas that relaxation prices only 220. These are abstract query
+prices. They are not the physical primitive prices of a selected supplier.
+The new result is the exact packing obstruction and its matching scheduler.
+No optimality claim is made over larger query alphabets.
+
+## Algorithms and finite evidence
+
+The subset dynamic program stores `d[mask]`, the minimum bins covering that
+mask. The bin containing its least item is some feasible submask S containing
+that item; remove S and use `1+d[mask xor S]`. Enumerating all such S is exact
+and reconstructs an attaining partition. There are O(3^k) arithmetic checks
+and O(2^k) table entries. This is exponential in output count, not a claimed
+polynomial optimization algorithm.
+
+An independent oracle successively puts each weight into every feasible
+existing bin or a new bin and keeps all distinct sorted load tuples. Labels
+of bins can be forgotten because all later feasibility decisions depend
+only on loads. This enumerates every feasible packing up to identical loads.
+The two methods agree on the fixed multiset domain recorded in the receipt.
+
+Every emitted schedule in that domain is also executed by ordinary integer
+matrix arithmetic on all basis columns of every arbitrary initial row.
+Each A_i and B is a literal two-by-two matrix; a checked pair does not
+commute. The interpreter checks every commit, every pending-weight boundary,
+both unchanged source rows and all outputs. It does not use the coefficient
+state to compute its endpoint.
+
+A separate breadth-first word search checks four weighted three-output
+contracts. It considers both signed B queries and every legal signed readout,
+without a packing bound, proposed tariff or restrictions on extra readouts.
+It searches increasing unit-query lengths through ten. Complete shortest
+layers and total distinct state counts appear in the generated receipt.
+
+Two exact quotients keep that search finite without discarding a better
+word. Simultaneously negating q and every e_i, while preserving f_i, is a
+sign symmetry of its queries and endpoint. Also, an output reaching
+`(e_i,f_i)=(0,1)` can commit immediately: delete all its later readouts from
+any successful continuation. Other outputs and the connector do not read
+it, its own correct final value remains correct, and reserved pending
+capacity only decreases. Thus an optimum exists with these greedy commits.
+This proves the search covers a shortest word, even though it does not count
+all words or all commit annotations.
+
+## Remaining obligations
+
+Predecessor private-work, coefficient preparation and fixed-tape routines
+are cited contracts, not executed or admitted here. If I denotes admission,
+P denotes reusable preparation and D denotes schedule construction, control
+and program access not already included in complete query prices, the full
+declared bill is `I+P+D+Q_min`. Packing computation belongs in D when needed;
+an optimal packing is not a free runtime oracle.
+
+This result supplies neither a physical reservation assignment nor an
+actual selected producer/consumer. Nonlinear operations, finite-field
+torsion, free output mixing, state-dependent prices, release of output
+storage, coefficient traffic, native frames, precision, owned erasure,
+stock, compiler closure and outer transfer need separate contracts. All five
+selected framework assumptions remain. No kappa, selected-frontier update
+or complete multiplication theorem follows. Independent human and formal
+proof-kernel review are unclaimed.

research/weighted-pending-fanout/README.md

@@ -0,0 +1,164 @@
+# Exact dirty-fanout tariff under weighted pending capacity
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof and constructive scheduler with exact finite
+corroboration. If unfinished output i reserves positive integer weight w_i
+under capacity C, let b be the minimum bin count for those weights. In the
+signed common-source query alphabet with permanent commits, the exact bill is
+
+```text
+N_Ai = 2 for every output,
+N_B  = 2 ceil(b/2),
+Q_min = 2 sum_i c_Ai + 2 ceil(b/2) c_B.
+```
+
+The new step replaces Sagar Thakrar's [PR1168](https://github.com/CrocSwap/integer-mult-bounds/pull/1168)
+cardinality cap by unequal lifetime reservations. The proof covers arbitrary
+longer words and gives an attaining schedule. The unweighted formula is a
+cited predecessor result. No predecessor executable is imported or replayed.
+
+For weights `(3,3,3,3,3,1)` and capacity 5, the five large outputs require
+different bins. Exactly six shared-source calls and twelve readouts are
+necessary and sufficient. Pricing capacity by total weight alone permits
+four shared-source calls. At declared complete prices `c_B=52,c_Ai=1`, that
+relaxation gives 220 while the exact optimum is 324. These are abstract query
+prices, not physical primitive counts or a runtime benchmark.
+
+## Contract and construction
+
+Arrays x,z,y_i are initially arbitrary. The only queries are
+`z += s Bx` and `y_i += s A_i z`, where s is +1 or -1. Every query preserves
+its source, spectators and private work and returns its heads. The fixed
+word must work universally for characteristic-zero linear maps A_i,B and
+all initial arrays, with endpoint `y_i += A_i Bx`, x,z unchanged. Commutation
+and invertibility of the maps are not required. Special relations or zero
+maps can change the optimum for a particular instance.
+
+An output is unfinished from its first readout until a correct permanent
+commit. No later query touches it. The sum of unfinished weights may never
+exceed C. Storage of unstarted and committed outputs is retained, not freed
+as scratch. Weights declare a scheduling resource; the theorem does not
+identify them with physical memory or unequal payload widths.
+
+Partition outputs into optimal feasible bins. For consecutive bins alternate
+s=+1,-1 and emit
+
+```text
+for i in bin: readout_i(-s)
+shared_source(s)
+for i in bin: readout_i(s); commit i
+```
+
+If the bin count is odd, append one inverse shared-source query. Each bin
+finishes before the next opens. [PROOF.md](PROOF.md) proves that every output
+must be active at some shared-source query; assigning it to such an event
+gives a feasible bin packing. Restoration forces an even query count.
+
+## Reproduce
+
+From the repository root, with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/weighted-pending-fanout/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/weighted-pending-fanout/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/weighted-pending-fanout
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/weighted-pending-fanout --check-source-history
+```
+
+Another CPython 3.12 path can replace the local interpreter. Direct replay
+prints `PASS_WEIGHTED_PENDING_FANOUT` in a generated JSON receipt binding all
+six package files by SHA256. It writes nothing and needs neither Git nor a
+predecessor package. The source manifest pins the retained README and notice
+as historical provenance, not live executable inputs. No receipt is handwritten.
+
+The fixed finite domain contains all weight multisets of length zero through
+six with weights in 1..C, at C=1..6. Its 1,715 contracts compare subset dynamic
+programming with independent enumeration of feasible bin-load states. Every
+emitted schedule is executed on all basis columns of every arbitrary initial
+array by literal two-by-two integer maps. A checked pair is noncommuting.
+The executor checks all commits and capacity boundaries, source and connector
+restoration, and every target. It executes 24,126 complete queries in this
+domain; 144 contracts strictly exceed the total-weight bound rounded up to
+an even integer.
+
+Four separate breadth-first searches over signed query words have minima
+10,8,8,8 for weights `(2,2,2)`, `(1,2,2)`, `(1,1,2)`, `(1,2,3)`, all at
+capacity 3. The searches visit 11,416, 36,719, 54,041 and 20,093 distinct
+states, respectively, including all layers through the shortest endpoint.
+They use neither the packing optimizer nor its proposed price to prune
+words. The proof justifies sign symmetry and immediate correct commits.
+Eighteen rejecting controls cover invalid resource domains, incomplete or
+overweight bins, a missing restore, premature/late output access, a changed
+source-query sign and an invalid instruction. A ten-output maximum-capacity
+fixture exercises the implementation's boundary. The universal theorem
+rests on the written argument, not these finite checks.
+
+## Limits and implementation constraints
+
+This reference accepts at most ten outputs and integer capacity at most
+65,536. The optimal packing computation is exponential in output count,
+using O(3^k) arithmetic checks and O(2^k) table entries. An implementation
+must pay packing preparation or supply a separately justified packing.
+Admission, reusable coefficient preparation, schedule/control storage and
+access add to the complete query bill; they are not set to zero here.
+
+There is no recursion, subprocess, network, dynamic evaluation or verifier
+write path. Functions fit within 60 physical lines. Packing has at most
+1,024 table entries; independent load enumeration has at most 203 states;
+word search has depth at most ten and at most 100,000 distinct stored states.
+The literal executor has at most 24 basis columns and 44 instructions.
+Six file reads are capped at 256 KiB each. Explicit exception checks remain
+active under `-O`. Normal and optimized warning-strict commands are registered.
+
+Power of Ten rule 3 has a managed-runtime deviation: Python integers, tuples,
+sets and matrices allocate dynamically. The enforced dimensions and search
+bounds limit live data; runtime allocator overhead is not instrumented.
+Rule 9 has a bounded control-callback deviation: eighteen immediately executed
+rejection callbacks call only packing, emit or literal. They retain no state.
+AST compilation and warning-strict execution supply local diagnostics. No
+separate lint/type analyzer or fixed-allocation native runtime is claimed.
+
+No selected producer/consumer or physical reservation assignment is supplied.
+Nonlinear maps, finite-characteristic torsion, free output mixing, changing
+sources, state-dependent tariffs, output-storage reuse and adaptive data-based
+words are outside the theorem. Native frames, precision/tapes, owned erasure,
+stock, compiler closure and outer transfer remain separate obligations. All
+five selected assumptions remain. No kappa, selected-frontier update, complete
+multiplication theorem, independent human review or proof-kernel acceptance
+is claimed. Selected cold replay, native suites, Lean and Docker are unrun.
+
+## Credit and scope
+
+Sagar Thakrar / PR1168 at `b53b07b5aed4e00358a0d0061ad99dbf5190ca2b` supplies
+the unfinished-output and permanent-commit interface and its unweighted
+all-word lower bound. Ross Richardson / PR938 supplies the coefficient state
+and equality-word context. CubeJerry / PR889 supplies shared dirty-source
+fanout and complete accounting; Chafik Boukhalfa / PR628 supplies the retained
+commutator lineage. The selected native/compiler contributors retain their
+existing attribution. Classical bin packing, dynamic programming, summation
+by parts and linearity are background; global literature priority is unclaimed.
+
+Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8.
+[TASK.json](TASK.json) explicitly changes the uniform-transfer-audit card to
+this recursive-interface side theorem. It does not discharge a selected
+assumption. Selected-baseline orientation passed and is source binding only.
+Discovery stopped at this first verified result.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375366)
+followed live handoffs, active Discussions, open/account PRs, local reservations
+and main/merged searches for weighted pending capacity, bin packing and general
+fanout formulas. Sparse cached notes and unpublished work remain coverage
+limits. No absence of overlap is claimed as a novelty certificate.
+
+## Open next questions
+
+- Bind one actual common-source caller to proved reservation weights and a
+  favorable full invoice. Start with its exact lifetimes and include query
+  implementation, packing, control, restoration and movement. No such caller
+  or physical reservation assignment is supplied.
+- Find a useful caller weight family with an exact cheaper packing algorithm.
+  Start with a source-bound restriction on its weights; the present general
+  reference is exponential and schedule preparation must be paid.
+
+Structured relevance, first steps and blockers are in [TASK.json](TASK.json).

research/weighted-pending-fanout/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": "research/bounded-pending-fanout-seed53/README.md",
+      "usage": "provenance",
+      "git_blob": "636098ae1b909c013c35515d4f9049c732b0e363",
+      "sha256": "0f71af68bf84ace97ee6e9543c9ac22390546c6713e0f2360f3e49383fd2b49f"
+    },
+    {
+      "path": "research/bounded-pending-fanout-seed53/NOTICE.md",
+      "usage": "provenance",
+      "git_blob": "64d83fbb3cb27a361c77763cac4eea8df24e0a43",
+      "sha256": "6b55ed6abad13b2be3ede9373e1503a88238afa8b41cf3ab7e8e4f551863cad4"
+    }
+  ]
+}