Prove fixed-prefix P104 tails are optimal for every concave tariff

research/p104-prefix-tail-optimum/PROOF.md

@@ -0,0 +1,166 @@
+# Exact optimum with the prefix paths fixed
+
+## 1. Contract and theorem
+
+Use Adam Gall's PR1940 supplied-copy boundary and its exact
+`SCHEDULE.json`. A parent edge `[S,k]` requires a centre-k read at the
+frame spanned by survivor labels in the eight-bit mask S. All survivor
+labels are independent, so inclusion of these frames is inclusion of
+masks and their dimensions are popcounts. These geometric and decoder
+facts are inherited premises, not newly audited here.
+
+Let D_k be the distinct masks assigned to centre k by the parent edges.
+A cover partitions each D_k into nonempty chains under strict inclusion.
+It has 32 chains in total. Each chain carries that one centre's exact
+value, enters at the singleton `{k}`, visits its chain masks, and exits at
+the full frame V of dimension 9. A frame increment of rank r costs f(r),
+and f(0)=0. No centre mixing, redrop, changed target order or changed
+entry/exit contract is allowed. All direct strict inclusion links are
+permitted, not just consecutive links in the published cover.
+
+**Theorem.** For every concave f on integer ranks 0,...,8, the minimum
+delivery-tail cost over these covers is
+
+```text
+85 f(1) + 17 f(2) + 19 f(3) + 20 f(4).
+```
+
+The minimum is attained by PR1940's published cover. Concavity here means
+that f(r)-f(r-1) is nonincreasing. Nondecreasing tariffs are included, but
+that additional restriction is unnecessary for the proof.
+
+The attaining construction and its 32-path count are credited to PR1940
+and Ali Romman's PR1125 respectively. The new assertion is optimality
+over the complete fixed-path chain-assignment class.
+
+## 2. Chain cardinalities and chronology
+
+The per-centre numbers of rank-four masks are
+
+```text
+centre             0  1  2  3  4  5  6  7
+rank-four masks    5  3  4  4  4  3  4  5
+```
+
+The checker enumerates these masks and stores them as antichain witnesses.
+A chain can contain at most one of them. Their counts sum to 32 and the
+published cover attains every count. Therefore every cover with 32 chains
+must have exactly the displayed number c_k at each centre. This is the
+fixed-prefix specialization of the credited rank-four antichain argument.
+
+Each target's successive prefix masks strictly increase in dimension.
+Every strict link in a carrier chain does too. Process equal-frame reads
+together and otherwise order by increasing dimension, breaking ties by
+mask. That respects both target and carrier dependencies. Thus changing
+the chain assignment within this class introduces no chronological cycle.
+The target moves and scalar reads are unchanged by the assignment.
+
+Every chain starts in dimension 1 and ends in dimension 9, hence its
+increment ranks sum to 8. Every cover therefore has rank mass
+32*8=256. This equality is essential for the linear term in section 5.
+
+## 3. A matching formulation with every legal link
+
+Fix a centre, put n=|D_k| and make a left and right vertex for every mask
+u in D_k. Include an edge u_L to v_R exactly when u is a proper subset of
+v. A matching of cardinality n-c_k is precisely a partition into c_k
+chains: a matched edge declares an immediate successor. Each mask has
+at most one predecessor and successor. Strict inclusion forbids cycles.
+Conversely, consecutive pairs in any cover give such a matching.
+
+Write a=|u| and b=|v|. Starting with each node on a separate chain gives
+the constant cost
+
+```text
+B_f = sum_(u in D_k) [f(|u|-1) + f(9-|u|)].
+```
+
+Joining u to v replaces u's exit and v's entry by one direct increment.
+Give the matching edge cost
+
+```text
+w_f(u,v) = f(b-a) - f(9-a) - f(b-1).
+```
+
+Then a cover's price equals B_f plus the sum of its matching-edge costs.
+This includes every entry and exit increment, including zero increments
+at singleton read frames. There is no charge omission at chain endpoints.
+
+Add a source with unit-capacity zero-cost arcs to all left vertices and
+unit-capacity zero-cost arcs from all right vertices to a sink. A matching
+is an integral source/sink flow of the prescribed value n-c_k.
+
+## 4. Exact optimality potentials
+
+For j=1,...,7 use the hinge tariff h_j(r)=min(r,j). Form the residual
+network at the published matching. An unused arc remains forward with
+its original cost; a used arc is reversed and its cost negated. This
+applies to the source/left and right/sink arcs too, not only links.
+
+For every centre and hinge the certificate gives one integer potential
+pi on all 2n+2 vertices. The checker enumerates every residual arc a to b
+and verifies
+
+```text
+cost(a,b) + pi(a) - pi(b) >= 0.
+```
+
+Every residual circulation then has nonnegative cost, since potentials
+telescope. The difference from the published flow to any other feasible
+flow of the same value is a sum of residual circulations. Thus no other
+matching, and hence no other c_k-chain cover, has a lower hinge price.
+This argument requires no trust in an optimization status or numerical
+tolerance. The optional certificate generator only finds the integer
+potentials; acceptance is the direct inequality check.
+
+There are 56 witnesses and 3,752 inequalities. The published cover's
+total hinge minima, including all centres, are
+
+```text
+j               1    2    3    4    5    6    7    8
+minimum       141  197  236  256  256  256  256  256
+```
+
+The j=8 column is the common linear rank mass. The source cover's
+histogram gives those values exactly. No global enumeration of chain
+covers is asserted; the dual inequalities cover every matching through
+the circulation argument.
+
+## 5. All concave tariffs
+
+Put Delta_r=f(r)-f(r-1) and d_j=Delta_j-Delta_(j+1). Discrete concavity
+is exactly d_j>=0 for j=1,...,7. Directly comparing first differences
+gives the identity, for r=0,...,8,
+
+```text
+f(r) = Delta_8*r + sum_(j=1)^7 d_j*min(r,j).
+```
+
+The linear rank sum is the same for every cover. The published cover
+minimizes every hinge separately by section 4. Taking their nonnegative
+linear combination proves the theorem. In particular, the restriction
+of r^s to these integer ranks is concave for every 0<s<1, so the exact
+minimum throughout that entire power interval is
+
+```text
+85 + 17*2^s + 19*3^s + 20*4^s.
+```
+
+No root search, sampled exponent, transcendental approximation or
+unproved extrapolation between tariffs enters this conclusion.
+
+## 6. Consequence and limits
+
+Within PR1940's fixed target prefix paths and 32-chain supplied-copy
+contract, there is no delivery-tail saving from chain reassignment.
+The same conclusion holds after adding the unchanged target-tail and
+scalar-read charges. This closes that bounded optimization route.
+
+Changing the prefix paths, chain count, term basis, copying/restoration
+contract or entry/exit frames changes the optimization problem. Such
+changes require a new complete bill. In particular, exact formation of
+the 24 extra supplied centre copies remains unresolved here, and no
+arbitrary-dirty restoration, native all-column realization, side-correction
+compatibility, physical compiler, precision/tape or analytic recovery
+obligation is discharged. The result is a scoped proof with a finite
+certificate, not a new supplier or complete multiplication theorem.

