From 8a813ca337e56ffe7f5e5f6f0dbd3ee55f4e8ad9 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Thu, 22 Oct 2026 13:53:03 +0000 Subject: [PATCH] Prove one shared-arena CRT axis fits the evaluator allowance. The PR #4192 scan, with one schoolbook product per tape action and the one-axis CRT bill, stays inside 2^{4 ell}(p+2)^{16}. The same charge on all 8(p+2) axes exceeds that allowance at p=2, ell=2. Co-authored-by: unpaidmoon --- research/crt-arena-root-axis/PROOF.md | 220 ++++++++++++++ research/crt-arena-root-axis/README.md | 83 +++++ research/crt-arena-root-axis/SOURCES.json | 30 ++ research/crt-arena-root-axis/TASK.json | 80 +++++ research/crt-arena-root-axis/VERIFY.json | 21 ++ research/crt-arena-root-axis/vendor/NOTICE.md | 9 + .../vendor/pr4192-crt-benes-scan-PROOF.md | 258 ++++++++++++++++ research/crt-arena-root-axis/verify.py | 284 ++++++++++++++++++ 8 files changed, 985 insertions(+) create mode 100644 research/crt-arena-root-axis/PROOF.md create mode 100644 research/crt-arena-root-axis/README.md create mode 100644 research/crt-arena-root-axis/SOURCES.json create mode 100644 research/crt-arena-root-axis/TASK.json create mode 100644 research/crt-arena-root-axis/VERIFY.json create mode 100644 research/crt-arena-root-axis/vendor/NOTICE.md create mode 100644 research/crt-arena-root-axis/vendor/pr4192-crt-benes-scan-PROOF.md create mode 100644 research/crt-arena-root-axis/verify.py diff --git a/research/crt-arena-root-axis/PROOF.md b/research/crt-arena-root-axis/PROOF.md new file mode 100644 index 0000000000..e2f7a81d53 --- /dev/null +++ b/research/crt-arena-root-axis/PROOF.md @@ -0,0 +1,220 @@ +# One root axis on a shared Beneš arena + +This is a counting proof for the shared-arena schedule left open by +`research/crt-uniform-evaluator`. It does not accept PR #4100, it does not +change κ, and it does not replace that package's per-table bound for a whole +batch of axes. + +## Proposition + +For all integers `p >= 2` and `1 <= h <= ell <= p`, write `q = p + 2`, +`N = 2^h` and `w = 4q`. One root axis, reconstructed by the pinned evaluator's +one-axis CRT bill and then compiled as four shared-arena networks, uses at +most + +```text +E(p, ell) = 2^{4 ell} q^{16} +``` + +bit-steps. The four networks are the forward rotation, the inverse rotation, +and the same pair for the inverse macro. Each network is the PR #4192 arena +on `N` wires, followed by one protected bit query. Beside every tape action +in that arena invoice, the scalar control may perform one `w`-bit by `w`-bit +schoolbook product. + +The same explicit charge, repeated for all `8q` axes, exceeds `E` at +`p = 2`, `ell = 2`, `h = 2`. The per-table evaluator already fits that batch +by a different scan. This note does not transfer its constant to the batch +under the arena charge. + +## Predecessor sentences + +The one-axis reconstruction bill is the evaluator's substitution +`m <= 8q`, `W <= 8q`: + +```text +65536 q^3 + 1024 q ell^3 + 1024 q^2. +``` + +Across `A <= 8q` axes that file multiplies the bill by `8q` and obtains +`524288 q^4 + 8192 q^2 ell^3 + 8192 q^3`. Writing one rotation table costs at +most `9(ell + 2)^2` bit-steps per wire. A schoolbook product of an `a`-bit +integer by a `b`-bit integer costs at most `8ab` bit-steps. + +PR #4192, at commit `519d811cc48693ad9969d6d7994bef3940167005`, fixes the +arena geometry. The unmodified proof is +`vendor/pr4192-crt-benes-scan-PROOF.md` (SHA256 +`c3eb4e14dc5ee0102cbf77c4a0e61db9989c2b8a0eaf7f0659a6e39373197474`). +It sets every record field to `w = 4p + 8` bits, hence `w = 4q`, and + +```text +J = N(h^2 + 3h + 1), B = 5 w J. +``` + +One logical access performs exactly `26 w J + 25 w` tape actions. +Initialization and erasure add `6B = 30 w J`. The protected input costs +`3 N h`. Owned output costs `3(2h - 1)N`, and one query costs +`3(2h - 1)N + 3`. The access census satisfies + +```text +A <= N^2 + 2 N h^2 + 24 N h + 3 N. +``` + +That file's uniform bound is `O((A + J + 1) B (p + 2)^2)` after charging +each scalar instruction `O(w^2)`. The leading piece of the charge below is +exactly that shape with coefficient `3328/5`: + +```text +8 w^2 * A * (26 w J) = (3328/5) A B q^2. +``` + +## The explicit bill + +For one network let + +```text +T_tape = A (26 w J + 25 w) + 30 w J + 3 N h + 6(2h - 1) N + 3, +T_scalar = 8 w^2 T_tape, +T_rot = 9 (ell + 2)^2 N. +``` + +`8 w^2` is the schoolbook cap at equal lengths. The touch formula in the +pinned evaluator is `3ab + 3a + b`; at `a = b = w >= 1` this is +`3w^2 + 4w <= 8w^2`, because `4 <= 5w`. The `w = 0` comparison `4 <= 0` is +false, so the cap is stated only for a positive width. + +One axis with four networks is + +```text +U = T_crt + 4 (T_rot + T_tape + T_scalar), +T_crt = 65536 q^3 + 1024 q ell^3 + 1024 q^2. +``` + +## Lemmas used for every admissible pair + +Write `N = 2^h` and `poly(h) = 2h^2 + 24h + 3`, so `A = N^2 + N poly(h)`. + +1. `poly(h+1) = poly(h) + 4h + 26`, because + `2(h+1)^2 - 2h^2 = 4h + 2` and `24(h+1) - 24h = 24`. + Directly, `poly(1) <= 30`, `poly(2) <= 60` and `poly(3) <= 120`. + For `h >= 3`, `4h + 26 <= 15 * 2^h`: the `h = 3` value is `38 <= 120`, + and `4(h+1) + 26 = 4h + 30 <= 15 * 2^h + 4 <= 30 * 2^h` once + `4 <= 15 * 2^h`. Thus `poly(h) <= 15 * 2^h` and `A <= 16 N^2` for every + integer `h >= 1`. + +2. `h^2 + 3h + 1 <= 5 h^2` because `(h - 1)(4h + 1) = 4h^2 - 3h - 1 >= 0` + for every integer `h >= 1`. Hence `J <= 5 N h^2`. At `h = 1`, `J = 10` + and `A >= 4`. + +3. The displayed exact census `(37 N h - 35 N) / 2` is at most the + convenient linear term `24 N h + 3 N`, because `11h + 41 > 0`. + +4. `15 h <= 16 * 4^h` for `h >= 1`. The base is `15 <= 64`. The step uses + `15 <= 48 * 4^h`, so `15(h+1) <= 16 * 4^h + 15 <= 64 * 4^h`. + +5. The tail `3 N h + 6(2h - 1)N + 3 = 15 N h - 6 N + 3` is at most + `15 N h` for `N >= 1`. Combined with `A >= N^2`, `J >= N` and `w >= 16`, + `15 N h <= A J w`. Also `J >= 10` gives `25 A <= (5/2) A J`, and + `A >= 4` gives `30 J <= (15/2) A J`, so + +```text +26 A J + 25 A + 30 J <= 36 A J, +T_tape <= 37 A J w. +``` + +6. `1 + 8 w^2 = 1 + 128 q^2 <= 129 q^2`. For `h + 2 <= q`, + `T_rot <= 9 q^2 N` at `ell = h`. Therefore one network is at most + `9 q^2 N + 19092 q^3 A J`, four networks are at most + `36 q^2 N + 76368 q^3 A J`, and `A J <= 80 N^3 h^2` gives + +```text +4 (T_rot + T_tape + T_scalar) <= 36 q^2 N + 6109440 q^3 N^3 h^2. +``` + +7. For `0 <= ell <= q - 2` and `q >= 4`, + `65536 q^3 <= 16384 q^4` and `1024 q^2 <= 64 q^4`, while + `1024 q ell^3 <= 1024 q^4`. Hence `T_crt <= 17472 q^4`. + +At `ell = h >= 2` and `q >= h + 2` (so `q >= 4`), + +```text +U <= 17472 q^4 + 36 q^2 N + 6109440 q^3 N^3 h^2. +``` + +Each of those three terms is at most one third of `2^{4h} q^{16}`. The first +two are smallest at `N = 4`, `q = 4`, where `52416 <= 2^{32}` and +`108 <= 2^{34}`, and both right-hand sides grow with `N` and `q`. The third +is `18328320 h^2 <= 2^h (h + 2)^{13}`. This holds at `h = 2` and `h = 3` by +direct powers. At `h = 4` it is `18328320 <= 6^{13}`. For `h >= 4` the +function `r(h) = 2^h (h+2)^{13} / h^2` is strictly increasing, because + +```text +r(h+1) / r(h) >= 2 (h / (h+1))^2 >= 32/25 > 1. +``` + +The middle comparison is `h >= 4`. Thus the majorant is at most the allowance +for every integer `h >= 2` and `q >= h + 2`. + +## The height-one line, and a longer modulus + +At `h = 1` the same polynomials give + +```text +U = 36868096 q^3 + 11776 q^2 + 288544 q + 732 + <= 37169148 q^3 +``` + +when `ell = 1`. For `q >= 4`, `37169148 <= 16 q^{13}`, so +`U <= 16 q^{16} = 2^{4} q^{16}`. + +For a longer modulus, fix `h` and `q` and raise `ell`. The parts of `U` that +depend on `ell` are `1024 q ell^3` and `36 N (ell + 2)^2`. For `ell >= 1`, + +```text +(ell+1)^3 - 16 ell^3 <= -8 ell^3 < 0, +(ell+3)^2 - 16 (ell+2)^2 = -15 ell^2 - 58 ell - 55 < 0, +``` + +and the `ell`-independent part `S` satisfies `-15 S < 0`. Therefore +`U(ell+1) < 16 U(ell)`. The allowance multiplies by exactly 16. Starting from +`ell = h`, every larger admissible `ell` stays inside the allowance. + +Every triple `p >= 2`, `1 <= h <= ell <= p` has `q = p + 2 >= 4` and +`q >= ell + 2 >= h + 2`. The height-one cubic or the `h >= 2` majorant covers +`ell = h`, and the step covers `ell > h`. + +## Two evaluated witnesses + +At `p = 2`, `ell = 2`, `h = 2` (`q = 4`, `N = 4`): + +```text +U = 38809248652, +E = 2^{40} = 1099511627776, +28 U <= E < 29 U. +``` + +On the box `h = 1..8`, `ell = h`, and the four values of `q` beginning at +`max(4, h+2)`, this pair has the largest ratio `U / E`. That box is a check. +The proof is the induction above. + +The same formulas with `32 = 8q` axes give + +```text +U_batch = 1241895956864 > E. +``` + +So this per-action schoolbook majorant fits one axis and does not fit the +whole displayed batch. The factor `8q` on the CRT term alone reproduces the +evaluator's six-term CRT display; the excess comes from repeating the arena, +not from the reconstruction. + +## What this does not prove + +Reservoir placement, the ordinary interchange callee, sparse repair, native +execution, and the outer multiplication theorem stay out of scope. The arena +is charged from the predecessor's census and tape formulas; this package does +not execute PR #4192's simulator or the retained Beneš compiler. The scalar +term is an explicit majorant large enough to cover one schoolbook product per +tape action. A tighter word-operation inventory could change the batch +comparison. No new κ is selected. The selected conditional value remains +`60403/20000000 = 0.00302015`. diff --git a/research/crt-arena-root-axis/README.md b/research/crt-arena-root-axis/README.md new file mode 100644 index 0000000000..46e9d3b64c --- /dev/null +++ b/research/crt-arena-root-axis/README.md @@ -0,0 +1,83 @@ +# One root axis on a shared Beneš arena + +**Scoped counting proof. No new κ.** The selected conditional exponent stays +`60403/20000000 = 0.00302015`. + +## Scope and evidence + +Original card: `uniform-transfer-audit`, refined to one open question of the +uniform CRT evaluator. That package proves + +```text +E(p, ell) <= 2^{4 ell} (p+2)^{16} +``` + +for per-table scans, with constant `C = 1`, and asks whether one root-axis +query still fits the same allowance when every logical access scans a single +shared arena, as in PR #4192, after the CRT offset is included. + +[PROOF.md](PROOF.md) answers that question for one axis. The axis pays the +pinned one-axis CRT bill, writes four rotation tables, and compiles each +table on the PR #4192 arena, including one protected bit query per network. +Every arena tape action may also pay one schoolbook product of two `w`-bit +words, `w = 4(p+2)`. For every integer `p >= 2` and `1 <= h <= ell <= p`, +the sum is at most `2^{4 ell} (p+2)^{16}`. + +The same charge on all `8(p+2)` axes exceeds the allowance at `p = 2`, +`ell = 2`, `h = 2`: `1241895956864 > 1099511627776`. The per-table proof +already covers that batch by a different schedule. This package does not move +that constant onto the simultaneous arena batch. + +At that same one-axis point the bill is `38809248652` against +`1099511627776`, and `28 U <= E < 29 U`. + +Reservoir placement, the ordinary callee, sparse repair, native execution and +the outer theorem are not proved. The arena simulator and the retained Beneš +compiler are not executed. The bit-step count is the counting argument. + +Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). +The selected record and catalogue are historical provenance. The PR #4192 +proof is not an ancestor of canonical main, so its bytes are the unmodified +vendor file +[vendor/pr4192-crt-benes-scan-PROOF.md](vendor/pr4192-crt-benes-scan-PROOF.md), +commit `519d811cc48693ad9969d6d7994bef3940167005`, SHA256 +`c3eb4e14dc5ee0102cbf77c4a0e61db9989c2b8a0eaf7f0659a6e39373197474`. +See [vendor/NOTICE.md](vendor/NOTICE.md). + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 scripts/research_package.py --package research/crt-arena-root-axis --check-only +python3.12 -B research/crt-arena-root-axis/verify.py +``` + +The verifier prints `PASS_CRT_ARENA_ROOT_AXIS`. + +## Open next questions + +1. Does a word-level scalar inventory, with a fixed number of `w`-bit + operations per arena record, bring all `8(p+2)` axes inside the same + allowance? The schoolbook-per-tape-action majorant does not: at `p = 2`, + `ell = 2` the 32-axis bill is `1241895956864`, above + `1099511627776`. The first step is to replace `8 w^2` per tape action by + the record comparisons named in PR #4192 §2 and repeat that comparison. + It is blocked here because that tighter inventory is not the theorem. +2. With one axis inside `E`, do the reservoir and the ordinary interchange + callee of `CRT.md` §3–§4 still fit their stated bills? The first step is + the `H >= G` comparison already named by `research/crt-uniform-evaluator`. + Placement geometry remains PR #4174 and is not an input here. + +## Credit + +Cinna Davis supplies the CRT construction and the shape of `E(p, ell)` in +PR #4100. `research/crt-uniform-evaluator` supplies the one-axis +reconstruction bill, the rotation-table tariff and the open question; that +package was prepared by unpaidmoon with Cursor Grok assistance. ToikY's +PR #4192 supplies the arena census, the tape invoice and the `O(w^2)` scalar +shape. The vendored proof is unmodified. The coverage map in PR #4311 records +the evaluator row this question continues. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No independent human review or proof-assistant acceptance is claimed. diff --git a/research/crt-arena-root-axis/SOURCES.json b/research/crt-arena-root-axis/SOURCES.json new file mode 100644 index 0000000000..1610a6b40a --- /dev/null +++ b/research/crt-arena-root-axis/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/crt-uniform-evaluator/PROOF.md", + "usage": "input", + "git_blob": "7175c780b63378963c00ea29d76a9d1d7f86bbf0", + "sha256": "a67dce487dfaf0f1748458cf052b85203654d63f84c4e362ae78fe1bae1a3d42" + }, + { + "path": "research/crt-uniform-evaluator/README.md", + "usage": "input", + "git_blob": "5b28a48bdc2ab7c9bb5e1103601ac0e9ff00ef14", + "sha256": "2328dd323a39f9b88677426c82ac538638ae3e40943fe3ca4c348d5c087a6aec" + } + ] +} diff --git a/research/crt-arena-root-axis/TASK.json b/research/crt-arena-root-axis/TASK.json new file mode 100644 index 0000000000..76895065d8 --- /dev/null +++ b/research/crt-arena-root-axis/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Does one root-axis query still fit 2^{4 ell}(p+2)^{16} when four rotation networks are compiled by the PR #4192 shared-arena scan, after the one-axis CRT bill is included, for every integer p >= 2 and 1 <= h <= ell <= p?", + "scope_change_reason": "The card asks for one quantified implication of #4100 at its caller. research/crt-uniform-evaluator already proves the per-table constant C=1 and leaves the shared-arena schedule open. This package takes that schedule for one root axis, including the four networks that axis builds and the one-axis CRT bill.", + "bottleneck_link": "PR #4100 pays E(p, ell) inside the CRT route. An explicit arena schedule that still fits that same E for one axis keeps the constant available for the scan PR #4192 describes. It does not select a new exponent. The same per-action charge does not fit all 8(p+2) axes at once.", + "budget_minutes": 60, + "stop_rule": "Stop after the one-axis four-network inequality and the explicit 8(p+2)-axis counterexample under the same charge. Do not price reservoir placement, the ordinary callee, or a new kappa.", + "outcome": "completed", + "evidence": "PROOF.md derives U <= 2^{4 ell}(p+2)^{16} for one axis and four arena networks, and shows the 32-axis bill at p=2, ell=2 exceeds that allowance. verify.py checks the inductions, source sentences, corner witnesses and the batch excess. It prints PASS_CRT_ARENA_ROOT_AXIS.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance with the proof, verifier and package text.", + "open_questions": [ + { + "question": "Does a word-level scalar inventory, with a fixed number of w-bit operations per arena record, bring all 8(p+2) axes inside 2^{4 ell}(p+2)^{16}?", + "why_it_matters": "The schoolbook-per-tape-action majorant fits one axis and exceeds the allowance on the full displayed batch at p=2, ell=2. A tighter inventory could change that batch comparison without changing the one-axis theorem.", + "first_step": "Replace 8 w^2 per tape action by the per-record comparisons in PR #4192 section 2 and compare the 8(p+2)-axis bill with 2^{4 ell}(p+2)^{16}.", + "blocked_by": "That tighter inventory is not proved in this package. The theorem uses one schoolbook product per tape action." + }, + { + "question": "With one arena axis inside E, do the reservoir placement and ordinary interchange callee of CRT.md sections 3-4 still fit their stated bills?", + "why_it_matters": "The evaluator constant is one factor in the CRT route. Placement and the callee can reintroduce an E-sized term.", + "first_step": "Check H >= G at G = 64(ell + ceil(log2(p+2))) on the size family in #4100, using C=1 for this one-axis arena bill.", + "blocked_by": "Placement geometry is PR #4174 and is not an input to this arena bill." + } + ] +} diff --git a/research/crt-arena-root-axis/VERIFY.json b/research/crt-arena-root-axis/VERIFY.json new file mode 100644 index 0000000000..b3dfaa01f8 --- /dev/null +++ b/research/crt-arena-root-axis/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-uniform-evaluator/PROOF.md", + "research/crt-uniform-evaluator/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source sentences, vendor SHA256, schoolbook cap, census inductions, majorant coefficients, height-one cubic, ell-step, corner 28 U <= E < 29 U, and the 32-axis excess at p=2, ell=2. A dropped 26wJ+25w sentence and the w=0 schoolbook cap are rejected." + } + ] +} diff --git a/research/crt-arena-root-axis/vendor/NOTICE.md b/research/crt-arena-root-axis/vendor/NOTICE.md new file mode 100644 index 0000000000..2ac7689183 --- /dev/null +++ b/research/crt-arena-root-axis/vendor/NOTICE.md @@ -0,0 +1,9 @@ +Unmodified copy of `research/crt-benes-scan/PROOF.md` from open pull request +#4192 (ToikY) at commit `519d811cc48693ad9969d6d7994bef3940167005`. + +SHA256: `c3eb4e14dc5ee0102cbf77c4a0e61db9989c2b8a0eaf7f0659a6e39373197474` + +That commit is not an ancestor of canonical main. The bytes are stored here so +a replay does not need the unmerged object. The file's own credit and +Apache-2.0 notice remain ToikY's and the predecessors named there. This +package does not change those bytes. diff --git a/research/crt-arena-root-axis/vendor/pr4192-crt-benes-scan-PROOF.md b/research/crt-arena-root-axis/vendor/pr4192-crt-benes-scan-PROOF.md new file mode 100644 index 0000000000..af1ea10b9d --- /dev/null +++ b/research/crt-arena-root-axis/vendor/pr4192-crt-benes-scan-PROOF.md @@ -0,0 +1,258 @@ +# Uniform sequential-arena Beneš compiler and queried bit + +This is a component audit of Cinna Davis's PR4100 `CRT.md:94–116` and +retained `check_batched_crt.py:12–50`. The original compiler, cycle +coloring and proposed full-scan simulation are predecessor work. This +note supplies a uniform encoded schedule, explicit arena traffic and +owned-output cleanup. It does not supply the complete CRT evaluator. + +## 1. Exact component interface + +Inputs use canonical self-delimiting binary encodings of positive integers +`h,p` (for example Elias gamma), of total O(log(p+2)) bits, with +`1<=h<=p`, and a **complete** permutation of `N=2^h` wires, as N +consecutive h-bit words on a protected sequential input tape. The +source tape is preserved. The program rejects repeated or out-of-range +entries; it does not call an uncharged sorting routine. + +The owned output contains `(2h-1)N` Boolean table entries in layer-major, +then wire-major order. The known layer schedule is + +``` +0,1,...,h-1,h-2,...,0. +``` + +A second interface takes that protected encoded network and `layer,address` +in fixed fields of widths `max(1,ceil(log2(2h-1)))` and h, respectively, +scans the whole network, and returns one owned bit. There are no arbitrary +leading-zero header strings or unbounded encodings within this input domain. +The finite simulator receives the decoded header integers; canonical header +decoding is part of the written uniform lowering, not executed microcode. +On successful calls all input/output heads return to their left markers. All private arena, +key and bounded-register workspace is cleared and returned. Uniform +parameters are read as data; no size-specific code, advice table or +random-access oracle is supplied. + +The alphabet is fixed: bit zero, bit one, blank and boundary markers. +The number of sequential tapes is fixed. A constant number of binary +registers and arithmetic scratch regions may occupy a fixed tape bank; +their widths are data, not new tapes or control states. +The owned output and owned queried-bit tape are fixed **roles**, reused +after their consumer transfers/clears the previous result. Python Tape +objects in the fixture model configurations, not newly allocated physical +tapes. A caller retaining many answers must serialize them to a fixed +output region and pay its additional copy/head movements. + +## 2. Flattened recursion and explicit stack + +Use binary-heap node IDs: root 1 and children `2v,2v+1`. Nodes at depth +`a=0,...,h-1` have size `m=N/2^a` and height `s=h-a`. Leaves have m=2. +For each node preallocate arrays P, INV and COLOR of m words and OUT +with `(2s-1)m` Boolean entries. Preallocate one shared N-entry DFS stack. +Every entry is a fixed-width record + +``` +(node,kind,layer,index,value), each field w=4p+8 bits. +``` + +Record kinds form a fixed finite set. No dictionary, object pointer, +host-index lookup or tape per node is part of this program. The record +layout is generated by fixed nested counter loops over depth, node, +kind, layer and index. There are exactly + +``` +J = N(h²+3h+1) records, +B = 5wJ arena cells. (1) +``` + +Indeed the all-node Boolean tables contribute `Nh²` entries, since +`sum_(s=1)^h (2s-1)=h²`; the three other arrays contribute `3Nh` +and the shared stack contributes N. All widths are explicit, including +unused padding in the Boolean values. + +Every logical get or put constructs its four-field key on **one reused +key tape**. It scans all J records from the left marker, compares all +four key words, reads or replaces the matching value, continues to the +end and returns the arena head. It returns the key head after each +comparison, then clears and returns that scratch tape. There is one +matching record. It may skip an unmatched value by w consecutive +right moves; this is not a jump to an addressed record. + +Copy the incoming permutation to root P. Process nodes in increasing +depth, using only bounded loop counters: + +1. Validate each node's P by range checks and pairwise distinctness. +2. For m=2, write its one identical-bit switch table and continue. +3. Otherwise build INV; then visit initial wires in increasing order. + For an uncolored wire assign color zero and push it on the shared + encoded stack. Pop in LIFO order and inspect neighbors, in this + order, `x XOR 1`, `INV[P[x] XOR 1]`. Mark a newly discovered vertex + before pushing it. Clear each popped stack entry immediately. +4. Write first/last tables and both child permutations, exactly as in + the retained compiler. + +No Python recursion stack is used by `compile_stream`. The graph DFS +stack is the explicit arena array; its top is a bounded register. +Each vertex is pushed and popped once, so capacity N suffices. +At the end of each node the stack is empty and its slots are cleared. + +Then process depths in decreasing order. Interleave each pair of +child tables using child `x mod 2` and child wire `floor(x/2)`; +write parent layers shifted up by one. Finally copy the entire root +table into the owned output using charged arena gets and sequential +output writes. Only **after** serialization erase the whole private +arena and return its head. There is no returned host list that silently +owns an uncharged network copy. + +## 3. Source equivalence and endpoint + +The two input-neighbor relations are perfect matchings. Their union +is a disjoint union of alternating even cycles, allowing parallel +matching edges. Opposite colors exist. Mark-before-push means each +vertex enters the stack once. The traversal order within a node is +the same as the source, so component orientation and every resulting +color agree exactly, not just up to an equivalent network. + +Every input pair and every output pair has one member of each color. +For each color c, `floor(x/2) -> floor(P[x]/2)` is therefore a +permutation on m/2 wires. This proves child validation and permits +induction. Distinct child calls share no state: replacing source DFS +recursion by top-down construction and bottom-up assembly preserves +the returned tables byte for byte. The first/last tables and child +selector use precisely the source formulas. + +Induction gives the desired permutation endpoint. First and last +tables are equal on the two wires of their target pair because +matching colors differ. An interior table inherits target independence +from its child: flipping its higher target bit preserves the selected +child parity. Thus each returned queried bit is independent of its +own active target bit. This is a theorem about the component; it +does not establish the full CRT caller's simultaneous target omission. + +## 4. Traffic, scalar lowering and quantified bound + +There are three separate statements: the **executed arena/key cell +invoice**, the **written bounded-scalar lowering**, and the resulting +**uniform asymptotic bit bound**. The Python simulator is not a +complete finite-state transition-table certificate. + +For a logical arena access, the arena/key tapes execute exactly + +``` +26wJ + 25w read/write/one-cell-head actions. (2) +``` + +Arena key reads cost `8wJ`; unmatched value skips plus the matching +read/write cost `wJ+w`; arena return costs `5wJ`. Key comparisons +read/return `12wJ`, and constructing/clearing/returning its key costs +24w. Sum these terms to obtain (2). Initialization and final arena +erasure/returns add `6B`. The modeled protected input read/return costs `3Nh`; +this excludes the host pre-admission length/bit-format checks. Their sequential +implementation is separately charged in the written scalar lowering below. +Owned network writing/return costs `3(2h-1)N`. Each complete query scan, +return and one-bit owned output costs exactly `3(2h-1)N+3` tape actions. +These exact numbers exclude scalar instruction work, not its cost. + +The finite simulator batches a contiguous block read/write/move by +charging the corresponding number of repeated one-cell operations. +Such methods advance from the current head only. An expanded one-cell +execution is checked against the batched version on the same case. +They have identical tape contents, heads and traffic. Byte slices used +to batch those moves are not indexed logical-array access instructions. + +To lower the remaining control, use a fixed bank of O(1) w-bit +registers with binary counters. Every integer comparison, copy, +increment, halving, parity/XOR, add, or schoolbook product used here +has a fixed sequential implementation in O(w²) time and O(w²) scratch, +including local head returns. Key equality is a streaming equality +flag, not an uncharged comparison of host strings. Input bit-format +checks, record construction, all loop/index/key generation and query +selection counters are charged by the same conservative envelope. +The Python integer mirrors are observations of this bounded control; +they are not treated as unit-cost machine arithmetic. +The bank explicitly includes candidate and supplied four-word key +buffers, the decoded value, parameters, node/depth/layer/index/top +counters and a fixed number of temporary arithmetic words. These +are O(1) fixed-width roles, not host lists growing with N. Reading +encoded parameters and clearing/returning every such private role +are included in the envelope. + +The width also covers full arena offsets, rather than only wire IDs: + +``` +B <= 20 * 2^p * (p+2)^3 + <= 160 * 2^(4p) < 2^(4p+8) = 2^w. (3) +``` + +Here `p+2<=2^(p+1)` for p>=1. All node IDs, values, sentinels, +depth/layer indices, DFS tops and record/cell loop counters fit in w +bits. Observer-only accumulated receipt counters need not be runtime +registers. A product may use two w-bit registers while being reduced +to a known in-range result. No growing collection of scalar registers +is hidden in the bound. + +Let A be the number of logical arena accesses. Across depths, total +node-size is Nh. Pairwise validation uses `N²-N-Nh/2` comparisons; +initial reads add Nh. At a nonleaf node with m wires and c components, +coloring uses m initial tests, 2c component-start accesses, 2m stack +pop/clear accesses, 6m edge accesses and `2(m-c)` discovery writes: +exactly 11m. Inverse and first/last/child construction add 2m and 7m, +giving exactly 20m nonleaf accesses. Bottom-up assembly uses +`2N(h-1)²` accesses. Root loading/serialization add `N+(2h-1)N`; +leaves add `3N/2`. Thus the exact valid-input census and a convenient +conservative bound are + +``` +A = N² + 2Nh² + (37Nh-35N)/2, +A <= N² + 2Nh² + 24Nh + 3N = O(N²(p+2)²). (4) +``` + +The displayed bound is conservative; it is derived from the loops, +not fitted to finite receipts. Loop control outside scans has +O(A+J) iterations. Scan/key comparison control has O(B) elementary +cell/word iterations per access. Charging each bounded scalar +instruction by O(w²), including its register access, gives + +``` +T_compile = O((A+J+1) B (p+2)²) + = O(N³ (p+2)^7), (5) +visited space = O(B+(p+2)²+Nh) = O(N(p+2)^3). (6) +``` + +Owned output and protected input are included in visited space. +The fixed inventory is the arena, reused key tape, input, owned +output, and a fixed scalar-work bank. The queried-bit interface uses +the protected output, one new owned bit, and that same fixed bank; +its time O(N(p+2)^3) is absorbed by (5). Register-work erasure/returns +are included in the scalar envelope. All parameters have one uniform +encoded implementation, independent of input size. + +For the source family `1<=h<=ell<=p`, (5) is bounded by +`O(2^(3ell)(p+2)^7)`, hence by the stated `O(2^(4ell)(p+2)^16)` E +allowance after a fixed constant. Even O(p) such component invocations +fit that allowance. This comparison does **not** certify all the +other work charged to E: CRT reconstruction/modular inversion, +transported descriptors, macro inverse keys, parameter generation +and the complete evaluator remain separate obligations. + +## 5. Corroboration and remaining boundary + +`verify.py` checks exact retained source bytes before calling its +reference compiler. Its executed arena traffic covers every get/put, +all DFS data, table serialization, erasure and head returns. Scalar +microcode is justified by the written construction above; its complete +literal transition table is not emitted or executed. No native or +full outer replay is represented by these tests. + +Finite cases include all permutations on two/four wires, modular +rotations and other eight/sixteen-wire permutations. Every output +table is compared exactly to the retained source, every query and +its target independence is checked, and every wire endpoint is +checked. Mutation/admission controls cover malformed encodings, +duplicate permutations, an incorrect matching edge, and missing +arena/query head returns. All checks remain active under Python -O. + +The result is a scoped constructive component proof plus independently +replayable corroboration. It is not a complete CRT evaluator, physical +ordinary interchange, native/precision closure, multiplication theorem +or selected-frontier change. diff --git a/research/crt-arena-root-axis/verify.py b/research/crt-arena-root-axis/verify.py new file mode 100644 index 0000000000..29317b523f --- /dev/null +++ b/research/crt-arena-root-axis/verify.py @@ -0,0 +1,284 @@ +#!/usr/bin/env python3 +"""Exact check of the one-axis shared-arena CRT bound. + +The argument is PROOF.md. Every comparison below is an integer identity or +an induction with an explicit base. No new kappa is claimed. +""" + +import hashlib +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +EVALUATOR = ROOT / "research" / "crt-uniform-evaluator" / "PROOF.md" +EVALUATOR_README = ROOT / "research" / "crt-uniform-evaluator" / "README.md" +VENDOR = PACKAGE / "vendor" / "pr4192-crt-benes-scan-PROOF.md" +VENDOR_SHA256 = "c3eb4e14dc5ee0102cbf77c4a0e61db9989c2b8a0eaf7f0659a6e39373197474" +CORNER_U = 38809248652 +CORNER_E = 1099511627776 +BATCH_U = 1241895956864 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def census(h): + width = 1 << h + records = width * (h * h + 3 * h + 1) + accesses = width * width + 2 * width * h * h + 24 * width * h + 3 * width + return width, records, accesses + + +def direct_charge(q, h, ell, networks=4, axes=1): + """One-axis bill, then an optional batch of identical axes.""" + word = 4 * q + width, records, accesses = census(h) + tape = ( + accesses * (26 * word * records + 25 * word) + + 30 * word * records + + 3 * width * h + + 6 * (2 * h - 1) * width + + 3 + ) + scalar = tape * 8 * word * word + rotation = 9 * (ell + 2) * (ell + 2) * width + reconstruction = 65536 * q ** 3 + 1024 * q * ell ** 3 + 1024 * q * q + return axes * (reconstruction + networks * (rotation + tape + scalar)) + + +def allowance(q, ell): + return (1 << (4 * ell)) * q ** 16 + + +def polynomial_charge(q, h): + """Same bill at ell = h, expanded as a cubic polynomial in q.""" + width, records, accesses = census(h) + tape_linear = 4 * (accesses * (26 * records + 25) + 30 * records) + tape_constant = 3 * width * h + 6 * (2 * h - 1) * width + 3 + rotation = 9 * (h + 2) * (h + 2) * width + cubic = 512 * tape_linear + 65536 + quadratic = 512 * tape_constant + 1024 + linear = 4 * tape_linear + 1024 * (h ** 3) + constant = 4 * rotation + 4 * tape_constant + return ( + cubic * q ** 3 + + quadratic * q ** 2 + + linear * q + + constant, + cubic, + quadratic, + linear, + constant, + ) + + +def bind_sources(): + evaluator = EVALUATOR.read_text(encoding="utf-8") + readme = EVALUATOR_README.read_text(encoding="utf-8") + vendor_bytes = VENDOR.read_bytes() + need(hashlib.sha256(vendor_bytes).hexdigest() == VENDOR_SHA256, "vendor hash") + need(len(vendor_bytes) == 12953, "vendor length") + vendor = vendor_bytes.decode("utf-8") + for needle in ( + "65536 q^3 + 1024 q ell^3 + 1024 q^2", + "9(ell + 2)^2", + "In every case the total is at most `8ab`.", + "524288 q^4 + 8192 q^2 ell^3 + 8192 q^3", + ): + need(needle in evaluator, "evaluator sentence " + needle) + need( + "Replay one root-axis query on a single arena, in the sense of PR #4192," + in readme, + "open-question sentence", + ) + for needle in ( + "each field w=4p+8 bits.", + "J = N(h²+3h+1) records,", + "B = 5wJ arena cells.", + "26wJ + 25w read/write/one-cell-head actions.", + "erasure/returns add `6B`.", + "protected input read/return costs `3Nh`", + "Owned network writing/return costs `3(2h-1)N`.", + "costs exactly `3(2h-1)N+3` tape actions.", + "A <= N² + 2Nh² + 24Nh + 3N", + ): + need(needle in vendor, "arena sentence " + needle) + dropped = vendor.replace("26wJ + 25w", "26wJ + 24w") + need("26wJ + 25w read/write/one-cell-head actions." not in dropped, "binder control") + + +def prove_schoolbook_cap(): + """A w-bit by w-bit schoolbook product is at most 8 w^2 bit-steps for w >= 1.""" + # Touch formula from the pinned evaluator: 3ab + 3a + b. + # At a = b = w this is 3w^2 + 4w, and 3w^2 + 4w <= 8w^2 iff 4 <= 5w. + need(4 <= 5 * 1, "schoolbook at w=1") + need(not (4 <= 5 * 0), "w=0 is outside the tariff") + + +def prove_census_bounds(): + """A <= 16 N^2, J <= 5 N h^2, and the tail comparisons, for every h >= 1.""" + # poly(h) = 2h^2 + 24h + 3. A = N^2 + N poly(h), N = 2^h. + # A <= 16 N^2 iff poly(h) <= 15 N. + # Expansion: poly(h+1) - poly(h) = 4h + 26. + # 2(h+1)^2 - 2h^2 = 4h + 2 and 24(h+1) - 24h = 24, sum 4h + 26. + need(4 + 2 + 24 == 4 + 26, "poly step coefficients") + need(2 * 1 + 24 * 1 + 3 <= 15 * 2, "A bound h=1") + need(2 * 4 + 24 * 2 + 3 <= 15 * 4, "A bound h=2") + need(2 * 9 + 24 * 3 + 3 <= 15 * 8, "A bound h=3") + # Auxiliary: 4h + 26 <= 15 * 2^h for h >= 3, by the base and + # 4(h+1)+26 = 4h+30 <= 15*2^h + 4 <= 30*2^h once 4 <= 15*2^h. + need(4 * 3 + 26 <= 15 * 8, "auxiliary base h=3") + need(4 <= 15 * 2, "auxiliary increment") + # J = N(h^2+3h+1) <= 5 N h^2 iff (h-1)(4h+1) >= 0. + # (h-1)(4h+1) = 4h^2 - 3h - 1. + need(4 - 3 - 1 == 0, "J discriminant at h=1") + # 15 h <= 16 * 4^h for h >= 1. Base 15 <= 64. + # 15(h+1) <= 16*4^h + 15 <= 64*4^h once 15 <= 48*4^h. + need(15 <= 16 * 4, "width induction base") + need(15 <= 48 * 4, "width induction increment") + # Exact displayed census is at most the convenient bound: + # (37h-35)/2 <= 24h+3 iff 0 <= 11h+41. + need(11 * 1 + 41 > 0, "census domination") + # J >= 10 and A >= 4 at the minimum h = 1, N = 2. + width, records, accesses = census(1) + need(records == 10 and accesses >= 4 and width == 2, "minimum census") + + +def prove_charge_constants(): + need(8 * 16 == 128, "scalar factor 8 w^2 = 128 q^2") + need(129 * 37 * 4 == 19092, "one-network coefficient") + need(4 * 19092 == 76368, "four-network coefficient") + need(16 * 5 == 80, "access-record product") + need(76368 * 80 == 6109440, "majorant coefficient") + need(1024 + 16384 + 64 == 17472, "reconstruction coefficient") + need(65536 == 16384 * 4, "cubic CRT term at q=4") + need(1024 == 64 * 16, "quadratic CRT term at q=4") + need(4 * 9 == 36, "four rotation tables") + # Leading arena term 8 w^2 * A * (26 w J) equals (3328/5) A B q^2. + need(8 * 16 * 26 == 3328, "leading coefficient") + need(5 * 4 == 20, "B = 5 w J and w = 4q give 20 q J") + + +def prove_allowance_majorant(): + """For h >= 2 and q >= h+2, the majorant is at most 2^{4h} q^{16}.""" + # Split the majorant into three terms, each at most one third of the + # allowance. The first two are smallest at N = 4, q = 4. + need(3 * 17472 == 52416, "term one multiplier") + need(3 * 36 == 108, "term two multiplier") + need(3 * 6109440 == 18328320, "term three multiplier") + need(52416 <= (1 << 32), "term one at N=4, q=4") + need(108 <= (1 << 34), "term two at N=4, q=4") + # Term three: 18328320 h^2 <= 2^h (h+2)^13 for every h >= 2. + need(18328320 * 4 <= (1 << 2) * (4 ** 13), "term three h=2") + need(18328320 * 9 <= (1 << 3) * (5 ** 13), "term three h=3") + need(18328320 <= 6 ** 13, "term three h=4, where r(4) = 6^13") + # For h >= 4, r(h) = 2^h (h+2)^13 / h^2 is strictly increasing because + # r(h+1)/r(h) >= 2 (h/(h+1))^2 >= 32/25 > 1. + need(5 * 4 >= 4 * (4 + 1), "h/(h+1) >= 4/5 at h=4") + need(32 > 25, "32/25 > 1") + + +def prove_h1_cubic(): + """At h = ell = 1 and every q >= 4, U <= (sum of coefficients) q^3 <= E.""" + value, cubic, quadratic, linear, constant = polynomial_charge(4, 1) + coefficient_sum = cubic + quadratic + linear + constant + need(coefficient_sum == 37169148, "h=1 coefficient sum") + need(value == direct_charge(4, 1, 1), "h=1 polynomial agrees") + need(coefficient_sum <= 16 * (4 ** 13), "h=1 against 16 q^13 at q=4") + for q in (4, 5, 9, 16): + charged, *_rest = polynomial_charge(q, 1) + need(charged == direct_charge(q, 1, 1), "h=1 agreement " + str(q)) + need(charged <= allowance(q, 1), "h=1 allowance " + str(q)) + + +def prove_ell_step(): + """Raising ell by one multiplies the exact bill by less than 16.""" + # For ell >= 1, ell(ell-1) >= 0 and ell^2(ell-1) >= 0, so + # ell^2 >= ell and ell^3 >= ell^2 >= 1. Thus + # 3 ell^2 + 3 ell + 1 <= 7 ell^3, and + # (ell+1)^3 - 16 ell^3 <= -8 ell^3 < 0. + need(3 + 3 + 1 == 7, "cubic ell absorption") + for ell in (1, 2, 5): + need(ell * (ell - 1) >= 0, "ell squared") + need((ell + 1) ** 3 - 16 * ell ** 3 <= -8 * ell ** 3, "ell cubic drop") + need((ell + 3) ** 2 - 16 * (ell + 2) ** 2 < 0, "ell rotation drop") + for h in (1, 2, 4): + for ell in (h, h + 2): + q = max(4, ell + 2) + need( + direct_charge(q, h, ell + 1) < 16 * direct_charge(q, h, ell), + "ell step " + str((q, h, ell)), + ) + + +def prove_corner_and_batch(): + corner = direct_charge(4, 2, 2) + bound = allowance(4, 2) + need(corner == CORNER_U, "corner witness") + need(bound == CORNER_E, "corner allowance") + need(28 * corner <= bound < 29 * corner, "corner factor") + need(bound // corner == 28, "corner quotient") + batch = direct_charge(4, 2, 2, networks=4, axes=32) + need(batch == BATCH_U, "batch witness") + need(batch > bound, "full axis batch exceeds this majorant") + # The predecessor's all-axis CRT display is the one-axis bill times 8q. + one_axis_crt = 65536 * 4 ** 3 + 1024 * 4 * 8 + 1024 * 16 + eight_q = 32 + displayed = 524288 * 4 ** 4 + 8192 * 16 * 8 + 8192 * 4 ** 3 + need(eight_q * one_axis_crt == displayed, "CRT bill scales by 8q") + + +def prove_grid(): + worst_ratio = None + worst_at = None + for h in range(1, 9): + for ell in range(h, h + 4): + for q in range(max(4, ell + 2), max(4, ell + 2) + 4): + charged = direct_charge(q, h, ell) + bound = allowance(q, ell) + need(charged <= bound, "grid " + str((q, h, ell))) + if h >= 2 and ell == h: + width = 1 << h + majorant = ( + 17472 * q ** 4 + + 36 * q * q * width + + 6109440 * q ** 3 * width ** 3 * h * h + ) + need(charged <= majorant <= bound, "majorant " + str((q, h))) + if ell == h: + ratio = (charged, bound) + if worst_ratio is None or charged * worst_ratio[1] > worst_ratio[0] * bound: + worst_ratio = ratio + worst_at = (q, h) + polynomial, *_rest = polynomial_charge(q, h) + need(polynomial == direct_charge(q, h, h), "polynomial " + str((q, h))) + need(worst_at == (4, 2), "grid maximum " + str(worst_at)) + + +def main(): + bind_sources() + prove_schoolbook_cap() + prove_census_bounds() + prove_charge_constants() + prove_allowance_majorant() + prove_h1_cubic() + prove_ell_step() + prove_corner_and_batch() + prove_grid() + print( + "PASS_CRT_ARENA_ROOT_AXIS" + " four_networks=true" + " corner_U=38809248652" + " corner_E=1099511627776" + " corner_quotient=28" + " batch_U=1241895956864" + " batch_exceeds=true" + " no_new_kappa=true" + ) + + +if __name__ == "__main__": + main()