From 0ec8a26572069b6109decadd488b9770944a4296 Mon Sep 17 00:00:00 2001
From: Aakash Thakkar <thakkaraakash@hotmail.com>
Date: Thu, 15 Oct 2026 00:22:09 -0500
Subject: [PATCH] Prove sharp stock-fit cutoff for the PR2234 BIT caller

---
 research/bit2234-stock-threshold/README.md    | 237 ++++++++++
 research/bit2234-stock-threshold/RESULT.json  | 104 +++++
 research/bit2234-stock-threshold/SOURCES.json |  40 ++
 research/bit2234-stock-threshold/TASK.json    | 122 +++++
 research/bit2234-stock-threshold/VERIFY.json  |  40 ++
 .../sources/pr2234/NOTICE.md                  |  54 +++
 .../sources/pr2234/PROOF.md                   | 433 ++++++++++++++++++
 .../bit2234-stock-threshold/test_verify.py    | 214 +++++++++
 research/bit2234-stock-threshold/verify.py    | 208 +++++++++
 9 files changed, 1452 insertions(+)
 create mode 100644 research/bit2234-stock-threshold/README.md
 create mode 100644 research/bit2234-stock-threshold/RESULT.json
 create mode 100644 research/bit2234-stock-threshold/SOURCES.json
 create mode 100644 research/bit2234-stock-threshold/TASK.json
 create mode 100644 research/bit2234-stock-threshold/VERIFY.json
 create mode 100644 research/bit2234-stock-threshold/sources/pr2234/NOTICE.md
 create mode 100644 research/bit2234-stock-threshold/sources/pr2234/PROOF.md
 create mode 100644 research/bit2234-stock-threshold/test_verify.py
 create mode 100644 research/bit2234-stock-threshold/verify.py