research/p104-prefix-tail-optimum/README.md

@@ -0,0 +1,115 @@
+# The fixed P104 prefix schedule already has the optimal concave tail
+
+The exact minimum delivery-tail price on the fixed prefix paths of Adam
+Gall's [PR1940](https://github.com/CrocSwap/integer-mult-bounds/pull/1940),
+using 32 monotone fixed-term chains, is
+
+```text
+85 f(1) + 17 f(2) + 19 f(3) + 20 f(4).
+```
+
+This holds for every concave rank tariff on the integer ranks 0 through 8
+with f(0)=0. In particular it holds simultaneously for every f(r)=r^s,
+0<s<1. Reassigning these read frames to different chains cannot improve
+that tail. A cheaper proposal must change another part of the contract.
+
+This is a scoped optimality proof with an exact finite dual certificate.
+The attaining histogram and the 32-chain construction belong to PR1940;
+their optimality on its fixed prefix paths is the new result. This settles
+the fixed-path part of that package's third Open next question. Target read
+orders are frozen. No global optimum over changed read orders is claimed.
+
+## Proof and evidence
+
+[PROOF.md](PROOF.md) reduces each centre's chain assignments to a
+fixed-cardinality bipartite matching. [CERTIFICATE.json](CERTIFICATE.json)
+contains integer potentials for seven hinge tariffs at each of eight
+centres. The verifier checks every residual arc directly, giving **56 dual
+witnesses and 3,752 nonnegative reduced-cost inequalities**. A discrete
+concave function is a nonnegative combination of those hinges plus a
+linear function. All covers have the same rank mass 256, so the duals
+prove the stated minimum for the entire tariff class.
+
+The domain contains all partitions of the 116 distinct centre/read-frame
+nodes from the pinned parent edges into 32 nested fixed-centre chains.
+Each chain enters at its singleton survivor and exits at the full
+nine-dimensional frame. Entry and exit moves are included. The proof
+allows every strict inclusion link, including links absent from the
+published cover. Chronology is preserved by increasing frame dimension.
+The fixed target tails and scalar reads add constants to this optimization.
+
+The exact centre values remain supplied at entry, as in PR1940. Formation
+of the 24 extra copies, arbitrary dirty-state restoration, side corrections,
+native phase/width realization, hosting, precision/tape and all-size
+compilation remain separate obligations. No current supplier invoice,
+new kappa or complete multiplication theorem is claimed. The selected
+frontier and its five assumptions are unchanged.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-prefix-tail-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-prefix-tail-optimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-prefix-tail-optimum --check-source-history
+```
+
+Replace the interpreter path with another CPython 3.12 interpreter when
+needed. Normal and optimized direct replays must print
+`PASS_P104_PREFIX_TAIL_OPTIMUM chains=32 frames=116 duals=56 inequalities=3752 controls=8 all_concave no_new_kappa`.
+The package runner must print `PASS_REGISTERED_RESEARCH_PACKAGE`.
+
+Normal replay is read-only. `--emit-certificate PATH` deterministically
+regenerates the dual certificate. `--emit-receipt PATH` generates the
+hash-bound result receipt after checking the certificate and eight semantic
+rejection controls. No optimization library or floating-point arithmetic
+is used by either path. [RESULT.json](RESULT.json) binds all seven package
+inputs and both live predecessor files by SHA256.
+
+## Source and implementation scope
+
+Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority
+revision 8. The question source is PR1940, head
+`a9b7dfe2809092a9a4c90784d12bb60061e995e8`.
+[SOURCES.json](SOURCES.json) pins the unchanged schedule and README at the
+canonical base. [TASK.json](TASK.json) records the changed scope from the
+current supplier card to this historical supplied-copy interface. The
+selected bindings-only positive control passed; predecessor scientific
+replays were not run or claimed as new work.
+
+Source files are capped at 256 KiB. The problem has eight centres, at most
+20 nodes per centre, at most 42 residual vertices, seven hinges and at most
+440 residual arcs per centre/hinge. The optional generator makes at most
+42 relaxation passes per witness. Acceptance uses explicit exceptions
+under normal and optimized Python. Functions stay below 60 lines; there
+is no recursion, network access or subprocess call.
+
+Power of Ten rule 3 deviation: CPython, JSON, lists, dictionaries and integer
+arithmetic allocate dynamically. This is confined to the bounded input,
+graph and certificate sizes above; file handles close on every exit.
+Verification checks those capacities and all dual inequalities. A larger
+problem requires a new capacity review before changing these limits.
+
+## Open next questions
+
+- Can different target read orders give a cheaper 32-chain supplied-copy
+  tail? Start with one changed parent-edge witness and rebuild all target
+  and delivery moves. The present certificate freezes those parent edges
+  and does not supply a global ordering bound.
+- Can an actual producer form and restore the 24 extra exact copies within
+  a favorable complete bill? Start with one rank-four-ending chain and
+  its arbitrary dirty-input correction. The required physical producer
+  and restoration contract remain missing.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Credit Adam Gall / PR1940
+for the question, prefix schedule, attaining histogram and supplied-copy
+boundary; Ali Romman / PR1125 for the 32-path obstruction; Josie Elliston /
+PR1071 for the pinned fixture; themilkman216 / PR968, DreamingOfClouds /
+PR717, PR446 and PR595, and Joel Pulikkan / GamingPuzzled / PR620 for the
+decoder and geometry lineage. Minimum-cost matching potentials and the
+discrete hinge decomposition are standard methods. The new contribution
+is this source-bound optimum for every concave rank tariff. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.

research/p104-prefix-tail-optimum/RESULT.json

@@ -0,0 +1,58 @@
+{
+  "chain_counts": [
+    5,
+    3,
+    4,
+    4,
+    4,
+    3,
+    4,
+    5
+  ],
+  "chains": 32,
+  "checked_residual_inequalities": 3752,
+  "claim_type": "scoped proof",
+  "controls_rejected": [
+    "duplicate-frame",
+    "omitted-frame",
+    "reversed-chain",
+    "wrong-survivor",
+    "false-optimum",
+    "short-potential",
+    "negative-reduced-cost",
+    "duplicate-hinge"
+  ],
+  "files_sha256": {
+    "CERTIFICATE.json": "ac4e90b370e1f159aa3bd7eab56385bbc4f75b5c7a174264dcc72c3f21b09bee",
+    "PROOF.md": "ff437c743ddf7663443de5b1987639ebe799b7465db95be99e0d149113290c96",
+    "README.md": "3d93982a4e5e18c465cdb7794718d1c5de9af187bccdc15908a77c342dc604f5",
+    "SOURCES.json": "922de1aae81ec26ff5b4a80128e288dce00e2f41c0823d6fe723d2b40ddbc9c1",
+    "TASK.json": "ead087e03d3be17abf50bf1cfd9fa0d8002fb4a258d96ea248155196dbf92edb",
+    "VERIFY.json": "d83c726dd387c8d5ab42fc3d95bc61c1727771c02f757d1f3fdda2e53f020c65",
+    "verify.py": "3d81aeee17dcaef9394fde3e0e0259526676ec2c4873a9dd7ed3875e6aab69ed"
+  },
+  "hinge_duals": 56,
+  "hinge_optima": {
+    "1": 141,
+    "2": 197,
+    "3": 236,
+    "4": 256,
+    "5": 256,
+    "6": 256,
+    "7": 256,
+    "8": 256
+  },
+  "inputs_sha256": {
+    "research/p104-target-order-delivery/README.md": "a21101c6f73fec3b23943c666b43256050f42f236d4ab9ee567ffb9c8354f10a",
+    "research/p104-target-order-delivery/SCHEDULE.json": "ddc8fe8271392bd5b7c795550a7c52b850fc3bb3efbbf43896c55e0ecc080f48"
+  },
+  "optimal_histogram": {
+    "1": 85,
+    "2": 17,
+    "3": 19,
+    "4": 20
+  },
+  "rank_mass": 256,
+  "read_frames": 116,
+  "schema": "p104-prefix-tail-result/v1"
+}

research/p104-prefix-tail-optimum/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/p104-target-order-delivery/README.md",
+      "usage": "input",
+      "git_blob": "582e4c79896884808b895972937eb7a9d597570a",
+      "sha256": "a21101c6f73fec3b23943c666b43256050f42f236d4ab9ee567ffb9c8354f10a"
+    },
+    {
+      "path": "research/p104-target-order-delivery/SCHEDULE.json",
+      "usage": "input",
+      "git_blob": "7d5039302d4cbea2a1650c8a9757016f3f549be8",
+      "sha256": "ddc8fe8271392bd5b7c795550a7c52b850fc3bb3efbbf43896c55e0ecc080f48"
+    }
+  ]
+}