Prove an explicit finite-depth leaf tail bound (no new κ)

research/direct-flow-finite-tail/PROOF.md

@@ -0,0 +1,148 @@
+# A finite-depth exponential envelope for the direct-flow leaf deficit
+
+This is a scoped written proof. The classical Berry–Esseen inequality is an
+external theorem. The exact verifier checks the finite numerical hypotheses
+and the rational constants below. It is not a formalization of this proof.
+
+## 1. Law and result
+
+Use Ryanson Jonathan / pinterbanget's PR #4467 paid law
+
+```
+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}.
+```
+
+Write Z(s)=sum_r P_r r^s and mu(s)=Z'(s)/Z(s). Let t be the invoice
+root sum_k W_k k^t=Z(t) in [0.9973,0.9974], and let alpha be the unique
+solution mu(alpha)=a=log(5). Put lambda=t-alpha. PR #6118 supplies the
+qualitative saturation theorem, its sharper parameters and the exact
+identification of the leaf measure. They are predecessor results.
+
+Let R_i be iid with p_t(r)=P_r r^t/Z(t), S_G=sum_i log(R_i),
+B_G=G a+delta, and define the unconditioned difference Y_G=B_G-S_G.
+Conditioning is written explicitly wherever it is used.
+
+**Theorem.** For every integer G>=11000, every delta in [0,log(5)], and
+all real x>=0,
+
+    Pr_t(Y_G>=x | S_G<=B_G) <= min(1, 5 exp(-lambda x)).
+
+Consequently, for all L>=0,
+
+    E_t[(Y_G-L)_+ | S_G<=B_G] <= (5/lambda) exp(-lambda L),
+    E_t[Y_G 1_{Y_G>=L} | S_G<=B_G]
+        <= 5 (L+1/lambda) exp(-lambda L).
+
+These are finite-depth tail and truncation-error bounds, uniform across the
+whole lockstep level. They are a partial answer to PR #4467 open question 2.
+They establish neither the Bahadur–Rao asymptotic nor its error term,
+and give no rate of convergence to Exp(lambda), no full-flow share or ceiling,
+and no new kappa. The law is historical, rather than the selected P104 law.
+
+## 2. A quantitative tilted-normal lemma
+
+Let q(r)=P_r r^alpha/Z(alpha). Under q, X=log(R) has mean a, variance
+sigma^2>0 and third absolute centered moment rho. Set b=(14/25) rho/sigma^3.
+Berry–Esseen gives a Kolmogorov distance at most b/sqrt(G) between
+Y=B_G-S_G and a normal variable Z with mean delta and variance G sigma^2.
+The constant 14/25=0.56 is deliberately conservative. For example,
+[Shevtsova, arXiv:1111.6554v1](https://arxiv.org/abs/1111.6554v1), abstract
+and Corollary 1, proves an iid constant below 0.4756. Only the weaker 0.56
+bound is used here. No nonlattice local-limit or finite-depth asymptotic
+expansion is needed for this lemma.
+
+If two distribution functions are within epsilon and f has finite total
+variation and vanishes at both infinities, integration by parts bounds the
+difference of their expectations by epsilon times the total variation of f.
+For f_x(y)=exp(-lambda y) 1_{y>=x}, x>=0, that variation is
+2 exp(-lambda x). The bound remains valid at atoms, by taking one-sided
+limits of distribution functions against the continuous normal CDF. Thus,
+with c=1/(sigma sqrt(2 pi)),
+
+    sqrt(G) E_q[f_x(Y)] <= exp(-lambda x) (c/lambda+2b).       (1)
+
+Indeed, the normal density is at most c/sqrt(G) everywhere. If
+
+    sigma sqrt(G) >= a+1/lambda,
+
+then for every 0<=delta<=a and 0<=y<=1/lambda its normal density is at
+least c exp(-1/2)/sqrt(G). Integration on that interval gives
+
+    sqrt(G) E_q[f_0(Y)]
+      >= c exp(-1/2) (1-exp(-1))/lambda - 2b.                (2)
+
+Whenever the right side is positive, division of (1) by (2) is legitimate.
+For every ordered tuple, p_t(tuple)/q(tuple) is
+
+    (Z(alpha)/Z(t))^G exp(lambda B_G) exp(-lambda Y).
+
+Its common factor cancels under conditioning. Therefore E_q[f_x]/E_q[f_0]
+is exactly the desired conditional tail. This change of measure, including
+its direction and normalization, holds at finite G.
+
+## 3. Explicit constants for this law
+
+The verifier establishes the following coarse intervals with exact rational
+series. It does not reproduce PR #6118's high-precision parameter receipt.
+
+    0.9973 < t < 0.9974,
+    0.9898 < alpha < 0.9899,
+    7/1000 < lambda < 8/1000,
+    7/5 < sigma < 3/2,
+    a < 2,
+    |log(r)-a| < 5/2 for every supported r.
+
+The last bound implies rho <= (5/2) sigma^2, hence b<=1. Also
+5/2 < sqrt(2 pi) < 8/3 implies 1/4<c<2/7. Elementary exponential
+series give exp(-1/2)>3/5 and 1-exp(-1)>3/5. Consequently (2) exceeds
+
+    (1/4)(3/5)(3/5)(1000/8)-2 = 37/4,
+
+whereas the coefficient in (1) is below
+
+    (2/7)(1000/7)+2 = 2098/49 < 5(37/4).
+
+The normal-window premise follows for G>=11000 from
+
+    ((2+1000/7)/(7/5))^2 = 25704900/2401 < 11000.
+
+This proves the tail inequality. The elementary pi bounds can be weakened
+to 25/8<pi<32/9; the familiar rational bounds 3.14<pi<22/7 suffice.
+Their truth is a standard mathematical input, not an output of the verifier.
+
+The endpoint signs certify a root t by continuity. Its uniqueness on the
+stated interval follows from a strictly positive derivative of
+sum W_k k^s - sum P_r r^s, also enclosed by the verifier. The strictly
+positive variance makes mu strictly increasing, so alpha is unique.
+
+## 4. Truncation and the actual leaf observable
+
+Integrating the tail from L to infinity proves the positive-part bound.
+The identity E[Y 1_{Y>=L}]=L Pr(Y>=L)+E[(Y-L)_+] proves the second bound,
+including L=0 and distributions with atoms. A convenient mean bound is
+E[Y] <= (1+log(5))/lambda, obtained by integrating min(1,5 exp(-lambda x)).
+
+For rank N, PR #6118 identifies G=floor(log_5(N/121)),
+delta=log(N/121)-G log(5), and an independent terminal rank R with law p_t.
+Its actual leaf depth is log(121)+Y_G-log(R). The terminal rank remains
+unconditioned. For G>=11000, clipping Y_G at L changes the mean actual leaf depth
+by at most (5/lambda) exp(-lambda L). This is a deterministic error bound
+for that truncation, not a bound on distance to the limiting mean.
+
+## Credit and limits
+
+The finite-depth envelope, its explicit threshold and truncation constants
+are produced by Nick Petalas. Ryanson Jonathan / pinterbanget supplied the
+law, diagnostic and quantitative open question in PR #4467. DLamdata's
+PR #6118 supplied the saturation proof and the precise leaf-measure statement.
+zxv supplied the direct flow, Cinna Davis the refined induction, and Jacob
+Alan Sussman the lockstep compiler. Berry–Esseen, change of measure and the
+bounded-variation expectation estimate are classical ingredients.
+
+The result does not discharge any of the selected record's five assumptions.
+No selected supplier, complete flow, physical word, native theorem, numerical
+induction ceiling or complete multiplication theorem is checked here.
+Independent human and formal proof-kernel review are unclaimed. Apache-2.0.

research/direct-flow-finite-tail/README.md

@@ -0,0 +1,106 @@
+# A finite-depth tail bound for the direct-flow leaf walk
+
+This scoped proof gives the historical raw-p7 leaf law an explicit
+finite-depth exponential envelope. For all G>=11000,
+0<=delta<=log(5), and x>=0,
+
+    Pr(Y_G>=x | S_G<=G log(5)+delta) <= min(1, 5 exp(-lambda x)).
+
+Here Y_G=G log(5)+delta-S_G and lambda=t-alpha is the tilt gap defined in
+[PROOF.md](PROOF.md). The bound on clipping the deficit at L>=0 is
+
+    E[(Y_G-L)_+ | survival] <= (5/lambda) exp(-lambda L).
+
+The same bound controls the resulting error in mean actual leaf depth,
+including the independent unconditioned terminal rank. The proof also gives
+E[Y_G 1_{Y_G>=L} | survival] <= 5(L+1/lambda) exp(-lambda L).
+
+This partially answers open question 2 of Ryanson Jonathan / pinterbanget's
+[PR #4467](https://github.com/CrocSwap/integer-mult-bounds/pull/4467).
+DLamdata's [PR #6118](https://github.com/CrocSwap/integer-mult-bounds/pull/6118),
+head `6310550e932de70243fc2aaab6f4885688b6fe21`, supplies the qualitative
+saturation theorem and exact leaf-measure identification. Those predecessor
+results are cited, rather than audited or claimed here. The new step uses
+Berry–Esseen and bounded-variation integration to replace an unspecified tail
+constant and onset by explicit finite values.
+
+This does not establish a Bahadur–Rao asymptotic or its error term, a rate of
+convergence to the exponential law, stable full-flow shares, a numerical
+induction ceiling, supplier admission or a new kappa. The selected PR6030
+record and its five assumptions are unchanged. This is historical compiler
+side work, not a selected-frontier improvement.
+
+## Reproduce
+
+Python 3.12, standard library only. From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/direct-flow-finite-tail/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/direct-flow-finite-tail
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/direct-flow-finite-tail --check-source-history
+```
+
+Other reviewers can replace the interpreter path with their CPython 3.12.
+The principal marker is `PASS_DIRECT_FLOW_FINITE_TAIL`. Each direct run prints
+a generated JSON receipt binding all six package files by SHA256. It writes
+nothing to the checkout. The registered normal and optimized commands repeat
+the exact numerical gates and rejecting controls with no dependence on Python
+assertions. Source laws are parsed as literals from the authenticated pinned
+file; no predecessor code executes.
+
+The certificate encloses only the coarse hypotheses needed by the new bound,
+not the predecessor's high-precision result. Logarithms use 48 terms of the
+atanh series after power-of-two reduction. Exponentials use 32 terms after
+scaling by 16, with geometric remainder bounds and four outward-rounded
+squarings. All acceptance decisions use integers or rational intervals.
+Finite Bernoulli fixtures separately check the tilt ratio and clipping
+identity at atoms. The written proof and the external Berry–Esseen theorem
+carry the universal probability claim; finite fixtures do not replace them.
+
+## Verification boundaries
+
+The exact source closure is in [SOURCES.json](SOURCES.json). The base is
+`721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8.
+The source question and advisory claim are recorded in [TASK.json](TASK.json).
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241861)
+precedes substantial work. PR6118's separate power-tariff follow-up concerns
+asymptotic moments, while this result gives a finite-depth tail envelope.
+
+No selected cold replay, full historical flow replay, native or physical
+program, Lean proof or complete multiplication theorem is run. The classical
+Berry–Esseen inequality and elementary pi bounds are external mathematical
+inputs. Independent human and formal proof-kernel review are unclaimed.
+
+The verifier uses bounded nonrecursive loops. It reads four fixed source
+records, parses an authenticated source with at most 100 top-level statements,
+and processes two supports of nine ranks no larger than 121. The finite-word
+fixtures stop at depth eight, with at most 256 words in a fixture. Functions
+stay below 60 lines. Every gate fails through an explicit exception, including
+under optimized Python. The JSON serializer has one fixed callback target.
+
+Power-of-Ten rule 3 has a managed-runtime deviation in `verify.py`: Python
+allocates Fraction integers and collections during execution. Fixed input
+inventories, fixed series lengths, 128-bit outward rounding and the depth-eight
+fixture cap bound the live workload. Source files are capped at one million
+bytes. The registered normal and optimized checks exercise this bounded path.
+A fixed-memory implementation would require a different arithmetic runtime;
+no such implementation or physical resource claim is made. Diagnostics use
+Python development mode and warnings as errors in local verification.
+
+## Open next questions
+
+Can an effective nonlattice interval local-limit bound give an explicit
+*decreasing* error for the distribution or mean relative to its exponential
+limit? This would quantify the onset of saturation. A first step is to pair
+such a remainder with the finite tail envelope proved here. The missing input
+is a quantitative local-limit estimate, not another tail-constant search.
+
+## Credit
+
+The finite-depth envelope and explicit truncation constants are produced by
+Nick Petalas. Ryanson Jonathan / pinterbanget supplied the fixed law and the
+explicit-constant question in PR4467. DLamdata supplied the saturation theorem
+and exact leaf observable in PR6118. zxv supplied the direct flow, Cinna Davis
+the refined induction, and Jacob Alan Sussman the lockstep compiler. The
+Berry–Esseen inequality, change of measure and bounded-variation estimate are
+classical. Predecessor files and credit lines remain unchanged. Apache-2.0.

research/direct-flow-finite-tail/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/verify.py",
+      "usage": "input",
+      "git_blob": "42440e630a46c6e581797f52bfb4c0c87bbdac3a",
+      "sha256": "2030d79d7f136b39b4e2a3f5b033af4bba18ab87579ec352267dc1697e02157d"
+    }
+  ]
+}

