Prove the full CRT arena batch threshold and sharp surcharge (no κ)

research/crt-arena-batch-threshold/PROOF.md

@@ -0,0 +1,133 @@
+# Full shared-arena batch threshold
+
+This is a scoped counting theorem about the explicit bill in unpaidmoon's
+[PR4650 proof](../crt-arena-root-axis/PROOF.md), at canonical main
+`624de9dc66858af0945e5f8a0942488d62280d43`. Its tariffs and arena census are
+premises here. The new result classifies the full batch without changing that
+bill. No predecessor executable is replayed.
+
+## Statement
+
+Let `p >= 2` and `1 <= h <= ell <= p` be integers. Put
+
+```
+q = p+2, N = 2^h, w = 4q,
+A = N^2 + 2Nh^2 + 24Nh + 3N,
+J = N(h^2+3h+1),
+T = A(26wJ+25w) + 30wJ + 3Nh + 6(2h-1)N + 3,
+U = 65536q^3 + 1024q ell^3 + 1024q^2
+    + 4[9(ell+2)^2 N + (1+8w^2)T],
+B = 8q U, E = 2^(4ell) q^16.
+```
+
+Thus `B` repeats the complete one-axis charge, including its CRT work and
+four networks, on the maximum `8q` axes. In particular every tape action
+still pays the optional schoolbook product of two `w`-bit words.
+
+Then `B < E` except at exactly `(p,ell,h) = (2,1,1)` and `(2,2,2)`.
+The least real constant `C` satisfying `B <= C E` throughout this domain is
+
+```
+C* = 9702312163 / 8589934592.
+```
+
+It is attained at `(2,2,2)`. These are comparisons of the stated majorant.
+An excess of that majorant is not a lower bound on an actual machine.
+
+## Proof for p >= 3
+
+First take `ell = h`, so `q >= max(5,h+2)`. PR4650's explicit-bill lemmas
+give, for `h >= 2`,
+
+```
+U <= 17472q^4 + 36q^2 N + 6109440q^3 N^3 h^2.
+```
+
+Multiplication by the full batch size gives
+
+```
+B <= 139776q^5 + 288q^3 N + 48875520q^4 N^3 h^2.
+```
+
+Each summand is strictly below `E/3`. For the first this is equivalent to
+`419328 < N^4 q^11`, which holds already at `N=4,q=5` and is preserved by
+increasing either variable. For the second it is
+`864 < N^3 q^13`, with the same smallest pair.
+
+The third comparison is
+
+```
+146626560 h^2 < 2^h q^12.
+```
+
+At `h=2,3`, use `q >= 5` and the respective exact comparisons
+
+```
+586506240 < 976562500,
+1319639040 < 1953125000.
+```
+
+At `h=4`, `q >= 6` gives `2346024960 < 34828517376`.
+For `h >= 4`, set `r(h) = 2^h(h+2)^12/h^2`. Then
+
+```
+r(h+1)/r(h) = 2 ((h+3)/(h+2))^12 (h/(h+1))^2
+             >= 2 (4/5)^2 = 32/25 > 1.
+```
+
+Consequently the `h=4` inequality propagates to every larger `h` using
+`q >= h+2`. This proves `B < E` at `ell=h>=2`.
+
+For `ell=h=1`, PR4650's height-one expansion gives
+
+```
+U <= 37169148q^3,
+B <= 297353184q^4 < 16q^16 = E,
+```
+
+since `297353184 < 16*5^12` and `q >= 5`.
+
+Now fix `q,h` and increase `ell`. The only `ell`-dependent terms in `U`
+are `1024q ell^3` and `36N(ell+2)^2`. For integer `ell>=1`,
+
+```
+(ell+1)^3 - 16ell^3 = -15ell^3+3ell^2+3ell+1 <= -8ell^3 < 0,
+(ell+3)^2 - 16(ell+2)^2 = -15ell^2-58ell-55 < 0.
+```
+
+The omitted part of `U` is positive and independent of `ell`, so
+`U(ell+1)<16U(ell)`. Multiplication by the fixed `8q` preserves this strict
+inequality, while `E(ell+1)=16E(ell)`. The result at `ell=h` therefore
+extends to every `ell>=h`, in particular the required `ell<=p`.
+
+## Exhaustion of p = 2 and sharp constant
+
+There are exactly three admissible pairs `(ell,h)` when `p=2`.
+Substitution into the displayed integers gives
+
+```
+(ell,h)    B                 E                 B/E
+(1,1)      75548846976       68719476736       590225367/536870912
+(2,1)      75549780608       1099511627776     590232661/8589934592
+(2,2)      1241895956864     1099511627776     9702312163/8589934592
+```
+
+The middle ratio is below one. The first exceeds one, and its numerator
+when written over `8589934592` is `9443605872 < 9702312163`. All `p>=3`
+ratios are below one by the proof above. Hence the last row is the global
+maximum and gives the stated least constant. This completes the proof.
+
+## Consequence and limits
+
+For every `p>=3`, changing the scalar inventory is unnecessary to fit the
+entire batch under this particular allowance. Over the full domain `p>=2`,
+the sharp majorant constant is `C*`, and the coarse integer constant two
+also suffices. This closes the large-parameter part of PR4650's batch
+question with its existing schedule; it does not supply the tighter
+word-operation inventory requested there.
+
+The arena tariff, CRT reconstruction premise and maximum batch size remain
+inherited. Reservoir placement, actual arena execution, repair, native lifting,
+all-size caller composition and the outer multiplication theorem are separate
+obligations. The selected frontier is unchanged. The quantified conclusion is
+proved by the inequalities above; finite checker output is corroboration.

