diff --git a/research/global-batch-library-minimum/README.md b/research/global-batch-library-minimum/README.md new file mode 100644 index 0000000000..da09d8fae4 --- /dev/null +++ b/research/global-batch-library-minimum/README.md @@ -0,0 +1,195 @@ +# Global minimum of a fixed chronological batching library + +A scoped proof, produced by Nick Petalas. + +For a fixed descending batch system, the recursively least LCM construction +has a stronger property than local minimality: its width at every rank divides +the width of every feasible competing library. Jointly enlarging earlier +libraries cannot reduce a later width. This settles the joint-library part of +Open next question 1 in Mihir Srivastava's +[PR #4507](https://github.com/CrocSwap/integer-mult-bounds/pull/4507), within +its fixed batching policy. It does not optimize different policies or schedules. +No new kappa is claimed. + +## Statement + +Fix base widths `b_0,...,b_(m-1) > 0`. For every `n >= m`, fix a positive +integer source count `S_n` and a finite list `C_n` of batches `(e,q)` with +`0 <= e < n` and positive integer `q`. The lists are fixed independently of +the chosen widths. Repeated cuts stay separate; an empty list is allowed. + +A feasible library has the prescribed base widths and, at every nonbase rank, + +```text +B_n = S_n A_n, A_n is a positive integer, +B_e divides A_n q for each (e,q) in C_n. +``` + +The last condition is the whole-invocation contract of #4507. It is a +conditional compiler model, not a new claim about physical realization. +Define + +```text +M_n(B) = lcm over (e,q) in C_n of B_e/gcd(B_e,q), +b_n = S_n M_n(b), with lcm(empty)=1. +``` + +**Theorem.** For any finite terminal rank, the recursively defined `b` is +feasible and `b_n | B_n` at every rank of every feasible library `B` with the +same base widths. In particular, it simultaneously minimizes all widths in +ordinary numerical order. It is the unique componentwise least library. +The conclusion holds at every rank of an infinite descending system as well, +by applying the finite assertion to each initial segment. + +**Proof.** The elementary identity + +```text +d divides a q iff d/gcd(d,q) divides a +``` + +shows that a library is feasible at rank `n` exactly when `M_n(B) | A_n`. +This is #4507's local lemma. It proves feasibility of `b` by induction. + +The new induction compares `b` with an arbitrary feasible library, allowing +all its earlier widths to differ. For positive integers `d | D`, + +```text +d/gcd(d,q) divides D/gcd(D,q). +``` + +For each prime `p`, the valuations of these two quotients are +`max(v_p(d)-v_p(q),0)` and `max(v_p(D)-v_p(q),0)`. The first is at most the +second. Thus `b_e | B_e` for earlier ranks implies `M_n(b) | M_n(B)`. +Feasibility gives `M_n(B) | A_n`, so +`b_n = S_n M_n(b) | S_n A_n = B_n`. The bases agree, completing the induction. +All widths are positive, so divisibility implies the claimed numerical order +and uniqueness. This uses elementary integer divisibility; no literature +priority is claimed for the underlying identity. + +## Exact feasible-library description and normalization + +Every feasible library has a unique positive integer slack at each nonbase rank: + +```text +B_n = S_n M_n(B) t_n, t_n >= 1. +``` + +Conversely, independently choosing any positive integer sequence `t_n` and +using this recurrence produces a feasible library. Necessity and uniqueness +follow by integer division using the local lemma; sufficiency follows directly +from the displayed batch divisibilities. Thus there is no hidden joint search +within this policy: all feasible alternatives are obtained by these slacks, +and the all-one slack vector is a simultaneous minimum. + +One can normalize any feasible library in increasing rank order by replacing +`B_n` with `b_n` while retaining every later width. Earlier ranks already equal +`b`; the new rank is feasible by definition. Every later constraint remains +valid because its newly substituted child width divides its previous value. +The later source counts and replication factors stay fixed. This gives a +feasible sequence of local replacements ending at the least library. + +The converse to the theorem alone is false: arbitrary coordinate multiples of +`b` need not be feasible. With base `1`, source counts `2,1`, an empty first +batch list and second list `[(1,1)]`, the least library is `(1,2,2)`. +The coordinate multiples `(1,6,2)` fail because `6` does not divide `2`. +The slack recurrence, rather than unrestricted coordinate multiplication, +is the exact description. + +## First fixture and executed evidence + +The three-rank fixture uses base `2`, source counts `3,5,2`, and batch lists +`[(0,1)]`, `[(0,2),(1,4)]`, `[(1,3),(2,5)]`. It gives +`b=(2,6,15,12)`. Slacks `(2,3,2)` instead give `(2,12,45,144)`. +Both are feasible and the least widths divide the enlarged ones coordinatewise. +The least sequence decreases at its last rank; monotonicity in rank is not +needed. + +`library.py` and `verify.py` are new implementations. They import no predecessor +programs and do not recount any predecessor width or flow. `RESULT.json` is +generated by the verifier and binds its exact implementation, statement and +metadata hashes. The finite checks enumerate candidate libraries directly, +independently of the slack constructor, then check divisibility, slack recovery +and feasibility after every normalization step. Larger deterministic systems +cover empty batch lists, repeated child ranks and nonunit bases. Semantic +controls distinguish source multiples, separate cuts, gcd savings and LCM from +product. Invalid inputs and the largest allowed rank/scalar boundary are tested. +The receipt reports the exact enumerated counts. These checks corroborate the +written all-size proof; they are not its substitute. + +The replay is read-only, standard-library CPython 3.12. From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/global-batch-library-minimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/global-batch-library-minimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/global-batch-library-minimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/global-batch-library-minimum --check-source-history +``` + +Substitute another CPython 3.12 executable when needed. `--write PATH` creates +a new receipt and refuses to overwrite an existing file. Default execution +requires the committed receipt. The final preflight command requires a commit. + +## Scope, limits and provenance + +The explicit scope change from `independent-moment` is a compiler-width side +result answering #4507, rather than a new paid moment or an audit. The current +source-binding orientation command passed. The card's historical +`scripts/research_baseline.py` first step was also attempted and failed with +`KeyError: 'bit_lower'` on the current selected schema; it is not a claimed pass. +Neither command replays a scientific predecessor result. + +The theorem assumes fixed source counts and batch lists, fixed bases, rank +descent, whole invocations and one common replication factor per rank. +It compares libraries built with that contract. Arbitrary alternative suppliers, +changed batch lists, per-class replication and cross-cut pooling are different +models. It gives no tighter asymptotic growth order, native admission, physical +routing or storage bill, new normalized leaf cost, full multiplication theorem +or selected-frontier change. Independent human and formal proof-kernel review +are unclaimed. + +Executable limits are 32 total ranks, 32 batches per rank, and positive source, +base, batch and slack values at most 65,535. Every constructed width divides the +product of all bases and all source/slack factors in its initial segment, so +its bit length is bounded by 16 times the number of factors. Python's managed +integer/collection allocation is a documented Power of Ten deviation; these +limits bound live storage and all loops. The constructor enforces its slack +limit; the literal feasibility predicate and slack recovery also accept wider +feasible libraries below their separate 1,536-bit width cap. Recompiling a +recovered slack above 65,535 is intentionally rejected. The executable +round-trip claim therefore covers the constructor domain only; a boundary +control demonstrates the distinction. There is no recursion or dynamic code +execution. Functions stay below 60 lines. Explicit exceptions preserve checks +under optimization. Warning-strict normal and optimized replay are registered; +no additional static analyzer or proof assistant is claimed. + +The pinned #4507 README supplies the local lemma, policy and open question. +It is provenance only, not a live scientific input or an executable dependency. +The main-tree and merged-PR searches covered distinctive terms for global +library optimization, least widths, coordinate divisibility and joint batching. +Live open PRs, recent account submissions and handoff claims were also read. +The cached card search had sparse omissions. None of these searches proves +novelty outside its stated coverage. + +## Open next questions + +Can independent replication of different path classes beat the common-factor +minimum without changing chronology or productive-input accounting? This is a +changed model and could escape the present obstruction. Start with one actual +flow containing two path classes with coprime local moduli; state how native +calls match and how completed arrays rejoin before computing a width. The +missing per-class matching and return contract blocks applying that relaxation +to the existing compiler. No new construction round is justified by this +integer result alone. + +## Credit + +Mihir Srivastava / mihir-s-05 supplied #4507's exact local gcd/LCM policy and +explicit joint-library question. Jacob Alan Sussman supplied the integer +lockstep compiler; zxv supplied #4436's chronological flow and #4483's +arbitrary-height setting. codyw912 supplied #4638's sharper width bounds and +arbitrary-height cut transfer. Cinna Davis supplied the native construction, +and Ryanson Jonathan supplied the separately credited flow/width evidence. +Their results are cited rather than reverified. The contribution produced by +Nick Petalas is the comparison with every feasible library, the slack +characterization and the feasible normalization argument. New material is +Apache-2.0. diff --git a/research/global-batch-library-minimum/RESULT.json b/research/global-batch-library-minimum/RESULT.json new file mode 100644 index 0000000000..739ca59fd6 --- /dev/null +++ b/research/global-batch-library-minimum/RESULT.json @@ -0,0 +1,83 @@ +{ + "claim_type": "scoped proof", + "controls": { + "capacity_controls": 3, + "invalid_inputs": 13, + "maximum_width_bits": 1008, + "semantic_controls": 8 + }, + "exhaustive": { + "candidate_libraries": 944784, + "feasible_libraries": 30591, + "normalization_steps": 61182, + "systems": 729 + }, + "fixture": { + "bases": [ + 2 + ], + "enlarged": [ + 2, + 12, + 45, + 144 + ], + "least": [ + 2, + 6, + 15, + 12 + ], + "levels": [ + [ + 3, + [ + [ + 0, + 1 + ] + ] + ], + [ + 5, + [ + [ + 0, + 2 + ], + [ + 1, + 4 + ] + ] + ], + [ + 2, + [ + [ + 1, + 3 + ], + [ + 2, + 5 + ] + ] + ] + ] + }, + "larger": { + "coordinates": 24576, + "libraries": 2048, + "systems": 128 + }, + "schema": "global-batch-library-minimum/v1", + "source_sha256": { + "README.md": "c873401f98a7751cba159a1ea3b6fcd47900d33096e42d0670eb09dfdbf95498", + "SOURCES.json": "a6e6bdcbd605b6e415ba254f80ec293d0af4ba142f46ba2b4b0e032565f99f8e", + "TASK.json": "728a8da437081919ae976b0e3ba03653c8928cbb8c09ab6f32d92934b9656066", + "VERIFY.json": "34e689a6584f05f8e993eb7e7af0b0e43d71f6739da768d9a699f3b62df547db", + "library.py": "307cd4dcdc3a3feca486f221c75e652055bdfa12815b5b35276e68f316cbe814", + "verify.py": "1d2c16ec4f95070c35ae84599b58f1fb3c5ab31b968adb5005feb4b158e4a4b9" + } +} diff --git a/research/global-batch-library-minimum/SOURCES.json b/research/global-batch-library-minimum/SOURCES.json new file mode 100644 index 0000000000..6d65464297 --- /dev/null +++ b/research/global-batch-library-minimum/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/chronological-batch-width/README.md", + "usage": "provenance", + "git_blob": "c85304a601f858774f425d5f3869ac0a6f85ec29", + "sha256": "0cf276c77016a98a0dabba822d27bb9cb94c0bf86ec353a16499fe85e6032c20" + } + ] +} diff --git a/research/global-batch-library-minimum/TASK.json b/research/global-batch-library-minimum/TASK.json new file mode 100644 index 0000000000..523c255a11 --- /dev/null +++ b/research/global-batch-library-minimum/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Global divisibility minimum and exact slack characterization for every library in a fixed descending chronological batch system.", + "scope_change_reason": "Answer the explicit joint-library part of PR4507 Open next question 1 with a new scoped proof, instead of auditing paid moments.", + "bottleneck_link": "Rules out joint enlargement of earlier common-replication libraries as a source of width savings; a further gain must change the batching contract.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved original extension and bounded exact corroboration.", + "outcome": "completed", + "evidence": "README.md proof; RESULT.json source-bound generated receipt; verify.py direct enumeration.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can independently replicated path classes reduce width while preserving chronological matching and return?", + "why_it_matters": "It changes a hypothesis of the global minimum theorem and may permit smaller productive width.", + "first_step": "Specify a two-class native matching and completed-return contract with coprime local moduli before computing a width.", + "blocked_by": "No per-class matching and rejoin contract is proved here." + } + ] +} diff --git a/research/global-batch-library-minimum/VERIFY.json b/research/global-batch-library-minimum/VERIFY.json new file mode 100644 index 0000000000..966e28ba9d --- /dev/null +++ b/research/global-batch-library-minimum/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": "Exact direct library enumeration, slack characterization, feasible normalization, semantic and invalid-input controls; source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same scoped result with optimization enabled; checks remain active." + } + ] +} diff --git a/research/global-batch-library-minimum/library.py b/research/global-batch-library-minimum/library.py new file mode 100644 index 0000000000..c273b42e02 --- /dev/null +++ b/research/global-batch-library-minimum/library.py @@ -0,0 +1,93 @@ +"""Finite exact batching libraries. See README.md for the unbounded theorem.""" +from math import gcd, lcm + +MAX_RANKS = 32 +MAX_BATCHES = 32 +MAX_INPUT = 65535 + + +def positive(value: int) -> bool: + return type(value) is int and 1 <= value <= MAX_INPUT + + +def validate(bases: tuple, levels: tuple) -> None: + """Validate once at the public system boundary; internal helpers trust it.""" + if not isinstance(bases, tuple) or not 1 <= len(bases) <= MAX_RANKS: + raise ValueError("bases must be a nonempty bounded tuple") + if not all(positive(value) for value in bases): + raise ValueError("base widths must be bounded positive integers") + if not isinstance(levels, tuple) or len(bases) + len(levels) > MAX_RANKS: + raise ValueError("too many levels or wrong container") + for offset, level in enumerate(levels): + if not isinstance(level, tuple) or len(level) != 2: + raise ValueError("level must be a source-count/batches pair") + sources, batches = level + if not positive(sources): + raise ValueError("source count must be a bounded positive integer") + if not isinstance(batches, tuple) or len(batches) > MAX_BATCHES: + raise ValueError("batches must be a bounded tuple") + rank = len(bases) + offset + for batch in batches: + if not isinstance(batch, tuple) or len(batch) != 2: + raise ValueError("batch must be a rank/count pair") + child, count = batch + if type(child) is not int or not 0 <= child < rank: + raise ValueError("child rank must strictly descend") + if not positive(count): + raise ValueError("batch count must be a bounded positive integer") + + +def multiplier(widths: list[int], batches: tuple) -> int: + """Local predecessor formula, applied only to validated system rows.""" + value = 1 + for child, count in batches: + width = widths[child] + value = lcm(value, width // gcd(width, count)) + return value + + +def compile_library(bases: tuple, levels: tuple, slacks: tuple) -> tuple[int, ...]: + """Each independent positive slack gives exactly one feasible library.""" + validate(bases, levels) + if not isinstance(slacks, tuple) or len(slacks) != len(levels): + raise ValueError("one slack is required per nonbase rank") + if not all(positive(value) for value in slacks): + raise ValueError("slacks must be bounded positive integers") + widths = list(bases) + for (sources, batches), slack in zip(levels, slacks, strict=True): + widths.append(sources * slack * multiplier(widths, batches)) + # All widths divide the product of base widths, sources and slacks. + if max(widths).bit_length() > 16 * (len(bases) + 2 * len(levels)): + raise ArithmeticError("width exceeded the proved product bound") + return tuple(widths) + + +def feasible(bases: tuple, levels: tuple, widths: tuple) -> bool: + """Literal whole-invocation conditions, without the gcd/LCM formula.""" + validate(bases, levels) + if not isinstance(widths, tuple) or len(widths) != len(bases) + len(levels): + raise ValueError("wrong library length") + if not all(type(value) is int and 0 < value < (1 << 1536) for value in widths): + raise ValueError("library widths must be bounded positive integers") + if widths[:len(bases)] != bases: + return False + for rank, (sources, batches) in enumerate(levels, start=len(bases)): + if widths[rank] % sources: + return False + replication = widths[rank] // sources + if any((replication * count) % widths[child] for child, count in batches): + return False + return True + + +def recover_slacks(bases: tuple, levels: tuple, widths: tuple) -> tuple[int, ...]: + """Recover the unique slack vector of a feasible library.""" + if not feasible(bases, levels, widths): + raise ValueError("library is infeasible") + slacks = [] + for rank, (sources, batches) in enumerate(levels, start=len(bases)): + modulus = sources * multiplier(list(widths[:rank]), batches) + if widths[rank] % modulus: + raise ArithmeticError("literal feasibility did not imply the modulus") + slacks.append(widths[rank] // modulus) + return tuple(slacks) diff --git a/research/global-batch-library-minimum/verify.py b/research/global-batch-library-minimum/verify.py new file mode 100644 index 0000000000..b9e18a7e6a --- /dev/null +++ b/research/global-batch-library-minimum/verify.py @@ -0,0 +1,168 @@ +"""Read-only exact corroboration; --write writes a source-bound receipt once.""" +import argparse +import hashlib +import itertools +import json +import sys +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +from library import compile_library, feasible, recover_slacks + + +def need(condition: bool, message: str) -> None: + if not condition: + raise AssertionError(message) + + +def fixture() -> dict: + bases = (2,) + levels = ((3, ((0, 1),)), (5, ((0, 2), (1, 4))), + (2, ((1, 3), (2, 5)))) + least = compile_library(bases, levels, (1, 1, 1)) + enlarged = compile_library(bases, levels, (2, 3, 2)) + need(least == (2, 6, 15, 12), "first working fixture") + need(enlarged == (2, 12, 45, 144), "enlarged fixture") + need(feasible(bases, levels, least), "least fixture feasible") + need(feasible(bases, levels, enlarged), "enlarged fixture feasible") + return {"bases": bases, "levels": levels, "least": least, "enlarged": enlarged} + + +def exhaustive_libraries() -> dict: + """Enumerate widths directly, so candidates are not generated by the theorem.""" + systems = libraries = admitted = normalizations = 0 + for base, s1, s2, q1, q2, q3 in itertools.product(range(1, 4), repeat=6): + bases = (base,) + levels = ((s1, ((0, q1),)), (s2, ((0, q2), (1, q3)))) + least = compile_library(bases, levels, (1, 1)) + systems += 1 + for a, b in itertools.product(range(1, 37), repeat=2): + widths = (base, a, b) + libraries += 1 + if not feasible(bases, levels, widths): + continue + admitted += 1 + need(all(big % small == 0 for small, big in zip(least, widths)), + "global divisibility") + slacks = recover_slacks(bases, levels, widths) + need(compile_library(bases, levels, slacks) == widths, "slack bijection") + # Normalize one rank, retaining all later widths exactly. + current = list(widths) + for rank in range(1, 3): + current[rank] = least[rank] + need(feasible(bases, levels, tuple(current)), "normalization remains feasible") + normalizations += 1 + return {"systems": systems, "candidate_libraries": libraries, + "feasible_libraries": admitted, "normalization_steps": normalizations} + + +def larger_libraries() -> dict: + """Deterministic finite families with repeated edges, empty cuts and nonunit bases.""" + systems = libraries = coordinates = 0 + for seed in range(1, 129): + bases = (1 + seed % 7, 1 + (seed * 3) % 11) + levels = [] + for rank in range(2, 12): + batches = tuple(((seed + j * 7) % rank, 1 + (seed * j + rank) % 13) + for j in range(seed % 6)) + levels.append((1 + (seed + rank * 5) % 17, batches)) + levels = tuple(levels) + least = compile_library(bases, levels, (1,) * len(levels)) + systems += 1 + for trial in range(1, 17): + slacks = tuple(1 + (seed * trial + j * 3) % 7 for j in range(len(levels))) + widths = compile_library(bases, levels, slacks) + need(feasible(bases, levels, widths), "generated library literal feasibility") + need(recover_slacks(bases, levels, widths) == slacks, "slack inversion") + need(all(big % small == 0 for small, big in zip(least, widths)), + "larger global divisibility") + libraries += 1 + coordinates += len(widths) + return {"systems": systems, "libraries": libraries, "coordinates": coordinates} + + +def expect_rejected(bases: tuple, levels: tuple, slacks: tuple, message: str) -> None: + try: + compile_library(bases, levels, slacks) + except ValueError as error: + need(str(error) == message, "wrong rejection cause") + else: + raise AssertionError("invalid system accepted") + + +def controls() -> dict: + bases, levels = (1,), ((2, ()), (1, ((1, 1),))) + least = compile_library(bases, levels, (1, 1)) + need(least == (1, 2, 2), "small control fixture") + need(not feasible(bases, levels, (1, 6, 2)), "mere coordinate multiples fail") + need(feasible(bases, levels, (1, 6, 6)), "propagated enlargement works") + # Removing the source-count divisibility would accept this width. + need(not feasible((1,), ((3, ()),), (1, 2)), "source multiple is mandatory") + # Aggregating two separate unit cuts loses their individual constraint. + cuts = ((1, ((0, 1), (0, 1))),) + pooled = ((1, ((0, 2),)),) + need(compile_library((2,), cuts, (1,)) == (2, 2), "separate cuts") + need(compile_library((2,), pooled, (1,)) == (2, 1), "pooling changes the system") + # Gcd savings cannot be deleted; conversely a product is not an LCM. + need(compile_library((6,), ((1, ((0, 3),)),), (1,)) == (6, 2), "gcd cancellation") + need(compile_library((2, 4), ((1, ((0, 1), (1, 1))),), (1,)) == (2, 4, 4), + "LCM is not product") + invalid = [ + ((), (), (), "bases must be a nonempty bounded tuple"), + ((True,), (), (), "base widths must be bounded positive integers"), + ((0,), (), (), "base widths must be bounded positive integers"), + ((65536,), (), (), "base widths must be bounded positive integers"), + ((1,), ((0, ()),), (1,), "source count must be a bounded positive integer"), + ((1,), ((1, ((1, 1),)),), (1,), "child rank must strictly descend"), + ((1,), ((1, ((-1, 1),)),), (1,), "child rank must strictly descend"), + ((1,), ((1, ((0, 0),)),), (1,), "batch count must be a bounded positive integer"), + ((1,), ((1, ()),), (), "one slack is required per nonbase rank"), + ((1,), ((1, ()),), (0,), "slacks must be bounded positive integers"), + ((1,), ((1, ()),) * 32, (1,) * 32, "too many levels or wrong container"), + ((1,), ((1, ((0, 1),) * 33),), (1,), "batches must be a bounded tuple"), + ] + for b, rows, slacks, message in invalid: + expect_rejected(b, rows, slacks, message) + need(compile_library((3, 5), (), ()) == (3, 5), "base-only library") + # Largest accepted rank and scalar limits exercise the memory bound. + big = tuple((65535, ((rank - 1, 1),)) for rank in range(1, 32)) + widths = compile_library((65535,), big, (65535,) * 31) + need(feasible((65535,), big, widths), "capacity boundary") + need(widths[-1].bit_length() == 1008, "growing integer capacity") + full = ((1, ((0, 1),) * 32),) + need(compile_library((2,), full, (1,)) == (2, 2), "maximum batch count") + # Literal feasibility is intentionally broader than the constructor's slack domain. + need(feasible((1,), ((1, ()),), (1, 65536)), "larger feasible slack") + need(recover_slacks((1,), ((1, ()),), (1, 65536)) == (65536,), "larger slack recovery") + expect_rejected((1,), ((1, ()),), (65536,), + "slacks must be bounded positive integers") + return {"semantic_controls": 8, "invalid_inputs": len(invalid) + 1, + "capacity_controls": 3, "maximum_width_bits": widths[-1].bit_length()} + + +def rebuild() -> dict: + sources = {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in ("library.py", "verify.py", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json")} + return {"schema": "global-batch-library-minimum/v1", "claim_type": "scoped proof", + "source_sha256": sources, "fixture": fixture(), "exhaustive": exhaustive_libraries(), + "larger": larger_libraries(), "controls": controls()} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="new receipt path; existing files are never overwritten") + args = parser.parse_args() + result = rebuild() + serialized = json.dumps(result, sort_keys=True, indent=2) + "\n" + if args.write: + with args.write.open("x", encoding="utf-8") as stream: + stream.write(serialized) + else: + need(serialized == (PACKAGE / "RESULT.json").read_text(), "source-bound receipt mismatch") + print("PASS_GLOBAL_BATCH_LIBRARY_MINIMUM", json.dumps(result["exhaustive"], sort_keys=True)) + print(json.dumps({"larger": result["larger"], "controls": result["controls"]}, sort_keys=True)) + + +if __name__ == "__main__": + main()