research/direct-flow-finite-tail/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "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"
+    ],
+    "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "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": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "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 an explicit finite-depth exponential tail and truncation-error envelope for the fixed PR4467 direct-flow leaf law.",
+  "scope_change_reason": "This takes PR4467 open question 2 as a scoped historical compiler side result, rather than claiming to discharge a selected P104 assumption. The source question is distinct from the concurrent PR6118 power-tariff phase-transition target.",
+  "bottleneck_link": "Quantitative control of conditioned leaf depth makes finite-depth truncation errors assessable. This historical raw-p7 lemma does not change the selected supplier, compiler or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first exact finite-depth tail envelope with a written proof and bounded certificate; leave convergence rates and full-flow shares open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py; runtime receipts bind all six package files by SHA256.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one bound the finite-G distance from the exponential limit or the limiting mean with an explicit decreasing error?",
+      "why_it_matters": "The envelope bounds truncation error but does not locate the onset of saturation accurately.",
+      "first_step": "Combine an effective interval local-limit estimate with the existing finite tail envelope.",
+      "blocked_by": "No quantitative nonlattice local-limit remainder is supplied."
+    }
+  ],
+  "coordination": {
+    "source_question": "PR #4467 open question 2",
+    "source_author": "pinterbanget",
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241861",
+    "predecessor": "PR #6118 at 6310550e932de70243fc2aaab6f4885688b6fe21"
+  },
+  "environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS arm64",
+    "dependencies": "standard library only"
+  },
+  "claim_type": "scoped written proof with finite exact numerical certificate"
+}