Prove the exact paired-color batch frontier and sharp 10/9 penalty

research/paired-color-batch-frontier/PROOF.md

@@ -0,0 +1,125 @@
+# Exact batch/color tradeoff for paired targets
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## Model and theorem
+
+There are `m >= 1` colors and two distinct targets of each color. A grouping
+partitions all `2m` targets into nonempty batches of size at most three.
+Targets can be reordered without restriction in this mathematical model.
+Write `B` for its number of batches and `I` for its number of color incidences:
+each color present in each batch contributes one. Each batch uses the same
+fixed reservoir width. For positive prices `A,C`, its declared bill is
+
+```text
+E = A B + C I.
+```
+
+The exact undominated frontier is
+
+```text
+B_min = ceil(2m/3),
+B_min <= B <= m:     I_min(B) = 2m-B.
+```
+
+In particular, batch count and color incidence cannot both attain their
+separate minima when `m >= 3`: the minima are `B_min` and `m`, and `I=m`
+requires at least `m` batches. The assertion excludes `m=1,2`, when
+`B_min=m` and both minima are attained together.
+
+## Lower bound
+
+Let `u` be the number of colors whose two targets occur in one batch. Each
+of these colors contributes one incidence. Every other color contributes
+two, because it has exactly two targets. Consequently `I=2m-u`.
+
+A capacity-three batch cannot contain two whole color pairs: that would
+require four targets. Thus `u <= B`, giving `I >= 2m-B`. Independently,
+capacity gives `B >= ceil(2m/3)`, and every color occurs somewhere, so
+`I >= m`. If `B>m`, the grouping is dominated by putting each pair in its
+own batch, which has `(B,I)=(m,m)`.
+
+## Attainment at every integer frontier point
+
+Fix `ceil(2m/3) <= B <= m`, and put `s=m-B`. Put a whole pair of each of
+the first `B` colors into its own batch. There are `B` batches of size two.
+The remaining `s` colors have `2s` targets. The capacity condition implies
+
+```text
+2s = 2m-2B <= B.
+```
+
+Place these `2s` targets in `2s` distinct batches, one additional target
+per batch. In particular, the two targets of any remaining color use
+distinct batches. No batch has more than three targets, all targets occur
+exactly once, and exactly `B` colors are unsplit. Thus `I=2m-B`.
+
+Every listed point is undominated: reducing `B` increases the minimum `I`.
+This proves the full frontier, including an explicit construction.
+
+## Exact positive-price optimum
+
+For every grouping, an attaining frontier grouping is at least as cheap.
+On the frontier,
+
+```text
+E(B) = 2m C + (A-C) B.
+```
+
+If `A<C`, its unique optimal pair of statistics is `(m,m)`; each batch is
+one whole pair. If `A>C`, its unique optimal pair is
+`(ceil(2m/3), 2m-ceil(2m/3))`. If `A=C`, every frontier point ties, and
+non-frontier points are more expensive. These conclusions cover arbitrary
+positive real prices; the checker uses exact rational instances.
+
+## Sharp exchange-only consequence
+
+Cinna Davis's CRT.md section 3 uses three reservoir placements and their
+three inverses per batch. Section 4 uses twelve H-bit shuttle exchanges
+per occupied color. Taking these counts as the declared exchange-only
+tariff, fix the same H in every batch and price one H-bit exchange as one
+unit: `A=6`, `C=12`. Additions, preparation, routing and repair are excluded
+from this sub-bill. The optimal exchange bill is `18m`.
+
+Even the best grouping among those using the minimum number of batches
+has bill `24m-6 ceil(2m/3)`. The ratio to the unrestricted optimum satisfies
+
+```text
+(24m-6 ceil(2m/3))/(18m)
+  = 4/3 - ceil(2m/3)/(3m)
+  <= 10/9.
+```
+
+Equality holds exactly when `3` divides `m`. The case `m=3` is explicit:
+write the two targets of color `a` as `a0,a1`, and similarly for `b,c`.
+
+```text
+minimum batches: {a0,a1,c0}, {b0,b1,c1}     B=2, I=4, E=60
+minimum bill:    {a0,a1}, {b0,b1}, {c0,c1}  B=3, I=3, E=54
+```
+
+Repeating this family gives equality for every positive multiple of three.
+Thus minimizing batch count can impose an avoidable penalty of exactly
+`10/9`, even after color occupancy is optimized within that batch count.
+Equivalently, the better grouping removes one tenth of the former exchange
+sub-bill in these examples.
+
+## Application boundary
+
+unpaidmoon's PR #5538 prices occupied colors, but does not optimize the
+joint batch/color statistics. This proof adds that optimization for the
+stated paired-target, capacity-three model. It does not revisit the
+predecessor's color count or production numbers.
+
+The same-width premise matters: shrinking H with the number of targets
+changes the objective. The unrestricted grouping premise also matters:
+actual CRT batches obey tree, control-reservoir, chronology and placement
+rules. Placement can change the position-mod-K colors themselves. This
+proof neither constructs a valid physical regrouping nor asserts that a
+current production layout has this color multiset or capacity. A full
+cost comparison must also retain all other operations and their prices.
+
+No new kappa, native operator, supplier admission, selected-frontier
+change, formal proof-kernel result or complete multiplication theorem
+follows. The ingredients are elementary partition counting; no claim of
+literature priority for general colored packing is made.

