Prove global fixed-batch library minimality (no new κ)

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.

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"
+  }
+}

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"
+    }
+  ]
+}