Make the fixed-height direct-flow recurrence bound fully effective

research/effective-direct-flow/README.md

@@ -0,0 +1,146 @@
+# An effective all-rank bound for the fixed-height direct flow
+
+**Scoped analytic theorem; no new kappa.** This answers the effective-onset
+question in [#6329](https://github.com/CrocSwap/integer-mult-bounds/pull/6329)
+(`research/direct-flow-exponent-gate`). For its exact historical raw-p7 scalar
+recurrence, retain the original height and every source, complement, boundary
+exit and terminal leaf. Set
+
+\[
+s=\frac{99739}{100000},\qquad
+G_0=2\cdot2^{10^{12}}+2,\qquad N_0=121\,5^{G_0}.
+\]
+
+Then, for **every integer \(n\ge1\)**,
+
+\[
+\boxed{L(n)\le N_0^{261/100000}\,n^{99739/100000}.}
+\]
+
+The predecessor already proved the upper exponent 0.99739 and identified the
+limiting scalar exponent. Its local-limit argument supplied no effective onset
+or majorant constant. This contribution supplies both. The threshold is
+deliberately enormous: it proves effectivity, not practical finite-size savings,
+and is not claimed to be optimal. Verification uses its exact symbolic expression;
+it does not construct that integer or run a flow of that size.
+
+## What closes the gap
+
+[LOCAL_LIMIT.md](LOCAL_LIMIT.md) proves a uniform interval local-limit estimate
+with explicit error O(1/log n) for the paid law. Compact Fourier interval
+majorants and minorants reduce the problem to a bounded frequency range.
+The elementary integer separation of powers of 2 and 3 supplies a quantitative
+gap on that range. The new implication has no ineffective irrationality constant
+or appeal to qualitative convergence. Atomic endpoints are covered.
+
+[PROOF.md](PROOF.md) transfers this estimate through all mixed target/paid
+layers and the full leaf tail. Working directly with source capacity minus
+exit cost avoids dividing approximate limiting masses. The independently
+checked limiting margin exceeds 40000; the explicit normalized error is below
+1600. Conservation at exponent one gives L(n)<=n, which provides the
+initial-range constant without enumerating the ranks below N_0.
+
+The classical Beurling--Selberg interval approximation is a cited theorem,
+with its precise normalization and an inspected primary-paper statement in
+LOCAL_LIMIT.md. The universal conclusion is a written proof, not a finite
+experiment or proof-assistant theorem. [REVIEW.md](REVIEW.md) records a separate
+adversarial AI review and discloses the reviewer's earlier contribution.
+
+## Reproduce and inspect
+
+From the repository root with standard-library Python 3.12:
+
+```sh
+python3 -I -W error -B research/effective-direct-flow/verify.py
+python3 -I -O -W error -B research/effective-direct-flow/verify.py
+python3 -B scripts/research_package.py --package research/effective-direct-flow
+python3 -I -W error -B research/effective-direct-flow/independent_checks.py
+```
+
+The two direct verifier commands print `PASS_EFFECTIVE_DIRECT_FLOW`. The
+registered replay runs both modes, independent arithmetic controls, and source
+transport checks. It authenticates five source files before
+using their bytes and writes no generated artifacts. The standalone verifier
+does not need Git or third-party libraries.
+
+The new numerical checker imports none of the predecessor's numerical engine.
+It uses integer endpoints on a 2^-128 grid, with directed rounding:
+
+- logarithms use 80 positive atanh terms after reduction to [1,2], with
+  tail 2z^161/[161(1-z^2)];
+- exponentials use 48 Taylor terms after division by 16, a geometric bound
+  on all omitted terms, and four squarings;
+- exact mean-root endpoint signs, three atom masses, variance, third
+  absolute moment, layer ratio and leaf decay are certified;
+- 512 positive binomial terms give a **lower** bound for complete complement
+  capacity. Omitting the remaining positive tail is valid for this one-sided
+  gate. The computed interval for the truncated margin is
+  `[47053.890913,47053.895405]`, so the full margin is above 40000;
+- small rational comparisons check the symbolic onset and complete error
+  budget without evaluating a huge power or a tiny floating exponential.
+
+Ten complete histograms at depths 0 through 3 compare an ordered-word
+decomposition with the authenticated original `Flow.merged()` implementation.
+Controls reject an extra terminal cap, a missing mixed layer, an insufficient
+onset, and invalid arithmetic domains. These finite checks corroborate the
+source binding and numerical premises; they do not prove an all-size limit.
+The separate exact arithmetic audit checks 3,969 signed interval pairs and
+630 signed ceiling cases against independent rational extrema. Optional
+`diagnostic.py` uses an independent 90-digit Decimal implementation and direct
+pairwise capacity sums; its rounded output is explicitly outside acceptance.
+Exact commands, environment and source-corruption checks are recorded in
+[VALIDATION.json](VALIDATION.json).
+
+## Sources, overlap and limitations
+
+Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+[SOURCES.json](SOURCES.json) binds the literal law, original flow and #6329
+proof/README/task by SHA256 and Git blob. The current selected record and its
+review are provenance, not inputs to this historical recurrence theorem.
+The source law, flow and exact mirror decomposition remain predecessor work.
+No frozen source is modified.
+
+The final live overlap refresh (2026-11-04, 07:00--07:02 UTC) covered 663 open
+PRs and 6,789 discussion records with complete remote pagination; targeted
+all-state PR searches and direct reading
+covered the relevant archived predecessors. Sparse local coverage was incomplete.
+[#6128](https://github.com/CrocSwap/integer-mult-bounds/pull/6128) already gives
+a conditional leaf-tail bound; it does not give this uniform interval estimate
+or a complete recurrence onset. The stronger changed-height construction of
+#4483 is a different recurrence and is not replaced here. This is a bounded
+overlap survey, not a claim of literature-wide novelty.
+
+The selected conditional P104 result remains **kappa = 0.003125804 (#6030)**.
+Its construction and review were followed and its source-binding baseline
+passed before this historical side question was selected. No selected cold
+replay, native supplier, physical caller bill, ownership/erasure proof,
+precision/tape proof, compiler-cost admission or exact integer-recovery theorem
+is supplied. The five selected framework assumptions remain.
+
+## Open next questions
+
+- Can sharper frequency separation and a less conservative layer budget reduce
+  the explicit onset enough for a useful finite-cost comparison? Start with
+  certified bounds on the actual characteristic function over a chosen compact
+  frequency interval. A rigorous stronger spectral estimate is the blocker.
+- Can an all-size physical implementation fund the complete fixed-height
+  recurrence? Start by binding its native operations and access, restoration
+  and precision costs to the exact source flow. The scalar theorem alone does
+  not supply that implementation or bill.
+
+[TASK.json](TASK.json) records the changed scope and these questions. The
+[coordination claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19391591)
+identifies this continuation of #6329's handoff.
+
+## Credit
+
+Prepared for **@alephnan with substantial OpenAI Codex assistance**, including
+parallel mathematical derivation, exact code, writing and adversarial review.
+No independent human acceptance or proof-kernel verification is claimed.
+
+Credit zxv (#4436/#4483), Ryanson Jonathan / pinterbanget (#4459/#4467),
+DLamdata (#6118), Nick Petalas (#6125/#6128), the full-flow exponent contribution
+prepared for @CubeJerry (#6329), Cinna Davis / 1337isnot1337, Jacob Alan Sussman,
+and the retained native/precision/analytic lineage. Beurling, Selberg and
+Vaaler retain credit for the classical Fourier approximation; Laura Shou's
+primary paper provides the inspected statement. New work is Apache-2.0.

research/effective-direct-flow/REVIEW.md

@@ -0,0 +1,155 @@
+# Separate adversarial review of the effective direct-flow argument
+
+**Disposition:** the reviewed written argument proves the stated explicit
+upper majorant for the pinned historical scalar recurrence, conditional on
+the stated classical Beurling--Selberg approximation theorem and the
+authenticated predecessor flow identities. No unresolved mathematical
+objection was found in this review. This is AI-assisted review, not human
+peer review, a proof-kernel check, or physical supplier admission.
+
+Reviewed files:
+
+- `LOCAL_LIMIT.md`: SHA256
+  `07702eabadefa4e2c435d6ea7e60c781aaa786fa875cab773a5962d8d2a2efe3`.
+- `PROOF.md`: SHA256
+  `e7dbe4e1705a307e9eb32f6f06b340fb2c49948cc749110d6be2c6fb3da94ea9`.
+
+The reviewing worker did not write these two files or the numerical verifier.
+It did contribute an earlier, coarser characteristic-function separation
+estimate during discovery. Consequently the later review is not claimed to
+be wholly independent of the discovery of that ingredient. The sharper
+constants, interval smoothing, mixed-layer propagation and final induction
+were reconstructed from the submitted drafts in a separate review pass.
+The numerical source law and predecessor mathematical identities remain
+shared dependencies.
+
+## Local-limit checks
+
+The review checked the following implications directly from the written
+hypotheses, rather than treating a small numerical experiment as an all-size
+argument:
+
+1. The centered support and variance bounds give
+   `|phi(t)| <= exp(-v*t^2/3)` for `|t|<=1/6`. The Taylor remainder constant
+   is `5/6 + 9/48 = 49/48`; integrating the telescoping estimate gives
+   `147/(16n)<10/n`.
+2. Nearest-integer phases at `log 2` and `log 3`, followed by separation of
+   the distinct integers `2^q` and `3^p`, give the stated lower bound for
+   the larger phase residual. The coefficient
+   `log(2)*log(3)/(2*pi)<1/8` permits angular cutoff `2*log(n)`.
+   The two retained atom pairs give the required
+   `exp(-sqrt(n)/320)` bound for the nth characteristic-function power.
+3. With the explicitly stated angular Fourier convention, the Selberg
+   spatial defect is `2*pi/T`. The signed minorant has the same sufficient
+   absolute-integral bound as the majorant. Fourier inversion is legitimate
+   because the bounded Fourier transforms have compact support.
+4. Enlarging the majorized interval and contracting the minorized interval
+   before taking their limit handles the actual atomic law, including
+   either convention at a cap. No density of the discrete sum is assumed.
+5. Both remainder expressions used in the symbolic onset decrease on the
+   declared domain. The exact comparisons at `w=60`, and then
+   `c_sigma*2/log(n)<15/10^12<10^-8`, support the stated all-size cutoff.
+6. Layer-cake transfer is valid for the exponential half-line kernel.
+   The complement kernel is decreasing since its inner function is convex
+   with `x*Q_s'(x)>=Q_s(x)`. The derivative singularity at `x=1` does not
+   invalidate continuity or monotone Stieltjes integration.
+
+The exact finite verifier authenticates the source and establishes its atom,
+centered-moment and other numerical hypotheses. It was executed successfully
+in this review pass, as detailed below. The analytic review does not replace
+those checks or claim a formal proof of the external Selberg theorem.
+
+## Complete-flow and induction checks
+
+The review independently reconstructed the tilted normalization. A mixed
+base contributes
+`A^(G-1)*q^h*exp(-alpha*B)*exp(alpha*u)`. Dividing by the proposed
+`F_G` therefore yields the multiplier `(1-q)*q^h*c_sigma*sqrt(G)`.
+The full leaf term has coefficient `J*P(s)/121^s`; its terminal paid letter
+is unconditioned. In particular no terminal cutoff or missing factor of
+the paid rank is used.
+
+The source and boundary windows match the predecessor's strict cap tests.
+Discarding root-source capacity is safe because it is nonnegative. The
+signed-window error is bounded by the sum of absolute kernel heights, not
+by cancellation. Stieltjes integration uses the same half-open windows as
+the flow and remains valid at atoms.
+
+All three ranges of mixed layers were checked separately. In the retained
+range, conditioning on the target letters leaves a bounded shift and at
+least `n_LLT` paid letters. The middle range uses the location-uniform
+probability bound only. The last range, including zero paid letters, uses
+the trivial supremum bound and geometric weights. The omitted infinite
+geometric weight of the limiting integral is separately charged.
+
+The arithmetic quantities reconstructed in this pass include
+
+```text
+Q = 52092027504,
+3*10^-8*Q = 1562.76082512,
+8*Q/((3/500)^2*10^18) = 0.011576006112.
+```
+
+The two finite Gaussian flattening bounds, the retained-layer index limits,
+and the elementary exponential comparisons for both tails were checked.
+The leaf half-line includes every interval after 5000, with no uncharged
+truncation. Its error and all mixed errors fit the declared total 1600.
+
+Finally the exact rank-one conservation surplus is 608. This makes the
+linear function an all-rank upper solution of the complete recurrence,
+so `L(n)<=n` follows before the improved induction starts. It supplies the
+explicit initial-range constant `N0^(1-s)` without enumerating that range.
+Uniformity in the actual level offset gives every integer `N>=N0`, not
+just level starts. The strong induction includes zero complements via
+`L(0)=0`.
+
+## Diagnostic corroboration and limits
+
+The following commands were executed successfully in the isolated worktree:
+
+```text
+python -I -W error -B research/effective-direct-flow/verify.py
+python -I -W error -B research/effective-direct-flow/independent_checks.py
+python -I -W error -B research/effective-direct-flow/diagnostic.py
+```
+
+The exact verifier returned `PASS_EFFECTIVE_DIRECT_FLOW`, including the
+outward lower bound `47053.890913` for the 512-term full margin, all numerical
+premises, symbolic uniform budgets and complete-flow controls. The separate
+`Fraction` oracle checked 3969 interval pairs, 1764 valid divisions, 2205
+zero-interval rejections and 630 signed ceilings. These controls exercise the
+verifier's arithmetic implementation; they are not an independent proof of
+the analytic theorem. The rounded 90-digit Decimal diagnostic, with literal
+inventories and no repository numerical imports, gave the corroborating
+512-term margin `47053.893158567844...`. It is not an acceptance gate.
+
+A separate elementary floating calculation, importing no package engine,
+evaluated 2999 positive-binomial terms at the midpoint of the predecessor
+tilt bracket. It gave approximately
+
+```text
+K(s) = 266657973.81101257,
+V(s) = 266610919.7758388,
+K(s)-V(s) = 47054.035173773766.
+```
+
+This agrees with the claimed conservative margin `>40000` but is only a
+diagnostic. The outward rational certificate, not these floats, establishes
+the numerical acceptance decision.
+
+One minor exposition issue was reported and resolved: the local-limit
+statement now explicitly includes interval length zero, and proves the
+singleton inequality by continuity from above for shrinking positive-length
+intervals. The final amendment also explicitly defines centering at the mean
+for the general-law formulation. Both changes were checked against the
+argument; neither changes any quantitative bound. No unresolved issue from
+this review remains.
+
+The review does not establish a lower onset, a better recurrence exponent,
+the physical correctness of the raw supplier, the selected P104 construction,
+or any discharge of native, owned-erasure, compiler, precision/tape or
+analytic-recovery assumptions. The complete finite source-flow identities
+are retained predecessor mathematics, with the package's declared bounded
+checks as corroboration.
+
+Prepared for @alephnan with substantial OpenAI Codex assistance. Apache-2.0.

research/effective-direct-flow/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "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-flow-exponent-gate/PROOF.md",
+      "usage": "input",
+      "git_blob": "d9f1e340bc2cc6241392a285dbcebef35630c478",
+      "sha256": "c6c2a52e2424186db09c28792b6956aa349ad2716ea8c81bf1f0faea875be0e4"
+    },
+    {
+      "path": "research/direct-flow-exponent-gate/README.md",
+      "usage": "input",
+      "git_blob": "4abfbf70374734423ae879dd7a31de40afd42e89",
+      "sha256": "16cdebfdea1f1d660527c14974973fe87e3b2e3841d27adbcbfd376da71a8bcd"
+    },
+    {
+      "path": "research/direct-flow-exponent-gate/TASK.json",
+      "usage": "input",
+      "git_blob": "7d98de314205d788ae149c5259686953c7c58664",
+      "sha256": "b20958d698cd7432cdb1f6d398325c55f60476f7ffa2aa6aa825de164f5098c7"
+    },
+    {
+      "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": "docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md",
+      "usage": "provenance",
+      "git_blob": "26f2f6324bce57e69e861d2aae5a27c9de325a8e",
+      "sha256": "8bd158b8ef68202000f167b9b78db0b31531b5b067b5cbd91b5bf35f3ddd1ab6"
+    }
+  ]
+}