From 2235b3c6008da352f0a8c0f778d26d27dc2455f8 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 12:42:17 +0000 Subject: [PATCH] docs(research): prove the paired-color batch frontier --- research/paired-color-batch-frontier/PROOF.md | 125 +++++++++++ .../paired-color-batch-frontier/README.md | 93 +++++++++ .../paired-color-batch-frontier/SOURCES.json | 36 ++++ .../paired-color-batch-frontier/TASK.json | 116 +++++++++++ .../paired-color-batch-frontier/VERIFY.json | 34 +++ .../paired-color-batch-frontier/verify.py | 196 ++++++++++++++++++ 6 files changed, 600 insertions(+) create mode 100644 research/paired-color-batch-frontier/PROOF.md create mode 100644 research/paired-color-batch-frontier/README.md create mode 100644 research/paired-color-batch-frontier/SOURCES.json create mode 100644 research/paired-color-batch-frontier/TASK.json create mode 100644 research/paired-color-batch-frontier/VERIFY.json create mode 100644 research/paired-color-batch-frontier/verify.py diff --git a/research/paired-color-batch-frontier/PROOF.md b/research/paired-color-batch-frontier/PROOF.md new file mode 100644 index 0000000000..5bf637099a --- /dev/null +++ b/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 `AC`, 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. diff --git a/research/paired-color-batch-frontier/README.md b/research/paired-color-batch-frontier/README.md new file mode 100644 index 0000000000..aebdf9c2c1 --- /dev/null +++ b/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 `AC`. 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. diff --git a/research/paired-color-batch-frontier/SOURCES.json b/research/paired-color-batch-frontier/SOURCES.json new file mode 100644 index 0000000000..fe9b211d61 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/paired-color-batch-frontier/TASK.json b/research/paired-color-batch-frontier/TASK.json new file mode 100644 index 0000000000..1b97597fea --- /dev/null +++ b/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." + } + ] +} diff --git a/research/paired-color-batch-frontier/VERIFY.json b/research/paired-color-batch-frontier/VERIFY.json new file mode 100644 index 0000000000..bc6c906fc6 --- /dev/null +++ b/research/paired-color-batch-frontier/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete capacity-three set partitions through five colors; attaining constructions through 256; exact positive-price optima, sharp 10/9 equality, fourteen rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete scientific checks with optimized Python; validation does not depend on assertions." + } + ] +} diff --git a/research/paired-color-batch-frontier/verify.py b/research/paired-color-batch-frontier/verify.py new file mode 100644 index 0000000000..488d98ad89 --- /dev/null +++ b/research/paired-color-batch-frontier/verify.py @@ -0,0 +1,196 @@ +#!/usr/bin/env python3 +"""Exact paired-color grouping checks; produced by Nick Petalas, Apache-2.0.""" + +import argparse +from fractions import Fraction +import hashlib +import json +from math import comb +from pathlib import Path +import sys + + +MAX_COLORS = 256 +PACKAGE_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py", +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def integer(value, low, high): + require(type(value) is int and low <= value <= high, "integer out of domain") + + +def first_batch_count(colors): + integer(colors, 1, MAX_COLORS) + return (2 * colors + 2) // 3 + + +def grouping(colors, batches): + integer(colors, 1, MAX_COLORS) + integer(batches, first_batch_count(colors), colors) + result = [[2 * color, 2 * color + 1] for color in range(batches)] + for index in range(colors - batches): + color = batches + index + result[2 * index].append(2 * color) + result[2 * index + 1].append(2 * color + 1) + return result + + +def inventory(colors, groups): + integer(colors, 1, MAX_COLORS) + require(isinstance(groups, (list, tuple)), "groups must be a sequence") + require(1 <= len(groups) <= 2 * colors, "invalid batch count") + entries = [] + incidences = 0 + for batch in groups: + require(isinstance(batch, (list, tuple)) and 1 <= len(batch) <= 3, + "batch capacity or emptiness") + for target in batch: + integer(target, 0, 2 * colors - 1) + entries.append(target) + incidences += len({target // 2 for target in batch}) + require(sorted(entries) == list(range(2 * colors)), "targets not a partition") + return len(groups), incidences + + +def partitions(targets): + """Canonical set partitions with block size at most three; no recursion.""" + integer(targets, 1, 10) + counts = [1] + [0] * targets + for size in range(1, targets + 1): + counts[size] = counts[size - 1] + if size >= 2: + counts[size] += (size - 1) * counts[size - 2] + if size >= 3: + counts[size] += comb(size - 1, 2) * counts[size - 3] + stack = [(0, ())] + # At depth k there are exactly counts[k] canonical partial partitions. + for _ in range(sum(counts)): + require(bool(stack), "enumeration ended before its exact node bound") + target, blocks = stack.pop() + if target == targets: + yield blocks + continue + stack.append((target + 1, blocks + ((target,),))) + for index in range(len(blocks)): + if len(blocks[index]) < 3: + changed = blocks[:index] + (blocks[index] + (target,),) + blocks[index + 1:] + stack.append((target + 1, changed)) + require(not stack, "enumeration exceeded its exact node bound") + + +def exhaustive_frontiers(): + rows = [] + for colors in range(1, 6): + minima = {} + count = 0 + for blocks in partitions(2 * colors): + batches, incidences = inventory(colors, blocks) + minima[batches] = min(minima.get(batches, 2 * colors + 1), incidences) + count += 1 + require(min(minima) == first_batch_count(colors), "capacity lower bound") + for batches in range(first_batch_count(colors), colors + 1): + require(minima[batches] == 2 * colors - batches, "frontier mismatch") + for batches in range(colors + 1, 2 * colors + 1): + require(minima[batches] >= colors, "dominated range mismatch") + rows.append({"colors": colors, "partitions": count, + "minimum_incidences": minima}) + return rows + + +def constructive_checks(): + cases = 0 + equality_colors = [] + for colors in range(1, MAX_COLORS + 1): + first = first_batch_count(colors) + for batches in range(first, colors + 1): + actual = inventory(colors, grouping(colors, batches)) + require(actual == (batches, 2 * colors - batches), "bad construction") + cases += 1 + dense_bill = 24 * colors - 6 * first + require(9 * dense_bill <= 10 * 18 * colors, "sharp ratio failed") + equality = 9 * dense_bill == 10 * 18 * colors + require(equality == (colors % 3 == 0), "ratio equality classification") + if equality: + equality_colors.append(colors) + return {"groupings": cases, "sharp_ratio_equality_colors": equality_colors} + + +def price_checks(rows): + prices = tuple(Fraction(value, 2) for value in (1, 2, 3, 4, 6, 12, 24)) + cases = 0 + for row in rows: + colors = row["colors"] + first = first_batch_count(colors) + for setup in prices: + for color_price in prices: + bills = [setup * batches + color_price * incidences + for batches, incidences in row["minimum_incidences"].items()] + chosen = colors if setup < color_price else first + expected = setup * chosen + color_price * (2 * colors - chosen) + require(min(bills) == expected, "price endpoint failed") + if setup == color_price: + for batches in range(first, colors + 1): + actual = row["minimum_incidences"][batches] + require(setup * batches + color_price * actual == expected, + "equal-price tie failed") + cases += 1 + return cases + + +def rejection_checks(): + bad = ( + (0, [[0, 1]]), (True, [[0, 1]]), (1, []), (1, [[]]), + (1, [[0, 0]]), (1, [[0]]), (1, [[0, 2]]), (1, [[False, 1]]), + (2, [[0, 1, 2, 3]]), (1, "01"), + ) + for colors, groups in bad: + try: + inventory(colors, groups) + except ValueError: + continue + raise ValueError("malformed grouping accepted") + for colors, batches in ((3, 1), (3, 4), (1, True), (257, 200)): + try: + grouping(colors, batches) + except ValueError: + continue + raise ValueError("out-of-domain constructor input accepted") + return len(bad) + 4 + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write generated evidence outside the package") + args = parser.parse_args() + package = Path(__file__).resolve().parent + if args.receipt is not None: + destination = args.receipt.resolve() + require(not destination.is_relative_to(package), "receipt must be outside package") + rows = exhaustive_frontiers() + construction = constructive_checks() + result = {"status": "PASS_PAIRED_COLOR_BATCH_FRONTIER", + "claim_type": "scoped written proof with finite corroboration", + "exhaustive_frontiers": rows, "construction": construction, + "price_cases": price_checks(rows), "rejection_controls": rejection_checks(), + "python": sys.version.split()[0], "optimized": sys.flags.optimize, + "source_sha256": {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES}} + dense = inventory(3, [[0, 1, 4], [2, 3, 5]]) + separate = inventory(3, [[0, 1], [2, 3], [4, 5]]) + require(6 * dense[0] + 12 * dense[1] == 60, "dense witness") + require(6 * separate[0] + 12 * separate[1] == 54, "optimal witness") + result["sharp_witness"] = {"dense_bill": 60, "optimal_bill": 54, "ratio": "10/9"} + encoded = json.dumps(result, sort_keys=True, indent=2) + "\n" + if args.receipt is not None: + args.receipt.write_text(encoded, encoding="utf-8") + print(encoded, end="") + + +if __name__ == "__main__": + main()