research/crt-arena-batch-threshold/README.md

@@ -0,0 +1,80 @@
+# The full shared-arena CRT batch fits from p = 3
+
+Scoped counting proof, with exact finite corroboration. No new kappa.
+
+For the explicit one-axis bill `U` in unpaidmoon's PR4650, repeat its complete
+CRT and four-network charge on all `8(p+2)` axes. Retain its schoolbook product
+beside every tape action. [PROOF.md](PROOF.md) proves that this full batch is
+strictly below `E = 2^(4ell)(p+2)^16` for all integers `p>=3` and
+`1<=h<=ell<=p`. The three admissible `p=2` cases are exhausted explicitly.
+Exactly `(p,ell,h)=(2,1,1)` and `(2,2,2)` exceed `E`.
+
+The least uniform constant in `8(p+2)U <= C E` is
+`C = 9702312163/8589934592`, attained at `(2,2,2)`. A majorant exceeding an
+allowance does not prove an actual machine lower bound. The new conclusion is
+that no scalar-inventory change is needed for the large-parameter batch under
+this particular allowance, despite the previously displayed small failure.
+
+## Evidence and reproduction
+
+The quantified result comes from the written proof. [verify.py](verify.py)
+independently forms the full batch, compares a second polynomial expansion,
+and checks all 45,759 triples with `2<=p<=64`. The generated, hash-bound
+[RESULT.json](RESULT.json) records the exact exceptions, the sharp witness,
+63 height inequalities, 64 extension steps and eight rejection controls.
+No predecessor executable is run. The verifier authenticates its one live
+proof input by SHA256 and Git blob identity. [SOURCES.json](SOURCES.json)
+pins the canonical base, catalogue, selected record and inherited bill.
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/crt-arena-batch-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/crt-arena-batch-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/crt-arena-batch-threshold
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/crt-arena-batch-threshold --check-source-history
+```
+
+The direct verifier prints `PASS_CRT_ARENA_BATCH_THRESHOLD`. Its checker has
+an explicit finite domain; the proof has no `p<=64` restriction. Normal and
+optimized checks retain all checks through explicit exceptions. Default replay
+does not rewrite the receipt; `--write-result` generates it deliberately.
+
+## Scope and credit
+
+Base is canonical main `624de9dc66858af0945e5f8a0942488d62280d43`, priority
+revision 7. [TASK.json](TASK.json) changes `uniform-transfer-audit` into an
+original analytic extension of another contributor's open batch question.
+The [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133323)
+states the proposed threshold and the first-result stopping rule.
+
+This contribution was produced by Nick Petalas. Credit unpaidmoon for
+[PR4650](https://github.com/CrocSwap/integer-mult-bounds/pull/4650)'s one-axis
+bill, its majorant lemmas and the batch question, and
+[PR4377](https://github.com/CrocSwap/integer-mult-bounds/pull/4377)'s CRT and
+rotation tariffs. Credit ToikY for
+[PR4192](https://github.com/CrocSwap/integer-mult-bounds/pull/4192)'s arena
+census and Cinna Davis for
+[PR4100](https://github.com/CrocSwap/integer-mult-bounds/pull/4100)'s CRT
+construction. Their claims are cited premises, not new verification deliverables.
+Predecessor files and attribution are unchanged. New work is Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+The arena and reconstruction tariffs remain inherited. This does not execute
+an arena, implement a tighter scalar inventory, compose reservoir placement or
+exceptional repair, admit a supplier, or prove the multiplication theorem.
+No Lean, Docker, native replay or full historical suite is required or run.
+The selected frontier is unchanged. Python's managed allocation is bounded by
+the fixed 64-parameter checker domain; no recursion or unbounded search is used.
+
+## Open next questions
+
+1. Can the actual word-level scalar inventory fit constant one at the two
+   excluded `p=2` corners? Start with the per-record comparisons in PR4192
+   section 2. The present majorant excess does not settle that question.
+2. Can this full-batch allowance be composed with reservoir placement and the
+   actual paid repair-key service of PR4795? Begin with one complete entry,
+   call and exit program, retaining all source-state queries and restoration
+   charges. Physical movement and all-size caller premises remain external.
+
+The [structured questions](TASK.json) record relevance, first steps and blockers.

research/crt-arena-batch-threshold/RESULT.json

@@ -0,0 +1,55 @@
+{
+  "status": "PASS_CRT_ARENA_BATCH_THRESHOLD",
+  "claim_type": "scoped proof with finite corroboration",
+  "grid_p_max": 64,
+  "grid_triples": 45759,
+  "exceptions": [
+    [
+      2,
+      1,
+      1
+    ],
+    [
+      2,
+      2,
+      2
+    ]
+  ],
+  "sharp_constant": "9702312163/8589934592",
+  "height_checks": 63,
+  "extension_checks": 64,
+  "rejection_controls": 8,
+  "p2_exhaustion": [
+    {
+      "p": 2,
+      "ell": 1,
+      "h": 1,
+      "batch": 75548846976,
+      "allowance": 68719476736,
+      "ratio": "590225367/536870912"
+    },
+    {
+      "p": 2,
+      "ell": 2,
+      "h": 1,
+      "batch": 75549780608,
+      "allowance": 1099511627776,
+      "ratio": "590232661/8589934592"
+    },
+    {
+      "p": 2,
+      "ell": 2,
+      "h": 2,
+      "batch": 1241895956864,
+      "allowance": 1099511627776,
+      "ratio": "9702312163/8589934592"
+    }
+  ],
+  "source_sha256": {
+    "PROOF.md": "8c9dbbd057811cfbca421234bc9b1f43f71d367a374508231d344c072ed779bb",
+    "verify.py": "7a484329cd3ac65b1f382193f64335cf4aa472b73066ffb392cecb0866ef7703",
+    "SOURCES.json": "0e27c0b68888e41ed0670aafab366b4627da9e8c28101647dc81e4b8d4b78689",
+    "TASK.json": "d9e6430ff9f76e537968719f8828d04cfb5429835bb7cc8c08199ad2e64ee148",
+    "VERIFY.json": "9b4a6efc1fd154209366b306fee5092dffe4f45e04f76f3d2e17ee3c91a95c30"
+  }
+}

research/crt-arena-batch-threshold/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/crt-arena-root-axis/PROOF.md",
+      "usage": "input",
+      "git_blob": "e2f7a81d5302aa3e5fdd8051da53def50525c130",
+      "sha256": "dc6871e84b882210ad9a96300bc22944530d783ca78b3badd5a174bf628d45aa"
+    }
+  ]
+}

research/crt-arena-batch-threshold/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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": "changed",
+  "actual_scope": "Prove the full shared-arena CRT batch threshold and its least uniform majorant constant.",
+  "scope_change_reason": "Original analytic extension of PR4650, rather than an audit of its one-axis theorem. The explicit full-batch counterexample leaves the unbounded p>=3 domain and sharp uniform constant unsettled.",
+  "bottleneck_link": "Closes the large-parameter arena-batch allowance under the inherited schoolbook tariff, without changing the scalar inventory or treating other CRT costs as zero.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first verified full-batch theorem; defer physical execution and new inventory to open questions.",
+  "outcome": "completed",
+  "evidence": "PROOF.md supplies the quantified argument; RESULT.json is generated by the exact bounded verifier.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the actual word-level scalar inventory fit constant one at the two excluded p=2 corners?",
+      "why_it_matters": "The present excess is a majorant excess and does not exclude a cheaper physical implementation.",
+      "first_step": "Replace one schoolbook product per tape action by the actual per-record comparisons in PR4192 section 2 and price the two finite cases.",
+      "blocked_by": "A tighter physical inventory is outside this theorem."
+    },
+    {
+      "question": "Can this full-batch allowance be composed with reservoir placement and the actual exceptional-repair evaluator?",
+      "why_it_matters": "The full batch theorem discharges only an arithmetic allowance, not total CRT cost.",
+      "first_step": "Bind one complete entry/call/exit program to the paid key service in PR4795, retaining every source-state query and restoration charge.",
+      "blocked_by": "Matched physical movement, ownership and all-size caller premises remain external."
+    }
+  ]
+}