Prove the sharp universal axis cutoff for the CRT reservoir envelope (no κ)

research/reservoir-universal-axis-cutoff/PROOF.md

@@ -0,0 +1,172 @@
+# Exact universal axis capacity of the reservoir majorant
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped mathematical proof with exact finite corroboration.
+The object optimized here is the inherited conservative factor-3 envelope.
+Its failure is not failure of the actual repair algorithm or actual error.
+
+## Contract
+
+Use Hiroki KUMAZAKI's PR4174 constructor, at the source pinned in
+SOURCES.json. An accepted layout has integers p>=1, c=ceil(log2(p+2)),
+ell>=max(2,c), a power of two d>=65536, and d widths in {ell-1,ell}.
+If a widths equal ell, its address length and maximum batch are
+
+```text
+L = d(ell-1)+a,  0<=a<=d,
+G = 64(ell+c),
+r_max = floor(L/(100G)) = floor((d(ell-1)+a)/(6400(ell+c))).
+```
+
+The minimum allowed d is 65536 because the constructor requires a power
+of two at least 51200. Every displayed parameter tuple passes its batch
+positivity and volume checks: L/(100G)>=d(ell-1)/(12800ell)>=d/25600>2.
+No requirement L<=p is imposed by this constructor.
+
+James Reed's PR4923 proves the conservative factor 3. PR4924/4925 derive
+the printed-envelope ratio. We cite those arithmetic premises, without
+replaying their verifiers or claiming their results as new. Relative to
+C_E times the printed room, the conservative ratio is
+
+```text
+R = 3 r_max ((p+2)/2^c)^64.
+```
+
+The question is exactly whether R<=p/6400 for every accepted ell and width
+pattern, at fixed p,d. C_E cancels. It is not evaluated or given a value.
+This is a different question from R<=1/6400 or from evaluating the real E.
+
+## The maximum batch is attained
+
+Put k=floor(d/6400). Then
+
+```text
+max_(ell,a) r_max = k.
+```
+
+For the upper bound, L<=d ell and ell/(ell+c)<1, so
+r_max<d/6400. Since d is a power of two and 6400=2^8*25, d/6400 is not an
+integer; hence r_max<=k. Define the positive remainder delta=d-6400k.
+For all widths equal ell, r_max>=k if and only if
+
+```text
+d ell >= 6400k(ell+c),
+(delta) ell >= 6400kc.
+```
+
+Thus the maximum is attained at the finite precision
+
+```text
+ell_* = max(2,c,ceil(6400kc/delta)),  a=d.
+```
+
+This supplies an actual accepted layout, not merely a limiting supremum.
+The minimum constructor precision and the open upper limit d/6400 both
+matter. Replacing the floor by a rounded or floating-point limit is unsafe.
+
+## The sharp capacity criterion
+
+Define the nonnegative integer
+
+```text
+M(p) = floor(p 2^(64c) / (19200 (p+2)^64)).
+```
+
+The following conditions are equivalent:
+
+1. Every accepted layout at p,d has R<=p/6400.
+2. 19200 floor(d/6400) (p+2)^64 <= p 2^(64c).
+3. floor(d/6400)<=M(p).
+4. d<=6400(M(p)+1)-1.
+
+The maximum-batch theorem proves the equivalence of 1 and 2, including
+necessity by the attaining all-wide layout. Integer division proves 2 iff
+3, and the definition of floor proves 3 iff 4. Equality is accepted.
+
+Consequently let D(p)=6400(M(p)+1)-1. If D(p)<65536, no allowed dyadic axis
+count passes uniformly in precision. Otherwise the largest allowed dyadic
+count is 2^floor(log2(D(p))). All smaller allowed dyadic counts pass; every
+larger allowed dyadic count has the explicit failure at ell_* above.
+
+The simple sufficient condition 3d<=p follows as a corollary: then
+19200k<3d<=p and ((p+2)/2^c)^64<=1. Unlike L<=p, it does not restrict ell.
+It is a sufficient corollary, not the sharp criterion.
+
+## No cutoff in p alone
+
+For each fixed p, M(p) is finite. Choose a power of two
+
+```text
+d >= max(65536, 6400(M(p)+1)).
+```
+
+Then floor(d/6400)>=M(p)+1. The accepted all-wide layout at ell_* fails
+the conservative inequality. This works for every p, however large.
+Therefore no finite cutoff in p can make this majorant hold on all layouts
+accepted by the constructor with unbounded d. A caller must control d or
+supply a different bound. This does not assert that actual repair fails.
+
+## Explicit boundary witnesses
+
+At p=131070=2^17-2 and d=65536, c=17, M(p)=6, and k=10. For all-wide
+layouts the inequality holds exactly when r_max<=6. For arbitrary width
+patterns, all-wide maximizes r_max at each precision. The first failing
+precision is therefore
+
+```text
+ceil(6400*7*17/(65536-6400*7)) = 37.
+```
+
+At ell=36, L=2359296, G=3392, r_max=6, and the ratio of the majorant to
+the p/6400 allowance is 3840/4369<1. At ell=37, L=2424832, G=3456,
+r_max=7, and that ratio is 4480/4369>1. Thus every allowed width pattern
+passes for 17<=ell<=36, while the all-wide pattern fails at 37. These
+layouts both have L>p. The verifier constructs them with the pinned Layout.
+
+At p=2^24-2, M(p)=873 and D(p)=5593599. The largest uniformly covered
+dyadic axis count is 4194304=2^22; the next count 8388608=2^23 fails at
+its attaining precision. This classifies the entire precision/width family
+at that p. It does not repeat PR4926's one-layout ratio 12.
+
+## Verification and limits
+
+The proof above supplies the unbounded quantifiers. The verifier checks
+finite arithmetic boxes, all width-count patterns in its stated boxes,
+the attaining precisions and their preceding seam, exact capacity neighbors,
+and four actual Layout fixtures. It never executes predecessor verifiers,
+the descriptor census, the repair program or the real E polynomial.
+RESULT.json gives generated counts, source hashes and all control results.
+Normal replay is read-only and rejects a changed receipt under -O.
+
+Native operations, simultaneous carry correctness, evaluator implementation,
+physical repair, memory, routing, restoration, all-size caller integration,
+compiler and outer multiplication remain separate obligations. The selected
+frontier is unchanged. No kappa, supplier admission or complete multiplication
+theorem is claimed. Independent human and formal proof-kernel review are unclaimed.
+
+## Code constraints
+
+The new verifier has no recursion. Every enumeration has a fixed finite range
+stated in the code and the receipt. Functions stay below 60 physical lines.
+Explicit exceptions enforce contracts and receipt comparison under -O.
+
+Power of Ten rule 3 has a managed-runtime deviation in verify.py: CPython
+allocates integers, containers and source Layout prefixes. The finite fixture
+has d<=65536; algebraic axis counts up to the stated finite probe exponent
+are represented as integers rather than materialized axes. File reads are
+capped at 1 MiB. The verifier releases one Layout before constructing the
+next. These bounds limit live algorithmic data; runtime internals are not
+allocation-instrumented. A native fixed-storage implementation would be
+required before allocation-prohibited use.
+
+Rules 8 and 9 have a source-execution deviation for the four Layout fixtures:
+runpy executes exactly one SHA256-authenticated, repository-pinned allocator
+and the checker calls its Layout constructor. It imports no predecessor
+checker, accepts no user-selected executable, and has no network or Git
+runtime dependency. The official read-only Git-free replay exercises this
+boundary. The source retains its own implementation and attribution; its
+unrelated routines are not changed or claimed compliant here.
+
+Warning-strict normal and optimized replay provide the local diagnostics.
+No static type checker is configured for this standalone package.