research/paired-color-batch-frontier/README.md

@@ -0,0 +1,93 @@
+# Exact paired-color batch frontier
+
+**Scoped written proof with finite corroboration; no new kappa.**
+For two targets of each of `m` colors and capacity-three fixed-width
+batches, the exact frontier is
+
+```text
+ceil(2m/3) <= B <= m,     I_min(B) = 2m-B.
+```
+
+Here `I` counts occupied colors across batches. For bill `A B+C I`, one
+batch per color is optimal when `A<C`; minimum batch count is optimal
+when `A>C`. Every frontier point ties when `A=C`.
+
+At the declared exchange-only prices `A=6,C=12`, minimizing batch count
+can cost a sharp `10/9` times the optimum: three colors cost `60` instead
+of `54`. The better grouping removes 10% of this exchange sub-bill.
+[PROOF.md](PROOF.md) gives the quantified proof and explicit groupings.
+
+This answers a scoped optimization step motivated by unpaidmoon's
+[PR #5538](https://github.com/CrocSwap/integer-mult-bounds/pull/5538),
+first Open next question. Its occupied-color result is cited, not audited
+or replayed. The new point is that minimizing batches and minimizing color
+macros can conflict; both statistics must enter the objective.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/paired-color-batch-frontier/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/paired-color-batch-frontier/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/paired-color-batch-frontier
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/paired-color-batch-frontier --check-source-history
+```
+
+The direct checker emits `PASS_PAIRED_COLOR_BATCH_FRONTIER`. It independently
+enumerates every capacity-three set partition for `1<=m<=5`, constructs every
+frontier point through `m=256`, checks rational positive-price optima against
+the enumerated partitions through `m=5`, checks every ratio equality through
+`m=256`, and rejects fourteen
+malformed inputs. `--receipt /absolute/scratch/path.json` writes generated
+evidence bound to SHA256 hashes of all six package files. No receipt is
+hand-written or required as an input.
+
+Local normal and optimized checks pass 64,098 enumerated partitions,
+11,136 attaining groupings, 245 rational price cases and fourteen rejection
+controls. Both registered commands pass. Hosted CI is reported separately
+in the contribution PR.
+
+The verifier is read-only unless given that output option. The enumeration
+uses an iterative stack with an exact finite node bound, at most ten target
+levels and no recursion. Python's managed allocations are a Power-of-Ten
+deviation: live enumeration state has at most 101 stack entries, with at
+most ten blocks of at most three integers each; constructed instances have
+at most 512 targets. No native build, Lean or Docker run is required.
+
+## Scope and limits
+
+The mathematical result allows unrestricted grouping and holds a common
+reservoir width fixed. Only the six placement and twelve per-color shuttle
+exchanges are priced in the `6B+12I` example. No actual layout is regrouped,
+and no production color multiplicity, legal physical reorder, invariant
+position-mod-K colors, complete tariff or caller is established.
+
+The selected frontier and the five framework assumptions are unchanged.
+Independent human and formal proof-kernel review are unclaimed. Metadata
+and source-history checks authenticate provenance and publication bytes;
+they do not prove the theorem. The finite enumeration corroborates the
+written proof rather than replacing its unbounded quantifiers.
+
+## Open next questions
+
+1. Does a source-bound CRT region admit any nontrivial regrouping with a
+   common reservoir width and stable colors? First identify one legal
+   tree/control/reservoir region and price its movement, restoration,
+   additions and repair. Blocker: this package supplies no such caller.
+2. What is the analogous exact frontier for other capacities or unequal
+   color multiplicities? Start with capacity four and explicit multiplicity
+   vectors. It would improve abstract screening; physical relevance still
+   requires the first question. No larger search is included here.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Credit unpaidmoon #5538 for the occupied-color tariff and its open question;
+Cinna Davis #4100 for the CRT construction and exchange counts; Hiroki
+KUMAZAKI #4174 for the layout; and Ryanson Jonathan #4329 for the guard and
+placement context. Their work is retained unchanged. Exact main-source
+pins are in [SOURCES.json](SOURCES.json); [TASK.json](TASK.json) records the
+changed scope relative to the current `uniform-transfer-audit` card.
+The frontier proof, attaining family and standalone finite checks are new
+in this contribution. No literature-priority claim for colored packing is made.

research/paired-color-batch-frontier/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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"
+    },
+    {
+      "path": "research/crt-occupied-color-macros/README.md",
+      "usage": "provenance",
+      "git_blob": "5131057f5e6bc7190bdccb1e9300ca011a376af9",
+      "sha256": "b6933f4e54aad26a3492aff191a58a96157ad3020c887d1010def025f0b65830"
+    },
+    {
+      "path": "research/crt-occupied-color-macros/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "72e6456316ae99a7b243f322b2ce7a37e1613d3e",
+      "sha256": "afbd47e9e81847cc9c16bd29a1751d6460c4de32d5ecc9de9e94e3d6f3567ad2"
+    },
+    {
+      "path": "research/unconditional-batched-crt/CRT.md",
+      "usage": "provenance",
+      "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6",
+      "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b"
+    }
+  ]
+}

research/paired-color-batch-frontier/TASK.json

@@ -0,0 +1,116 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "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 assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "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": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "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 batch/color-incidence frontier for two targets per color and capacity-three fixed-width batches; arbitrary positive setup/color prices and a sharp 10/9 exchange-only penalty for minimum-batch grouping.",
+  "scope_change_reason": "The current card asks to discharge one selected assumption at its caller. This is instead an elementary grouping theorem motivated by PR5538 Open next question 1. It isolates a missing joint batch/color optimization and supplies no caller-bound assumption discharge.",
+  "bottleneck_link": "Occupied colors price compact CRT macros. A smaller batch count can require more color macros. The theorem gives an exact screening tradeoff under fixed width and unrestricted grouping; actual source-region legality and complete costs remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first exact paired-color tradeoff and its independent finite enumeration; do not extend to other capacities or a physical caller.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the unbounded proof; verify.py independently enumerates capacity-three set partitions through five colors, constructs all frontier points through 256 colors, and checks exact positive-price optima and rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does an actual CRT region permit fixed-width regrouping with stable colors?",
+      "why_it_matters": "Only a legal source-bound regrouping can turn this exchange sub-bill improvement into a physical gain.",
+      "first_step": "Identify one tree/control/reservoir region, retain guard placement, and price movement, additions, restoration and repair.",
+      "blocked_by": "No source-bound caller or production color multiset is supplied here."
+    },
+    {
+      "question": "What is the exact frontier for other capacities or unequal color multiplicities?",
+      "why_it_matters": "It would give broader abstract screening bounds.",
+      "first_step": "Start with capacity four and explicit multiplicity vectors.",
+      "blocked_by": "Physical relevance still requires a legal source-bound region."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+    "priority_revision": 8,
+    "checked_utc": "2026-10-27T12:41:40.081257+00:00"
+  },
+  "predecessors": [
+    {
+      "pr": 5538,
+      "author": "unpaidmoon",
+      "role": "Occupied-color tariff and first open next question; cited only."
+    },
+    {
+      "pr": 4100,
+      "author": "Cinna Davis",
+      "role": "CRT construction and exchange-count model; cited only."
+    },
+    {
+      "pr": 4174,
+      "author": "Hiroki KUMAZAKI",
+      "role": "Layout context; cited only."
+    },
+    {
+      "pr": 4329,
+      "author": "Ryanson Jonathan",
+      "role": "Guard and placement context; cited only."
+    }
+  ]
+}