Prove sharp migration tariffs for two reusable resources (no new κ)

research/two-resource-migration-tariff/PROOF.md

@@ -0,0 +1,123 @@
+# Exact tariffs for two reusable resources
+
+This is a scoped written proof. The finite verifier corroborates it; it is
+not a formal proof-kernel certificate or a physical implementation theorem.
+
+## Model
+
+There are n>=1 labelled consumers. Consumer i is live on a nonempty half-open
+interval [s_i,t_i), has a fixed nonempty eligibility list L_i contained in
+{0,1}, and pays w_i>=0 each time it moves between the two resources while
+remaining live. Initial placement and release are free. Simultaneously live
+consumers occupy distinct resources. There is no reserved initial or final
+placement. The lists do not change during a lifetime.
+
+Partition time at the distinct endpoints. A schedule gives a legal injection
+on every elementary time interval, including intervals with no live consumers.
+At a boundary its charge is the sum of w_i over consumers present on both
+sides whose resource changes. Atomic exchanges are allowed. This is an
+optimistic transfer model: a physical realization may need extra storage,
+movement, restoration and time. We prove no zero-cost physical migration.
+
+Pointwise Hall feasibility means every active set has an injective eligible
+placement. In this two-resource model this says that at most two consumers
+are live and, when two are live, their lists have union {0,1}. It guarantees a
+schedule when migrations are allowed, since independent legal placements can
+be chosen at every elementary interval.
+
+## Theorem 1: exact weighted optimum and a checkable certificate
+
+For each elementary interval k let S_k be its set of legal placements.
+Pointwise feasibility implies 1<=|S_k|<=2. For consecutive placements a,b set
+
+    c(a,b) = sum_{i live in both, a(i)!=b(i)} w_i.
+
+Then the exact minimum charge is the shortest layered-path cost with every
+initial placement free and every terminal placement accepted. In particular,
+
+    D_0(a) = 0,
+    D_k(b) = min_{a in S_{k-1}} [D_{k-1}(a)+c(a,b)],
+    optimum = min_{b in S_last} D_last(b).
+
+Every schedule is one such path with exactly that charge, and every path is
+an allowed atomic schedule. Induction on the layer proves the recurrence.
+There are at most 2n-1 layers and four arcs per layer boundary. After endpoints
+are sorted, a sweep constructs the states and optimum in O(n) steps. Sorting
+costs O(n log n). These bounds count exact arithmetic operations.
+
+The implementation emits a path and integer potentials p_k(a). A separate
+checker tests the path's cost M, p_0(a)<=0 for every initial state,
+
+    p_k(b)-p_{k-1}(a) <= c(a,b) on every arc,
+    p_last(b) >= M for every terminal state.
+
+Along every competing path these inequalities telescope to charge>=M.
+The supplied path attains M. Thus the checker does not need to repeat the
+minimization. The optimizer's distances satisfy these certificate conditions.
+Integer weights are the executable interface; the mathematical recurrence
+also holds for arbitrary nonnegative real weights with exact comparisons.
+
+Allowing extra changes inside an elementary interval cannot defeat the lower
+bound. Sample the placement once in each interval. A consumer whose sampled
+resources differ across a boundary must move at least once between samples.
+For a fixed consumer these sampling windows are disjoint, and its lifetime
+contains each such window. Nonnegative charges therefore dominate the sampled
+path's charge. The event model already attains its own optimum.
+
+## Theorem 2: the sharp worst-case migration count is max(0,n-2)
+
+Set every weight to one. Every pointwise-feasible instance admits a schedule
+with at most max(0,n-2) migrations. For every n>=1 there is an instance whose
+minimum is exactly this number.
+
+For the upper bound, separate the connected components of the interval
+overlap graph, using positive-length overlap. Isolated consumers cost zero.
+In a component with k>=2 consumers, process starts in time order, with endings
+before starts at the same time. At most two consumers can be live.
+
+Choose the initial placement of the first consumer to accommodate the first
+consumer overlapping it. Such a choice exists by pointwise feasibility, and
+no intervening consumer belongs to that component. If both begin together,
+choose any feasible placement of the pair. This first pair costs no migration.
+
+At every later start there is at most one continuing consumer. If its current
+resource permits the new consumer's placement, do nothing. Otherwise the new
+consumer must have a singleton list equal to that occupied resource. Hall
+feasibility forces the continuing consumer to be eligible for the other
+resource; move it once and start the new consumer. With no continuing consumer,
+the new placement is free. Two simultaneous new starts also need no migration.
+Thus each start after the first pair incurs at most one migration. The component
+cost is at most k-2. Summing components is at most n-2 whenever n>=2 and there
+is a nontrivial component. With only isolated consumers it is zero. This proves
+the stated bound, including n=1.
+
+For sharpness at n>=2, use one flexible consumer on [0,2n-1) with list {0,1}.
+For i=1,...,n-1 put a blocker on [2i-1,2i), whose singleton resource is
+(i-1) modulo 2. Blockers are disjoint and the instance is pointwise feasible.
+During consecutive blockers the long consumer must occupy opposite resources.
+It therefore moves at least n-2 times. It can move once in each intervening
+gap, attaining the bound. At n=1 a single consumer attains zero.
+
+Giving the long consumer weight W yields exact optimum W(n-2), since no
+blocker can move. Consequently pointwise compatibility leaves an unbounded
+additive migration bill even at concurrency two. At n=3 the family is the
+smallest pointwise-feasible instance without a constant-per-lifetime eligible
+assignment. One or two consumers always admit a fixed assignment: assign
+disjoint consumers independently, or use their common feasible placement if
+they overlap.
+
+## Research consequence and limits
+
+Ali Romman's [PR #5781](https://github.com/CrocSwap/integer-mult-bounds/pull/5781)
+explicitly excludes temporal reuse from its static assignment model. The new
+step solves this particular temporal extension and quantifies an obligation
+that a per-time matching relaxation omits. This does not exhibit an error in
+that predecessor, nor was its matcher run to establish this result. Hall's
+theorem and layered shortest paths are classical; the scoped tariff, sharp
+family and independently checked implementation are the contribution here.
+
+The two-resource assumption, fixed lists, free initial/final placement and
+atomic migration contract matter. This is no theorem about arbitrary coupled
+native consumers or three or more resources. No actual helper lifetime export,
+physical transfer word, selected supplier invoice, new kappa, uniform compiler,
+stock/precision/tape proof or complete multiplication theorem is supplied.