diff --git a/research/bit2234-stock-threshold/README.md b/research/bit2234-stock-threshold/README.md
new file mode 100644
index 0000000000..ede0d322c4
--- /dev/null
+++ b/research/bit2234-stock-threshold/README.md
@@ -0,0 +1,237 @@
+# Sharp borrowing-fit threshold for the proposed PR2234 BIT caller
+
+For the exact stock prescribed by [Jose Manuel's PR2234](https://github.com/CrocSwap/integer-mult-bounds/pull/2234),
+**311,311 is the least uniform integer cutoff above which the borrowed stock
+always fits**. The result holds for every permitted prime `q>2^80`. At width
+311,310 an explicitly certified prime gives exactly half-width borrowing,
+which violates the source's strict fit condition.
+
+This replaces the word "Eventually" in one stock-fit implication of the
+pending proof. It does not certify that entire construction, change the
+selected frontier, or identify its stock with the fourteen retained
+bootstrap-stage coefficients. No new multiplication exponent is claimed.
+
+## Exact source and theorem
+
+The predecessor is pinned at
+`d047ef86fbc5b1614d3d8e2b8d3441413beab73f`,
+`research/selected-bit-recursive-closure/PROOF.md`, sections 1, 6 and 8.
+Its unchanged [proof](sources/pr2234/PROOF.md) and
+[attribution notice](sources/pr2234/NOTICE.md) are retained with Git blob and
+SHA256 identities in [SOURCES.json](SOURCES.json). No predecessor code runs.
+
+For each integer width `e>=1` and prime `q>2^80`, define
+
+```
+c = 17/10000,  w = ceil(e^c),
+M = lcm(28416,28425) = 269241600,
+K(w) = M |GL_64(F_q)| q^(4096(w-1)),
+D(e) = 0                         if e<64,
+D(e) = 1+D(42 floor(e/64))        otherwise,
+S(e) = K(w)^D(e),  k(e,q) = ceil(log_q S(e)).
+```
+
+**Theorem.** For every such prime and every integer `e>=311311`,
+`k(e,q)<e/2`. No smaller integer can replace 311311 in this uniform statement.
+
+The stock is chosen from the original width `e`, before the body width is
+chosen, exactly as in the source. Sharpness concerns this prescribed stock
+and strict fit test. It does not assert that every smaller width fails, that
+this stock is minimal, or that a different borrowing algorithm cannot work.
+
+## 1. Integer upper bound and exact depth staircase
+
+Counting independent columns gives
+
+```
+|GL_64(F_q)| = q^4096 P(q),
+P(q) = product_(i=1)^64 (1-q^-i),   0<P(q)<1.
+```
+
+Since `M<2^29` and `q>2^80`,
+`log_q K < 4096w+29/80`. The first term is integral after multiplication
+by `D`, so, also when `D=0`,
+
+```
+k <= U(e) := 4096 w D(e) + ceil(29 D(e)/80).                 (1)
+```
+
+Let `b_d` be the first width of depth at least `d`. Inverting the floor
+recurrence gives
+
+```
+b_1=64,   b_(d+1)=64 ceil(b_d/42).
+```
+
+Indeed `D(e)>=d+1` iff `42 floor(e/64)>=b_d`. These thresholds are strictly
+increasing and characterize the entire depth staircase. For
+`311311<=e<2^20`, `1<e^c<2`, hence `w=2` exactly. Equation (1) then gives
+four constant-bound intervals:
+
+| Widths, inclusive | D(e) | U(e) | First width minus 2U(e) |
+| --- | ---: | ---: | ---: |
+| 311311–405311 | 19 | 155655 | 1 |
+| 405312–617663 | 20 | 163848 | 77616 |
+| 617664–941247 | 21 | 172040 | 273584 |
+| 941248–1048575 | 22 | 180232 | 580784 |
+
+The positive margins prove strict fit on all four intervals. All endpoints
+come from the recurrence, rather than a numerical logarithm approximation.
+
+## 2. Infinite tail, including every later atom-width ceiling jump
+
+Two active levels reduce width by a factor less than one half, since
+`2*42^2<64^2`; floors can only reduce the child. Therefore
+`D(e)<=2 ceil(log2 e)` for `e>=2`. This weak bound is sufficient here.
+
+For `e>=2^20`, put `j=floor(log2 e)>=20`. Then
+
+```
+D(e)<=2(j+1),   w=ceil(e^c)<=2*2^(c(j+1)),
+log_q K < 4097w,
+k <= B_j+1,   B_j=16388(j+1)2^(c(j+1)).                    (2)
+```
+
+We prove `B_j+1<2^(j-1)` for every integer `j>=20`. At the first index,
+`21c<1/2` and `sqrt(2)<3/2`, so
+
+```
+B_20+1 < 16388*21*(3/2)+1 = 516223 < 524288 = 2^19.
+```
+
+The ratio of successive normalized `B` terms obeys
+
+```
+(B_(j+1)/2^j)/(B_j/2^(j-1))
+  = ((j+2)/(j+1))*2^c/2 < (22/21)*(3/4) = 11/14 < 1.
+```
+
+The normalized additional 1 contracts by `1/2<=11/14`, so the same strict
+bound persists for `B_j+1`. Combining this with (2) and `e>=2^j` gives
+`k<2^(j-1)<=e/2`. This argument treats all later ceiling jumps without
+enumerating widths or assuming that `k/e` is monotone at those jumps.
+
+## 3. Exact failure at the preceding width
+
+Take
+
+```
+e*=311310,  w=2,  D(e*)=19,
+q*=213*2^80+1 = 257501199577916014212415489.
+```
+
+Section 4 certifies that `q*` is prime. For this prime the verifier checks
+the small integer inequalities
+
+```
+2(q*)^6 < M^19 < (q*)^7,   38 < q*-1.                    (3)
+```
+
+The elementary product inequality `product(1-x_i)>=1-sum(x_i)` implies
+`P(q*)>1-1/(q*-1)`. Bernoulli's inequality then gives
+`P(q*)^19>1-19/(q*-1)>1/2`. Together with (3),
+
+```
+(q*)^6 < M^19 P(q*)^19 < (q*)^7,
+155654 < log_(q*) S(e*) < 155655,
+k(e*,q*) = 155655 = e*/2.
+```
+
+Thus strict fit fails at `311310`. This is a witness for the actual stock,
+not merely a failure of the sufficient upper guard. Every smaller proposed
+universal cutoff includes this width, proving minimality of 311311.
+
+## 4. Self-contained prime certificate
+
+The replay checks
+
+```
+7^((q*-1)/2) mod q* = q*-1,
+(2^80+1)^2 > q*.
+```
+
+Here is the elementary reason this proves primality. If a prime `p` divides
+`q*`, then 7 is a unit modulo `p` and its order divides `213*2^80` but does
+not divide `213*2^79`. Since 213 is odd, `2^80` divides that order and hence
+`p-1`. Consequently `p>=2^80+1>sqrt(q*)`. A composite positive integer has
+a prime divisor no larger than its square root, a contradiction. The check
+uses exact modular exponentiation, with no probable-prime assumption.
+
+## Reproduction and evidence boundaries
+
+From the repository root, using Python 3.12 and the standard library:
+
+```sh
+python3.12 -I -B research/bit2234-stock-threshold/verify.py
+python3.12 scripts/research_package.py --package research/bit2234-stock-threshold
+```
+
+Expected verifier marker:
+`PASS_BIT2234_STOCK_THRESHOLD cutoff=311311 boundary=311310`.
+The registered replay also runs the tests normally and with `-O`.
+Source authentication and acceptance checks do not depend on Python assertions.
+The stored [RESULT.json](RESULT.json) must equal a fresh exact reconstruction;
+missing or changed results fail, without automatic regeneration.
+
+The separate tests build a bottom-up maximum over every child rank 1–42,
+cross-check the inverse staircase through 2^21, test distant exact atom-width
+ceiling boundaries, and reject source/receipt corruption through the public
+CLI in both modes. Boundary controls expose replacing strict fit by weak fit,
+flooring either logarithmic or atom-width rounding, omitting high matrix
+fibers, and a false prime witness. The universal statement rests on the
+written proof above; finite checks do not substitute for its quantifiers.
+
+This result does not implement the full GL64 payload, establish the caller's
+time or restoration contracts, or execute the selected cold replay. Nor does
+it identify a practical runtime cutoff: constants, the fixed prime, and other
+interfaces remain those of the pending construction. The selected-stage
+stock, complex supplier, precision/tape and outer-transfer obligations are
+not discharged by this stock calculation.
+
+## Overlap and scope change
+
+Base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4.
+The `selected-stock-envelope` card is explicitly **changed** to the actual
+reserve of the proposed replacement caller, rather than a retained selected
+bootstrap stage. Its native BIT dimension is 64; the separate complex
+dimension 73 is not substituted here. [TASK.json](TASK.json) records this
+decision, live overlap coverage and the final freshness checkpoint.
+
+PR2084/2120 already supply conditional BIT stock coefficients; PR2105
+studies complex depth; PR2097 supplies a fresh-field theorem. PR2289/2295
+formalize the PR2234 time recurrence and numerical moment. PR2310 and the
+active Discussion2319 concern control preparation and joined dispatch.
+This contribution proves the explicit universal fit threshold and its sharp
+boundary, not those earlier statements. Its
+[canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2209#discussioncomment-18941213)
+is in the existing BIT-closure discussion.
+
+## Open next questions
+
+1. Does a smaller stock, chosen self-consistently from the post-borrow body
+   width, fit earlier while retaining the complete-row divisibility contract?
+   This could reduce reserve without changing the moment. Start by studying
+   the integer fixed-point inequality using `D(floor((e-k)/w))`; first prove
+   that the changed stock supplies every recursive packet. That contract
+   change blocks any direct use of this theorem's sharpness claim.
+2. Can a joined implementation certify fresh fields, restored row/work and
+   the uniform time bound at the same interfaces? This is needed for caller
+   admission. Start with PR2234 sections 5–7 and the PR2310/Discussion2319
+   preparation/dispatch work. Full physical composition remains the blocker;
+   a fit threshold alone cannot certify it.
+
+## Credit
+
+Prepared for Aakash (@aakashthakkar) with substantial OpenAI Codex assistance
+in source review, mathematics, implementation, writing and separate agent
+checks. No independent human review or proof-assistant verification is claimed.
+New work is Apache-2.0, following the repository license.
+
+Jose Manuel (@jmbarrancoml) supplied PR2234's caller, exact reserve and depth
+definitions, and the borrowing argument. Its retained notice credits the
+selected PR589/PR555 word, alephnan's PR1627 proof, eumemic's GL framework,
+source527 and the named routing/parking contributors. Josie Elliston's
+PR1956/1965, ToikY's PR1990, Adam Gall's PR2084/2097, Nick Petalas's PR2120
+and Sricharan Vagvala's PR2105 motivated the distinct stock, fit and producer
+boundaries. Their constructions and generic depth/stock principles are not
+claimed as new here.
diff --git a/research/bit2234-stock-threshold/RESULT.json b/research/bit2234-stock-threshold/RESULT.json
new file mode 100644
index 0000000000..d0aab690a3
--- /dev/null
+++ b/research/bit2234-stock-threshold/RESULT.json
@@ -0,0 +1,104 @@
+{
+  "schema_version": 1,
+  "status": "PROVED_STOCK_FIT_ONLY",
+  "scope": "Prescribed PR2234 K(w)^D(e), all integer e and all primes q>2^80; not supplier admission.",
+  "cutoff": 311311,
+  "parameters": {
+    "dimension": 64,
+    "maximum_rank": 42,
+    "live_families": 28416,
+    "physical_slots": 28425,
+    "multiplicity": 269241600,
+    "atom_power": "17/10000",
+    "source_pr": 2234
+  },
+  "depth_thresholds_through_tail": [
+    64,
+    128,
+    256,
+    448,
+    704,
+    1088,
+    1664,
+    2560,
+    3904,
+    5952,
+    9088,
+    13888,
+    21184,
+    32320,
+    49280,
+    75136,
+    114496,
+    174528,
+    265984,
+    405312,
+    617664,
+    941248,
+    1434304
+  ],
+  "finite_intervals": [
+    {
+      "first": 311311,
+      "last": 405311,
+      "depth": 19,
+      "atom_width": 2,
+      "stock_digit_upper": 155655,
+      "strict_margin_at_first": 1
+    },
+    {
+      "first": 405312,
+      "last": 617663,
+      "depth": 20,
+      "atom_width": 2,
+      "stock_digit_upper": 163848,
+      "strict_margin_at_first": 77616
+    },
+    {
+      "first": 617664,
+      "last": 941247,
+      "depth": 21,
+      "atom_width": 2,
+      "stock_digit_upper": 172040,
+      "strict_margin_at_first": 273584
+    },
+    {
+      "first": 941248,
+      "last": 1048575,
+      "depth": 22,
+      "atom_width": 2,
+      "stock_digit_upper": 180232,
+      "strict_margin_at_first": 580784
+    }
+  ],
+  "tail": {
+    "first_width": 1048576,
+    "first_dyadic_index": 20,
+    "stock_bound_coefficient": 16388,
+    "base_upper_plus_one": "516223",
+    "half_width_at_base": 524288,
+    "normalized_contraction_upper": "11/14"
+  },
+  "sharpness": {
+    "width": 311310,
+    "atom_width": 2,
+    "depth": 19,
+    "prime_certificate": {
+      "q": "257501199577916014212415489",
+      "odd_multiplier": 213,
+      "two_exponent": 80,
+      "base": 7,
+      "modular_residue": "257501199577916014212415488"
+    },
+    "log_q_stock_open_interval": [
+      155654,
+      155655
+    ],
+    "borrowed_digits": 155655,
+    "twice_borrowed_digits": 311310,
+    "integer_power_checks": {
+      "2*q^6<M^19": true,
+      "M^19<q^7": true
+    }
+  }
+}
diff --git a/research/bit2234-stock-threshold/SOURCES.json b/research/bit2234-stock-threshold/SOURCES.json
new file mode 100644
index 0000000000..b99451802d
--- /dev/null
+++ b/research/bit2234-stock-threshold/SOURCES.json
@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    }
+  ],
+  "external_sources": [
+    {
+      "path": "sources/pr2234/PROOF.md",
+      "source_repository": "jmbarrancoml/integer-mult-bounds",
+      "source_pr": 2234,
+      "source_commit": "d047ef86fbc5b1614d3d8e2b8d3441413beab73f",
+      "source_path": "research/selected-bit-recursive-closure/PROOF.md",
+      "git_blob": "6c410cab5713979214a45835091fbeb9ee9b8531",
+      "sha256": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344",
+      "usage": "Exact textual definition and attribution; no predecessor code executed."
+    },
+    {
+      "path": "sources/pr2234/NOTICE.md",
+      "source_repository": "jmbarrancoml/integer-mult-bounds",
+      "source_pr": 2234,
+      "source_commit": "d047ef86fbc5b1614d3d8e2b8d3441413beab73f",
+      "source_path": "research/selected-bit-recursive-closure/NOTICE.md",
+      "git_blob": "a5ccfbecbd225d4b63d9ce85edb2fac90f37147c",
+      "sha256": "c144e34c24470ca53df77527b9687ae9b345a4d88a506d839312ca26584cfe79",
+      "usage": "Exact textual definition and attribution; no predecessor code executed."
+    }
+  ]
+}
diff --git a/research/bit2234-stock-threshold/TASK.json b/research/bit2234-stock-threshold/TASK.json
new file mode 100644
index 0000000000..c0d9d30a98
--- /dev/null
+++ b/research/bit2234-stock-threshold/TASK.json
@@ -0,0 +1,122 @@
+{
+  "schema_version": 1,
+  "task_id": "selected-stock-envelope",
+  "priority_revision": 4,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "original_card": {
+    "id": "selected-stock-envelope",
+    "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?",
+    "starting_points": [
+      "research/selected-bootstrap-stock-audit/README.md",
+      "research/bootstrap-cutoff-time-space-split/README.md",
+      "certificates/selected-result.json",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.",
+      "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope."
+    ],
+    "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #1956/#1965/#1990 in the batch review and the stock-audit source boundary. Its actual selected coefficient remains uncomputed.",
+      "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission."
+    },
+    "first_experiment": "Choose one of the fourteen recorded stages, pin its producer, and derive the parent reserve and depth coefficient. Stop with a precise source-level missing lemma if that coefficient cannot yet be bounded; do not rerun the already checked headroom arithmetic as a new result.",
+    "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.",
+    "allowed_variations": [
+      "One stage or one explicit reserve/depth implication.",
+      "An independently checked same-domain proof repair, retaining all remaining assumptions."
+    ],
+    "scope_change_triggers": [
+      "Importing the historical 57604 or 252 allowance without a selected-producer binding.",
+      "Calling a conditional fit lemma a full outer-proof adoption."
+    ],
+    "overlap_terms": [
+      "selected stock",
+      "stock envelope",
+      "bootstrap cutoff",
+      "1956",
+      "1965",
+      "1990"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Determine the least uniform integer cutoff E0 such that the explicit PR2234 stock K(w)^D(e) fits k=ceil(log_q S)<e/2 for every integer e>=E0 and every prime q>2^80, at c=17/10000.",
+  "scope_change_reason": "Live overlap already covers conditional selected-stage coefficients and depth improvements (#2084/#2105/#2120/#2097). Follow the proposed completed BIT caller #2234 instead: its actual source-defined reserve has only an eventual fit statement. This changes the producer, not the selected-stage sigma_j or frontier.",
+  "bottleneck_link": "Replace one unspecified sufficiently-large-width condition in a proposed completed ordinary caller with a sharp source-bound integer domain; supplier realization and selected-stage adoption remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Finish a universal fit proof, exact boundary witness and independent checks within the 60-minute session, or report the precise unproved step. Do not repeat selected cutoff headroom arithmetic.",
+  "outcome": "completed",
+  "evidence": "Written universal fit proof and actual-prime sharpness witness; exact integer/Fraction verifier reconstructs RESULT.json, authenticates frozen predecessor text, and runs independent all-rank/ceiling/CLI corruption controls. See README and VERIFY.json.",
+  "author": "Aakash (@aakashthakkar), with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance in source review, mathematics, code, writing and separate agent checks; no independent human or formal-kernel review.",
+  "open_questions": [
+    {
+      "question": "Can a smaller post-borrow-body stock fit earlier with complete recursive row divisibility?",
+      "why_it_matters": "Could reduce required reserve; the proved sharp threshold is for the original-width stock only.",
+      "first_step": "Analyze k >= ceil(log_q K(w)^D(floor((e-k)/w))) and verify the changed parent/child row factorization.",
+      "blocked_by": "A proof that the altered stock still supplies all recursive packets and the chosen body width."
+    },
+    {
+      "question": "Does a joined physical implementation establish the completed row/work and uniform-time contracts?",
+      "why_it_matters": "Stock fit does not admit the proposed ordinary caller or an outer multiplication theorem.",
+      "first_step": "Review PR2234 sections 5-7 with PR2310 and active Discussion2319 preparation/dispatch work.",
+      "blocked_by": "Complete caller/primitive composition and independent review, outside this numerical stock audit."
+    }
+  ],
+  "selection": "Priority-4 central-interface override after live handoff/overlap review; specific card retrieval saved outside the package.",
+  "predecessor": {
+    "pr": 2234,
+    "head": "d047ef86fbc5b1614d3d8e2b8d3441413beab73f",
+    "author": "Jose Manuel (@jmbarrancoml)",
+    "path": "research/selected-bit-recursive-closure/PROOF.md"
+  },
+  "freshness": {
+    "upstream_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+    "priority_revision": 4,
+    "checked_utc": "2026-10-15T05:21:09.121942+00:00",
+    "canonical_main_unchanged": true,
+    "predecessor_head_unchanged": true,
+    "coverage": {
+      "open_prs": {
+        "fetched_at": "2026-10-15T05:19:29.186710+00:00",
+        "complete_pagination": true,
+        "records": 539
+      },
+      "discussions": {
+        "fetched_at": "2026-10-15T05:21:08.999557+00:00",
+        "complete_pagination": true,
+        "records": 1036
+      }
+    },
+    "local_records": 1538,
+    "warnings": [],
+    "targeted_matches": "Only this package and its own advance Discussion2209 claim. Separate broad card/predecessor searches inspected the prior conditional results.",
+    "limitations": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission."
+  },
+  "verification": {
+    "interpreter": "CPython 3.12.13",
+    "platform": "macOS arm64",
+    "checks": [
+      "source-bound exact certificate",
+      "8 independent tests including normal and optimized CLI controls",
+      "Registered normal and optimized replay passes",
+      "65 research workflow tests report OK, with 3 skips",
+      "Selected source-binding baseline passes; not a full cold replay"
+    ],
+    "not_checked": [
+      "Full selected cold replay",
+      "Full PR2234 physical payload and time/locality contract",
+      "Fourteen retained selected-stage sigma_j",
+      "Formal-kernel proof or independent human review"
+    ]
+  },
+  "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2209#discussioncomment-18941213",
+  "scope_key": "pr2234-prescribed-stock-c17-over-10000-primes-above-2pow80"
+}
diff --git a/research/bit2234-stock-threshold/VERIFY.json b/research/bit2234-stock-threshold/VERIFY.json
new file mode 100644
index 0000000000..bec74ce5df
--- /dev/null
+++ b/research/bit2234-stock-threshold/VERIFY.json
@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Authenticate predecessor proof/notice; reconstruct exact finite staircase, all-width tail premises and actual-prime sharpness certificate; require stored receipt equality."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent all-rank depth oracle and inverse thresholds, exact large atom ceilings, strict/ceil/prime controls, and normal/optimized public CLI corruptions in temporary copies."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Run the same mathematical and corruption controls with Python assertions disabled."
+    }
+  ]
+}
diff --git a/research/bit2234-stock-threshold/sources/pr2234/NOTICE.md b/research/bit2234-stock-threshold/sources/pr2234/NOTICE.md
new file mode 100644
index 0000000000..a5ccfbecbd
--- /dev/null
+++ b/research/bit2234-stock-threshold/sources/pr2234/NOTICE.md
@@ -0,0 +1,54 @@
+# Attribution and source scope
+
+Jose Manuel (`jmbarrancoml`) prepared this contribution with substantial
+OpenAI Codex assistance in mathematical analysis, code, tests and writing.
+We use the repository's Apache-2.0 license and retain source notices in the
+eight unchanged vendored Python files. `SOURCES.json` records their original
+paths, commits and SHA256 values; we checked byte equality against those
+Git objects before publication.
+
+We credit the following predecessors:
+
+* OpenAI's retained framework and Douglas Colkitt: the stream, ordinary
+  interchange, row-volume and tape contracts, with their source notices.
+* DreamingOfClouds: selected PR589 tuning, on eumemic's PR555 base word.
+  The lineage includes Dugongue's PR541/548 and rohanarun's PR542.
+* alephnan: PR1627, retained as `research/pr589-five-helper-hosting`, for the
+  literal word, whole-call dirty-helper cancellation and chronological proof.
+* eumemic: PR490's whole-owner GL local-ring argument.
+* The source527 contributors: retained normal forms, weighted leaf
+  factorization and ordinary borrowing method, with the existing notices.
+* commdata2338: PR2160 selected good normal form, PR2188 mixed descriptor
+  grammar, and PR1379 unequal-buffer parking boundary. We vendor PR2188's
+  `descriptor.py` unchanged at `77bb4e8cfe3e8c89f6e281eaf948454ee487796a`.
+* RossRichardson: PR2159 full-ring fallback topology, covariance and charge,
+  at `9022b980917b7a9dd0bf1e9cb8012a16ea30293b`.
+* Jose Manuel: PR2157 fixed dyadic routes (`eb1bf93950e9b14f7fadca7892866e9f29a26ad3`),
+  PR2171 controlled streams (`416aac58960660edced905dc7d914c126d357290`),
+  PR2195 GL packet integration (`3a1cf78a1ba6322129e42d80c50d21765524d612`),
+  and PR2207 fallback continuation (`149d55d90d3c0877ed3d78e1deca8eb2f72e0d00`).
+* The authors of the retained `moment.py` and `base_two_moment.py` engines:
+  we reuse their rational arithmetic at one coarse point, with input pins.
+* 1337isnot1337: adjacent PR2212 route inventory, at
+  `cd37bdf943876f81a60522e13cf838a464ed3104`; we do not reproduce that census.
+
+The new work binds the remaining actual residual labels, gives causal symbolic
+field references and completed leaf/header bases, and composes the weighted
+caller by strong induction. We derive the resulting ordinary-interchange
+saving with the elementary base. We claim neither a new generic weighted
+factorization nor a new generic parking lemma.
+
+The retained `physical_stream.py` contains an explicit weighted-child test
+oracle and `qadic_streams.py` contains an ordinary test oracle. We retain
+those files unchanged for their sequential primitives and arithmetic. The
+new completed leaf/header paths never call those oracles; the replay replaces
+them with rejecting functions. Their presence does not implement recursive
+children. PROOF.md supplies that separate construction.
+
+The pending predecessor PRs remain subject to review. We have not merged or
+closed them. The repository's selected result remains unchanged.
+
+For the exact written premises, see the pinned
+[PR2195 packet proof](https://github.com/CrocSwap/integer-mult-bounds/blob/3a1cf78a1ba6322129e42d80c50d21765524d612/research/selected-bit-local-ring-sweeps/PROOF.md),
+[PR2171 adapter proof](https://github.com/CrocSwap/integer-mult-bounds/blob/416aac58960660edced905dc7d914c126d357290/research/selected-bit-controlled-streams/PROOF.md)
+and [PR2207 fallback proof](https://github.com/CrocSwap/integer-mult-bounds/blob/149d55d90d3c0877ed3d78e1deca8eb2f72e0d00/research/selected-bit-fallback-streams/PROOF.md).
diff --git a/research/bit2234-stock-threshold/sources/pr2234/PROOF.md b/research/bit2234-stock-threshold/sources/pr2234/PROOF.md
new file mode 100644
index 0000000000..6c410cab57
--- /dev/null
+++ b/research/bit2234-stock-threshold/sources/pr2234/PROOF.md
@@ -0,0 +1,433 @@
+# Recursive closure of the selected BIT interchange
+
+We give a written construction on a fixed number of finite-alphabet multitape
+streams. We retain the sequential stream model of `02-streams.tex`: complete
+address ranges, arbitrary Boolean payload, charged scans, counters, rewinds and
+scratch erasure. We prove an ordinary binary chunk-interchange bound
+
+    O(V E^(1-a)),  a = 169711/100000000 = 0.00169711,
+
+for two complete E-bit address chunks and arbitrary complete spectators, where
+V counts payload bits. The machine restores spectators and clears its work.
+We fix one odd prime q>2^80 throughout; constants and the fixed tape count may
+depend on q and the selected word. We make no practical runtime claim.
+
+We supply a mathematical algorithm and finite interface checks. We have not
+translated the entire recursive machine into transition tables or a proof
+assistant. Reviewers must assess the composition argument below. The selected
+finite certificate and the multiplication theorem have further interfaces,
+including the complex supplier and analytic transfer; we leave their status
+unchanged.
+
+## 1. Sources and the recursive contract
+
+We use DreamingOfClouds' selected PR589 word, building on eumemic's PR555 word,
+and alephnan's PR1627 literal/chronological proof. We reuse the GL local-ring
+packet integration of PR2195, the good adapters of PR2171, the fallback word
+of PR2159/PR2207, and commdata2338's PR2188 weight grammar. Source527 already
+gives the weighted factorization and outer borrowing method. PR1379 supplies
+the unequal-buffer parking boundary. `SOURCES.json` pins the executable inputs;
+`NOTICE.md` identifies the pending source commits and mathematical reuse.
+
+Fix an original radix-q width e, c=17/10000, and w=ceil(e^c). Put B=q^w and
+R=Z/B. We keep w fixed throughout one coarse recursion. Let C_n reverse n
+atom positions. For a diagonal unit vector A, we construct
+
+    F_A(H,D) = (A C_n D, C_n A^-1 H).
+
+We quantify over any two ordered complete n-atom chunks, with arbitrary
+complete preceding, intervening and following fields. This includes two
+subchunks of one former bank, which we need for fallback reversals. We allow
+arbitrary correlated dirty payload values.
+
+We generate A from a constant unit by the Good and FallbackPair expressions
+below. A may read earlier frozen matrix fields; it may not read this node's
+fresh family, matrix or unused stock. A unit child starts a new constant
+expression but retains its global generation depth. We bound that depth by
+the original root width, including after such a reset.
+
+At return we require the specified address permutation on I/O, pointwise
+restoration of row and spectator coordinates, empty local work and restored
+head positions. For a parking top h, we visit no cell below h-1 and write no
+cell below h. We require a time bound uniform in parked contents and h.
+
+## 2. Actual residuals and full-ring preparation
+
+PR1627 reconstructs 636 rational frame projectors and proves the nesting
+identities used by both selected literal programs. Their entries lie in
+Z[1/2]. For an idempotent P0 of rational rank r, its characteristic polynomial
+is T^(64-r)(T-1)^r. Reduction modulo an odd q preserves this identity and
+idempotent diagonalizability, hence rank r, including when q divides r.
+
+Choose independent image columns of P0 and kernel columns of I-P0 modulo q.
+Their lifts form a unit matrix B0 over R and satisfy
+
+    P0 = B0 diag(I_r,0) B0^-1.
+
+We compute this identity in control arithmetic. We do not move payload through
+B0. For the actual owner chart sigma and raw physical header g, the provider
+passes g sigma B0 to the retained coordinate normalizer. It therefore computes
+exactly P=g sigma P0 sigma^-1 g^-1.
+
+For MOVE, we use the positive nested frame difference and the actual owner
+sigma. The common stage projector cancels. The reflected orientation gives
+the same positive residual. For COPY, we first copy and align the source
+packet to d=g sigma. Its private header is d and its projector label is P0;
+we set its additional chart to I. Applying sigma again would change the
+operator. ERASE retains the literal transported-source equality guard.
+
+For an idle remainder, we subtract the actual hosted slots from its pending
+axes and use the fixed family chart. We skip the zero remainder. The provider
+binds 28,278 canonical requests and 32 replicas, giving
+
+    H_1=381024, H_2=400416, H_3=22752, H_4=26880,
+    H_5=29376, H_6=17376, H_7=26784, H_42=288.
+
+We obtain 541 distinct base labels and 1,235 assembled charts. The finite
+checks verify image/kernel bases over Z/9 and Z/25 for each label, and 120
+full 128-coordinate operators from selected MOVE, COPY and idle requests.
+These cases supplement the identities; they do not enumerate GL64(R).
+
+## 3. One schedule per complete low packet
+
+Write g=g0+qG with g0 in GL64(F_q) and G in [q^(w-1)]^4096. For a fixed
+request, call g0 good when the first r northeast pivots of PC are units.
+Equivalently, require the leading k principal minors of P to be nonzero
+modulo q for 1<=k<=r. Unit tests depend only on g0. The full coefficients
+still depend on G.
+
+For each k, multiply its minor by det(g)^k to obtain a polynomial of degree
+at most 64k in the entries of g. Conjugating the fixed split rank-r projector
+to diag(I_r,0) gives a nonzero witness. The union of these zero sets has
+fraction at most 64r(r+1)/(2q) in all matrices. Since
+
+    |GL64(F_q)|/q^4096 = product_(i=1)^64 (1-q^-i) > 1/2,
+
+the bad fraction for this request is at most 2*64^3/q<10^-16. We use this
+bound separately for each paid edge. We do not require one matrix to be good
+for every label or multiply the bound by the number of labels.
+
+On a good packet, unweighted northeast elimination gives unit-lower matrices
+L,R0 and a pivot vector delta. Split rank and a unit rank-r minor force the
+remaining Schur block to vanish over R itself. We retain q-multiples in the
+arithmetic; reduction modulo q alone would not establish that conclusion.
+The normal-form factorization in source527/PR2171 uses ordered head, tail
+and cross ADDs, one weighted child, and the inverse adapters. For n=64f,
+
+    A_child[k f+j] = A[k f+j] delta_k,  0<=k<r, 0<=j<f.
+
+The child has rf atoms. Both adapter halves contain
+2f(r(127-r)+4096) later-target ADD slots. We retain zero slots, so the schedule
+is common across high lifts and columns. We use no ordinary body interchange
+inside these adapters.
+
+On a bad packet, perform the retained 128-row unnormalized elimination with
+the first available unit pivot. If pi_t tracks original row labels and
+B_j=diag(A[0f+j],...,A[63f+j],1,...,1), the weighted state is
+
+    M_t^weighted = B_(pi_t,j) M_t B_j^-1.
+
+Thus the pivot itinerary equals the unweighted itinerary. A shear i<-i+c k
+uses c*b_(pi_t(i),j)/b_(pi_t(k),j). Row swaps remain unit swaps and advance pi.
+Diagonal pairs use the final pi. We reconstruct in inverse chronology, with
+each shear's own snapshot, as PR2207 does. We retain zero shear slots.
+
+Replace an upper shear by a unit interchange, a later-target shear, and a
+unit interchange. A physical same-orientation interchange uses a reversal
+of the later field, a reversed weighted child, and the same reversal again.
+We implement each reversal by a unit child on its two halves, omitting the
+middle atom when its width is odd. Weighted pair children have width f;
+orientation children have width floor(f/2). We can bound the number directly:
+there are at most 127 elimination swaps, 254 diagonal-pair swaps and twice
+8128 upper-shear brackets. Each swap needs at most three reversed children,
+so 3*(127+254+16256)=49911<32*64^2. We retain the larger source allowance.
+The final sign is a sequential fixed-sign pass.
+
+The branch, slot positions and child widths therefore depend on the fixed
+request and g0, not on G or the incoming unit values. We execute each child
+once on the complete high packet. We never dispatch one child for each G.
+
+## 4. Symbolic ancestry and the completed leaf
+
+`Expression` stores fixed request IDs, low matrices, atom widths, chronological
+field slots and Good/FallbackPair nodes. An evaluator substitutes the values
+of older high fields from its current I/O prefix. A Good node evaluates the
+formula above. A FallbackPair node evaluates
+
+    d_i * b_(pi_final(i),j) / b_(i,j),
+
+with the physical reversal of j when its first field lies in the tail bank.
+The first-unit elimination plan depends only on the stored low matrix; the
+evaluator recomputes the full-ring coefficients from that field's high value.
+Every denominator is a unit. An inductive expression therefore defines unit
+weights on its whole prefix domain.
+
+When entering a child, we append a reference to the current parent field and
+its exact request/low metadata. We freeze that field after the relevant row
+route and preserve it through the child. The child takes its own fresh matrix
+from the unused stock. `FrozenFields` rejects a future field, a changed low
+matrix, or a reference out of chronological order. The evaluator has no unused
+stock argument. One expression serves all high lifts; a numeric matrix from
+one test point cannot stand in for that expression.
+
+For n<64, handle each pair (H_i,D_(n-1-i)) with unit a=A_i. Let J exchange the
+two atoms and L(c) send D to D+cH. In chronological order execute
+
+    J, L(a), J, L(-a^-1), J, L(a), J, D<- -D.
+
+Multiplication gives (H,D)<-(aD,a^-1H), the source527 weighted factorization.
+For J, interchange each of the w corresponding radix-q digit positions.
+For one digit pair, split by its values (x,y) into q^2 sequential buckets,
+then merge in (y,x) order, retaining intervening and suffix fields. Erase the
+buckets and rewind. This uses O_q(V) time per digit and a fixed q^2 tape
+inventory. We use four ordinary atom exchanges, three ordered shifts and one
+sign per pair, hence O(Vw) at a stopped leaf. We require no recursive callee
+there. The n=0 case is identity.
+
+An ordered shift with coefficient c(prefix) rotates a complete B-block target
+fibre by c*x. Split at B-(c*x mod B), merge the two parts in reverse order,
+then erase and reset scratch. This works for zero and nonunit c. A fixed sign
+retains target block zero and reverses the order of the other blocks while
+preserving their internal bits. We retain the PR2171/PR2207 sequential loops.
+
+## 5. Closed header routes and whole-call interpretation
+
+PR2157 gives fixed dyadic words for the selected data/helper charts. Our
+checker replays their inverse words to the actual provider charts. Their
+coefficient alphabet is contained in {+-1/4,+-1/2,+-1,+-2,+-4}. For a fixed
+integer multiplier, split into its fixed number of monotone pieces. For a
+dyadic affine operation, retain the low-digit carry and compose integer
+scaling, an ordered high-field shift, and inverse scaling. A reversed pair
+of header fields uses two elementary high-field interchanges from section 4.
+We charge O(Vw) per fixed route. At w=1 the high fields disappear, but we
+still permute the low classes.
+
+During an individual entry update a work header can have a singular low
+matrix. We interpret that step on the complete high cube. Only at the end
+of the complete column factor do we use the GL header again. We do not invoke
+a residual callee on a partial chart. The complete route is an invertible
+right multiplication and preserves the GL domain. We use the 111 family
+charts only in idle-projector control arithmetic, without routing their
+payload. We never use an arbitrary ancestor-dependent unit as a number of
+monotone-piece tapes.
+
+We now define a complete internal node. Write n=64f+delta. First execute the
+leaf on the last delta head atoms and first delta tail atoms, with weight
+offset 64f. Keep the first 64f head atoms and last 64f tail atoms as the core;
+the peeled fields join its gap. This preserves the existing flat-index rule.
+
+Decode the fresh rows as in section 6. Interpret the pinned global schedule
+in order. At a local sweep, visit its 32 replicas and common low classes;
+finish the whole literal local program before advancing to another low
+class. For each role use its actual complete owned packet. Interpret:
+
+* MOVE: select the owned packet, execute its bound residual by section 3,
+  and replace that packet in its family.
+* ADD: select copies of target and source, route both to the common header,
+  XOR their Boolean payloads, route the target back, and replace only the
+  target packet. Keep the original source. Erase the work copies.
+* COPY: select and align a source copy into fresh private work, then execute
+  the bound rank-seven transport. Keep its common header through the private
+  lifetime. The selected program uses it as a source and never MOVEs it.
+* ERASE: use the matching transported-source guard proved in the literal
+  replay. Erase the equal private work and restore its head.
+
+For a source or target on the private stream, use its common header directly.
+Same-family ADDs still select separate complete low packets. The explicit
+helper completions distinguish them modulo every odd q; pointwise distinction
+of two high matrices alone would not suffice. PR2195 proves this stronger
+low-packet property and the restricted-fibre procedure.
+
+Execute global bridges as family XORs, idle remainders as their bound residuals,
+and the terminal exchange as a fixed family-stream permutation. These are
+the same chronological endpoints as the PR1627/PR2195 whole-call argument.
+At fixed common d, the decoded-frame induction handles correlated dirty
+helpers and the private equality guard. Write the completed low-class
+endpoint as S_d times a product of unary helper permutations R_(j,d).
+The retained local endpoint leaves no helper/data cross terms. The 222 data
+families are distinct, disjoint from helper families, and have matching paired
+source/target routes. Each data route bijects low classes. Consequently
+different common low classes affect disjoint data packets.
+
+Only unary helper endpoints can overlap. For a fixed physical header g,
+helper j appears at precisely the common low class g0 sigma_j. Its endpoint
+preserves g and acts through the projector
+g A_port E_(S_j) A_port^-1 g^-1. The selected supports S_j are disjoint where
+the hosting argument combines them. Their unary permutations commute, and
+the local endpoint identity accepts the previously transformed dirty inputs.
+This proves the whole local sweep. To move endpoints across different global
+calls, we still use the verified untouched hosting intervals; commutation
+alone does not permit crossing an intervening data shear.
+
+For incoming A, conjugate the entire address argument by Q_A=diag(A,I).
+We use the same A across the current family and cover coordinates. It
+commutes with current-header routes and common-frame scalar XOR operations.
+The provider implements the conjugated residuals; the equality guards and
+dirty-helper cancellation carry through. We obtain F_A on every live family.
+We restore the decoded row field and merge the original row order.
+
+`recursive_plan.caller` binds every paid residual to this chronology and
+checks the private-source restrictions. It is a macroplan checker. We do
+not describe its digest as execution of the enormous selected payload.
+
+## 6. Fresh stock, parking and strong induction
+
+Let W=28416 live families, P=28425 physical slots, M=lcm(W,P)=269241600,
+N=|GL64(F_q)|, H=q^(4096(w-1)), and K=MNH. Define
+
+    D(n)=0 for n<64; D(n)=1+D(42 floor(n/64)) otherwise.
+
+For row count t K^D(n), decode [W] x [N] x [H] x [U], where
+
+    U=t*9475*K^(D(n)-1).
+
+Allocate private and selector copies as work, not arbitrary input rows to
+clear. A fixed family/low packet has volume v=V/(WN); we retain all H and U.
+For each child n'<=42 floor(n/64), D(n')<=D(n)-1 and K^D(n') divides U.
+The child receives complete fresh stock for each old high value. It preserves
+the old high field as a spectator. The same argument covers f and floor(f/2)
+fallback children.
+
+Use W live stream tapes and four packet buffers for private, source, target
+and route output. Close split scratch before a child and finish a full-family
+replacement before invoking another child. At a recursive boundary the
+occupied volume is at most V+4v. With B0=W+4 role slots, PR1379's unequal-size
+wrapper costs at most
+
+    5(V+4v)-v+9B0-2 = 5V+19v+9B0-2,
+
+excluding the child. We charge descriptor copies, dispatch and markers too.
+We do not use the equal-volume 14V corollary for these unequal buffers.
+
+Before the child, copy its finite descriptor and control state onto local
+control tapes. Park the inactive payload buffers and caller state above the
+entry delimiter. Move the active complete packet to child I/O. The child
+reads ancestor values from its I/O prefix counters, never from buried parking
+records. It uses relative tape origins, stops at its own delimiters and
+erases only its own visited work. On return restore the inactive buffers and
+caller state. The tape inventory remains fixed: recursive calls reuse the
+same role, bucket, arithmetic and control tapes after parking them.
+
+We prove endpoint, row restoration, scratch closure and locality together by
+strong induction on n. Section 4 supplies the leaves. At an internal node
+the peeled leaf closes; each child width is positive and strictly smaller
+than n and receives the stock and expression contract just proved. Apply
+the induction hypothesis at each parked boundary. The ordered adapters,
+routes, selection and XOR loops close their scratch. Section 5 then proves
+the parent endpoint. PR1379's trace proof composes the delimiter bounds.
+This closes the completed weighted-child premise; we do not assume the
+ordinary supplier whose saving we derive in section 8.
+
+## 7. Uniform time and the stopped recurrence
+
+We account for control work as well as payload movement. Schoolbook ring
+arithmetic, fixed-size elimination and sequential access to the local
+descriptor have polynomial cost in w, log e and the generation depth d.
+A pair descriptor can branch into two parent evaluations; recomputation
+therefore costs at most 2^d times a fixed polynomial, with an additional
+polynomial factor in the root atom count if we prepare a literal vector.
+Since d<=D(e)<=2 ceil(log2(max(2,e))) and e<=w^(1/c), this cost is polynomial
+in w on the stated root-coupled domain.
+
+For an atom ADD, each coefficient preparation accompanies at least q^w
+target blocks. For a header pass the complete high target contributes
+q^(w-1) blocks. Every fixed polynomial divided by either quantity has a
+finite supremum over w>=1. Recompute on split and merge rather than retaining
+an array indexed by the high fibre. Ripple counters have amortized linear
+movement cost; initialize them once per scan and do not reread unrelated
+spectator counters per fibre. Fixed low tables and finite labels depend on
+q, not e. Thus these scans have the stated uniform bounds. For independently
+chosen n,w,d, retain the preparation quotient instead of this absorption.
+
+The selected word has fixed length. Good and bad bodies use O(n) ordered
+atom passes; header routes use O(Vw) each; selections, XORs, erasure and
+parking use O(V) each. We include their finite q-dependent multiplicities
+in a constant C. The local nonrecursive charge is C V(n+w), including the
+remainder leaf. This is an asymptotic accounting, not an explicit optimized
+finite invoice for the selected multiplier. PR2212 prices the separate
+same-family route inventory and leaves further whole-invocation charges.
+
+Normalize by logical volume and bound the worst generated call by T(n,w).
+For positive widths below 64, T<=Cw. The bad fraction is at most epsilon=10^-16
+for each request, and each fallback has at most 32*64^2 children of width at
+most f=floor(n/64). We may overcount good calls on bad classes, obtaining
+
+    T(n,w) <= sum_r (H_r/W) T(r f,w)
+              + epsilon F/W * max_(1<=j<=f) T(j,w) + C(n+w),
+    F=32*64^2*sum_r H_r=118606528512.
+
+We prove a monotone upper bound, so the maximum causes no extra factor.
+Define mu_t=(sum H_r(r/64)^t + epsilon F(1/64)^t)/W. The two retained outward
+rational engines independently give
+
+    mu_1 = 2874298095721977/2890625000000000 < 199/200,
+    mu_(1-c) < 9999/10000.
+
+Induct on n and use f<=n/64. Increasing C to cover the leaf constants gives
+
+    T(n,w) <= 200 C n + 10000 C n^(1-c) w.
+
+Indeed the first term leaves at least Cn after the recursive linear mass,
+and the second leaves at least C n^(1-c)w>=Cw. We treat n=0 separately.
+The resulting constants are independent of ancestor contents, stack top,
+row multiplicity and original e.
+
+## 8. Internal borrowing and binary interchange
+
+Choose the sufficient stock S=K(w)^D(e) from the original width e, before
+choosing a body width. Since M<q, N<q^4096 and H=q^(4096(w-1)),
+
+    log_q K < 4096w+1 <=4097w.
+
+Borrow k=ceil(log_q S)=O(w log e) leading digits from the earlier chunk.
+Eventually k<e/2. The physical order is
+
+    H_hi, H_body, gap, D_hi, D_body.
+
+Use the complete H_hi range as preceding rows; retain D_hi in the gap.
+Pad only that row range to ceil(q^k/S)S, by a factor below two. Split each
+body into whole w-digit atoms and fewer than w remainder digits. Handle
+the remainder by elementary digit interchanges, retaining the other fields.
+
+On the atom bodies use the chronological ordinary wrapper from source527:
+
+    D<-D-H; F_I; D<-D+H; F_I; D<-H-D.
+
+Direct substitution yields (H,D)<-(D,H). The three updates use ordered atom
+passes; the two F_I calls reuse the same restored row stock. Their constant
+multiplicity stays outside the coarse recurrence. Remove the row padding
+after this completed endpoint, then interchange H_hi and D_hi by k elementary
+digit passes. The result is the full ordinary radix-q chunk interchange.
+
+With n<=e/w and w=ceil(e^c), its time is
+
+    O(V [e^(1-c) + e^(1-c+c^2) + e^c log e])
+      = O(V e^(1-c(1-c))).
+
+The first exponent lies below the middle by c^2; the borrowing exponent lies
+below it by (1-c)^2. For the bounded set of small widths where borrowing
+does not fit, use the elementary whole-chunk interchange. Absorb that finite
+set into the same constant. We claim no useful numerical cutoff.
+
+Finally embed each complete binary range [2^E] into
+[q^ceil(E/log2(q))]. Pad both ranges, increasing volume by less than q^2.
+Execute the completed ordinary radix-q interchange and remove padding.
+Its endpoint preserves the genuine rectangle, even though intermediate
+address operations can mix genuine and padded positions. Fixed q preserves
+the exponent and the number of tapes. We obtain the stated binary bound.
+
+## 9. Evidence and remaining limits
+
+We check all source-bound base labels, selected full operators, symbolic
+temporal controls, physical leaves, fixed header routes, low/full plan
+compatibility, chronological request coverage and exact coarse moments.
+The negative controls exercise same-rank label substitution, double owner
+alignment, high-to-low coefficient truncation, wrong inverse, omitted digit
+movement and future-field capture. `RESULT.json` records their scope.
+
+We have not run the entire selected payload, enumerated GL64, produced a
+transition-table compiler, or formalized this proof. Our Python tapes measure
+the specified payload adapters; the written argument accounts for arithmetic
+and recursive control. We prepared the argument and code with substantial
+OpenAI Codex assistance. Independent mathematical review remains necessary.
+We do not infer a multiplication exponent or alter the selected frontier.
diff --git a/research/bit2234-stock-threshold/test_verify.py b/research/bit2234-stock-threshold/test_verify.py
new file mode 100644
index 0000000000..d0f255cc04
--- /dev/null
+++ b/research/bit2234-stock-threshold/test_verify.py
@@ -0,0 +1,214 @@
+#!/usr/bin/env python3
+"""Independent finite oracles and rejection tests; no predecessor execution."""
+from array import array
+import importlib.util
+import json
+from math import lcm
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+import unittest
+
+
+PACKAGE = Path(__file__).resolve().parent
+SPEC = importlib.util.spec_from_file_location("stock_threshold_verifier", PACKAGE / "verify.py")
+verify = importlib.util.module_from_spec(SPEC)
+sys.modules[SPEC.name] = verify
+SPEC.loader.exec_module(verify)
+
+
+def all_child_depths(limit):
+    """Bottom-up maximum over every rank 1..42, independently of max-rank descent.
+
+    All n in [64*f, 64*f+63] have the same child list. Filling one such
+    block at a time makes the exhaustive oracle small enough for CI.
+    """
+    result = array("H", [0]) * (limit + 1)
+    for first in range(64, limit + 1, 64):
+        f = first // 64
+        value = 1 + max(result[rank * f] for rank in range(1, 43))
+        stop = min(first + 64, limit + 1)
+        result[first:stop] = array("H", [value]) * (stop - first)
+    return result
+
+
+def cli(package, optimized):
+    command = [sys.executable, "-I", "-B"]
+    if optimized:
+        command.append("-O")
+    command.append(str(package / "verify.py"))
+    return subprocess.run(command, cwd=package.parent, capture_output=True,
+                          text=True, timeout=60, check=False)
+
+
+def replace_threshold(value):
+    """Change the claimed first universal width without depending on JSON keys."""
+    if type(value) is int and value == 311311:
+        return 311310, 1
+    if value == "311311":
+        return "311310", 1
+    if isinstance(value, list):
+        pairs = [replace_threshold(item) for item in value]
+        return [item for item, _ in pairs], sum(count for _, count in pairs)
+    if isinstance(value, dict):
+        pairs = {key: replace_threshold(item) for key, item in value.items()}
+        return {key: item for key, (item, _) in pairs.items()}, sum(
+            count for _, count in pairs.values())
+    return value, 0
+
+
+class StockThresholdTests(unittest.TestCase):
+    def test_all_child_depth_oracle(self):
+        oracle = all_child_depths(10000)
+        for width, expected in enumerate(oracle):
+            self.assertEqual(verify.depth(width), expected, width)
+        self.assertEqual(oracle[63], 0)
+        self.assertEqual(oracle[64], 1)
+        self.assertEqual(oracle[127], 1)
+        self.assertEqual(oracle[128], 2)
+
+    def test_inverse_thresholds_against_forward_oracle(self):
+        limit = 2 ** 20
+        oracle = all_child_depths(2 * limit)
+        expected = []
+        previous = 0
+        for width in range(64, len(oracle), 64):
+            if oracle[width] > previous:
+                expected.append(width)
+                previous = oracle[width]
+                if width > limit:
+                    break
+        actual = verify.thresholds(limit)
+        self.assertEqual(actual, expected)
+        self.assertGreater(expected[-1], limit)
+        for level, boundary in enumerate(expected, 1):
+            self.assertEqual(oracle[boundary - 1], level - 1)
+            self.assertEqual(oracle[boundary], level)
+        self.assertEqual(expected[18:23],
+                         [265984, 405312, 617664, 941248, 1434304])
+
+    def test_exact_atom_ceilings(self):
+        cases = [(1, 1), (2, 2), (311310, 2), (2 ** 20, 2),
+                 (2 ** 588, 2), (2 ** 589, 3),
+                 (2 ** 10000 - 1, 2 ** 17),
+                 (2 ** 10000, 2 ** 17),
+                 (2 ** 10000 + 1, 2 ** 17 + 1)]
+        for width, expected in cases:
+            self.assertEqual(verify.atom_width(width), expected)
+            self.assertLess((expected - 1) ** 10000, width ** 17)
+            self.assertLessEqual(width ** 17, expected ** 10000)
+
+    def test_strict_fit_and_rounding_controls(self):
+        width = 311310
+        self.assertEqual(verify.depth(width), 19)
+        self.assertEqual(verify.guard(width), 155655)
+        self.assertEqual(verify.guard(width + 1), 155655)
+        self.assertEqual(2 * verify.guard(width), width)
+        self.assertFalse(2 * verify.guard(width) < width)
+        self.assertTrue(2 * verify.guard(width) <= width)  # Incorrect weak fit.
+        self.assertTrue(2 * verify.guard(width + 1) < width + 1)
+        # Flooring the atom width, or omitting the high-lift contribution,
+        # removes 4096*19 digits. It incorrectly announces a fit here.
+        self.assertEqual(verify.guard(width, w=1), 77831)
+        self.assertTrue(2 * verify.guard(width, w=1) < width)
+        # The actual logarithm is strictly between 155654 and 155655;
+        # replacing its ceiling with its floor also gives a false fit.
+        self.assertTrue(2 * (verify.guard(width) - 1) < width)
+
+    def test_finite_guard_intervals(self):
+        first = verify.thresholds(2 ** 20)
+        last_failure = 0
+        for level, (lo, end) in enumerate(zip(first, first[1:]), 1):
+            hi = min(end - 1, 2 ** 20 - 1)
+            if lo > hi:
+                break
+            # Fraction-free rational ceiling, independent of guard().
+            stock = (80 * 8192 * level + 29 * level + 79) // 80
+            self.assertEqual(verify.guard(lo), stock)
+            self.assertEqual(verify.guard(hi), stock)
+            failing = min(hi, 2 * stock)
+            if failing >= lo:
+                last_failure = max(last_failure, failing)
+        self.assertEqual(last_failure, 311310)
+
+    def test_prime_and_actual_stock_sharpness(self):
+        q = 213 * 2 ** 80 + 1
+        self.assertEqual(q, 257501199577916014212415489)
+        self.assertEqual(pow(7, (q - 1) // 2, q), q - 1)
+        self.assertGreater((2 ** 80 + 1) ** 2, q)
+        m = lcm(28416, 28425)
+        self.assertEqual(m, 269241600)
+        self.assertGreater(m ** 19, 2 * q ** 6)
+        self.assertLess(m ** 19, q ** 7)
+        self.assertGreater(q - 1, 2 * 19)  # P^19 > 1-19/(q-1) > 1/2.
+        self.assertIsInstance(verify.verify_proth(q), dict)
+        self.assertIsInstance(verify.sharpness_certificate(), dict)
+        for candidate, base in [(q, 1), (q + 2, 7)]:
+            with self.assertRaises(verify.VerificationError):
+                verify.verify_proth(candidate, base=base)
+        with self.assertRaises(verify.VerificationError):
+            verify.sharpness_certificate(base=1)
+
+    def test_receipt_is_deterministic(self):
+        expected = json.loads((PACKAGE / "RESULT.json").read_text())
+        self.assertEqual(verify.build_receipt(), expected)
+        self.assertEqual(verify.build_receipt(), expected)
+
+    def test_public_cli_and_copy_corruptions(self):
+        with tempfile.TemporaryDirectory(prefix="stock audit ") as temporary:
+            copied = Path(temporary) / "package with spaces"
+            shutil.copytree(PACKAGE, copied, ignore=shutil.ignore_patterns("__pycache__"))
+            result_path = copied / "RESULT.json"
+            source_path = copied / "sources" / "pr2234" / "PROOF.md"
+            original_result = result_path.read_bytes()
+            original_source = source_path.read_bytes()
+            verify.verify_sources(copied)
+            for optimized in (False, True):
+                with self.subTest(optimized=optimized, mutation="none"):
+                    completed = cli(copied, optimized)
+                    self.assertEqual(completed.returncode, 0,
+                                     completed.stdout + completed.stderr)
+                    self.assertEqual(result_path.read_bytes(), original_result)
+                with self.subTest(optimized=optimized, mutation="missing receipt"):
+                    result_path.unlink()
+                    completed = cli(copied, optimized)
+                    self.assertNotEqual(completed.returncode, 0)
+                    self.assertFalse(result_path.exists())
+                    result_path.write_bytes(original_result)
+                with self.subTest(optimized=optimized, mutation="wrong threshold"):
+                    changed, count = replace_threshold(json.loads(original_result))
+                    self.assertGreater(count, 0, "receipt must state its threshold")
+                    damaged = (json.dumps(changed, sort_keys=True) + "\n").encode()
+                    result_path.write_bytes(damaged)
+                    completed = cli(copied, optimized)
+                    self.assertNotEqual(completed.returncode, 0)
+                    self.assertEqual(result_path.read_bytes(), damaged)
+                    result_path.write_bytes(original_result)
+                for key, replacement in (("schema_version", True), ("cutoff", 311311.0)):
+                    with self.subTest(optimized=optimized, mutation="JSON type", field=key):
+                        changed = json.loads(original_result)
+                        self.assertIs(type(changed[key]), int)
+                        changed[key] = replacement
+                        damaged = (json.dumps(changed, sort_keys=True) + "\n").encode()
+                        result_path.write_bytes(damaged)
+                        completed = cli(copied, optimized)
+                        self.assertNotEqual(completed.returncode, 0)
+                        self.assertEqual(result_path.read_bytes(), damaged)
+                        result_path.write_bytes(original_result)
+                with self.subTest(optimized=optimized, mutation="source coefficient"):
+                    self.assertIn(b"269241600", original_source)
+                    damaged = original_source.replace(b"269241600", b"269241601")
+                    source_path.write_bytes(damaged)
+                    with self.assertRaises(verify.VerificationError):
+                        verify.verify_sources(copied)
+                    completed = cli(copied, optimized)
+                    self.assertNotEqual(completed.returncode, 0)
+                    self.assertEqual(source_path.read_bytes(), damaged)
+                    self.assertEqual(result_path.read_bytes(), original_result)
+                    source_path.write_bytes(original_source)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/research/bit2234-stock-threshold/verify.py b/research/bit2234-stock-threshold/verify.py
new file mode 100644
index 0000000000..f7ee08f8c3
--- /dev/null
+++ b/research/bit2234-stock-threshold/verify.py
@@ -0,0 +1,208 @@
+#!/usr/bin/env python3
+"""Exact premises for the PR2234 stock-fit theorem; see README for the proof.
+
+Aakash (@aakashthakkar), with substantial OpenAI Codex assistance. Apache-2.0.
+No floating point, external dependencies, predecessor execution or regeneration.
+"""
+from fractions import Fraction
+import hashlib
+import json
+from math import gcd, lcm
+from pathlib import Path
+import re
+import sys
+
+PACKAGE = Path(__file__).resolve().parent
+LIVE = 28416
+PHYSICAL = 28425
+MULTIPLICITY = 269241600
+DIMENSION = 64
+MAX_RANK = 42
+POWER = Fraction(17, 10000)
+CUTOFF = 311311
+TAIL = 1 << 20
+WITNESS_Q = 213 * (1 << 80) + 1
+
+
+class VerificationError(ValueError):
+    pass
+
+
+def require(ok, message):
+    if not ok:
+        raise VerificationError(message)
+
+
+def depth(e):
+    """Literal source recurrence, evaluated without recursion or a depth cache."""
+    require(type(e) is int and e >= 0, "width must be a nonnegative integer")
+    result = 0
+    while e >= DIMENSION:
+        e = MAX_RANK * (e // DIMENSION)
+        result += 1
+    return result
+
+
+def thresholds(limit):
+    """First width of each positive depth, including the first beyond limit."""
+    require(type(limit) is int and limit >= DIMENSION, "invalid threshold limit")
+    result = [DIMENSION]
+    while result[-1] <= limit:
+        result.append(DIMENSION * ((result[-1] + MAX_RANK - 1) // MAX_RANK))
+    return result
+
+
+def atom_width(e):
+    """Exact ceil(e**(17/10000)); only bounded boundary probes call this."""
+    require(type(e) is int and e >= 1, "atom width requires a positive integer")
+    target = e ** POWER.numerator
+    lo, hi = 0, 1
+    while hi ** POWER.denominator < target:
+        lo, hi = hi, 2 * hi
+    while hi - lo > 1:
+        mid = (lo + hi) // 2
+        if mid ** POWER.denominator >= target:
+            hi = mid
+        else:
+            lo = mid
+    return hi
+
+
+def guard(e, w=None):
+    """Upper bound on ceil(log_q S); optional w is a caller-proved atom width."""
+    if w is None:
+        w = atom_width(e)
+    require(type(w) is int and w >= 1, "invalid atom width")
+    d = depth(e)
+    return DIMENSION**2 * w * d + (29 * d + 79) // 80
+
+
+def verify_proth(q, k=213, s=80, base=7):
+    """Check the elementary prime certificate proved in README section 4."""
+    require(type(q) is int and type(k) is int and type(s) is int,
+            "integer prime certificate required")
+    require(s >= 1 and 0 < k < 1 << s and k % 2 == 1, "invalid Proth shape")
+    require(q == k * (1 << s) + 1, "prime certificate shape mismatch")
+    require(1 < base < q and gcd(base, q) == 1, "nonunit prime witness")
+    residue = pow(base, (q - 1) // 2, q)
+    require(residue == q - 1, "prime witness does not give minus one")
+    require(((1 << s) + 1)**2 > q, "prime-divisor lower bound too small")
+    return {"q": str(q), "odd_multiplier": k, "two_exponent": s,
+            "base": base, "modular_residue": str(residue)}
+
+
+def sharpness_certificate(q=WITNESS_Q, base=7):
+    prime = verify_proth(q, base=base)
+    e = CUTOFF - 1
+    d, w = depth(e), atom_width(e)
+    require((d, w) == (19, 2), "wrong boundary depth or atom width")
+    require(q > 1 << 80, "prime outside the source domain")
+    # P=product(1-q^-i) > 1-1/(q-1), so P^d > 1-d/(q-1) > 1/2.
+    require(2 * d < q - 1, "cover-product lower bound fails")
+    power = MULTIPLICITY**d
+    require(2 * q**6 < power, "sixth-power lower witness fails")
+    require(power < q**7, "seventh-power upper witness fails")
+    integral_part = DIMENSION**2 * w * d
+    stock_digits = integral_part + 7
+    require(2 * stock_digits == e, "boundary is not an exact strict-fit failure")
+    return {"width": e, "atom_width": w, "depth": d,
+            "prime_certificate": prime,
+            "log_q_stock_open_interval": [integral_part + 6, integral_part + 7],
+            "borrowed_digits": stock_digits, "twice_borrowed_digits": e,
+            "integer_power_checks": {"2*q^6<M^19": True, "M^19<q^7": True}}
+
+
+def verify_sources(package=PACKAGE):
+    """Authenticate retained text before reading any source-defined constants."""
+    package = Path(package)
+    manifest = json.loads((package / "SOURCES.json").read_text(encoding="utf-8"))
+    sources = manifest["external_sources"]
+    expected_paths = {"sources/pr2234/PROOF.md", "sources/pr2234/NOTICE.md"}
+    require({row["path"] for row in sources} == expected_paths and len(sources) == 2,
+            "predecessor source inventory mismatch")
+    payloads = {}
+    for row in sources:
+        require(row["source_commit"] == "d047ef86fbc5b1614d3d8e2b8d3441413beab73f",
+                "unexpected predecessor commit")
+        data = (package / row["path"]).read_bytes()
+        require(hashlib.sha256(data).hexdigest() == row["sha256"],
+                "source SHA256 mismatch: " + row["path"])
+        blob = hashlib.sha1(b"blob " + str(len(data)).encode("ascii") + b"\0" + data).hexdigest()
+        require(blob == row["git_blob"], "source Git blob mismatch: " + row["path"])
+        payloads[row["path"]] = data.decode("utf-8")
+    proof = payloads["sources/pr2234/PROOF.md"]
+    require(re.search(r"c=17/10000, and w=ceil\(e\^c\)", proof), "atom-power definition drift")
+    for fragment in (
+        "one odd prime q>2^80", "Let W=28416 live families, P=28425 physical slots, M=lcm(W,P)=269241600",
+        "N=|GL64(F_q)|, H=q^(4096(w-1)), and K=MNH", "D(n)=0 for n<64; D(n)=1+D(42 floor(n/64)) otherwise",
+        "S=K(w)^D(e) from the original width e", "Borrow k=ceil(log_q S)", "Eventually k<e/2",
+    ):
+        require(fragment in proof, "source-definition drift: " + fragment)
+    return {row["path"]: row["sha256"] for row in sources}
+
+
+def build_receipt():
+    require(lcm(LIVE, PHYSICAL) == MULTIPLICITY, "physical/live lcm mismatch")
+    require(MULTIPLICITY < 1 << 29, "multiplicity logarithm allowance fails")
+    require(2 * MAX_RANK**2 < DIMENSION**2, "two-level halving fails")
+    require(20 * POWER < 1, "finite interval no longer has atom width two")
+    stairs = thresholds(TAIL)
+    finite = []
+    for d, (start, end) in enumerate(zip(stairs, stairs[1:]), 1):
+        lo, hi = max(CUTOFF, start), min(TAIL - 1, end - 1)
+        if lo > hi:
+            continue
+        require(depth(lo) == d == depth(hi), "inverse-depth boundary mismatch")
+        upper = DIMENSION**2 * 2 * d + (29 * d + 79) // 80
+        require(2 * upper < lo, "finite interval is not strictly safe")
+        finite.append({"first": lo, "last": hi, "depth": d, "atom_width": 2,
+                       "stock_digit_upper": upper, "strict_margin_at_first": lo - 2 * upper})
+    require(finite[0]["first"] == CUTOFF and finite[-1]["last"] == TAIL - 1,
+            "finite proof does not reach both endpoints")
+    require(all(left["last"] + 1 == right["first"] for left, right in zip(finite, finite[1:])),
+            "finite proof has a coverage gap")
+    # Infinite tail: B_j=16388*(j+1)*2^(c*(j+1)), j=floor(log2 e)>=20.
+    # All irrational comparisons are discharged by c*21<1/2 and sqrt(2)<3/2.
+    require(21 * POWER < Fraction(1, 2), "tail base exponent fails")
+    require(POWER < Fraction(1, 2) and Fraction(3, 2)**2 > 2, "tail ratio premise fails")
+    coefficient = 4 * (DIMENSION**2 + 1)
+    base_upper = coefficient * 21 * Fraction(3, 2) + 1
+    contraction = Fraction(22, 21) * Fraction(3, 4)
+    require(base_upper < 1 << 19, "tail base has no strict margin")
+    require(Fraction(1, 2) <= contraction < 1, "tail plus-one term does not contract")
+    witness = sharpness_certificate()
+    return {
+        "schema_version": 1,
+        "status": "PROVED_STOCK_FIT_ONLY",
+        "scope": "Prescribed PR2234 K(w)^D(e), all integer e and all primes q>2^80; not supplier admission.",
+        "cutoff": CUTOFF,
+        "parameters": {"dimension": DIMENSION, "maximum_rank": MAX_RANK, "live_families": LIVE,
+                       "physical_slots": PHYSICAL, "multiplicity": MULTIPLICITY,
+                       "atom_power": str(POWER), "source_pr": 2234},
+        "depth_thresholds_through_tail": stairs,
+        "finite_intervals": finite,
+        "tail": {"first_width": TAIL, "first_dyadic_index": 20,
+                 "stock_bound_coefficient": coefficient, "base_upper_plus_one": str(base_upper),
+                 "half_width_at_base": 1 << 19, "normalized_contraction_upper": str(contraction)},
+        "sharpness": witness,
+    }
+
+
+def main():
+    try:
+        verify_sources()
+        expected = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8"))
+        actual = build_receipt()
+        canonical = lambda value: json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False)
+        require(canonical(actual) == canonical(expected),
+                "stored receipt differs from exact reconstruction")
+    except (OSError, ValueError, KeyError, TypeError) as exc:
+        print("FAIL_BIT2234_STOCK_THRESHOLD: " + str(exc), file=sys.stderr)
+        return 1
+    print("PASS_BIT2234_STOCK_THRESHOLD cutoff=311311 boundary=311310 intervals=4 "
+          "uniform_prime_domain=q>2^80 exact_prime_witness=verified no_new_kappa")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())