research/reservoir-universal-axis-cutoff/README.md

@@ -0,0 +1,98 @@
+# Exact universal axis cutoff for the CRT reservoir envelope
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped mathematical proof with exact finite corroboration.
+For every fixed ambient parameter p and allowed dyadic axis count d, the
+largest batch over all accepted precisions and width patterns is exactly
+floor(d/6400), and a finite all-wide layout attains it. Consequently the
+inherited conservative factor-3 envelope fits the printed repair allowance
+for every such layout exactly when
+
+```text
+c = ceil(log2(p+2)),
+M = floor(p 2^(64c) / (19200 (p+2)^64)),
+d <= 6400(M+1)-1.
+```
+
+Every larger allowed d has an explicit accepted failure witness. Thus no
+cutoff in p alone covers the constructor's unbounded axis counts. This
+settles a new uniform capacity question beyond the predecessor's individual
+layouts. The proof is in [PROOF.md](PROOF.md), including the exact hypotheses
+and an attaining precision. It does not reverify a predecessor theorem.
+
+For example, at p=131070 and d=65536 every width pattern passes through
+precision 36, while the all-wide layout fails at precision 37. The exact
+ratios to the allowance are 3840/4369 and 4480/4369, respectively. At
+p=2^24-2, the largest axis count covered uniformly in precision is 2^22;
+2^23 fails at its explicit attaining precision.
+
+These are statements about the conservative printed majorant. A failed
+majorant is not a counterexample to actual repair, the smaller error bound
+or the real E polynomial. No physical supplier, selected-frontier change,
+new kappa or complete multiplication theorem is claimed.
+
+## Reproduce
+
+From the repository root with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/reservoir-universal-axis-cutoff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/reservoir-universal-axis-cutoff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/reservoir-universal-axis-cutoff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/reservoir-universal-axis-cutoff --check-source-history
+```
+
+Substitute another CPython 3.12 executable as needed. The direct marker is
+PASS_RESERVOIR_UNIVERSAL_AXIS_CUTOFF. Default replay is read-only and compares
+the entire generated [receipt](RESULT.json), including package/live-input
+SHA256 hashes. `--write NEW_PATH` generates a new receipt and refuses an
+existing file. Source pins and provenance are in [SOURCES.json](SOURCES.json).
+The checker needs neither Git nor network at runtime. It imports no
+predecessor verifier and does not run the descriptor census or repair engine.
+
+The finite checks cover 74,880 precision rows, 1,152 attainment seams, all
+393,222 width-count patterns in six boxes, 1,464 capacity-neighbor probes
+at 732 ambient parameters, four actual source Layout fixtures and fourteen
+domain/source/receipt controls. The
+unbounded quantifiers come from the written floor argument, not from the
+finite probes. [VERIFY.json](VERIFY.json) registers normal and optimized
+warning-strict commands. Code constraints and bounded runtime deviations
+are recorded in the proof.
+
+## Open next questions
+
+1. Optimize the exact published window factor instead of the conservative
+   constant 3. Start with the batch staircase and decreasing correction as
+   precision varies. Those competing terms are not optimized here.
+2. Bind an enclosing physical caller's reached p,d,ell values to this
+   criterion and the charged E envelope. The real evaluator, repair,
+   routing, restoration, native and outer obligations remain open.
+
+Structured first steps and blockers are in [TASK.json](TASK.json).
+Independent human and formal proof-kernel review are unclaimed. No Lean,
+Docker, selected cold replay or complete multiplier execution was run.
+
+## Source context and credit
+
+Base: canonical main 3f0152a32eeebac0df11946dbd50cabe5a7f7839, priority
+revision 8. The selected conditional kappa remains .003125804. The
+formal-interface-lemma card is changed to this original arithmetic theorem
+rather than a formalization or audit. The known-working selected binding
+command passed; it was orientation only.
+
+Credit Hiroki KUMAZAKI for [PR4174's constructor](https://github.com/CrocSwap/integer-mult-bounds/pull/4174),
+James Reed for [PR4923's factor 3](https://github.com/CrocSwap/integer-mult-bounds/pull/4923),
+[PR4925's ratio](https://github.com/CrocSwap/integer-mult-bounds/pull/4925)
+and [PR4926's edge comparison](https://github.com/CrocSwap/integer-mult-bounds/pull/4926).
+The compact-switch density/room premises in PR4646 and PR4328, Cinna Davis's
+PR4100 CRT framework and their retained predecessor lineage keep their credit.
+Integer division and monotonicity are standard. The new step is the exact
+unbounded precision optimization, sharp axis-capacity criterion and explicit
+failure construction for this envelope. No literature-priority claim is made.
+
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267742).
+Overlap covered live open PRs, recent account work, active hub claims,
+local reservations, distinctive main README formulas and merged PR bodies.
+Unpublished work and historical diffs outside those searches remain limits.
+Only this new package is changed; frozen inputs and contributor notices remain.

research/reservoir-universal-axis-cutoff/RESULT.json

@@ -0,0 +1,110 @@
+{
+  "actual_layouts": [
+    {
+      "G": 2176,
+      "L": 1114112,
+      "d": 65536,
+      "ell": 17,
+      "p": 131070,
+      "r_max": 5,
+      "wide": 65536
+    },
+    {
+      "G": 3392,
+      "L": 2359296,
+      "d": 65536,
+      "ell": 36,
+      "p": 131070,
+      "r_max": 6,
+      "wide": 65536
+    },
+    {
+      "G": 3456,
+      "L": 2359296,
+      "d": 65536,
+      "ell": 37,
+      "p": 131070,
+      "r_max": 6,
+      "wide": 0
+    },
+    {
+      "G": 3456,
+      "L": 2424832,
+      "d": 65536,
+      "ell": 37,
+      "p": 131070,
+      "r_max": 7,
+      "wide": 65536
+    }
+  ],
+  "capacities": {
+    "ambient_parameters": 732,
+    "dyadic_neighbors": 1464,
+    "examples": {
+      "1": {
+        "axis_limit": 33036799,
+        "batch_capacity": 5161,
+        "largest_accepted_dyadic_count": 16777216
+      },
+      "131070": {
+        "axis_limit": 44799,
+        "batch_capacity": 6,
+        "largest_accepted_dyadic_count": null
+      },
+      "16777214": {
+        "axis_limit": 5593599,
+        "batch_capacity": 873,
+        "largest_accepted_dyadic_count": 4194304
+      },
+      "2": {
+        "axis_limit": 6399,
+        "batch_capacity": 0,
+        "largest_accepted_dyadic_count": null
+      },
+      "9240576": {
+        "axis_limit": 116387500828673071187199,
+        "batch_capacity": 18185547004480167372,
+        "largest_accepted_dyadic_count": 75557863725914323419136
+      }
+    },
+    "no_p_cutoff_witnesses": 732
+  },
+  "capacity": "d <= 6400*(floor(p*2^(64*c)/(19200*(p+2)^64))+1)-1",
+  "claim_type": "scoped proof with finite corroboration",
+  "controls": [
+    "invalid_domain_0",
+    "invalid_domain_1",
+    "invalid_domain_2",
+    "invalid_domain_3",
+    "invalid_domain_4",
+    "invalid_domain_5",
+    "invalid_domain_6",
+    "invalid_domain_7",
+    "invalid_domain_8",
+    "allow_one_excess_batch",
+    "check_only_minimum_precision",
+    "check_only_narrow_widths",
+    "changed_source_byte",
+    "boolean_receipt_count"
+  ],
+  "maximum_batch": "floor(d/6400), attained",
+  "maximum_grid": {
+    "attaining_seams": 1152,
+    "precision_rows": 74880
+  },
+  "no_new_kappa": true,
+  "schema_version": 1,
+  "source_sha256": {
+    "PROOF.md": "cebd3a64f4ba9873d9ea705056e9a39bd13c27b48d6a5d564e17f0c165c32903",
+    "README.md": "b1c607b19ce68d6e897b626e8cc9fe2e5602aad755df2786a5173775d8b03839",
+    "SOURCES.json": "e0b6822cb2560c536ca2f2dc1e35199a10c6167ca0ecaf0b7714c1ebb6836d45",
+    "TASK.json": "fc0a08d6f7d5b70b94643b78a5450e63a404f848abc54a7dfc1db72ad9f6a7fc",
+    "VERIFY.json": "29e2777e8ad15608068e299a9009e516a0d0fdf0171b19656dff156dd93656b7",
+    "research/crt-reservoir-placement/allocator.py": "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688",
+    "verify.py": "79a551ae5991952609fd2dcdc1747958446119d45b948fba3c820e0b641fdb83"
+  },
+  "width_counts": {
+    "complete_width_count_patterns": 393222,
+    "layouts": 6
+  }
+}