Sharpen R437 row stock to 9475·A^D and certify descendant arithmetic

research/r437-descendant-stock/README.md

@@ -0,0 +1,180 @@
+# R437 descendant stock: retain the 9475 factor once
+
+**Scoped stock theorem and arithmetic path certificate; no new kappa.** For the
+row quotient and stock guard used by the pinned R437 physical caller, sufficient
+root stock is
+
+\[
+ R=t\,9475\,A^{D(n)},\qquad
+ A=28416\,|\mathrm{GL}_{64}(\mathbb F_q)|\,q^{4096(w-1)},\quad t\geq1,
+\]
+
+when `n >= 64`; any positive row count suffices for this internal-node condition
+when `n < 64`. Here `D(n)=0` below 64 and
+`D(n)=1+D(42 floor(n/64))` otherwise. The original root's `q,w` stay fixed.
+
+PR4176's `NUMERICAL.md` section 5 uses the stronger sufficient stock `t K^D`,
+where `K=lcm(28416,28425)|GL64|q^(4096(w-1))=9475 A`.
+Thus at positive depth `D` this component's least sufficient divisor is smaller
+by exactly **9475^(D-1)**. This does not identify a defect in that conservative
+bound. Its `check_stock_rows` intentionally rejects our smaller stock for `D>1`;
+the frozen numerical wrapper is unchanged and does not admit it.
+
+The new divisor is necessary and sufficient for **all paths allowed by this
+rank-ceiling row-guard model**. Necessity is not a claim that every maximal path
+is produced by the actual compiler, or that this is the least stock for every
+other construction obligation. The universal result is the written argument
+below; finite checks support its source binding and implementation.
+
+## Actual source boundary
+
+All sources are exact bytes at canonical main
+`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`; `SOURCES.json` binds their blobs and
+SHA256 digests. No predecessor source is edited.
+
+1. `r437-pooled-native-interface/replica_catalogue.py`, `ReplicaTopology`, has
+   28,416 families. `selected-bit-physical-caller/macro_binding.py`,
+   `SelectedBinding`, sets cutoff 64 and `stock_multiple=9475`.
+2. `fresh_rows.quotient` divides positive rows successively by the family count,
+   `context.codes.size=|GL64(F_q)|`, then by `q` exactly `4096(w-1)` times.
+   Its `radix_power` source yields once per division of `q^w` by `q` until 1;
+   the first of those `w` iterations is skipped for each of 4096 matrix entries.
+   Every remainder must be zero, and the quotient must be positive.
+3. `Machine.node` stores that quotient as `unused` and immediately requires
+   divisibility by 9475. Its `prepare_child` handoff passes `unused` as the
+   child's `rows` port through the fixed `CAPSULE` ordering. It does not divide
+   the child's inherited row count by 9475.
+4. `r437-carrier-integration/numerical.py` supplies the declared maximum paid
+   rank 42 and the depth recurrence. The separate native/compiler claim that
+   every child width is at most `42 floor(n/64)` is retained as a premise.
+
+These facts identify the recurrence `R_child=R_parent/A` and the local
+condition `9475 | R_child`. They do not price `Count` arithmetic, prove the
+complete request inventory, or execute a recursive payload. The source's
+`SelectedBinding.check_stock` placeholder is not presented as an installed
+descendant validator.
+
+## Proof and exact scope
+
+Put `S=9475`. First fix any positive integers `A,S` and a path with exactly `d`
+internal transitions. At transition `j`, starting with `j=1`, the unchanged
+guards require a positive exact quotient `R/A^j` divisible by `S`.
+The final condition implies `S A^d | R`. Conversely, if `R=t S A^d`, every
+quotient is the positive integer `t S A^(d-j)`, so all guards pass. Consequently
+the least positive stock on a path of length `d` is **S A^d**, without any
+coprimality assumption about `A` and `S`. With zero transitions no guard is run.
+
+For the width model, let `g(n)=42 floor(n/64)`. On internal widths, `g` is
+nondecreasing and strictly smaller than `n`. Iterating it shows that `D` is
+nondecreasing. Every permitted child `1 <= c <= g(n)` therefore satisfies
+`D(c) <= D(n)-1`. Along a path at depth `j`, `D(n_j) <= D(n_0)-j`.
+Starting with `R_0=t S A^D`, exact row inheritance gives
+
+\[
+ R_j=t S A^{D-j}.
+\]
+
+If node `j` is internal, `D-j >= 1`, so its quotient remains divisible by `S`.
+Moreover its inherited rows are divisible by the new sufficient divisor for
+its entire remaining subtree: for `D(n_j)>0`, the multiplier is
+`t A^(D-j-D(n_j))`. At a leaf the divisor is 1. This proves all bounded paths
+are covered, including early leaf termination and paths stopping internally.
+
+The maximal path `n,g(n),g(g(n)),...` has exactly `D(n)` transitions in the
+declared model. Applying the first paragraph to that path proves necessity
+within the model. A compiler that forbids that path might permit less stock;
+we make no such reachability claim. Additional stock predicates outside the
+two identified guards are also outside this minimum claim.
+
+`stock.py` implements a separate arithmetic certificate. It anchors the first
+node to a supplied root, preserves its field and precision, checks the rank
+ceiling, and requires **exact** parent-to-child row equality. Local divisibility
+alone is insufficient: at widths `128 -> 84`, twice the correct child stock
+passes its local divisibility test but is not the parent's quotient. The
+checker rejects that forged path. The supplied root still needs external
+prime, precision, source and Program authentication. This component does not
+replace PR4176's complete `checked_entry` or remove its root-only restriction.
+
+## Reproduction and evidence
+
+Python 3.12, standard library only:
+
+```sh
+python -B scripts/research_package.py --package research/r437-descendant-stock
+```
+
+Direct replay, including in a Git-free export containing the declared inputs:
+
+```sh
+python -B research/r437-descendant-stock/verify.py
+python -O -B research/r437-descendant-stock/verify.py
+```
+
+Ordinary verification is read-only and compares the complete deterministic
+`RESULT.json`. Explicit `--write` is reserved for receipt regeneration.
+The receipt reports:
+
+- 1,024 width comparisons with the pinned depth function and **323,232** child
+  transitions checking the depth inequality.
+- **25,620** exhaustive abstract `(A,S,d,R)` cases comparing the formula with
+  repeated local guards (`A=1..5`, `S=1..4`, `d=0..4`, `1 <= R <= 2 S A^d+1`,
+  with leaf divisor 1). These include non-coprime factors.
+- **14** internal nodes through the unchanged AST of `fresh_rows.quotient` and
+  the four-statement quotient/stock block in `Machine.node`, using an explicitly
+  substituted **integer Count/Word adapter**, including the source's radix loop.
+  This checks control-flow arithmetic,
+  not binary tape operations, acquisition, cleanup or timing.
+- Four full maximal paths with `(q,w,n)=(3,1,64),(3,2,128),(5,2,512),(3,2,2048)`.
+  At width 512, depth 4, the old/new stock factor is **850,624,046,875**. At
+  width 2048, depth 7, it is **723,561,269,122,002,197,265,625**. These are row
+  cardinality ratios, not time savings or practical materialized datasets.
+- **17** rejecting controls, including locally divisible but unrelated rows,
+  lost high-lift/family/9475 factors, one missing recursive factor, precision
+  and field changes, wrong widths, missing roots, and continuation below cutoff.
+  Three controls confirm that the predecessor's stronger wrapper rejects the
+  new smaller stock; this is expected, not a failed predecessor test.
+
+The q=3/q=5 fixtures are semantic arithmetic checks, not the q>2^80 numerical
+admission. No full selected cold replay, compiler catalogue, Lean, Docker,
+native payload, source preparation or physical tape simulation was run. The
+orientation command `research_selected_baseline.py` stopped on an omitted
+`certificates/checkpoints/frontier4359.json` in this sparse checkout; no baseline
+pass is claimed. The selected record remains conditional kappa 0.00302015.
+
+## Coordination and attribution
+
+Task `r437-carrier-integration`, revision 7, refined from the bit-mechanisms
+draw `5b8bdff3d61d78a94ac212b844fcd944` to this exact stock implication.
+[Discussion #4682](https://github.com/CrocSwap/integer-mult-bounds/discussions/4682)
+is the canonical claim/result. Overlap checks covered R437, descendant/path
+certificates, 9475 and stock-divisor terms. The initial remote snapshot had
+448 open PRs and 3,606 Discussion records with complete pagination; local
+coverage was sparse and closed PR bodies/code diffs were not fully searched.
+The central ledger was consulted. PR4584 audits the separate pivot implication;
+PR4612 concerns selected BIT row stock, with different atom and call boundaries.
+
+Chris R / Clear1nsight's PR4067 and PR4176 supply the changed carrier, complete
+source interface, conservative K^D bound and explicit descendant-certificate
+gap. unpaidmoon / PR4147 supplies the earlier coefficient audit, not recomputed
+here. The literal caller and stock interfaces retain Jose Manuel /
+jmbarrancoml, David Arias, Nick Petalas, ywz65 and the PR2753/2769 lineage.
+The R437/hosting/source predecessors retain ai-nanachi, Ali Romman, Sagar Thakrar,
+Rohan Arun, zxv, Ross Richardson and all notices in the pinned packages.
+New proof, arithmetic certificate and checks: Mihir Srivastava (mihir-s-05),
+with substantial OpenAI Codex assistance. Apache-2.0. This is author-checked
+work with separately written arithmetic, not independent human review or
+formal proof-kernel verification.
+
+## Open next questions
+
+1. **Bind an arithmetic path to actual produced Program events.** This is
+   necessary before extending the numerical entry to descendants. Start with
+   one authenticated `checked_entry` root, its `Machine.prepare_child` handoff
+   and decoded chronological STEP. The blocker is proving actual request,
+   width, source identity and inherited `rows` correspondence; a list of valid
+   integers does not establish that correspondence.
+2. **Price or implement the guard on the physical Count tapes.** The theorem
+   removes a repeated stock factor but gives no physical cost reduction. Start
+   by running the unchanged quotient and stock check with real tape Count
+   objects and the same fixed root precision. Complete source-table, payload,
+   visited-backing and blank-return costs remain separate obligations.

research/r437-descendant-stock/RESULT.json

@@ -0,0 +1,120 @@
+{
+  "abstract_guard_cases": 25620,
+  "bounded_child_transitions": 323232,
+  "depth_widths": 1024,
+  "fixtures": [
+    {
+      "certificate": {
+        "depth": 1,
+        "root_multiplier": 1,
+        "scope": "arithmetic stock only; Program/source binding remains external",
+        "terminal_width": 42,
+        "transitions": 1
+      },
+      "old_to_new_factor": "1",
+      "q": 3,
+      "root_stock_bits": 6520,
+      "root_stock_sha256": "b4b2fab41fd0a7ab8f92729e4049ab786f2b7de7db4938ba58754e3ce4c38be3",
+      "w": 1,
+      "widths": [
+        64,
+        42
+      ]
+    },
+    {
+      "certificate": {
+        "depth": 2,
+        "root_multiplier": 1,
+        "scope": "arithmetic stock only; Program/source binding remains external",
+        "terminal_width": 42,
+        "transitions": 2
+      },
+      "old_to_new_factor": "9475",
+      "q": 3,
+      "root_stock_bits": 26010,
+      "root_stock_sha256": "fb854591452036d2cbacbaad05d441a36f7f0f8434c7b8f185c9b877811d15b2",
+      "w": 2,
+      "widths": [
+        128,
+        84,
+        42
+      ]
+    },
+    {
+      "certificate": {
+        "depth": 4,
+        "root_multiplier": 1,
+        "scope": "arithmetic stock only; Program/source binding remains external",
+        "terminal_width": 42,
+        "transitions": 4
+      },
+      "old_to_new_factor": "850624046875",
+      "q": 5,
+      "root_stock_bits": 76156,
+      "root_stock_sha256": "8bd793adab2a26e4096b73ab69c93bf9c55f9d61f5d467d68265d40d1158815c",
+      "w": 2,
+      "widths": [
+        512,
+        336,
+        210,
+        126,
+        42
+      ]
+    },
+    {
+      "certificate": {
+        "depth": 7,
+        "root_multiplier": 1,
+        "scope": "arithmetic stock only; Program/source binding remains external",
+        "terminal_width": 42,
+        "transitions": 7
+      },
+      "old_to_new_factor": "723561269122002197265625",
+      "q": 3,
+      "root_stock_bits": 91000,
+      "root_stock_sha256": "46cf1c4882729cec1f8ffa18058b80433c0c8a4e0a56344a05be475a24c00cdc",
+      "w": 2,
+      "widths": [
+        2048,
+        1344,
+        882,
+        546,
+        336,
+        210,
+        126,
+        42
+      ]
+    }
+  ],
+  "literal_internal_nodes": 14,
+  "rejected_controls": [
+    "old_guard_rejects_new_stock_n128",
+    "old_guard_rejects_new_stock_n512",
+    "old_guard_rejects_new_stock_n2048",
+    "locally_valid_but_unrelated_descendant",
+    "changed_precision",
+    "changed_field",
+    "missing_root",
+    "wrong_child_width",
+    "transition_below_cutoff",
+    "noninteger_rows",
+    "empty_path",
+    "lost_9475_factor",
+    "inexact_family_factor",
+    "empty_stock",
+    "lost_high_lift_factor",
+    "undivided_child_rows",
+    "one_missing_recursion_factor"
+  ],
+  "scope": "Sharp row-guard arithmetic; integer Count adapter, no tape/payload replay, supplier admission or new kappa",
+  "source_sha256": {
+    "research/r437-carrier-integration/NUMERICAL.md": "e2303eec688d963390f5df4440300bee75840c2c485d94d7342a7d2ef1430438",
+    "research/r437-carrier-integration/numerical.py": "83f2b60a90ab2d0354c5c84f48af246ab416605c3ae4bd62368bbe5f23bb53bb",
+    "research/r437-pooled-native-interface/replica_catalogue.py": "d093a5a5421596d82c6c6e9fbc7fbf3f313c803a7ba423d666b98344b1912ff3",
+    "research/selected-bit-physical-caller/inputs/pr2753/predecessor/fresh_rows.py": "e4ae08fbd658add630eb7754ebe0cbcb42c6f39cf4128f9cb92e27fcf5213a7d",
+    "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/cardinality.py": "505d5e560c5a507e6184edcc19a87cf1fed243eb34a5cb21fbe1e4fe017e7f22",
+    "research/selected-bit-physical-caller/macro_binding.py": "9ef31765d03d2c54fad9296f2ff0707a190ce169e44de4f0f45214e3c410c01a",
+    "research/selected-bit-physical-caller/macro_machine.py": "7bc6e42072a09a08ac961e05c3da01cde012d740d4b4c605f298d994f2ad7c5a"
+  },
+  "status": "PASS_R437_DESCENDANT_STOCK"
+}

research/r437-descendant-stock/SOURCES.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "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/r437-carrier-integration/NUMERICAL.md",
+      "usage": "input",
+      "git_blob": "1001480b0ba8da8bae4ae8f53c18d8c6aa9d7b57",
+      "sha256": "e2303eec688d963390f5df4440300bee75840c2c485d94d7342a7d2ef1430438"
+    },
+    {
+      "path": "research/r437-carrier-integration/numerical.py",
+      "usage": "input",
+      "git_blob": "d3411758be96f22f8d64e02ba278dc46b21639c5",
+      "sha256": "83f2b60a90ab2d0354c5c84f48af246ab416605c3ae4bd62368bbe5f23bb53bb"
+    },
+    {
+      "path": "research/r437-pooled-native-interface/replica_catalogue.py",
+      "usage": "input",
+      "git_blob": "1fa6ea58c5193952bc6175cbb9f1a778a6502eac",
+      "sha256": "d093a5a5421596d82c6c6e9fbc7fbf3f313c803a7ba423d666b98344b1912ff3"
+    },
+    {
+      "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/fresh_rows.py",
+      "usage": "input",
+      "git_blob": "aa3a327604308d3a5c7a27b65f5e631d430ab093",
+      "sha256": "e4ae08fbd658add630eb7754ebe0cbcb42c6f39cf4128f9cb92e27fcf5213a7d"
+    },
+    {
+      "path": "research/selected-bit-physical-caller/macro_binding.py",
+      "usage": "input",
+      "git_blob": "c197eb6458be9374cb4684c654bfc99e619dcaf0",
+      "sha256": "9ef31765d03d2c54fad9296f2ff0707a190ce169e44de4f0f45214e3c410c01a"
+    },
+    {
+      "path": "research/selected-bit-physical-caller/macro_machine.py",
+      "usage": "input",
+      "git_blob": "5a032e8923f7f8b22bb98f3e39b804beb9906c16",
+      "sha256": "7bc6e42072a09a08ac961e05c3da01cde012d740d4b4c605f298d994f2ad7c5a"
+    },
+    {
+      "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/cardinality.py",
+      "usage": "input",
+      "git_blob": "b8ba857e32c5903408e1e61ff916300848b4a208",
+      "sha256": "505d5e560c5a507e6184edcc19a87cf1fed243eb34a5cb21fbe1e4fe017e7f22"
+    }
+  ]
+}