research/two-resource-migration-tariff/README.md

@@ -0,0 +1,85 @@
+# Sharp migration tariffs for two reusable resources
+
+Claim type: scoped written proof with finite corroboration. This contribution
+was produced by Nick Petalas. Apache-2.0.
+
+For n>=1 consumers with fixed half-open lifetimes and nonempty fixed lists of
+eligible resources from {0,1}, pointwise Hall feasibility guarantees a schedule
+with at most max(0,n-2) migrations. This bound is sharp for every n. One long
+flexible consumer and alternating resource-fixed short consumers attain it.
+Giving the long consumer transfer price W makes the exact bill W(n-2) at n>=2.
+Thus independent per-time matching can omit arbitrarily large transfer charges.
+Three consumers already give the smallest obstruction to a placement that stays
+fixed throughout each lifetime.
+
+The package also constructs a minimum-cost schedule for arbitrary nonnegative
+integer per-consumer transfer prices. There are at most two assignments per
+elementary interval. A layered shortest path gives the optimum in O(n log n)
+arithmetic operations including endpoint sorting. A path and dual arc potentials
+certify optimality without repeating the optimization. See [PROOF.md](PROOF.md).
+
+This answers the temporal-reuse boundary left outside Ali Romman's
+[PR #5781](https://github.com/CrocSwap/integer-mult-bounds/pull/5781), exact head
+`cb06de3a4f6e2a2c927eb3aa3f9f43a578f73a1f`, specifically its
+`docs/research/compatible-resource-assignment.md` Open next questions. The
+predecessor supplies the question and static interface, and is cited without
+rerunning its matcher. Hall's theorem and layered shortest paths are classical
+inputs. No new general matching algorithm is claimed.
+
+## Evidence and reproduction
+
+From the repository root, run:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-resource-migration-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/two-resource-migration-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-resource-migration-tariff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-resource-migration-tariff --check-source-history
+```
+
+Another CPython 3.12 interpreter path can replace the absolute path. The verifier
+uses only the standard library, writes no files, and emits a generated receipt
+bound to the six package files by SHA-256. It enumerates all labelled lifetimes
+with endpoints in {0,1,2,3,4}, all three nonempty eligibility lists and one to
+three consumers, using both unit and labelled integer prices. Its independent
+oracle enumerates literal assignments on every integer unit cell, including
+cells without an endpoint. Additional checks cover seeded weighted timelines,
+the sharp family through 512 consumers, half-open touching lifetimes, invalid
+inputs and forged optimality certificates. Counts are printed by the verifier.
+
+## Scope and limits
+
+The executable interface accepts 1..512 consumers, integer endpoints in
+0..10^6 and integer migration prices in 0..10^12. The written theorem has no
+consumer bound and depends only on endpoint order; its weighted recurrence also
+allows nonnegative real prices with exact comparisons.
+
+Initial placement and release are free, and migrations are atomic. Fixed
+initial/final owners, changing lists, coupled consumers, physical movement,
+spare storage for exchanges and more than two resources are outside this model.
+No actual caller's ownership schedule has been exported. These are abstract
+transfer costs, not an admitted physical bill. No new kappa, selected-frontier
+change or complete multiplication theorem is claimed. Independent human and
+formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+1. Bind one actual caller's pair of owners, fixed lifetimes and paid transfers
+   to this interface. Start by exporting every live interval and legal transfer
+   including restoration. A physical source adapter and transfer word are absent.
+2. Determine the sharp migration count with three resources and fixed lists.
+   Start with exact small timelines. A separate argument is needed; the two-state
+   bound does not transfer.
+
+Structured relevance, first steps and blockers are in [TASK.json](TASK.json).
+
+## Implementation limits
+
+All production loops are bounded by 512 consumers, 1024 endpoints and two states
+per cell. The independent oracle is bounded by six consumers and nine integer
+time units. Functions remain below 60 lines. Python necessarily allocates dynamic
+objects; the fixed input bounds limit live collections. Runtime allocation and
+ordinary library dispatch are explicit Power of Ten deviations. No recursion,
+dynamic code execution, external programs or inherited source imports are used.
+Warning-strict normal and optimized runs keep the explicit certificate and input
+checks active. The two internal assertions are redundant dimension invariants.

research/two-resource-migration-tariff/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}

research/two-resource-migration-tariff/TASK.json

@@ -0,0 +1,113 @@
+{
+  "schema_version": 1,
+  "task_id": "supplier-boundary-audit",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "supplier-boundary-audit",
+    "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?",
+    "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"
+    ],
+    "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": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.",
+    "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": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.",
+    "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": [
+      "supplier admission",
+      "5717",
+      "5719",
+      "5708",
+      "owned lifetime"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3801: successor scatter-boundary decision package.",
+        "evidence": "research/scatter-boundary-decision/README.md",
+        "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.",
+        "status": "author-checked",
+        "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd",
+        "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": "Exact weighted migration tariffs and sharp max(0,n-2) transfer count for two reusable compatible resources over fixed half-open lifetimes.",
+  "scope_change_reason": "The assigned card concerns supplier admission. This is a self-contained interface side result on the temporal-reuse boundary explicitly excluded by PR5781, rather than an audit or supplier-admission claim.",
+  "bottleneck_link": "Pointwise compatible reuse does not price moves of a continuing helper. The exact temporal relaxation can expose an omitted transfer obligation before physical caller expansion.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved and independently enumerated temporal tariff; do not extend to more resources or physical installation.",
+  "outcome": "completed",
+  "evidence": "PROOF.md supplies the universal argument; verify.py prints PASS_TWO_RESOURCE_MIGRATION_TARIFF with complete finite-oracle counts and generated SHA-256 bindings.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual caller export authenticated fixed lifetimes, eligible owner pairs and nonzero migration tariffs for this two-resource model?",
+      "why_it_matters": "Only source-bound data makes the temporal lower bound relevant to a complete supplier invoice.",
+      "first_step": "Export one pair of physical owners and list every live interval and legal transfer, including restoration.",
+      "blocked_by": "No physical source adapter or transfer word is supplied."
+    },
+    {
+      "question": "What replaces the sharp n-2 migration bound for three reusable resources with fixed lists?",
+      "why_it_matters": "The two-state proof depends on two resources and does not establish a general hosting limit.",
+      "first_step": "Test three resources on small exact lifetimes with fixed lists and count charged persistent changes.",
+      "blocked_by": "A separate combinatorial argument and larger state space are required."
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 5781,
+      "author": "Ali Romman",
+      "head": "cb06de3a4f6e2a2c927eb3aa3f9f43a578f73a1f",
+      "question_source": "docs/research/compatible-resource-assignment.md, Open next questions",
+      "usage": "Question and static-interface context only; no executable dependency or predecessor replay."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19215637",
+  "environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS 27.0.1 arm64",
+    "dependencies": "Python standard library only"
+  },
+  "claim_type": "scoped written proof with finite corroboration"
+}