diff --git a/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md b/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md
new file mode 100644
index 0000000000..814323fd93
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/CLAUDE-RESPONSE.md
@@ -0,0 +1,5 @@
+# Claude Code review response
+
+The initial Claude Code (Opus 5.5) review of `ff365dba6911ce615bec76e8d1f149faf1fe16ca`, its follow-up at `6310550e932de70243fc2aaab6f4885688b6fe21`, and the OpenAI Codex (GPT-6 Astra) responses are consolidated in [REVIEW.md](REVIEW.md).
+
+Use [the current evidence index](VALIDATION.md#current-evidence-index) for checked source hashes, commands and receipts. The theorem and numerical bounds are unchanged. This file preserves existing links; REVIEW.md is the authoritative review record. All reviews are AI reviews, not human or formal verification.
diff --git a/research/direct-flow-leaf-saturation/PROOF.md b/research/direct-flow-leaf-saturation/PROOF.md
new file mode 100644
index 0000000000..6d8ed0c657
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/PROOF.md
@@ -0,0 +1,123 @@
+# A nonlattice saturation theorem for the fixed #4467 leaf law
+
+This is a scoped mathematical proof using the classical nonlattice interval local-limit theorem stated below. The Python certificate verifies its source-specific numerical hypotheses and finite source-law controls; it is not a proof-kernel verification of this argument. No finite-depth error rate is claimed.
+
+## 1. Source law and statement
+
+Use the fixed raw-p7 inventories in Ryanson Jonathan / pinterbanget's #4467 (`research/direct-flow-leaf-walk/verify.py`):
+
+```
+P = {1:37305, 2:10695, 3:3360, 4:1530, 5:300,
+     8:1464, 16:448, 32:448, 48:448}
+W = {5:420, 6:270, 7:840, 8:1395, 9:3195,
+     25:448, 41:448, 57:448, 121:224}
+m = 121
+```
+
+Let `Z(s) = Σ_r P_r r^s`, `μ(s) = Z'(s)/Z(s)`, and let `t` be the unique root of `Σ_k W_k k^t = Z(t)` in the certified interval `[0.99731351095114, 0.99731351095116]`. Put `a = log 5`. Let `α` be the unique solution of `μ(α)=a` and set `λ=t−α`.
+
+The certificate also bounds the invoice derivative strictly above 211661 on the predecessor’s entire bisection interval `[0.99,1]`, so the isolated root is its unique root there. The certificate proves `μ(t)>a`, `α∈[0.98981438244597, 0.98981438244599]`, and thus `λ∈[0.00749912850515, 0.00749912850519]`. All intervals here are outward bounds, not floating-point root guesses. Uniqueness of α follows from `μ'(s)=Var_s(log r)>0`, its limits 0 and log48 at the two infinities, and `0<a<log48`.
+
+Under `p_t(r)=P_r r^t/Z(t)`, take independent `X_i=log R_i` and write `S_G=Σ_{i=1}^G X_i`. For any `δ∈[0,a]` let `B_G=Ga+δ`, and condition on `S_G≤B_G`. Define `Y_G=B_G−S_G` on that event.
+
+**Theorem.** Uniformly for `δ∈[0,a]`, as `G→∞`,
+
+1. `P_t(Y_G≥x | S_G≤B_G) → exp(−λx)` for each fixed `x≥0`;
+2. `E_t[Y_G | S_G≤B_G] → 1/λ`.
+
+The condition has positive probability because `P_1>0`.
+
+**Actual leaf consequence.** For every integer rank `N≥121`, set `G=floor(log_5(N/121))` and `δ=log(N/121)−G log5∈[0,a)`. Write `L_N(ℓ)=X_N(ℓ)−BX_N(ℓ)` for the pinned flow's leaf-exit multiplicity at rank `ℓ`, subtracting its boundary-exit histogram from its complete exit histogram and interpreting missing entries as zero. Define its potential-weighted mean leaf log-depth by
+
+```
+D_leaf(N) = [Σ_ℓ L_N(ℓ) ℓ^t log(N/ℓ)] / [Σ_ℓ L_N(ℓ) ℓ^t]
+          = [Σ_ρ Σ_r F[G][ρ] P_r (rρ)^t log(N/(rρ))] / [Σ_ρ Σ_r F[G][ρ] P_r (rρ)^t].
+```
+
+Here `F[G]` is the prefix-count table described in §2, and both sums over `r` use the entire paid inventory. The denominators are positive because the all-ones prefix and terminal rank are present. Then
+
+`D_leaf(N) → log121 − μ(t) + 1/λ ∈ [136.51870330,136.51870331]`
+
+as `N→∞`, including sequences approaching either end of a lockstep level. There is no restriction to the level starts `N=121·5^G`.
+
+## 2. Why this is the source's measure
+
+The pinned `diagnostics/overlap_flow.py` constructs `F[d][ρ]` by multiplying `d` paid ranks and retaining a new product precisely when `121·ρ≤N`. All paid ranks are positive integers, so their logarithms are nonnegative: the final product constraint implies every earlier constraint. Consequently `F[G][ρ]` is exactly the sum of `Π_i P_{r_i}` over ordered G-tuples with product ρ and `ρ≤N/121`.
+
+In its `d==G` branch, the flow issues *every* final rank `r` with multiplicity `F[G][ρ] P_r` at exit rank `rρ`. This final rank is **not conditioned** by `121·rρ≤N`. Weighting by `(rρ)^t` factorizes into the conditioned G-step law above and an independent terminal `R` with law `p_t`.
+
+Thus, exactly at every finite N,
+
+`E[log(N/(Rρ))] = log121 − μ(t) + E[Y_G | S_G≤B_G]`.
+
+This G-versus-G+1 distinction matters. The checker independently enumerates ordered words through G=3 and compares all leaf multiplicities with the whole-flow `X−BX`; an extra-terminal-truncation mutant fails. The source audit also checks the original #4436 flow. These are finite controls for the source derivation, not evidence for the asymptotic theorem.
+
+## 3. The classical input and its hypotheses
+
+We use the nonlattice interval local-limit theorem in the following standard form. If iid real `V_i` have mean zero, finite positive variance `σ²`, and a nonlattice law, then for each fixed `h>0`,
+
+`sup_x | sqrt(G) P(Σ V_i∈[x,x+h)) − h/(σ sqrt(2π)) exp(−x²/(2Gσ²)) | → 0`.
+
+Reference: C. Stone, “A local limit theorem for nonlattice multi-dimensional distribution functions,” *The Annals of Mathematical Statistics* 36(2) (1965), 546–551, [DOI 10.1214/aoms/1177700165](https://doi.org/10.1214/aoms/1177700165), **Corollary 1, equation (7), derived from the Theorem, equation (5), with footnote 2's uniformity convention**. The displayed form is a specialization, not a verbatim quotation. Use `d=1`, `A_G=0`, `B_G=√G` in Stone's normalization (his `B_G` is unrelated to our barrier `Ga+δ`), and normal limiting density `φ_σ(u)=exp(−u²/(2σ²))/(σ√(2π))`. For `T_G=Σ V_i` and any fixed width `H>0`, substitute `x=X/√G` and `h=H/√G` in his half-open boxes. This gives, uniformly over `X∈R`,
+
+```
+P(T_G∈[X,X+H)) = ∫_[X/√G,(X+H)/√G) φ_σ(u) du + o(G^(−1/2))
+               = (H/√G) φ_σ(X/√G) + o(G^(−1/2)).
+```
+
+The second equality uses uniform continuity of the Gaussian density. Multiplying by `√G` gives the required supremum statement; footnote 2 makes the remainder uniform in the unlisted variable `x`, hence also in `X`. The paper's Corollary 4, equation (12), is only a fixed-`x` statement and is not the input used for our uniform concentration bound. Stone's theorem is an external mathematical dependency; no discrete law is replaced by a density without this interval argument.
+
+Apply it to the tilted law `q(r)=P_r r^α/Z(α)`, with `V=log r−a`. Its mean is zero by definition, and its variance is positive and finite because the support is finite and contains distinct points of positive mass. The ordinary central limit theorem supplies Stone's normal domain-of-attraction hypothesis with this normalization. The support is nonlattice: it contains `0,log2,log3` before centering. If all belonged to a translate of `hZ`, their differences would imply `log2/log3` rational. An integer relation `u log2=v log3` with nonzero integers would imply `2^u=3^v`, contradicting unique factorization. Centering and tilting do not alter this property.
+
+This support argument verifies Stone's characteristic-function condition (2). Indeed, for `θ≠0`, equality `|E exp(iθV)|=1` holds exactly when the unit complex variable `exp(iθV)` is almost surely constant, equivalently when the support lies in `c/θ+(2π/θ)Z` for some real `c`. Thus nonlattice support gives strict inequality for every nonzero `θ`.
+
+The finite support does **not** satisfy Stone's stronger condition (3): simultaneous approximation of its finitely many phases gives arbitrarily large `|θ|` for which the characteristic-function modulus approaches one. Under that condition, Stone's equations (6) and (8) extend the local-limit statement to boxes as small as `exp(−cn)` for a suitable `c>0`; their remainder is still an unquantified `o(1)`. Neither equation is used here. Our proof uses equations (5) and (7) for fixed unnormalized windows. Neither cited version supplies an explicit quantitative convergence rate, error constant or onset `G`; failure of condition (3) is not the explanation for this missing quantitative information. Such bounds require additional work and are not ruled out by this argument.
+
+Two consequences are used:
+
+- For fixed finite intervals in y, `sqrt(G) Q(B_G−S_G∈I) → |I|/(σ sqrt(2π))`, uniformly over bounded δ.
+- There is a constant C such that for all `G≥1` and all real x, `sqrt(G) Q(S_G∈[x,x+1))≤C`.
+
+The second follows from the theorem for h=1 for sufficiently large G, and enlarging C for finitely many smaller G. It is an existence bound, not a computable convergence rate. Either convention for half-open intervals works: the maximum atom is `o(G^(-1/2))`, by bounding it with an interval of arbitrary fixed h and then taking h down to zero. This also handles an atom at the exact truncation boundary.
+
+## 4. Weighted local limits and integrable tails
+
+Write `c=1/(σ sqrt(2π))`. For the nonnegative functions
+
+`f_0(y)=exp(−λy)`, `f_1(y)=y exp(−λy)`, and `f_x(y)=1_{y≥x} exp(−λy)`,
+
+we claim, uniformly in δ,
+
+`sqrt(G) E_q[f(B_G−S_G) 1_{S_G≤B_G}] → c ∫_0^∞ f(y)dy`.
+
+On a fixed compact interval this follows by upper and lower step-function approximations and the interval local limit. The functions are bounded and Riemann integrable there, including the single jump of `f_x`; the possible boundary atom is negligible by §3.
+
+For an integer `J≥0` and the tail partition into intervals `[j,j+1)`, the concentration bound in §3 gives, uniformly over G and δ,
+
+`sqrt(G) E_q[f_0(Y_G) 1_{Y_G≥J}] ≤ C Σ_{j≥J} exp(−λj)`,
+
+and
+
+`sqrt(G) E_q[f_1(Y_G) 1_{Y_G≥J}] ≤ C Σ_{j≥J} (j+1) exp(−λj)`.
+
+Here Y_G denotes the unconditioned difference `B_G−S_G` inside the indicated nonnegative event. Both series tend to zero as `J→∞` because λ>0; `f_x≤f_0` has the same domination. This proves the weighted local limits and supplies the missing uniform-integrability argument for the mean. Weak convergence alone would not suffice.
+
+## 5. Undoing the tilt
+
+For an ordered G-tuple,
+
+`p_t(tuple)/q(tuple) = (Z(α)/Z(t))^G exp(λ S_G)`.
+
+On writing `S_G=B_G−y`, the common factor `(Z(α)/Z(t))^G exp(λ B_G)` cancels in every conditional ratio. Hence
+
+`P_t(Y_G≥x | S_G≤B_G) = E_q[f_x(B_G−S_G) 1_{S_G≤B_G}] / E_q[f_0(B_G−S_G) 1_{S_G≤B_G}]`,
+
+and the analogous numerator with `f_1` gives the conditional expectation. By §4, the three scaled integrals converge to `c exp(−λx)/λ`, `c/λ²`, and `c/λ`. The denominator limit is strictly positive, so their ratios converge uniformly over δ to `exp(−λx)` and `1/λ`. Section 2 then gives the claimed leaf-depth limit.
+
+## 6. Scope, controls, and remaining decisions
+
+This proves the saturation that #4467 explicitly labelled heuristic. It does **not** prove its suggested total log-gap `g∞≈122`, stable source/boundary/leaf shares, any numerical refined-induction ceiling, or the quoted astronomical ranks required to achieve a saving. Those require separate control of other flow components and a finite-depth estimate. The raw-p7 inventory is historical and is not the selected #6030 invoice.
+
+Nonlattice support is essential for this limit law. For `X∈{0,log2}` with probabilities `(1/3,2/3)` and even G, conditioned at `B_G=G log2/2`, λ=1 but the limiting deficit is `log2` times a geometric variable with probabilities `2^(-j-1)`, j≥0. Its mean is `log2`, not 1. Indeed the successive binomial mass ratio below G/2 tends to 1/2 and is bounded by 1/2, which proves both the geometric limit and mean convergence by domination. The verifier includes this failure control. Zero or negative relative drift likewise lies outside the theorem's λ>0 hypothesis.
+
+Credit: the flow is zxv's #4436, the refined induction is Cinna Davis / 1337isnot1337's #4405, the lockstep construction is Jacob Alan Sussman's Theorem 1G, and the source law, saturation conjecture and diagnostics are Ryanson Jonathan / pinterbanget's #4467 (following #4465). This proof and certificate were prepared for DLamdata with substantial OpenAI Codex assistance. Apache-2.0. Internal AI checks are not independent human review or formal verification.
diff --git a/research/direct-flow-leaf-saturation/README.md b/research/direct-flow-leaf-saturation/README.md
new file mode 100644
index 0000000000..bf1ce2a4c5
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/README.md
@@ -0,0 +1,54 @@
+# The fixed #4467 leaf deficit saturates, uniformly across lockstep levels
+
+This package proves the saturation predicted by Ryanson Jonathan / pinterbanget's [#4467](https://github.com/CrocSwap/integer-mult-bounds/pull/4467). For its fixed raw-p7 paid-rank law, the conditional deficit `B_G−S_G` converges to `Exp(λ)`, **including convergence of the mean**, uniformly for `B_G=G log5+δ`, `0≤δ<log5`. The actual source has **G conditioned paid ranks plus one unconditioned terminal rank**.
+
+The exact rational certificate encloses `λ ∈ [0.00749912850515, 0.00749912850519]`, limiting mean deficit in `[133.34882837,133.34882838]`, and limiting actual leaf log-depth in **`[136.51870330,136.51870331]`**. The added value over #4467's numerical conjecture is the proof, bounded-offset uniformity and certified numerical hypotheses.
+
+This resolves the qualitative leaf-saturation question. It supplies **no explicit finite-depth error rate**, stable-share theorem, full-flow log-gap limit, numerical refined-induction ceiling, new κ or supplier admission. The raw-p7 profile is historical; the selected #6030 record and its five assumptions are unchanged. The predecessor's estimated `.0025–.0026` ceiling and astronomical finite-rank thresholds remain unproved here.
+
+## Start here
+
+| Reader's goal | Read or run |
+| --- | --- |
+| Understand the theorem and source law | [PROOF.md §§1–2](PROOF.md#1-source-law-and-statement), then §§3–5 for the argument. |
+| Reproduce the finite checks | The command below; [VERIFY.json](VERIFY.json) declares all four checks and five predecessor inputs. |
+| Find the evidence for current code | [VALIDATION.md: current evidence index](VALIDATION.md#current-evidence-index), including source hashes, log links and historical/current distinctions. |
+| Assess objections and independence | [REVIEW.md](REVIEW.md): current verdict, all six Claude findings and resolutions, shared dependencies, then review history. |
+| Continue the research | [Open next questions](#open-next-questions); [TASK.json](TASK.json) retains the original card, actual scope and structured questions. |
+
+From the repository root, using **Python 3.12** and the standard library only:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/direct-flow-leaf-saturation
+```
+
+This runs all four registered checks serially; the recorded run took about **75 seconds**. It verifies finite numerical/source evidence, not the analytic theorem. [VALIDATION.md](VALIDATION.md#reproduction-and-evidence-reuse) gives Git-free commands, optimized-mode receipts and when evidence must be rerun. The [contribution PR is #6118](https://github.com/CrocSwap/integer-mult-bounds/pull/6118); consult it for live review and CI status.
+
+## What supports each claim
+
+| Claim | Supporting evidence | Limit |
+| --- | --- | --- |
+| Conditional distribution and mean converge uniformly over offsets | [Written proof](PROOF.md), using Stone's interval local-limit theorem and a uniform expectation-tail bound | Classical theorem is an external dependency; no effective finite-G rate. |
+| Root, tilt and limiting mean lie in the stated intervals | [verify.py](verify.py) and [RESULT.json](RESULT.json), using exact rational enclosures | Certifies this fixed source law, not a new supplier or multiplication bound. |
+| The source emits G conditioned ranks and an unconditioned terminal rank | All-G source reading in [PROOF.md §2](PROOF.md#2-why-this-is-the-sources-measure); eight primary and ten independent complete-histogram fixtures against #4467 and #4436 | Fixtures overlap and stop at G=3; they corroborate the derivation rather than exhaust all G. |
+| Specified source faults are rejected | [test_controls.py](test_controls.py): changed-byte checks plus re-pinned empty/truncated #4467 branches and an altered #4436 returned histogram, normal and optimized | Semantic rejection comes from the actual histogram comparisons; terminal-cut flags describe fixture sensitivity only. |
+| Numerical enclosures contain independent bounds on the executed domain | [test_enclosures.py](test_enclosures.py): 16 log and 127 exp arguments; three targeted remainder faults rejected | Finite captured domain; shared exact arithmetic and exponential series, not all-input formal verification. |
+
+The numerical certificate uses a 48-term `2 atanh(z)` series with a geometric tail for logarithms, and an 80-term exponential series with the Lagrange majorant `3^5` on `[0,5]`. The independent checker uses a different logarithm series and a geometric exponential-tail bound. Root isolation uses endpoint signs and a derivative lower bound; tilt uniqueness uses positive variance. Decimals are rounded outward; no predecessor floating-point root finder or data fit supplies the certificate. A lattice countermodel demonstrates the need for nonlattice support; the certificate also checks positive drift and rejects invalid interval-operation inputs.
+
+## Sources and coordination
+
+Scientific base: `721c03822c421b7f7fcbb2598993b947c4d88419`; priority revision 8. #4467's frozen source head is `5f5c1f98c62b9ce4f3db6c0ca47a850a0be577dc`. Its [completed investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19111052) and [request for a saturation proof](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19111508) are predecessor coordination references. The canonical coordination record is [#1166 comment 19240402](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19240402). [SOURCES.json](SOURCES.json) pins every live predecessor input to the base; no unmerged source history is needed.
+
+The original direct flow is zxv's #4436 (`56003680aee2871773de408e5f01cc5dd46b144c`); the refined induction is Cinna Davis / 1337isnot1337's #4405; the lockstep construction is Jacob Alan Sussman's Theorem 1G. #4467, following #4465, already conjectured saturation and measured it numerically. The added value here is the proof, bounded-offset uniformity, certified hypotheses, and explicit separation of the leaf result from the whole-flow extrapolations.
+
+## Open next questions
+
+1. **Give a certified finite-G error bound.** Start by obtaining an effective interval local-limit estimate for this fixed tilted log-rank law, then combine it with the weighted-tail decomposition in PROOF.md §4. A useful result would give explicit constants and an onset for the conditional mean error, uniformly over the level offset. The present proof's concentration constant and onset are existential. Stone's stronger nonlattice refinements extend the allowed box sizes, but still provide no quantified remainder; their failure for finite support does not explain the missing error rate. Reuse the pinned law, tilt enclosure and tail decomposition, but review and certify any new quantitative estimates.
+2. **Analyze the other flow components and the exact induction ratio.** Start from #4436's source and boundary sums at the same bounded level offset, retaining all terms. A useful first result would be a source-bound formula or bound for one component's normalized potential contribution, with any offset dependence explicit. Stable shares and the exact-ratio asymptotic remain blockers to a whole-flow ceiling; the leaf limit alone supplies neither. Reuse the source pins and leaf identity, not the predecessor's heuristic total ceiling.
+
+Related pending work by Nick Petalas: [#6125](https://github.com/CrocSwap/integer-mult-bounds/pull/6125) (`f58e29052a0bbb4e123ea777b5e03321fde6f31f`) extends this framework to three power-tariff regimes; [#6128](https://github.com/CrocSwap/integer-mult-bounds/pull/6128) (`9be0bd96279cd66098a9d536ffd0092fd771550a`) reports an explicit finite-depth tail envelope and clipping bound. Both cite our `6310550e` scientific snapshot. These descriptions were checked, but their proofs and certificates were not audited here. A continuation should assess that work before duplicating it; a decreasing convergence-error estimate remains open in both descriptions.
+
+Structured questions are in [TASK.json](TASK.json). A wider construction search needs a separate justification under the repository's family-expansion gate.
+
+Prepared for DLamdata with substantial OpenAI Codex (GPT-6 Astra) assistance, including separate agents for independent mathematical/source checks and skeptical review. Claude Code (Opus 5.5) reviewed the initial published snapshot; [REVIEW.md](REVIEW.md) records its findings and the response. These are AI reviews, not human or formal verification or maintainer acceptance. Predecessor credit and Apache-2.0 licensing are retained.
diff --git a/research/direct-flow-leaf-saturation/RESULT.json b/research/direct-flow-leaf-saturation/RESULT.json
new file mode 100644
index 0000000000..a799a944c4
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/RESULT.json
@@ -0,0 +1,49 @@
+{
+  "controls": {
+    "interval_domain_rejections": 3,
+    "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1"
+  },
+  "finite_law": {
+    "ordered_word_max_depth": 3,
+    "source_check": "complete actual X-BX histogram equals ordered-word enumeration",
+    "terminal_cut_distinguishing_fixtures": 8,
+    "whole_flow_fixtures": 8
+  },
+  "parameters": {
+    "alpha": [
+      "0.98981438244597",
+      "0.98981438244599"
+    ],
+    "drift_above_log5": [
+      "0.016477707041",
+      "0.016477707042"
+    ],
+    "invoice_derivative_lower_bound_interval_0_99_to_1": [
+      "211661.930309",
+      "211661.930310"
+    ],
+    "lambda": [
+      "0.00749912850515",
+      "0.00749912850519"
+    ],
+    "mean_deficit_limit": [
+      "133.34882837",
+      "133.34882838"
+    ],
+    "mean_leaf_depth_limit": [
+      "136.51870330",
+      "136.51870331"
+    ],
+    "mean_log_rank": [
+      "1.625915619475",
+      "1.625915619476"
+    ],
+    "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds",
+    "t_star": [
+      "0.99731351095114",
+      "0.99731351095116"
+    ]
+  },
+  "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.",
+  "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS"
+}
diff --git a/research/direct-flow-leaf-saturation/REVIEW.md b/research/direct-flow-leaf-saturation/REVIEW.md
new file mode 100644
index 0000000000..4993b9e5d3
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/REVIEW.md
@@ -0,0 +1,95 @@
+# Review findings and evidence limits
+
+## Current review status
+
+Current source hashes and checks are indexed in [VALIDATION.md](VALIDATION.md#current-evidence-index). The follow-up review of `6310550e932de70243fc2aaab6f4885688b6fe21` was applied to `9946b1c42466ada889c10cd0cea7522d6360a63b`, whose intervening changes were documentation only. This response corrects one Stone paragraph and adds a control for the original #4436 comparison. The theorem, its argument, all numerical results and pinned predecessor inputs are unchanged.
+
+Claude Code (Opus 5.5) reviewed both the initial `ff365dba6911ce615bec76e8d1f149faf1fe16ca` snapshot and the response at `6310550e`. Its follow-up confirmed findings 1, 2, 3, 4 and 6 were resolved except for the Stone wording below; finding 5 remains a disclosed coverage limit. The six findings and follow-up resolutions below are the canonical review record. OpenAI Codex (GPT-6 Astra) performed the fixes and internal checks. These are AI reviews, not independent human review, proof-kernel verification or maintainer acceptance.
+
+### Follow-up findings at 6310550e
+
+| Finding | Resolution | Evidence and limit |
+| --- | --- | --- |
+| Stone's stronger condition was incorrectly described as giving a rate | PROOF.md now distinguishes refinements (6)/(8), allowing boxes as small as exp(−cn), from a quantified remainder rate. Their remainder is still unquantified o(1); neither refinement is used. README and the original finding-1 record below are corrected too. | The wording originated in the first Claude review and was corrected by its follow-up primary-text check. Internal review confirms only this explanatory paragraph changed; a fresh primary-PDF retrieval remained unavailable internally. No theorem or argument change. |
+| No control guarded the original #4436 Flow comparison | A scratch copy changes the returned boundary histogram by one count, re-pins that source, and requires the specific `(121, 'original Flow class')` rejection in normal and optimized modes. | The mutation is applied after Flow's own telescoping check, so that check cannot mask the comparison. Deleting just the original-Flow comparison must now make the new control fail; positive fixtures remain unchanged. |
+
+Internal follow-up review independently checked that the returned-boundary mutation changes the N=121 leaf count at rank 1 from 37305 to 37304 after all native invariants, verified re-pinning and restoration, and compared the deleted-guard results. No unresolved blocker remained in the scoped fix. Current proof/control hashes and executed evidence are recorded in VALIDATION.md.
+
+The follow-up review also independently exercised production remainder faults, deletion of the primary source comparison, and disabled standalone pin checks. Those are reported Claude runs, not additional local runs. Local commands and results for this response are distinguished in VALIDATION.md.
+
+
+## Claude review findings
+
+| Finding | Resolution | Evidence and limit |
+| --- | --- | --- |
+| 1. Stone statement and uniformity need precise citation | PROOF.md §3 now names Corollary 1 (7), Theorem (5) and footnote 2; gives the normalization/rescaling and characteristic-function/support equivalence. | Fixed-x (12) is explicitly not the source of uniform concentration. The review reports checking the primary paper; the follow-up internal proof review corroborated the uniform form from Stone's later text but did not retrieve the original afresh. Stone's stronger nonlattice condition fails for finite support, but (6)/(8) concern shrinking boxes, not quantified remainder rates. Neither refinement is used; quantitative rates by other methods remain possible. |
+| 2. Terminal-rank flags overstate coverage | Removed the redundant self-factorization assertion; renamed flags as fixture sensitivity. The source identity is the complete histogram comparison. | `test_controls.py` empties or truncates #4467's leaf branch in a temporary tree, re-pins the mutant bytes, and requires semantic rejection by both source-law entry points, normally and under `-O`. The follow-up adds a distinct control for the original #4436 comparison. A checksum failure cannot count as this semantic rejection. |
+| 3. Remainder bounds lack discriminating controls | Added `test_enclosures.py`, an exact-rational independent enclosure oracle. | It checks every successful log/exp argument captured from current `parameters()` and `controls()`. Logarithms use a different series; exponentials use a positive-series geometric tail rather than the primary Lagrange bound. Zero logarithm/exponential tails and the invalid majorant 1 are rejected at explicit fixtures even though the old rounded receipt did not distinguish them. |
+| 4. Standalone independent source checker lacks byte binding | `independent_source.py` authenticates every declared live input before any predecessor import. | Comment-only mutations to both predecessor verifier and original flow are rejected by both standalone entry points in normal and optimized modes. No Git is needed. |
+| 5. Executable source domain ends at G≤3 | Retained and explicitly scoped; no unnecessary search expansion. | The source proof is for every G, while the local primary/independent fixtures remain eight/ten checks through G=3. Claude reported further G=4–5 corroboration; this package does not present that as a newly executed local check. |
+| 6. Leaf observable lacks an explicit formula | PROOF.md §1 now defines the normalized potential-weighted sum over `X−BX`, and its equivalent sum with weights `F[G][ρ] P_r (rρ)^t`. | The final rank uses the full paid inventory and both denominators are positive. The limit is unchanged. |
+
+## Shared dependencies and remaining limits
+
+The remainder oracle certifies containment on the captured finite argument domain. Both implementations still share Python's exact rational arithmetic and the exponential series; the logarithm series and exponential remainder arguments differ. This is not formal verification or a proof of the routines for arbitrary future inputs. Its domain digest and loaded verifier SHA identify the checked inputs and code. It independently checks the log/exp building blocks, not the surrounding interval operations, the μ(t) construction or outward rounding; those rely on the pinned receipt, code review and the earlier independent decimal diagnostic. The diagnostic corroborates values but does not itself certify rational bounds.
+
+The +1 histogram mutations are regressions for the fixed narrow root bracket, not general tests of interval arithmetic. The derivative-bound endpoint ordering is justified by the written monotonicity argument and code review; a changed printed derivative is also caught by the expected receipt. The new enclosure tests do not claim to independently prove that derivative formula.
+
+The source mutation controls exercise the complete histogram equality checks. A flag saying that a fixture has an exit above N/121 only describes its ability to distinguish truncation; it does not independently authenticate or validate a source implementation.
+
+The registered runner still declares Python 3.12. README commands now explicitly select `python3.12` to avoid a default `python3` selecting 3.13 and failing that version gate. No dependency or runner policy is changed.
+
+The independent mathematical derivation and lead proof both use Stone's interval local-limit theorem. Initial internal reviewers did not retrieve the original 1965 full text; Claude's later primary-text review supplied the precise equation/footnote mapping. The follow-up internal reviewer corroborated the uniform form using Stone's later text but did not retrieve the original paper afresh. These are distinct review steps, not multiple independent checks of that primary citation.
+
+The independent and primary finite source checks share the pinned inventories and ordered-word characterization; they compare against two separately implemented predecessor flows. Eight primary and ten independent fixtures include overlapping ranks and extend only through G=3. They are corroborating examples, not an exhaustive all-G check or evidence for the asymptotic theorem.
+
+For commands and current receipts, use [VALIDATION.md](VALIDATION.md#current-evidence-index). Finite-depth rates, stable whole-flow shares, the exact refined-induction ceiling and supplier admission remain open. The selected #6030 record is unchanged.
+
+## Historical review record
+
+### Internal review of the first response
+
+Before the new Claude follow-up, an internal reviewer checked the alternative logarithm series, the degree 82 exponential geometric tail, full containment, targeted remainder fixtures, re-pinned #4467 source mutations and pre-import hashes. It found no blocker at that review's scope. Reviewed verifier SHA256 `3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d`; oracle `b92a75601ef676ab0b412395eb2ccaa52c8e802f89fe1fb2f3820cafa173aea4`; then-current proof `09dc0d6fd22b5e502b812543ddf78395ab7deacc894cd52430709475acfb2978`. The subsequent Claude review identified the Stone wording and missing #4436 guard recorded above. The old proof hash is retained as provenance, not a hash of the corrected current proof.
+
+
+The following sections record the initial `ff365dba6911ce615bec76e8d1f149faf1fe16ca` contribution and intermediate reviewed bytes. Their hashes and receipts are historical; use the current evidence index above for present code. Two separate OpenAI Codex agents examined pinned source inputs before seeing the lead's proof.
+
+### Independent mathematical derivation
+
+The first verifier derived the bounded-offset exponential deficit law and expectation limit from the source independently, then compared the written proof. It identified the need for a global interval concentration bound to justify the mean, and verified the extra outgoing rank is unconditioned. Its 70-digit mpmath diagnostic found `λ≈0.00749912850517142053` and limiting leaf mean `136.518703301364906…`, agreeing with the later rational intervals. Those floating-point values are diagnostic, not the certified evidence.
+
+The independent argument and lead proof both use Stone's interval local-limit theorem. Thus this is an independently derived argument with a **shared classical theorem**, not two unrelated foundations or an independent proof of that theorem. Neither review retrieved the original 1965 theorem's full text; the exact standard interval formulation used is stated in PROOF.md. Original journal contents and published bibliographies corroborate the citation.
+
+The comparison reviewed PROOF.md SHA256 `6c3bdfeeb87bf007d6d37fd2eb131ddf9cbff548d837ecb880f72c0bd229c7d4`. It found no gap in the source law, uniform bounded-offset argument, boundary-atom treatment, or expectation tail bound. It caught a bibliographic error: the draft's Duke journal reference was wrong. The final proof uses *Annals of Mathematical Statistics* 36(2), 546–551 (1965), DOI `10.1214/aoms/1177700165`. This correction and spelling out integer J do not change the argument.
+
+### Independent source check
+
+The second verifier reconstructed the leaf histogram by enumerating ordered paid-rank words, then compared it with **both** #4467's diagnostic flow and the original #4436 `Flow` class. Ten exact fixtures straddle lockstep boundaries: N=121,604,605,606,3024,3025,3026,15124,15125,15126. Their leaf support sizes are 9,9,26,26,30,55,55,65,98,98. All agree; every fixture distinguishes incorrectly truncating the outgoing rank.
+
+The independently written check is preserved as [independent_source.py](independent_source.py), with its output in [logs/independent.log](logs/independent.log). The lead changed only its path selection for portability and replaced assertions with explicit errors so its controls survive `-O`; both forms of the integrated script were rerun. The independent check and primary fixture share the same source inventories and ordered-word characterization, but compare against separately implemented predecessor flows. This checks source interpretation, not the asymptotic theorem.
+
+Source identities checked against retained #4467 head `5f5c1f98c62b9ce4f3db6c0ca47a850a0be577dc`:
+
+| Input | SHA256 |
+| --- | --- |
+| `research/direct-flow-leaf-walk/verify.py` | `2030d79d7f136b39b4e2a3f5b033af4bba18ab87579ec352267dc1697e02157d` |
+| `research/direct-flow-leaf-walk/diagnostics/overlap_flow.py` | `7a1945cadb6bf8f8d88eae32f321ad75c10d5280805e111de6bb02d3d7628117` |
+| `research/direct-flow-leaf-walk/README.md` | `bf79c953cd02ad62ffd44c58ae4f5b78f2b3439574176140ba6eceb1b77430cc` |
+
+Original `research/direct-mixed-flow/flow.py` matches #4436 head `56003680aee2871773de408e5f01cc5dd46b144c` (SHA256 `460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a`). Its retained p7 receipt has SHA256 `9b814be97e3b45fcc28eafa8a65694897a7387f71a14d44796c6aadf303d7fab`; `strictification.paid` and `.targets` equal P,W. All replay inputs are pinned at the publication base, so these historical source-head references are provenance, not required foreign commits.
+
+### Skeptical proof and checker review
+
+The second reviewer then inspected the frozen proof and verifier (verifier SHA256 `a290589881aa04480ac1b50245a1c0faf3e1acebebea9d99ddc227280c519cfe`; see validation source hashes for final integrated bytes). It checked the rational logarithm and exponential remainders, endpoint isolation, nonlattice premise, tail bounds, and claim limits. Normal and `-I -O` verifier outputs agreed. Altered source bytes, a corrupted expected receipt, and +1 paid/target multiplicity mutations were rejected.
+
+No blocking issue was found. The reviewer recommended strengthening monotonicity from the tiny root enclosure to the predecessor's full `[0.99,1]` bisection interval. The final checker implements that stronger bound, exceeding 211661, and includes both +1 histogram controls. The lead reran all affected evidence after this change; the original review hashes do not pretend to identify the final bytes.
+
+### Initial integration review
+
+The skeptical reviewer read the integrated stronger derivative bound, both +1 histogram controls, portable two-source fixture and package claims. No blocker remained. Final reviewed proof SHA256 `b6edd825bc5a3a48fc2860533040faa111c7f239f8724bb3b50cc8a3bdfdc6e7`; verifier SHA256 `9a6ed8de94eab4a643685eba3697d34503bae9dd4c6097b6b8a6f230c29dd3b8`. The reviewer checked that the last proof change was only PR-reference spelling. The confirmed canonical claim link was added to README. Registered evidence and publication checks are reported separately.
+
+### Overlap and limits
+
+Orientation coverage was complete for 375 open PRs, 5,222 closed/merged PRs, 5,771 Discussion records and 8,348 local notes at base `721c03822c421b7f7fcbb2598993b947c4d88419` (2026-10-28 11:09–11:11 UTC). Broader body searches also found #4477's disposition, the later finite-share diagnostic, and the author's explicit request for a saturation proof; these still left the proof open. The final refresh is recorded in VALIDATION.md. No body search establishes novelty or covers every code diff.
+
+Remaining obligations are an effective finite-depth rate and the other full-flow components/exact induction ratio. Finite tests do not prove the asymptotic result; the asymptotic result does not certify finite-depth extrapolations, a supplier, or the multiplication theorem.
diff --git a/research/direct-flow-leaf-saturation/SOURCES.json b/research/direct-flow-leaf-saturation/SOURCES.json
new file mode 100644
index 0000000000..25904cd40d
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/direct-flow-leaf-walk/README.md",
+      "usage": "input",
+      "git_blob": "02ddde948f2e94874850eadd70d7d32559916848",
+      "sha256": "bf79c953cd02ad62ffd44c58ae4f5b78f2b3439574176140ba6eceb1b77430cc"
+    },
+    {
+      "path": "research/direct-flow-leaf-walk/diagnostics/overlap_flow.py",
+      "usage": "input",
+      "git_blob": "60c1997786cc452e0828c127a47582c1aeeef7f4",
+      "sha256": "7a1945cadb6bf8f8d88eae32f321ad75c10d5280805e111de6bb02d3d7628117"
+    },
+    {
+      "path": "research/direct-flow-leaf-walk/verify.py",
+      "usage": "input",
+      "git_blob": "42440e630a46c6e581797f52bfb4c0c87bbdac3a",
+      "sha256": "2030d79d7f136b39b4e2a3f5b033af4bba18ab87579ec352267dc1697e02157d"
+    },
+    {
+      "path": "research/direct-mixed-flow/flow.py",
+      "usage": "input",
+      "git_blob": "07175cd6e1f2c2367c2e78eca7f163fef18d301d",
+      "sha256": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a"
+    },
+    {
+      "path": "research/direct-mixed-flow/vendor/p7-RESULT.json",
+      "usage": "input",
+      "git_blob": "ebb30a9b3b94fb159a316350f7da57bde4a30c25",
+      "sha256": "9b814be97e3b45fcc28eafa8a65694897a7387f71a14d44796c6aadf303d7fab"
+    }
+  ]
+}
diff --git a/research/direct-flow-leaf-saturation/TASK.json b/research/direct-flow-leaf-saturation/TASK.json
new file mode 100644
index 0000000000..fcc181cdfb
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/TASK.json
@@ -0,0 +1,105 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "invoice",
+      "signed moment",
+      "productive target",
+      "independent recount"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove conditional leaf-deficit distribution and mean saturation for the fixed raw-p7 law of #4467, uniformly over bounded lockstep offsets; certify source-specific parameters.",
+  "scope_change_reason": "Handoff-first selection: #4467 explicitly leaves its saturation conjecture unproved. This is a historical source-specific asymptotic obligation, rather than a new selected supplier invoice audit. Complete live overlap found no later proof; priority revision8 and selected6030 are retained as context.",
+  "bottleneck_link": "Settles whether deeper repetition of this fixed direct-flow leaf law can yield unbounded leaf log-depth; does not transfer a historical cap to the current supplier.",
+  "budget_minutes": 90,
+  "stop_rule": "Stop after a source-bound saturation proof and certified hypotheses. No stable-share theorem, finite-G rate, whole-flow ceiling, supplier admission or construction search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, RESULT.json, independent_source.py, test_enclosures.py, REVIEW.md, CLAUDE-RESPONSE.md and VALIDATION.md.",
+  "author": "DLamdata",
+  "ai_assistance": "Substantial OpenAI Codex assistance, including two separate native AI agents for independent derivation/source checks and skeptical review. No human or proof-kernel verification.",
+  "open_questions": [
+    {
+      "question": "Give an explicit finite-G error bound for the conditional mean and its uniformity over level offsets.",
+      "why_it_matters": "The theorem proves a limit but does not certify the predecessor's astronomical finite-rank extrapolations.",
+      "first_step": "Derive a quantitative interval local limit estimate for this fixed log-rank law and combine it with the exponential tail bound in PROOF.md \u00a74.",
+      "blocked_by": "The qualitative Stone theorem has no certified error constants or effective onset in this package."
+    },
+    {
+      "question": "Determine the source, boundary and leaf potential shares in the entire fixed direct flow and use the exact refined-induction ratio.",
+      "why_it_matters": "Leaf saturation alone does not prove the predecessor's suggested total log-gap or numerical exponent ceiling.",
+      "first_step": "Analyze the original #4436 source/boundary sums at the same bounded level offset, preserving all terms.",
+      "blocked_by": "No uniform share limit or exact-ratio asymptotic is established here."
+    }
+  ]
+}
diff --git a/research/direct-flow-leaf-saturation/VALIDATION.md b/research/direct-flow-leaf-saturation/VALIDATION.md
new file mode 100644
index 0000000000..cda10273f7
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/VALIDATION.md
@@ -0,0 +1,140 @@
+# Validation and reproducibility
+
+## Current evidence index
+
+The current hashes, exact commands, stdout/stderr and results are in [followup-validation.json](logs/followup-validation.json). This follow-up to `9946b1c42466ada889c10cd0cea7522d6360a63b` corrects one explanatory Stone paragraph, adds a semantic mutation for the original #4436 comparison, and updates its verification description. The numerical certificate, source checker, enclosure oracle, RESULT.json and SOURCES.json are unchanged. The theorem and its argument are unchanged.
+
+| Evidence | Receipt | Scope |
+| --- | --- | --- |
+| Registered replay and metadata | [current run record](logs/followup-validation.json) | All four registered commands, with the new #4436 control; source hashes identify the executed bytes. |
+| Optimized mutation controls and deleted-comparison attack | [current run record](logs/followup-validation.json) | A one-count returned-histogram mutation must reach the original-Flow comparison. Removing that comparison makes the control fail; normal and optimized modes are distinguished in the record. |
+| Independent rational enclosures | [normal receipt](logs/claude-enclosures-normal.json), [optimized receipt](logs/claude-enclosures-optimized.json) | Unchanged verifier/oracle bytes; 16 log and 127 exp arguments. The current registered run also repeats the normal oracle check. |
+| Committed export and Git-free changed-control replay | [current run record](logs/followup-validation.json) | The changed mutation suite is replayed from an exported tree without Git. Earlier full export replays remain evidence for unchanged direct entry points. |
+| Written theorem and review | [PROOF.md](PROOF.md), [review findings](REVIEW.md) | Scoped analytic argument with Stone's theorem as an external input; corrected prose makes no quantitative-rate claim. |
+
+The registered replay passed in 75.175 s and metadata in 0.300 s. The isolated mutation suite passed in normal/optimized modes in 31.698/31.589 s; deleting only the original-Flow comparison caused the intended control failure in 1.439/1.541 s. Both positive independent-source baselines passed. All five unchanged numerical/source files were compared byte-for-byte with `6310550e`; the proof differs in exactly one explanatory paragraph. Internal review found no unresolved blocker. At scientific follow-up commit `309eff43c247b711026eda5e5629409a89ff6242`, committed-byte/source-history and official export/check commands passed for 47 package/input files. The changed mutation suite then passed in isolated optimized mode without Git in 33.424 s; all 48 exported files, including the export manifest, remained byte-identical. The subsequent evidence commit adds only this record and the consolidated log, without changing scientific files.
+
+`followup-validation.json` is the current response record. The `claude-` receipts below identify the first response at `553198839618962e07519b51cb3bbe808ca6f1dc`; they do not exercise the new #4436 mutation. Unprefixed receipts identify the initial `ff365dba` evidence. Earlier numerical receipts still apply where their scientific hashes match unchanged files; historical proof/control hashes must not be mistaken for current hashes. No original receipt was replaced.
+
+Base and last upstream refresh: `721c03822c421b7f7fcbb2598993b947c4d88419`, 2026-10-28. Priority revision 8. The branch adds only `research/direct-flow-leaf-saturation/`; frozen predecessors and the selected record are unchanged.
+
+## Reproduction and evidence reuse
+
+Python 3.12, standard library only. From the repository root, run the four checks serially with the registered entry point (observed total about 75 seconds):
+
+```sh
+python3.12 -B scripts/research_package.py --package research/direct-flow-leaf-saturation
+```
+
+The runner enforces Python 3.12; a default `python3` selecting 3.13 fails its version gate. For an exported tree without Git, run these direct commands from the export root:
+
+```sh
+python3.12 -B research/direct-flow-leaf-saturation/verify.py --expect research/direct-flow-leaf-saturation/RESULT.json
+python3.12 -B research/direct-flow-leaf-saturation/independent_source.py
+python3.12 -B research/direct-flow-leaf-saturation/test_controls.py
+python3.12 -B research/direct-flow-leaf-saturation/test_enclosures.py
+```
+
+The JSON run manifests preserve the additional optimized-mode commands actually executed. Metadata-only validation uses the registered command with `--check-only`; it does not execute the mathematical checks.
+
+Reusing these receipts requires matching the scientific hashes and predecessor pins. Changes to the proof require renewed argument review; changes to code, numerical data or inputs require the affected numerical/source checks and updated receipts. Documentation-only navigation edits require link, claim-consistency and metadata checks plus confirmation that the scientific bytes remain unchanged. Export checks establish availability and integrity; they do not prove the theorem.
+
+## First review response: historical validation
+
+The first response addressed the six findings on `ff365dba6911ce615bec76e8d1f149faf1fe16ca`; [REVIEW.md](REVIEW.md#claude-review-findings) maps scope and evidence. All `RESULT.json.parameters` values compare exactly equal to that snapshot. The receipt's source-check labels changed to report histogram equality and fixture sensitivity accurately. The finite source domains remain G≤3.
+
+The following Python 3.12 runs all exited 0. Commands, environment and final scientific-source hashes are in [logs/claude-validation.json](logs/claude-validation.json):
+
+| Check | Seconds | Output |
+| --- | --- | --- |
+| metadata | 0.282 | [log](logs/claude-metadata.log) |
+| registered | 75.068 | [log](logs/claude-registered.log) |
+| optimized | 14.372 | [log](logs/claude-optimized.log) |
+| independent-optimized | 0.155 | [log](logs/claude-independent-optimized.log) |
+| mutations-optimized | 30.389 | [log](logs/claude-mutations-optimized.log) |
+
+The first response expanded the registered replay to four commands, including the independent rational enclosure test. Normal and optimized oracle checks additionally passed in 28.674 s and 27.920 s with identical receipts; [timings](logs/claude-enclosures-timing.json), [normal receipt](logs/claude-enclosures-normal.json), [optimized receipt](logs/claude-enclosures-optimized.json). They cover 16 integer logarithm arguments and 127 distinct rational exponential arguments, and reject all three reported remainder faults. Their receipts identify the loaded verifier SHA and exact argument-domain digest. This independently certifies finite-domain enclosure containment, not all-input correctness or the asymptotic theorem.
+
+Both standalone source checkers reject altered source bytes. In this first response, re-pinned empty and terminal-truncated #4467 branches were rejected by the #4467 histogram comparisons, in normal and optimized modes; this evidence did not guard the original #4436 comparison. This separates source semantics from checksum failures and from fixture sensitivity. Fixed-root-bracket and corrupted-receipt controls remain separately labelled.
+
+The final internal review found no blocking issue in the updated proof, source binding, mutation tests or oracle mathematics. Primary numerical functions were compared by AST against the reviewed snapshot and are unchanged; only `finite_law` changed in verify.py. The oracle's last change adds the loaded source SHA to its receipt and was separately reviewed. The earlier README's “adds eight”→“checks eight” wording avoids implying eighteen distinct source ranks; this prose-only change affects no evidence.
+
+## First response: committed export and Git-free replay
+
+Scientific follow-up commit: `553198839618962e07519b51cb3bbe808ca6f1dc`. Committed-byte comparison with `--check-source-history` passed for all 41 package/input files, with the original base as the source-history ancestor. The official exporter and archive check both reported `PASS_RESEARCH_EXPORT` for those 41 files:
+
+```sh
+python3.12 -B scripts/check_research_commit.py --package research/direct-flow-leaf-saturation --check-source-history
+python3.12 -B scripts/export_research_package.py export --package research/direct-flow-leaf-saturation --ref 553198839618962e07519b51cb3bbe808ca6f1dc --output /tmp/leaf-saturation-reviewed.tar
+python3.12 -B scripts/export_research_package.py check /tmp/leaf-saturation-reviewed.tar
+```
+
+The archive was extracted into a fresh directory, using an absolute Python 3.12 executable with PATH set to an empty directory and no Git available. All four direct commands passed: primary certificate 15.962 s, independent source checker 0.090 s, mutation controls 31.220 s, and independent enclosure checks 28.117 s. [logs/claude-portable-results.json](logs/claude-portable-results.json) records exact commands, exit codes and links to their logs. The scientific bytes are exactly the commit above; the subsequent evidence commit adds only these logs, this validation record and model attribution. Final publication-byte and export checks are repeated after that evidence commit.
+
+Pre-publication refresh at 2026-10-28T12:34:31Z found canonical main unchanged at `721c03822c421b7f7fcbb2598993b947c4d88419` and no guidance/priority change. A bounded live check of the 100 most recently updated PRs (all states) and 100 Discussions reached back to October 28 00:24Z and October 25 03:58Z respectively, overlapping the earlier complete body snapshots. Exact predecessor and saturation-term checks found no new competing saturation result; this is body-level coverage, not a claim to have reviewed every diff or reply. Existing #6118 was confirmed open and draft before the update.
+
+## Historical documentation consolidation checks
+
+The documentation commit `9946b1c42466ada889c10cd0cea7522d6360a63b`, following `6310550e932de70243fc2aaab6f4885688b6fe21`, changed only README.md, REVIEW.md, CLAUDE-RESPONSE.md and this file. A Python 3.12 link/anchor scan passed all 56 relative links in those documents. SHA256 checks matched all eight scientific files to `logs/claude-validation.json` and `553198839618962e07519b51cb3bbe808ca6f1dc`; byte comparisons confirmed all 28 logs unchanged from `6310550e`. Package metadata/source pins and `git diff --check` passed. Independent AI documentation review preserved the original limitations and corrected wording that had overstated the executed drift controls. Positive drift is certified; no nonpositive-drift test is claimed.
+
+No scientific replay was rerun for this documentation-only change; the then-current scientific receipts applied to identical bytes at `9946b1c`. The later Stone/control response is indexed separately above. Committed-byte/source-history and export checks are performed on the documentation commit before publication. Reproduce the metadata and committed-byte checks with:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/direct-flow-leaf-saturation --check-only
+python3.12 -B scripts/check_research_commit.py --package research/direct-flow-leaf-saturation --check-source-history
+```
+
+## Hosted CI
+
+The previously opened draft #6118's hosted run at `ff365dba` had a failed planning job and skipped replay. Its [actual job log](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40681403297/job/122792722146) reports two failures in `test_research_current_status`: the old selected-family CI text and an exact bold-value match. The shared files involved are unchanged from base. This is separate from the passing package replay; no unrelated suite or shared documentation repair was added here. The subsequent run at `6310550e932de70243fc2aaab6f4885688b6fe21` has the same two failing tests and skipped replay, confirmed from its [job log](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40689120787/job/122819086604): 678 tests, two failures, 23 skips. These are pinned historical statuses; consult #6118 for later heads.
+
+## Historical validation
+
+The remaining records describe the initial `ff365dba6911ce615bec76e8d1f149faf1fe16ca` contribution. Numerical parameter intervals remain unchanged, but these older receipts predate the source-check and remainder-control improvements.
+
+### Initial local evidence actually run
+
+Environment: 3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]; Linux-6.18.55-x86_64-with-glibc2.41. Standard library only. The retained environment was activated in the isolated contribution worktree. No dependencies were installed.
+
+The exact commands, elapsed seconds, return codes, and final scientific-file hashes are in [logs/validation.json](logs/validation.json). All commands below exited 0:
+
+| Check | Exit | Seconds | Output |
+| --- | --- | --- | --- |
+| metadata | 0 | 0.207 | [log](logs/metadata.log) |
+| primary | 0 | 15.394 | [log](logs/primary.log) |
+| optimized | 0 | 16.419 | [log](logs/optimized.log) |
+| independent | 0 | 0.098 | [log](logs/independent.log) |
+| independent-optimized | 0 | 0.169 | [log](logs/independent-optimized.log) |
+| mutations | 0 | 30.049 | [log](logs/mutations.log) |
+| mutations-optimized | 0 | 30.11 | [log](logs/mutations-optimized.log) |
+| registered | 0 | 43.277 | [log](logs/registered.log) |
+
+Primary and optimized outputs match RESULT.json exactly. The two independent source runs cover ten exact fixtures and reject outgoing-rank truncation. Mutation controls reject altered input bytes in normal/optimized modes, a corrupted receipt under optimized Python, and +1 paid/target multiplicity changes. The registered replay runs all three commands serially and passes; metadata validation is separate from the mathematical proof.
+
+The final proof's reference spelling and canonical Discussion link were normalized after these runs; these prose-only edits change no numerical input or mathematical statement. The scientific hash inventory records the final proof bytes and states that adjustment. The full source root monotonicity bound, corrected citation, independent source integration and mutation controls were already present for these runs.
+
+### Freshness and overlap
+
+Canonical upstream was fetched before selection and again before packaging; both fetched SHAs equal the base above, so no rebase or scientific-source migration was needed. Final cached body refresh: open PRs 2026-10-28T11:20:57Z (376 records), Discussions 2026-10-28T11:22:05Z (5,771 records), complete pagination with no warnings. The earlier closed/merged snapshot at 11:11:49Z has 5,222 records. All 8,348 tracked local note paths were searched; the new package adds two notes. No additional saturation proof was found. A separate live read confirmed the user's [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19240402). Searches cover bodies and local top-level notes, not every diff or historical source.
+
+### Verification scope
+
+The finite verifier certifies source bindings, rational numerical hypotheses, and semantic controls. The asymptotic argument is the written PROOF.md using the explicitly stated classical interval local-limit theorem. Internal AI reviewers found no unresolved mathematical blocker; REVIEW.md records corrections, final integration and shared dependencies.
+
+No selected-construction replay, `make verify`, historical heavy suite, Lean, or Docker run is applicable to this isolated package. Explicit finite-depth bounds, stable whole-flow shares, the exact refined-induction ceiling, supplier admission, and all five selected framework assumptions remain unrun/unresolved here. Hosted CI is separate; consult the contribution PR for its actual status.
+
+### Initial committed bytes and portable replay
+
+At scientific commit `9465f263a673d2d86e7262523cbeb0e796f486cf`, the following commands passed on all 26 package/input files:
+
+```sh
+python3 -B scripts/check_research_commit.py --package research/direct-flow-leaf-saturation --check-source-history
+python3 -B scripts/export_research_package.py export --package research/direct-flow-leaf-saturation --ref 9465f263a673d2d86e7262523cbeb0e796f486cf --output /tmp/leaf-saturation.tar
+python3 -B scripts/export_research_package.py check /tmp/leaf-saturation.tar
+```
+
+The actual temporary archive path was outside the repository; `/tmp/leaf-saturation.tar` above is the portable equivalent. Both exporter commands reported `PASS_RESEARCH_EXPORT`. Committed-byte comparison reported `PASS_RESEARCH_COMMIT_BYTES`, with source-history commit `721c03822c421b7f7fcbb2598993b947c4d88419`.
+
+After extraction into a fresh directory, with PATH pointing to an empty directory and no Git available, all three direct package commands passed: main verifier 14.383 s, independent source checker 0.094 s, mutation controls 28.189 s. [logs/portable-results.json](logs/portable-results.json) records the actual commands, exits and logs. Their source bytes are exactly the scientific commit above; subsequent packaging adds these logs and this record without changing the proof or checker.
+
+These checks establish committed-source availability, transport integrity and portable replay. They do not prove the analytic theorem. Final publication-byte preflight is repeated after recording this evidence; the PR pins the final contribution SHA.
diff --git a/research/direct-flow-leaf-saturation/VERIFY.json b/research/direct-flow-leaf-saturation/VERIFY.json
new file mode 100644
index 0000000000..12a862ef59
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/VERIFY.json
@@ -0,0 +1,53 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/direct-flow-leaf-walk/README.md",
+    "research/direct-flow-leaf-walk/diagnostics/overlap_flow.py",
+    "research/direct-flow-leaf-walk/verify.py",
+    "research/direct-mixed-flow/flow.py",
+    "research/direct-mixed-flow/vendor/p7-RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py",
+        "--expect",
+        "{package}/RESULT.json"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact rational root/drift/tilt/limit enclosures, eight whole-flow fixtures, lattice and domain failure controls; classical LLT proof is written, not machine-checked."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/independent_source.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Ten independent ordered-word fixtures compare complete #4436 and #4467 leaf histograms after authenticating every input; terminal-cut fields describe fixture sensitivity."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_controls.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Reject altered bytes in both standalone entry points; re-pinned empty/truncated #4467 branches and altered #4436 returned histogram rejected by their comparisons in normal and optimized modes; fixed-bracket and receipt regressions."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_enclosures.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent exact rational bounds at every executed log/exp argument; reject zero logarithm/exponential tails and invalid exponential remainder majorant."
+    }
+  ]
+}
diff --git a/research/direct-flow-leaf-saturation/independent_source.py b/research/direct-flow-leaf-saturation/independent_source.py
new file mode 100644
index 0000000000..14c045c668
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/independent_source.py
@@ -0,0 +1,38 @@
+"""Independent source audit. DLamdata with OpenAI Codex assistance; Apache-2.0."""
+import importlib.util, pathlib, collections, itertools, math, json, hashlib
+ROOT=pathlib.Path(__file__).resolve().parents[2]
+def need(ok, message):
+ if not ok: raise ValueError(message)
+# Authenticate every declared live input before executing either predecessor.
+# This is independent of the primary verifier and also works without Git.
+manifest=json.loads((pathlib.Path(__file__).resolve().parent/'SOURCES.json').read_text())
+for row in manifest['files']:
+ if row['usage']=='input':
+  need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'], 'source mismatch: '+row['path'])
+def load(relative,name):
+ s=importlib.util.spec_from_file_location(name,ROOT/relative);m=importlib.util.module_from_spec(s);s.loader.exec_module(m);return m
+old=load('research/direct-flow-leaf-walk/diagnostics/overlap_flow.py','audit_flow')
+walk=load('research/direct-flow-leaf-walk/verify.py','audit_walk')
+native=load('research/direct-mixed-flow/flow.py','native_flow')
+receipt=json.loads((ROOT/'research/direct-mixed-flow/vendor/p7-RESULT.json').read_text())['strictification']
+need({int(k):v for k,v in receipt['paid'].items()}==walk.P, 'paid source inventory')
+need({int(k):v for k,v in receipt['targets'].items()}==walk.W, 'target source inventory')
+rows=[]
+for N in [121,604,605,606,3024,3025,3026,15124,15125,15126]:
+ f=old.flow(N,walk.W,walk.P); G=f['G']
+ exact=collections.Counter()
+ for ranks in itertools.product(walk.P,repeat=G):
+  rho=math.prod(ranks)
+  if 121*rho>N:continue
+  multiplicity=math.prod(walk.P[r] for r in ranks)
+  for r,pr in walk.P.items():exact[r*rho]+=multiplicity*pr
+ leaf=collections.Counter(f['X']);leaf.subtract(f['BX']);leaf=+leaf
+ need(exact==leaf,(N,'leaf histogram'))
+ actual=native.Flow(walk.W,walk.P,N).merged()
+ other=actual['exits'].copy();other.subtract(actual['boundary_exits']);other=+other
+ need(other==exact,(N,'original Flow class'))
+ # Fixture sensitivity only; the source checks are exact==leaf and other==exact above.
+ wrong=collections.Counter({r:c for r,c in exact.items() if 121*r<=N})
+ need(wrong!=exact,(N,'fixture does not distinguish terminal truncation'))
+ rows.append({'N':N,'G':G,'leaf_ranks':len(exact),'terminal_cut_distinguished':True})
+print(json.dumps({'status':'PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION','fixtures':rows},indent=2))
diff --git a/research/direct-flow-leaf-saturation/logs/claude-enclosures-normal.json b/research/direct-flow-leaf-saturation/logs/claude-enclosures-normal.json
new file mode 100644
index 0000000000..22b2ef62f1
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-enclosures-normal.json
@@ -0,0 +1,33 @@
+{
+  "all_exp_arguments_below": "479/100",
+  "distinct_exp_rational_arguments": 127,
+  "domain_sha256": "5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4",
+  "exp_oracle": "degree-82 positive series; exact ratio-bounded geometric tail",
+  "log_integer_arguments": [
+    1,
+    2,
+    3,
+    4,
+    5,
+    6,
+    7,
+    8,
+    9,
+    16,
+    25,
+    32,
+    41,
+    48,
+    57,
+    121
+  ],
+  "log_oracle": "256-term -log(1-q) series; exact positive geometric tail",
+  "mutations_rejected": [
+    "zero_log_tail_at_log2",
+    "zero_exp_tail_at_exp1",
+    "invalid_exp_majorant_one_at_exp1"
+  ],
+  "production_source_sha256": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d",
+  "scope": "Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.",
+  "status": "PASS_INDEPENDENT_RATIONAL_ENCLOSURES"
+}
diff --git a/research/direct-flow-leaf-saturation/logs/claude-enclosures-optimized.json b/research/direct-flow-leaf-saturation/logs/claude-enclosures-optimized.json
new file mode 100644
index 0000000000..22b2ef62f1
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-enclosures-optimized.json
@@ -0,0 +1,33 @@
+{
+  "all_exp_arguments_below": "479/100",
+  "distinct_exp_rational_arguments": 127,
+  "domain_sha256": "5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4",
+  "exp_oracle": "degree-82 positive series; exact ratio-bounded geometric tail",
+  "log_integer_arguments": [
+    1,
+    2,
+    3,
+    4,
+    5,
+    6,
+    7,
+    8,
+    9,
+    16,
+    25,
+    32,
+    41,
+    48,
+    57,
+    121
+  ],
+  "log_oracle": "256-term -log(1-q) series; exact positive geometric tail",
+  "mutations_rejected": [
+    "zero_log_tail_at_log2",
+    "zero_exp_tail_at_exp1",
+    "invalid_exp_majorant_one_at_exp1"
+  ],
+  "production_source_sha256": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d",
+  "scope": "Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.",
+  "status": "PASS_INDEPENDENT_RATIONAL_ENCLOSURES"
+}
diff --git a/research/direct-flow-leaf-saturation/logs/claude-enclosures-timing.json b/research/direct-flow-leaf-saturation/logs/claude-enclosures-timing.json
new file mode 100644
index 0000000000..0035686976
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-enclosures-timing.json
@@ -0,0 +1,14 @@
+[
+  {
+    "mode": "normal",
+    "returncode": 0,
+    "elapsed_seconds": 28.674,
+    "max_rss_kib": 18612
+  },
+  {
+    "mode": "optimized",
+    "returncode": 0,
+    "elapsed_seconds": 27.92,
+    "max_rss_kib": 19620
+  }
+]
diff --git a/research/direct-flow-leaf-saturation/logs/claude-independent-optimized.log b/research/direct-flow-leaf-saturation/logs/claude-independent-optimized.log
new file mode 100644
index 0000000000..5f7f01fadc
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-independent-optimized.log
@@ -0,0 +1,65 @@
+{
+  "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION",
+  "fixtures": [
+    {
+      "N": 121,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 604,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 605,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 606,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 3024,
+      "G": 1,
+      "leaf_ranks": 30,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 3025,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 3026,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 15124,
+      "G": 2,
+      "leaf_ranks": 65,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 15125,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 15126,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_cut_distinguished": true
+    }
+  ]
+}
diff --git a/research/direct-flow-leaf-saturation/logs/claude-metadata.log b/research/direct-flow-leaf-saturation/logs/claude-metadata.log
new file mode 100644
index 0000000000..a6c9fb298a
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-metadata.log
@@ -0,0 +1 @@
+PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)
diff --git a/research/direct-flow-leaf-saturation/logs/claude-mutations-optimized.log b/research/direct-flow-leaf-saturation/logs/claude-mutations-optimized.log
new file mode 100644
index 0000000000..4a287e277c
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-mutations-optimized.log
@@ -0,0 +1 @@
+PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions
diff --git a/research/direct-flow-leaf-saturation/logs/claude-optimized.log b/research/direct-flow-leaf-saturation/logs/claude-optimized.log
new file mode 100644
index 0000000000..a799a944c4
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-optimized.log
@@ -0,0 +1,49 @@
+{
+  "controls": {
+    "interval_domain_rejections": 3,
+    "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1"
+  },
+  "finite_law": {
+    "ordered_word_max_depth": 3,
+    "source_check": "complete actual X-BX histogram equals ordered-word enumeration",
+    "terminal_cut_distinguishing_fixtures": 8,
+    "whole_flow_fixtures": 8
+  },
+  "parameters": {
+    "alpha": [
+      "0.98981438244597",
+      "0.98981438244599"
+    ],
+    "drift_above_log5": [
+      "0.016477707041",
+      "0.016477707042"
+    ],
+    "invoice_derivative_lower_bound_interval_0_99_to_1": [
+      "211661.930309",
+      "211661.930310"
+    ],
+    "lambda": [
+      "0.00749912850515",
+      "0.00749912850519"
+    ],
+    "mean_deficit_limit": [
+      "133.34882837",
+      "133.34882838"
+    ],
+    "mean_leaf_depth_limit": [
+      "136.51870330",
+      "136.51870331"
+    ],
+    "mean_log_rank": [
+      "1.625915619475",
+      "1.625915619476"
+    ],
+    "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds",
+    "t_star": [
+      "0.99731351095114",
+      "0.99731351095116"
+    ]
+  },
+  "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.",
+  "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS"
+}
diff --git a/research/direct-flow-leaf-saturation/logs/claude-portable-0.log b/research/direct-flow-leaf-saturation/logs/claude-portable-0.log
new file mode 100644
index 0000000000..a799a944c4
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-portable-0.log
@@ -0,0 +1,49 @@
+{
+  "controls": {
+    "interval_domain_rejections": 3,
+    "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1"
+  },
+  "finite_law": {
+    "ordered_word_max_depth": 3,
+    "source_check": "complete actual X-BX histogram equals ordered-word enumeration",
+    "terminal_cut_distinguishing_fixtures": 8,
+    "whole_flow_fixtures": 8
+  },
+  "parameters": {
+    "alpha": [
+      "0.98981438244597",
+      "0.98981438244599"
+    ],
+    "drift_above_log5": [
+      "0.016477707041",
+      "0.016477707042"
+    ],
+    "invoice_derivative_lower_bound_interval_0_99_to_1": [
+      "211661.930309",
+      "211661.930310"
+    ],
+    "lambda": [
+      "0.00749912850515",
+      "0.00749912850519"
+    ],
+    "mean_deficit_limit": [
+      "133.34882837",
+      "133.34882838"
+    ],
+    "mean_leaf_depth_limit": [
+      "136.51870330",
+      "136.51870331"
+    ],
+    "mean_log_rank": [
+      "1.625915619475",
+      "1.625915619476"
+    ],
+    "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds",
+    "t_star": [
+      "0.99731351095114",
+      "0.99731351095116"
+    ]
+  },
+  "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.",
+  "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS"
+}
diff --git a/research/direct-flow-leaf-saturation/logs/claude-portable-1.log b/research/direct-flow-leaf-saturation/logs/claude-portable-1.log
new file mode 100644
index 0000000000..5f7f01fadc
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-portable-1.log
@@ -0,0 +1,65 @@
+{
+  "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION",
+  "fixtures": [
+    {
+      "N": 121,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 604,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 605,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 606,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 3024,
+      "G": 1,
+      "leaf_ranks": 30,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 3025,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 3026,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 15124,
+      "G": 2,
+      "leaf_ranks": 65,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 15125,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 15126,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_cut_distinguished": true
+    }
+  ]
+}
diff --git a/research/direct-flow-leaf-saturation/logs/claude-portable-2.log b/research/direct-flow-leaf-saturation/logs/claude-portable-2.log
new file mode 100644
index 0000000000..4a287e277c
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-portable-2.log
@@ -0,0 +1 @@
+PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions
diff --git a/research/direct-flow-leaf-saturation/logs/claude-portable-3.log b/research/direct-flow-leaf-saturation/logs/claude-portable-3.log
new file mode 100644
index 0000000000..22b2ef62f1
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-portable-3.log
@@ -0,0 +1,33 @@
+{
+  "all_exp_arguments_below": "479/100",
+  "distinct_exp_rational_arguments": 127,
+  "domain_sha256": "5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4",
+  "exp_oracle": "degree-82 positive series; exact ratio-bounded geometric tail",
+  "log_integer_arguments": [
+    1,
+    2,
+    3,
+    4,
+    5,
+    6,
+    7,
+    8,
+    9,
+    16,
+    25,
+    32,
+    41,
+    48,
+    57,
+    121
+  ],
+  "log_oracle": "256-term -log(1-q) series; exact positive geometric tail",
+  "mutations_rejected": [
+    "zero_log_tail_at_log2",
+    "zero_exp_tail_at_exp1",
+    "invalid_exp_majorant_one_at_exp1"
+  ],
+  "production_source_sha256": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d",
+  "scope": "Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.",
+  "status": "PASS_INDEPENDENT_RATIONAL_ENCLOSURES"
+}
diff --git a/research/direct-flow-leaf-saturation/logs/claude-portable-results.json b/research/direct-flow-leaf-saturation/logs/claude-portable-results.json
new file mode 100644
index 0000000000..4575d9dc68
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-portable-results.json
@@ -0,0 +1,49 @@
+{
+  "export_commit": "553198839618962e07519b51cb3bbe808ca6f1dc",
+  "git_available": false,
+  "path": "empty directory",
+  "runs": [
+    {
+      "command": [
+        "python3.12",
+        "-B",
+        "research/direct-flow-leaf-saturation/verify.py",
+        "--expect",
+        "research/direct-flow-leaf-saturation/RESULT.json"
+      ],
+      "exit_code": 0,
+      "seconds": 15.962,
+      "log": "logs/claude-portable-0.log"
+    },
+    {
+      "command": [
+        "python3.12",
+        "-B",
+        "research/direct-flow-leaf-saturation/independent_source.py"
+      ],
+      "exit_code": 0,
+      "seconds": 0.09,
+      "log": "logs/claude-portable-1.log"
+    },
+    {
+      "command": [
+        "python3.12",
+        "-B",
+        "research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "exit_code": 0,
+      "seconds": 31.22,
+      "log": "logs/claude-portable-2.log"
+    },
+    {
+      "command": [
+        "python3.12",
+        "-B",
+        "research/direct-flow-leaf-saturation/test_enclosures.py"
+      ],
+      "exit_code": 0,
+      "seconds": 28.117,
+      "log": "logs/claude-portable-3.log"
+    }
+  ]
+}
diff --git a/research/direct-flow-leaf-saturation/logs/claude-registered.log b/research/direct-flow-leaf-saturation/logs/claude-registered.log
new file mode 100644
index 0000000000..0aeabff141
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-registered.log
@@ -0,0 +1,153 @@
+CHECK Exact rational root/drift/tilt/limit enclosures, eight whole-flow fixtures, lattice and domain failure controls; classical LLT proof is written, not machine-checked.
+{
+  "controls": {
+    "interval_domain_rejections": 3,
+    "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1"
+  },
+  "finite_law": {
+    "ordered_word_max_depth": 3,
+    "source_check": "complete actual X-BX histogram equals ordered-word enumeration",
+    "terminal_cut_distinguishing_fixtures": 8,
+    "whole_flow_fixtures": 8
+  },
+  "parameters": {
+    "alpha": [
+      "0.98981438244597",
+      "0.98981438244599"
+    ],
+    "drift_above_log5": [
+      "0.016477707041",
+      "0.016477707042"
+    ],
+    "invoice_derivative_lower_bound_interval_0_99_to_1": [
+      "211661.930309",
+      "211661.930310"
+    ],
+    "lambda": [
+      "0.00749912850515",
+      "0.00749912850519"
+    ],
+    "mean_deficit_limit": [
+      "133.34882837",
+      "133.34882838"
+    ],
+    "mean_leaf_depth_limit": [
+      "136.51870330",
+      "136.51870331"
+    ],
+    "mean_log_rank": [
+      "1.625915619475",
+      "1.625915619476"
+    ],
+    "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds",
+    "t_star": [
+      "0.99731351095114",
+      "0.99731351095116"
+    ]
+  },
+  "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.",
+  "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS"
+}
+CHECK Ten independent ordered-word fixtures compare complete #4436 and #4467 leaf histograms after authenticating every input; terminal-cut fields describe fixture sensitivity.
+{
+  "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION",
+  "fixtures": [
+    {
+      "N": 121,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 604,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 605,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 606,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 3024,
+      "G": 1,
+      "leaf_ranks": 30,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 3025,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 3026,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 15124,
+      "G": 2,
+      "leaf_ranks": 65,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 15125,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_cut_distinguished": true
+    },
+    {
+      "N": 15126,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_cut_distinguished": true
+    }
+  ]
+}
+CHECK Reject altered bytes in both standalone entry points; re-pinned empty/truncated source branches rejected semantically in normal and optimized modes; fixed-bracket and receipt regressions.
+PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions
+CHECK Independent exact rational bounds at every executed log/exp argument; reject zero logarithm/exponential tails and invalid exponential remainder majorant.
+{
+  "all_exp_arguments_below": "479/100",
+  "distinct_exp_rational_arguments": 127,
+  "domain_sha256": "5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4",
+  "exp_oracle": "degree-82 positive series; exact ratio-bounded geometric tail",
+  "log_integer_arguments": [
+    1,
+    2,
+    3,
+    4,
+    5,
+    6,
+    7,
+    8,
+    9,
+    16,
+    25,
+    32,
+    41,
+    48,
+    57,
+    121
+  ],
+  "log_oracle": "256-term -log(1-q) series; exact positive geometric tail",
+  "mutations_rejected": [
+    "zero_log_tail_at_log2",
+    "zero_exp_tail_at_exp1",
+    "invalid_exp_majorant_one_at_exp1"
+  ],
+  "production_source_sha256": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d",
+  "scope": "Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.",
+  "status": "PASS_INDEPENDENT_RATIONAL_ENCLOSURES"
+}
+PASS_REGISTERED_RESEARCH_PACKAGE research/direct-flow-leaf-saturation outcome=completed
diff --git a/research/direct-flow-leaf-saturation/logs/claude-validation.json b/research/direct-flow-leaf-saturation/logs/claude-validation.json
new file mode 100644
index 0000000000..a83289ceb0
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/claude-validation.json
@@ -0,0 +1,84 @@
+{
+  "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]",
+  "platform": "Linux-6.18.55-x86_64-with-glibc2.41",
+  "reviewed_predecessor": "ff365dba6911ce615bec76e8d1f149faf1fe16ca",
+  "upstream": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "runs": [
+    {
+      "name": "metadata",
+      "command": [
+        "python3.12",
+        "-B",
+        "scripts/research_package.py",
+        "--package",
+        "research/direct-flow-leaf-saturation",
+        "--check-only"
+      ],
+      "exit_code": 0,
+      "seconds": 0.282,
+      "log": "logs/claude-metadata.log"
+    },
+    {
+      "name": "registered",
+      "command": [
+        "python3.12",
+        "-B",
+        "scripts/research_package.py",
+        "--package",
+        "research/direct-flow-leaf-saturation"
+      ],
+      "exit_code": 0,
+      "seconds": 75.068,
+      "log": "logs/claude-registered.log"
+    },
+    {
+      "name": "optimized",
+      "command": [
+        "python3.12",
+        "-B",
+        "-O",
+        "research/direct-flow-leaf-saturation/verify.py",
+        "--expect",
+        "research/direct-flow-leaf-saturation/RESULT.json"
+      ],
+      "exit_code": 0,
+      "seconds": 14.372,
+      "log": "logs/claude-optimized.log"
+    },
+    {
+      "name": "independent-optimized",
+      "command": [
+        "python3.12",
+        "-B",
+        "-O",
+        "research/direct-flow-leaf-saturation/independent_source.py"
+      ],
+      "exit_code": 0,
+      "seconds": 0.155,
+      "log": "logs/claude-independent-optimized.log"
+    },
+    {
+      "name": "mutations-optimized",
+      "command": [
+        "python3.12",
+        "-B",
+        "-O",
+        "research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "exit_code": 0,
+      "seconds": 30.389,
+      "log": "logs/claude-mutations-optimized.log"
+    }
+  ],
+  "enclosure_agent_runs": "logs/claude-enclosures-timing.json",
+  "scientific_files_sha256": {
+    "PROOF.md": "09dc0d6fd22b5e502b812543ddf78395ab7deacc894cd52430709475acfb2978",
+    "verify.py": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d",
+    "RESULT.json": "d195c3fd5620bf2e64dc7d677c79ad52e780aefde9534d4e6a02a5ff1b9c9bdd",
+    "independent_source.py": "abe248ffc0012fdcb7a941c399cba0f5f943c006d86368553c1c3317442f5773",
+    "test_controls.py": "ff4e4b8b8a34416b6e93a32ab2afbdd3733ce6e730a0df51a946d47b4a3836a5",
+    "test_enclosures.py": "b92a75601ef676ab0b412395eb2ccaa52c8e802f89fe1fb2f3820cafa173aea4",
+    "SOURCES.json": "90997ec1be8cd8c3e588d71a349783b2f1696a224dc082749f3886bebd8c2c4a",
+    "VERIFY.json": "07b8cf8da544a3049f817664381b3d26b3c5e35454ce2e308cfa41a6f3e76663"
+  }
+}
diff --git a/research/direct-flow-leaf-saturation/logs/followup-validation.json b/research/direct-flow-leaf-saturation/logs/followup-validation.json
new file mode 100644
index 0000000000..bdfa91cfc1
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/followup-validation.json
@@ -0,0 +1,226 @@
+{
+  "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]",
+  "platform": "Linux-6.18.55-x86_64-with-glibc2.41",
+  "reviewed_snapshot": "6310550e932de70243fc2aaab6f4885688b6fe21",
+  "starting_head": "9946b1c42466ada889c10cd0cea7522d6360a63b",
+  "base": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "scientific_files_sha256": {
+    "PROOF.md": "6e32d89065b5fb14c457fa990a166f68c840ec16566c480000dc620ad842aa4e",
+    "verify.py": "3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d",
+    "RESULT.json": "d195c3fd5620bf2e64dc7d677c79ad52e780aefde9534d4e6a02a5ff1b9c9bdd",
+    "independent_source.py": "abe248ffc0012fdcb7a941c399cba0f5f943c006d86368553c1c3317442f5773",
+    "test_controls.py": "7039979fb32e410470bc5d2cd664c519cca2d0924b8e461b9290662b9b31fbb9",
+    "test_enclosures.py": "b92a75601ef676ab0b412395eb2ccaa52c8e802f89fe1fb2f3820cafa173aea4",
+    "SOURCES.json": "90997ec1be8cd8c3e588d71a349783b2f1696a224dc082749f3886bebd8c2c4a",
+    "VERIFY.json": "9c007727bbd9b0128e25d8394d40b60047f132b4d954b7eea974653de89b83f2"
+  },
+  "runs": [
+    {
+      "name": "metadata",
+      "command": [
+        "/workspace/integer-mult-bounds/.venv/bin/python",
+        "-B",
+        "scripts/research_package.py",
+        "--package",
+        "research/direct-flow-leaf-saturation",
+        "--check-only"
+      ],
+      "reproduce": [
+        "python3.12",
+        "-B",
+        "scripts/research_package.py",
+        "--package",
+        "research/direct-flow-leaf-saturation",
+        "--check-only"
+      ],
+      "exit_code": 0,
+      "seconds": 0.3,
+      "stdout": "PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)\n",
+      "stderr": ""
+    },
+    {
+      "name": "registered",
+      "command": [
+        "/workspace/integer-mult-bounds/.venv/bin/python",
+        "-B",
+        "scripts/research_package.py",
+        "--package",
+        "research/direct-flow-leaf-saturation"
+      ],
+      "reproduce": [
+        "python3.12",
+        "-B",
+        "scripts/research_package.py",
+        "--package",
+        "research/direct-flow-leaf-saturation"
+      ],
+      "exit_code": 0,
+      "seconds": 75.175,
+      "stdout": "CHECK Exact rational root/drift/tilt/limit enclosures, eight whole-flow fixtures, lattice and domain failure controls; classical LLT proof is written, not machine-checked.\n{\n  \"controls\": {\n    \"interval_domain_rejections\": 3,\n    \"lattice_countermodel\": \"geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1\"\n  },\n  \"finite_law\": {\n    \"ordered_word_max_depth\": 3,\n    \"source_check\": \"complete actual X-BX histogram equals ordered-word enumeration\",\n    \"terminal_cut_distinguishing_fixtures\": 8,\n    \"whole_flow_fixtures\": 8\n  },\n  \"parameters\": {\n    \"alpha\": [\n      \"0.98981438244597\",\n      \"0.98981438244599\"\n    ],\n    \"drift_above_log5\": [\n      \"0.016477707041\",\n      \"0.016477707042\"\n    ],\n    \"invoice_derivative_lower_bound_interval_0_99_to_1\": [\n      \"211661.930309\",\n      \"211661.930310\"\n    ],\n    \"lambda\": [\n      \"0.00749912850515\",\n      \"0.00749912850519\"\n    ],\n    \"mean_deficit_limit\": [\n      \"133.34882837\",\n      \"133.34882838\"\n    ],\n    \"mean_leaf_depth_limit\": [\n      \"136.51870330\",\n      \"136.51870331\"\n    ],\n    \"mean_log_rank\": [\n      \"1.625915619475\",\n      \"1.625915619476\"\n    ],\n    \"method\": \"exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds\",\n    \"t_star\": [\n      \"0.99731351095114\",\n      \"0.99731351095116\"\n    ]\n  },\n  \"scope\": \"Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.\",\n  \"status\": \"PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS\"\n}\nCHECK Ten independent ordered-word fixtures compare complete #4436 and #4467 leaf histograms after authenticating every input; terminal-cut fields describe fixture sensitivity.\n{\n  \"status\": \"PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION\",\n  \"fixtures\": [\n    {\n      \"N\": 121,\n      \"G\": 0,\n      \"leaf_ranks\": 9,\n      \"terminal_cut_distinguished\": true\n    },\n    {\n      \"N\": 604,\n      \"G\": 0,\n      \"leaf_ranks\": 9,\n      \"terminal_cut_distinguished\": true\n    },\n    {\n      \"N\": 605,\n      \"G\": 1,\n      \"leaf_ranks\": 26,\n      \"terminal_cut_distinguished\": true\n    },\n    {\n      \"N\": 606,\n      \"G\": 1,\n      \"leaf_ranks\": 26,\n      \"terminal_cut_distinguished\": true\n    },\n    {\n      \"N\": 3024,\n      \"G\": 1,\n      \"leaf_ranks\": 30,\n      \"terminal_cut_distinguished\": true\n    },\n    {\n      \"N\": 3025,\n      \"G\": 2,\n      \"leaf_ranks\": 55,\n      \"terminal_cut_distinguished\": true\n    },\n    {\n      \"N\": 3026,\n      \"G\": 2,\n      \"leaf_ranks\": 55,\n      \"terminal_cut_distinguished\": true\n    },\n    {\n      \"N\": 15124,\n      \"G\": 2,\n      \"leaf_ranks\": 65,\n      \"terminal_cut_distinguished\": true\n    },\n    {\n      \"N\": 15125,\n      \"G\": 3,\n      \"leaf_ranks\": 98,\n      \"terminal_cut_distinguished\": true\n    },\n    {\n      \"N\": 15126,\n      \"G\": 3,\n      \"leaf_ranks\": 98,\n      \"terminal_cut_distinguished\": true\n    }\n  ]\n}\nCHECK Reject altered bytes in both standalone entry points; re-pinned empty/truncated #4467 branches and altered #4436 returned histogram rejected by their comparisons in normal and optimized modes; fixed-bracket and receipt regressions.\nPASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized repinned_original_flow_return_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions\nCHECK Independent exact rational bounds at every executed log/exp argument; reject zero logarithm/exponential tails and invalid exponential remainder majorant.\n{\n  \"all_exp_arguments_below\": \"479/100\",\n  \"distinct_exp_rational_arguments\": 127,\n  \"domain_sha256\": \"5e27ec5fc8e5fe372d5511730fd47d3d9acac76ae707221b11bfa99b963c58e4\",\n  \"exp_oracle\": \"degree-82 positive series; exact ratio-bounded geometric tail\",\n  \"log_integer_arguments\": [\n    1,\n    2,\n    3,\n    4,\n    5,\n    6,\n    7,\n    8,\n    9,\n    16,\n    25,\n    32,\n    41,\n    48,\n    57,\n    121\n  ],\n  \"log_oracle\": \"256-term -log(1-q) series; exact positive geometric tail\",\n  \"mutations_rejected\": [\n    \"zero_log_tail_at_log2\",\n    \"zero_exp_tail_at_exp1\",\n    \"invalid_exp_majorant_one_at_exp1\"\n  ],\n  \"production_source_sha256\": \"3a88ad1da0691afefead7d71c00ab4a51d547c770a40dc2e232c39dc02d8366d\",\n  \"scope\": \"Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.\",\n  \"status\": \"PASS_INDEPENDENT_RATIONAL_ENCLOSURES\"\n}\nPASS_REGISTERED_RESEARCH_PACKAGE research/direct-flow-leaf-saturation outcome=completed\n",
+      "stderr": ""
+    },
+    {
+      "name": "git-free-optimized-mutation-controls",
+      "export_commit": "309eff43c247b711026eda5e5629409a89ff6242",
+      "command": [
+        "/workspace/integer-mult-bounds/.venv/bin/python",
+        "-I",
+        "-O",
+        "-B",
+        "research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "reproduce": [
+        "python3.12",
+        "-I",
+        "-O",
+        "-B",
+        "research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "git_available": false,
+      "path": "empty directory",
+      "exit_code": 0,
+      "seconds": 33.424,
+      "stdout": "PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized repinned_original_flow_return_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions\n",
+      "stderr": "",
+      "exported_files_unchanged": 48
+    }
+  ],
+  "independent_guard_runs": [
+    {
+      "variant": "intact_comparison",
+      "mode": "normal",
+      "command": [
+        "/workspace/integer-mult-bounds/.venv/bin/python",
+        "-I",
+        "-B",
+        "/workspace/work/assignment-20261028/followup2-s7bzl6f4/research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "returncode": 0,
+      "elapsed_seconds": 31.698,
+      "result": "PASS_MUTATION_CONTROLS including intended original Flow comparison"
+    },
+    {
+      "variant": "intact_comparison",
+      "mode": "optimized",
+      "command": [
+        "/workspace/integer-mult-bounds/.venv/bin/python",
+        "-I",
+        "-O",
+        "-B",
+        "/workspace/work/assignment-20261028/followup2-s7bzl6f4/research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "returncode": 0,
+      "elapsed_seconds": 31.589,
+      "result": "PASS_MUTATION_CONTROLS including intended original Flow comparison"
+    },
+    {
+      "variant": "deleted_original_comparison",
+      "mode": "normal",
+      "command": [
+        "/workspace/integer-mult-bounds/.venv/bin/python",
+        "-I",
+        "-B",
+        "/workspace/work/assignment-20261028/followup2-l1jemiz6/research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "returncode": 1,
+      "elapsed_seconds": 1.439,
+      "result": "ValueError: control did not reject with \"(121, 'original Flow class')\": 0,"
+    },
+    {
+      "variant": "deleted_original_comparison",
+      "mode": "optimized",
+      "command": [
+        "/workspace/integer-mult-bounds/.venv/bin/python",
+        "-I",
+        "-O",
+        "-B",
+        "/workspace/work/assignment-20261028/followup2-l1jemiz6/research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "returncode": 1,
+      "elapsed_seconds": 1.541,
+      "result": "ValueError: control did not reject with \"(121, 'original Flow class')\": 0,"
+    }
+  ],
+  "independent_positive_runs": [
+    {
+      "command": [
+        "/workspace/integer-mult-bounds/.venv/bin/python",
+        "-I",
+        "-B",
+        "research/direct-flow-leaf-saturation/independent_source.py"
+      ],
+      "elapsed_seconds": 0.109,
+      "returncode": 0,
+      "status": "positive baseline passed"
+    },
+    {
+      "command": [
+        "/workspace/integer-mult-bounds/.venv/bin/python",
+        "-I",
+        "-O",
+        "-B",
+        "research/direct-flow-leaf-saturation/independent_source.py"
+      ],
+      "elapsed_seconds": 0.182,
+      "returncode": 0,
+      "status": "positive baseline passed"
+    }
+  ],
+  "guard_reproduction": {
+    "mirror": "Copy test_controls.py, verify.py, independent_source.py, SOURCES.json, RESULT.json and every usage=input source into a scratch root at their original relative paths.",
+    "deletion": "Delete exactly the line need(other==exact,(N,'original Flow class')) from the scratch independent_source.py, preserving all other statements.",
+    "commands": [
+      "python3.12 -I -B research/direct-flow-leaf-saturation/test_controls.py",
+      "python3.12 -I -O -B research/direct-flow-leaf-saturation/test_controls.py"
+    ],
+    "expected": "With comparison intact: exit0/PASS_MUTATION_CONTROLS. With it deleted: exit1 and control did not reject with original Flow class; its child had returned0."
+  },
+  "internal_review": {
+    "verdict": "No unresolved blocker in scoped fix.",
+    "scope": "Independent argument/code check of N121 rank1 37305-to-37304 returned-histogram mutation, re-pinning/restoration and comparison deletion; one-paragraph Stone wording correction; evidence/provenance limits.",
+    "primary_text": "Precise Stone (6)/(8) reading supplied by Claude Code follow-up; fresh internal primary-PDF retrieval unavailable.",
+    "ai_assistance": "OpenAI Codex (GPT-6 Astra); Claude Code (Opus 5.5) follow-up. No human or formal verification."
+  },
+  "committed_export": {
+    "commit": "309eff43c247b711026eda5e5629409a89ff6242",
+    "files_including_inputs": 47,
+    "source_history_ancestor": "721c03822c421b7f7fcbb2598993b947c4d88419",
+    "checks": [
+      "PASS_RESEARCH_COMMIT_BYTES --check-source-history",
+      "PASS_RESEARCH_EXPORT export",
+      "PASS_RESEARCH_EXPORT check"
+    ],
+    "reproduction": [
+      [
+        "python3.12",
+        "-B",
+        "scripts/check_research_commit.py",
+        "--package",
+        "research/direct-flow-leaf-saturation",
+        "--ref",
+        "309eff43c247b711026eda5e5629409a89ff6242",
+        "--check-source-history"
+      ],
+      [
+        "python3.12",
+        "-B",
+        "scripts/export_research_package.py",
+        "export",
+        "--package",
+        "research/direct-flow-leaf-saturation",
+        "--ref",
+        "309eff43c247b711026eda5e5629409a89ff6242",
+        "--output",
+        "/tmp/leaf-followup.tar"
+      ],
+      [
+        "python3.12",
+        "-B",
+        "scripts/export_research_package.py",
+        "check",
+        "/tmp/leaf-followup.tar"
+      ]
+    ],
+    "command_note": "Preflight ran at scientific HEAD309eff43c; export used --ref HEAD and a temporary archive outside the repository. Reproduction commands resolve that head explicitly and substitute /tmp for the archive path."
+  }
+}
diff --git a/research/direct-flow-leaf-saturation/logs/independent-optimized.log b/research/direct-flow-leaf-saturation/logs/independent-optimized.log
new file mode 100644
index 0000000000..f50d39a3e3
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/independent-optimized.log
@@ -0,0 +1,65 @@
+{
+  "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION",
+  "fixtures": [
+    {
+      "N": 121,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 604,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 605,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 606,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3024,
+      "G": 1,
+      "leaf_ranks": 30,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3025,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3026,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15124,
+      "G": 2,
+      "leaf_ranks": 65,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15125,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15126,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_truncation_rejected": true
+    }
+  ]
+}
diff --git a/research/direct-flow-leaf-saturation/logs/independent.log b/research/direct-flow-leaf-saturation/logs/independent.log
new file mode 100644
index 0000000000..f50d39a3e3
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/independent.log
@@ -0,0 +1,65 @@
+{
+  "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION",
+  "fixtures": [
+    {
+      "N": 121,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 604,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 605,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 606,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3024,
+      "G": 1,
+      "leaf_ranks": 30,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3025,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3026,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15124,
+      "G": 2,
+      "leaf_ranks": 65,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15125,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15126,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_truncation_rejected": true
+    }
+  ]
+}
diff --git a/research/direct-flow-leaf-saturation/logs/metadata-final.log b/research/direct-flow-leaf-saturation/logs/metadata-final.log
new file mode 100644
index 0000000000..a6c9fb298a
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/metadata-final.log
@@ -0,0 +1 @@
+PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)
diff --git a/research/direct-flow-leaf-saturation/logs/metadata.log b/research/direct-flow-leaf-saturation/logs/metadata.log
new file mode 100644
index 0000000000..a6c9fb298a
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/metadata.log
@@ -0,0 +1 @@
+PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)
diff --git a/research/direct-flow-leaf-saturation/logs/mutations-optimized.log b/research/direct-flow-leaf-saturation/logs/mutations-optimized.log
new file mode 100644
index 0000000000..ba3e3e0348
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/mutations-optimized.log
@@ -0,0 +1 @@
+PASS_MUTATION_CONTROLS source_bytes_normal_and_optimized corrupted_receipt paid_and_target_count_plus_one
diff --git a/research/direct-flow-leaf-saturation/logs/mutations.log b/research/direct-flow-leaf-saturation/logs/mutations.log
new file mode 100644
index 0000000000..ba3e3e0348
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/mutations.log
@@ -0,0 +1 @@
+PASS_MUTATION_CONTROLS source_bytes_normal_and_optimized corrupted_receipt paid_and_target_count_plus_one
diff --git a/research/direct-flow-leaf-saturation/logs/optimized.log b/research/direct-flow-leaf-saturation/logs/optimized.log
new file mode 100644
index 0000000000..33db553260
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/optimized.log
@@ -0,0 +1,48 @@
+{
+  "controls": {
+    "interval_domain_rejections": 3,
+    "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1"
+  },
+  "finite_law": {
+    "extra_terminal_truncation": "rejected",
+    "ordered_word_max_depth": 3,
+    "whole_flow_fixtures": 8
+  },
+  "parameters": {
+    "alpha": [
+      "0.98981438244597",
+      "0.98981438244599"
+    ],
+    "drift_above_log5": [
+      "0.016477707041",
+      "0.016477707042"
+    ],
+    "invoice_derivative_lower_bound_interval_0_99_to_1": [
+      "211661.930309",
+      "211661.930310"
+    ],
+    "lambda": [
+      "0.00749912850515",
+      "0.00749912850519"
+    ],
+    "mean_deficit_limit": [
+      "133.34882837",
+      "133.34882838"
+    ],
+    "mean_leaf_depth_limit": [
+      "136.51870330",
+      "136.51870331"
+    ],
+    "mean_log_rank": [
+      "1.625915619475",
+      "1.625915619476"
+    ],
+    "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds",
+    "t_star": [
+      "0.99731351095114",
+      "0.99731351095116"
+    ]
+  },
+  "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.",
+  "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS"
+}
diff --git a/research/direct-flow-leaf-saturation/logs/portable-0.log b/research/direct-flow-leaf-saturation/logs/portable-0.log
new file mode 100644
index 0000000000..33db553260
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/portable-0.log
@@ -0,0 +1,48 @@
+{
+  "controls": {
+    "interval_domain_rejections": 3,
+    "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1"
+  },
+  "finite_law": {
+    "extra_terminal_truncation": "rejected",
+    "ordered_word_max_depth": 3,
+    "whole_flow_fixtures": 8
+  },
+  "parameters": {
+    "alpha": [
+      "0.98981438244597",
+      "0.98981438244599"
+    ],
+    "drift_above_log5": [
+      "0.016477707041",
+      "0.016477707042"
+    ],
+    "invoice_derivative_lower_bound_interval_0_99_to_1": [
+      "211661.930309",
+      "211661.930310"
+    ],
+    "lambda": [
+      "0.00749912850515",
+      "0.00749912850519"
+    ],
+    "mean_deficit_limit": [
+      "133.34882837",
+      "133.34882838"
+    ],
+    "mean_leaf_depth_limit": [
+      "136.51870330",
+      "136.51870331"
+    ],
+    "mean_log_rank": [
+      "1.625915619475",
+      "1.625915619476"
+    ],
+    "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds",
+    "t_star": [
+      "0.99731351095114",
+      "0.99731351095116"
+    ]
+  },
+  "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.",
+  "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS"
+}
diff --git a/research/direct-flow-leaf-saturation/logs/portable-1.log b/research/direct-flow-leaf-saturation/logs/portable-1.log
new file mode 100644
index 0000000000..f50d39a3e3
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/portable-1.log
@@ -0,0 +1,65 @@
+{
+  "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION",
+  "fixtures": [
+    {
+      "N": 121,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 604,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 605,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 606,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3024,
+      "G": 1,
+      "leaf_ranks": 30,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3025,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3026,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15124,
+      "G": 2,
+      "leaf_ranks": 65,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15125,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15126,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_truncation_rejected": true
+    }
+  ]
+}
diff --git a/research/direct-flow-leaf-saturation/logs/portable-2.log b/research/direct-flow-leaf-saturation/logs/portable-2.log
new file mode 100644
index 0000000000..ba3e3e0348
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/portable-2.log
@@ -0,0 +1 @@
+PASS_MUTATION_CONTROLS source_bytes_normal_and_optimized corrupted_receipt paid_and_target_count_plus_one
diff --git a/research/direct-flow-leaf-saturation/logs/portable-results.json b/research/direct-flow-leaf-saturation/logs/portable-results.json
new file mode 100644
index 0000000000..1855fd7914
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/portable-results.json
@@ -0,0 +1,40 @@
+{
+  "export_commit": "9465f263a673d2d86e7262523cbeb0e796f486cf",
+  "export_files": 26,
+  "git_available": false,
+  "path": "empty directory",
+  "runs": [
+    {
+      "command": [
+        "python3",
+        "-B",
+        "research/direct-flow-leaf-saturation/verify.py",
+        "--expect",
+        "research/direct-flow-leaf-saturation/RESULT.json"
+      ],
+      "exit_code": 0,
+      "seconds": 14.383,
+      "log": "logs/portable-0.log"
+    },
+    {
+      "command": [
+        "python3",
+        "-B",
+        "research/direct-flow-leaf-saturation/independent_source.py"
+      ],
+      "exit_code": 0,
+      "seconds": 0.094,
+      "log": "logs/portable-1.log"
+    },
+    {
+      "command": [
+        "python3",
+        "-B",
+        "research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "exit_code": 0,
+      "seconds": 28.189,
+      "log": "logs/portable-2.log"
+    }
+  ]
+}
diff --git a/research/direct-flow-leaf-saturation/logs/primary.log b/research/direct-flow-leaf-saturation/logs/primary.log
new file mode 100644
index 0000000000..33db553260
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/primary.log
@@ -0,0 +1,48 @@
+{
+  "controls": {
+    "interval_domain_rejections": 3,
+    "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1"
+  },
+  "finite_law": {
+    "extra_terminal_truncation": "rejected",
+    "ordered_word_max_depth": 3,
+    "whole_flow_fixtures": 8
+  },
+  "parameters": {
+    "alpha": [
+      "0.98981438244597",
+      "0.98981438244599"
+    ],
+    "drift_above_log5": [
+      "0.016477707041",
+      "0.016477707042"
+    ],
+    "invoice_derivative_lower_bound_interval_0_99_to_1": [
+      "211661.930309",
+      "211661.930310"
+    ],
+    "lambda": [
+      "0.00749912850515",
+      "0.00749912850519"
+    ],
+    "mean_deficit_limit": [
+      "133.34882837",
+      "133.34882838"
+    ],
+    "mean_leaf_depth_limit": [
+      "136.51870330",
+      "136.51870331"
+    ],
+    "mean_log_rank": [
+      "1.625915619475",
+      "1.625915619476"
+    ],
+    "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds",
+    "t_star": [
+      "0.99731351095114",
+      "0.99731351095116"
+    ]
+  },
+  "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.",
+  "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS"
+}
diff --git a/research/direct-flow-leaf-saturation/logs/registered.log b/research/direct-flow-leaf-saturation/logs/registered.log
new file mode 100644
index 0000000000..b4772c2b4a
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/registered.log
@@ -0,0 +1,118 @@
+CHECK Exact rational root/drift/tilt/limit enclosures, eight whole-flow fixtures, lattice and domain failure controls; classical LLT proof is written, not machine-checked.
+{
+  "controls": {
+    "interval_domain_rejections": 3,
+    "lattice_countermodel": "geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1"
+  },
+  "finite_law": {
+    "extra_terminal_truncation": "rejected",
+    "ordered_word_max_depth": 3,
+    "whole_flow_fixtures": 8
+  },
+  "parameters": {
+    "alpha": [
+      "0.98981438244597",
+      "0.98981438244599"
+    ],
+    "drift_above_log5": [
+      "0.016477707041",
+      "0.016477707042"
+    ],
+    "invoice_derivative_lower_bound_interval_0_99_to_1": [
+      "211661.930309",
+      "211661.930310"
+    ],
+    "lambda": [
+      "0.00749912850515",
+      "0.00749912850519"
+    ],
+    "mean_deficit_limit": [
+      "133.34882837",
+      "133.34882838"
+    ],
+    "mean_leaf_depth_limit": [
+      "136.51870330",
+      "136.51870331"
+    ],
+    "mean_log_rank": [
+      "1.625915619475",
+      "1.625915619476"
+    ],
+    "method": "exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds",
+    "t_star": [
+      "0.99731351095114",
+      "0.99731351095116"
+    ]
+  },
+  "scope": "Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.",
+  "status": "PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS"
+}
+CHECK Ten independent ordered-word fixtures agree with PR4436 and PR4467 leaf histograms; wrong final truncation rejected.
+{
+  "status": "PASS_INDEPENDENT_SOURCE_LEAF_IDENTIFICATION",
+  "fixtures": [
+    {
+      "N": 121,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 604,
+      "G": 0,
+      "leaf_ranks": 9,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 605,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 606,
+      "G": 1,
+      "leaf_ranks": 26,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3024,
+      "G": 1,
+      "leaf_ranks": 30,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3025,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 3026,
+      "G": 2,
+      "leaf_ranks": 55,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15124,
+      "G": 2,
+      "leaf_ranks": 65,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15125,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_truncation_rejected": true
+    },
+    {
+      "N": 15126,
+      "G": 3,
+      "leaf_ranks": 98,
+      "terminal_truncation_rejected": true
+    }
+  ]
+}
+CHECK Reject changed source bytes, altered histogram bracket, and corrupted expected receipt, including under optimized Python.
+PASS_MUTATION_CONTROLS source_bytes_normal_and_optimized corrupted_receipt paid_and_target_count_plus_one
+PASS_REGISTERED_RESEARCH_PACKAGE research/direct-flow-leaf-saturation outcome=completed
diff --git a/research/direct-flow-leaf-saturation/logs/validation.json b/research/direct-flow-leaf-saturation/logs/validation.json
new file mode 100644
index 0000000000..7a3734b6f2
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/logs/validation.json
@@ -0,0 +1,117 @@
+{
+  "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]",
+  "platform": "Linux-6.18.55-x86_64-with-glibc2.41",
+  "base": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "runs": [
+    {
+      "name": "metadata",
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_package.py",
+        "--package",
+        "research/direct-flow-leaf-saturation",
+        "--check-only"
+      ],
+      "exit_code": 0,
+      "seconds": 0.207,
+      "log": "logs/metadata.log"
+    },
+    {
+      "name": "primary",
+      "command": [
+        "python3",
+        "-B",
+        "research/direct-flow-leaf-saturation/verify.py",
+        "--expect",
+        "research/direct-flow-leaf-saturation/RESULT.json"
+      ],
+      "exit_code": 0,
+      "seconds": 15.394,
+      "log": "logs/primary.log"
+    },
+    {
+      "name": "optimized",
+      "command": [
+        "python3",
+        "-B",
+        "-O",
+        "research/direct-flow-leaf-saturation/verify.py",
+        "--expect",
+        "research/direct-flow-leaf-saturation/RESULT.json"
+      ],
+      "exit_code": 0,
+      "seconds": 16.419,
+      "log": "logs/optimized.log"
+    },
+    {
+      "name": "independent",
+      "command": [
+        "python3",
+        "-B",
+        "research/direct-flow-leaf-saturation/independent_source.py"
+      ],
+      "exit_code": 0,
+      "seconds": 0.098,
+      "log": "logs/independent.log"
+    },
+    {
+      "name": "independent-optimized",
+      "command": [
+        "python3",
+        "-B",
+        "-O",
+        "research/direct-flow-leaf-saturation/independent_source.py"
+      ],
+      "exit_code": 0,
+      "seconds": 0.169,
+      "log": "logs/independent-optimized.log"
+    },
+    {
+      "name": "mutations",
+      "command": [
+        "python3",
+        "-B",
+        "research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "exit_code": 0,
+      "seconds": 30.049,
+      "log": "logs/mutations.log"
+    },
+    {
+      "name": "mutations-optimized",
+      "command": [
+        "python3",
+        "-B",
+        "-O",
+        "research/direct-flow-leaf-saturation/test_controls.py"
+      ],
+      "exit_code": 0,
+      "seconds": 30.11,
+      "log": "logs/mutations-optimized.log"
+    },
+    {
+      "name": "registered",
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_package.py",
+        "--package",
+        "research/direct-flow-leaf-saturation"
+      ],
+      "exit_code": 0,
+      "seconds": 43.277,
+      "log": "logs/registered.log"
+    }
+  ],
+  "scientific_files_sha256": {
+    "PROOF.md": "b6edd825bc5a3a48fc2860533040faa111c7f239f8724bb3b50cc8a3bdfdc6e7",
+    "verify.py": "9a6ed8de94eab4a643685eba3697d34503bae9dd4c6097b6b8a6f230c29dd3b8",
+    "RESULT.json": "7c0b9019941b2178c58c846a1077748669eab39c39128b4ca9e5f6455f736aef",
+    "independent_source.py": "4aef5b1d0c61a9af68d27c4fdda924e188363a9b7444c75e6d1c6b666db834b0",
+    "test_controls.py": "04410e43354ebb70ad52dc18ecd3d54e3369b2c41161558555dc12c37bb9ac61",
+    "SOURCES.json": "90997ec1be8cd8c3e588d71a349783b2f1696a224dc082749f3886bebd8c2c4a",
+    "VERIFY.json": "b7e76cf715a9d4bcbf0482f64856852ccf410d1c5fecbb7fed04283550e72e54"
+  },
+  "post_run_prose_edit": "Normalized PR-number references to #NUMBER and linked the verified canonical claim; no mathematical or computational change."
+}
diff --git a/research/direct-flow-leaf-saturation/test_controls.py b/research/direct-flow-leaf-saturation/test_controls.py
new file mode 100644
index 0000000000..853574c027
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/test_controls.py
@@ -0,0 +1,113 @@
+#!/usr/bin/env python3
+"""Mutation controls for the certificate boundary. DLamdata/Codex, Apache-2.0."""
+import hashlib
+import importlib.util
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+spec = importlib.util.spec_from_file_location('certificate', HERE / 'verify.py')
+v = importlib.util.module_from_spec(spec)
+spec.loader.exec_module(v)
+
+
+def require_rejection(argv, cwd, needle):
+    run = subprocess.run(argv, cwd=cwd, text=True, capture_output=True, timeout=60)
+    if run.returncode == 0 or needle not in run.stderr:
+        raise ValueError(f'control did not reject with {needle!r}: {run.returncode}, {run.stderr[-400:]}')
+
+
+def repin(package, root, relative):
+    manifest = json.loads((package / 'SOURCES.json').read_text())
+    for row in manifest['files']:
+        if row['path'] == relative:
+            row['sha256'] = hashlib.sha256((root / relative).read_bytes()).hexdigest()
+    (package / 'SOURCES.json').write_text(json.dumps(manifest))
+
+
+with tempfile.TemporaryDirectory(prefix='leaf-saturation-controls-') as directory:
+    root = Path(directory)
+    package = root / 'research/direct-flow-leaf-saturation'
+    package.mkdir(parents=True)
+    for name in ('verify.py', 'independent_source.py', 'SOURCES.json', 'RESULT.json'):
+        shutil.copy2(HERE / name, package / name)
+    sources = json.loads((HERE / 'SOURCES.json').read_text())
+    for row in sources['files']:
+        if row['usage'] == 'input':
+            target = root / row['path']
+            target.parent.mkdir(parents=True, exist_ok=True)
+            shutil.copy2(ROOT / row['path'], target)
+    # Both standalone entry points must bind bytes before executing inputs.
+    for relative in ('research/direct-flow-leaf-walk/verify.py', 'research/direct-mixed-flow/flow.py'):
+        source = root / relative
+        original = source.read_bytes()
+        source.write_bytes(original + b'\n# corrupt-source control\n')
+        for script in ('verify.py', 'independent_source.py'):
+            for mode in ([], ['-O']):
+                require_rejection([sys.executable, *mode, '-B', str(package / script)], root, 'source mismatch: ' + relative)
+        source.write_bytes(original)
+
+    # Exercise the actual source-histogram assertions. Re-pin mutant bytes so
+    # a checksum failure cannot masquerade as a semantic rejection.
+    relative = 'research/direct-flow-leaf-walk/diagnostics/overlap_flow.py'
+    source = root / relative
+    original = source.read_text()
+    branch = '                    if d == G:\n                        add(X, rank, issued); continue'
+    if original.count(branch) != 1:
+        raise ValueError('source mutation anchor drift')
+    mutations = {
+        'empty_leaf': '                    if d == G:\n                        continue',
+        'truncated_terminal': '                    if d == G:\n                        if m * rank <= N: add(X, rank, issued)\n                        continue',
+    }
+    probe = "import runpy,sys; v=runpy.run_path(sys.argv[1]); v['finite_law'](*v['bindings']())"
+    for replacement in mutations.values():
+        source.write_text(original.replace(branch, replacement))
+        repin(package, root, relative)
+        for mode in ([], ['-O']):
+            require_rejection([sys.executable, *mode, '-B', '-c', probe, str(package / 'verify.py')], root, 'ordered words disagree with actual leaf exits')
+            require_rejection([sys.executable, *mode, '-B', str(package / 'independent_source.py')], root, 'leaf histogram')
+    source.write_text(original)
+    shutil.copy2(HERE / 'SOURCES.json', package / 'SOURCES.json')
+
+    # Corrupt only the original Flow class's returned boundary histogram, after
+    # its own conservation checks. This reaches the independent comparison
+    # instead of failing an earlier producer invariant or byte-authentication.
+    relative = 'research/direct-mixed-flow/flow.py'
+    source = root / relative
+    original = source.read_text()
+    field = "'boundary_exits': boundary,"
+    if original.count(field) != 1:
+        raise ValueError('original Flow mutation anchor drift')
+    source.write_text(original.replace(field, "'boundary_exits': boundary + Counter({1: 1}),"))
+    repin(package, root, relative)
+    for mode in ([], ['-O']):
+        require_rejection([sys.executable, *mode, '-B', str(package / 'independent_source.py')],
+                          root, "(121, 'original Flow class')")
+    source.write_text(original)
+    shutil.copy2(HERE / 'SOURCES.json', package / 'SOURCES.json')
+
+    expected = json.loads((package / 'RESULT.json').read_text())
+    expected['parameters']['lambda'][0] = '0.0'
+    receipt = package / 'corrupt-result.json'
+    receipt.write_text(json.dumps(expected))
+    require_rejection([sys.executable, '-O', '-B', str(package / 'verify.py'), '--expect', str(receipt)], root, 'expected receipt mismatch')
+
+# These are regressions for this narrow pinned root bracket, not general
+# coverage of enclosure arithmetic; test_enclosures.py checks that separately.
+for name in ('paid', 'target'):
+    P, W, M = v.bindings()
+    histogram = P if name == 'paid' else W
+    histogram[min(histogram)] += 1
+    try:
+        v.parameters(P, W, M)
+    except ValueError as error:
+        if 'invoice root bracket' not in str(error):
+            raise
+    else:
+        raise ValueError('changed histogram passed fixed root certificate: ' + name)
+print('PASS_MUTATION_CONTROLS both_standalone_pins_normal_and_optimized repinned_empty_and_truncated_leaf_sources_normal_and_optimized repinned_original_flow_return_normal_and_optimized corrupted_receipt fixed_bracket_count_regressions')
diff --git a/research/direct-flow-leaf-saturation/test_enclosures.py b/research/direct-flow-leaf-saturation/test_enclosures.py
new file mode 100644
index 0000000000..61c01cdddf
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/test_enclosures.py
@@ -0,0 +1,170 @@
+#!/usr/bin/env python3
+"""Exact independent enclosure checks and discriminating remainder mutations.
+
+The logarithm oracle uses -log(1-q)=sum(q**k/k), rather than the primary
+atanh series. After n=2**e*u, 1<=u<2, both log(2) and log(u) have q<=1/2.
+For K=256 the positive remainder is at most
+q**(K+1)/((K+1)*(1-q)).
+
+The exponential oracle sums through degree 82. Its first omitted term is
+x**83/83!, and every subsequent term ratio is at most x/84<=5/84, so a
+geometric series bounds its tail. This does not use the primary Lagrange
+bound exp(x)<3**5. Both implementations still share the ordinary exponential
+series and Python's exact Fraction arithmetic; these finite checks are not a
+formal proof of either series or of all future inputs.
+
+Every successful log/exp argument in the primary parameters and controls is
+checked. The domain is collected from that execution, not independently
+inferred. Three mutations use smaller, explicitly named discriminating
+fixtures; they do not rerun a mutated scientific certificate.
+
+Prepared for DLamdata with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+from fractions import Fraction
+from functools import lru_cache
+from pathlib import Path
+import hashlib
+import json
+
+HERE = Path(__file__).resolve().parent
+PRODUCTION = HERE / 'verify.py'
+Q = Fraction
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def load(source):
+    """Compile the actual source bytes, with no import bytecode-cache reuse."""
+    namespace = {'__name__': 'enclosure_test_subject', '__file__': str(PRODUCTION)}
+    exec(compile(source, str(PRODUCTION), 'exec'), namespace)
+    return namespace
+
+
+@lru_cache(None)
+def log_oracle(n):
+    need(isinstance(n, int) and n >= 1, 'oracle positive integer log input')
+    e = n.bit_length() - 1
+    u = Q(n, 1 << e)
+
+    def minus_log_one_minus(q):
+        need(0 <= q <= Q(1, 2), 'oracle log range reduction')
+        term = Q(1)
+        lower = Q(0)
+        for k in range(1, 257):
+            term *= q
+            lower += term / k
+        remainder = term * q / (257 * (1 - q))
+        return lower, lower + remainder
+
+    lo2, hi2 = minus_log_one_minus(Q(1, 2))
+    lou, hiu = minus_log_one_minus(1 - 1 / u)
+    return e * lo2 + lou, e * hi2 + hiu
+
+
+@lru_cache(None)
+def exp_oracle(x):
+    need(isinstance(x, Q) and 0 <= x <= 5, 'oracle rational exp domain [0,5]')
+    term = lower = Q(1)
+    for k in range(1, 83):
+        term *= x / k
+        lower += term
+    first_omitted = term * x / 83
+    upper = lower + first_omitted / (1 - x / 84)
+    return lower, upper
+
+
+def check_enclosure(kind, argument, production_interval, oracle_interval):
+    lo, hi = production_interval
+    oracle_lo, oracle_hi = oracle_interval
+    need(all(isinstance(x, Q) for x in (lo, hi, oracle_lo, oracle_hi)),
+         kind + ' arithmetic must remain exact Fraction')
+    need(lo <= oracle_lo <= oracle_hi <= hi,
+         kind + ' enclosure fails exact independent containment')
+
+
+def actual_arguments(subject):
+    logs, exponentials = set(), set()
+    original_log, original_exp = subject['log_bounds'], subject['exp_point']
+
+    def track_log(n):
+        value = original_log(n)
+        logs.add(n)
+        return value
+
+    def track_exp(x):
+        value = original_exp(x)
+        exponentials.add(x)
+        return value
+
+    subject['log_bounds'], subject['exp_point'] = track_log, track_exp
+    P, W, M = subject['bindings']()
+    subject['parameters'](P, W, M)
+    subject['controls']()
+    # The full verifier's remaining finite_law function uses integer products
+    # and counts only; it makes no log_bounds or exp_point calls.
+    need(logs and exponentials, 'empty production argument coverage')
+    return logs, exponentials, original_log, original_exp
+
+
+def reject_mutation(source, name, old, new, kind, argument):
+    need(source.count(old) == 1, 'mutation source anchor changed: ' + name)
+    mutated = load(source.replace(old, new))
+    function = mutated['log_bounds' if kind == 'log' else 'exp_point']
+    oracle = log_oracle if kind == 'log' else exp_oracle
+    try:
+        check_enclosure(kind, argument, function(argument), oracle(argument))
+    except ValueError as error:
+        need(str(error) == kind + ' enclosure fails exact independent containment',
+             'mutation rejected for an unrelated reason: ' + name)
+        return name
+    raise ValueError('remainder mutation escaped independent check: ' + name)
+
+
+def main():
+    source = PRODUCTION.read_text(encoding='utf-8')
+    subject = load(source)
+    logs, exponentials, production_log, production_exp = actual_arguments(subject)
+    for n in sorted(logs):
+        check_enclosure('log', n, production_log(n), log_oracle(n))
+    for x in sorted(exponentials):
+        check_enclosure('exp', x, production_exp(x), exp_oracle(x))
+    # Known exact endpoints also guard the oracle's zero cases.
+    need(log_oracle(1) == (Q(0), Q(0)) and exp_oracle(Q(0)) == (Q(1), Q(1)),
+         'independent oracle identity fixtures')
+    mutations = [
+        reject_mutation(source, 'zero_log_tail_at_log2',
+                        '        return total, total + tail',
+                        '        return total, total', 'log', 2),
+        reject_mutation(source, 'zero_exp_tail_at_exp1',
+                        'tail = Q(3 ** 5) * term * x / 81',
+                        'tail = Q(0)', 'exp', Q(1)),
+        reject_mutation(source, 'invalid_exp_majorant_one_at_exp1',
+                        'tail = Q(3 ** 5) * term * x / 81',
+                        'tail = Q(1) * term * x / 81', 'exp', Q(1)),
+    ]
+    need(max(exponentials) < Q(479, 100), 'actual exp argument ceiling changed')
+    # A deterministic domain digest records exact argument coverage without
+    # printing the large rational numerators/denominators.
+    domain = json.dumps({'log': sorted(logs),
+                         'exp': [[str(x.numerator), str(x.denominator)]
+                                 for x in sorted(exponentials)]},
+                        sort_keys=True, separators=(',', ':')).encode()
+    print(json.dumps({
+        'status': 'PASS_INDEPENDENT_RATIONAL_ENCLOSURES',
+        'production_source_sha256': hashlib.sha256(source.encode('utf-8')).hexdigest(),
+        'log_integer_arguments': sorted(logs),
+        'distinct_exp_rational_arguments': len(exponentials),
+        'all_exp_arguments_below': '479/100',
+        'domain_sha256': hashlib.sha256(domain).hexdigest(),
+        'log_oracle': '256-term -log(1-q) series; exact positive geometric tail',
+        'exp_oracle': 'degree-82 positive series; exact ratio-bounded geometric tail',
+        'mutations_rejected': mutations,
+        'scope': 'Exact containment at every argument captured from current parameters and controls; finite mutation discrimination, not a formal verifier or an all-input enclosure proof.'
+    }, indent=2, sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/direct-flow-leaf-saturation/verify.py b/research/direct-flow-leaf-saturation/verify.py
new file mode 100644
index 0000000000..83d2cd9276
--- /dev/null
+++ b/research/direct-flow-leaf-saturation/verify.py
@@ -0,0 +1,223 @@
+#!/usr/bin/env python3
+"""Exact source/parameter/finite-law checks; does not mechanically prove the LLT.
+DLamdata with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+from fractions import Fraction as Q
+from functools import lru_cache
+from pathlib import Path
+import argparse
+import ast
+import hashlib
+import itertools
+import json
+import math
+import runpy
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+# Rational intervals. No machine floating-point arithmetic in certification.
+def add(a, b):
+    return a[0] + b[0], a[1] + b[1]
+
+
+def neg(a):
+    return -a[1], -a[0]
+
+
+def mul(a, b):
+    v = [x * y for x in a for y in b]
+    return min(v), max(v)
+
+
+def div(a, b):
+    need(b[0] > 0, 'positive denominator required')
+    return mul(a, (1 / b[1], 1 / b[0]))
+
+
+def pt(x):
+    return Q(x), Q(x)
+
+
+@lru_cache(None)
+def log_bounds(n):
+    """log(n) via 2 atanh(z), |z|<=1/3, with geometric tail."""
+    need(isinstance(n, int) and n >= 1, 'positive integer log input')
+    if n == 1:
+        return pt(0)
+    e = n.bit_length() - 1
+    u = Q(n, 2 ** e)
+
+    def series(z):
+        total = sum((2 * z ** (2 * k + 1) / (2 * k + 1) for k in range(48)), Q(0))
+        tail = 2 * z ** 97 / (97 * (1 - z * z))
+        return total, total + tail
+
+    return add(mul(pt(e), series(Q(1, 3))), series((u - 1) / (u + 1)))
+
+
+@lru_cache(None)
+def exp_point(x):
+    """Taylor enclosure for 0<=x<=5; exp(x)<=3^5 bounds remainder."""
+    need(0 <= x <= 5, 'exp domain [0,5]')
+    term = total = Q(1)
+    for k in range(1, 81):
+        term = term * x / k
+        total += term
+    tail = Q(3 ** 5) * term * x / 81
+    return total, total + tail
+
+
+def exp_bounds(x):
+    return exp_point(x[0])[0], exp_point(x[1])[1]
+
+
+def power(n, t):
+    return exp_bounds(mul(log_bounds(n), pt(t)))
+
+
+def moment(hist, t, derivative=False):
+    out = pt(0)
+    for rank, count in hist.items():
+        term = mul(pt(count), power(rank, t))
+        if derivative:
+            term = mul(term, log_bounds(rank))
+        out = add(out, term)
+    return out
+
+
+def mean(hist, t):
+    return div(moment(hist, t, True), moment(hist, t))
+
+
+def rounded(a, places=12):
+    scale = 10 ** places
+    lo = a[0].numerator * scale // a[0].denominator
+    hi = -((-a[1].numerator * scale) // a[1].denominator)
+    def fmt(k):
+        sign = '-' if k < 0 else ''
+        k = abs(k)
+        return f'{sign}{k // scale}.{k % scale:0{places}d}'
+    return [fmt(lo), fmt(hi)]
+
+
+def bindings():
+    source = json.loads((HERE / 'SOURCES.json').read_text())
+    for row in source['files']:
+        if row['usage'] == 'input':
+            need(hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'],
+                 'source mismatch: ' + row['path'])
+    path = ROOT / 'research/direct-flow-leaf-walk/verify.py'
+    constants = {}
+    for node in ast.parse(path.read_text()).body:
+        if isinstance(node, ast.Assign) and len(node.targets) == 1 and isinstance(node.targets[0], ast.Name):
+            if node.targets[0].id in ('P', 'W', 'M'):
+                constants[node.targets[0].id] = ast.literal_eval(node.value)
+    need(set(constants) == {'P', 'W', 'M'}, 'source constants missing')
+    return constants['P'], constants['W'], constants['M']
+
+
+def parameters(P, W, M):
+    t = (Q('0.99731351095114'), Q('0.99731351095116'))
+    alpha = (Q('0.98981438244597'), Q('0.98981438244599'))
+    # Positive derivative on the full source bisection interval identifies its root.
+    f_lo = add(moment(W, t[0]), neg(moment(P, t[0])))
+    f_hi = add(moment(W, t[1]), neg(moment(P, t[1])))
+    derivative = add(moment(W, Q('0.99'), True), neg(moment(P, Q(1), True)))
+    need(f_lo[1] < 0 < f_hi[0] and derivative[0] > 0, 'invoice root bracket')
+    a = log_bounds(5)
+    need(mean(P, alpha[0])[1] < a[0] and mean(P, alpha[1])[0] > a[1], 'tilt mean bracket')
+    mu = mean(P, t[0])[0], mean(P, t[1])[1]  # mean strictly increases: derivative=variance>0.
+    drift = add(mu, neg(a))
+    need(drift[0] > 0, 'positive drift')
+    need(all(P.get(k, 0) > 0 for k in (1, 2, 3)), 'nonlattice support witness 1,2,3')
+    lam = add(t, neg(alpha))
+    inverse = div(pt(1), lam)
+    depth = add(add(log_bounds(M), neg(mu)), inverse)
+    return {'t_star': rounded(t, 14), 'alpha': rounded(alpha, 14),
+            'lambda': rounded(lam, 14), 'mean_log_rank': rounded(mu),
+            'invoice_derivative_lower_bound_interval_0_99_to_1': rounded(derivative, 6),
+            'drift_above_log5': rounded(drift), 'mean_deficit_limit': rounded(inverse, 8),
+            'mean_leaf_depth_limit': rounded(depth, 8),
+            'method': 'exact Fraction arithmetic, log atanh48 and exp Taylor80 with positive remainder bounds'}
+
+
+def finite_law(P, W, M):
+    # Independent ordered-word enumeration vs the predecessor's whole-flow X-BX.
+    flow = runpy.run_path(str(ROOT / 'research/direct-flow-leaf-walk/diagnostics/overlap_flow.py'))['flow']
+    count = 0
+    terminal_cut_distinguishing_fixtures = 0
+    for G in range(4):
+        for N in (M * 5 ** G, M * 5 ** G + M * 5 ** G // 2):
+            got = flow(N, W, P)
+            need(got['G'] == G, 'flow depth')
+            prefixes = {}
+            for word in itertools.product(P, repeat=G):
+                rho = math.prod(word)
+                if M * rho <= N:
+                    prefixes[rho] = prefixes.get(rho, 0) + math.prod(P[r] for r in word)
+            leaves, wrong = {}, {}
+            for rho, multiplicity in prefixes.items():
+                for r, pr in P.items():
+                    e = rho * r
+                    leaves[e] = leaves.get(e, 0) + multiplicity * pr
+                    if M * e <= N:
+                        wrong[e] = wrong.get(e, 0) + multiplicity * pr
+            actual = {e: c - got['BX'].get(e, 0) for e, c in got['X'].items() if c != got['BX'].get(e, 0)}
+            need(actual == leaves, 'ordered words disagree with actual leaf exits')
+            # This checks fixture sensitivity, not an additional source identity.
+            # Source coverage is the complete actual==leaves comparison above.
+            terminal_cut_distinguishing_fixtures += wrong != leaves
+            count += 1
+    need(terminal_cut_distinguishing_fixtures > 0, 'no fixture distinguishes terminal truncation')
+    return {'whole_flow_fixtures': count, 'ordered_word_max_depth': 3,
+            'terminal_cut_distinguishing_fixtures': terminal_cut_distinguishing_fixtures,
+            'source_check': 'complete actual X-BX histogram equals ordered-word enumeration'}
+
+
+def controls():
+    # Lattice countermodel: X in {0,log2}, p(X=log2)=2/3, barrier n log2/2.
+    # At even n the limiting gap/log2 is geometric with mean 1, whereas
+    # the nonlattice formula would give mean gap=1 (lambda=1).
+    means = []
+    for n in (40, 400):
+        denominator = sum(math.comb(n, k) * 2 ** k for k in range(n // 2 + 1))
+        numerator = sum((n // 2 - k) * math.comb(n, k) * 2 ** k for k in range(n // 2 + 1))
+        means.append(Q(numerator, denominator))
+    need(0 < means[0] < means[1] < 1, 'lattice geometric control')
+    need(mul(pt(means[1]), log_bounds(2))[1] < Q(7, 10), 'lattice mean must differ from exponential mean 1')
+    rejected = 0
+    for f in (lambda: div(pt(1), (-Q(1), Q(1))), lambda: exp_point(Q(-1)), lambda: log_bounds(0)):
+        try:
+            f()
+        except ValueError:
+            rejected += 1
+    need(rejected == 3, 'interval domain controls')
+    # Elementary exact enclosure controls include endpoint exp0/log1 identities.
+    need(log_bounds(1) == pt(0) and exp_point(Q(0)) == pt(1), 'identity fixtures')
+    need(log_bounds(2)[0] > Q(69, 100) and log_bounds(2)[1] < Q(7, 10), 'log2 fixture')
+    return {'lattice_countermodel': 'geometric mean gap/log2 tends to 1; finite n=400 gap<0.7, not exponential mean1',
+            'interval_domain_rejections': rejected}
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--expect', type=Path)
+    args = parser.parse_args()
+    P, W, M = bindings()
+    result = {'status': 'PASS_DIRECT_FLOW_LEAF_SATURATION_CHECKS', 'parameters': parameters(P, W, M),
+              'finite_law': finite_law(P, W, M), 'controls': controls(),
+              'scope': 'Source identity, rigorous numerical hypotheses and finite controls only; see PROOF.md for classical-LLT-based theorem. No finite-depth rate, total-flow ceiling or new kappa.'}
+    if args.expect:
+        need(result == json.loads(args.expect.read_text()), 'expected receipt mismatch')
+    print(json.dumps(result, indent=2, sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()