diff --git a/research/adaptive-chronological-batching/README.md b/research/adaptive-chronological-batching/README.md new file mode 100644 index 0000000000..d8cb94c3f4 --- /dev/null +++ b/research/adaptive-chronological-batching/README.md @@ -0,0 +1,279 @@ +# Chronological batch divisibility for arbitrary-height forests + +**Result (conditional batching transfer, no new kappa).** Mihir Srivastava's +[PR #4507](https://github.com/CrocSwap/integer-mult-bounds/pull/4507) gives the +least per-cut replication factor for the *default-height* direct flow of zxv's +[PR #4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436). Its open +question 2 asks whether that policy survives the arbitrary-height forests of +[PR #4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483). It does. +For every height `G >= 0` and every ambient rank whose forest contains a unit, +the same batch list, least-LCM replication factor and cost recurrence hold, and +the normalized rank-one leaf cost is unchanged. #4483 already covers the +aggregate arbitrary-height flow, so what is new here is the **batch level**: +which exits must form one whole supplier batch, and why. The conditional +width theorem below bounds width growth, not a tighter leaf exponent; +there is no convergence or native-admission claim. + +**Executed evidence.** Python 3.12.14, standard library only. +The direct isolated replay passed in 35.02 s: 405 nonempty census fixtures, +19,089 literal oracle classes, 2,304 brute-force minimality cases and 25 +semantic rejection controls. Six compilations check 186,476 chronological +batch constraints. The final width replay passed in 2.20 s: four additional finite +compilations, 13,377 batch constraints, three pinned profile applications +and two boundary controls. Receipts are [RESULT.json](RESULT.json) and +[WIDTH-RESULT.json](WIDTH-RESULT.json). + +Huge receipt integers are represented by bit length and big-endian SHA256; +the exact calculations and acceptance comparisons still use integers. +No global integer-to-decimal safety limit is disabled. + +Independent OpenAI review of the Anthropic batching implementation found no +blocking issue; its isolated optimized replay passed in 34.39 s. Independent +Anthropic review of the OpenAI width implementation and its proof found no +gap; its final isolated optimized replay passed in 2.25 s. These are AI +checks, not human or proof-kernel acceptance. + +The companion conditional all-rank width theorem is in [WIDTH.md](WIDTH.md). +It is a separate argument, written and reviewed by the parent, and is not +repeated here. This package and the preserved +[default-height package](../chronological-width-bound/README.md) form one +contribution with two scoped replays, not two competing submissions. + +**Delta against the closest proofs and checks.** +[#4586](https://github.com/CrocSwap/integer-mult-bounds/pull/4586) at +`aadb7bc59390683450b1969e4632f546929dc569` already proves the default-height +bound `log B_N=O((1+log N)^(d+2))`. The default companion sharpens it to +`d+1` by bounding visits to each source-count plateau. +[#4588](https://github.com/CrocSwap/integer-mult-bounds/pull/4588) at +`2f6578907b7f8718a13921552cc3069d3908e936` supplies independent finite +default checks. [#4591](https://github.com/CrocSwap/integer-mult-bounds/pull/4591) +at `84c0fb3a39bcb1e4b8c48892bfdd8a6e7ae58a50` checks arbitrary-height +aggregate identities, not feasibility of each actual chronological cut. +This package adds that cut-level transfer and its conditional fixed-parameter +all-rank envelope; it does not claim the inherited aggregate identities, +least-LCM algorithm or default finite width improvement as new. + +**Specialization is symbolic, with distinct hypotheses.** WIDTH.md gives +`z=max(0,1-g log_M(k0))` and degree `d'+1`. At `M=k0,g=1`, `d'=d,z=0`, +so it recovers the default order on their common domain. The named adaptive +code interface requires positive `a,b`, hence `g=a+b>=2`; that route does +not exercise `g=1`. Direct fixed-height/g witnesses are separate. WIDTH.md +assumes paid rank one for nonemptiness; the default proof needs no such +assumption because its root is nonempty. The default plateau-product and +adaptive level-LCM divisors differ; neither is claimed universally smaller. + +## 1. What is certified + +Fix positive integer multiplicities `W_k` (target ranks, `2 <= k0 <= k <= m`) +and `P_r` (chronological paid ranks, `1 <= r <= rmax < m`). At ambient rank `n` +put `C = floor(n/m)` and pick any integer height `G >= 0`. The forest has one +class per paid-round path `(d, rho)`; `rho` is the product of the paid ranks +along the path. Class `(d, rho)` holds the units `u(alpha)` of every target +multiindex of degree `G-d` with `rho c(alpha) <= C` (PROOF.md of #4483, section +1). A class that holds no unit still spawns its child at paid rank `r` whenever +`rho r <= C`; those children can hold units and fresh sources. + +**Batches.** The complete batch list at `n` is + +1. `(n-s, S_s)` for every source rank `s`, taken before the flow starts, and +2. `(e, q)` for each *cut*: one paid position of one path class, grouping the + equal-rank unmatched exits of that class's units. + +The replicated copies, the repeated paid positions and the repeated path +classes are occurrences. They multiply the exit and cost census, **never** the +`q` of a cut. + +**Theorem A.** Let `B_j > 0` be the prescribed widths for `j < n`, with +`B_0 = 1`, and let `S > 0` be the source count. Put + +```text +a_n = lcm over batches (e,q) of B_e / gcd(B_e, q), B_n = S a_n. +``` + +Then (i) every batch is a whole number of supplier invocations at replication +`a_n`, (ii) `a_n` is the least such positive integer for this policy and these +`B_j`, and (iii) the normalized leaf cost obeys #4483's recurrence + +```text +L(n) = [ sum_s S_s L(n-s) + sum_e E_e L(e) ] / sum_s S_s, +``` + +independent of every `B_j`. This equals the leaf cost of the nested #4436 +widths at each rank, whenever both widths are valid. + +## 2. Why #4507's proof extends + +#4507's argument uses only the following facts about the forest. Each is +re-derived for arbitrary `G`; none needs `G = floor(log_k0 C)`. + +* **Divisibility (ii).** `B_e` divides `a q` exactly when `(B_e/g) | a` for + `g = gcd(B_e, q)`, because `B_e/g` and `q/g` are coprime. The conditions for + all batches hold exactly when their LCM divides `a`. This is height-free + number theory. +* **Strict descent.** Every recursive call must have a smaller rank so strong + induction supplies `B_j`. An exit is an actual paid job of rank `r z` + with `z <= C`, so `1 <= e <= rmax n/m < n`. A source has rank + `k z` with column `z <= C`, hence `1 <= s <= n`, and its complement `n-s` + lies in `[0, n-1]`; rank 0 costs 0. **Root sources can be small** at large + `G` (as small as `k0^(G+1)`), which breaks the default-height lower bound + `s > n/m` on every source. It does not break descent: only `s >= 1` is used, + and a smaller `s` only enlarges the complement rank. +* **Cut structure.** At depth `G` a present class has `F_0(1) = 1` unit, so each + paid position of a leaf class is a cut of size one. At depth `d < G` a present + parent at product `c` supplies `F_(G-d)(c)` units and the child at paid + rank `r` demands the Pascal terms with `rho r c/k <= C`. Present supply + covers demand (Pascal expansion), the positive difference is one cut at + rank `rho r c`, and demand with an **absent** parent + (`rho c > C`) is a fresh inner source. Distinct target multisets with one + product `c` are one cut because they leave through the same rank, `rho r c`; + the batch list sums them. +* **Empty classes.** A class that holds no unit has an empty supply but its + child may not, so the path must continue while `rho r <= C`. Dropping it + loses the later components and their sources. This is the case that the + default height never reaches, since there the root is always nonempty. +* **Chronology.** Each class and all its exits return before the next + suspended paid position resumes, so cuts of different paths or positions are + never pooled even if their ranks agree. + +The cost step is the same: complements contribute +`sum_s (a S_s/B_(n-s)) P_(n-s)` leaves and cuts contribute +`sum_cuts (a q/B_e) P_e` with all occurrences kept. Dividing by `B_n = a S` +cancels `a`, and induction from `B_e = 1, P_e = e` below `m` gives the +recurrence. No claim is made about physical routing or native cost. + +**Mathematical limitation.** Minimality is local to this policy, one fixed +library of smaller widths, and one common replication per rank. Joint +optimization, fractional or per-class replication, and widths not forced by +divisibility are outside it. Nonemptiness of the forest is a hypothesis: the +verifier requires a unit, and an empty flow is not replaced by a supplier. A +paid rank one makes this automatic (WIDTH.md). + +## 3. Independent checks + +`batching.py` holds the multiplicative-polynomial census (`census`, +`batch_rows`, `multiplier`, `compile_widths`, `check_ledger`, `leaf_total`). It +imports no predecessor code. `verify.py` supplies three separate references. + +1. **Literal oracle.** `oracle_flow` enumerates ordered target words by sorted + content, instantiates every paid position separately, and returns each + child before the next position. It uses no Pascal coefficient, no + product-keyed polynomial and no compressed path count. It is compared on + roots, inner sources, boundary exits, leaf exits, columns, units, matched + jobs and the full multiset of cuts `(depth, rho, paid rank, exit rank, q)`, + at toy profiles and several `G`, in both paid orders for two fixtures. +2. **Closed form.** `closed_form` recomputes cut sizes and fresh sources from + `Q = sum_(k|c, rho r (c/k) > C) W_k F_(G-d-1)(c/k)` and its absent-parent + counterpart, sharing nothing with the census. +3. **Authenticated #4483 Flow.** The bytes of `research/rank-convergence/flow.py` + and `research/direct-mixed-flow/flow.py` are hashed against pins before + `exec`. Sources, exits and unit columns are compared on all 405 nonempty + fixtures. Every fixture has paid rank one; rejection of a wholly empty + forest is not exercised. Empty-root forests with later components are. + +On top of this the verifier recovers #4507's default-height widths and leaf +counts, checks that the least width divides the nested one at every rank, +checks the normalized cost recurrence in exact rationals, and brute-forces the +minimality of the LCM against all small `(B, q)` pairs. + +## 4. Semantic controls + +Each control must fail for the stated reason; a wrong exception type or +message fails the check. + +| Control | Why it is semantic | +| --- | --- | +| drop-empty-parent | Suppresses the later components below an empty class. Disagrees with the literal oracle and with the authenticated Flow on the empty-root fixture. | +| drop-boundary, drop-leaf | Remove premature or final exits. Disagree with the oracle and break the formal rank-invoice cancellation. | +| ignore-path-multiplier | Child eligibility without the paid prefix. | +| split-collisions | Keeps distinct same-product target multisets in separate cuts. A pinned collision geometry (targets 2, 4, 8) merges two contents at rank 80. | +| pooled aggregate, occurrences, leaf-pooled | Each pooled multiplier passes its own rows but leaves an actual cut with a nonzero remainder. The verifier first finds a geometry with a real gap for each policy. | +| multiplier missing a prime factor | `a/p` leaves a remainder; `2a` is accepted. | +| zero, boolean and future-rank inputs, equal paid and target maximum, non-integer multiplicity | Contract violations. | +| omitted occurrence leaf cost | Breaks the exact normalized recurrence. | +| tampered flow bytes | Fail before execution. | +| perturbed receipts | A false root, a false unit column and a missing cut fail the ledger. | + +## 5. Source inputs and bounded domain + +Pinned in [SOURCES.json](SOURCES.json) and declared in [VERIFY.json](VERIFY.json): +#4507's `README.md` and `batches.py`; #4483's `PROOF.md`, `flow.py` and +`BENCHMARKS.json`; `direct-mixed-flow/flow.py`; the p7 invoice at +`higher-moment-strictification/RESULT.json`; and, for the width probes, +`native-lattice-retiming/RESULT.json` and `compact-joint-compiler/arithmetic/RESULT.json`. + +The real profile is the pinned raw p7 invoice (7,688 target and 55,998 paid +items), never a retuned strictification. The later +[PR #4533](https://github.com/CrocSwap/integer-mult-bounds/pull/4533) changes +the height base; this package does not certify that geometry. + +Bounded replay domain, set by the code: + +* Oracle census: `n = factor m + extra` for small factors, all eight height + rules, `G <= 6` (`G <= 2` for the heavy repeated-paid profile). The oracle + stops at 300,000 classes. +* Least-width compilations: four toy geometries through rank 100 and two p7 + height rules through rank 1,209. +* Real-profile source comparison: p7 at ranks 121 through 60,000 for the + census only; no all-rank compile there. +* Width probes: see `width_bound.py` and WIDTH.md. + +## Reproduce + +From the repository root: + +```sh +python3.12 -B research/adaptive-chronological-batching/verify.py --write +python3.12 -B research/adaptive-chronological-batching/verify.py +python3.12 -O -B research/adaptive-chronological-batching/verify.py +python3.12 -B research/adaptive-chronological-batching/width_bound.py --write +python3.12 -I -O -B research/adaptive-chronological-batching/width_bound.py +python3 scripts/research_package.py --package research/adaptive-chronological-batching --check-only +``` + +The complete registered replay is +`python3.12 -B scripts/research_package.py --package research/adaptive-chronological-batching`. +`--write` is needed only to intentionally regenerate receipts, not to replay them. +The other scoped replay in the same PR is +`python3.12 -B scripts/research_package.py --package research/chronological-width-bound`. + +`--write` regenerates the committed receipt and then exits. A plain run +replays and requires equality with the receipt. `--survey` prints the +authoring statistics for the pooling gaps. + +## Coordination and historical provenance + +The base `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`, priority revision 7, +the `independent-moment` original card and all source pins remain historical +provenance. The consolidation comparison uses fetched main +`fbc9ea0249746acca4f504d4fda2b84e0e36cf0d`: selected conditional κ is +`.00302015` from #4470, not #4483 or #4507. No selected-frontier file changes. +The 2026-10-22 overlap refresh covers 408 open PRs at 13:08:38 UTC, 3,852 +closed PRs at 13:09:39 UTC and 3,577 Discussion records at 13:09:11 UTC, +with complete reported pagination. This non-atomic snapshot is not an +exhaustive novelty proof; the actual #4586/#4588/#4591 proofs/code supply +the comparison above. Evidence and the combined PR draft remain local-only +pending publication approval. Existing receipts report author/AI runs and +were not regenerated during consolidation; no human/formal acceptance is claimed. + +## Open next questions + +1. **Retuned geometries.** Does a pinned retuned height base such as #4533's 768 + for p16 keep the same divisibility and width envelope? This matters because + a new base changes the forest. A first step is to add its `(M, g)` to the + probes, with an authenticated profile pin, and compare each cap to the + source Flow. Blocker: the pinned profile bytes. +2. **Sharper width envelope.** Can actual gcd savings or narrower semigroup + counts tighten the bound of WIDTH.md? A first step is an exact prime-valuation + recurrence at selected pinned p7 ranks, then a symbolic bound retaining gcd + cancellation. Finite fits alone cannot prove the asymptotic improvement. + +## Credit + +Predecessor work: Jacob Alan Sussman's integer lockstep compiler; zxv's #4436 +chronological flow and #4483 arbitrary-height wrapper; Mihir Srivastava's #4507 +least batching policy, whose proof this package extends; Ryanson Jonathan's +#4459 mirror identity underlies the #4483 accounting. New material here is +Apache-2.0, prepared for codyw912 with substantial AI assistance (OpenAI model +sessions and an Anthropic-model implementation worker). The independent +mathematical challenge of WIDTH.md was also AI review. None of it is human or +proof-kernel verification. diff --git a/research/adaptive-chronological-batching/RESULT.json b/research/adaptive-chronological-batching/RESULT.json new file mode 100644 index 0000000000..6a065ed35b --- /dev/null +++ b/research/adaptive-chronological-batching/RESULT.json @@ -0,0 +1,974 @@ +{ + "brute_force_minimality_cases": 2304, + "census_equalities": { + "boundary_exits": 150, + "empty_parent_later_components": 197, + "empty_roots": 151, + "flows": 405, + "height_above_default": 151, + "inner_sources": 283, + "oracle_classes": 19089, + "repeated_cut_occurrences": 405, + "target_product_collisions": 0 + }, + "claim_type": "conditional batch-level transfer and exact finite accounting", + "geometries": [ + { + "batch_constraints": 1045, + "compiled_ranks": 96, + "cuts": 599, + "leaves": { + "bits": 71, + "unsigned_big_endian_sha256": "fdeb9abfe4cb702fb565f1372a960823f460c893762f61a3d59cf6e17d3dc074" + }, + "maximum": 100, + "name": "overlap-two-bit", + "nested_leaves": { + "bits": 777, + "unsigned_big_endian_sha256": "51bda840a1c97fab628999f630390c326c43a437a76a1f2b62e88dffe4d8ba30" + }, + "nested_width": { + "bits": 771, + "unsigned_big_endian_sha256": "56b23ff43d53172ac67bc343ec3346aadcd6f2c85fdac0b86dbbe38722176fb3" + }, + "normalized_leaf_cost_unchanged": true, + "paid": { + "1": 2, + "4": 1 + }, + "pooling_gaps": { + "aggregate": { + "first": { + "cut": [ + 1, + 1, + 4, + 8, + 1, + 2 + ], + "cut_multiplier": 4, + "failing_cuts": 1, + "height": 2, + "n": 10, + "pooled_multiplier": 2, + "pooled_remainder": 2, + "width": 4 + }, + "ranks_underpaying": 56, + "ranks_with_gap": 56 + }, + "leaf-pooled": { + "first": null, + "ranks_underpaying": 0, + "ranks_with_gap": 0 + }, + "occurrences": { + "first": { + "cut": [ + 1, + 1, + 4, + 8, + 1, + 2 + ], + "cut_multiplier": 4, + "failing_cuts": 1, + "height": 2, + "n": 10, + "pooled_multiplier": 2, + "pooled_remainder": 2, + "width": 4 + }, + "ranks_underpaying": 56, + "ranks_with_gap": 56 + } + }, + "record_sha256": "c05c2af8335e4d66a73f42ebdfc29c5013509dab81e053be5378f45f109fea47", + "rule": [ + "adaptive", + 2, + 1, + 1 + ], + "strict_width_gains": 95, + "targets": { + "2": 1, + "5": 1 + }, + "width": { + "bits": 65, + "unsigned_big_endian_sha256": "cbda8a45ebe1bc8991eab1c731e0d77b2c930bcb6694bdc2feafea01a7e2c9d4" + } + }, + { + "batch_constraints": 1112, + "compiled_ranks": 93, + "cuts": 515, + "leaves": { + "bits": 78, + "unsigned_big_endian_sha256": "7c373f56b76f75c6b1317bbc0926f386e8d316afd86947867aa84c4ef7d2d446" + }, + "maximum": 100, + "name": "collision-two-bit", + "nested_leaves": { + "bits": 701, + "unsigned_big_endian_sha256": "0dd74f3cc2962df941b3c18a87efe2f8388e6891f0f114c7b9c4974489482438" + }, + "nested_width": { + "bits": 697, + "unsigned_big_endian_sha256": "3fd6fe61a15223b14751445e6937f63b39d03e08ebf42c7629110c35766bdaa0" + }, + "normalized_leaf_cost_unchanged": true, + "paid": { + "1": 2, + "3": 1 + }, + "pooling_gaps": { + "aggregate": { + "first": { + "cut": [ + 3, + 1, + 3, + 24, + 1, + 8 + ], + "cut_multiplier": 62725028184, + "failing_cuts": 2, + "height": 6, + "n": 64, + "pooled_multiplier": 15681257046, + "pooled_remainder": 23814, + "width": 31752 + }, + "ranks_underpaying": 21, + "ranks_with_gap": 21 + }, + "leaf-pooled": { + "first": null, + "ranks_underpaying": 0, + "ranks_with_gap": 0 + }, + "occurrences": { + "first": { + "cut": [ + 3, + 1, + 3, + 24, + 1, + 8 + ], + "cut_multiplier": 62725028184, + "failing_cuts": 2, + "height": 6, + "n": 64, + "pooled_multiplier": 15681257046, + "pooled_remainder": 23814, + "width": 31752 + }, + "ranks_underpaying": 21, + "ranks_with_gap": 21 + } + }, + "record_sha256": "93ae9878eeb63040ff1248443c261f10b4709fdc60e2adbe3112927bf3f6a358", + "rule": [ + "adaptive", + 2, + 1, + 1 + ], + "strict_width_gains": 92, + "targets": { + "2": 1, + "4": 1, + "8": 1 + }, + "width": { + "bits": 73, + "unsigned_big_endian_sha256": "2a6ff195ab924b8305eb6b8ab0f70fcd6cf7e72ecc9da035667d68b301c880f2" + } + }, + { + "batch_constraints": 1349, + "compiled_ranks": 98, + "cuts": 834, + "leaves": { + "bits": 139, + "unsigned_big_endian_sha256": "59583d6669684933d9d549325f3cdff4deecbada518f441f982d6ade9a9d471b" + }, + "maximum": 100, + "name": "repeat-two-bit", + "nested_leaves": { + "bits": 2026, + "unsigned_big_endian_sha256": "2c4938cda95a9b7af70f53207b49f924eefedc1812edcc98741074cce88f0926" + }, + "nested_width": { + "bits": 2020, + "unsigned_big_endian_sha256": "6e650da31d2296e2a8197f5f908c1cd3fad75ba6220b9b7096e3dd85f77099ff" + }, + "normalized_leaf_cost_unchanged": true, + "paid": { + "1": 6, + "2": 2 + }, + "pooling_gaps": { + "aggregate": { + "first": { + "cut": [ + 4, + 4, + 2, + 8, + 1, + 1728 + ], + "cut_multiplier": 5700, + "failing_cuts": 1, + "height": 4, + "n": 12, + "pooled_multiplier": 475, + "pooled_remainder": 475, + "width": 5700 + }, + "ranks_underpaying": 85, + "ranks_with_gap": 85 + }, + "leaf-pooled": { + "first": { + "cut": [ + 4, + 4, + 2, + 8, + 1, + 1728 + ], + "cut_multiplier": 5700, + "failing_cuts": 1, + "height": 4, + "n": 12, + "pooled_multiplier": 475, + "pooled_remainder": 475, + "width": 5700 + }, + "ranks_underpaying": 85, + "ranks_with_gap": 85 + }, + "occurrences": { + "first": { + "cut": [ + 4, + 4, + 2, + 8, + 1, + 1728 + ], + "cut_multiplier": 5700, + "failing_cuts": 1, + "height": 4, + "n": 12, + "pooled_multiplier": 475, + "pooled_remainder": 475, + "width": 5700 + }, + "ranks_underpaying": 85, + "ranks_with_gap": 85 + } + }, + "record_sha256": "a7e6c56d1bd4c371161de06645c7fe1b0c58bc12ff78b6d743ce2f553ca3ae37", + "rule": [ + "adaptive", + 2, + 1, + 1 + ], + "strict_width_gains": 97, + "targets": { + "2": 4, + "3": 1 + }, + "width": { + "bits": 133, + "unsigned_big_endian_sha256": "aa049981f3ee4da5cca21b17b87420cf710513467160f227d67d404aa9165a6e" + } + }, + { + "batch_constraints": 1349, + "compiled_ranks": 98, + "cuts": 834, + "leaves": { + "bits": 94, + "unsigned_big_endian_sha256": "c7f005e5c0009d618eda5abc42bf07177df79485b72251ad081209322a7a24dd" + }, + "maximum": 100, + "name": "repeat-default", + "nested_leaves": { + "bits": 1008, + "unsigned_big_endian_sha256": "1302eac01cf514d2855c821612c64c9d38a6c9ff55f12115f72bf34a9906b9d5" + }, + "nested_width": { + "bits": 1002, + "unsigned_big_endian_sha256": "398043f007044ec4c1ba14eda89bf66b48733ce7a22bb855a3bc17a4665b5952" + }, + "normalized_leaf_cost_unchanged": true, + "paid": { + "1": 6, + "2": 2 + }, + "pooling_gaps": { + "aggregate": { + "first": { + "cut": [ + 2, + 4, + 2, + 8, + 1, + 8 + ], + "cut_multiplier": 700, + "failing_cuts": 1, + "height": 2, + "n": 12, + "pooled_multiplier": 175, + "pooled_remainder": 175, + "width": 700 + }, + "ranks_underpaying": 56, + "ranks_with_gap": 56 + }, + "leaf-pooled": { + "first": { + "cut": [ + 2, + 4, + 2, + 8, + 1, + 8 + ], + "cut_multiplier": 700, + "failing_cuts": 1, + "height": 2, + "n": 12, + "pooled_multiplier": 175, + "pooled_remainder": 175, + "width": 700 + }, + "ranks_underpaying": 56, + "ranks_with_gap": 56 + }, + "occurrences": { + "first": { + "cut": [ + 2, + 4, + 2, + 8, + 1, + 8 + ], + "cut_multiplier": 700, + "failing_cuts": 1, + "height": 2, + "n": 12, + "pooled_multiplier": 175, + "pooled_remainder": 175, + "width": 700 + }, + "ranks_underpaying": 56, + "ranks_with_gap": 56 + } + }, + "record_sha256": "1abb2f920d0752473b3d6849520e87ac7fd1ee24923cc3ecebef6c92b9475ee0", + "rule": [ + "default" + ], + "strict_width_gains": 97, + "targets": { + "2": 4, + "3": 1 + }, + "width": { + "bits": 88, + "unsigned_big_endian_sha256": "b5cdb894bc41c24d0a3c8f74c29fa83624cd11cf51de04af408918b25707924b" + } + }, + { + "batch_constraints": 94017, + "compiled_ranks": 1089, + "cuts": 51909, + "leaves": { + "bits": 5460, + "unsigned_big_endian_sha256": "e8a7c29deadd63775b2819c0a76f3f521be34aa9f2d615ca305f18fb47d38ba3" + }, + "maximum": 1209, + "name": "p7-two-bit-height", + "nested_leaves": { + "bits": 74492, + "unsigned_big_endian_sha256": "9ae7cabac3e91302f4c51776c1b6a610295d782b36eec3ac05034e871749ce24" + }, + "nested_width": { + "bits": 74481, + "unsigned_big_endian_sha256": "1a5835faf31726739d73294f5e2dcae182530b4b7269ef5ad1448b9c41935cd9" + }, + "normalized_leaf_cost_unchanged": true, + "paid": { + "1": 37305, + "16": 448, + "2": 10695, + "3": 3360, + "32": 448, + "4": 1530, + "48": 448, + "5": 300, + "8": 1464 + }, + "pooling_gaps": { + "aggregate": { + "first": { + "cut": [ + 3, + 1, + 48, + 288, + 270, + 23258363138136000 + ], + "cut_multiplier": { + "bits": 2815, + "unsigned_big_endian_sha256": "b0004eb49ceac61bb68a9349a6aa500abd73ad273cb1343150bb657951235aff" + }, + "failing_cuts": 2, + "height": 4, + "n": 726, + "pooled_multiplier": { + "bits": 2805, + "unsigned_big_endian_sha256": "34c1e6c4f900dbe0719d913a840f2fce070853956a9bf4a46c9273fd42df8509" + }, + "pooled_remainder": { + "bits": 535, + "unsigned_big_endian_sha256": "d34d252434b4f6854b2692c1ba3d3008ffd18976829ee636b80414b6a77352a2" + }, + "width": { + "bits": 535, + "unsigned_big_endian_sha256": "498b8d1fe684b35d825c92b59a4abb5ad44e8757089443c54b756cdef3fa3467" + } + }, + "ranks_underpaying": 60, + "ranks_with_gap": 60 + }, + "leaf-pooled": { + "first": null, + "ranks_underpaying": 0, + "ranks_with_gap": 0 + }, + "occurrences": { + "first": { + "cut": [ + 3, + 1, + 48, + 288, + 270, + 23258363138136000 + ], + "cut_multiplier": { + "bits": 2815, + "unsigned_big_endian_sha256": "b0004eb49ceac61bb68a9349a6aa500abd73ad273cb1343150bb657951235aff" + }, + "failing_cuts": 2, + "height": 4, + "n": 726, + "pooled_multiplier": { + "bits": 2805, + "unsigned_big_endian_sha256": "34c1e6c4f900dbe0719d913a840f2fce070853956a9bf4a46c9273fd42df8509" + }, + "pooled_remainder": { + "bits": 535, + "unsigned_big_endian_sha256": "d34d252434b4f6854b2692c1ba3d3008ffd18976829ee636b80414b6a77352a2" + }, + "width": { + "bits": 535, + "unsigned_big_endian_sha256": "498b8d1fe684b35d825c92b59a4abb5ad44e8757089443c54b756cdef3fa3467" + } + }, + "ranks_underpaying": 60, + "ranks_with_gap": 60 + } + }, + "record_sha256": "a092230468c3c41a4a0dfecf79d8109f8b45e5fefda152377095d0164da6bf04", + "rule": [ + "adaptive", + 2, + 1, + 1 + ], + "strict_width_gains": 1088, + "targets": { + "121": 224, + "25": 448, + "41": 448, + "5": 420, + "57": 448, + "6": 270, + "7": 840, + "8": 1395, + "9": 3195 + }, + "width": { + "bits": 5450, + "unsigned_big_endian_sha256": "206c746e5204d6543fbbaa6896c9d02874ebe2f477d2d787a286a190f51c04b0" + } + }, + { + "batch_constraints": 87604, + "compiled_ranks": 1089, + "cuts": 48642, + "leaves": { + "bits": 4532, + "unsigned_big_endian_sha256": "f1004041f7bef8040ab183c01e305fabb1d19a73a5961d89ece13169d5b549fb" + }, + "maximum": 1209, + "name": "p7-four-base-height", + "nested_leaves": { + "bits": 36648, + "unsigned_big_endian_sha256": "0ac4fbe185f594091f868f8b6272730df6eae75d9b3e9285db19b77e3f9b1db2" + }, + "nested_width": { + "bits": 36637, + "unsigned_big_endian_sha256": "6c4e3698210556dabc7ff01bfdde0c50187af3b0d8420501d22a6440dfae0619" + }, + "normalized_leaf_cost_unchanged": true, + "paid": { + "1": 37305, + "16": 448, + "2": 10695, + "3": 3360, + "32": 448, + "4": 1530, + "48": 448, + "5": 300, + "8": 1464 + }, + "pooling_gaps": { + "aggregate": { + "first": null, + "ranks_underpaying": 0, + "ranks_with_gap": 0 + }, + "leaf-pooled": { + "first": null, + "ranks_underpaying": 0, + "ranks_with_gap": 0 + }, + "occurrences": { + "first": null, + "ranks_underpaying": 0, + "ranks_with_gap": 0 + } + }, + "record_sha256": "45948ac366e1bf992431380fdc576f73f8acb00b7a4c2205012634a4ca3610aa", + "rule": [ + "adaptive", + 4, + 1, + 1 + ], + "strict_width_gains": 1088, + "targets": { + "121": 224, + "25": 448, + "41": 448, + "5": 420, + "57": 448, + "6": 270, + "7": 840, + "8": 1395, + "9": 3195 + }, + "width": { + "bits": 4522, + "unsigned_big_endian_sha256": "9d61f7fc5a6ec0774c43bc6846181fd3e83cf38e2051295bfb6f931ec3305dad" + } + } + ], + "no_convergence_or_native_admission_claim": true, + "no_new_kappa": true, + "real_profile_census": [ + { + "cuts": 9, + "empty_parent_feeds": 0, + "empty_root": false, + "height": 0, + "n": 121, + "sources": 7688 + }, + { + "cuts": 9, + "empty_parent_feeds": 0, + "empty_root": false, + "height": 0, + "n": 30975, + "sources": 7688 + }, + { + "cuts": 317, + "empty_parent_feeds": 0, + "empty_root": false, + "height": 2, + "n": 30976, + "sources": 1659179037440 + }, + { + "cuts": 317, + "empty_parent_feeds": 0, + "empty_root": false, + "height": 2, + "n": 31000, + "sources": 1659179037440 + }, + { + "cuts": 331, + "empty_parent_feeds": 0, + "empty_root": false, + "height": 2, + "n": 60000, + "sources": 960696476160 + }, + { + "cuts": 9, + "empty_parent_feeds": 0, + "empty_root": false, + "height": 0, + "n": 121, + "sources": 7688 + }, + { + "cuts": 9, + "empty_parent_feeds": 0, + "empty_root": false, + "height": 0, + "n": 241, + "sources": 7688 + }, + { + "cuts": 18, + "empty_parent_feeds": 2189616975, + "empty_root": true, + "height": 2, + "n": 242, + "sources": 16833775303800 + }, + { + "cuts": 27, + "empty_parent_feeds": 2440306575, + "empty_root": true, + "height": 2, + "n": 363, + "sources": 18761076948600 + }, + { + "cuts": 36, + "empty_parent_feeds": 6128264498095996875, + "empty_root": true, + "height": 4, + "n": 484, + "sources": { + "bits": 76, + "unsigned_big_endian_sha256": "6b59df0f93b099042063abbbc975aabe06ab4ad2e7c3eefd3b61f1f59c45e9df" + } + }, + { + "cuts": 87, + "empty_parent_feeds": { + "bits": 94, + "unsigned_big_endian_sha256": "475cd2d17c48bf66d40fdb621bf72d70fc1a4d91e6025ff5b04984c861f5de9d" + }, + "empty_root": true, + "height": 6, + "n": 1209, + "sources": { + "bits": 107, + "unsigned_big_endian_sha256": "0ff4965ced077c32a5ddad8de19ae92f0358b4b60c5d3193c133e6734285c1b1" + } + } + ], + "rejected_controls": [ + "boolean batch count", + "boolean multiplier", + "census fault drop-boundary versus ledger", + "census fault drop-boundary versus literal oracle", + "census fault drop-empty-parent versus literal oracle", + "census fault drop-leaf versus ledger", + "census fault drop-leaf versus literal oracle", + "census fault ignore-path-multiplier versus literal oracle", + "false root credit", + "false unit column", + "future rank", + "missing cut", + "multiplier missing a prime factor", + "non-integer multiplicity", + "omitted repeated-occurrence leaf cost", + "paid rank equal to target maximum", + "pooling aggregate (overlap-two-bit n=10)", + "pooling leaf-pooled (repeat-two-bit n=12)", + "pooling occurrences (overlap-two-bit n=10)", + "split target-product collision", + "suppressed empty class versus source Flow", + "tampered flow bytes rejected before execution", + "zero batch count", + "zero multiplier", + "zero width" + ], + "schema": "adaptive-chronological-batching/v1", + "small_table_overlap_two_bit": [ + { + "height": 0, + "leaves": 9, + "multiplier": 1, + "n": 5, + "nested_width": 2, + "sources": 2, + "width": 2 + }, + { + "height": 0, + "leaves": 11, + "multiplier": 1, + "n": 6, + "nested_width": 4, + "sources": 2, + "width": 2 + }, + { + "height": 0, + "leaves": 25, + "multiplier": 2, + "n": 7, + "nested_width": 8, + "sources": 2, + "width": 4 + }, + { + "height": 0, + "leaves": 29, + "multiplier": 2, + "n": 8, + "nested_width": 16, + "sources": 2, + "width": 4 + }, + { + "height": 0, + "leaves": 65, + "multiplier": 4, + "n": 9, + "nested_width": 32, + "sources": 2, + "width": 8 + }, + { + "height": 2, + "leaves": 270, + "multiplier": 4, + "n": 10, + "nested_width": 256, + "sources": 8, + "width": 32 + }, + { + "height": 2, + "leaves": 300, + "multiplier": 4, + "n": 11, + "nested_width": 2048, + "sources": 8, + "width": 32 + }, + { + "height": 2, + "leaves": 328, + "multiplier": 4, + "n": 12, + "nested_width": 16384, + "sources": 8, + "width": 32 + }, + { + "height": 2, + "leaves": 359, + "multiplier": 4, + "n": 13, + "nested_width": 131072, + "sources": 8, + "width": 32 + }, + { + "height": 2, + "leaves": 1534, + "multiplier": 16, + "n": 14, + "nested_width": 1048576, + "sources": 8, + "width": 128 + }, + { + "height": 2, + "leaves": 1600, + "multiplier": 16, + "n": 15, + "nested_width": 8388608, + "sources": 8, + "width": 128 + }, + { + "height": 2, + "leaves": 1720, + "multiplier": 16, + "n": 16, + "nested_width": 67108864, + "sources": 8, + "width": 128 + }, + { + "height": 2, + "leaves": 1831, + "multiplier": 16, + "n": 17, + "nested_width": 536870912, + "sources": 8, + "width": 128 + }, + { + "height": 2, + "leaves": 7798, + "multiplier": 64, + "n": 18, + "nested_width": 4294967296, + "sources": 8, + "width": 512 + }, + { + "height": 2, + "leaves": 8172, + "multiplier": 64, + "n": 19, + "nested_width": 34359738368, + "sources": 8, + "width": 512 + }, + { + "height": 4, + "leaves": 177952, + "multiplier": 128, + "n": 20, + "nested_width": 3023656976384, + "sources": 88, + "width": 11264 + }, + { + "height": 4, + "leaves": 188912, + "multiplier": 128, + "n": 21, + "nested_width": 266081813921792, + "sources": 88, + "width": 11264 + }, + { + "height": 4, + "leaves": 198936, + "multiplier": 128, + "n": 22, + "nested_width": 23415199625117696, + "sources": 88, + "width": 11264 + }, + { + "height": 4, + "leaves": 208280, + "multiplier": 128, + "n": 23, + "nested_width": 2060537567010357248, + "sources": 88, + "width": 11264 + }, + { + "height": 4, + "leaves": 218528, + "multiplier": 128, + "n": 24, + "nested_width": { + "bits": 68, + "unsigned_big_endian_sha256": "4209ab04c539a62a4024dc39d840236a47a62ff2a251ca17107aff10b9251a80" + }, + "sources": 88, + "width": 11264 + }, + { + "height": 4, + "leaves": 199972, + "multiplier": 128, + "n": 25, + "nested_width": { + "bits": 74, + "unsigned_big_endian_sha256": "962cc6f6c09712c61dda0878f0c9cafae8ba2d41e70c7cfcfdb3e508def75673" + }, + "sources": 80, + "width": 10240 + }, + { + "height": 4, + "leaves": 209818, + "multiplier": 128, + "n": 26, + "nested_width": { + "bits": 80, + "unsigned_big_endian_sha256": "7257b84d2e071a1b84feb7fffceb69bd44a995dd9c2e72594ddd305e58674407" + }, + "sources": 80, + "width": 10240 + }, + { + "height": 4, + "leaves": 217924, + "multiplier": 128, + "n": 27, + "nested_width": { + "bits": 87, + "unsigned_big_endian_sha256": "900188b7e9b15b9ecb0e2a60ee2b44cf307572b3b7c41d0d022791958a4045d4" + }, + "sources": 80, + "width": 10240 + }, + { + "height": 4, + "leaves": 4924592, + "multiplier": 2816, + "n": 28, + "nested_width": { + "bits": 93, + "unsigned_big_endian_sha256": "4f5535adc5e810fe7e12c0b1593bf10c2d8aa5cc10bd708c22a1cd6fe496a069" + }, + "sources": 80, + "width": 225280 + } + ], + "source_sha256": { + "research/chronological-batch-width/README.md": "0cf276c77016a98a0dabba822d27bb9cb94c0bf86ec353a16499fe85e6032c20", + "research/chronological-batch-width/batches.py": "73e7ab4a1925ee7d412d0f2b5d28b70f3a9e43e427c2ec6f6d89f193b84655ef", + "research/compact-joint-compiler/arithmetic/RESULT.json": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091", + "research/direct-mixed-flow/flow.py": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a", + "research/higher-moment-strictification/RESULT.json": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156", + "research/native-lattice-retiming/RESULT.json": "1ac2e581ea51e6448503a68caf4bf44aeb32470c2e2674c91f007af4a3abd2e3", + "research/rank-convergence/BENCHMARKS.json": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850", + "research/rank-convergence/PROOF.md": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376", + "research/rank-convergence/flow.py": "daad9e8e122e0521e0509cd5d36dca16eb5156289f1a77d19a85aa2020f4da8f" + } +} diff --git a/research/adaptive-chronological-batching/SOURCES.json b/research/adaptive-chronological-batching/SOURCES.json new file mode 100644 index 0000000000..9af428528f --- /dev/null +++ b/research/adaptive-chronological-batching/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/chronological-batch-width/README.md", + "usage": "input", + "git_blob": "c85304a601f858774f425d5f3869ac0a6f85ec29", + "sha256": "0cf276c77016a98a0dabba822d27bb9cb94c0bf86ec353a16499fe85e6032c20" + }, + { + "path": "research/chronological-batch-width/batches.py", + "usage": "input", + "git_blob": "98feaef4156223829971089765bd483518c3b754", + "sha256": "73e7ab4a1925ee7d412d0f2b5d28b70f3a9e43e427c2ec6f6d89f193b84655ef" + }, + { + "path": "research/compact-joint-compiler/arithmetic/RESULT.json", + "usage": "input", + "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff", + "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091" + }, + { + "path": "research/direct-mixed-flow/flow.py", + "usage": "input", + "git_blob": "07175cd6e1f2c2367c2e78eca7f163fef18d301d", + "sha256": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a" + }, + { + "path": "research/higher-moment-strictification/RESULT.json", + "usage": "input", + "git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a", + "sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156" + }, + { + "path": "research/native-lattice-retiming/RESULT.json", + "usage": "input", + "git_blob": "93defc5ececebd542332fc42d6a78f0af222cd1c", + "sha256": "1ac2e581ea51e6448503a68caf4bf44aeb32470c2e2674c91f007af4a3abd2e3" + }, + { + "path": "research/rank-convergence/BENCHMARKS.json", + "usage": "input", + "git_blob": "bc58c96abda014c28de91eca3ff10a7d4ec30b32", + "sha256": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850" + }, + { + "path": "research/rank-convergence/PROOF.md", + "usage": "input", + "git_blob": "75f451837204bd141f357e7f5e5d6c6f42e1423e", + "sha256": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376" + }, + { + "path": "research/rank-convergence/flow.py", + "usage": "input", + "git_blob": "7f5198a5d4ca0aaf508e8e47faa10dd75bf20980", + "sha256": "daad9e8e122e0521e0509cd5d36dca16eb5156289f1a77d19a85aa2020f4da8f" + } + ] +} diff --git a/research/adaptive-chronological-batching/TASK.json b/research/adaptive-chronological-batching/TASK.json new file mode 100644 index 0000000000..5734f2e4ce --- /dev/null +++ b/research/adaptive-chronological-batching/TASK.json @@ -0,0 +1,120 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "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": "Adaptive part of one combined width contribution: certify per-cut divisibility and unchanged normalized leaf cost of PR #4507's chronological batching for PR #4483's arbitrary-height forests, with an independent literal ordered-word/paid-path oracle, closed-form cut formulas, authenticated source Flow comparison, semantic controls and a conditional all-rank width envelope (WIDTH.md). The companion chronological-width-bound package separately sharpens #4586's default logarithmic degree from d+2 to d+1 through bounded per-plateau visits.", + "scope_change_reason": "Originally take #4507 open question 2 after overlap review instead of the independent-moment card; consolidate with the preserved default package into one PR, not duplicate theorem submissions. #4483 covers arbitrary-height aggregate flow, #4519/#4588 independently check default finite widths, #4521 counts the expanded compiler, #4586 already proves default quasipolynomial growth, and #4591 checks arbitrary-height aggregate identities rather than actual cut divisibility. None of those inherited results is claimed as new.", + "bottleneck_link": "A constructive finite compiler at adaptive heights needs every suspended chronological cut to be a whole number of supplier invocations; aggregate histograms hide infeasible cuts. Side result: no exponent, kappa or native admission changes.", + "budget_minutes": 150, + "stop_rule": "One transfer theorem with its proof, one literal-oracle replay over bounded toy flows, toy and pinned-p7 least-width compilations, semantic controls, and the conditional width envelope with pinned p7/native4453/p16 geometry probes; stop before native admission, convergence claims or a tighter all-rank valuation analysis.", + "outcome": "completed", + "evidence": "Direct isolated verify.py passed: 405 census fixtures, 19089 literal oracle classes, 2304 brute-force minimality cases, 186476 chronological constraints in six compilations and 25 controls. Final width_bound.py passed four finite compilations with 13377 constraints, three pinned profile applications and two controls, including a zero-visit level. RESULT.json and WIDTH-RESULT.json preserve exact receipts; WIDTH.md gives the symbolic all-rank proof. Separate different-family reviews and optimized replays passed for both implementations. No human or proof-kernel acceptance.", + "author": "codyw912, with substantial OpenAI assistance; builds on Mihir Srivastava's #4507, zxv's #4436/#4483 and Jacob Alan Sussman's integer compiler", + "ai_assistance": "Substantial AI assistance in code, proofs and writing: Anthropic implementation of the cut compiler, OpenAI implementation of the width witnesses and coordination, independent Anthropic mathematical challenge supplying the level-run proof, OpenAI cut-compiler review/replay and Anthropic width-proof/implementation review/replay. No human or proof-kernel verification is claimed.", + "coordination": { + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4503", + "companion_package": "research/chronological-width-bound", + "publication": "LOCAL-ONLY; one combined PR with two scoped replay packages pending publication approval", + "consolidation_main_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "selection_context": "Historical base/card/pins unchanged; live comparison selected conditional kappa .00302015 from #4470, not #4483 or #4507. No selected-frontier edit.", + "consolidation_overlap_coverage": "2026-10-22: 408 open PRs at 13:08:38UTC, 3852 closed PRs at 13:09:39UTC, 3577 Discussion records at 13:09:11UTC; complete reported pagination, non-atomic snapshot, not exhaustive novelty proof.", + "nearest_overlap": [ + "PR4586 aadb7bc59390683450b1969e4632f546929dc569: default d+2 proof; companion sharpens to d+1", + "PR4588 2f6578907b7f8718a13921552cc3069d3908e936: independent finite default checks", + "PR4591 84c0fb3a39bcb1e4b8c48892bfdd8a6e7ae58a50: arbitrary-height aggregate identities, not actual cut divisibility" + ], + "specialization_boundary": "Symbolic M=k0,g=1 gives d'=d,z=0; named adaptive interface requires positive a,b and g=a+b>=2. Direct-g finite witnesses are separate, not an all-rank default specialization replay. WIDTH.md assumes paid rank one; the default companion proves root nonemptiness without it. Plateau-product and level-LCM divisors differ; no universal numerical dominance." + }, + "open_questions": [ + { + "question": "Do the retuned geometries (for example PR #4533 height base 768 for p16) keep the same per-cut divisibility and width envelope?", + "why_it_matters": "The application probes bind only the BENCHMARKS height bases; a retuned M changes the forest and its cut inventory.", + "first_step": "Add the retuned (M, g) rows to the geometry probes of width_bound.py with an authenticated profile pin and compare each cap against the source Flow.", + "blocked_by": "A pinned retuned profile and its authenticated source bytes." + }, + { + "question": "Can the all-rank width envelope be tightened with actual gcd savings or narrower semigroup counts?", + "why_it_matters": "WIDTH.md bounds log B_N only from above and cannot compare against any nested-width lower bound.", + "first_step": "Compute the exact prime-valuation recurrence at selected pinned p7 ranks, then derive a symbolic inequality retaining gcd cancellation; finite fits alone are not an asymptotic proof.", + "blocked_by": "Cost of exact large-rank compilation; an eventual source-count lower bound is needed for any exponential-versus-subexponential comparison." + } + ] +} diff --git a/research/adaptive-chronological-batching/VERIFY.json b/research/adaptive-chronological-batching/VERIFY.json new file mode 100644 index 0000000000..ef840ed004 --- /dev/null +++ b/research/adaptive-chronological-batching/VERIFY.json @@ -0,0 +1,58 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/chronological-batch-width/README.md", + "research/chronological-batch-width/batches.py", + "research/compact-joint-compiler/arithmetic/RESULT.json", + "research/direct-mixed-flow/flow.py", + "research/higher-moment-strictification/RESULT.json", + "research/native-lattice-retiming/RESULT.json", + "research/rank-convergence/BENCHMARKS.json", + "research/rank-convergence/PROOF.md", + "research/rank-convergence/flow.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Authenticate #4483 Flow bytes, compare independent per-cut census with literal ordered-word oracle, closed-form cut formulas and source Flow, compile least widths/costs for toy and pinned p7 height rules, and reject pooled/missing-class/missing-boundary/bad-multiplier controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same replay with assertions disabled; every check uses explicit exceptions." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/width_bound.py" + ], + "timeout_seconds": 120, + "checks": "Integer decrement, source-count, semigroup plateau, level-run chain and all-prime divisor witnesses on four toy compilations; source-bound p7/native4453/p16 boundary census and edge-decrement checks only. The all-rank statement is the symbolic theorem in WIDTH.md, not an all-rank raw-profile execution or native-admission claim." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/width_bound.py" + ], + "timeout_seconds": 120, + "checks": "The same width-bound replay in isolated mode with assertions disabled." + } + ] +} diff --git a/research/adaptive-chronological-batching/WIDTH-RESULT.json b/research/adaptive-chronological-batching/WIDTH-RESULT.json new file mode 100644 index 0000000000..1326fac9ac --- /dev/null +++ b/research/adaptive-chronological-batching/WIDTH-RESULT.json @@ -0,0 +1,547 @@ +{ + "boundary_controls": [ + "omitted_height_generator", + "false_default_root_contraction" + ], + "claim": "Symbolic all-rank theorem in WIDTH.md; finite integer witnesses here", + "finite_compilations": [ + { + "M": 3, + "all_rank_integer_divisibility": true, + "bit_envelope": 2076, + "constraints": 3705, + "divisor": { + "bits": 349, + "unsigned_big_endian_sha256": "acc4026d2fd4e41acd40cab3a6f33fbe9929de03874bc936223c8838720185e5" + }, + "final_width": { + "bits": 118, + "unsigned_big_endian_sha256": "ee7e586fe743910903929eaf24e2887876adcafd0d01d8416b66d3bbab339c4e" + }, + "g": 1, + "levels": [ + { + "decrement": 1, + "high": 14, + "level": 0, + "low": 5, + "observed_visits": 5, + "plateaus": 2, + "visit_bound": 10 + }, + { + "decrement": 3, + "high": 44, + "level": 1, + "low": 15, + "observed_visits": 8, + "plateaus": 5, + "visit_bound": 10 + }, + { + "decrement": 8, + "high": 134, + "level": 2, + "low": 45, + "observed_visits": 12, + "plateaus": 9, + "visit_bound": 12 + }, + { + "decrement": 16, + "high": 300, + "level": 3, + "low": 135, + "observed_visits": 11, + "plateaus": 10, + "visit_bound": 11 + } + ], + "maximum": 300, + "maximum_chain_depth": 33, + "name": "new-height-prime", + "observed_census_changes": 13, + "ordinary_cutoff": 5, + "paid": { + "1": 2, + "4": 1 + }, + "plateaus": 26, + "prime_box": 72, + "rank_and_height_primes": [ + 2, + 3, + 5 + ], + "regime": "subexponential", + "targets": { + "2": 1, + "5": 1 + } + }, + { + "M": 4, + "all_rank_integer_divisibility": true, + "bit_envelope": 1542, + "constraints": 4389, + "divisor": { + "bits": 551, + "unsigned_big_endian_sha256": "307939131d100cb6363f662ad719bd5b5b818f06c20b2926512d992bc4b2d7f0" + }, + "final_width": { + "bits": 87, + "unsigned_big_endian_sha256": "a40492b112ead48b7b2944085b3878eab084022db978aa29f67c28099303023a" + }, + "g": 2, + "levels": [ + { + "decrement": 1, + "high": 19, + "level": 0, + "low": 5, + "observed_visits": 8, + "plateaus": 2, + "visit_bound": 15 + }, + { + "decrement": 4, + "high": 79, + "level": 1, + "low": 20, + "observed_visits": 8, + "plateaus": 4, + "visit_bound": 15 + }, + { + "decrement": 16, + "high": 300, + "level": 2, + "low": 80, + "observed_visits": 8, + "plateaus": 6, + "visit_bound": 14 + } + ], + "maximum": 300, + "maximum_chain_depth": 22, + "name": "quasipolynomial-boundary", + "observed_census_changes": 11, + "ordinary_cutoff": 5, + "paid": { + "1": 2, + "4": 1 + }, + "plateaus": 12, + "prime_box": 18, + "rank_and_height_primes": [ + 2, + 5 + ], + "regime": "quasipolynomial", + "targets": { + "2": 1, + "5": 1 + } + }, + { + "M": 2, + "all_rank_integer_divisibility": true, + "bit_envelope": 1080, + "constraints": 1795, + "divisor": { + "bits": 342, + "unsigned_big_endian_sha256": "3021febfe37b96c3746612a86ed9aa09b98baf8f5fce003aaf1a4c2fc7cfefb2" + }, + "final_width": { + "bits": 97, + "unsigned_big_endian_sha256": "c7b5072940cb4fdda884e6c96d1c17ec8f9778026265c039339a222732c6d841" + }, + "g": 3, + "levels": [ + { + "decrement": 1, + "high": 9, + "level": 0, + "low": 5, + "observed_visits": 3, + "plateaus": 1, + "visit_bound": 5 + }, + { + "decrement": 2, + "high": 19, + "level": 1, + "low": 10, + "observed_visits": 3, + "plateaus": 1, + "visit_bound": 5 + }, + { + "decrement": 4, + "high": 39, + "level": 2, + "low": 20, + "observed_visits": 3, + "plateaus": 2, + "visit_bound": 5 + }, + { + "decrement": 8, + "high": 79, + "level": 3, + "low": 40, + "observed_visits": 3, + "plateaus": 2, + "visit_bound": 5 + }, + { + "decrement": 16, + "high": 150, + "level": 4, + "low": 80, + "observed_visits": 3, + "plateaus": 3, + "visit_bound": 5 + } + ], + "maximum": 150, + "maximum_chain_depth": 13, + "name": "empty-root-components", + "observed_census_changes": 9, + "ordinary_cutoff": 5, + "paid": { + "1": 2, + "4": 1 + }, + "plateaus": 9, + "prime_box": 15, + "rank_and_height_primes": [ + 2, + 5 + ], + "regime": "quasipolynomial", + "targets": { + "2": 1, + "5": 1 + } + }, + { + "M": 7, + "all_rank_integer_divisibility": true, + "bit_envelope": 2800, + "constraints": 3488, + "divisor": { + "bits": 560, + "unsigned_big_endian_sha256": "b51d8a27b4ae54dffa3abe2d0f9c4301c1316794af688b0d4ae7157473898c53" + }, + "final_width": { + "bits": 139, + "unsigned_big_endian_sha256": "9cbb7e4bc7bca0eba6e703c6d7ed07aee49690e4861b71fe3e85ee7649849fad" + }, + "g": 2, + "levels": [ + { + "decrement": 1, + "high": 55, + "level": 0, + "low": 56, + "observed_visits": 0, + "plateaus": 4, + "visit_bound": 0 + }, + { + "decrement": 7, + "high": 300, + "level": 1, + "low": 56, + "observed_visits": 31, + "plateaus": 10, + "visit_bound": 35 + } + ], + "maximum": 300, + "maximum_chain_depth": 31, + "name": "collisions-and-larger-base", + "observed_census_changes": 8, + "ordinary_cutoff": 56, + "paid": { + "1": 1, + "5": 1 + }, + "plateaus": 14, + "prime_box": 36, + "rank_and_height_primes": [ + 2, + 5, + 7 + ], + "regime": "subexponential", + "targets": { + "2": 1, + "4": 1, + "8": 1 + } + } + ], + "no_new_kappa": true, + "profile_applications": [ + { + "M": 256, + "boundary_probes": [ + { + "cap": 1, + "checked_batch_rows": 36, + "height": 0, + "root_minimum": 5, + "source_types": 9, + "sources": 7688 + }, + { + "cap": 2, + "checked_batch_rows": 36, + "height": 0, + "root_minimum": 5, + "source_types": 9, + "sources": 7688 + }, + { + "cap": 5, + "checked_batch_rows": 36, + "height": 0, + "root_minimum": 5, + "source_types": 9, + "sources": 7688 + }, + { + "cap": 255, + "checked_batch_rows": 36, + "height": 0, + "root_minimum": 5, + "source_types": 9, + "sources": 7688 + }, + { + "cap": 256, + "checked_batch_rows": 1146, + "height": 2, + "root_minimum": 125, + "source_types": 256, + "sources": 1659179037440 + }, + { + "cap": 257, + "checked_batch_rows": 1146, + "height": 2, + "root_minimum": 125, + "source_types": 256, + "sources": 1659179037440 + }, + { + "cap": 512, + "checked_batch_rows": 1156, + "height": 2, + "root_minimum": 125, + "source_types": 249, + "sources": 961235968512 + }, + { + "cap": 65535, + "checked_batch_rows": 924, + "height": 2, + "root_minimum": 125, + "source_types": 165, + "sources": 454401884672 + }, + { + "cap": 65536, + "checked_batch_rows": 11376, + "height": 4, + "root_minimum": 3125, + "source_types": 2163, + "sources": 127879181882927792384 + } + ], + "exponent": "1-log_256(25)", + "g": 2, + "k0": 5, + "m": 121, + "profile": "p7" + }, + { + "M": 1024, + "boundary_probes": [ + { + "cap": 1, + "checked_batch_rows": 56, + "height": 0, + "root_minimum": 4, + "source_types": 14, + "sources": 11560 + }, + { + "cap": 2, + "checked_batch_rows": 56, + "height": 0, + "root_minimum": 4, + "source_types": 14, + "sources": 11560 + }, + { + "cap": 4, + "checked_batch_rows": 56, + "height": 0, + "root_minimum": 4, + "source_types": 14, + "sources": 11560 + }, + { + "cap": 1023, + "checked_batch_rows": 56, + "height": 0, + "root_minimum": 4, + "source_types": 14, + "sources": 11560 + }, + { + "cap": 1024, + "checked_batch_rows": 4192, + "height": 2, + "root_minimum": 64, + "source_types": 841, + "sources": 3061480776192 + }, + { + "cap": 1025, + "checked_batch_rows": 4204, + "height": 2, + "root_minimum": 64, + "source_types": 841, + "sources": 3039213470208 + }, + { + "cap": 2048, + "checked_batch_rows": 4208, + "height": 2, + "root_minimum": 64, + "source_types": 869, + "sources": 2331386723840 + }, + { + "cap": 1048575, + "checked_batch_rows": 3074, + "height": 2, + "root_minimum": 64, + "source_types": 557, + "sources": 1544804416000 + }, + { + "cap": 1048576, + "checked_batch_rows": 105810, + "height": 4, + "root_minimum": 1024, + "source_types": 16357, + "sources": 340739254901836627968 + } + ], + "exponent": "3/5", + "g": 2, + "k0": 4, + "m": 153, + "profile": "native4453" + }, + { + "M": 1024, + "boundary_probes": [ + { + "cap": 1, + "checked_batch_rows": 54, + "height": 0, + "root_minimum": 4, + "source_types": 13, + "sources": 10928 + }, + { + "cap": 2, + "checked_batch_rows": 54, + "height": 0, + "root_minimum": 4, + "source_types": 13, + "sources": 10928 + }, + { + "cap": 4, + "checked_batch_rows": 54, + "height": 0, + "root_minimum": 4, + "source_types": 13, + "sources": 10928 + }, + { + "cap": 1023, + "checked_batch_rows": 54, + "height": 0, + "root_minimum": 4, + "source_types": 13, + "sources": 10928 + }, + { + "cap": 1024, + "checked_batch_rows": 3926, + "height": 2, + "root_minimum": 64, + "source_types": 801, + "sources": 2523156594176 + }, + { + "cap": 1025, + "checked_batch_rows": 3934, + "height": 2, + "root_minimum": 64, + "source_types": 799, + "sources": 2502413434368 + }, + { + "cap": 2048, + "checked_batch_rows": 3962, + "height": 2, + "root_minimum": 64, + "source_types": 804, + "sources": 1898704285696 + }, + { + "cap": 1048575, + "checked_batch_rows": 2870, + "height": 2, + "root_minimum": 64, + "source_types": 455, + "sources": 1305034698752 + }, + { + "cap": 1048576, + "checked_batch_rows": 92068, + "height": 4, + "root_minimum": 1024, + "source_types": 16022, + "sources": 243080258566155304960 + } + ], + "exponent": "3/5", + "g": 2, + "k0": 4, + "m": 145, + "profile": "p16" + } + ], + "schema": "adaptive-width-bound/v1", + "source_sha256": { + "research/chronological-batch-width/README.md": "0cf276c77016a98a0dabba822d27bb9cb94c0bf86ec353a16499fe85e6032c20", + "research/chronological-batch-width/batches.py": "73e7ab4a1925ee7d412d0f2b5d28b70f3a9e43e427c2ec6f6d89f193b84655ef", + "research/compact-joint-compiler/arithmetic/RESULT.json": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091", + "research/direct-mixed-flow/flow.py": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a", + "research/higher-moment-strictification/RESULT.json": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156", + "research/native-lattice-retiming/RESULT.json": "1ac2e581ea51e6448503a68caf4bf44aeb32470c2e2674c91f007af4a3abd2e3", + "research/rank-convergence/BENCHMARKS.json": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850", + "research/rank-convergence/PROOF.md": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376", + "research/rank-convergence/flow.py": "daad9e8e122e0521e0509cd5d36dca16eb5156289f1a77d19a85aa2020f4da8f" + } +} diff --git a/research/adaptive-chronological-batching/WIDTH.md b/research/adaptive-chronological-batching/WIDTH.md new file mode 100644 index 0000000000..4c637ac896 --- /dev/null +++ b/research/adaptive-chronological-batching/WIDTH.md @@ -0,0 +1,262 @@ +# Uniform width bounds for the adaptive chronological compiler + +This is a **conditional all-rank width theorem**, not an extrapolation from a +finite scan. It uses this package's arbitrary-height cut inventory and the +least-LCM batching policy of Mihir Srivastava's +[PR #4507](https://github.com/CrocSwap/integer-mult-bounds/pull/4507). +The flow and adaptive height are zxv's +[PR #4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483), extending +Jacob Alan Sussman's integer compiler. Native semantics and the actual order +of individual paid positions remain premises. + +For fixed height parameters `M >= 2`, `g >= 1`, put + +```text +k0 = min(target ranks), m = max(target ranks), +z = max(0, 1 - g log_M(k0)). +``` + +The least widths satisfy + +\[ +\boxed{\log B_N=O\!\left(N^z(\log N)^{d'+1}\right)}, +\] + +where `d'` counts distinct primes dividing any target rank, paid rank **or M**. +When `k0^g >= M` this is quasipolynomial. Otherwise `0 < z < 1`, so it is +subexponential. The constants depend on the fixed native rule, `M` and `g`. +This is an upper bound, not a tight growth rate, optimal batching theorem, +leaf-cost improvement, physical cost bound or new κ. + +This theorem and the +[default-height proof](../chronological-width-bound/README.md) are two +scoped parts of one contribution. The default proof sharpens +[#4586](https://github.com/CrocSwap/integer-mult-bounds/pull/4586) +(`aadb7bc59390683450b1969e4632f546929dc569`) from logarithmic degree +`d+2` to `d+1` via bounded per-plateau visits; it does not originate the +quasipolynomial classification. Independent finite default checks in +[#4588](https://github.com/CrocSwap/integer-mult-bounds/pull/4588) +(`2f6578907b7f8718a13921552cc3069d3908e936`) are complementary. +[#4591](https://github.com/CrocSwap/integer-mult-bounds/pull/4591) +(`84c0fb3a39bcb1e4b8c48892bfdd8a6e7ae58a50`) checks arbitrary-height +aggregate identities, not actual chronological cut divisibility. That +cut-level transfer is proved in this package's README; the new width +bound here applies to its resulting recurrence. + +## 1. Hypotheses and exact recurrence + +Let `W_k` and `P_r` be positive integer multiplicities, with + +```text +2 <= k0 <= k <= m, 1 <= r <= rmax < m. +``` + +Assume a paid rank-one position. This sufficient hypothesis makes every +height-G forest nonempty: the all-rank-one paid path reaches a degree-zero +leaf unit. Every finite forest with a unit has at least one fresh source. +More general rules require their own nonemptiness proof; an empty flow must +not be silently substituted by a productive supplier. +The default companion has a separate root-nonemptiness proof and needs +no paid rank-one position. Thus the theorem as stated here does not +subsume its entire hypothesis domain. + +Let `W = sum W_k`, `P = sum P_r`. Widths are one below any fixed ordinary +cutoff `n0 >= m`. For `n >= n0`, define exactly + +```text +C_n = floor(n/m), +ell(n) = floor(log_M C_n), +G_n = g ell(n). +``` + +**Default specialization versus executable interface.** Formally setting +`M=k0,g=1` gives the default height, `d'=d` (the primes of `k0` already +occur among target ranks), `z=0` and logarithmic degree `d+1`. This is a +symbolic specialization, with the nonemptiness qualification above. The +named `('adaptive', M, a, b)` interface in `batching.py` requires positive +integers `a,b`, so `g=a+b>=2`; no claim is made that this route ran `g=1`. +`width_bound.py` also takes `g` directly for its finite witnesses, including +a `g=1` toy case; that is not an all-rank default specialization replay. + +Instantiate **all** chronological classes of the height-G_n forest, including +later components beneath empty parent classes. Let `S_n > 0` be the source +count and let `(j,q)` range over every upfront complement and separate exit +cut in the policy proved in README.md. Then + +\[ +a_n=\operatorname{lcm}_{(j,q)}\frac{B_j}{\gcd(B_j,q)}, +\qquad B_n=S_na_n. \tag{1} +\] + +Repeated occurrences of a cut do not multiply `q`. The proof below needs only +that every `j` is an actual complement or exit, and that (1) is the policy. +For every prime `p`, without any restriction to the rank-prime alphabet, + +\[ +v_p(B_n)\le v_p(S_n)+\max_{j\text{ invoked at }n}v_p(B_j). \tag{2} +\] + +Strong induction bounds this valuation by a sum of source valuations along +one decreasing recursive rank chain. Different primes can use different +chains; no common maximizing chain is asserted. + +## 2. Every recursive edge has an integer decrement + +All unit columns are at most `C_n`. A paid exit has +`j <= rmax C_n`, hence `n-j >= C_n`. A nonroot source has rank greater than +`n/m`, so its complement decreases the ambient rank by at least `C_n+1`. +A root source, if present, contains `G_n+1` target letters, so its rank is +at least `k0^(G_n+1)`. Thus every recursive child satisfies + +\[ +n-j\ge\delta(n):=\min(C_n,k_0^{G_n+1})\ge1. \tag{3} +\] + +An empty root class imposes no root-source obligation. This is why the +argument remains valid when the default-height fixed-factor contraction +fails. In particular, it does not assume every source exceeds `n/m`. + +For `N >= n0`, put `Lambda = floor(log_M floor(N/m))`. At level `ell`, set + +```text +lo_ell = max(n0, m M^ell), +hi_ell = min(N, m M^(ell+1)-1), +delta_ell = min(M^ell, k0^(g ell+1)), +t_ell = 0 if hi_ell < lo_ell, + 1 + floor((hi_ell-lo_ell)/delta_ell) otherwise. +``` + +Along a descending chain, the nodes at one level are contiguous. Consecutive +nodes of that run drop by at least `delta_ell`; therefore there are at most +`t_ell` nodes at that level. These bounds require integer arithmetic only. + +## 3. Source counts are constant on multiplicative-semigroup plateaus + +Let `Gamma'` be the semigroup generated by the target ranks, the paid ranks +and `M`, including 1. Every eligibility comparison has the form +`rho*c <= C_n`, where `rho*c` is in this semigroup. Height changes occur at +`C_n = M^ell`, also in `Gamma'`. All finite source and cut data are therefore +constant between successive elements of `Gamma'`. Complement ranks `n-s` +are **not** constant, and are not used in this plateau claim. + +Write `S(gamma)` for the source count at plateau start `gamma`. The number +of starts through `C` satisfies + +\[ +J(C)\le\prod_{p\mid M\prod k\prod r} + (1+\lfloor\log_p C\rfloor)=O((\log C)^{d'}). \tag{4} +\] + +This box can contain unattainable products; it is only an upper bound. +The prime factors of `S(gamma)` need not belong to this alphabet. + +At height `G`, the number of units is bounded by + +\[ +U\le\sum_{h=0}^G W^hP^{G-h}\le(W+P)^G. +\] + +The second inequality follows by comparing binomial coefficients; it also +holds at `G=0`. Each unit has `W` target demand slots. Fresh sources are a +subset, so + +\[ +1\le S(\gamma)\le W(W+P)^{g\ell}. \tag{5} +\] + +## 4. Exact divisor and bit envelope + +For each level, let `L_ell` be the LCM of all `S(gamma)` with +`M^ell <= gamma < M^(ell+1)` and `gamma <= floor(N/m)`; an empty LCM is 1. +The levels with `t_ell=0` contribute nothing. Equations (2) and (3), applied +to each prime's chain, prove + +\[ +\boxed{B_n\mid Q_N:=\prod_{\ell=0}^{\Lambda}L_\ell^{t_\ell} + \quad(0\le n\le N).} \tag{6} +\] + +Let `J_ell` count the starts included in `L_ell`. The following is an entirely +integer bit envelope: + +\[ +b_N=\sum_\ell t_\ell J_\ell + \left(\lceil\log_2 W\rceil+g\ell\lceil\log_2(W+P)\rceil\right). +\] + +Then `B_n <= Q_N <= 2^b_N` for every `n <= N`. Computing enormous `Q_N` is +not necessary to use the symbolic theorem. The finite verifier uses exact +integer divisibility on bounded fixtures, rather than sampling a few primes. +The default companion instead uses a product of individual plateau source +counts raised to its constant plateau-visit bound. That divisor and (6) +are different certificates; equal asymptotic order at `M=k0,g=1` does not +establish universal finite numerical dominance of either one. + +## 5. Growth in the two regimes + +If `k0^g >= M`, then `delta_ell=M^ell` and +`t_ell <= m(M-1)`. Equations (4) and (5) immediately give +`log B_N = O((log N)^(d'+1))`. + +Otherwise put `rho=M/k0^g > 1` and `z=log_M rho`. The level lengths obey + +\[ +t_\ell\le 1+m(M-1)+\frac{m(M-1)}{k_0}\rho^\ell. +\] + +Summing the geometric progression gives +`sum t_ell = O(rho^Lambda) = O(N^z)`. Combining this with (4) and (5) +proves the stated subexponential bound. Here `0 < z < 1` because +`k0 >= 2` and `g >= 1`. + +There is no unconditional comparison with an exponential **lower** bound +for adaptive nested widths: that would require an additional eventual +source-count lower bound of two. Finite least-versus-nested comparisons in +RESULT.json remain separate evidence. + +## 6. Source-bound applications and verification scope + +The pinned `rank-convergence/BENCHMARKS.json` fixes `g=witness.a+witness.b=2`: + +| Profile | m | k0 | M | Proven exponent z | +| --- | ---: | ---: | ---: | --- | +| p7 | 121 | 5 | 256 | `1-log_256(25)` | +| native4453 | 153 | 4 | 1024 | `3/5` | +| p16 | 145 | 4 | 1024 | `3/5` | + +All three have paid rank one. The theorem is about these exact raw profiles, +not materialized strictifications. The later +[PR #4533](https://github.com/CrocSwap/integer-mult-bounds/pull/4533) retunes +`M`; its different geometry is not certified by these application receipts. +The theorem allows any *fixed* `M,g`, not parameters depending on `n`. + +`width_bound.py` checks integer decrements, source bounds, semigroup plateaus, +per-level chain-visit bounds and the all-prime divisor on finite toy +compilations. It separately binds the three real geometries and exercises +height boundaries through `M^2`, without materializing their all-rank +compilers. Finite checks exercise the proof's hypotheses and implementations; +they are not a proof of the asymptotic statement. + +The historical base and immutable input pins are unchanged. At the +consolidation comparison main `fbc9ea0249746acca4f504d4fda2b84e0e36cf0d`, +the selected conditional κ is `.00302015` from #4470; #4483/#4507 remain +non-selected research inputs, not an admitted replacement frontier. + +## 7. Remaining obligations and credit + +Correctness of arbitrary-height chronological cuts is established separately +in README.md and the package's literal oracle checks. The full native word, +owned restoration, storage, routing, precision, stock, fixed-tape execution, +analytic transfer and exact recovery are not admitted here. No normalized +leaf exponent, κ, practical threshold or selected result changes. + +A sharper width bound might use actual gcd savings or narrower semigroup +counts. Neither is needed for this result. A concrete next question is +whether these bounds can replace one declared finite-resource envelope at +its actual multiplication caller, with all physical costs still charged. + +Prepared for codyw912 with substantial OpenAI assistance. An independent +Anthropic-model mathematical challenge checked the root/decrement argument +and supplied the sharper integer level-run form and the two growth regimes. +This is AI review, not independent human or proof-kernel verification. +Predecessor attribution above and in README.md remains intact. Apache-2.0. diff --git a/research/adaptive-chronological-batching/batching.py b/research/adaptive-chronological-batching/batching.py new file mode 100755 index 0000000000..0347e94fec --- /dev/null +++ b/research/adaptive-chronological-batching/batching.py @@ -0,0 +1,297 @@ +#!/usr/bin/env python3 +"""Per-cut census and least batch widths for arbitrary-height forests. + +Multiplicative-polynomial implementation of the capped overlapping-rank flow +of zxv's PR #4436 at an explicit integer height G (the arbitrary-height forest +of PR #4483), with the cut-aware batching policy of PR #4507. The integer +Pascal compiler is Jacob Alan Sussman's. This module imports no predecessor +code and no ordered-word enumeration: the checker supplies those oracles. +Prepared with substantial AI assistance. Apache-2.0. +""" +from collections import Counter +from math import gcd, lcm + +# Verification-only fault switches. Production callers pass none. Each models a +# plausible arbitrary-height shortcut that the verifier must reject. +CENSUS_FAULTS = frozenset({ + 'drop-empty-parent', # stop a path whose own class holds no unit + 'drop-boundary', # discard premature exits above the leaf depth + 'drop-leaf', # discard exits at the final depth + 'ignore-path-multiplier', # child eligibility without the paid prefix + 'split-collisions', # keep target-product collisions in separate cuts +}) +POLICIES = ('per-cut', 'aggregate', 'occurrences', 'leaf-pooled') + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def is_count(value): + return type(value) is int and value > 0 + + +def validate(targets, paid, n): + for histogram in (targets, paid): + require(isinstance(histogram, dict) and bool(histogram), 'nonempty histogram') + require(all(is_count(k) and is_count(v) for k, v in histogram.items()), + 'positive integer histogram') + require(type(n) is int and 2 <= min(targets) <= max(targets) <= n + and max(paid) < max(targets), 'strict rank contract') + + +def floor_log(value, base): + require(is_count(value) and type(base) is int and base >= 2, 'integer logarithm') + result = 0 + while value >= base: + value //= base + result += 1 + return result + + +def height(rule, targets, n): + """Integer height: ('default',), ('adaptive', M, a, b) or ('fixed', G).""" + cap = n//max(targets) + kind = rule[0] + if kind == 'default': + return floor_log(cap, min(targets)) + if kind == 'adaptive': + _, base, a, b = rule + require(is_count(a) and is_count(b), 'positive adaptive multipliers') + return (a+b)*floor_log(cap, base) + require(kind == 'fixed' and type(rule[1]) is int and rule[1] >= 0, 'height rule') + return rule[1] + + +def target_layers(targets, cap, depth, split=False): + """F_h: ordered target words of length h by product (or product and letters). + + Distinguishable copies of one rank carry weight W_k. Products above cap are + dropped: all target ranks are at least two, so they never recover. + """ + layers = [{(1, ()): 1}] + for _ in range(depth): + following = Counter() + for (c, tag), count in layers[-1].items(): + for k, copies in targets.items(): + if c*k <= cap: + following[(c*k, tuple(sorted(tag+(k,))) if split else ())] += count*copies + layers.append(dict(following)) + return layers + + +def census(targets, paid, cap, G, faults=frozenset()): + """Every chronological cut of the height-G forest at integer cutoff ``cap``. + + A class is (depth d, path multiplier rho). Its present units are ordered + target words of length G-d with rho*c <= cap. Each unit demands one job per + target letter; the child at paid rank r (multiplier rr=rho*r) accepts those + demands whose tail fits rr. Present parents cover child demand; the excess + leaves as exits of that one cut. Demand with no present parent is a fresh + source. A class keeps spawning children while rr <= cap, even if empty. + """ + require(is_count(cap) and type(G) is int and G >= 0, 'cap and height') + require(faults <= CENSUS_FAULTS, 'known fault switch') + split = 'split-collisions' in faults + layers = target_layers(targets, cap, G, split) + one = (1, ()) + + def supply(depth, rho): + return {key: q for key, q in layers[G-depth].items() if rho*key[0] <= cap} + + def demand(depth, rho): + result = Counter() + for (c, tag), q in supply(depth, rho).items(): + for k, copies in targets.items(): + result[(c*k, tuple(sorted(tag+(k,))) if split else ())] += copies*q + return result + + roots, inner = Counter(), Counter() + for (c, _), q in demand(0, 1).items(): + roots[c] += q + boundary, leaves, columns = Counter(), Counter(), Counter() + cuts, units, matched, empty_feeds = [], 0, 0, 0 + paths = {1: 1} + for depth in range(G+1): + following = Counter() + for rho, occurrences in sorted(paths.items()): + here = supply(depth, rho) + units += occurrences*sum(here.values()) + for (c, _), q in here.items(): + columns[rho*c] += occurrences*q + for r, repeats in sorted(paid.items()): + rr, copies = rho*r, occurrences*repeats + local = Counter() + if depth == G: + if here.get(one, 0): + local[(rr, ())] = here[one] + else: + below = demand(depth+1, rho if 'ignore-path-multiplier' in faults else rr) + for key in here.keys() | below.keys(): + have, want = here.get(key, 0), below.get(key, 0) + require(have == 0 or want <= have, 'present parent covers demand') + matched += copies*min(have, want) + if have > want: + local[(rr*key[0], key[1])] = have-want + elif want > have: + inner[rr*key[0]] += copies*(want-have) + if rr <= cap and not ('drop-empty-parent' in faults and not here): + following[rr] += copies + if not here and rr <= cap and supply(depth+1, rr): + empty_feeds += copies + for (e, tag), q in sorted(local.items()): + if ('drop-leaf' in faults and depth == G) \ + or ('drop-boundary' in faults and depth < G): + continue + cuts.append((depth, rho, r, e, q, copies)) + (leaves if depth == G else boundary)[e] += copies*q + paths = following + roots, inner, boundary, leaves = (+x for x in (roots, inner, boundary, leaves)) + return {'cap': cap, 'height': G, 'roots': roots, 'inner': inner, + 'sources': roots+inner, 'boundary': boundary, 'leaves': leaves, + 'exits': boundary+leaves, 'cuts': cuts, 'columns': +columns, + 'units': units, 'column_mass': sum(z*q for z, q in columns.items()), + 'matched': matched, 'empty_parent_feeds': empty_feeds} + + +def compressed_cuts(flow): + """Occurrences of each (depth, rho, paid rank, exit rank, batch size).""" + result = Counter() + for depth, rho, r, e, count, copies in flow['cuts']: + result[(depth, rho, r, e, count)] += copies + return result + + +def rank_invoice(flow, targets, paid): + """Sources minus exits minus unit targets plus unit paid jobs, by rank.""" + invoice = Counter(flow['sources']) + invoice.subtract(flow['exits']) + for z, count in flow['columns'].items(): + for k, w in targets.items(): + invoice[k*z] -= count*w + for r, w in paid.items(): + invoice[r*z] += count*w + return {rank: v for rank, v in invoice.items() if v} + + +def check_ledger(flow, targets, paid, n): + """Structural obligations of one arbitrary-height flow at ambient rank n.""" + validate(targets, paid, n) + m, rmax = max(targets), max(paid) + require(flow['cap'] == n//m, 'cutoff is floor(n/m)') + for name in ('roots', 'inner', 'sources', 'boundary', 'leaves', 'exits', 'columns'): + require(all(is_count(k) and is_count(v) for k, v in flow[name].items()), + 'positive integer inventory '+name) + require(bool(flow['sources']) and bool(flow['columns']), 'nonempty arbitrary-height flow') + require(flow['sources'] == flow['roots']+flow['inner'], 'root/inner source partition') + require(flow['exits'] == flow['boundary']+flow['leaves'], 'boundary/leaf exit partition') + require(all(1 <= s <= n for s in flow['sources']), 'sources fit the ambient rank') + require(all(m*s > n for s in flow['inner']), 'inner source lower bound') + require(all(1 <= e < n and m*e <= rmax*n for e in flow['exits']), 'strict exit descent') + require(all(m*z <= n for z in flow['columns']), 'unit columns fit cutoff') + require(sum(flow['columns'].values()) == flow['units'], 'unit column count') + cut_exits = Counter() + for _, _, _, e, q, copies in flow['cuts']: + require(is_count(q) and is_count(copies), 'positive cut size and occurrences') + cut_exits[e] += q*copies + require(cut_exits == flow['exits'], 'cut inventory equals exit inventory') + require(not rank_invoice(flow, targets, paid), 'formal rank-invoice cancellation') + return True + + +def batch_rows(flow, n, policy='per-cut'): + """(rank, array count) batches that one unreplicated pass must complete.""" + require(policy in POLICIES, 'known batching policy') + rows = [(n-s, q) for s, q in sorted(flow['sources'].items())] + cuts = flow['cuts'] + if policy == 'per-cut': + rows += [(e, q) for _, _, _, e, q, _ in cuts] + elif policy == 'aggregate': + rows += sorted(flow['exits'].items()) + elif policy == 'occurrences': + rows += [(e, q*copies) for _, _, _, e, q, copies in cuts] + else: + rows += [(e, q) for depth, _, _, e, q, _ in cuts if depth < flow['height']] + rows += sorted(flow['leaves'].items()) + return rows + + +def multiplier(widths, rows): + result = 1 + for rank, count in sorted(set(rows)): + require(type(rank) is int and 0 <= rank < len(widths), 'smaller rank') + require(is_count(count), 'positive batch count') + width = widths[rank] + require(is_count(width), 'positive supplier width') + result = lcm(result, width//gcd(width, count)) + return result + + +def check_rows(widths, rows, replication): + require(is_count(replication), 'positive replication') + for rank, count in rows: + if replication*count % widths[rank]: + raise ValueError('whole chronological batch') + + +def leaf_total(flow, n, widths, leaves, replication, occurrences=True): + """Rank-one leaves of the replicated recursive calls (rank 0 costs 0).""" + total = sum(replication*q//widths[n-s]*leaves[n-s] for s, q in flow['sources'].items()) + for _, _, _, e, q, copies in flow['cuts']: + total += replication*q//widths[e]*leaves[e]*(copies if occurrences else 1) + return total + + +def compile_widths(targets, paid, maximum, rule, occurrence_cost=True): + """Least cut-feasible widths and the nested #4436 widths for one height rule.""" + m = max(targets) + widths, nested = [1]*m, [1]*m + leaves, nested_leaves = list(range(m)), list(range(m)) + records, flows = [], {} + gaps = {p: {'ranks_with_gap': 0, 'ranks_underpaying': 0, 'first': None} + for p in POLICIES if p != 'per-cut'} + for n in range(m, maximum+1): + G = height(rule, targets, n) + if (n//m, G) not in flows: + flows[(n//m, G)] = census(targets, paid, n//m, G) + flow = flows[(n//m, G)] + check_ledger(flow, targets, paid, n) + rows = batch_rows(flow, n) + a = multiplier(widths, rows) + check_rows(widths, rows, a) + count = sum(flow['sources'].values()) + width, old_width = a*count, nested[-1]*count + require(old_width % width == 0, 'least width divides nested width') + check_rows(nested, rows, nested[-1]) + total = leaf_total(flow, n, widths, leaves, a, occurrence_cost) + old_total = leaf_total(flow, n, nested, nested_leaves, nested[-1]) + for policy in gaps: + pooled_rows = batch_rows(flow, n, policy) + pooled = multiplier(widths, pooled_rows) + gaps[policy]['ranks_with_gap'] += pooled != a + # The relaxed policy always satisfies its own rows; the question + # is whether its multiplier also completes every actual cut. + check_rows(widths, pooled_rows, pooled) + failing = [(e, q) for e, q in rows if pooled*q % widths[e]] + if failing: + gaps[policy]['ranks_underpaying'] += 1 + if gaps[policy]['first'] is None: + rank, size = failing[0] + cut = next(c for c in flow['cuts'] if c[3] == rank and c[4] == size) + gaps[policy]['first'] = { + 'n': n, 'height': G, 'pooled_multiplier': pooled, + 'cut_multiplier': a, 'cut': list(cut), 'width': widths[rank], + 'pooled_remainder': pooled*size % widths[rank], + 'failing_cuts': len(failing)} + widths.append(width) + nested.append(old_width) + leaves.append(total) + nested_leaves.append(old_total) + records.append({'n': n, 'height': G, 'multiplier': a, 'sources': count, + 'batches': len(rows), 'cuts': len(flow['cuts']), + 'width': width, 'nested_width': old_width, 'leaves': total, + 'nested_leaves': old_total}) + return {'widths': widths, 'nested': nested, 'leaves': leaves, + 'nested_leaves': nested_leaves, 'records': records, 'gaps': gaps, + 'flows': flows} diff --git a/research/adaptive-chronological-batching/verify.py b/research/adaptive-chronological-batching/verify.py new file mode 100644 index 0000000000..0bcd283333 --- /dev/null +++ b/research/adaptive-chronological-batching/verify.py @@ -0,0 +1,719 @@ +#!/usr/bin/env python3 +"""Exact verifier: per-cut batching on arbitrary-height chronological forests. + +Compares an independent multiplicative-polynomial census (batching.py) with +(i) a literal ordered-word/paid-position oracle written here and (ii) the +frozen #4483 Flow, whose bytes are authenticated before execution. Then it +checks least widths, unchanged normalized leaf cost, pooled-batch failures and +semantic rejection controls. Standard library only; no native admission. + +Prepared with substantial AI assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from fractions import Fraction +from itertools import combinations_with_replacement, product as cartesian +import hashlib +import json +from math import gcd, prod +from pathlib import Path +import sys +import tempfile +from types import ModuleType + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +sys.path.insert(0, str(HERE)) +import batching as B # noqa: E402 +from batching import require # noqa: E402 + +# Executable predecessor bytes are pinned here as well as in SOURCES.json. +EXEC_PINS = { + 'research/rank-convergence/flow.py': + 'daad9e8e122e0521e0509cd5d36dca16eb5156289f1a77d19a85aa2020f4da8f', + 'research/direct-mixed-flow/flow.py': + '460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a', + 'research/chronological-batch-width/batches.py': + '73e7ab4a1925ee7d412d0f2b5d28b70f3a9e43e427c2ec6f6d89f193b84655ef', +} +PROFILE_SOURCE = 'research/higher-moment-strictification/RESULT.json' + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(data): + return json.dumps(data, sort_keys=True, separators=(',', ':')).encode() + + +def integer_record(value): + raw = value.to_bytes(max(1, (value.bit_length()+7)//8), 'big') + return {'bits': value.bit_length(), 'unsigned_big_endian_sha256': digest(raw)} + + +def compact_integers(value, limit=1 << 64): + """Replace every integer above ``limit`` by its bit length and big-endian + SHA256, so receipts digest unlimited integers without decimal strings.""" + if type(value) is int: + if abs(value) <= limit: + return value + record = integer_record(abs(value)) + return record if value > 0 else {'negative': record} + if isinstance(value, dict): + return {k: compact_integers(v, limit) for k, v in value.items()} + if isinstance(value, (list, tuple)): + return [compact_integers(v, limit) for v in value] + return value + +# -------------------------------------------------------------------------- +# Source authentication +# -------------------------------------------------------------------------- + +def authenticated(relative, sources): + """Bytes of a SOURCES.json input row after SHA256 and Git-blob checks.""" + row = sources[relative] + data = (ROOT/relative).read_bytes() + require(digest(data) == row['sha256'], 'source SHA256 '+relative) + blob = hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + require(blob == row['git_blob'], 'source Git blob '+relative) + if relative in EXEC_PINS: + require(row['sha256'] == EXEC_PINS[relative], 'executable source pin '+relative) + return data + + +def source_rows(): + rows = json.loads((HERE/'SOURCES.json').read_text(encoding='utf-8'))['files'] + return {row['path']: row for row in rows if row['usage'] == 'input'} + + +def load_module(data, name, path, expected_sha): + """Execute source bytes only after their SHA256 equals the pin.""" + require(digest(data) == expected_sha, 'changed executable source bytes') + module = ModuleType(name) + module.__file__ = str(path) + exec(compile(data, str(path), 'exec'), module.__dict__) + return module + + +def load_predecessors(sources): + check = {path: authenticated(path, sources) for path in sources} + flow_path = ROOT/'research/rank-convergence/flow.py' + flow = load_module(check['research/rank-convergence/flow.py'], '_adaptive_flow_4483', + flow_path, EXEC_PINS['research/rank-convergence/flow.py']) + batches = load_module(check['research/chronological-batch-width/batches.py'], + '_chronological_batches_4507', + ROOT/'research/chronological-batch-width/batches.py', + EXEC_PINS['research/chronological-batch-width/batches.py']) + return flow, batches, check + + +def expect_failure(function, fragment): + try: + function() + except ValueError as exc: + require(fragment in str(exc), 'expected rejection '+repr(fragment)+', got '+repr(str(exc))) + return str(exc) + raise ValueError('control accepted: '+fragment) + + +# -------------------------------------------------------------------------- +# Independent literal oracle: ordered target words and each paid position +# -------------------------------------------------------------------------- + +def oracle_flow(targets, paid_word, cap, G, class_limit=300000): + """Replay the forest from ordered target words and individual paid jobs. + + No Pascal coefficient, product-keyed polynomial or merged path count is + used. A unit is an ordered target word of the class's remaining length + whose product (with the path multiplier) fits cap; its weight is the + product of rank multiplicities. A parent job and a child demand are the + same job exactly when their words have the same rank multiset. Every paid + position is processed separately and every child returns before the next + position. A child with multiplier above cap contains no unit, hence + neither do its descendants, and is not instantiated. + """ + ranks = sorted(targets) + cache = {} + classes = 0 + + def words(level, rho): + """Weight of each ordered word of this length by its sorted content.""" + if (level, rho) not in cache: + found = Counter() + + def extend(prefix, column, weight): + if len(prefix) == level: + found[tuple(sorted(prefix))] += weight + return + for k in ranks: + if rho*column*k <= cap: + extend(prefix+(k,), column*k, weight*targets[k]) + if rho <= cap: + extend((), 1, 1) + cache[(level, rho)] = found + return cache[(level, rho)] + + def column(content): + result = 1 + for k in content: + result *= k + return result + + def demand_of(level, rho): + """Jobs requested by the units of words(level, rho): word plus a letter.""" + result = Counter() + for content, weight in words(level, rho).items(): + for k in ranks: + result[tuple(sorted(content+(k,)))] += targets[k]*weight + return result + + out = {'roots': Counter(), 'inner': Counter(), 'boundary': Counter(), + 'leaves': Counter(), 'columns': Counter(), 'units': 0, + 'matched': 0, 'cuts': Counter()} + + def process(depth, rho, incoming): + nonlocal classes + classes += 1 + require(classes <= class_limit, 'oracle class limit') + want = demand_of(G-depth, rho) + for content, weight in want.items(): + require(incoming[content] <= weight, 'oracle incoming fits demand') + missing = weight-incoming[content] + if missing: + out['roots' if depth == 0 else 'inner'][rho*column(content)] += missing + here = words(G-depth, rho) + for content, weight in here.items(): + out['units'] += weight + out['columns'][rho*column(content)] += weight + for r in paid_word: + rr = rho*r + if depth == G: + for content, weight in here.items(): + out['leaves'][rr*column(content)] += weight + out['cuts'][(depth, rho, r, rr*column(content), weight)] += 1 + continue + child_want = demand_of(G-depth-1, rr) + passed, local = Counter(), Counter() + for content in here.keys() | child_want.keys(): + have, need = here.get(content, 0), child_want.get(content, 0) + passed[content] = min(have, need) + out['matched'] += min(have, need) + if have > need: + local[rr*column(content)] += have-need + for rank, weight in sorted(local.items()): + out['boundary'][rank] += weight + out['cuts'][(depth, rho, r, rank, weight)] += 1 + if rr <= cap: + process(depth+1, rr, +passed) + + process(0, 1, Counter()) + out['classes'] = classes + return {k: (+v if isinstance(v, Counter) and k != 'cuts' else v) for k, v in out.items()} + + +def paid_word(paid, reverse=False): + word = [r for r in sorted(paid) for _ in range(paid[r])] + return word[::-1] if reverse else word + + +def same_as_oracle(flow, oracle): + """Compare every census component with the literal replay.""" + for mine, theirs in (('roots', 'roots'), ('inner', 'inner'), ('boundary', 'boundary'), + ('leaves', 'leaves'), ('columns', 'columns')): + require(Counter(flow[mine]) == Counter(oracle[theirs]), 'literal oracle '+mine) + require(flow['units'] == oracle['units'], 'literal oracle units') + require(flow['matched'] == oracle['matched'], 'literal oracle matched jobs') + require(B.compressed_cuts(flow) == oracle['cuts'], 'literal oracle cut multiset') + return True + + +def same_as_source(flow, source): + """Compare with the authenticated #4483 Flow receipt (sources, exits, splits).""" + pairs = (('roots', 'root_sources'), ('inner', 'nonroot_sources'), + ('sources', 'sources'), ('boundary', 'boundary_exits'), + ('leaves', 'leaf_exits'), ('exits', 'exits'), ('columns', 'unit_columns')) + for mine, theirs in pairs: + require(Counter(flow[mine]) == Counter(source[theirs]), 'source Flow '+mine) + for mine, theirs in (('units', 'units'), ('column_mass', 'column_mass'), + ('matched', 'matched_jobs')): + require(flow[mine] == source[theirs], 'source Flow '+mine) + return True + + +# -------------------------------------------------------------------------- +# Fixtures +# -------------------------------------------------------------------------- + +TOY_PROFILES = [ + ('overlap', {2: 1, 5: 1}, {1: 2, 4: 1}), + ('collision', {2: 1, 4: 1, 8: 1}, {1: 2, 3: 1}), + ('weighted', {2: 2, 3: 1}, {1: 1, 2: 2}), + ('repeat', {2: 4, 3: 1}, {1: 6, 2: 2}), +] +HEIGHT_RULES = [('fixed', 0), ('fixed', 1), ('fixed', 2), ('fixed', 3), + ('default',), ('adaptive', 2, 1, 1), ('adaptive', 2, 2, 1), + ('adaptive', 3, 1, 1)] + +GEOMETRIES = [ + # name, targets, paid, rule, maximum + ('overlap-two-bit', {2: 1, 5: 1}, {1: 2, 4: 1}, ('adaptive', 2, 1, 1), 100), + ('collision-two-bit', {2: 1, 4: 1, 8: 1}, {1: 2, 3: 1}, ('adaptive', 2, 1, 1), 100), + ('repeat-two-bit', {2: 4, 3: 1}, {1: 6, 2: 2}, ('adaptive', 2, 1, 1), 100), + ('repeat-default', {2: 4, 3: 1}, {1: 6, 2: 2}, ('default',), 100), +] +P7_GEOMETRIES = [ + # (the BENCHMARKS witness base 256 gives G=0 through rank 1,000; it is + # exercised only by the census comparison below at its true boundaries) + ('p7-two-bit-height', ('adaptive', 2, 1, 1), 1209), + ('p7-four-base-height', ('adaptive', 4, 1, 1), 1209), +] +SURVEY = GEOMETRIES + [ + ('weighted-two-bit', {2: 2, 3: 1}, {1: 1, 2: 2}, ('adaptive', 2, 1, 1), 100), + ('overlap-three', {2: 1, 5: 1}, {1: 2, 4: 1}, ('adaptive', 3, 1, 1), 100), + ('overlap-g2', {2: 1, 5: 1}, {1: 2, 4: 1}, ('fixed', 2), 100), + ('collision-g2', {2: 1, 4: 1, 8: 1}, {1: 2, 3: 1}, ('fixed', 2), 100), + ('repeat-g2', {2: 4, 3: 1}, {1: 6, 2: 2}, ('fixed', 2), 100), + ('repeat-g3', {2: 4, 3: 1}, {1: 6, 2: 2}, ('fixed', 3), 100), + ('triple-g2', {2: 1, 3: 1, 5: 2}, {1: 3, 2: 1, 4: 2}, ('fixed', 2), 100), + ('triple-two-bit', {2: 1, 3: 1, 5: 2}, {1: 3, 2: 1, 4: 2}, ('adaptive', 2, 1, 1), 100), +] + + +def p7_profile(sources): + data = authenticated(PROFILE_SOURCE, sources) + bench = json.loads(authenticated('research/rank-convergence/BENCHMARKS.json', sources)) + case = next(c for c in bench['cases'] if c['name'] == 'p7') + require(case['source'] == PROFILE_SOURCE and case['profile_key'] == 'invoice_oracle', + 'BENCHMARKS p7 profile source') + invoice = json.loads(data)['invoice_oracle'] + parse = lambda h: {int(k): v for k, v in h.items()} + targets, paid = parse(invoice['targets']), parse(invoice['paid']) + require(sum(targets.values()) == 7688 and sum(paid.values()) == 55998, 'p7 census') + return targets, paid, case['witness'] + + +# -------------------------------------------------------------------------- +# Checks +# -------------------------------------------------------------------------- + +def source_receipt(Flow, targets, paid, n, G): + return Flow(targets, paid, n, G).merged() + + +def census_equalities(Flow): + """Polynomial census == literal oracle == authenticated #4483 Flow.""" + stats = Counter() + features = Counter() + for name, targets, paid in TOY_PROFILES: + m = max(targets) + word = paid_word(paid) + heavy = sum(paid.values()) > 5 + for factor in ((1, 2, 3, 4, 5, 8) if heavy else (1, 2, 3, 4, 5, 6, 8, 11)): + for extra in ((0, m-1) if not heavy else (0,)): + n = factor*m+extra + for rule in HEIGHT_RULES: + G = B.height(rule, targets, n) + if G > (2 if heavy else 6): + continue + flow = B.census(targets, paid, n//m, G) + oracle = oracle_flow(targets, word, n//m, G) + same_as_oracle(flow, oracle) + same_as_closed(flow, closed_form(targets, paid, n//m, G)) + if (name, G) in (('overlap', 2), ('weighted', 3)): + same_as_oracle(flow, oracle_flow(targets, word[::-1], n//m, G)) + try: + source = source_receipt(Flow, targets, paid, n, G) + except ValueError as exc: + require('Empty arbitrary-height flow' in str(exc), 'source rejection reason') + expect_failure(lambda: B.check_ledger(flow, targets, paid, n), + 'nonempty arbitrary-height flow') + stats['empty_flows_rejected_by_both'] += 1 + continue + same_as_source(flow, source) + B.check_ledger(flow, targets, paid, n) + stats['flows'] += 1 + stats['oracle_classes'] += oracle['classes'] + features['empty_roots'] += not flow['roots'] + features['empty_parent_later_components'] += flow['empty_parent_feeds'] > 0 + features['inner_sources'] += bool(flow['inner']) + features['boundary_exits'] += bool(flow['boundary']) + features['repeated_cut_occurrences'] += any(c[5] > 1 for c in flow['cuts']) + features['height_above_default'] += G > B.height(('default',), targets, n) + features['target_product_collisions'] += has_collision(targets, G, n//m) + return {**stats, **features} + + +def ordered_products(histogram, length, cap): + """Ordered words of one length by product, truncated at cap (all ranks >= 1).""" + result = Counter({1: 1}) + for _ in range(length): + following = Counter() + for column, count in result.items(): + for rank, weight in histogram.items(): + if column*rank <= cap: + following[column*rank] += count*weight + result = following + return result + + +def closed_form(targets, paid, cap, G): + """Cut sizes, root and inner sources straight from the proof's formulas. + + With F_h the ordered-target-word polynomial, a present parent product c at + class (d, rho) and paid rank r (rr = rho*r) leaves at rank rr*c with size + Q = sum over k | c with rr*(c/k) > cap of W_k F_{G-d-1}(c/k), + a leaf class (d = G) leaves one unit at rank rr, and an absent parent + product c (rho*c > cap) adds to the fresh sources at rank rr*c the amount + sum over k | c with rr*(c/k) <= cap of W_k F_{G-d-1}(c/k). + Nothing here classifies jobs by content or reuses a flow data structure. + """ + F = [ordered_products(targets, h, cap) for h in range(G+1)] + roots, inner, cuts = Counter(), Counter(), Counter() + for column, count in F[G].items(): + for k, weight in targets.items(): + roots[k*column] += weight*count + for d in range(G+1): + for rho, occurrences in ordered_products(paid, d, cap).items(): + for r, repeats in paid.items(): + rr, copies = rho*r, occurrences*repeats + if d == G: + cuts[(d, rho, r, rr, 1)] += copies + continue + below = F[G-d-1] + for c, parent in F[G-d].items(): + if rho*c <= cap: + size = sum(w*below.get(c//k, 0) for k, w in targets.items() + if c % k == 0 and rr*(c//k) > cap) + if size: + cuts[(d, rho, r, rr*c, size)] += copies + # Absent parents: products c = c'*k with c' eligible below. + fresh = Counter() + for cprime, count in below.items(): + if rr*cprime <= cap: + for k, w in targets.items(): + if rho*cprime*k > cap: + fresh[cprime*k] += w*count + for c, amount in fresh.items(): + inner[rr*c] += copies*amount + return {'roots': +roots, 'inner': +inner, 'cuts': cuts} + + +def same_as_closed(flow, formula): + require(Counter(flow['roots']) == formula['roots'], 'closed form roots') + require(Counter(flow['inner']) == formula['inner'], 'closed form inner sources') + require(B.compressed_cuts(flow) == formula['cuts'], 'closed form cuts') + return True + + +def has_collision(targets, G, cap): + """Two distinct same-length target multisets share a product <= cap.""" + for level in range(1, G+1): + seen = {} + for content in combinations_with_replacement(sorted(targets), level): + column = prod(content) + if column <= cap and seen.setdefault(column, content) != content: + return True + return False + + +COLLISION = ({2: 1, 4: 1, 8: 1}, {1: 1, 5: 1}, 128, 2) + + +EMPTY_PARENT = ({2: 1, 5: 1}, {1: 2, 4: 1}, 10, 2) + + +def collision_witness(): + """(2,8) and (4,4) share column 16 and leave the same cut at paid rank 5. + + Both distinct contents exit one cut at rank 80; merging them is part of the + policy (one batch per rank per cut), and the split fault must be caught. + """ + targets, paid, n, G = COLLISION + cap = n//max(targets) + flow = B.census(targets, paid, cap, G) + oracle = oracle_flow(targets, paid_word(paid), cap, G) + same_as_oracle(flow, oracle) + require(has_collision(targets, G, cap), 'collision witness collides') + merged = [c for c in flow['cuts'] if c[3] == 80 and c[2] == 5 and c[0] == 0] + require(len(merged) == 1 and merged[0][4] == 2, 'colliding contents form one cut of size 2') + split = B.census(targets, paid, cap, G, frozenset({'split-collisions'})) + require(len(split['cuts']) > len(flow['cuts']), 'split fault separates collisions') + return flow, split, oracle + + + + +def p7_census(Flow, targets, paid, witness): + """Real profile: the witness height boundary and a two-bit-base height.""" + rows = [] + for rule, ns in ((('adaptive', witness['height_base'], witness['a'], witness['b']), + (121, 30975, 30976, 31000, 60000)), + (('adaptive', 2, 1, 1), (121, 241, 242, 363, 484, 1209))): + for n in ns: + G = B.height(rule, targets, n) + flow = B.census(targets, paid, n//max(targets), G) + same_as_source(flow, source_receipt(Flow, targets, paid, n, G)) + B.check_ledger(flow, targets, paid, n) + rows.append({'n': n, 'height': G, 'sources': sum(flow['sources'].values()), + 'cuts': len(flow['cuts']), 'empty_root': not flow['roots'], + 'empty_parent_feeds': flow['empty_parent_feeds']}) + return rows + + +def minimality_bruteforce(): + count = 0 + for b1, b2, q1, q2 in cartesian(range(1, 9), range(1, 9), range(1, 7), range(1, 7)): + brute = next(a for a in range(1, b1*b2+1) if a*q1 % b1 == 0 and a*q2 % b2 == 0) + require(B.multiplier([b1, b2], [(0, q1), (1, q2)]) == brute, 'least multiplier') + count += 1 + return count + + +def rational_recurrence(targets, paid, rule, result): + """Normalized leaf cost from aggregate inventories, independent of widths.""" + m = max(targets) + cost = [Fraction(k) for k in range(m)] + flows = result['flows'] + for n in range(m, len(result['widths'])): + f = flows[(n//m, B.height(rule, targets, n))] + cost.append((sum(q*cost[n-s] for s, q in f['sources'].items()) + + sum(q*cost[e] for e, q in f['exits'].items())) + / sum(f['sources'].values())) + require(cost[n] == Fraction(result['leaves'][n], result['widths'][n]), + 'rational leaf recurrence') + require(cost[n] == Fraction(result['nested_leaves'][n], result['nested'][n]), + 'unchanged normalized leaf cost') + return True + + +def summarize(name, targets, paid, rule, maximum, result): + records = result['records'] + gains = sum(r['width'] < r['nested_width'] for r in records) + for r in records: + require(r['nested_width'] % r['width'] == 0, 'least width divides nested width') + gaps = {p: dict(v) for p, v in result['gaps'].items()} + return {'name': name, 'rule': list(rule), 'maximum': maximum, + 'targets': {str(k): v for k, v in sorted(targets.items())}, + 'paid': {str(k): v for k, v in sorted(paid.items())}, + 'compiled_ranks': len(records), + 'batch_constraints': sum(r['batches'] for r in records), + 'cuts': sum(r['cuts'] for r in records), + 'strict_width_gains': gains, + 'width': integer_record(result['widths'][-1]), + 'nested_width': integer_record(result['nested'][-1]), + 'leaves': integer_record(result['leaves'][-1]), + 'nested_leaves': integer_record(result['nested_leaves'][-1]), + 'normalized_leaf_cost_unchanged': True, + 'record_sha256': digest(canonical(compact_integers(records))), + 'pooling_gaps': gaps} + + +def compile_geometry(name, targets, paid, rule, maximum): + result = B.compile_widths(targets, paid, maximum, rule) + rational_recurrence(targets, paid, rule, result) + return result, summarize(name, targets, paid, rule, maximum, result) + + +def default_recovery(batches, targets, paid, maximum): + """The default-height specialization reproduces #4507's widths and leaves.""" + mine = B.compile_widths(targets, paid, maximum, ('default',)) + old = batches.compile_widths(targets, paid, maximum) + require(mine['widths'] == old['widths'] and mine['nested'] == old['nested_widths'] + and mine['leaves'] == old['leaves'], '#4507 default-height recovery') + return True + + +def controls(Flow, results): + rejected = {} + + def reject(name, function, fragment): + rejected[name] = expect_failure(function, fragment) + + # Census faults on a forest with no root unit, later components below an + # empty class, inner sources, boundary exits and repeated paid positions. + targets, paid, n, G = EMPTY_PARENT + cap = n//max(targets) + truth = B.census(targets, paid, cap, G) + require(not truth['roots'] and truth['inner'] and truth['boundary'] + and truth['empty_parent_feeds'] > 0 and any(c[5] > 1 for c in truth['cuts']), + 'empty-parent witness exercises every class') + oracle = oracle_flow(targets, paid_word(paid), cap, G) + same_as_oracle(truth, oracle) + B.check_ledger(truth, targets, paid, n) + for fault in ('drop-empty-parent', 'drop-boundary', 'drop-leaf', 'ignore-path-multiplier'): + reject('census fault '+fault+' versus literal oracle', + lambda fault=fault: same_as_oracle( + B.census(targets, paid, cap, G, frozenset({fault})), oracle), + 'literal oracle') + for fault in ('drop-boundary', 'drop-leaf'): + bad = B.census(targets, paid, cap, G, frozenset({fault})) + reject('census fault '+fault+' versus ledger', + lambda bad=bad: B.check_ledger(bad, targets, paid, n), + 'formal rank-invoice cancellation') + # Suppressing the empty parent also disagrees with the authenticated Flow. + bad = B.census(targets, paid, cap, G, frozenset({'drop-empty-parent'})) + reject('suppressed empty class versus source Flow', + lambda: same_as_source(bad, source_receipt(Flow, targets, paid, n, G)), 'source Flow') + # Target-product collisions: distinct contents with one product form one cut. + collide, split, collision_oracle = collision_witness() + reject('split target-product collision', + lambda: same_as_oracle(split, collision_oracle), 'literal oracle') + # Tampered executable bytes fail before execution. + with tempfile.TemporaryDirectory() as directory: + path = Path(directory)/'tampered_flow.py' + data = (ROOT/'research/rank-convergence/flow.py').read_bytes()+b'\nraise RuntimeError("ran")\n' + path.write_bytes(data) + reject('tampered flow bytes rejected before execution', + lambda: load_module(data, 'tampered', path, + EXEC_PINS['research/rank-convergence/flow.py']), + 'changed executable source bytes') + # Pooled policies: each relaxed multiplier passes its own rows (positive + # fixture) but leaves an actual chronological cut incomplete. + chosen = {} + for geometry, (result, summary) in results.items(): + for policy, gap in summary['pooling_gaps'].items(): + if gap['first'] and policy not in chosen: + chosen[policy] = (geometry, result, gap['first']) + specs = {g[0]: (g[1], g[2], g[3]) for g in GEOMETRIES} + specs.update({g[0]: (*P7_PROFILE_CACHE['p7'][:2], g[1]) for g in P7_GEOMETRIES}) + for policy, (geometry, result, first) in sorted(chosen.items()): + widths, flow_n = result['widths'], first['n'] + tg, pd, rule = specs[geometry] + flow = B.census(tg, pd, flow_n//max(tg), B.height(rule, tg, flow_n)) + rows = B.batch_rows(flow, flow_n) + pooled = B.multiplier(widths, B.batch_rows(flow, flow_n, policy)) + B.check_rows(widths, B.batch_rows(flow, flow_n, policy), pooled) + reject('pooling '+policy+' ('+geometry+' n='+str(flow_n)+')', + lambda: B.check_rows(widths, rows, pooled), 'whole chronological batch') + # A bad multiplier: remove one prime factor from the least value. + result = results['repeat-two-bit'][0] + widths = result['widths'] + n = 60 + flow = B.census({2: 4, 3: 1}, {1: 6, 2: 2}, n//3, B.height(('adaptive', 2, 1, 1), {2: 4, 3: 1}, n)) + rows = B.batch_rows(flow, n) + a = B.multiplier(widths, rows) + require(a > 1, 'nontrivial multiplier fixture') + p = next(q for q in range(2, a+1) if a % q == 0) + B.check_rows(widths, rows, a) + B.check_rows(widths, rows, 2*a) # positive: any multiple is valid + reject('multiplier missing a prime factor', lambda: B.check_rows(widths, rows, a//p), + 'whole chronological batch') + reject('zero multiplier', lambda: B.check_rows(widths, rows, 0), 'positive replication') + reject('boolean multiplier', lambda: B.check_rows(widths, rows, True), 'positive replication') + reject('zero batch count', lambda: B.multiplier([1], [(0, 0)]), 'positive batch count') + reject('boolean batch count', lambda: B.multiplier([1], [(0, True)]), 'positive batch count') + reject('future rank', lambda: B.multiplier([1], [(1, 1)]), 'smaller rank') + reject('zero width', lambda: B.multiplier([0], [(0, 1)]), 'positive supplier width') + reject('paid rank equal to target maximum', + lambda: B.validate({2: 1, 5: 1}, {5: 1}, 10), 'strict rank contract') + reject('non-integer multiplicity', lambda: B.validate({2: 1.0, 5: 1}, {1: 1}, 10), + 'positive integer histogram') + # Dropped repeated-occurrence leaf cost breaks cost preservation. + bad = B.compile_widths({2: 4, 3: 1}, {1: 6, 2: 2}, 40, ('adaptive', 2, 1, 1), False) + reject('omitted repeated-occurrence leaf cost', + lambda: rational_recurrence({2: 4, 3: 1}, {1: 6, 2: 2}, ('adaptive', 2, 1, 1), bad), + 'rational leaf recurrence') + # Perturbed receipts are rejected by the ledger. + flow = B.census({2: 1, 5: 1}, {1: 2, 4: 1}, 4, 2) + n = 20 + for label, mutate, fragment in ( + ('false root credit', lambda f: f['roots'].update({10: 1}), 'root/inner source partition'), + ('false unit column', lambda f: f['columns'].update({1: 1}), 'unit column count'), + ('missing cut', lambda f: f['cuts'].pop(), 'cut inventory equals exit inventory')): + def run(mutate=mutate): + clone = {k: (Counter(v) if isinstance(v, Counter) else list(v) if isinstance(v, list) else v) + for k, v in flow.items()} + mutate(clone) + B.check_ledger(clone, {2: 1, 5: 1}, {1: 2, 4: 1}, n) + reject(label, run, fragment) + return rejected + + +P7_PROFILE_CACHE = {} + + +def main_result(): + sources = source_rows() + flow_module, batches, _ = load_predecessors(sources) + Flow = flow_module.Flow + require(sources.keys() >= set(EXEC_PINS), 'executable sources declared') + targets7, paid7, witness = p7_profile(sources) + P7_PROFILE_CACHE['p7'] = (targets7, paid7, witness) + + equalities = census_equalities(Flow) + require(equalities['flows'] > 0 and equalities['empty_roots'] > 0 + and equalities['empty_parent_later_components'] > 0 + and equalities['repeated_cut_occurrences'] > 0 + and equalities['height_above_default'] > 0, 'fixtures exercise all classes') + p7_rows = p7_census(Flow, targets7, paid7, witness) + require(any(r['empty_parent_feeds'] for r in p7_rows), 'real-profile empty parent') + brute = minimality_bruteforce() + for name, t, p, rule, maximum in GEOMETRIES: + if rule == ('default',): + default_recovery(batches, t, p, maximum) + default_recovery(batches, {2: 1, 5: 1}, {1: 2, 4: 1}, 60) + + results = {} + for name, t, p, rule, maximum in GEOMETRIES: + results[name] = compile_geometry(name, t, p, rule, maximum) + for name, rule, maximum in P7_GEOMETRIES: + results[name] = compile_geometry(name, targets7, paid7, rule, maximum) + for policy in ('aggregate', 'occurrences', 'leaf-pooled'): + require(any(s['pooling_gaps'][policy]['first'] for _, s in results.values()), + 'a real pooling gap for '+policy) + require(any(s['strict_width_gains'] for _, s in results.values()), 'strict width gain') + rejected = controls(Flow, results) + first = results['overlap-two-bit'][0] + table = [{k: v for k, v in r.items() if k in ('n', 'height', 'multiplier', 'sources', + 'width', 'nested_width', 'leaves')} + for r in first['records'][:24]] + return {'schema': 'adaptive-chronological-batching/v1', + 'claim_type': 'conditional batch-level transfer and exact finite accounting', + 'no_new_kappa': True, 'no_convergence_or_native_admission_claim': True, + 'source_sha256': {p: r['sha256'] for p, r in sorted(sources.items())}, + 'census_equalities': equalities, 'real_profile_census': p7_rows, + 'brute_force_minimality_cases': brute, + 'geometries': [s for _, s in results.values()], + 'small_table_overlap_two_bit': table, + 'rejected_controls': sorted(rejected)} + + +def survey(): + """Authoring aid: print pooling-gap and width-gain statistics per geometry.""" + sources = source_rows() + targets7, paid7, witness = p7_profile(sources) + rows = [(n, t, p, r, m) for n, t, p, r, m in SURVEY] + rows += [(n, targets7, paid7, r, m) for n, r, m in P7_GEOMETRIES] + for name, t, p, rule, maximum in rows: + result = B.compile_widths(t, p, maximum, rule) + s = summarize(name, t, p, rule, maximum, result) + print(json.dumps({'name': name, 'gains': s['strict_width_gains'], + 'ranks': s['compiled_ranks'], 'cuts': s['cuts'], + 'width_bits': s['width']['bits'], 'nested_bits': s['nested_width']['bits'], + 'gaps': {k: [v['ranks_with_gap'], v['first'] and v['first']['n']] + for k, v in s['pooling_gaps'].items()}}), flush=True) + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--write', action='store_true', help='authoring only: replace RESULT.json') + ap.add_argument('--survey', action='store_true', help='authoring only: print gap survey') + args = ap.parse_args() + if args.survey: + survey() + return + result = json.loads(canonical(compact_integers(main_result()))) + target = HERE/'RESULT.json' + if args.write: + target.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n', + encoding='utf-8', newline='\n') + else: + require(result == json.loads(target.read_text(encoding='utf-8')), + 'committed result matches fresh replay') + print('PASS_ADAPTIVE_CHRONOLOGICAL_BATCHING flows='+str(result['census_equalities']['flows']) + +' controls='+str(len(result['rejected_controls']))) + + +if __name__ == '__main__': + main() diff --git a/research/adaptive-chronological-batching/width_bound.py b/research/adaptive-chronological-batching/width_bound.py new file mode 100755 index 0000000000..cc8aedc99f --- /dev/null +++ b/research/adaptive-chronological-batching/width_bound.py @@ -0,0 +1,278 @@ +#!/usr/bin/env python3 +"""Exact finite witnesses for WIDTH.md's symbolic adaptive width theorem. + +Reuses this package's cut census; does not claim a second independent compiler. +The source profile and #4483 census comparisons are authenticated by verify.py. +Prepared for codyw912 with substantial OpenAI assistance; the integer level-run +proof was supplied by an independent Anthropic mathematical challenge. +Apache-2.0. +""" +from bisect import bisect_right +from collections import defaultdict +from math import lcm, prod +from pathlib import Path +import argparse +import json +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import batching as B +import verify as V + +require = B.require + + +def prime_support(generators): + primes = set() + for value in generators: + p = 2 + while p * p <= value: + while value % p == 0: + primes.add(p) + value //= p + p += 1 + if value > 1: + primes.add(value) + return sorted(primes) + + +def semigroup(generators, cap): + generators = sorted(set(k for k in generators if k > 1)) + seen, todo = {1}, [1] + while todo: + value = todo.pop() + for k in generators: + if k > cap // value: + break + following = value * k + if following not in seen: + seen.add(following) + todo.append(following) + return sorted(seen) + + +def signature(flow): + histograms = ('roots', 'inner', 'sources', 'boundary', 'leaves', 'exits', 'columns') + return (flow['height'], tuple(tuple(sorted(flow[k].items())) for k in histograms), + tuple(flow['cuts']), flow['units'], flow['column_mass'], flow['matched']) + + +def level_limits(m, k0, M, g, maximum, cutoff): + result = [] + for level in range(B.floor_log(maximum // m, M) + 1): + low = max(cutoff, m * M ** level) + high = min(maximum, m * M ** (level + 1) - 1) + decrement = min(M ** level, k0 ** (g * level + 1)) + visits = 0 if low > high else 1 + (high - low) // decrement + result.append({'level': level, 'low': low, 'high': high, + 'decrement': decrement, 'visit_bound': visits}) + return result + + +def check_edges(flow, targets, paid, n, M, g): + B.check_ledger(flow, targets, paid, n) + k0, m = min(targets), max(targets) + level = B.floor_log(n // m, M) + require(flow['height'] == g * level, 'adaptive height at the exact cutoff') + root_floor = k0 ** (g * level + 1) + require(all(s >= root_floor for s in flow['roots']), 'root target-word lower bound') + decrement = min(n // m, root_floor) + rows = B.batch_rows(flow, n) + require(all(0 <= j < n and n - j >= decrement for j, _ in rows), + 'every actual recursive edge has the integer decrement') + W, P = sum(targets.values()), sum(paid.values()) + source_count = sum(flow['sources'].values()) + require(1 <= source_count <= W * (W + P) ** flow['height'], + 'positive source count and arbitrary-height demand-slot bound') + return rows + + +def clear_source_caches(module): + for method in (module.BaseFlow.column, module.BaseFlow.points, + module.BaseFlow.units, module.BaseFlow.demand): + method.cache_clear() + + +def finite_case(name, targets, paid, M, g, maximum, source_module, cutoff=None): + m, k0 = max(targets), min(targets) + cutoff = m if cutoff is None else cutoff + require(paid.get(1, 0) > 0 and maximum >= cutoff >= m, 'nonempty rule and ordinary base') + cap = maximum // m + generators = set(targets) | set(paid) | {M} + primes = prime_support(generators) + starts = semigroup(generators, cap) + starts_set = set(starts) + box = prod(1 + B.floor_log(cap, p) for p in primes) + require(len(starts) <= box, 'prime-exponent box bounds plateau count') + flows, counts = {}, {} + previous = None + changes = [] + for c in range(1, cap + 1): + G = g * B.floor_log(c, M) + flow = B.census(targets, paid, c, G) + check_edges(flow, targets, paid, m * c, M, g) + source = source_module.Flow(targets, paid, m * c, G).merged() + V.same_as_source(flow, source) + clear_source_caches(source_module) + current = signature(flow) + if current != previous: + require(c in starts_set, 'every census change is a semigroup threshold') + changes.append(c) + flows[c] = flow + if c in starts_set: + counts[c] = sum(flow['sources'].values()) + plateau = starts[bisect_right(starts, c) - 1] + require(counts[plateau] == sum(flow['sources'].values()), 'constant plateau source count') + previous = current + + limits = level_limits(m, k0, M, g, maximum, cutoff) + level_lcms = [1] * len(limits) + level_counts = [0] * len(limits) + for c in starts: + level = B.floor_log(c, M) + level_lcms[level] = lcm(level_lcms[level], counts[c]) + level_counts[level] += 1 + divisor = prod(value ** row['visit_bound'] for value, row in zip(level_lcms, limits)) + W, P = sum(targets.values()), sum(paid.values()) + ceil_log_W = (W - 1).bit_length() + ceil_log_WP = (W + P - 1).bit_length() + bit_bound = sum(row['visit_bound'] * level_counts[level] + * (ceil_log_W + g * level * ceil_log_WP) + for level, row in enumerate(limits)) + require(divisor <= 1 << bit_bound, 'exact integer bit envelope') + + widths = [1] * cutoff + depths = [0] * cutoff + visits = [{} for _ in range(cutoff)] + maximum_visits = defaultdict(int) + constraints = 0 + for n in range(cutoff, maximum + 1): + flow = flows[n // m] + rows = check_edges(flow, targets, paid, n, M, g) + children = set(j for j, _ in rows) + replication = B.multiplier(widths, rows) + B.check_rows(widths, rows, replication) + width = replication * sum(flow['sources'].values()) + require(divisor % width == 0, 'all-prime level-run divisor at every rank') + widths.append(width) + depth = 1 + max((depths[j] for j in children), default=0) + require(depth <= sum(row['visit_bound'] for row in limits), 'chain-depth upper bound') + depths.append(depth) + level = B.floor_log(n // m, M) + visit = {} + for j in children: + for ell, number in visits[j].items(): + visit[ell] = max(visit.get(ell, 0), number) + visit[level] = visit.get(level, 0) + 1 + for ell, number in visit.items(): + require(number <= limits[ell]['visit_bound'], 'per-level chain visit bound') + maximum_visits[ell] = max(maximum_visits[ell], number) + visits.append(visit) + constraints += len(rows) + return {'name': name, 'targets': targets, 'paid': paid, 'M': M, 'g': g, + 'maximum': maximum, 'ordinary_cutoff': cutoff, + 'regime': 'quasipolynomial' if k0 ** g >= M else 'subexponential', + 'rank_and_height_primes': primes, 'plateaus': len(starts), + 'observed_census_changes': len(changes), 'prime_box': box, + 'constraints': constraints, 'maximum_chain_depth': max(depths), + 'levels': [{**row, 'observed_visits': maximum_visits[row['level']], + 'plateaus': level_counts[row['level']]} for row in limits], + 'final_width': V.integer_record(widths[-1]), + 'divisor': V.integer_record(divisor), 'bit_envelope': bit_bound, + 'all_rank_integer_divisibility': True} + + +def profile_boundaries(sources, source_module): + benchmarks = json.loads(V.authenticated('research/rank-convergence/BENCHMARKS.json', sources)) + expected = {'p7': (121, 5, 256, 2, 7688, 55998), + 'native4453': (153, 4, 1024, 2, 11560, 69273), + 'p16': (145, 4, 1024, 2, 10928, 64620)} + reports = [] + for case in benchmarks['cases']: + if case['name'] not in expected: + continue + raw = json.loads(V.authenticated(case['source'], sources)) + raw = raw[case['profile_key']] if case['profile_key'] else raw + targets = {int(k): v for k, v in raw['targets'].items()} + paid = {int(k): v for k, v in raw['paid'].items()} + witness = case['witness'] + M, g = witness['height_base'], witness['a'] + witness['b'] + m, k0 = max(targets), min(targets) + require((m, k0, M, g, sum(targets.values()), sum(paid.values())) == expected[case['name']], + 'source-bound profile and unchanged adaptive geometry') + require(paid.get(1, 0) > 0, 'paid rank one supplies nonempty forests') + if case['name'] != 'p7': + require(M ** 2 == k0 ** (5 * g), 'exact three-fifths width exponent') + rows = [] + for cap in sorted({1, 2, k0, M - 1, M, M + 1, 2 * M, M * M - 1, M * M}): + G = g * B.floor_log(cap, M) + flow = B.census(targets, paid, cap, G) + source = source_module.Flow(targets, paid, m * cap, G).merged() + V.same_as_source(flow, source) + clear_source_caches(source_module) + # Both ends of a floor(n/m) block matter; n=m*C alone is insufficient. + constraints = sum(len(check_edges(flow, targets, paid, n, M, g)) + for n in (m * cap, m * (cap + 1) - 1)) + if flow['roots']: + require(min(flow['roots']) == k0 ** (G + 1), 'sharp root-word minimum') + rows.append({'cap': cap, 'height': G, 'source_types': len(flow['sources']), + 'sources': sum(flow['sources'].values()), + 'root_minimum': min(flow['roots'], default=None), + 'checked_batch_rows': constraints}) + reports.append({'profile': case['name'], 'M': M, 'g': g, 'k0': k0, 'm': m, + 'exponent': '1-log_256(25)' if case['name'] == 'p7' else '3/5', + 'boundary_probes': rows}) + require({row['profile'] for row in reports} == set(expected), 'all three pinned applications') + return reports + + +def controls(): + targets, paid = {2: 1, 5: 1}, {1: 2, 4: 1} + before = B.census(targets, paid, 3, 0) + after = B.census(targets, paid, 3, 1) + require(signature(before) != signature(after), 'height jump changes actual census') + require(3 not in semigroup(set(targets) | set(paid), 3), 'omitted M loses a real threshold') + flow = B.census(targets, paid, 10, 1) + require(min(flow['roots']) == 4 and 5 * min(flow['roots']) <= 50, + 'adaptive root contradicts the default all-source contraction') + return ['omitted_height_generator', 'false_default_root_contraction'] + + +def run(): + sources = V.source_rows() + source_module, _, _ = V.load_predecessors(sources) + cases = [ + ('new-height-prime', {2: 1, 5: 1}, {1: 2, 4: 1}, 3, 1, 300, None), + ('quasipolynomial-boundary', {2: 1, 5: 1}, {1: 2, 4: 1}, 4, 2, 300, None), + ('empty-root-components', {2: 1, 5: 1}, {1: 2, 4: 1}, 2, 3, 150, None), + ('collisions-and-larger-base', {2: 1, 4: 1, 8: 1}, {1: 1, 5: 1}, 7, 2, 300, 56), + ] + reports = [finite_case(*case[:-1], source_module, cutoff=case[-1]) for case in cases] + return {'schema': 'adaptive-width-bound/v1', 'no_new_kappa': True, + 'claim': 'Symbolic all-rank theorem in WIDTH.md; finite integer witnesses here', + 'source_sha256': {p: r['sha256'] for p, r in sorted(sources.items())}, + 'finite_compilations': reports, + 'profile_applications': profile_boundaries(sources, source_module), + 'boundary_controls': controls()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true', help='Regenerate this package receipt') + args = parser.parse_args() + result = run() + path = HERE / 'WIDTH-RESULT.json' + if args.write: + path.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + require(json.loads(path.read_text()) == json.loads(json.dumps(result)), 'width receipt equality') + print('PASS_ADAPTIVE_WIDTH_BOUND', json.dumps({ + 'compilations': len(result['finite_compilations']), + 'constraints': sum(row['constraints'] for row in result['finite_compilations']), + 'profiles': len(result['profile_applications']), + 'controls': len(result['boundary_controls']), 'no_new_kappa': True}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/chronological-width-bound/README.md b/research/chronological-width-bound/README.md new file mode 100644 index 0000000000..7548fd2060 --- /dev/null +++ b/research/chronological-width-bound/README.md @@ -0,0 +1,407 @@ +# A quasipolynomial width bound for chronological batching + +**Result: for a fixed default-height mixed rule, the least per-cut widths of +[#4507](https://github.com/CrocSwap/integer-mult-bounds/pull/4507) satisfy** + +\[ +\log B_N=O((\log N)^{d+1}), +\] + +where `d` is the number of distinct primes dividing the target and paid +ranks. Equivalently, `B_N = exp(O((log N)^(d+1)))`. This sharpens the +default-height bound `log B_N = O((1+log N)^(d+2))` already proved in +[#4586](https://github.com/CrocSwap/integer-mult-bounds/pull/4586) at +`aadb7bc59390683450b1969e4632f546929dc569`: bounded visits to each +source-count plateau remove one logarithmic factor. It sharpens the answer +to the all-rank width question in [Discussion #4503](https://github.com/CrocSwap/integer-mult-bounds/discussions/4503) +without changing the normalized leaf cost. It is an upper bound, not a +tight growth law or a practical size estimate. + +The proof is a prime-valuation argument over contracting rank chains. +Finite replays below exercise its hypotheses; they are not the proof of +an asymptotic claim. **No new κ, convergence theorem, physical supplier +admission or selected-frontier change is claimed.** + +This is one contribution with two separately replayable packages. This +package retains the default-height proof and witnesses; the companion +[adaptive package](../adaptive-chronological-batching/README.md) proves +arbitrary-height cut transfer and its conditional all-rank width bound. +Neither package is a second batching algorithm or a separate submission. + +## 1. Exact boundary and predecessor delta + +Let a fixed native rule have target multiplicities `W_k > 0` and paid +multiplicities `P_r > 0`, with + +```text +2 <= k_min <= k <= m = max target rank, +1 <= r <= r_max < m, +W = sum_k W_k, P = sum_r P_r. +``` + +The multiplicities are positive integers. `P` counts paid positions, not +just distinct paid ranks. At rank `n >= m`, use precisely #4436's default +height + +```text +C_n = floor(n/m), +G_n = floor(log_(k_min) C_n). +``` + +Use ordinary base widths `B_j = 1` for `0 <= j < m`. For every larger +rank, #4507's policy groups all source complements upfront, and groups +unmatched exits at one paid position of one chronological path class. +Repeated paths and paid positions remain separate cuts. If its source +count is `S_n` and its rank/count batches are `(e,q)`, its least replication +factor and width are + +```text +a_n = lcm_(e,q) B_e / gcd(B_e,q), +B_n = S_n * a_n. +``` + +Every parent waits for its exits and child before resuming. There is no +cross-cut pooling or fractional invocation. The correctness and minimality +of that policy are Mihir Srivastava's #4507 result; the integer flow is +zxv's #4436, building on Jacob Alan Sussman's compiler. This package adds +a **uniform growth bound for their width sequence**, not a new batching +algorithm. #4519 separately recomputes the predecessor's finite numbers. +[#4588](https://github.com/CrocSwap/integer-mult-bounds/pull/4588) at +`2f6578907b7f8718a13921552cc3069d3908e936` adds independent finite +default-height checks, not the new `d+1` proof. + +The fixed native word's arbitrary-input/all-column correctness, whole-job +adapters, owned state and physical execution contracts remain premises. +The theorem below is also a statement about an integer recurrence without +those physical premises. Positive rank surplus is not needed for the +width bound itself; resource consequences using surplus are conditional +on it, as in #4436. + +**Specialization and nonemptiness.** The default root has a unit because +`k_min^G <= C`; no paid rank-one position is required. The companion +[WIDTH.md](../adaptive-chronological-batching/WIDTH.md) assumes paid rank +one as a sufficient nonemptiness condition for arbitrary heights. At +`M=k_min, g=1` its symbolic formula gives `d'=d, z=0` and the same `d+1` +order on their common hypotheses. Its named adaptive height interface uses +positive `a,b` with `g=a+b>=2`, so that route does not exercise `g=1`. +The default plateau-product divisor here and the companion level-LCM +divisor are different certificates; no universal finite numerical dominance +is claimed. [#4591](https://github.com/CrocSwap/integer-mult-bounds/pull/4591) +at `84c0fb3a39bcb1e4b8c48892bfdd8a6e7ae58a50` checks arbitrary-height +aggregate identities, not the actual cut divisibility proved by the companion. + +## 2. Source-count plateaus + +Let `Γ` be the multiplicative semigroup generated by all target and paid +ranks, including `1`. Let `Π` be their prime support and `d = |Π|`. For a +positive integer cap `C`, the entire default flow depends only on + +```text +{ gamma in Γ : gamma <= C }. +``` + +To see this, the target-word counts at each degree are fixed integer +coefficients. The cap only tests target products, paid path products, +their products, and the powers of `k_min` determining the height. Every +threshold is in `Γ`. The child demand uses a target word with one factor +removed, then its paid-prefix product; this is still in `Γ`. Path +multiplicities and repeated paid positions do not introduce new threshold +values. Consequently sources, exits, cuts (including their repetition +counts), and `S` are constant between consecutive elements of `Γ`. + +Write `S(γ)` for the source count on the plateau starting at `γ`, and +`γ+` for the next semigroup element. Since `k_min * γ` is in `Γ`, + +```text +γ+ <= k_min * γ. +``` + +The plateaus need not have distinct source counts. Counting them rather +than deduplicating equal counts is safe. For `X >= 1`, + +\[ +|\Gamma\cap[1,X]| +\le \prod_{p\in\Pi}(1+\lfloor\log_p X\rfloor) +\le (1+\lfloor\log_2 X\rfloor)^d. +\] + +This is just the exponent box containing every `Π`-smooth product. The +box can contain numbers not in `Γ`; only an upper bound is used. + +At depth `h`, there are at most `P^h` paid paths and `W^(G-h)` units per +path. Thus, including degree zero, + +\[ +U\le\sum_{h=0}^G P^hW^{G-h}\le(W+P)^G, +\qquad 1\le S\le WU\le W(W+P)^G. +\] + +The middle inequality follows from the binomial expansion, whose +coefficients are at least one. A root unit with product `k_min^G <= C` +always exists; its target demands also give `S >= W`. + +## 3. Every recursive rank contracts + +Every source has rank `s > n/m`. A root source has target degree `G+1`, +so its product is at least `k_min^(G+1) > C_n`; integrality gives +`s >= C_n+1 > n/m`. A nonroot source comes from an absent parent point. +That parent's integer product exceeds `C_n`; multiplying by a paid rank +at least one retains the strict lower bound. Every source fits `n`, since +it is the target of an eligible native unit. + +Therefore a complement rank satisfies + +```text +0 <= n-s < (m-1)n/m. +``` + +An exit is a rank-`r` job from a unit of column at most `C_n`, hence + +```text +0 < e <= r_max * C_n <= (m-1)n/m < n. +``` + +Set `α = (m-1)/m < 1`. Every recursive edge has rank at most `α` times +its parent's rank. This specific fact is why the default-height boundary +matters. It is not inferred merely from strict descent. + +## 4. Prime valuations follow a contracting chain + +Fix any prime `p`, not necessarily a prime dividing a native rank. For a +batch `(e,q)`, + +```text +v_p(B_e/gcd(B_e,q)) <= v_p(B_e). +``` + +Since the valuation of an LCM is the maximum, + +\[ +v_p(B_n)\le v_p(S_n)+\max_{e\text{ invoked at }n}v_p(B_e). +\] + +Strong induction bounds this by the largest sum of source-count valuations +along a recursive rank chain ending below `m`. The maximizing chain may +be different for each prime; the next bound holds for **every** chain. +No joint choice of a maximizing chain is assumed. + +Put + +```text +τ = m * ceil(log2 k_min). +``` + +Bernoulli's inequality gives + +\[ +(m/(m-1))^m=(1+1/(m-1))^m +\ge1+m/(m-1)>2, +\] + +so `α^m < 1/2`, and `α^τ < 1/k_min`. A descending chain can visit a +single cap plateau at most `τ` times. Otherwise, let its first and +`τ`-steps-later ranks be `n_i` and `n_(i+τ)` in the same plateau `γ`. +The cap condition gives `mγ <= n_(i+τ)` and `n_i < mγ+`, while + +\[ +n_{i+\tau}\le\alpha^\tau n_i +< m\gamma^+/k_{\min}\le m\gamma, +\] + +contradiction. Caps never increase, so visits to one plateau are +contiguous. + +It follows for **every prime** that + +\[ +v_p(B_n)\le\tau\sum_{\gamma\in\Gamma,\ \gamma\le\lfloor N/m\rfloor} +v_p(S(\gamma)),\qquad n\le N. +\] + +Hence the explicit integer divisibility certificate is + +\[ +\boxed{\quad B_n\mid Q_N:= +\prod_{\gamma\in\Gamma,\ \gamma\le\lfloor N/m\rfloor}S(\gamma)^\tau, +\quad 0\le n\le N.\quad} +\] + +Repeated equal `S(γ)` values intentionally retain one factor per plateau. +Their prime factors need not lie in `Π`; `Π` bounds plateau **locations**, +not the prime support of the widths. + +## 5. Uniform logarithmic bound and consequence + +Let `C = floor(N/m)` and `G = floor(log_(k_min) C)` for `N >= m`. +Combining the preceding bounds yields + +\[ +\log_2 B_N\le +\tau\prod_{p\in\Pi}(1+\lfloor\log_p C\rfloor) +\bigl(\log_2 W+G\log_2(W+P)\bigr). +\] + +Replacing each logarithm on the right by its integer ceiling produces the +explicit bit envelope checked by `verify.py`. All parameters of the +native rule are fixed, so the right-hand side is +`O((log N)^(d+1))`. This proves the stated result for all ranks. + +The proof does not need the gcd savings: the same upper bound applies +when replication is the LCM of the invoked child widths without dividing +by batch counts. The structural improvement over #4436's nested choice +comes from using **only actually invoked, contracting ranks**, rather +than insisting that `B_(n-1)` divide each replication factor. + +When `W >= 2`, the old nested policy has +`B_N(old) = product_(n=m..N) S_n >= W^(N-m+1)`, an exponential lower bound. +The quasipolynomial upper bound is therefore an asymptotic width +improvement in that case. This does not say that the new upper bound is +tight. In the degenerate rule `{2:1} <- {1:1}`, both widths stay one. + +The normalized leaf recurrence is unchanged by valid replication, + +```text +L(n) = [sum_s S_s L(n-s) + sum_e E_e L(e)] / S_n. +``` + +Thus no saving exponent improves merely from this theorem. Where a +positive rank surplus `Δ` and the source native contracts apply, #4436's +identity `B_N*N - P_N = Δ*Qcol_N` also gives the same quasipolynomial +upper order for its raw-instance and owned-center counts. No unpriced +router, full fixed-tape constant or eventual multiplication threshold is +included in that consequence. + +## 6. Executed evidence + +Python 3.12.14, standard library, Linux. The direct isolated-Python +receipt-generation command completed in about four seconds in the author environment. +The receipt records five fixtures and **102,215 chronological batch +constraints**, with two source representations compared at every cap. + +| Fixed rule | N | Rank-prime count | Plateaus | Least width bits | Nested width bits | `Q_N` bits | +| --- | ---: | ---: | ---: | ---: | ---: | ---: | +| `{2:1,5:1} <- {1:2,4:1}` | 1000 | 2 | 19 | 136 | 8940 | 664 | +| `{2:4,3:1} <- {1:6,2:2}` | 1000 | 2 | 30 | 285 | 18105 | 1283 | +| `{2:1,4:1,8:1} <- {1:2,3:1,7:1}` | 300 | 3 | 18 | 153 | 2195 | 962 | +| Frozen raw p7 | 1000 | 7 | 8 | 2524 | 17504 | 59923 | +| `{2:1} <- {1:1}` | 100 | 1 | 6 | 1 | 1 | 1 | + +The raw-p7 finite width comparison is predecessor evidence reproduced here, +not a new finite improvement. Its conservative `Q_N` is larger than the +nested width at this small rank. A better asymptotic upper order does not +imply a numerically smaller bound at every finite rank. +The raw histograms here come from +`higher-moment-strictification/RESULT.json:invoice_oracle`. A separate exact +comparison found both target and paid histograms equal to #4507's vendored +`p7-RESULT.json:strictification.native_inventory` (7,688 targets and 55,998 +paid positions). That source-equivalence comparison is author-run evidence, +not an additional gate in this package's registered replay. + +New checks include full flow/cut plateau signatures, exponent-box counts, +source bounds, every child contraction, chain-depth and per-plateau-visit +dynamic programs, eleven explicit prime-valuation recurrences, and exact +**all-prime integer divisibility** for every computed width. The eleven +sampled valuations are diagnostics only; they are not substituted for the +all-prime divisibility check or the quantified proof. + +Four boundary controls are exercised: + +1. Omitting paid-rank generator `3` from `{2,5} <- {1,3}` misses the real + cap-3 change, where source count increases from 3 to 4. +2. Changing the height base to `5` at `n=50` introduces root source rank + `4 <= n/m=10`, invalidating the source lower bound used here. +3. The retained rank-12 pooled multiplier `175` fails the separate + one-job rank-8 cuts; the chronological multiplier is `700`. +4. Erasing prime `5` from the proposed divisor fails the actual rank-3 + width `5`, even if other-prime checks are retained. + +`verify.py` authenticates all live inputs before loading two predecessor +implementations. It **does not claim an independently written width +compiler**: #4507's compiler produces the widths, #4436's exponent-vector +flow cross-checks its source census, and the new checks certify the stated +bounds on those outputs. Cut correctness is inherited from #4507's literal +fixtures; this package does not replay that independent cut oracle. The +normalized-cost gate is the retained compiler's exact cross-product equality +between least-batch and nested leaf totals at every rank, not a separately +implemented rational recurrence. The symbolic proof is complete above. +Separate Anthropic-model review challenged it and supplied the sharper +bounded plateau-visit argument; that is not human or proof-kernel verification. + +## 7. Reproduction and coordination + +From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/chronological-width-bound --check-only +python3.12 -B scripts/research_package.py --package research/chronological-width-bound +python3.12 -I -O -B research/chronological-width-bound/verify.py +``` + +The other scoped replay in the same PR is: + +```sh +python3.12 -B scripts/research_package.py --package research/adaptive-chronological-batching +``` + +`--write` regenerates only this package's `RESULT.json`. Source pins are in +`SOURCES.json`; the historical task card and selected record remain +provenance, not moving scientific inputs. Reproduction requires Python 3.12 +and the standard library; no Nix or direnv environment is required. + +Historical base: canonical main `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`, +priority revision 7. The historical selected record was `23/10000`; those +bytes and the task card remain provenance. The consolidation comparison +uses fetched main `fbc9ea0249746acca4f504d4fda2b84e0e36cf0d`, whose selected +conditional κ is `.00302015` from #4470; #4483 and #4507 are not selected. +No selected record is edited. Scope is explicitly **changed** from +`independent-moment` invoice coverage to #4507's open all-rank width question. + +The historical theorem-specific refresh at 2026-10-22 04:01 UTC searched +5,860 tracked local note paths, 317 open PRs and 3,412 Discussion records +with complete reported pagination, but no fresh closed-PR scan or diffs. +The consolidation refresh on the same date covered 408 open PRs at +13:08:38 UTC, 3,852 closed PRs at 13:09:39 UTC and 3,577 Discussion records +at 13:09:11 UTC, with complete reported pagination. It is a non-atomic +snapshot, not exhaustive novelty proof. Actual #4586/#4588/#4591 proofs +and code determine the scoped delta above. #4519's finite recount and +#4521's expanded-count audit remain complementary. + +Discussion posting returned HTTP 403, so this evidence remains +**LOCAL-ONLY until publication approval**. No public reservation or +result is claimed. The historical baseline fails on the new certificate's +missing `bit_lower`; the #4463 successor +`python3 -B scripts/research_selected_baseline.py` passed source-bound +orientation. No selected cold replay was run. + +## Open next questions + +1. **Can the logarithmic degree or constants be sharpened?** The prime-box + count ignores dependencies among generator exponent vectors. A first + step is to replace it by a rigorously bounded exponent lattice of lower + rank. The present argument supplies no tight lower bound for `B_N`. +2. **How can the adaptive envelope be sharpened?** The companion + [WIDTH.md](../adaptive-chronological-batching/WIDTH.md) now supplies a + root/decrement and level-visit argument for fixed adaptive parameters. + A next step is to retain actual gcd savings or narrower semigroup counts. + The rank-4 source control above still blocks copying the default + fixed-contraction proof unchanged to arbitrary heights. +3. **Which physical constants inherit the improved width?** Substitute + the bound into one actual emitted compiler's owned-state and routing + ledger, preserving encoded addresses and all temporary stock. Physical + realization and the retained analytic/precision/recovery contracts have + not been re-proved here. + +## Attribution + +Jacob Alan Sussman: multinomial integer compiler and Theorem 1G. +zxv: #4436's chronological overlapping flow and resource accounting, on +#4359 and the retained native/outer lineage. Mihir Srivastava / mihir-s-05: +#4507's least per-cut replication policy, finite width witnesses and +explicit all-rank handoff. Ryanson Jonathan / pinterbanget: #4456/#4476 +flow and width audits, and #4519's separate recount. Cinna Davis / +1337isnot1337: raw-p7 construction and inherited native lineage. + +Prepared for **codyw912**, with substantial OpenAI assistance in theorem, +implementation and writing, and separate Anthropic-model mathematical +challenge. Retained scientific sources keep their own notices. New work +is Apache-2.0. No independent human or formal-kernel acceptance is claimed. diff --git a/research/chronological-width-bound/RESULT.json b/research/chronological-width-bound/RESULT.json new file mode 100644 index 0000000000..6333d32638 --- /dev/null +++ b/research/chronological-width-bound/RESULT.json @@ -0,0 +1,234 @@ +{ + "cases": [ + { + "all_rank_statement_source": "README.md symbolic proof; finite checks are witnesses only", + "chronological_constraints": 20746, + "coarse_depth_bound": 40, + "distinct_source_counts": 19, + "explicit_log2_upper_bound": 3520, + "largest_chain_depth": 21, + "largest_observed_plateau_visits": 3, + "least_width_bits": 136, + "maximum_rank": 1000, + "name": "overlapping_two_rank", + "nested_width_bits": 8940, + "normalized_cost_agreement": true, + "observed_flow_changes": 19, + "paid": { + "1": 2, + "4": 1 + }, + "rank_primes": [ + 2, + 5 + ], + "semigroup_plateaus": 19, + "sharp_divisor_bits": 664, + "sharp_divisor_sha256": "91c6453ae924e48b7b8d13c9b67c8f5ccbc3498798ef7eb825ebe3f82eb87a17", + "smooth_box": 32, + "source_representation_comparisons": 200, + "targets": { + "2": 1, + "5": 1 + }, + "tau": 5, + "width_sequence_sha256": "213eddb3e3bcc5f5e14ee9d71addf2a598b76680418c64f90c9678a21539fe32" + }, + { + "all_rank_statement_source": "README.md symbolic proof; finite checks are witnesses only", + "chronological_constraints": 23426, + "coarse_depth_bound": 27, + "distinct_source_counts": 30, + "explicit_log2_upper_bound": 5670, + "largest_chain_depth": 14, + "largest_observed_plateau_visits": 2, + "least_width_bits": 285, + "maximum_rank": 1000, + "name": "chronology_counterexample_family", + "nested_width_bits": 18105, + "normalized_cost_agreement": true, + "observed_flow_changes": 30, + "paid": { + "1": 6, + "2": 2 + }, + "rank_primes": [ + 2, + 3 + ], + "semigroup_plateaus": 30, + "sharp_divisor_bits": 1283, + "sharp_divisor_sha256": "78ab680a41e7bb92f8961098f34dcf56373077d5f0cabd3823b78c131c4946e2", + "smooth_box": 54, + "source_representation_comparisons": 333, + "targets": { + "2": 4, + "3": 1 + }, + "tau": 3, + "width_sequence_sha256": "fcf05281828d4de3f40af8ee68d2048d61249613ade0e6feec7faf79303f9cf7" + }, + { + "all_rank_statement_source": "README.md symbolic proof; finite checks are witnesses only", + "chronological_constraints": 10765, + "coarse_depth_bound": 48, + "distinct_source_counts": 16, + "explicit_log2_upper_bound": 6528, + "largest_chain_depth": 24, + "largest_observed_plateau_visits": 4, + "least_width_bits": 153, + "maximum_rank": 300, + "name": "product_collisions", + "nested_width_bits": 2195, + "normalized_cost_agreement": true, + "observed_flow_changes": 18, + "paid": { + "1": 2, + "3": 1, + "7": 1 + }, + "rank_primes": [ + 2, + 3, + 7 + ], + "semigroup_plateaus": 18, + "sharp_divisor_bits": 962, + "sharp_divisor_sha256": "50ba4522acd03029f76a7f73e29d5e01ef8fbf8996d21ce70dcb86720cdbc624", + "smooth_box": 48, + "source_representation_comparisons": 37, + "targets": { + "2": 1, + "4": 1, + "8": 1 + }, + "tau": 8, + "width_sequence_sha256": "4b19bb1cebcbd83d3c77df6e08f4db991a5241c1185de3904e3b9bce7e785144" + }, + { + "all_rank_statement_source": "README.md symbolic proof; finite checks are witnesses only", + "chronological_constraints": 47080, + "coarse_depth_bound": 484, + "distinct_source_counts": 5, + "explicit_log2_upper_bound": 336864, + "largest_chain_depth": 153, + "largest_observed_plateau_visits": 25, + "least_width_bits": 2524, + "maximum_rank": 1000, + "name": "raw_p7", + "nested_width_bits": 17504, + "normalized_cost_agreement": true, + "observed_flow_changes": 5, + "paid": { + "1": 37305, + "2": 10695, + "3": 3360, + "4": 1530, + "5": 300, + "8": 1464, + "16": 448, + "32": 448, + "48": 448 + }, + "rank_primes": [ + 2, + 3, + 5, + 7, + 11, + 19, + 41 + ], + "semigroup_plateaus": 8, + "sharp_divisor_bits": 59923, + "sharp_divisor_sha256": "de052653fd92327df3b3210059aee9225a5774e17ebe3ef37ce44266577af04a", + "smooth_box": 32, + "source_representation_comparisons": 8, + "targets": { + "5": 420, + "6": 270, + "7": 840, + "8": 1395, + "9": 3195, + "25": 448, + "41": 448, + "57": 448, + "121": 224 + }, + "tau": 363, + "width_sequence_sha256": "79f9cf98c28c5c68ce21ff685ac9f7b742ff96a5e5f99aa0e46fb482f90ba0ed" + }, + { + "all_rank_statement_source": "README.md symbolic proof; finite checks are witnesses only", + "chronological_constraints": 198, + "coarse_depth_bound": 12, + "distinct_source_counts": 1, + "explicit_log2_upper_bound": 60, + "largest_chain_depth": 5, + "largest_observed_plateau_visits": 1, + "least_width_bits": 1, + "maximum_rank": 100, + "name": "unit_width_degenerate", + "nested_width_bits": 1, + "normalized_cost_agreement": true, + "observed_flow_changes": 6, + "paid": { + "1": 1 + }, + "rank_primes": [ + 2 + ], + "semigroup_plateaus": 6, + "sharp_divisor_bits": 1, + "sharp_divisor_sha256": "bd87b2cda99df5b642ac9c0a97d3bc76f9921e2cce16058faa44bc954dbb065f", + "smooth_box": 6, + "source_representation_comparisons": 50, + "targets": { + "2": 1 + }, + "tau": 2, + "width_sequence_sha256": "e5bc4cf93627b9767c8a8b04473fd518a614255aacb37e8bf81d48f88c57d4ef" + } + ], + "claim_type": "conditional uniform width theorem", + "no_new_kappa": true, + "rejected_controls": [ + { + "cap": 3, + "name": "omit_paid_generator", + "source_counts": [ + 3, + 4 + ] + }, + { + "n": 50, + "n_over_m": 10, + "name": "changed_height_breaks_source_bound", + "source_rank": 4 + }, + { + "cut_count": 1, + "cut_rank": 8, + "name": "aggregate_pooling_not_admitted", + "pooled": 175, + "required": 700 + }, + { + "name": "omit_required_source_prime", + "prime": 5, + "rank": 3, + "width": 5 + } + ], + "schema": "chronological-width-bound/v1", + "source_sha256": { + "research/chronological-batch-width/README.md": "0cf276c77016a98a0dabba822d27bb9cb94c0bf86ec353a16499fe85e6032c20", + "research/chronological-batch-width/RESULT.json": "2750ea29f5d9d40aac5d97f1c4aa6482b5315003a9b50d1a21afae81b86d739a", + "research/chronological-batch-width/batches.py": "73e7ab4a1925ee7d412d0f2b5d28b70f3a9e43e427c2ec6f6d89f193b84655ef", + "research/direct-mixed-flow/README.md": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8", + "research/direct-mixed-flow/flow.py": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a", + "research/higher-moment-strictification/RESULT.json": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156" + }, + "theorem": "For a fixed default-height rule, log B_N = O((log N)^(d+1)); see symbolic proof." +} diff --git a/research/chronological-width-bound/SOURCES.json b/research/chronological-width-bound/SOURCES.json new file mode 100644 index 0000000000..a14046d14e --- /dev/null +++ b/research/chronological-width-bound/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/chronological-batch-width/README.md", + "usage": "input", + "git_blob": "c85304a601f858774f425d5f3869ac0a6f85ec29", + "sha256": "0cf276c77016a98a0dabba822d27bb9cb94c0bf86ec353a16499fe85e6032c20" + }, + { + "path": "research/chronological-batch-width/RESULT.json", + "usage": "input", + "git_blob": "2dd0cda6507acf81f72603151de62826a90a4fe5", + "sha256": "2750ea29f5d9d40aac5d97f1c4aa6482b5315003a9b50d1a21afae81b86d739a" + }, + { + "path": "research/chronological-batch-width/batches.py", + "usage": "input", + "git_blob": "98feaef4156223829971089765bd483518c3b754", + "sha256": "73e7ab4a1925ee7d412d0f2b5d28b70f3a9e43e427c2ec6f6d89f193b84655ef" + }, + { + "path": "research/direct-mixed-flow/README.md", + "usage": "input", + "git_blob": "3be00f754b9ffa23e64b3eafe7706e3ac139993a", + "sha256": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8" + }, + { + "path": "research/direct-mixed-flow/flow.py", + "usage": "input", + "git_blob": "07175cd6e1f2c2367c2e78eca7f163fef18d301d", + "sha256": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a" + }, + { + "path": "research/higher-moment-strictification/RESULT.json", + "usage": "input", + "git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a", + "sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156" + } + ] +} diff --git a/research/chronological-width-bound/TASK.json b/research/chronological-width-bound/TASK.json new file mode 100644 index 0000000000..e21d45366a --- /dev/null +++ b/research/chronological-width-bound/TASK.json @@ -0,0 +1,132 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "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": "Default-height part of one combined width contribution: sharpen PR #4586's log B_N=O((1+log N)^(d+2)) to d+1 for #4507's least chronological widths on #4436's fixed default-height flow, using bounded per-plateau visits. The companion adaptive-chronological-batching package supplies arbitrary-height cut transfer and a conditional all-rank envelope; the two scientific replays remain separate.", + "scope_change_reason": "Originally take Discussion4503 / PR4507 open question1 after handoff-first overlap review instead of the independent-moment card. Consolidation credits #4586's existing quasipolynomial proof and #4588's independent finite default checks; #4591 checks arbitrary-height aggregate identities, not the companion's actual cut divisibility. This is width-resource growth, not a new batching algorithm or unchanged invoice recomputation.", + "bottleneck_link": "The integer compiler requires finite productive widths and batch integrality. A quantified width bound strengthens its resource accounting without assuming a new supplier saving.", + "budget_minutes": 120, + "stop_rule": "Stop on a source-count plateau or recursive-contraction counterexample; do not infer an asymptotic bound from finite scans or extend it to changed heights without a new proof.", + "outcome": "completed", + "evidence": "README.md gives a symbolic all-rank proof. RESULT.json records five fixtures, 102215 chronological constraints, exact integer divisibility and four boundary controls. Runtime and metadata verification remain distinct from human or formal acceptance.", + "author": "codyw912", + "ai_assistance": "Substantial OpenAI assistance in theorem, implementation and writing; separate Anthropic-model mathematical challenge supplied the sharper plateau-visit argument. No human or proof-kernel verification claimed.", + "coordination": { + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4503", + "publication": "LOCAL-ONLY; Discussion mutation returned HTTP403 and branch awaits donor approval", + "upstream_checked_utc": "2026-10-22T03:30:00Z", + "overlap_checked_utc": "2026-10-22T04:01:35Z", + "overlap_coverage": "5860 tracked local note paths complete, 317 open PRs and 3412 Discussion records with complete pagination; no fresh closed-PR or diff search", + "nearest_overlap": ["PR4507 least policy and finite widths", "PR4519 independent finite recount", "PR4521 expanded instance counts", "PR4483 changed-height convergence, excluded here"], + "companion_package": "research/adaptive-chronological-batching", + "publication_scope": "One combined PR with two scoped replay packages; local-only pending publication approval", + "copied_from_commit": "099267b65810ebe095076e211b74beeed5575b25", + "consolidation_main_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "selection_context": "Historical base/card/pins unchanged; live comparison selected conditional kappa .00302015 from #4470, not #4483 or #4507. No selected-frontier edit.", + "consolidation_overlap_coverage": "2026-10-22: 408 open PRs at 13:08:38UTC, 3852 closed PRs at 13:09:39UTC, 3577 Discussion records at 13:09:11UTC; complete reported pagination, non-atomic snapshot, not exhaustive novelty proof. Earlier overlap timestamps and coverage above remain historical provenance.", + "consolidation_nearest_overlap": [ + "PR4586 aadb7bc59390683450b1969e4632f546929dc569: existing default d+2 proof; this package sharpens to d+1", + "PR4588 2f6578907b7f8718a13921552cc3069d3908e936: independent finite default checks", + "PR4591 84c0fb3a39bcb1e4b8c48892bfdd8a6e7ae58a50: arbitrary-height aggregate identities, not actual cut divisibility" + ], + "specialization_boundary": "Companion symbolic M=kmin,g=1 gives d'=d,z=0; its positive-a,b adaptive interface has g>=2. Default root nonemptiness needs no paid rank one, unlike the sufficient premise of adaptive WIDTH.md. Plateau-product and level-LCM divisors differ; no universal numerical dominance." + }, + "open_questions": [ + { + "question": "Can the exponent-lattice dimension sharpen the logarithmic degree?", + "why_it_matters": "The prime-exponent box may overcount attainable plateau locations.", + "first_step": "Bound the integer lattice generated by the actual rank exponent vectors, with explicit constants.", + "blocked_by": "No tight width lower bound or source-valuation distribution is established." + }, + { + "question": "Can the companion's conditional adaptive width envelope be sharpened?", + "why_it_matters": "adaptive-chronological-batching/WIDTH.md now supplies the arbitrary-height root/decrement and level-visit proof, but not tight growth or physical admission.", + "first_step": "Retain actual gcd savings or rigorously narrow the semigroup count for one fixed authenticated geometry.", + "blocked_by": "The default fixed-contraction proof still fails for small root sources, as the rank50 control demonstrates; no tight lower bound is established." + }, + { + "question": "Which physical constants inherit this improved width?", + "why_it_matters": "Productive width alone does not price encoded routing, stock or precision.", + "first_step": "Substitute the bound into one pinned emitted compiler's complete owned-state and routing ledger.", + "blocked_by": "Native, tape, analytic and recovery obligations remain inherited." + } + ] +} diff --git a/research/chronological-width-bound/VERIFY.json b/research/chronological-width-bound/VERIFY.json new file mode 100644 index 0000000000..31edf780bb --- /dev/null +++ b/research/chronological-width-bound/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/chronological-batch-width/README.md", + "research/chronological-batch-width/RESULT.json", + "research/chronological-batch-width/batches.py", + "research/direct-mixed-flow/README.md", + "research/direct-mixed-flow/flow.py", + "research/higher-moment-strictification/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact semigroup plateaus, contraction, source bounds, chain/valuation envelopes, all-prime divisibility and four boundary controls on five fixed-rule fixtures. The retained compiler checks normalized leaf costs against its nested construction by exact cross-products, not an independent rational recurrence; cut correctness is inherited from the predecessor's literal fixtures. The uniform claim is proved symbolically in README.md." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Repeat the exact scientific witness checks with assertions disabled and isolated Python imports." + } + ] +} diff --git a/research/chronological-width-bound/verify.py b/research/chronological-width-bound/verify.py new file mode 100755 index 0000000000..3c826a436d --- /dev/null +++ b/research/chronological-width-bound/verify.py @@ -0,0 +1,322 @@ +#!/usr/bin/env python3 +"""Exact witnesses for a uniform width theorem, not an asymptotic experiment. + +The chronological flow and least-width implementation are authenticated +predecessor inputs. New plateau, contraction and divisibility checks below +exercise the hypotheses of the written proof; they do not prove it by census. +Prepared for codyw912 with substantial OpenAI and Anthropic assistance. +Apache-2.0. +""" + +from bisect import bisect_right +from collections import Counter +from hashlib import sha256 +from math import gcd, lcm, prod +from pathlib import Path +from types import ModuleType +import argparse +import json + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticated_sources(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + pins = {} + for row in sources["files"]: + if row["usage"] != "input": + continue + raw = (ROOT / row["path"]).read_bytes() + require(sha256(raw).hexdigest() == row["sha256"], "Source bytes: " + row["path"]) + pins[row["path"]] = raw + return pins + + +def load(pins, relative, name): + raw = pins[relative] + module = ModuleType(name) + module.__file__ = str(ROOT / relative) + exec(compile(raw, module.__file__, "exec"), module.__dict__) + return module + + +def floor_log(n, base=2): + require(type(n) is int and n >= 1 and type(base) is int and base >= 2, + "Positive logarithm domain") + exponent = 0 + while n >= base: + n //= base + exponent += 1 + return exponent + + +def ceil_log2(n): + require(type(n) is int and n >= 1, "Positive logarithm domain") + return (n - 1).bit_length() + + +def prime_support(ranks): + result = set() + for rank in ranks: + require(type(rank) is int and rank >= 1, "Positive integer rank") + p = 2 + while p * p <= rank: + while rank % p == 0: + result.add(p) + rank //= p + p += 1 + if rank > 1: + result.add(rank) + return sorted(result) + + +def semigroup(ranks, cap): + """Enumerate distinct products, not prime-smooth numbers outside the rule.""" + require(cap >= 1, "Positive cap") + generators = sorted(set(r for r in ranks if r > 1)) + require(generators, "Nontrivial target generator") + seen, stack = {1}, [1] + while stack: + x = stack.pop() + for r in generators: + if r > cap // x: + break + y = r * x + if y not in seen: + seen.add(y) + stack.append(y) + return sorted(seen) + + +def signature(flow): + """Full compressed chronological inventory, including per-cut repetitions.""" + return ( + tuple(sorted(flow["sources"].items())), + tuple(sorted(flow["exits"].items())), + tuple(sorted(flow["boundary_exits"].items())), + tuple(tuple(sorted(cut.items())) for cut in flow["cuts"]), + flow["height"], flow["units"], flow["column_mass"], flow["matched_jobs"], + ) + + +def valuation(n, p): + require(n >= 1 and p >= 2, "Valuation domain") + exponent = 0 + while n % p == 0: + exponent += 1 + n //= p + return exponent + + +def digest_integers(values): + digest = sha256() + for value in values: + raw = value.to_bytes(max(1, (value.bit_length() + 7) // 8), "big") + digest.update(len(raw).to_bytes(8, "big")) + digest.update(raw) + return digest.hexdigest() + + +def verify_case(name, targets, paid, maximum, batches, original): + m, kmin = max(targets), min(targets) + W, P = sum(targets.values()), sum(paid.values()) + cap = maximum // m + gamma = semigroup(set(targets) | set(paid), cap) + primes = prime_support(set(targets) | set(paid)) + smooth_box = prod(1 + floor_log(cap, p) for p in primes) + require(len(gamma) <= smooth_box, "Smooth exponent-box bound") + tau = m * ceil_log2(kmin) + require(2 * (m - 1) ** m < m ** m, "Integer block contraction") + + by_cap, starts, changes = {}, {}, [] + prior_signature = None + predecessor_comparisons = 0 + for c in range(1, cap + 1): + flow = batches.direct_flow(targets, paid, m * c) + current = signature(flow) + if current != prior_signature: + require(c in gamma, "Flow changes only at rank-semigroup thresholds") + changes.append(c) + if c in gamma: + starts[c] = sum(flow["sources"].values()) + source_count = sum(flow["sources"].values()) + require(W <= source_count <= W * (W + P) ** flow["height"], + "Source count bounds include all paid multiplicities") + require(flow["height"] == floor_log(c, kmin), "Default height") + plateau = gamma[bisect_right(gamma, c) - 1] + require(source_count == starts[plateau], "Constant source count on plateau") + # The older exponent-vector implementation does not aggregate collisions + # before matching. Compare it with the polynomial predecessor explicitly. + older = original.Flow(targets, paid, m * c).merged() + for key in ("sources", "exits", "boundary_exits", "units", "column_mass", "matched_jobs"): + require(flow[key] == older[key], "Two source representations: " + key) + predecessor_comparisons += 1 + # Bound retained functools caches; no source file or algorithm is altered. + for method in (original.Flow.column, original.Flow.points, + original.Flow.units, original.Flow.demand): + method.cache_clear() + by_cap[c] = flow + prior_signature = current + + compiled = batches.compile_widths(targets, paid, maximum) + widths = compiled["widths"] + product_bound = prod(starts.values()) ** tau + lcm_sources = lcm(*starts.values()) + depth_bound = m * (floor_log(maximum // m) + 1) + coarser_bound = lcm_sources ** depth_bound + # All values here are integers; the displayed log bound is an upper bound + # in bits, not a floating-point logarithm used for acceptance. + source_bits = ceil_log2(W) + floor_log(cap, kmin) * ceil_log2(W + P) + bit_bound = tau * smooth_box * source_bits + require(product_bound <= 1 << bit_bound, "Explicit logarithmic envelope") + + depths = [0] * m + visits = [{} for _ in range(m)] + valuation_primes = (2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31) + chains = {p: [0] * m for p in valuation_primes} + maximum_visit = 0 + exact_constraints = 0 + for n in range(m, maximum + 1): + flow = by_cap[n // m] + rows = batches.requirements(flow, n) + require(all(m * e <= (m - 1) * n for e, _ in rows), "Every child contracts") + require(all(m * (n - s) < (m - 1) * n for s in flow["sources"]), + "Strict complement contraction") + require(all(m * e <= max(paid) * n for e in flow["exits"]), + "Paid-exit contraction") + child_ranks = sorted(set(e for e, _ in rows)) + depth = 1 + max(depths[e] for e in child_ranks) + depths.append(depth) + require(depth <= m * (floor_log(n // m) + 1), "Integer chain-depth bound") + here = gamma[bisect_right(gamma, n // m) - 1] + counts = {} + for e in child_ranks: + for label, count in visits[e].items(): + counts[label] = max(counts.get(label, 0), count) + counts[here] = counts.get(here, 0) + 1 + visits.append(counts) + require(max(counts.values()) <= tau, "Bounded visits per plateau") + maximum_visit = max(maximum_visit, max(counts.values())) + S = sum(flow["sources"].values()) + for p in valuation_primes: + v = valuation(S, p) + max(chains[p][e] for e in child_ranks) + chains[p].append(v) + require(valuation(widths[n], p) <= v, "Width valuation bounded by a chain") + require(v <= tau * sum(valuation(s, p) for s in starts.values()), + "Plateau valuation envelope") + require(v <= depth * max(valuation(s, p) for s in starts.values()), + "Coarse valuation envelope") + require(product_bound % widths[n] == 0, "Sharp all-prime divisor") + require(coarser_bound % widths[n] == 0, "Coarse all-prime divisor") + exact_constraints += len(rows) + + require(compiled["nested_widths"][-1] % widths[-1] == 0, + "Predecessor nested width is a multiple") + return { + "name": name, "maximum_rank": maximum, "targets": targets, "paid": paid, + "rank_primes": primes, "semigroup_plateaus": len(gamma), + "observed_flow_changes": len(changes), "distinct_source_counts": len(set(starts.values())), + "smooth_box": smooth_box, "tau": tau, "largest_observed_plateau_visits": maximum_visit, + "largest_chain_depth": max(depths), "coarse_depth_bound": depth_bound, + "source_representation_comparisons": predecessor_comparisons, + "chronological_constraints": exact_constraints, + "least_width_bits": widths[-1].bit_length(), + "nested_width_bits": compiled["nested_widths"][-1].bit_length(), + "sharp_divisor_bits": product_bound.bit_length(), + "explicit_log2_upper_bound": bit_bound, + "width_sequence_sha256": digest_integers(widths), + "sharp_divisor_sha256": digest_integers([product_bound]), + "normalized_cost_agreement": True, + "all_rank_statement_source": "README.md symbolic proof; finite checks are witnesses only", + } + + +def rejection_controls(batches, original): + controls = [] + targets, paid = {2: 1, 5: 1}, {1: 1, 3: 1} + before, after = (batches.direct_flow(targets, paid, 5 * c) for c in (2, 3)) + require(3 not in semigroup(targets, 3) and signature(before) != signature(after), + "Omitting paid generators must miss an actual threshold") + controls.append({"name": "omit_paid_generator", "cap": 3, + "source_counts": [sum(before["sources"].values()), sum(after["sources"].values())]}) + + shifted = original.Flow({2: 1, 5: 1}, {1: 2, 4: 1}, 50, height_base=5).merged() + require(not shifted["all_sources_above_n_over_m"] and 4 in shifted["sources"], + "Changed height invalidates the default source premise") + controls.append({"name": "changed_height_breaks_source_bound", "n": 50, + "source_rank": 4, "n_over_m": 10}) + + one = batches.direct_flow({2: 4, 3: 1}, {1: 6, 2: 2}, 12) + compiled = batches.compile_widths({2: 4, 3: 1}, {1: 6, 2: 2}, 12) + a = batches.multiplier(compiled["widths"], batches.requirements(one, 12)) + pooled = batches.multiplier(compiled["widths"], batches.requirements(one, 12, True)) + bad = next(c for c in one["cuts"] if pooled * c["count"] % compiled["widths"][c["rank"]]) + require(pooled == 175 and a == 700, "Frozen chronological counterexample") + controls.append({"name": "aggregate_pooling_not_admitted", "pooled": pooled, + "required": a, "cut_rank": bad["rank"], "cut_count": bad["count"]}) + + small = batches.compile_widths({2: 4, 3: 1}, {1: 6, 2: 2}, 12)["widths"] + require(any(B % 5 == 0 for B in small), "Nontrivial prime in actual width") + # A claimed all-prime divisor with every factor 5 erased cannot bound even + # the smallest width-5 instance, regardless of passing other prime checks. + sources = [sum(batches.direct_flow({2: 4, 3: 1}, {1: 6, 2: 2}, 3 * c)["sources"].values()) + for c in semigroup({1, 2, 3}, 4)] + sharp = prod(sources) ** 3 + erased = sharp // (5 ** valuation(sharp, 5)) + require(erased % small[3] != 0, "Deleting required prime must reject") + controls.append({"name": "omit_required_source_prime", "prime": 5, "rank": 3, + "width": small[3]}) + for method in (original.Flow.column, original.Flow.points, + original.Flow.units, original.Flow.demand): + method.cache_clear() + return controls + + +def run(): + pins = authenticated_sources() + batches = load(pins, "research/chronological-batch-width/batches.py", "frozen_batches") + original = load(pins, "research/direct-mixed-flow/flow.py", "frozen_direct_flow") + raw = json.loads(pins["research/higher-moment-strictification/RESULT.json"])["invoice_oracle"] + raw_targets = {int(k): v for k, v in raw["targets"].items()} + raw_paid = {int(k): v for k, v in raw["paid"].items()} + cases = [ + ("overlapping_two_rank", {2: 1, 5: 1}, {1: 2, 4: 1}, 1000), + ("chronology_counterexample_family", {2: 4, 3: 1}, {1: 6, 2: 2}, 1000), + ("product_collisions", {2: 1, 4: 1, 8: 1}, {1: 2, 3: 1, 7: 1}, 300), + ("raw_p7", raw_targets, raw_paid, 1000), + ("unit_width_degenerate", {2: 1}, {1: 1}, 100), + ] + reports = [verify_case(*case, batches, original) for case in cases] + controls = rejection_controls(batches, original) + return {"schema": "chronological-width-bound/v1", "claim_type": "conditional uniform width theorem", + "no_new_kappa": True, "source_sha256": {k: sha256(v).hexdigest() for k, v in pins.items()}, + "cases": reports, "rejected_controls": controls, + "theorem": "For a fixed default-height rule, log B_N = O((log N)^(d+1)); see symbolic proof."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="Regenerate this package's own receipt") + args = parser.parse_args() + report = run() + encoded = json.dumps(report, indent=2, sort_keys=True) + "\n" + path = HERE / "RESULT.json" + if args.write: + path.write_text(encoded) + else: + require(json.loads(path.read_text()) == json.loads(encoded), "Committed receipt equality") + print("PASS_CHRONOLOGICAL_WIDTH_BOUND", json.dumps({ + "cases": len(report["cases"]), + "constraints": sum(c["chronological_constraints"] for c in report["cases"]), + "controls": len(report["rejected_controls"]), "no_new_kappa": True, + }, sort_keys=True)) + + +if __name__ == "__main__": + main()