Skip to content

Prove exact destination-priced dirty-fanout tariffs over local rings - #5163

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
lee-phys:codex/local-ring-row-fanout
Oct 23, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
lee-phys:codex/local-ring-row-fanout

Conversation

@lee-phys

@lee-phys lee-phys commented Oct 23, 2026 •

Copy link
Copy Markdown

For three arbitrary dirty rows over Z/4 with demand (2,1,1), this proves the exact optimum at every positive source price and every positive destination-only ADD price c_ij=c_i. The eight attaining aggregate count vectors are the complete Pareto frontier; each is uniquely optimal for some positive price vector. With source prices (1,9,9) and all ADD prices one the optimum is 6; with (100,1000,1000) it is 106.

The proof extends to any number of rows over any commutative local ring with at least one unit demand, including zero-demand temporary recipients; finiteness is unnecessary. It gives an O(q) price formula and explicit attaining words. The new lower-bound step tracks a necessary unit source insertion: at a nonunit-demand row it requires either another insertion or at least two incoming ADDs. The incoming-row return lemma covers arbitrary interleavings and is deliberately not a per-edge claim.

Locality is essential for this formula. An exact Z/6 counterexample with demand (2,3,1), source prices (10,10,100) and destination prices (100,100,1) has optimum 24, whereas extending the local formula outside its domain gives 32.

Scope: positive stationary coefficient-independent complete abstract gate prices, a preserved disjoint source and exact restoration of every original dirt column. Independently pricing all six directed edges remains open, as do nonzero all-nonunit demand lists and a complete physical caller. This resolves a price family of #5045/#5139's three-row question, not the unrestricted directed-price problem. No new supplier, kappa or selected-frontier change.

Evidence and reproduction

Only five files under research/local-ring-row-fanout/ are added.

  • Six local rings, including the eight-element non-chain square-zero ring: 2,011 demand-list instances, 6,033 price instances and 25,179 candidate words; 213,744 formal-column forward/inverse executions and 6,688 literal forward/inverse executions.
  • Sixteen separately implemented packed-state bidirectional Dijkstra queries over unrestricted three-row Z/4 words, settling 154,814 entries in total. All nonzero coefficients and six directed edges are available, without depth cutoff or formula-based pruning. Frontier bounds certify each shortest path; the literal interpreter independently replays its endpoint and price. This is not enumeration of the entire state graph.
  • Fifteen built-in controls and three rejected disposable optimized-script mutations: missing unit-arrival charge, missing dirt preparation, and incorrect oracle prices.
  • Registered isolated warning-strict normal/optimized replay, metadata/pins, committed-byte preflight and official export integrity pass. Read-only Git-free normal/optimized export replay passes with identical output and all six exported files unchanged.
python3.12 -B scripts/research_package.py --package research/local-ring-row-fanout --check-only
python3.12 -B scripts/research_package.py --package research/local-ring-row-fanout
python3.12 -B scripts/check_research_commit.py --package research/local-ring-row-fanout

The universal claims rest on the written proof; finite checks corroborate bounded cases. Independent human and proof-kernel acceptance are unclaimed. Optional full source-history ancestry checking was not run in the shallow checkout. Lean, Docker, selected supplier replay and physical caller admission were outside this algebraic contribution and were not run.

Task, overlap and attribution

Explicit donor continuation; the historical bit-helper-contract card is marked changed with its complete original object preserved. Scientific base is canonical main a5df48c55ea806d7952b65acc9c76d878ff09b13, priority revision 7, fetched unchanged before submission. Exact contribution head: cdd7714c20352f7106f005066c3ed65534e98516.

Canonical claim. Entry pagination covered 312 open PRs at 11:04 UTC and 4,318 Discussion records at 11:06 UTC on 2026-10-23. Submission checks refreshed targeted all-state fanout/three-row/nonunit PR searches and live #5030 plus the latest ten #1166 handoffs; no resolving successor was found in that coverage. Sparse historical notes, arbitrary diffs and unpublished work were not exhaustively searched.

Prepared by lee-phys with substantial OpenAI Codex assistance in derivation, implementation, checking and writing; no subagents or independent reviewers. Credit Krzysztof Wójt #5045 for the source-count method and two-row repeated/mixing words; Nick Petalas #4916 for the ring-valued contract; Ross Richardson #3063/#3121 for destination/edge tariffs and dirt restoration; Cinna Davis #1944/#1968, Anthony #774, Oscar Fennell #759, Tekalign #3130 and the retained lineage. Exact #4916/#5045 sources are provenance-pinned at main. Pending #5139 motivates the question but is not a proof or runtime dependency. Apache-2.0.

README/TASK give concrete next steps for independent edge prices, all-nonunit demands and a physical caller.

Merge Danger

Door: two-way. Blast radius: isolated. Five new package files.

Hosted CI

Both hosted checks passed at exact contribution head cdd7714c20352f7106f005066c3ed65534e98516 in Registered research packages run 39945882387: planning in 4m37s and focused package replay in 1m25s. Run metadata confirms conclusion success and the exact head. The replay runs both registered normal and optimized commands. Execution success is separate from independent acceptance of the universal written proof.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants