From a37805e3af702295062dd9986bc92a4b186fc166 Mon Sep 17 00:00:00 2001
From: JoyboyBrian <gzybrian@gmail.com>
Date: Fri, 23 Oct 2026 00:50:44 -0700
Subject: [PATCH 1/2] Prove eligibility-sensitive selected source envelope
 below 3.070 N

---
 .../README.md                                 | 119 +++++
 .../RESULT.json                               | 256 +++++++++
 .../SOURCES.json                              |  53 ++
 .../TASK.json                                 | 101 ++++
 .../VENDOR.json                               |  37 ++
 .../VERIFY.json                               |  36 ++
 .../vendor/flow-README.md                     | 496 ++++++++++++++++++
 .../vendor/flow.py                            | 198 +++++++
 .../vendor/predecessor.md                     | 252 +++++++++
 .../vendor/selected-PROOF.md                  | 102 ++++
 .../vendor/selected.json                      | 274 ++++++++++
 .../verify.py                                 | 194 +++++++
 12 files changed, 2118 insertions(+)
 create mode 100644 research/selected-truncated-source-envelope/README.md
 create mode 100644 research/selected-truncated-source-envelope/RESULT.json
 create mode 100644 research/selected-truncated-source-envelope/SOURCES.json
 create mode 100644 research/selected-truncated-source-envelope/TASK.json
 create mode 100644 research/selected-truncated-source-envelope/VENDOR.json
 create mode 100644 research/selected-truncated-source-envelope/VERIFY.json
 create mode 100644 research/selected-truncated-source-envelope/vendor/flow-README.md
 create mode 100644 research/selected-truncated-source-envelope/vendor/flow.py
 create mode 100644 research/selected-truncated-source-envelope/vendor/predecessor.md
 create mode 100644 research/selected-truncated-source-envelope/vendor/selected-PROOF.md
 create mode 100644 research/selected-truncated-source-envelope/vendor/selected.json
 create mode 100644 research/selected-truncated-source-envelope/verify.py

diff --git a/research/selected-truncated-source-envelope/README.md b/research/selected-truncated-source-envelope/README.md
new file mode 100644
index 0000000000..2e90ed5948
--- /dev/null
+++ b/research/selected-truncated-source-envelope/README.md
@@ -0,0 +1,119 @@
+# A truncated-source envelope for the selected nested compiler
+
+**Author-checked scoped proof; no new κ or physical admission.** For the unchanged selected #4470 product/completion/splitting rule and #4436 nested widths, let `H=64215200000000`, `N=2^H` and `K=ceil(log2 B_N)/H`. This package improves [Sagar Thakrar's #5026](https://github.com/CrocSwap/integer-mult-bounds/pull/5026) upper bound from `K/N < 3.639` to **`K/N < 3.070`**. Its inherited lower bound `K/N > 2.943` is unchanged, so the conditional bracket has ratio below `1.044`. The selected conditional κ remains `60403/20000000`.
+
+The new ingredient is an eligibility-sensitive source census and a first-moment bound on its root and nonroot terms. It changes no batching, call, completion, split, complement or physical tariff. It does not optimize the outer cutoff. The general inequality is uniform at every integer rank `n>=M`; the numerical accumulated result applies at the selected `N` without constructing that integer.
+
+## Source-bound definitions
+
+Use the positive productive multiplicities `T_k`, paid multiplicities `P_r`, ambient rank `M=max k`, productive floor `L=min k>=2`, and `max r<M`. Write `W=sum T_k`, `T1=sum k T_k`, `P1=sum r P_r`, `x=n/M`, and `G=max{g:M L^g<=n}`. Define `c(a)=product k^a_k` and `u(a)=multinomial(|a|;a) product T_k^a_k`. A chronological paid path `sigma` has multiplier `rho_sigma`; repetitions are separate path positions, not rank mass.
+
+The pinned #4436 implementation instantiates `u(a)` units at depth `d` precisely when `|a|=G-d` and `rho_sigma c(a)<=x`. Each unit has `T_k` target slots of rank `rho_sigma c(a)k`. Its Pascal matching rule consumes every child demand when the parent point exists; when it does not, the child slot receives a distinct new top source. The target-slot label consists of the chronological path, unit instance and target position. These labels remain distinct even when their ranks coincide. Aggregating labels by rank sums positive integer counts and never aliases source arrays.
+
+## Exact truncated root and nonroot census
+
+The root count is exactly
+
+```text
+R_n = W sum_{|a|=G, c(a)<=x} u(a).
+```
+
+For a nonroot depth `d=1,...,G`, let `sigma` be a paid path of length `d-1`, and let `r` be its next chronological paid position. The source count is exactly
+
+```text
+D_(n,d) = sum_sigma sum_r sum_{|a|=G-d} sum_k
+          u(a) T_k [rho_sigma r c(a)<=x<rho_sigma c(a)k].
+S_n = R_n + sum_(d=1..G) D_(n,d).
+```
+
+Here `sum_r` includes each paid position, with its full multiplicity. The first indicator is the actual child-unit eligibility condition. The second is the absence of the parent point `a+e_k`. If that point exists, the complete Pascal identity says its supply is `u(a+e_k)`, at least the eligible child demand, so no new source is created. If it is absent, every eligible demanded slot is a source. This proves the formula without assuming full layers or monotonicity.
+
+Every counted source rank `s` satisfies `x<s<=n`. At the root, `s=c(a)k>=L^(G+1)>x`, and eligibility gives `s<=M c(a)<=n`. At a nonroot source, absence gives `rho_sigma c(a)k>x`; multiplying by `r>=1` gives `s=r rho_sigma c(a)k>x`, while child eligibility and `k<=M` give `s<=n`. The interval is strict at its lower end. This is the useful truncation constraint, not an additional assumed rule.
+
+## Uniform weighted envelope, including every nonroot layer
+
+Since each source has `s>x`, its unit count satisfies `1<s/x`. Sum over the exact census, then enlarge each eligible set only *after* introducing its rank weight. The full rank-weight sum of the root target slots is `T1^(G+1)`. At depth `d`, summing paid paths contributes `P1^d`, the remaining productive word contributes `T1^(G-d)`, and the final target slot contributes `T1`. Consequently, uniformly for every `n>=M`,
+
+```text
+S_n < (T1/x) sum_(d=0..G) P1^d T1^(G-d).                   (1)
+```
+
+This bound counts sources, not paid rank mass as paid calls. In particular, if `P1<=T1`,
+
+```text
+S_n < (G+1) T1^(G+1)/x
+    <= (G+1) T1 (T1/L)^G.                                (2)
+```
+
+The second step uses `x>=L^G`. The old untruncated count scales with `(W+Q+1)^G`, where `Q` is paid call count; (2) instead scales with `(T1/L)^G`. Both root and missing-parent terms are included. No exact source count or height monotonicity is assumed, except the elementary monotonicity of `G(n)` itself.
+
+## Fully charged selected application
+
+The retained selected invoice gives raw productive count `W0=10928`, productive rank mass `T10=239886`, paid rank mass `P10=239134`, and ambient rank `145`. The fixed product power is `v=1024`, productive completion floor `L=21^v`, and paid split cutoff `J=20^v`. If `D` is the sum of all completion ranks, chronological product, completion and splitting give exactly
+
+```text
+T1 = T10^v + D,       P1 = P10^v + D,
+0 <= D <= W0^v L,    T1-P1 = T10^v-P10^v > 0.
+```
+
+Each completion is paid on disjoint coordinates of its target, and splitting preserves its full rank mass. Thus `P1<T1<=U`, where `U=239886^1024+10928^1024*21^1024`. The condition needed by (2) is proved from the charged invoice, not inferred from a favorable uncharged profile. There is no need to materialize the product histogram.
+
+Use the same exact integer height upper bound as #5026:
+
+```text
+h = floor((H-(bit_length(M)-1))/(bit_length(L)-1))
+  = 14279564152,                 M=145^1024.
+```
+
+For every `M<=n<=N`, `G(n)<=h`. Since `U/L>=W>=1`, (2) implies
+
+```text
+log2 S_n < log2(h+1) + log2 U + h log2(U/L)
+         < bit_length(h+1) + bit_length(U)
+           + h (bit_length(U)-(bit_length(L)-1))
+         = X = 197115103572543.
+```
+
+Only integers with tens of thousands of bits occur in this calculation. The previous `X` was `233670787813430`. Nested widths satisfy `B_n=B_(n-1)S_n` above the base and `B_n=1` below it, hence `log2 B_N < N X`. Because `NX` is an integer, `ceil(log2 B_N)<=NX`. Finally the exact comparison `1000X < 3070H` proves `K/N<3070/1000`. This upper sum does not replace `S_n` by a monotone interpolation. Every complement and exit batch continues using the original nested divisible width; complements are part of the program but create no extra factor in its defining `B_n=B_(n-1)S_n` recurrence.
+
+## Discriminating finite fixtures
+
+The actual selected invoice at reduced product power `v=1`, after the same completion and splitting, has these independently computed root and nonroot counts:
+
+| n | G | Root | Nonroot | Total |
+| ---: | ---: | ---: | ---: | ---: |
+| 3044 | 0 | 10928 | 0 | 10928 |
+| 3045 | 1 | 85150976 | 243240704 | 328391680 |
+| 3046 | 1 | 85150976 | 243240704 | 328391680 |
+| 63944 | 1 | 119421184 | 0 | 119421184 |
+| 63945 | 2 | 663496404992 | 7221750536448 | 7885246941440 |
+| 63946 | 2 | 663496404992 | 7221750536448 | 7885246941440 |
+
+At `n=3045`, one missing-parent source has `d=1`, parent multiplier `1`, paid rank `20`, child column `1`, target rank `145`, source rank `2900` and multiplicity `1254400`. The child is eligible because `145*20<=3045`, but the parent point is absent because `145*145>3045`. Thus a root-only bound misses actual sources.
+
+Inside the same height-one slab, increasing `n` from `3624` to `3625` increases the root count from `85150976` to `90046720` but reduces nonroot demand from `243240704` to `208492032`. The total falls from `328391680` to `298538752`. This directly rejects monotonicity of `S_n`.
+
+The verifier independently computes weighted ordered-word sums and compares the entire source-rank spectrum with the pinned multivariate Pascal implementation on all six selected fixtures. Twelve tiny literal chronological replays also agree, including a paid/target overlap control. Distinct chronological copies are retained through multiplicities; no production product or huge-rank word is expanded. Six semantic controls reject omitted eligibility, omitted nonroot demand, source monotonicity, rank-mass/call confusion, omitted paid completion and omitted source complements. They use explicit exceptions and run under `-O`.
+
+## Reproduction and evidence boundary
+
+Python 3.12, standard library only, from repository root:
+
+```sh
+python3.12 -I -B research/selected-truncated-source-envelope/verify.py
+python3.12 -I -O -B research/selected-truncated-source-envelope/verify.py
+python3.12 scripts/research_package.py --package research/selected-truncated-source-envelope
+```
+
+Source spectra are compared in full during replay and retained as deterministic SHA256 receipts. The numerical and finite receipt is [RESULT.json](RESULT.json). Immutable inputs, hashes, original paths and commits are in [VENDOR.json](VENDOR.json) and [SOURCES.json](SOURCES.json). Pending #5026's exact relevant README is retained, as are the selected invoice/proof and #4436 flow implementation/proof. Direct verification is Git-free. Provenance and source-history checks are separate from mathematical validation. All package checks are author-checked; independent review and proof-kernel validation are not claimed.
+
+This is a uniform source-count proof under the unchanged compiler and native hypotheses, supported by finite calibrations. It is not an emitted compiler, minimal width, physical row-depth admission, optimal coefficient, new outer cutoff, new κ, or a proof of the multiplication theorem. Native all-column, owned storage, routing, whole-job adapters, precision/tape, analytic, prime and recovery obligations remain inherited and unrun.
+
+## Open next questions
+
+1. Can a fractional moment or a sharper eligible-boundary law further reduce the interval between the inherited `2.943` lower and new `3.070` upper coefficients? First derive a uniform moment bound preserving the same nonroot absence indicator and all completion mass; a new histogram census or outer-root calculation alone does not answer it. No further expansion is needed for the present result.
+2. Physical realization remains a separate handoff: bind this permitted mathematical width to the actual fixed-program stock/ownership/routing interface and its complete tariff. This package does not provide that implementation.
+
+## Attribution
+
+Prepared by JoyboyBrian with substantial OpenAI Codex (GPT-6 Astra) assistance. New material is Apache-2.0. Credit Sagar Thakrar (#5026 and its explicit truncated-source handoff); James Reed/jwr404 (#4972/#4970); Mark/Matarener (#4612 and stock audit); zxv (#4436 nested widths and flow, strictification and retained stock/native sources); Cinna Davis and zxv (#4440/#4470); Jacob Alan Sussman (Theorem 1G multinomial lockstep construction); Ryanson Jonathan (#4476); and mihir-s-05 (#4507/#4519). Retained files preserve their original notices and predecessor attribution. The canonical investigation is [Discussion #5061](https://github.com/CrocSwap/integer-mult-bounds/discussions/5061). Source/publication provenance is not scientific acceptance.
diff --git a/research/selected-truncated-source-envelope/RESULT.json b/research/selected-truncated-source-envelope/RESULT.json
new file mode 100644
index 0000000000..149fe54601
--- /dev/null
+++ b/research/selected-truncated-source-envelope/RESULT.json
@@ -0,0 +1,256 @@
+{
+  "coefficient": {
+    "H": 64215200000000,
+    "K_over_N_strict_upper": "3070/1000",
+    "N": "2^64215200000000",
+    "Tbar_log2_upper": 18301,
+    "X": 197115103572543,
+    "height_upper": 14279564152,
+    "previous_X": 233670787813430,
+    "previous_strict_upper": "3639/1000",
+    "ratio_log2_upper": 13804,
+    "raw_paid_mass": 239134,
+    "raw_target_mass": 239886
+  },
+  "evidence": "author-checked scoped proof and finite calibration",
+  "literal_checks": [
+    [
+      5,
+      2,
+      0,
+      2
+    ],
+    [
+      9,
+      2,
+      0,
+      2
+    ],
+    [
+      10,
+      2,
+      2,
+      4
+    ],
+    [
+      19,
+      2,
+      2,
+      4
+    ],
+    [
+      20,
+      2,
+      6,
+      8
+    ],
+    [
+      25,
+      2,
+      6,
+      8
+    ],
+    [
+      5,
+      3,
+      0,
+      3
+    ],
+    [
+      9,
+      3,
+      0,
+      3
+    ],
+    [
+      10,
+      6,
+      1,
+      7
+    ],
+    [
+      19,
+      6,
+      1,
+      7
+    ],
+    [
+      20,
+      12,
+      7,
+      19
+    ],
+    [
+      25,
+      12,
+      8,
+      20
+    ]
+  ],
+  "negative_controls": [
+    "ignore-root-eligibility",
+    "omit-nonroot-demand",
+    "assume-source-monotonicity",
+    "rank-mass-is-call-count",
+    "omit-paid-completion",
+    "omit-source-complements"
+  ],
+  "nonmonotonicity": [
+    {
+      "by_depth": [
+        243240704
+      ],
+      "first_nonroot": {
+        "child_column": 1,
+        "count": 1254400,
+        "depth": 1,
+        "paid_rank": 20,
+        "parent_multiplier": 1,
+        "source_rank": 2900,
+        "target_rank": 145
+      },
+      "height": 1,
+      "n": 3624,
+      "nonroot": 243240704,
+      "root": 85150976,
+      "source_rank_types": 104,
+      "source_spectrum_sha256": "4577b010b53d167d9fe4a07f1559070577e4a58e24495c549646977ee8be134b",
+      "total": 328391680
+    },
+    {
+      "by_depth": [
+        208492032
+      ],
+      "first_nonroot": {
+        "child_column": 1,
+        "count": 1254400,
+        "depth": 1,
+        "paid_rank": 20,
+        "parent_multiplier": 1,
+        "source_rank": 2900,
+        "target_rank": 145
+      },
+      "height": 1,
+      "n": 3625,
+      "nonroot": 208492032,
+      "root": 90046720,
+      "source_rank_types": 101,
+      "source_spectrum_sha256": "8c9fc8827981b19c6ed97e7b93d00b9d52078e571a4af1162c37d932979263c7",
+      "total": 298538752
+    }
+  ],
+  "schema_version": 1,
+  "selected_kappa_unchanged": "60403/20000000",
+  "selected_v1": [
+    {
+      "by_depth": [],
+      "first_nonroot": null,
+      "height": 0,
+      "n": 3044,
+      "nonroot": 0,
+      "root": 10928,
+      "source_rank_types": 9,
+      "source_spectrum_sha256": "88c6975b420fd81040e173ae76da7de44b91200d0e806da3b7ebf8bc4d03e64c",
+      "total": 10928
+    },
+    {
+      "by_depth": [
+        243240704
+      ],
+      "first_nonroot": {
+        "child_column": 1,
+        "count": 1254400,
+        "depth": 1,
+        "paid_rank": 20,
+        "parent_multiplier": 1,
+        "source_rank": 2900,
+        "target_rank": 145
+      },
+      "height": 1,
+      "n": 3045,
+      "nonroot": 243240704,
+      "root": 85150976,
+      "source_rank_types": 104,
+      "source_spectrum_sha256": "4577b010b53d167d9fe4a07f1559070577e4a58e24495c549646977ee8be134b",
+      "total": 328391680
+    },
+    {
+      "by_depth": [
+        243240704
+      ],
+      "first_nonroot": {
+        "child_column": 1,
+        "count": 1254400,
+        "depth": 1,
+        "paid_rank": 20,
+        "parent_multiplier": 1,
+        "source_rank": 2900,
+        "target_rank": 145
+      },
+      "height": 1,
+      "n": 3046,
+      "nonroot": 243240704,
+      "root": 85150976,
+      "source_rank_types": 104,
+      "source_spectrum_sha256": "4577b010b53d167d9fe4a07f1559070577e4a58e24495c549646977ee8be134b",
+      "total": 328391680
+    },
+    {
+      "by_depth": [
+        0
+      ],
+      "first_nonroot": null,
+      "height": 1,
+      "n": 63944,
+      "nonroot": 0,
+      "root": 119421184,
+      "source_rank_types": 45,
+      "source_spectrum_sha256": "e110c46d629db6956bdc1f8c157b96d03f9f0fcf105a806be2fce8c80f88ae22",
+      "total": 119421184
+    },
+    {
+      "by_depth": [
+        4115879484416,
+        3105871052032
+      ],
+      "first_nonroot": {
+        "child_column": 21,
+        "count": 9774284800,
+        "depth": 1,
+        "paid_rank": 20,
+        "parent_multiplier": 1,
+        "source_rank": 60900,
+        "target_rank": 145
+      },
+      "height": 2,
+      "n": 63945,
+      "nonroot": 7221750536448,
+      "root": 663496404992,
+      "source_rank_types": 688,
+      "source_spectrum_sha256": "561bc928587de833ba5c1dc5b975b1b13447c16df84696ed302ee3b8ce9ca1cf",
+      "total": 7885246941440
+    },
+    {
+      "by_depth": [
+        4115879484416,
+        3105871052032
+      ],
+      "first_nonroot": {
+        "child_column": 21,
+        "count": 9774284800,
+        "depth": 1,
+        "paid_rank": 20,
+        "parent_multiplier": 1,
+        "source_rank": 60900,
+        "target_rank": 145
+      },
+      "height": 2,
+      "n": 63946,
+      "nonroot": 7221750536448,
+      "root": 663496404992,
+      "source_rank_types": 688,
+      "source_spectrum_sha256": "561bc928587de833ba5c1dc5b975b1b13447c16df84696ed302ee3b8ce9ca1cf",
+      "total": 7885246941440
+    }
+  ]
+}
diff --git a/research/selected-truncated-source-envelope/SOURCES.json b/research/selected-truncated-source-envelope/SOURCES.json
new file mode 100644
index 0000000000..fd4812ed2d
--- /dev/null
+++ b/research/selected-truncated-source-envelope/SOURCES.json
@@ -0,0 +1,53 @@
+{
+  "schema_version": 1,
+  "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4",
+  "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/selected-truncated-source-envelope/vendor/flow.py",
+      "usage": "input",
+      "pin": "head:4c0a359d88f22f05189d51f48387750b801a45d4:research/direct-mixed-flow/flow.py",
+      "git_blob": "07175cd6e1f2c2367c2e78eca7f163fef18d301d",
+      "sha256": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a"
+    },
+    {
+      "path": "research/selected-truncated-source-envelope/vendor/selected.json",
+      "usage": "input",
+      "pin": "head:b9a13c1673e0e9697de410de16e8bbf3207a7363:research/joint-helper-lattice/RESULT.json",
+      "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596",
+      "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21"
+    },
+    {
+      "path": "research/selected-truncated-source-envelope/vendor/selected-PROOF.md",
+      "usage": "input",
+      "pin": "head:b9a13c1673e0e9697de410de16e8bbf3207a7363:research/joint-helper-lattice/PROOF.md",
+      "git_blob": "e41106031da41fade7a7419c17a32c1bd9aa103b",
+      "sha256": "43ef4251cc300f1b18cbe8cdb060f96f95748e6797d2478b4c04b79a8373ef91"
+    },
+    {
+      "path": "research/selected-truncated-source-envelope/vendor/predecessor.md",
+      "usage": "input",
+      "pin": "head:6e1e7d47ed7fd7f3f7197cad7c19f8237c062b06:research/selected-complex-width-envelope/README.md",
+      "git_blob": "b59d4127cc00ab8f04d76175c254d0fa4e8b0bea",
+      "sha256": "421842e929b13a2adf3b3071257e36d42c0b1e7001d87be8d8df88a9a4ef7e6b"
+    },
+    {
+      "path": "research/selected-truncated-source-envelope/vendor/flow-README.md",
+      "usage": "input",
+      "pin": "head:4c0a359d88f22f05189d51f48387750b801a45d4:research/direct-mixed-flow/README.md",
+      "git_blob": "3be00f754b9ffa23e64b3eafe7706e3ac139993a",
+      "sha256": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8"
+    }
+  ]
+}
diff --git a/research/selected-truncated-source-envelope/TASK.json b/research/selected-truncated-source-envelope/TASK.json
new file mode 100644
index 0000000000..27c52600eb
--- /dev/null
+++ b/research/selected-truncated-source-envelope/TASK.json
@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "selected-stock-envelope",
+  "priority_revision": 7,
+  "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4",
+  "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",
+      "research/stock-margin-chain/README.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 #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.",
+      "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 actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.",
+    "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.",
+      "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality."
+    ],
+    "overlap_terms": [
+      "selected stock",
+      "stock envelope",
+      "bootstrap cutoff",
+      "1956",
+      "1965",
+      "1990",
+      "2972",
+      "stock-margin-chain",
+      "actual_stock_coefficient"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.",
+        "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation",
+        "remaining": "Derive one actual reserve/depth coefficient from the selected producer.",
+        "status": "reviewed",
+        "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Uniform eligibility-sensitive root and missing-demand source census for the unchanged selected4470 rule and PR4436 nested widths.",
+  "scope_change_reason": "Answer PR5026 open handoff with a first-moment truncation bound, keeping batching and every completion/split unchanged.",
+  "bottleneck_link": "Bounds the accumulated mathematical row-depth coefficient K, not physical supplier admission or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at a strictly sharper uniform accumulated coefficient or a precise failed implication; no product expansion or giant N.",
+  "outcome": "completed",
+  "evidence": "Uniform root/nonroot first-moment proof; exact K/N<3.070; six selected v=1 boundary fixtures; twelve literal comparisons and six semantic rejection controls.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance (GPT-6 Astra).",
+  "open_questions": [
+    {
+      "question": "Can a fractional moment retaining nonroot eligibility narrow the inherited 2.943 lower and 3.070 upper bracket?",
+      "why_it_matters": "Improves the same accumulated mathematical width coefficient.",
+      "first_step": "Derive a uniform fractional-moment inequality with all completion and absence terms.",
+      "blocked_by": "A sharper completed-product moment bound; no product materialization."
+    },
+    {
+      "question": "Does the mathematical nested width fit the physical stock and routing interface?",
+      "why_it_matters": "Count bounds are not physical supplier admission.",
+      "first_step": "Bind one named source invocation to a complete owner/route tariff.",
+      "blocked_by": "Inherited physical implementation obligations; outside this task."
+    }
+  ],
+  "first_fixture": "Actual selected raw invoice reduced to v=1, n=145*21^g plus -1,0,1 for g=1,2; tiny literal flows separately.",
+  "bounds": {
+    "maximum_fixture_height": 2,
+    "selected_product_materialized": false,
+    "giant_N_materialized": false
+  },
+  "inherited_obligations": [
+    "Native all-column correctness",
+    "Whole-job adapters",
+    "Owned restoration",
+    "Precision/tape and analytic recovery",
+    "No selected frontier change"
+  ]
+}
diff --git a/research/selected-truncated-source-envelope/VENDOR.json b/research/selected-truncated-source-envelope/VENDOR.json
new file mode 100644
index 0000000000..cba2af1743
--- /dev/null
+++ b/research/selected-truncated-source-envelope/VENDOR.json
@@ -0,0 +1,37 @@
+[
+  {
+    "head": "4c0a359d88f22f05189d51f48387750b801a45d4",
+    "original_path": "research/direct-mixed-flow/flow.py",
+    "retained_path": "vendor/flow.py",
+    "sha256": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a",
+    "license": "Apache-2.0; original attribution retained"
+  },
+  {
+    "head": "b9a13c1673e0e9697de410de16e8bbf3207a7363",
+    "original_path": "research/joint-helper-lattice/RESULT.json",
+    "retained_path": "vendor/selected.json",
+    "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21",
+    "license": "Apache-2.0; original attribution retained"
+  },
+  {
+    "head": "b9a13c1673e0e9697de410de16e8bbf3207a7363",
+    "original_path": "research/joint-helper-lattice/PROOF.md",
+    "retained_path": "vendor/selected-PROOF.md",
+    "sha256": "43ef4251cc300f1b18cbe8cdb060f96f95748e6797d2478b4c04b79a8373ef91",
+    "license": "Apache-2.0; original attribution retained"
+  },
+  {
+    "head": "6e1e7d47ed7fd7f3f7197cad7c19f8237c062b06",
+    "original_path": "research/selected-complex-width-envelope/README.md",
+    "retained_path": "vendor/predecessor.md",
+    "sha256": "421842e929b13a2adf3b3071257e36d42c0b1e7001d87be8d8df88a9a4ef7e6b",
+    "license": "Apache-2.0; original attribution retained"
+  },
+  {
+    "head": "4c0a359d88f22f05189d51f48387750b801a45d4",
+    "original_path": "research/direct-mixed-flow/README.md",
+    "retained_path": "vendor/flow-README.md",
+    "sha256": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8",
+    "license": "Apache-2.0; original attribution retained"
+  }
+]
diff --git a/research/selected-truncated-source-envelope/VERIFY.json b/research/selected-truncated-source-envelope/VERIFY.json
new file mode 100644
index 0000000000..f7f8880237
--- /dev/null
+++ b/research/selected-truncated-source-envelope/VERIFY.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/selected-truncated-source-envelope/vendor/flow.py",
+    "research/selected-truncated-source-envelope/vendor/selected.json",
+    "research/selected-truncated-source-envelope/vendor/selected-PROOF.md",
+    "research/selected-truncated-source-envelope/vendor/predecessor.md",
+    "research/selected-truncated-source-envelope/vendor/flow-README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Exact source census, first-moment envelope, selected coefficient, and semantic rejection controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Exact source census, first-moment envelope, selected coefficient, and semantic rejection controls"
+    }
+  ]
+}
diff --git a/research/selected-truncated-source-envelope/vendor/flow-README.md b/research/selected-truncated-source-envelope/vendor/flow-README.md
new file mode 100644
index 0000000000..3be00f754b
--- /dev/null
+++ b/research/selected-truncated-source-envelope/vendor/flow-README.md
@@ -0,0 +1,496 @@
+# Direct mixed flow and explicit compiler size: a partial research checkpoint
+
+**Publication authorized by the user on October 21, 2026.** This is a partial
+compiler/resource checkpoint; the direct exponent gate remains open.
+
+The target is a structural successor to
+[PR4433](https://github.com/CrocSwap/integer-mult-bounds/pull/4433): remove the
+tensor/padding step needed by overlapping ranks and control the complete
+finite compiler's size. The user requested a significance target twice the
+previous contribution. That is an ambitious scope target, not a numerical
+measurement or a claim that it has been achieved.
+
+Two results are established under the source native-word hypotheses:
+
+1. A **finite chronological integer flow** works when paid ranks overlap
+   target ranks, provided `max paid < ambient`. It retains and pays every
+   unmatched job as an exit. All recursive ranks decrease. This gives a
+   finite uniform compiler, **without a proved near-root saving**.
+2. Choosing **nested divisible widths** gives `B_N <= exp(O(N log N))`.
+   Exact rank-one accounting also bounds raw instances, owned centers,
+   routing slots and the source finite-constant envelopes. This batching
+   choice preserves the normalized leaf cost and therefore applies to the
+   already supported PR4433 supplier.
+
+The main exponent target remains open. Exact compilation at rank 1,000 on
+the raw p7 profile fails the desired saving. That finite failure is not an
+asymptotic obstruction, and it does not invalidate PR4433's separated recipe.
+No new κ, selected frontier, native admission or physical runtime is claimed.
+
+## 1. Source boundary and decision
+
+The starting point is Jacob Alan Sussman's multinomial lockstep construction,
+retained by PR4359. Its separated proof requires `r_max < k_min` so every
+parent output is consumed. PR4416 and PR4433 instead repair the raw p7
+overlap by chronological products, paid completion and splitting.
+
+Retain the four native hypotheses of
+[FINITE-PRECOMPILATION.md](vendor/FINITE-PRECOMPILATION.md): a correct
+all-column arbitrary-input word, disjoint splitting with complete spectators,
+permitted and priced whole-job adapters, and finite-program closure with
+owned initialization/erasure. Equal rank alone does not supply an adapter.
+Changed finite combinatorics do not independently admit those hypotheses.
+
+**Continue, with two separate gates.** The finite-flow gate is now proved and
+checked. The exponent gate requires a new uniform estimate on the complete
+complement-plus-exit recurrence. Do not expand a search solely because a
+moment root is favorable. The size theorem is useful independently, since
+the predecessor leaves productive width and owned-instance counts implicit.
+
+| Obligation | Evidence / remaining work |
+| --- | --- |
+| Integer matching with overlapping ranks | Proved below; literal and merged replays agree |
+| Chronological return and strictly smaller exits | Proved under `r_max < m`; no cross-round matching |
+| Source complements and full uniform output | Source integer-batch induction, with nested divisible widths |
+| Direct near-root saving | **Open**; rank 1,000 fails; no global conclusion |
+| Productive width, rank-one leaves, raw instances, owned centers | Explicit bounds below, with exact finite controls |
+| Routing slots, encoded records and source finite-constant envelopes | Counted below in the stated grammar; physical implementations retain their own tariffs |
+| Native all-column, physical, analytic, precision and recovery premises | Inherited; no full replay or new admission |
+
+## 2. Partially matched integer lockstep flow
+
+Let positive integer target multiplicities be W_k, chronological paid rounds
+have ranks r_j, and let
+
+```
+2 <= k_min <= m=max(k),   1 <= r_max < m.
+```
+
+The paid word may have `r_max >= k_min`. At a fixed integer top rank n>=m,
+put
+
+```
+c(a) = product_k k^a_k,
+u(a) = multinomial(|a|;a) product_k W_k^a_k,
+R(rho) = {a : m*rho*c(a) <= n},
+G = floor(log_(k_min)(floor(n/m))).
+```
+
+For every paid-round path s of length d<=G with multiplier rho_s, instantiate
+u(a) units at column rho_s*c(a), for every point a in R(rho_s) of degree
+G−d. This is the source class construction. For a parent class with
+multiplier rho, its rank-r round supplies u(b) jobs at point b when b is
+present. The child demand at that point is
+
+```
+D(b) = sum over eligible (b−e_k) of W_k*u(b−e_k).
+```
+
+The complete Pascal sum is u(b). Therefore:
+
+- If the parent point b exists, `0 <= D(b) <= u(b)`. Route D(b) of the
+  **whole** issued jobs to the child. Complete the remaining u(b)−D(b)
+  jobs as paid exits, at their actual rank `e=r*rho*c(b)`.
+- If the parent point is absent, supply the child demand with new distinct
+  top input arrays. These are source jobs, not copies of issued data.
+- At depth G, every point has degree zero; all paid jobs are exits.
+
+No fractional jobs, cloned productive inputs or uncharged discarded requests
+are introduced. Within each point, choose a fixed enumeration of parent
+jobs and target slots and match their first D(b) elements. The rest have
+explicit endpoints and remain on their actual owners.
+
+### Sources and exits
+
+At the root, every demanded point has degree G+1, so it is outside R(1).
+Its rank s is in `(n/m,n]`. A non-root source has no parent point, hence
+`m*rho_parent*c(b)>n`; its rank is `r*rho_parent*c(b)>r*n/m>=n/m`.
+Its eligible child target ensures s<=n. Thus every source is a positive
+job in `(n/m,n]`.
+
+Every exit belongs to an actual parent unit, so
+
+```
+e <= r_max*n/m < n.
+```
+
+This holds for the new premature exits as well as leaf exits. A premature
+exit has at least one omitted Pascal term, with
+`m*r*rho*c(b)/k > n`; consequently `e > k_min*n/m`. These are large exits
+near the upper boundary. They cannot be assigned the old bound
+`r_max*(n/m)^theta` with theta<1. That lost estimate is the exponent issue.
+
+### Chronology and arbitrary inputs
+
+Run all scalar steps of a class in their specified order. At paid position
+j, issue that position for every unit, partition its whole issued jobs into
+matched and unmatched slots, finish all unmatched exits and the entire child
+class, restore adapters, and only then resume position j+1. The child takes
+incoming jobs from this one parent round plus its new top sources. It never
+waits for a later round of a suspended parent. The finite class depth is G;
+all complement and exit calls have rank below n, so their uniform programs
+are already available by strong induction.
+
+Distinct slots in one class have distinct physical fields. Routing fewer
+parent slots than the original full-Pascal construction preserves this
+property. Arbitrary-input native correctness permits correlated values,
+including current owned-center contents; it does not permit field aliasing
+or extra productive credit. Each unit has its own owned identities and
+retains them until its word clears them. These requirements are unchanged.
+
+### Exact potential and count identities
+
+Let S_s and E_e be integer source and exit inventories, U the unit count,
+and Qcol the sum of the units' positive integer column multiplicities.
+Cancellation of matched jobs gives, exactly at rank one,
+
+```
+sum_s S_s*s − sum_e E_e*e = Delta * Qcol,
+Delta = sum_k W_k*k − sum_j r_j.
+```
+
+At any real exponent t, the corresponding identity is
+
+```
+sum_s S_s*s^t − sum_e E_e*e^t
+    = (T_t−P_t) * sum_units column^t.
+```
+
+Thus a favorable raw t-moment survives as a superpotential. It does **not**
+by itself pay the source complements. Writing W=sum W_k and P=number of
+paid rounds, complete untruncated layer counts give
+
+```
+U <= sum_(d=0..G) P^d W^(G−d) <= (W+P+1)^(G+1),
+S := sum_s S_s <= W*U,
+sum_e E_e <= P*U.
+```
+
+The source package's separated case is unchanged: no premature exits occur.
+The verifier compares it with the byte-identical predecessor literal replay.
+
+## 3. Nested divisible widths and complete count bounds
+
+Use the ordinary base B_n=1, P_n=n below m, with B_0=1 and P_0=0. For n>=m
+choose the replication factor and productive width
+
+```
+a_n = B_(n−1),    B_n = a_n*S_n.
+```
+
+Every earlier width B_e divides B_(n−1), by induction. Therefore every
+source-complement batch and exit batch is an integer number of smaller
+uniform programs. This is a concrete choice within the source compiler's
+existing denominator-clearing freedom; no optimum is claimed. Its previous
+option to use an LCM is retained as predecessor context.
+
+As in the source compiler, each of the a_n*S_n original arrays first gets
+its disjoint complementary job, then its one source job through the flow.
+All exits are completed by smaller uniform programs. The result is a full
+rank-n transform on every original array. Owned storage is excluded from B_n.
+
+The normalized leaf count satisfies the **same exact recurrence** for any
+valid replication choice:
+
+```
+L(n) = (1/S_n) * [sum_s S_s L(n−s) + sum_e E_e L(e)].
+```
+
+Changing the replication factors changes width and total counts equally.
+It does not spend supplier saving or alter any outer parameter.
+
+For a fixed final N and h=G(N), all n<=N satisfy
+
+```
+S_n <= C_N := W*(W+P+1)^(h+1),
+B_N = product_(n=m..N) S_n <= C_N^N.
+```
+
+Since h=O(log N), **log B_N=O(N log N)** for a fixed mixed rule. Repeatedly
+multiplying all previous widths is unnecessary. This bounds one explicit
+realization; the original compiler did not require that inefficient choice.
+
+If Delta>0, telescope rank-one mass over the fully expanded uniform program:
+
+```
+B_N*N − P_N = Delta * Qcol_N,
+U_N <= Qcol_N <= B_N*N/Delta.
+```
+
+All raw columns are positive integers, which gives the middle inequality.
+Thus paid leaves and raw instances have the same `exp(O(N log N))` bound.
+With one owned center per raw unit, the center count is at most U_N. A rule
+with O_local distinct owned banks per invocation instead gets O_local*U_N.
+Extra router scratch must be counted separately.
+
+### Routing and word description
+
+Count one routing slot for every source, every exit, every unit target slot
+and every unit paid position. At one flow its count is at most
+`2*(W+P)*U`. The same bound telescopes over all recursive calls, because
+each call contributes its own local unit instances. Exact compilation checks
+this identity alongside widths and leaves.
+
+In the macro grammar that records a whole-job adapter, inverse adapter or
+whole-field move as one record, a slot can be handled with at most sixteen
+records: up to two whole-job conjugations and their inverses, park/load/
+return/reorder moves, and explicit scratch initialization and erasure.
+Allocate separate owned scratch for those moves when needed; no zero-cost
+routing or free copying is assumed. Let A bound the fixed unit's complete
+nonrecursive record count, owned operations and scalar coefficient heights.
+The final weighted record allowance satisfies the conservative bound
+
+```
+R_bar <= A*U_N + 32*(W+P)*U_N + P_N
+      <= (A+32*(W+P)+1)*B_N*N,  for Delta>=1.
+```
+
+R_bar bounds both the macro count and the sum of scalar-height and native
+record allowances. Every owned bank has an explicit initialization record,
+so total allocated owned banks can also be bounded by R_bar; the sharper
+raw-center bound remains separate. This is a **description/record bound**,
+not a new tariff for executing a
+general matrix or permutation. A Gaussian monomial adapter's dense binary
+address matrix and quadratic phase have O(N^2) descriptor bits. Explicit role indices add O(log B_N)
+bits. Thus an encoding of this finite word still has
+`exp(O(N log N))` bits for a fixed unit and its finite coefficient alphabet.
+If physical expansion of one adapter needs F(N) native records, multiply
+the routing term by its actual F(N). That physical implementation, coefficient
+heights and tape costs remain separately priced native obligations. They
+are not set to zero by the macro bound.
+
+## 4. Applying the size result to PR4433
+
+The new nested widths may be used in the separated compiler of PR4433.
+Its normalized L(n), ambient N, uniform saving and outer ledger remain
+unchanged. Therefore this application does not need the still-open direct
+exponent lemma.
+
+With `v=150`, `H=349300000000`, `N=2^H`, the completed mixed rule has
+
+```
+W = 7688^150 < 2^1950,
+P <= 131115^150 + 7688^150*15^150 < 2^2701,
+W+P+1 < 2^2702.
+```
+
+The bound on P counts every original and completion call by its positive
+rank mass; splitting preserves that mass. Since k_min>=2, h<=H. Set
+
+```
+D = 1950 + 2702*(H+1) = 943808600004652.
+```
+
+There is consequently a realization of the same proposed conditional
+κ=0.00268647 supplier satisfying
+
+```
+B_N < 2^(D * 2^H),
+P_N < B_N * 2^H.
+```
+
+More finely, after expanding every product, padding, split and compiler call
+back to the raw p7 word, that word has surplus 608. Product/completion/split
+boundaries cancel, so
+
+```
+B_N*N − P_N = 608 * sum_raw_p7_instances column,
+U_raw <= (B_N*N − P_N)/608.
+```
+
+This is also an explicit bound on raw p7 center banks under the safe
+one-center-per-instance allocation. These are large upper bounds, not
+emitted words, smallest widths or practical precision estimates. They replace
+one implicit part of the source finite-constant prescription. The native
+adapter bodies, analytic transfer and physical costs retain their original
+conditions; a closed bound for the source's finite-constant prescription is
+given next, without a new physical runtime or exact-recovery threshold.
+
+### A closed envelope for the source finite constants
+
+The exported THREE-base native word has exactly 22,633 records in each
+orientation. Source-bound counting retains all 15 copies, the literal p7
+controller, scalar allowance 2,490,856, every productive/paid/contact/helper/
+idle slot, and all routing and owned operations. A raw macro allowance is
+
+```
+A_raw = 15*8*(decompressed native JSON bytes)
+      + 8*(literal controller JSON bytes)
+      + 32*(2490856 + all declared slots + 15*22633) < 2^40.
+```
+
+The payload-bit terms overcount the coefficient literals and full local
+descriptors, including both orientations. The 32-per-slot term overcounts
+whole-job normalizers and inverses, field movements, initialization and
+erasure. It is a bound on the declared source word in this grammar, not
+independent verification of its functional correctness or physical tariffs.
+
+For the chronological v-fold product, its number of raw p7 invocations is
+
+```
+U_v = sum_(i=0..v−1) 7688^(v−1−i)*55998^i < 2^2392.
+```
+
+At every product level retain the whole-job matching wrappers. A conservative
+product allowance is
+
+```
+A_product <= (2^40 + 32*v*(7688+55998+1))*U_v + 32*v*55998^v.
+```
+
+Add 32 records for every final paid call, completion role and original paid
+position. Counting paid calls by their rank mass gives
+
+```
+A_completed <= A_product
+    + 32*(131115^v + 7688^v*15^v + 7688^v + 55998^v).
+```
+
+A dense local binary map/quadratic phase and role index fit in
+`64*(121^v)^2` bits per such record. The verifier checks the integer bound
+`A_completed * 64*(121^v)^2 < 2^5000`. Thus **A=2^5000** is a valid weighted
+record/description allowance for this fixed completed unit. It includes all
+source coefficients and owned operations, with a large deliberate overcount.
+No instruction list of the completed product is emitted.
+
+Since `A+32*(W+P)+1 < 2^5001`, use the envelope
+
+```
+R_bar < 2^(D*2^H + H + 5001).
+```
+
+Apply the existing source finite-constant prescription to the **newly expanded
+word**. With Z=B_N+owned banks, G its scalar coefficient envelope, and P_N
+its rank-one leaves, we have `Z<=2*R_bar`, `G<=8*R_bar`, `P_N<=R_bar` and
+`N<=R_bar`. Therefore
+
+```
+E = 64*(Z+N+P_N+G+1)^3
+  < 2^(3*D*2^H + 3*H + 15021),
+B_constant = P_N+E,
+C0 = 32*N*B_constant^2
+   < 2^(6*D*2^H + 7*H + 30049)
+   < 2^(8*D*2^H).
+```
+
+The last comparison uses `2^H>=H+1` and an exact polynomial integer check
+on D and H. These are explicit, very loose upper bounds for the inherited
+semantic precision/stock constants, conditional on that source prescription
+and its admitted native record implementations. The exact numerical outer
+input threshold, prime exclusions and physical tape costs remain separate.
+
+## 5. Exact finite checks and the open exponent gate
+
+The verifier uses no floating-point acceptance tests. It checks:
+
+- Nine literal/merged flows at ranks 20, 40 and 80: a separated control,
+  strict overlap `{2:1,5:1} <- {1:2,4:1}`, and Sussman's open equality
+  example `{2:4,3:1} <- {1:6,2:2}`. Every whole input and exit agrees.
+- The separated control agrees with the unchanged Sussman literal replay.
+- Complete nested-width compilations through rank 100 on both overlap
+  examples, checking every recursive batch, routing count and rank identity.
+- Raw p7 through rank 1,000: **880 exact nonbase compilations**. B_1000 has
+  17,504 bits; the saved receipt binds all large computed integers by their
+  unsigned big-endian hashes, avoiding enormous decimal dumps.
+- Removing premature exits violates mass conservation. Removing batch
+  replication fails integer divisibility. Allowing a paid rank equal to
+  the ambient rank is rejected because strict rank descent is unavailable.
+
+For raw p7 at rank 1,000, exact arithmetic gives
+
+```
+L(1000) > 990 > 1000^(1−0.00268647).
+```
+
+The second comparison is elementary and exact: `ln(2)>2/3` from its first
+atanh term and `1000>2^9` give `ln(1000)>6`. Then
+`1000^κ > 1+6κ > 100/99`. No log approximation is used in this rejection.
+This checks one finite failure and keeps it distinct from the infinite-rank
+question.
+
+The missing lemma is a uniform bound on the **whole** recurrence. For some
+fixed p and sufficiently large n, one would need, for example,
+
+```
+sum_e E_e e^t (1+log2(e))^p
+ + sum_s S_s (n−s)^t (1+log2(n−s))^p
+ <= S_n n^t (1+log2(n))^p,
+```
+
+with zero-rank terms defined separately and a correctly funded base range.
+The premature exits have rank proportional to n. Their logarithmic factors
+cannot use the old fixed theta<1 power contraction. A raw moment advantage
+alone does not prove this inequality.
+
+Exploratory `approximate_leaves` in flow.py evaluates the recurrence in
+floating point and is deliberately excluded from verification. A bounded
+run through 20,000 ranks found saving about 0.000827 for the default height;
+varying the height did not approach 0.00268647 there. This is local search
+evidence, not a lower bound or a reason to enlarge the same scan. A better
+boundary estimate or a changed flow is the next research obligation.
+
+## 6. Reproduction and provenance
+
+Python 3.12, standard library only:
+
+```sh
+python3.12 -B research/direct-mixed-flow/verify.py
+python3.12 -B scripts/research_package.py --package research/direct-mixed-flow --check-only
+python3.12 -B scripts/research_package.py --package research/direct-mixed-flow
+```
+
+Use `verify.py --out /absolute/new/result.json` for a fresh receipt.
+[RESULT.json](RESULT.json) contains exact flows, integer compilation hashes,
+symbolic size bounds and negative controls. `flow.py` is the new algorithm;
+the verifier independently compares its merged and literal traversal outputs.
+Those are two internal implementations, not an independent mathematical review.
+
+Canonical base is `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority revision
+7. SOURCES.json pins orientation metadata. VENDOR.json separately binds eleven
+unchanged exports by commit, full path, Git blob and SHA256. Their bytes and
+notices are preserved; direct replay needs no foreign Git objects. The source
+theorem and earlier finite compiler remain attributed hypotheses, not new work.
+
+Local validation used Python 3.12.8 on macOS arm64. The registered replay,
+metadata/pin check and committed-byte preflight passed. A separate Git-free
+copy passed with `python3.12 -I -O -B verify.py`; changed-native-source and
+changed-receipt controls both rejected. Replay uses exact integer arithmetic
+and source hashes, with no network or foreign Git objects. The repository is
+shallow, so a full source-history preflight was not attempted. No Lean, Docker,
+full native/all-column admission, physical adapter expansion or historical
+suite was run. Independent mathematical acceptance remains open.
+
+The overlap refresh at 18:48 UTC covered 538 open PR bodies and 3,280
+discussion/comment records, with complete reported pagination. Specific
+searches for direct overlapping-rank compilers, Pascal matching and nested
+widths found no matching public item in that scope; this is not a novelty
+certificate. Existing PR4433 supplies the fixed-rank application, and the
+source theorem explicitly leaves the unseparated exponent open. No Discussion
+claim or PR has been posted for this partial checkpoint.
+
+## Open next questions
+
+1. **Close or refute the direct exponent gate for this capped flow.** Start
+   with a proved bound on premature-exit potential relative to the actual
+   complement capacity. This decides whether the flow can replace the
+   tensor/padding layer. A larger rank scan is not a uniform proof.
+2. **Independently admit the physical expansions and precision prescription.**
+   Audit the conservative A allowance against the actual native caller and
+   bind every adapter's physical implementation, row movements and recovery
+   exclusions. The encoded constants above use the inherited semantics;
+   description size is not a physical execution tariff.
+3. **Tighten the constructive width.** The nested product is an explicit
+   upper bound, not an optimized LCM. A useful next step would control prime
+   valuations of the actual source counts; another arbitrary batching choice
+   would not by itself establish a smaller physical supplier.
+
+Prepared by zxv with substantial OpenAI Codex assistance in research, code
+and writing. No subagents or independent human mathematical review were
+used. New material is Apache-2.0. The integer lockstep/Pascal construction
+and original open unseparated question are Jacob Alan Sussman's work, retained
+at upstream `wht-power-saving-lean` commit
+`563b4e6e913625637f36ba7869bf5fcd0dd4975a`; its LICENSE and NOTICE are included.
+PR4359 supplies the native finite-precompilation bridge and p7 predecessor
+lineage. PR4416's p7 product/padding is @1337isnot1337's work. PR4433 supplies
+the unchanged sufficient rank. Their original contributor credit remains
+in the authenticated exports.
diff --git a/research/selected-truncated-source-envelope/vendor/flow.py b/research/selected-truncated-source-envelope/vendor/flow.py
new file mode 100644
index 0000000000..07175cd6e1
--- /dev/null
+++ b/research/selected-truncated-source-envelope/vendor/flow.py
@@ -0,0 +1,198 @@
+#!/usr/bin/env python3
+"""Capped whole-integer lockstep flow, retaining unmatched jobs as paid exits.
+
+Generalizes Jacob Alan Sussman's separated multinomial construction.
+zxv with substantial OpenAI Codex assistance. Apache-2.0.
+This is a finite flow, not a theorem that it attains the mixed-root saving.
+"""
+from collections import Counter
+from functools import lru_cache
+from math import comb, prod
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+class Flow:
+    def __init__(self, targets, paid, n, extra_height=0, height_base=None):
+        self.T, self.P, self.n = dict(targets), dict(paid), n
+        self.K = tuple(sorted(targets))
+        self.m, self.kmin, self.rmax = max(targets), min(targets), max(paid)
+        need(2 <= self.kmin <= self.m and self.rmax < self.m <= n,
+             'finite direct-flow rank contract')
+        need(all(isinstance(v, int) and v > 0 for x in (targets, paid)
+                 for v in x.values()), 'positive integer inventories')
+        self.cap = n//self.m
+        self.height_base = self.kmin if height_base is None else height_base
+        need(isinstance(self.height_base, int) and self.height_base >= 2, 'integer height base')
+        self.G, least = 0, 1
+        while least*self.height_base <= self.cap:
+            self.G += 1
+            least *= self.height_base
+        need(isinstance(extra_height, int) and extra_height >= 0, 'nonnegative extra height')
+        self.G += extra_height
+        self.zero = (0,)*len(self.K)
+
+    @lru_cache(None)
+    def column(self, a):
+        return prod(k**v for k, v in zip(self.K, a))
+
+    @lru_cache(None)
+    def points(self, height, cap):
+        """(a, u(a)) at fixed degree; exact multinomial integer weights."""
+        result = {}
+
+        def visit(i, remaining, c, weight, a):
+            if i == len(self.K):
+                if remaining == 0 and c <= cap:
+                    result[a] = weight
+                return
+            k, w = self.K[i], self.T[self.K[i]]
+            for count in range(remaining+1):
+                new_c = c*k**count
+                if new_c > cap:
+                    break
+                visit(i+1, remaining-count, new_c,
+                      weight*comb(remaining, count)*w**count, a+(count,))
+
+        if cap >= 1:
+            visit(0, height, 1, 1, ())
+        return result
+
+    @lru_cache(None)
+    def units(self, depth, rho):
+        return self.points(self.G-depth, self.cap//rho)
+
+    @lru_cache(None)
+    def demand(self, depth, rho):
+        result = Counter()
+        for a, count in self.units(depth, rho).items():
+            for i, k in enumerate(self.K):
+                b = list(a)
+                b[i] += 1
+                result[tuple(b)] += count*self.T[k]
+        return result
+
+    def merged(self):
+        sources, exits, boundary = Counter(), Counter(), Counter()
+        units = columns = 0
+        matched = 0
+        path_counts = Counter({1:1})
+        for b, count in self.demand(0, 1).items():
+            sources[self.column(b)] += count
+        for depth in range(self.G+1):
+            following = Counter()
+            for rho, paths in path_counts.items():
+                batch = self.units(depth, rho)
+                units += paths*sum(batch.values())
+                columns += paths*sum(count*rho*self.column(a) for a, count in batch.items())
+                for rank, repetitions in self.P.items():
+                    new_rho = rho*rank
+                    copies = paths*repetitions
+                    if depth == self.G:
+                        need(set(batch) <= {self.zero}, 'leaf degree zero')
+                        exits[new_rho] += copies*batch.get(self.zero, 0)
+                        continue
+                    child = self.demand(depth+1, new_rho)
+                    if new_rho <= self.cap:
+                        following[new_rho] += copies
+                    for b in set(batch) | set(child):
+                        supply, demand = batch.get(b, 0), child.get(b, 0)
+                        e = new_rho*self.column(b)
+                        consumed = min(supply, demand)
+                        matched += copies*consumed
+                        if supply > demand:
+                            exits[e] += copies*(supply-demand)
+                            boundary[e] += copies*(supply-demand)
+                        elif demand > supply:
+                            need(supply == 0, 'Pascal demand cannot exceed present supply')
+                            sources[e] += copies*(demand-supply)
+            path_counts = following
+        sources, exits, boundary = +sources, +exits, +boundary
+        need(sources and all(1 <= s <= self.n for s in sources),
+             'all sources are positive and fit parent')
+        if self.height_base <= self.kmin:
+            need(all(self.n < self.m*s for s in sources), 'default top source bound')
+        need(all(1 <= e < self.n and self.m*e <= self.rmax*self.n for e in exits),
+             'all paid exits strictly smaller than parent')
+        need(all(self.m*e > self.kmin*self.n for e in boundary),
+             'premature exits have a failed boundary term')
+        mass = lambda h: sum(k*v for k, v in h.items())
+        surplus = mass(self.T)-mass(self.P)
+        need(mass(sources)-mass(exits) == surplus*columns,
+             'exact rank-one telescoping identity')
+        W, P = sum(self.T.values()), sum(self.P.values())
+        bound = sum(P**d*W**(self.G-d) for d in range(self.G+1))
+        need(units <= bound and sum(sources.values()) <= W*units,
+             'full integer unit/source count bounds')
+        return {'n': self.n, 'height': self.G, 'sources': sources, 'exits': exits,
+                'boundary_exits': boundary, 'units': units, 'column_mass': columns,
+                'source_count': sum(sources.values()), 'matched_jobs': matched,
+                'minimum_source': min(sources), 'all_sources_above_n_over_m':
+                    all(self.n < self.m*s for s in sources),
+                'rank_one_surplus': surplus, 'unit_count_upper': bound}
+
+    def literal(self, paid_word, class_limit=200000):
+        """Every round returns before the next; no merging of round paths."""
+        need(Counter(paid_word) == Counter(self.P), 'literal paid word matches invoice')
+        sources, exits = Counter(), Counter()
+        classes = 0
+
+        def process(depth, rho, incoming):
+            nonlocal classes
+            classes += 1
+            need(classes <= class_limit, 'literal replay class limit')
+            wanted = self.demand(depth, rho)
+            need(all(v <= wanted.get(b, 0) for b, v in incoming.items()),
+                 'all incoming whole jobs fit child slots')
+            for b, count in wanted.items():
+                missing = count-incoming.get(b, 0)
+                if missing:
+                    sources[rho*self.column(b)] += missing
+            batch = self.units(depth, rho)
+            for rank in paid_word:
+                new_rho = rho*rank
+                if depth == self.G:
+                    for a, count in batch.items():
+                        exits[new_rho*self.column(a)] += count
+                    continue
+                child = self.demand(depth+1, new_rho)
+                passed = Counter()
+                for b, count in batch.items():
+                    consumed = min(count, child.get(b, 0))
+                    if consumed:
+                        passed[b] = consumed
+                    if count > consumed:
+                        exits[new_rho*self.column(b)] += count-consumed
+                # All unconsumed exits and this entire child return at this
+                # paid position, before any later parent round is issued.
+                process(depth+1, new_rho, passed)
+
+        process(0, 1, Counter())
+        return {'sources': +sources, 'exits': +exits, 'classes': classes}
+
+
+def approximate_leaves(targets, paid, maximum, checkpoints, extra_height=0, height_base=None):
+    """Exploratory floating point recurrence; never an acceptance certificate."""
+    m = max(targets)
+    leaves = list(map(float, range(maximum+1)))
+    saved = {}
+    previous_cap = None
+    for n in range(m, maximum+1):
+        cap = n//m
+        if cap != previous_cap:
+            recipe = Flow(targets, paid, n, extra_height, height_base).merged()
+            source, exit = recipe['sources'], recipe['exits']
+            count = recipe['source_count']
+            exit_charge = sum(v*leaves[e] for e, v in exit.items())
+            previous_cap = cap
+        leaves[n] = (sum(v*leaves[n-s] for s, v in source.items())+exit_charge)/count
+        if n in checkpoints:
+            from math import log
+            saved[n] = {'leaves_approx': leaves[n],
+                        'effective_saving_approx': 1-log(leaves[n])/log(n),
+                        'source_types': len(source), 'exit_types': len(exit),
+                        'boundary_exit_types': len(recipe['boundary_exits'])}
+    return saved
diff --git a/research/selected-truncated-source-envelope/vendor/predecessor.md b/research/selected-truncated-source-envelope/vendor/predecessor.md
new file mode 100644
index 0000000000..b59d4127cc
--- /dev/null
+++ b/research/selected-truncated-source-envelope/vendor/predecessor.md
@@ -0,0 +1,252 @@
+# A two-sided complex row-depth coefficient for the #4470 nested compiler
+
+**Scoped written bound with author-checked exact arithmetic; no new κ.**
+The selected conditional exponent remains `60403/20000000`. This answers the
+open coefficient-bracket question of James Reed's [PR4972](https://github.com/CrocSwap/integer-mult-bounds/pull/4972).
+It does not compute an astronomical word or change the compiler.
+
+Put `H = 64215200000000`, `N = 2^H`, and
+
+```
+K = ceil(log2 B_N) / H.
+```
+
+For the actual #4470 product/completion/splitting rule and **#4436's nested
+divisible-width realization**, the written argument below proves
+
+```
+(2943/1000) N < K < (3639/1000) N.
+```
+
+The endpoint ratio is below `5/4`. The older lower bound used only
+`S_n >= 2`, while the upper bound counted paid rank mass as paid calls and
+used `G(N) <= H`. Counting actual root sources, charging every split and
+completion, and using the productive floor give the sharper bounds.
+These are bounds on the same permitted realization, not a search for
+smaller batching widths. #4470 does not specify a unique minimal `B_N`.
+
+In the **same conservative outer-accounting formula** as #4972, retaining
+its `c_row = 1`, support-width tariff `Cw = 232960`, BIT share, nesting and
+sum allowances, `K < 4N` gives:
+
+| Quantity | PR4972 | This bound |
+| --- | ---: | ---: |
+| Complex-share `log2` upper bound | 64,215,200,000,022 | 64,215,200,000,008 |
+| `log2 C` upper bound | 64,215,200,000,024 | 64,215,200,000,010 |
+| Displayed sufficient-fit `log2 p` | 64,473,100,659,050 | 64,473,100,659,036 |
+
+The factor-`5/4` bracket is for **K**, not for an optimal `C`. The outer
+figures retain the predecessor's deliberately loose tariffs and do not
+admit them independently. The numerical threshold comparison is a
+consequence of the new source-count bound, not a second cutoff search.
+
+## Source-bound rule and realization
+
+At base `bee95ce88f9f19802f0613f92838895cd0e14a1f`,
+`joint-helper-lattice/RESULT.json` and `PROOF.md` §§4–6 give:
+
+```
+raw productive count W0 = 10928; raw paid count Q0 = 64620;
+raw paid rank mass R0 = 239134; raw ambient rank m0 = 145;
+v = 1024; productive floor b = 21; paid cutoff c = 20.
+```
+
+The product has `W = W0^v` productive fields. Complete each target of rank
+below `L = b^v` to rank L on disjoint coordinates of that same field, then
+split every paid job at `J = c^v`. Its ambient rank is `M = m0^v` and its
+minimum productive rank is L. Completion and splitting retain all paid
+charges and do not add productive fields. Native correctness, whole-job
+adapters and physical tariffs remain the source hypotheses.
+
+Exactly 7792 raw productive fields have rank at most 21. The ordered
+product choices using only those fields give at least
+
+```
+A = 7792^1024
+```
+
+distinct final targets of rank **exactly L**: their original product rank
+is at most L, and paid completion raises it to L when necessary. This is
+a lower bound on one target multiplicity, not credit for all W targets.
+
+Use the default-height flow of `direct-mixed-flow/README.md` §§2–3:
+
+```
+G(n) = max {g >= 0 : M L^g <= n},    n >= M;
+B_n = 1 below M;
+a_n = B_(n-1),  B_n = a_n S_n;
+B_N = product_(n=M..N) S_n.
+```
+
+`S_n` counts all distinct top sources at rank n. The nested widths make
+every complement/exit batch integral. #4507's least chronological widths
+and #4483's changed-height compiler are different choices and are not used.
+
+## Proof of the two bounds
+
+**1. Fully charged paid-count upper bound.** Let Q be the final number of
+paid calls. For any positive rank R, splitting at J produces
+`ceil(R/J) <= 1 + R/J` calls. Original product calls have count `Q0^v` and
+total rank mass `R0^v`. Every completion has rank below L, and there are
+at most W completions. Hence the integer bound
+
+```
+Q <= Qbar = Q0^v + ceil(R0^v/J) + W ceil(L/J)
+```
+
+charges original calls, every original rounding surcharge and every
+completion. A completion of rank zero contributes no actual call; the
+bound may still overcount it. Write `C0 = W + Qbar + 1`.
+
+**2. A root-source injection.** In the source flow, the root multi-index
+having G copies of the minimum target type is eligible because
+`M L^G <= n`. It has at least `A^G` unit instances. Each has W distinct
+productive target slots; all these root slots are top sources, at rank
+at most n. Therefore
+
+```
+S_n >= W A^G(n).
+```
+
+These slots are distinct source arrays in the integer flow, not copied
+values or extra productive credit. The source's full-layer count also gives
+
+```
+S_n <= W (W+Q+1)^(G(n)+1) <= W C0^(G(n)+1).
+```
+
+**3. Height bounds without logarithmic approximations.** For a positive
+integer x, `bit_length(x)-1 <= log2(x) < bit_length(x)`. Thus
+
+```
+hlo = floor((H - bit_length(M)) / bit_length(L))
+    = 14276389504;
+hhi = floor((H - (bit_length(M)-1)) / (bit_length(L)-1))
+    = 14279564152;
+hlo <= G(N) <= hhi.
+```
+
+The lower estimate certifies `M L^hlo <= N`. For every integer
+`n >= M L^(hlo-1)`, `G(n) >= hlo-1`. This interval contains at least
+`N(1-1/L)` indices because `M L^(hlo-1) <= N/L`. Since `hlo >= 1`,
+the interval lies in the nonbase range. All other factors `S_n` are positive
+integers, so their logarithms cannot decrease the lower bound.
+
+Define the following small, exactly computable integers:
+
+```
+Xlo = (bit_length(W)-1) + (hlo-1)(bit_length(A)-1)
+    = 188990844254451;
+Xhi = bit_length(W) + (hhi+1)bit_length(C0)
+    = 233670787813430.
+```
+
+Summing the source logarithms proves
+
+```
+N(1-1/L) Xlo <= log2 B_N <= N Xhi.
+```
+
+The upper endpoint `N Xhi` is an integer, so it also bounds
+`ceil(log2 B_N)`. Exact integer comparisons now give
+
+```
+1000 (L-1) Xlo > 2943 L H;
+1000 Xhi < 3639 H;
+4 Xhi L < 5 (L-1) Xlo.
+```
+
+Divide by NH to obtain the stated coefficient bracket and its ratio.
+No integer of size N, no full target inventory and no uniform word is
+constructed in these checks. All integer powers computed here have only
+tens of thousands of bits.
+
+**4. Conditional outer substitution.** `batched-complex-rows.tex` and
+#4972 identify the row-depth coefficient as K under their stated contract.
+The previous formula multiplies K by an upward width factor `2^5` and
+a nesting factor 2. Since `Xhi < 4H`, `K < 4N`, so its complex share is
+below `2^(H+8)`. The unchanged BIT bound is `2^51973930319885`; the
+unchanged old-stock allowance is `2^74`. The predecessor's factor-four
+sum allowance gives `log2 C <= H+10`.
+
+For its displayed sufficient condition
+`(log2 C+10+3 ulog2(Lp))/(1-1/250) <= (69999991/70000000) Lp`,
+the verifier partitions positive integers Lp by bit length and solves
+each resulting rational linear inequality. This gives the least integer
+for that particular upward-rounded formula without assuming its stepwise
+predicate is monotone. It is not an exact physical input threshold.
+
+## Reproduction and verification scope
+
+From the repository root, Python 3.12, standard library only:
+
+```sh
+python3.12 -I -W error -B research/selected-complex-width-envelope/verify.py
+python3.12 -I -O -W error -B research/selected-complex-width-envelope/verify.py
+python3.12 -B scripts/research_package.py --package research/selected-complex-width-envelope
+```
+
+The read-only verifier authenticates every live input by SHA-256 and Git
+blob identity before and after replay. It loads only the authenticated
+#4436 flow bytes, compares merged and literal chronological flows on small
+instances, checks source/nested-width bounds and twelve exact product/
+completion/splitting cases, and requires five mathematical rejection
+controls. `RESULT.json` binds the deterministic arithmetic and finite scope.
+Direct commands support a Git-free export; metadata/provenance checks
+separately require Git. `--emit` prints the receipt to stdout.
+
+Author validation used Linux x86_64 and Python 3.12.15. Both registered
+normal/optimized modes pass: 366 small source flows, 12 literal comparisons,
+332 nested lower checks, 16 height checks, 12 product/pad/split cases and
+six reduced-power (`v=1`) calibrations of the actual #4470 raw invoice at
+rank/height boundaries. Five mathematical controls reject. Allow a minute
+for the bounded replay. Committed-byte and Git-free export checks are
+separate publication evidence; the optional full-history ancestry preflight
+is not claimed in this shallow checkout.
+
+Finite checks corroborate the written inequalities; they are not a proof
+by enumeration of every rank or native operator. All evidence from this
+session is **author-checked**, including the separately implemented
+arithmetic. No independent reviewer or proof kernel is claimed.
+
+Not checked: exact `B_N`, least/alternative batching widths, a physical
+compiled word, all-column/native correctness, owned-bank and route bodies,
+precision or fixed tapes, BIT/outer supplier admission, analytic/prime/
+recovery hypotheses, or the full selected cold replay. The `c_row`, `Cw`
+and unchanged BIT/old-stock tariffs are explicit inherited premises in the
+outer substitution. No selected record, predecessor or frozen source is edited.
+
+## Open next questions
+
+1. **Sharpen the root/source census rather than change batching.** The
+   coefficient bracket is below 5/4 but not exact. Derive a uniform bound
+   on all eligible root multi-indices and nonroot source classes for this
+   same fixed rule. First compare those counts on the literal small flows;
+   stop if the additional estimate only renames the existing bounds.
+   The missing ingredient is a quantified truncated-source estimate, not
+   another numerical outer-root calculation.
+2. **Bind the inherited physical stock interface.** This count result
+   supplies B_N for one permitted finite realization. A full implementation
+   still needs the actual fixed-program stock, routing, owned-storage and
+   precision/tape contracts. Begin with one named source-bound invocation
+   and its complete ownership ledger; the enormous uniform word is not
+   materialized here.
+
+## Attribution and task
+
+Card `selected-stock-envelope`, adversarial-audit, priority revision 7,
+refined to PR4972's open next question. Seed
+`12681598eca9c3a85296c48193125739`; exact sources and card are in
+`SOURCES.json` and `TASK.json`.
+
+Credit James Reed / jwr404 (#4972 coefficient and handoff, #4970 old leaf);
+Mark / Matarener (#4612 and `lockstep-live-role-audit`); zxv (#4436 nested
+widths, higher-moment strictification and retained native/stock sources);
+Cinna Davis / 1337isnot1337 and zxv (#4440/#4470); Jacob Alan Sussman
+(Theorem 1G multinomial lockstep flow); Ryanson Jonathan (#4476 separate
+width checks); and mihir-s-05 / #4507 and its #4519 recount for the distinct
+chronological batching boundary. All retained source notices remain intact.
+
+Prepared by Sagar Thakrar with substantial OpenAI Codex assistance, solo.
+New material is Apache-2.0. The claim and subsequent handoff are linked in
+the contribution PR; no scientific acceptance is inferred from publication.
diff --git a/research/selected-truncated-source-envelope/vendor/selected-PROOF.md b/research/selected-truncated-source-envelope/vendor/selected-PROOF.md
new file mode 100644
index 0000000000..e41106031d
--- /dev/null
+++ b/research/selected-truncated-source-envelope/vendor/selected-PROOF.md
@@ -0,0 +1,102 @@
+# Construction and proof obligations
+
+## 1. Exact predecessor and changed object
+
+The input is PR4447 at commit `322e0ec764aa7ef7801383feb1f656e460dd8bed`, with its credited THREE-base native word, PR4441 helper-boundary retiming, and the added three-dimensional frame at B/480. `SOURCES.json` binds all external proof inputs by Git blob and SHA-256.
+
+There are 632 persistent local fields: 224 main fields and 408 helpers. Each helper is an arbitrary independent input, not initialized scratch. The separate owned center is initialized and erased under the inherited native contract. None of its eight uses receives productive-input credit.
+
+The patch retains the scalar order and coefficients in each orientation. It retains all native warp events and every main-field boundary. It changes 38 helper entrance frames, 47 helper terminal frames, and 414 scalar contact frames. A source pin accompanies every changed boundary or contact. The two orientations retain their exact inverse-transpose scalar correspondence.
+
+The optional search jointly optimized both helper boundaries and every mutable scalar contact over the finite intervals of subspaces of F2^9. Fixed main and warp events bound those intervals. The largest quotient dimension was five, so its interval has 374 subspaces. The discovery model used one-hot frame choices and edge marginals, with negative whole-helper credit. Its floating-point solution is a proposal, not a certificate. The following construction and exact tests do not use its claimed optimum.
+
+## 2. Frame-coordinate invariant
+
+Let C_F be the source's exact canonical frame operator for subspace F. Interpret a field at frame F as C_F applied to its logical arbitrary value. For nested frames E contained in F, the paid transport is C_F C_E^{-1}. Its Fourier rank is dim(F)-dim(E). The implementation follows the source's `adjoint().then(...)` composition convention and lowers the operator itself, not only that rank formula.
+
+At each scalar operation, all participating persistent fields are first moved into its declared common frame. A scalar linear combination commutes with the common frame operator. Therefore the operation implements the unchanged logical scalar step. A native warp is run only at its original pinned input frame, and leaves the original pinned output frame. This proves the invariant by induction through the complete chronological word.
+
+At the end of the word, main fields have their unchanged original endpoints. Helper r has the whole residual C_{T_r} C_{S_r}^{-1}, where S_r and T_r are its new entrance and exit. Every checked S_r is a proper subspace of T_r. Its positive productive rank is dim(T_r)-dim(S_r). There is no duplicate field, discarded helper, clean-input assumption, or free temporary productive input.
+
+The helper normalizers are recomputed on these whole-job boundaries. Every new transport and each distinct helper boundary is lowered in both orientations with exact Clifford tableaux and absolute phases. The receipt contains 423 distinct transport/boundary pairs, including 406 newly occurring transport pairs relative to PR4447. Two retained literal interpreters check the complete 632-column endpoint. The argument is the frame-coordinate invariant; the finite replay independently checks its application to the submitted circuit.
+
+## 3. Complete local bill and uniform moment gain
+
+Write H_r for productive helpers of rank r and P_r for paid jobs of rank r. The predecessor has
+
+    H_old = {4:26, 5:2, 7:29, 8:42, 9:309}
+    P_old = {1:2254, 2:514, 3:444, 4:103, 5:40, 8:8}.
+
+The new word has
+
+    H_new = {4:28, 7:7, 8:47, 9:326}
+    P_new = {1:2237, 2:388, 3:494, 4:147, 5:36, 8:8}.
+
+There are 408 helpers in both words. The new paid list has 3,310 entries, 53 fewer than the predecessor. Helper rank mass increases from 3,434 to 3,471, and paid rank mass from 5,290 to 5,327. Their difference remains 1,856. In particular, the improvement is not obtained by keeping old productive credit after removing paid work.
+
+For 0<t<1, define the local surplus as sum H_r r^t minus sum P_r r^t. The new-minus-old surplus is exactly
+
+    D(t) = 17 + 126*2^t - 50*3^t - 42*4^t + 2*5^t
+           - 22*7^t + 5*8^t + 17*9^t.
+
+The verifier first checks D(1)=0. It then encloses D'(t) on 128 rational subintervals covering [0,1]. On [l,r], positive terms use the upper bound for rank^r log(rank), and negative terms use the lower bound for rank^l log(rank). Every resulting upper bound is strictly negative. Thus D is strictly decreasing on [0,1], and D(t)>D(1)=0 for every 0<t<1. This proves a uniform local improvement, not just a favorable rounded score at the chosen saving.
+
+The whole rank-eight center jobs are included in both profiles. Scalar work, helper normalizers, fixed monomial routes and owned allocation/erasure are included under the explicit finite nonrecursive allowances in RESULT.json. These allowances do not claim those operations are free.
+
+## 4. The new p16 controller
+
+Use the PR4440 constructor with p=16 and prefix length a=7, hence suffix length 8. Keep the thick stages {0,32,1,3,...,31}. There are 18 full native calls and 15 query-only shears. Each full call receives a fresh, disjoint set of 408 helper fields. Each query-only shear costs one rank-one job per port and contributes no helper or scratch productive credit.
+
+CONTROLLER.json contains the complete emitted native/query/idle word and its rational scalar boundary programs. A separate literal Laurent replay checks every coefficient. The left and right boundary matrices transform it to the declared diagonal, with central exponents exactly +1 or -1. Changed query orientation and replacing a paid thin query by an unpaid full stage both change the operator and are rejected.
+
+There are 112 port copies. Main productive ranks are 145 with multiplicity 224; ranks 17,25,33,41,49,57,65 each with multiplicity 448; and rank 73 with multiplicity 224. The matching whole-idle paid ranks are 16,24,32,40,48,56,64 with multiplicity 448, and rank 72 with multiplicity 224.
+
+Add 18 copies of H_new to the targets, 18 copies of P_new to the paid list, and 112*15 additional rank-one paid queries. This gives the complete profiles recorded in RESULT.json. They have 10,928 independent productive fields, 64,620 paid jobs, target rank mass 239,886, and paid rank mass 239,134. Their surplus is 752 = 48*18-112. Literal event counting and independent whole-call substitution give exactly the same invoice.
+
+The source contact and phase proof is local to one old nine-axis block and one fresh eight-axis block. It therefore applies at every thick p16 stage after embedding, with all other axes as spectators. The new helper boundaries do not change those main contacts. Their actual residual operators are supplied by Section 2. The BIT controller and its native rational charts remain unchanged.
+
+## 5. Exact root, paid completion and splitting
+
+Let T_t and P_t be the complete target and paid moments. The new root is enclosed strictly between 0.0030201659770 and 0.0030201659771, using t=1-C. An exact interval argument verifies that the surplus is decreasing for 0<=C<=1/20 and negative on the remainder 1/20<=C<=1. This is a fixed-invoice ceiling, not a global bound for other words.
+
+Take TESTED = 0.003020155, tensor power v=1024, tail offset u=1/5, paid cutoff 20^v and productive floor 21^v. Define
+
+    alpha = P_t/T_t,
+    gamma = P_(t+u)/(20^u T_t),
+    delta = 21 * (# productive fields)/(20^TESTED T_t).
+
+Two independent rational interval implementations verify the positive raw margin. The first also certifies
+
+    alpha < 1 - 10^-9,   gamma < 97/100,   delta < 97/100.
+
+The p16 completion tail is larger than the predecessor's 19/20 limit; this package explicitly replaces that limit with 97/100. No old tail allowance is silently reused. The same exact block inequality (97/100)^128 < 1/16 handles both tails. The inherited paid-completion and higher-moment splitting theorem consequently bounds the normalized final paid moment by
+
+    1/(1 + 1024*10^-9) + 4/2^32 < 1.
+
+Every short productive job is completed on additional disjoint axes of its same arbitrary field. Every original or added large paid job is split with its full rounding surcharge. The strict inequality 20^64 < 21^63 gives paid/target separation. These are paid operations; no padded target appears without its completion charge.
+
+## 6. Effective finite compiler and outer transfer
+
+The raw ambient rank is 145, so the tensor ambient rank is 145^1024. Use theta=63/64 and logarithm power 1000 in the credited logarithmic compiler majorant. The verifier checks
+
+    2*(20^1024)^64 <= (145^1024)^63,
+    (1-TESTED)*145^(-1024*TESTED) > theta^1000,
+    145^(1024*TESTED) < 2^1000.
+
+Set kappa=0.00302015 and d=(TESTED-kappa)/7=1/1,400,000,000. The integer test
+
+    (1,400,000,000*j + 1)^1000 < 2^j
+
+passes at j=45,868 and fails at j-1. Thus the retained theorem supplies the sufficient uniform rank N=2^64,215,200,000,000. This is an existence construction with explicit finite constants. The resulting word is not materialized and no practical implementation claim follows.
+
+The new local scalar and fixed-route bound remains below 10^7 per full call. Eighteen such calls, all 15 thin-query charges, every scalar controller and boundary operation fit the complete raw bound 10^9. The number of roles, private storage, coefficient matrices and tapes is finite for the compiled template. Their sizes affect the eventual threshold and are not claimed uniform while changing that template.
+
+Retain the source BIT ordinary saving 0.0034, with atom exponent 0.004. Its delayed-cover, weighted-child, row-stock and conversion conditions are rechecked through the source package. Use complex uniform saving kappa+6d, followed by b=kappa+5d, a=kappa+4d, q=kappa+3d, epsilon=1-d, beta=1-3d, r0=d/10, stop=d and layout=d. All nine outer cost rows, 54 strict predicates and four functional guards pass exactly. The old BIT cap and closed exponent gaps are explicit rejected controls.
+
+## 7. Status of the conclusion
+
+Subject to the retained all-column/native and physical-operation contracts, owned erasure, whole-job matching, finite-template compiler closure, precision and fixed-tape bounds, analytic decomposition, prime avoidance and exact recovery, this construction gives the source framework's conditional multiplication saving kappa=0.00302015.
+
+The submitted change establishes an exact finite native word and a fully charged conditional parameter transfer. It does not remove the inherited analytic or physical premises. It does not promote the selected frontier, certify global optimality, claim a runtime speedup, or claim independent human or proof-assistant acceptance.
+
+Credits: zxv's native and higher-moment/logarithmic work; Jacob Alan Sussman's finite mixed-flow theorem; Cinna Davis's prior p7 padding, query-thinned and retimed constructions; and the unchanged credited scalar, Clifford, geometry and outer-ledger sources. New material was prepared for Cinna Davis with substantial OpenAI assistance, Apache-2.0.
diff --git a/research/selected-truncated-source-envelope/vendor/selected.json b/research/selected-truncated-source-envelope/vendor/selected.json
new file mode 100644
index 0000000000..edf41a49a0
--- /dev/null
+++ b/research/selected-truncated-source-envelope/vendor/selected.json
@@ -0,0 +1,274 @@
+{
+  "compiler": {
+    "H": 64215200000000,
+    "N": "2^64215200000000",
+    "eta": {
+      "lower": "0.000000206231977820868640096499",
+      "upper": "0.000000206231977820868640096500"
+    },
+    "gap": "1/1400000000",
+    "integer_test_exponent": 45868,
+    "logarithm_power": 1000,
+    "theta": "63/64",
+    "uniform_saving": "528527/175000000",
+    "word_materialized": false
+  },
+  "fixed_profile_ceiling": {
+    "decreasing_through_C": "1/20",
+    "headroom": [
+      "15977/1000000000000",
+      "159771/10000000000000"
+    ],
+    "negative_derivative_upper": {
+      "lower": "-195970.145588045890401261885812812963",
+      "upper": "-195970.145588045890401261885812812962"
+    },
+    "remaining_interval_moment_upper": {
+      "lower": "-6847.019825166589746262304732988153",
+      "upper": "-6847.019825166589746262304732988152"
+    },
+    "root": [
+      "3020165977/1000000000000",
+      "30201659771/10000000000000"
+    ]
+  },
+  "full_calls": 18,
+  "gain_over_PR4416": "4171/12500000",
+  "gain_over_PR4440": "1203/20000000",
+  "gain_over_PR4441": "191/10000000",
+  "gain_over_PR4447": "473/25000000",
+  "kappa": "60403/20000000",
+  "kappa_decimal": "0.00302015",
+  "local_helpers": {
+    "4": 28,
+    "7": 7,
+    "8": 47,
+    "9": 326
+  },
+  "local_paid": {
+    "1": 2237,
+    "2": 388,
+    "3": 494,
+    "4": 147,
+    "5": 36,
+    "8": 8
+  },
+  "negative_controls": {
+    "closed_epsilon": [
+      "epsilon_below_one",
+      "global_gamma_power_slack",
+      "actual_logarithmic_gamma_guard",
+      "source_axis_superpolynomial",
+      "gaussian_above_main",
+      "new_semantic_guard_with_C1_one"
+    ],
+    "closed_uniform": [
+      "new_complex_uniform_saving_above_b"
+    ],
+    "old_BIT": [
+      "actual_bit_above_effective"
+    ],
+    "unfunded_endpoint": [
+      "main_transform_above_kappa",
+      "global_coordinate_router_above_kappa",
+      "fused_gaussian_above_kappa",
+      "group_bit_router_above_kappa",
+      "boundary_algebraic_matrix_above_kappa"
+    ]
+  },
+  "nonrecursive": {
+    "local_route_bound": 4814000,
+    "local_scalar_allowance": 158168,
+    "raw_budget": 1000000000,
+    "raw_upper": 181098496
+  },
+  "ordinary_BIT": {
+    "admitted": "17/5000",
+    "after_cover": "69/20000",
+    "atom": "1/250",
+    "before_cover": "3459/1000000",
+    "ordinary_saving": "8590884599/2500000000000",
+    "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses"
+  },
+  "outer": {
+    "functional_checks": {
+      "actual_new_BIT_stock_sublinear": "348599999253/350000000000",
+      "fixed_halo_explicit_metadata_branch": "26950000001/350000000",
+      "new_BIT_row_stock_sublinear_in_active_group": "1395799997009/1400000000000",
+      "new_semantic_group_guard": "3/1400000000"
+    },
+    "margins": {
+      "boundary_algebraic_matrix": "5919499595771787/1960000000000000000",
+      "fused_gaussian": "5919499587315361/1960000000000000000",
+      "global_coordinate_router": "2114107/700000000",
+      "group_bit_router": "2959750493657679/980000000000000000",
+      "group_scans": "699999999/700000000",
+      "main_transform": "5919498195771787/1960000000000000000",
+      "microbox_face_corrections": "26950000001/350000000",
+      "polynomial_products": "1399999999/1400000000",
+      "sparse_union_movement": "802169499595771787/1960000000000000000"
+    },
+    "parameters": {
+      "a": "2114107/700000000",
+      "b": "845643/280000000",
+      "beta": "1399999997/1400000000",
+      "bit_saving": "17/5000",
+      "cap_xi": "1782169498195771787/1960000000000000000",
+      "complex_uniform_saving": "528527/175000000",
+      "d": "1/1400000000",
+      "epsilon": "1399999999/1400000000",
+      "kappa": "60403/20000000",
+      "lambda_": "398791939/400000000",
+      "lambda_prime": "1395771787/1400000000",
+      "layout": "1/1400000000",
+      "q": "4228213/1400000000",
+      "r0": "1/14000000000",
+      "stop": "1/1400000000",
+      "tested_saving": "604031/200000000"
+    },
+    "strict_checks": {
+      "actual_bit_above_effective": "265893/700000000",
+      "actual_logarithmic_gamma_guard": "1/1400000000",
+      "actual_logarithmic_group_guard": "177830503904228213/980000000000000000",
+      "alpha_logarithm_absorption": "1/14000000000",
+      "boundary_algebraic_matrix_above_kappa": "5595771787/1960000000000000000",
+      "cap_above_band": "802169498195771787/1960000000000000000",
+      "cap_below_cell": "177830500404228213/1960000000000000000",
+      "cap_below_phase_cell_power": "2137830501804228213/1960000000000000000",
+      "complex_above_effective": "1/1400000000",
+      "complex_below_one_over_32": "7904357/280000000",
+      "complex_endpoint": "1/700000000",
+      "epsilon_below_one": "1/1400000000",
+      "epsilon_positive": "1399999999/1400000000",
+      "fine_prime_halo_umbrella": "7/2",
+      "fused_gaussian_above_kappa": "5587315361/1960000000000000000",
+      "gaussian_above_main": "695771787/980000000000000000",
+      "global_coordinate_router_above_kappa": "1/350000000",
+      "global_gamma_power_slack": "9/14000000000",
+      "group_below_dimension": "1/700000000",
+      "group_bit_router_above_kappa": "3493657679/980000000000000000",
+      "group_gauge_power_slack": "177830503834228213/980000000000000000",
+      "group_key_fits_record": "1/700000000",
+      "group_positive": "1399999997/1400000000",
+      "group_scans_above_kappa": "348942947/350000000",
+      "halo_covers_generic_inverse_radius": "5",
+      "improvement_over_user_baseline": "644589790400418148631/500000000000000000000000",
+      "lambda_above_internal": "1/2800000000",
+      "lambda_above_sigma": "3/2800000000",
+      "lambda_above_tau": "1/2800000000",
+      "lambda_prime_above_lambda": "1/2800000000",
+      "lambda_prime_above_leaf": "559154357/392000000000000000",
+      "leaf_saving_above_effective": "279154357/392000000000000000",
+      "main_transform_above_kappa": "4195771787/1960000000000000000",
+      "membership_arithmetic_fits_record": "1/1400000000",
+      "microbox_face_corrections_above_kappa": "53897885897/700000000",
+      "microbox_halo_volume": "110600000003/1400000000",
+      "new_complex_uniform_saving_above_b": "1/1400000000",
+      "new_semantic_guard_with_C1_one": "1/1400000000",
+      "polynomial_products_above_kappa": "1395771789/1400000000",
+      "positive_layout_slack": "1/1400000000",
+      "q_below_effective": "1/1400000000",
+      "q_below_internal": "1/1400000000",
+      "q_below_leaf": "559154357/392000000000000000",
+      "q_positive": "4228213/1400000000",
+      "short_record_fallback": "279154357/280000000",
+      "source_axis_superpolynomial": "1/1400000000",
+      "sparse_union_movement_above_kappa": "796250005595771787/1960000000000000000",
+      "stop_below_one": "1399999999/1400000000",
+      "stop_positive": "1/1400000000",
+      "strassen_integer_power_gap": "1951441519231",
+      "support_router_span": "3/1400000000",
+      "theta_positive_polynomial_power": "2",
+      "union_header_fits_record": "3/1400000000",
+      "union_tag_work_per_visit_fits_record": "3/1400000000"
+    }
+  },
+  "paid": {
+    "1": 41946,
+    "16": 448,
+    "2": 6984,
+    "24": 448,
+    "3": 8892,
+    "32": 448,
+    "4": 2646,
+    "40": 448,
+    "48": 448,
+    "5": 648,
+    "56": 448,
+    "64": 448,
+    "72": 224,
+    "8": 144
+  },
+  "paid_calls": 64620,
+  "pairs": 16,
+  "prefix_pairs": 7,
+  "productive_fields": 10928,
+  "query_shears": 15,
+  "scope": "Author-checked conditional construction; retained native/all-column, owned-erasure, whole-job, analytic, precision, tape, prime and recovery contracts. No selected promotion or formal/human acceptance.",
+  "source_heads": {
+    "PR4440": "40e22a83ed660d3d6074c4f2dbf14bfb621eee51",
+    "PR4441_combination": "5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39",
+    "PR4447": "322e0ec764aa7ef7801383feb1f656e460dd8bed",
+    "helper_retiming": "ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9"
+  },
+  "source_inputs": 51,
+  "status": "PASS_CONDITIONAL_JOINT_HELPER_KAPPA_00302015",
+  "strictification": {
+    "alpha": {
+      "lower": "0.999999988558808354139963023136",
+      "upper": "0.999999988558808354139963023137"
+    },
+    "cutoff": 20,
+    "delta": {
+      "lower": "0.958284435309221389866479909583",
+      "upper": "0.958284435309221389866479909584"
+    },
+    "floor": 21,
+    "gamma": {
+      "lower": "0.956176646497545264598139374323",
+      "upper": "0.956176646497545264598139374324"
+    },
+    "limits": [
+      "999999999/1000000000",
+      "97/100",
+      "97/100"
+    ],
+    "normalized_paid_upper": "2097152001953127/2097154147483648",
+    "power": 1024,
+    "tail_offset": "1/5",
+    "tested": "604031/200000000"
+  },
+  "targets": {
+    "145": 224,
+    "17": 448,
+    "25": 448,
+    "33": 448,
+    "4": 504,
+    "41": 448,
+    "49": 448,
+    "57": 448,
+    "65": 448,
+    "7": 126,
+    "73": 224,
+    "8": 846,
+    "9": 5868
+  },
+  "uniform_local_gain": {
+    "coefficients": {
+      "1": 17,
+      "2": 126,
+      "3": -50,
+      "4": -42,
+      "5": 2,
+      "7": -22,
+      "8": 5,
+      "9": 17
+    },
+    "derivative_upper": {
+      "lower": "-16.327581880492435373215953558618",
+      "upper": "-16.327581880492435373215953558617"
+    },
+    "intervals": 128,
+    "vanishes_at_one": true
+  }
+}
diff --git a/research/selected-truncated-source-envelope/verify.py b/research/selected-truncated-source-envelope/verify.py
new file mode 100644
index 0000000000..7f7b0caef9
--- /dev/null
+++ b/research/selected-truncated-source-envelope/verify.py
@@ -0,0 +1,194 @@
+#!/usr/bin/env python3
+"""Eligibility-sensitive source counts; JoyboyBrian with OpenAI Codex, Apache-2.0."""
+from collections import Counter
+from fractions import Fraction
+from hashlib import sha256
+import json
+from pathlib import Path
+import sys
+from types import ModuleType
+
+PACKAGE = Path(__file__).resolve().parent
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def sources():
+    retained = json.loads((PACKAGE / 'VENDOR.json').read_text())
+    out = {}
+    for row in retained:
+        raw = (PACKAGE / row['retained_path']).read_bytes()
+        need(sha256(raw).hexdigest() == row['sha256'], 'changed source bytes')
+        out[Path(row['retained_path']).name] = raw
+    return out
+
+
+def words(inventory, degree):
+    """Weighted ordered rank words, used only for tiny reduced fixtures."""
+    out = Counter({1: 1})
+    for _ in range(degree):
+        following = Counter()
+        for x, count in out.items():
+            for rank, multiplicity in inventory.items():
+                following[x * rank] += count * multiplicity
+        out = following
+    return out
+
+
+def census(targets, paid, n):
+    """Independent ordered-word sum of root and absent-parent target slots."""
+    m, low = max(targets), min(targets)
+    need(n >= m and low >= 2 and max(paid) < m, 'rank contract')
+    g, column = 0, 1
+    while m * column * low <= n:
+        g += 1
+        column *= low
+    need(g <= 3, 'bounded fixture budget')
+    root_spectrum = Counter()
+    for c, count in words(targets, g).items():
+        if m * c <= n:
+            for k, multiplicity in targets.items():
+                root_spectrum[c * k] += count * multiplicity
+    root = sum(root_spectrum.values())
+    nonroot_spectrum = Counter()
+    nonroot, first = 0, None
+    by_depth = []
+    for d in range(1, g + 1):
+        subtotal = 0
+        for rho, paths in words(paid, d - 1).items():
+            for r, repetitions in paid.items():
+                for c, units in words(targets, g - d).items():
+                    if m * rho * r * c > n:
+                        continue
+                    for k, multiplicity in targets.items():
+                        if m * rho * c * k > n:
+                            count = paths * repetitions * units * multiplicity
+                            subtotal += count
+                            nonroot_spectrum[rho * r * c * k] += count
+                            if first is None:
+                                first = {'depth': d, 'parent_multiplier': rho, 'paid_rank': r,
+                                         'child_column': c, 'target_rank': k, 'source_rank': rho * r * c * k,
+                                         'count': count}
+        nonroot += subtotal
+        by_depth.append(subtotal)
+    return {'n': n, 'height': g, 'root': root, 'nonroot': nonroot,
+            'by_depth': by_depth, 'total': root + nonroot, 'first_nonroot': first,
+            'source_spectrum': [list(row) for row in sorted((root_spectrum + nonroot_spectrum).items())]}
+
+
+def complete(targets, paid, floor, cutoff):
+    t, p = Counter(), Counter(paid)
+    for k, count in targets.items():
+        t[max(k, floor)] += count
+        if k < floor:
+            p[floor - k] += count
+    split = Counter()
+    for k, count in p.items():
+        quotient, remainder = divmod(k, cutoff)
+        split[cutoff] += quotient * count
+        if remainder:
+            split[remainder] += count
+    return +t, +split
+
+
+def mass(inventory):
+    return sum(k * count for k, count in inventory.items())
+
+
+def rejected(condition, name):
+    try:
+        need(condition, name)
+    except ValueError:
+        return name
+    raise ValueError('negative control accepted: ' + name)
+
+
+def verify():
+    inputs = sources()
+    flow_module = ModuleType('pinned_flow')
+    exec(compile(inputs['flow.py'], 'vendor/flow.py', 'exec'), flow_module.__dict__)
+    selected = json.loads(inputs['selected.json'])
+    raw_t = {int(k): v for k, v in selected['targets'].items()}
+    raw_p = {int(k): v for k, v in selected['paid'].items()}
+    targets, paid = complete(raw_t, raw_p, 21, 20)
+    need(mass(targets) - mass(paid) == mass(raw_t) - mass(raw_p) == 752, 'completion/split conservation')
+    calibration = []
+    for g in (1, 2):
+        for offset in (-1, 0, 1):
+            n = 145 * 21 ** g + offset
+            exact = census(targets, paid, n)
+            flow = flow_module.Flow(targets, paid, n).merged()
+            need(exact['total'] == flow['source_count'], 'selected root/nonroot census mismatch')
+            need(dict(exact['source_spectrum']) == dict(flow['sources']), 'selected spectrum mismatch')
+            need(all(145 * s > n for s in flow['sources']), 'strict source threshold')
+            degree = exact['height']
+            envelope = Fraction((degree + 1) * mass(targets) ** (degree + 1) * 145, n)
+            need(exact['total'] < envelope, 'selected moment envelope')
+            calibration.append(exact)
+    # This downward jump occurs inside a fixed-height slab, not at a height reset.
+    decline = [census(targets, paid, n) for n in (145 * 25 - 1, 145 * 25)]
+    need(decline[0]['height'] == decline[1]['height'] == 1, 'decline in one slab')
+    need(decline[0]['total'] > decline[1]['total'], 'source count is not monotone')
+    literal_cases = []
+    for t, p in [({2: 1, 5: 1}, {1: 2}), ({2: 2, 5: 1}, {1: 1, 4: 1})]:
+        for n in (5, 9, 10, 19, 20, 25):
+            f = flow_module.Flow(t, p, n)
+            actual = f.literal([r for r, count in p.items() for _ in range(count)])
+            independent = census(t, p, n)
+            need(independent['total'] == sum(actual['sources'].values()), 'literal census mismatch')
+            need(dict(independent['source_spectrum']) == dict(actual['sources']), 'literal spectrum mismatch')
+            need(all(count > 0 for _, count in independent['source_spectrum']), 'positive source multiplicity')
+            t1, p1, g = mass(t), mass(p), independent['height']
+            upper = Fraction(5 * t1 * sum(p1 ** d * t1 ** (g-d) for d in range(g+1)), n)
+            need(independent['total'] < upper, 'general moment bound')
+            need(all(5 * s > n and s <= n for s in actual['sources']), 'source bounds')
+            literal_cases.append([n, independent['root'], independent['nonroot'], independent['total']])
+    v, H = selected['strictification']['power'], selected['compiler']['H']
+    need((v, H) == (1024, 64215200000000), 'selected context')
+    W, L, M = sum(raw_t.values()) ** v, 21 ** v, 145 ** v
+    tbar = mass(raw_t) ** v + W * L
+    hhi = (H - (M.bit_length() - 1)) // (L.bit_length() - 1)
+    ratio_log_upper = tbar.bit_length() - (L.bit_length() - 1)
+    x = (hhi + 1).bit_length() + tbar.bit_length() + hhi * ratio_log_upper
+    need(mass(raw_t) > mass(raw_p), 'positive completed surplus')
+    need(1000 * x < 3070 * H, 'K/N < 3.070')
+    need(x < 233670787813430, 'strict improvement against PR5026 Xhi')
+    root_fixture = calibration[1]
+    controls = [
+        rejected(root_fixture['root'] == sum(targets.values()) ** 2, 'ignore-root-eligibility'),
+        rejected(root_fixture['total'] == root_fixture['root'], 'omit-nonroot-demand'),
+        rejected(decline[1]['total'] >= decline[0]['total'], 'assume-source-monotonicity'),
+        rejected(sum(targets.values()) == mass(targets), 'rank-mass-is-call-count'),
+        rejected(mass(targets) - mass(raw_p) == 752, 'omit-paid-completion'),
+        rejected(all(n - s == 0 for n in (10,) for s in flow_module.Flow({2:1,5:1},{1:2},n).merged()['sources']), 'omit-source-complements'),
+    ]
+    need(sources() == inputs, 'source bytes changed during replay')
+    for row in calibration + decline:
+        spectrum = row.pop('source_spectrum')
+        row['source_rank_types'] = len(spectrum)
+        row['source_spectrum_sha256'] = sha256(json.dumps(spectrum, separators=(',', ':')).encode()).hexdigest()
+    return {'schema_version': 1, 'evidence': 'author-checked scoped proof and finite calibration',
+            'selected_kappa_unchanged': '60403/20000000', 'selected_v1': calibration,
+            'nonmonotonicity': decline, 'literal_checks': literal_cases, 'negative_controls': controls,
+            'coefficient': {'H': H, 'N': '2^64215200000000', 'raw_target_mass': mass(raw_t),
+                            'raw_paid_mass': mass(raw_p), 'Tbar_log2_upper': tbar.bit_length(),
+                            'ratio_log2_upper': ratio_log_upper, 'height_upper': hhi, 'X': x,
+                            'K_over_N_strict_upper': '3070/1000', 'previous_strict_upper': '3639/1000',
+                            'previous_X': 233670787813430}}
+
+
+if __name__ == '__main__':
+    try:
+        need(sys.argv[1:] in ([], ['--emit']), 'usage: verify.py [--emit]')
+        result = verify()
+        if sys.argv[1:] == ['--emit']:
+            print(json.dumps(result, indent=2, sort_keys=True))
+        else:
+            need(result == json.loads((PACKAGE / 'RESULT.json').read_text()), 'changed receipt')
+            print('PASS_SELECTED_TRUNCATED_SOURCE_ENVELOPE: K/N < 3.070; 6 selected fixtures; 12 literal checks; 6 controls')
+    except (ValueError, OSError, KeyError, TypeError) as exc:
+        print('FAIL_SELECTED_TRUNCATED_SOURCE_ENVELOPE: ' + str(exc), file=sys.stderr)
+        sys.exit(1)

From 103f8130fe617e8c720af4cb6ce63cf638085d76 Mon Sep 17 00:00:00 2001
From: JoyboyBrian <gzybrian@gmail.com>
Date: Fri, 23 Oct 2026 00:51:50 -0700
Subject: [PATCH 2/2] Bind retained source pins to published package history

---
 research/selected-truncated-source-envelope/README.md  |  2 +-
 .../selected-truncated-source-envelope/SOURCES.json    | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/research/selected-truncated-source-envelope/README.md b/research/selected-truncated-source-envelope/README.md
index 2e90ed5948..90eef1e03f 100644
--- a/research/selected-truncated-source-envelope/README.md
+++ b/research/selected-truncated-source-envelope/README.md
@@ -105,7 +105,7 @@ python3.12 -I -O -B research/selected-truncated-source-envelope/verify.py
 python3.12 scripts/research_package.py --package research/selected-truncated-source-envelope
 ```
 
-Source spectra are compared in full during replay and retained as deterministic SHA256 receipts. The numerical and finite receipt is [RESULT.json](RESULT.json). Immutable inputs, hashes, original paths and commits are in [VENDOR.json](VENDOR.json) and [SOURCES.json](SOURCES.json). Pending #5026's exact relevant README is retained, as are the selected invoice/proof and #4436 flow implementation/proof. Direct verification is Git-free. Provenance and source-history checks are separate from mathematical validation. All package checks are author-checked; independent review and proof-kernel validation are not claimed.
+Source spectra are compared in full during replay and retained as deterministic SHA256 receipts. The numerical and finite receipt is [RESULT.json](RESULT.json). Immutable inputs, hashes, original paths and commits are in [VENDOR.json](VENDOR.json) and [SOURCES.json](SOURCES.json). Pending #5026's exact relevant README is retained, as are the selected invoice/proof and #4436 flow implementation/proof. Direct verification is Git-free. `SOURCES.json` live-input pins resolve to the retained bytes in this contribution's own history; `VENDOR.json` separately records their original heads and paths, so a cached pending-predecessor Git object is not required. Provenance and source-history checks are separate from mathematical validation. On macOS arm64 with Python 3.12, registered normal and optimized replay passed in under one second, and a Git-free copied package passed under `-O`. Altering a retained source or the result receipt caused rejection. All package checks are author-checked; independent review and proof-kernel validation are not claimed.
 
 This is a uniform source-count proof under the unchanged compiler and native hypotheses, supported by finite calibrations. It is not an emitted compiler, minimal width, physical row-depth admission, optimal coefficient, new outer cutoff, new κ, or a proof of the multiplication theorem. Native all-column, owned storage, routing, whole-job adapters, precision/tape, analytic, prime and recovery obligations remain inherited and unrun.
 
diff --git a/research/selected-truncated-source-envelope/SOURCES.json b/research/selected-truncated-source-envelope/SOURCES.json
index fd4812ed2d..4340f6a13c 100644
--- a/research/selected-truncated-source-envelope/SOURCES.json
+++ b/research/selected-truncated-source-envelope/SOURCES.json
@@ -17,35 +17,35 @@
     {
       "path": "research/selected-truncated-source-envelope/vendor/flow.py",
       "usage": "input",
-      "pin": "head:4c0a359d88f22f05189d51f48387750b801a45d4:research/direct-mixed-flow/flow.py",
+      "pin": "head:a37805e3af702295062dd9986bc92a4b186fc166:research/selected-truncated-source-envelope/vendor/flow.py",
       "git_blob": "07175cd6e1f2c2367c2e78eca7f163fef18d301d",
       "sha256": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a"
     },
     {
       "path": "research/selected-truncated-source-envelope/vendor/selected.json",
       "usage": "input",
-      "pin": "head:b9a13c1673e0e9697de410de16e8bbf3207a7363:research/joint-helper-lattice/RESULT.json",
+      "pin": "head:a37805e3af702295062dd9986bc92a4b186fc166:research/selected-truncated-source-envelope/vendor/selected.json",
       "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596",
       "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21"
     },
     {
       "path": "research/selected-truncated-source-envelope/vendor/selected-PROOF.md",
       "usage": "input",
-      "pin": "head:b9a13c1673e0e9697de410de16e8bbf3207a7363:research/joint-helper-lattice/PROOF.md",
+      "pin": "head:a37805e3af702295062dd9986bc92a4b186fc166:research/selected-truncated-source-envelope/vendor/selected-PROOF.md",
       "git_blob": "e41106031da41fade7a7419c17a32c1bd9aa103b",
       "sha256": "43ef4251cc300f1b18cbe8cdb060f96f95748e6797d2478b4c04b79a8373ef91"
     },
     {
       "path": "research/selected-truncated-source-envelope/vendor/predecessor.md",
       "usage": "input",
-      "pin": "head:6e1e7d47ed7fd7f3f7197cad7c19f8237c062b06:research/selected-complex-width-envelope/README.md",
+      "pin": "head:a37805e3af702295062dd9986bc92a4b186fc166:research/selected-truncated-source-envelope/vendor/predecessor.md",
       "git_blob": "b59d4127cc00ab8f04d76175c254d0fa4e8b0bea",
       "sha256": "421842e929b13a2adf3b3071257e36d42c0b1e7001d87be8d8df88a9a4ef7e6b"
     },
     {
       "path": "research/selected-truncated-source-envelope/vendor/flow-README.md",
       "usage": "input",
-      "pin": "head:4c0a359d88f22f05189d51f48387750b801a45d4:research/direct-mixed-flow/README.md",
+      "pin": "head:a37805e3af702295062dd9986bc92a4b186fc166:research/selected-truncated-source-envelope/vendor/flow-README.md",
       "git_blob": "3be00f754b9ffa23e64b3eafe7706e3ac139993a",
       "sha256": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8"
     }