From 04da76ebfb827cabb3560d3c65edee908f39df63 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 05:48:04 +0700 Subject: [PATCH 1/2] research: #4436 direct exponent gate reduces to a uniform boundary-exit share (lemma + p7 scan) Co-Authored-By: Claude Opus 5.5 --- research/direct-flow-boundary-share/README.md | 82 ++++++++++++++ .../direct-flow-boundary-share/SOURCES.json | 18 +++ research/direct-flow-boundary-share/TASK.json | 100 +++++++++++++++++ .../direct-flow-boundary-share/VERIFY.json | 18 +++ research/direct-flow-boundary-share/verify.py | 105 ++++++++++++++++++ 5 files changed, 323 insertions(+) create mode 100644 research/direct-flow-boundary-share/README.md create mode 100644 research/direct-flow-boundary-share/SOURCES.json create mode 100644 research/direct-flow-boundary-share/TASK.json create mode 100644 research/direct-flow-boundary-share/VERIFY.json create mode 100644 research/direct-flow-boundary-share/verify.py diff --git a/research/direct-flow-boundary-share/README.md b/research/direct-flow-boundary-share/README.md new file mode 100644 index 0000000000..9864a7043f --- /dev/null +++ b/research/direct-flow-boundary-share/README.md @@ -0,0 +1,82 @@ +# #4436's direct-exponent gate reduces to a uniform boundary-exit share + +**Claim type:** a written conditional lemma plus numerical evidence. **No new κ, and no proof of the +uniform bound.** It addresses zxv's [#4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436) +open exponent gate. #4436 notes that its direct flow for overlapping ranks creates *boundary exits* +of rank greater than `k_min·n/m`, "near the upper boundary", which "cannot be assigned the old bound". + +## Lemma (conditional) + +The setting is #4436's direct flow at top rank `n ≥ m`, with an exponent `t` above the unit's mixed +root and `z0 = t + δ`. Assume: + +- **(A) Potential.** `Σ_e x_e e^t ≤ Σ_s w_s s^t` over all exits. This holds because matched jobs + cancel and each unit's paid `t`-potential is at most its target potential. +- **(B) Ranks.** Sources satisfy `n/m < s ≤ n`. Boundary exits satisfy `e ≤ r_max·n/m`. Leaf exits + satisfy `e ≤ E(n) = r_max(n/m)^θ`. +- **(C) Boundary share.** `Σ_boundary x_e e^t ≤ β Σ_s w_s s^t`, uniformly in `n`. + +Then the exit coefficient obeys + + κ(n) = Σ_e x_e e^(z0) / Σ_s w_s s^(z0) ≤ β·r_max^δ + (m E(n)/n)^δ. + +**Proof.** Boundary part: +`Σ_b x_e e^(z0) ≤ (r_max n/m)^δ Σ_b x_e e^t ≤ (r_max n/m)^δ β Σ w_s s^t ≤ β r_max^δ Σ w_s s^(z0)`, +using `s > n/m`. Leaf part: `Σ_l x_e e^(z0) ≤ E^δ Σ_l x_e e^t ≤ E^δ Σ w_s s^t ≤ (mE/n)^δ Σ w_s s^(z0)`, +using (A). ∎ + +#4405's refined induction needs only `κ(n) ≤ η = z0·m^(z0−1)` for all `n` beyond an explicit +threshold. Since `(mE/n)^δ → 0`, the induction closes if `β·r_max^δ < η`, and the direct flow then +attains every saving below the unit's root, with an explicit finite rank. For raw p7, `m = 121`, +`r_max = 48` and `η ≈ 0.984`, so the condition is roughly `β < 0.98`. + +So the gate reduces to proving a **uniform boundary-exit share bound** (C) with `β < η·r_max^{−δ}`. + +## Evidence for (C) on raw p7 + +`verify.py` uses an independent implementation of #4436's flow, the same as in my #4456. It scans +3,394 ranks: every `N` from 121 to 3,000, plus a 1% geometric grid up to 495,968. At each rank it +checks exactly that exits are at most `r_max·N/m`, that leaf exits are at most `r_max^(G+1)`, and the +rank-one potential identity. It then computes `β(N)` at `t = 1 − 0.0026865`: + +| | value | +| --- | --- | +| maximum `β(N)` | **0.1545**, at `N = 1089` | +| typical `β(N)` for `N ≥ 10⁴` | 0.075–0.11 | +| maximum `exit/N` | 0.39669 = 48/121, the bound attained | + +The observed `β` sits far below the roughly 0.98 that the lemma needs. These are finite floating-point +measurements, not a proof. + +## Not covered + +- **A proof of (C)**, which needs counting the omitted Pascal terms at the top boundary. +- **The explicit rank and outer ledger** for a direct-flow endpoint. +- **Native premises.** + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/direct-flow-boundary-share --check-only +python3.12 -B scripts/research_package.py --package research/direct-flow-boundary-share +``` + +The verifier prints `PASS_DIRECT_FLOW_BOUNDARY_SHARE` in about 50 seconds, using only the standard +library. + +## Open next questions + +1. **Prove a uniform bound on the boundary-exit `t`-potential share.** + - *Why it matters:* it would close #4436's exponent gate, giving the direct saving without + tensoring. + - *First step:* boundary exits occur at points `b` with `m·ρ·r·c(b)/k > n` for some `k`. Bound + their `u(b)`-weighted potential by the multinomial mass of the last layer. + +## Credit + +- The direct flow and the gate are zxv's (#4436). +- The refined induction is 1337isnot1337's (#4405). +- The lockstep construction is Jacob Alan Sussman's Theorem 1G. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/direct-flow-boundary-share/SOURCES.json b/research/direct-flow-boundary-share/SOURCES.json new file mode 100644 index 0000000000..9124bb10fe --- /dev/null +++ b/research/direct-flow-boundary-share/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/direct-flow-boundary-share/TASK.json b/research/direct-flow-boundary-share/TASK.json new file mode 100644 index 0000000000..183cbc53e7 --- /dev/null +++ b/research/direct-flow-boundary-share/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "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_status": "refined", + "actual_scope": "Reduce #4436's open direct-exponent gate to a uniform boundary-exit t-potential share bound (written lemma) and measure that share on raw p7.", + "scope_change_reason": "Follow-up to #4456; #4436 left the direct exponent gate open.", + "bottleneck_link": "A direct-flow exponent would remove the tensor/padding step behind the kappa ~0.0027-0.0030 claims.", + "budget_minutes": 30, + "stop_rule": "Stop at the conditional lemma and measurements.", + "outcome": "completed", + "evidence": "Lemma: kappa_exit <= beta r_max^delta + (mE/n)^delta, so the refined induction closes if beta r_max^delta < eta (~0.984 for p7). Measured max beta 0.1545 over 3,394 ranks to 5e5.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Prove a uniform bound on the boundary-exit t-potential share.", + "why_it_matters": "It would close #4436's exponent gate.", + "first_step": "Bound the u(b)-weighted potential of boundary points by the last-layer multinomial mass.", + "blocked_by": "None." + } + ] +} diff --git a/research/direct-flow-boundary-share/VERIFY.json b/research/direct-flow-boundary-share/VERIFY.json new file mode 100644 index 0000000000..ae1058e63c --- /dev/null +++ b/research/direct-flow-boundary-share/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Independent #4436 direct flow on raw p7 at 3,394 ranks (121..495,968): exits <= r_max N/m, leaf exits <= r_max^(G+1), exact potential identity; maximum boundary-exit t-potential share below 0.16 (observed 0.1545)." + } + ] +} diff --git a/research/direct-flow-boundary-share/verify.py b/research/direct-flow-boundary-share/verify.py new file mode 100644 index 0000000000..cd104e64af --- /dev/null +++ b/research/direct-flow-boundary-share/verify.py @@ -0,0 +1,105 @@ +#!/usr/bin/env python3 +"""Boundary-exit potential share in #4436's direct p7 flow (evidence for a conditional reduction). + +Using an independent implementation of #4436's partially matched flow (the same as research/pr4436-direct-flow-check), +for every rank 121 <= N <= 3000 and a 1%-geometric grid up to 5*10^5 this computes + beta(N) = sum over boundary exits x_e e^t / sum over sources w_s s^t, t = 1 - 0.0026865, +and checks: every exit is at most r_max N / m (r_max = 48, m = 121), every leaf exit is at most r_max^(G+1), the +exact rank-one potential identity holds, and max beta < 0.16 (observed 0.1545). Floating-point shares are +numerical evidence for the README's conditional lemma, not a proof of a uniform bound. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import json +import sys + +from fractions import Fraction as Q +from math import factorial +def multis(n_types, size): + if n_types == 0: + if size == 0: yield () + return + for x in range(size + 1): + for rest in multis(n_types - 1, size - x): yield (x,) + rest +def flow(N, W, P): + ks = sorted(W); m = ks[-1]; kmin = ks[0] + def c(a): + v = 1 + for k, x in zip(ks, a): v *= k ** x + return v + def u(a): + v = factorial(sum(a)) + for k, x in zip(ks, a): v = v // factorial(x) * W[k] ** x + return v + G = 0 + while kmin ** (G + 1) <= N // m: G += 1 + F = [{1: 1}] + for d in range(1, G + 1): + nxt = {} + for rho, cnt in F[d - 1].items(): + for r, pr in P.items(): + if m * rho * r <= N: nxt[rho * r] = nxt.get(rho * r, 0) + cnt * pr + F.append(nxt) + S, X, BX = {}, {}, {} + col = units = matched = 0 + add = lambda D, k, v: D.__setitem__(k, D.get(k, 0) + v) + present = lambda rho, a: m * rho * c(a) <= N + for d in range(G + 1): + for rho, cnt in F[d].items(): + for b in multis(len(ks), G - d): + if not present(rho, b): continue + units += cnt * u(b); col += cnt * u(b) * rho * c(b) + for r, pr in P.items(): + issued = cnt * pr * u(b); rank = r * rho * c(b) + if d == G: + add(X, rank, issued); continue + D = sum(W[k] * u(tuple(x - (i == j) for j, x in enumerate(b))) + for i, k in enumerate(ks) if b[i] > 0 and present(rho * r, tuple(x - (i == j) for j, x in enumerate(b)))) + matched += cnt * pr * D + if issued - cnt * pr * D: + add(X, rank, issued - cnt * pr * D); add(BX, rank, issued - cnt * pr * D) + for a in multis(len(ks), G): + if present(1, a): + for k in ks: add(S, k * c(a), W[k] * u(a)) + for d in range(1, G + 1): + for rho, cnt in F[d - 1].items(): + for r, pr in P.items(): + for a in multis(len(ks), G - d): + if not present(rho * r, a): continue + for i, k in enumerate(ks): + b = list(a); b[i] += 1 + if not present(rho, tuple(b)): + add(S, rho * r * c(tuple(b)), cnt * pr * u(a) * W[k]) + return dict(G=G, S=S, X=X, BX=BX, col=col, units=units, matched=matched) + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def main(): + W = {5: 420, 6: 270, 7: 840, 8: 1395, 9: 3195, 25: 448, 41: 448, 57: 448, 121: 224} + P = {1: 37305, 2: 10695, 3: 3360, 4: 1530, 5: 300, 8: 1464, 16: 448, 32: 448, 48: 448} + m, rmax, surplus = 121, 48, 608 + t = 1 - 0.0026865 + Ns = sorted(set(list(range(121, 3001)) + [int(121 * 1.01 ** k) for k in range(0, 850)])) + Ns = [n for n in Ns if n <= 500000] + best, at = 0.0, None + for N in Ns: + r = flow(N, W, P) + need(all(e * m <= rmax * N for e in r["X"]), f"N={N}: exits <= r_max N/m") + need(all(e <= rmax ** (r["G"] + 1) or e in r["BX"] for e in r["X"]), f"N={N}: leaf exits <= r_max^(G+1)") + need(sum(s * v for s, v in r["S"].items()) - sum(e * v for e, v in r["X"].items()) == surplus * r["col"], + f"N={N}: potential identity") + st = sum(v * s ** t for s, v in r["S"].items()) + bt = sum(v * e ** t for e, v in r["BX"].items()) + if bt / st > best: + best, at = bt / st, N + need(best < 0.16, "max boundary share below 0.16") + print(json.dumps({"status": "PASS_DIRECT_FLOW_BOUNDARY_SHARE", "ranks_scanned": len(Ns), "max_N": Ns[-1], + "max_boundary_share": round(best, 6), "at_N": at, "eta_reference": 0.984, + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main()) From 488a75a9e95e14448b6301719249f876f3999931 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 06:05:02 +0700 Subject: [PATCH 2/2] Correct #4459: leaf exits dominate; add exact mirror identity and rigorous boundary-share bound Co-Authored-By: Claude Opus 5.5 --- research/direct-flow-boundary-share/README.md | 106 ++++++++++-------- research/direct-flow-boundary-share/TASK.json | 10 +- .../direct-flow-boundary-share/VERIFY.json | 2 +- research/direct-flow-boundary-share/verify.py | 98 ++++++++++++++-- 4 files changed, 156 insertions(+), 60 deletions(-) diff --git a/research/direct-flow-boundary-share/README.md b/research/direct-flow-boundary-share/README.md index 9864a7043f..a9c718b8e3 100644 --- a/research/direct-flow-boundary-share/README.md +++ b/research/direct-flow-boundary-share/README.md @@ -1,58 +1,72 @@ -# #4436's direct-exponent gate reduces to a uniform boundary-exit share +# #4436's boundary exits: a mirror identity, a rigorous share bound, and a correction -**Claim type:** a written conditional lemma plus numerical evidence. **No new κ, and no proof of the -uniform bound.** It addresses zxv's [#4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436) -open exponent gate. #4436 notes that its direct flow for overlapping ranks creates *boundary exits* -of rank greater than `k_min·n/m`, "near the upper boundary", which "cannot be assigned the old bound". +**Claim type:** an exact identity and a rigorous uniform bound for #4436's boundary exits, plus a +**correction** to this package's first version and finite measurements of the true exit coefficient. +**No new κ.** It concerns zxv's [#4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436) +open direct-exponent gate. -## Lemma (conditional) +## Correction to the first version -The setting is #4436's direct flow at top rank `n ≥ m`, with an exponent `t` above the unit's mixed -root and `z0 = t + δ`. Assume: +The first version (head `04da76eb`) claimed that the gate reduces to a uniform boundary-exit share +bound. That claim is **wrong**. -- **(A) Potential.** `Σ_e x_e e^t ≤ Σ_s w_s s^t` over all exits. This holds because matched jobs - cancel and each unit's paid `t`-potential is at most its target potential. -- **(B) Ranks.** Sources satisfy `n/m < s ≤ n`. Boundary exits satisfy `e ≤ r_max·n/m`. Leaf exits - satisfy `e ≤ E(n) = r_max(n/m)^θ`. -- **(C) Boundary share.** `Σ_boundary x_e e^t ≤ β Σ_s w_s s^t`, uniformly in `n`. +- **The flaw.** Its lemma assumed leaf exits have rank `E(n) = o(n)`, so that their term + `(mE/n)^δ` vanishes. In #4436's direct flow this is false. Leaf exits `rρ` with `ρ ∈ F[G]` reach + **0.397·N**, and they carry **85–92 %** of the source `t`-potential at every scanned rank. +- **What stands.** The lemma is still valid as a conditional statement, but its leaf hypothesis + fails here. +- **What controls the gate.** The total exit coefficient, measured below. -Then the exit coefficient obeys +## Mirror identity (exact) - κ(n) = Σ_e x_e e^(z0) / Σ_s w_s s^(z0) ≤ β·r_max^δ + (m E(n)/n)^δ. +Use #4436's lockstep nodes. A *base* is a pair `(ρ, a)` with `ρ ∈ F[d]`, `|a| = G−d−1` and +`0 ≤ d < G`, of weight `μ = cnt(ρ)·u(a)` and size `z = ρ·c(a)`. Write `I(x) = m z/N ∈ x` for the +window condition. Then: -**Proof.** Boundary part: -`Σ_b x_e e^(z0) ≤ (r_max n/m)^δ Σ_b x_e e^t ≤ (r_max n/m)^δ β Σ w_s s^t ≤ β r_max^δ Σ w_s s^(z0)`, -using `s > n/m`. Leaf part: `Σ_l x_e e^(z0) ≤ E^δ Σ_l x_e e^t ≤ E^δ Σ w_s s^t ≤ (mE/n)^δ Σ w_s s^(z0)`, -using (A). ∎ + boundary exits = Σ_{r>k} P_r W_k · [base (ρ,a) with I(1/r, 1/k]] at rank r k z, + sources = Σ_{k>r} P_r W_k · [base (ρ,a) with I(1/k, 1/r]] at rank r k z + top layer. -#4405's refined induction needs only `κ(n) ≤ η = z0·m^(z0−1)` for all `n` beyond an explicit -threshold. Since `(mE/n)^δ → 0`, the induction closes if `β·r_max^δ < η`, and the direct flow then -attains every saving below the unit's root, with an explicit finite rank. For raw p7, `m = 121`, -`r_max = 48` and `η ≈ 0.984`, so the condition is roughly `β < 0.98`. +An exit occurs where node `(ρ, a+e_k)` is present but `(ρr, a)` is absent. A source occurs where +`(ρr, a)` is present but `(ρ, a+e_k)` is absent. So exits and inner sources are the same base measure +seen through mirrored windows. `verify.py` checks both equalities exactly, as multisets, at +`N = 1089, 3000, 20000` and `100000`. -So the gate reduces to proving a **uniform boundary-exit share bound** (C) with `β < η·r_max^{−δ}`. +## Rigorous uniform bound on the boundary share -## Evidence for (C) on raw p7 +Let `M(J) = Σ_{bases in J} μ z^t`. Split the windows into elementary intervals `J` cut at the +points `1/r` and `1/k`. Then exits `= Σ_J E_J M(J)` and inner sources `= Σ_J S_J M(J)`, where +`E_J` and `S_J` sum `P_r W_k (rk)^t` over the exit and source windows covering `J`. Every exit window +lies inside `(1/48, 1/5]`, and each of its pieces is covered by source windows. Hence, for every `N`: -`verify.py` uses an independent implementation of #4436's flow, the same as in my #4456. It scans -3,394 ranks: every `N` from 121 to 3,000, plus a 1% geometric grid up to 495,968. At each rank it -checks exactly that exits are at most `r_max·N/m`, that leaf exits are at most `r_max^(G+1)`, and the -rank-one potential identity. It then computes `β(N)` at `t = 1 − 0.0026865`: + β(N) ≤ max_J E_J / S_J = 0.3208 (raw p7, t = 1 − 0.0026865). -| | value | -| --- | --- | -| maximum `β(N)` | **0.1545**, at `N = 1089` | -| typical `β(N)` for `N ≥ 10⁴` | 0.075–0.11 | -| maximum `exit/N` | 0.39669 = 48/121, the bound attained | +The measured maximum is 0.1545. Even the crude cover bound, which compares all exits against the +source pairs `r ≤ 5`, `k ≥ 57` only, gives 0.753. So hypothesis (C) of the first version is now a +theorem. It is no longer the bottleneck. -The observed `β` sits far below the roughly 0.98 that the lemma needs. These are finite floating-point -measurements, not a proof. +## The exit coefficient, measured + +This is the quantity #4405's refined induction actually needs: + + κ(N, z0) = Σ x_e e^{z0} / Σ w_s s^{z0}, with κ ≤ η = z0·m^{z0−1} required. + +At `t` the exit and source potentials balance (κ = 1.000000), and κ falls only slowly as `z0` rises. + +| saving `1−z0` | η | sup κ, N ≥ 10³ | N ≥ 10⁴ | N ≥ 10⁵ | N ≥ 3·10⁵ | +| --- | --- | --- | --- | --- | --- | +| 0.002 | 0.98847 | 0.99864 | 0.99826 | 0.99807 | 0.99798 | +| 0.001 | 0.99422 | 0.99667 | 0.99573 | 0.99526 | 0.99504 | +| 0.0008 | 0.99537 | 0.99628 | 0.99523 | 0.99470 | **0.99445** | + +Through `N ≤ 5·10⁵`, the refined-induction test with the direct flow passes at saving 0.0008 for +`N ≥ 3·10⁵`, and fails at 0.001. That agrees with the effective saving of about 0.0008 that #4456 +measured near `N = 3·10⁴`. The slow downward drift of sup κ is finite evidence only. ## Not covered -- **A proof of (C)**, which needs counting the omitted Pascal terms at the top boundary. -- **The explicit rank and outer ledger** for a direct-flow endpoint. -- **Native premises.** +- Any asymptotic statement about κ(N, z0). +- An explicit-rank endpoint. +- Native premises. ## Reproduce @@ -61,16 +75,18 @@ python3.12 -B scripts/research_package.py --package research/direct-flow-boundar python3.12 -B scripts/research_package.py --package research/direct-flow-boundary-share ``` -The verifier prints `PASS_DIRECT_FLOW_BOUNDARY_SHARE` in about 50 seconds, using only the standard +The verifier prints `PASS_DIRECT_FLOW_BOUNDARY_SHARE` in about 35 seconds, using only the standard library. ## Open next questions -1. **Prove a uniform bound on the boundary-exit `t`-potential share.** - - *Why it matters:* it would close #4436's exponent gate, giving the direct saving without - tensoring. - - *First step:* boundary exits occur at points `b` with `m·ρ·r·c(b)/k > n` for some `k`. Bound - their `u(b)`-weighted potential by the multinomial mass of the last layer. +1. **Do the leaf exits admit a mirror-type comparison with the sources?** + - *Why it matters:* leaf exits are about 90 % of the exit potential, so they decide κ. + - *First step:* write leaf exits `rρ` (`ρ ∈ F[G]`) and last-layer sources over a common base, as + above. +2. **Does sup κ(N, z0) converge, and to what?** + - *Why it matters:* it decides the direct saving. + - *First step:* a renewal-type analysis of the tilted base measure near `log(N/m)`. ## Credit diff --git a/research/direct-flow-boundary-share/TASK.json b/research/direct-flow-boundary-share/TASK.json index 183cbc53e7..4b41ba78d6 100644 --- a/research/direct-flow-boundary-share/TASK.json +++ b/research/direct-flow-boundary-share/TASK.json @@ -80,20 +80,20 @@ ] }, "scope_status": "refined", - "actual_scope": "Reduce #4436's open direct-exponent gate to a uniform boundary-exit t-potential share bound (written lemma) and measure that share on raw p7.", + "actual_scope": "#4436's boundary exits: exact mirror identity, rigorous uniform share bound 0.3208, and a correction (leaf exits dominate) with the measured exit coefficient vs eta.", "scope_change_reason": "Follow-up to #4456; #4436 left the direct exponent gate open.", "bottleneck_link": "A direct-flow exponent would remove the tensor/padding step behind the kappa ~0.0027-0.0030 claims.", "budget_minutes": 30, "stop_rule": "Stop at the conditional lemma and measurements.", "outcome": "completed", - "evidence": "Lemma: kappa_exit <= beta r_max^delta + (mE/n)^delta, so the refined induction closes if beta r_max^delta < eta (~0.984 for p7). Measured max beta 0.1545 over 3,394 ranks to 5e5.", + "evidence": "Mirror identity exact at 4 ranks; beta <= 0.3208 for all N (measured max 0.1545). Correction: leaf exits reach 0.397N with 85-92% of the t-potential, so the first version's reduction fails. Refined-induction test passes at saving 0.0008 and fails at 0.001 through N<=5e5.", "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", "open_questions": [ { - "question": "Prove a uniform bound on the boundary-exit t-potential share.", - "why_it_matters": "It would close #4436's exponent gate.", - "first_step": "Bound the u(b)-weighted potential of boundary points by the last-layer multinomial mass.", + "question": "Do leaf exits admit a mirror-type comparison with sources?", + "why_it_matters": "They carry ~90% of the exit potential and decide kappa.", + "first_step": "Write leaf exits and last-layer sources over a common base.", "blocked_by": "None." } ] diff --git a/research/direct-flow-boundary-share/VERIFY.json b/research/direct-flow-boundary-share/VERIFY.json index ae1058e63c..b2b4795ff5 100644 --- a/research/direct-flow-boundary-share/VERIFY.json +++ b/research/direct-flow-boundary-share/VERIFY.json @@ -12,7 +12,7 @@ "{package}/verify.py" ], "timeout_seconds": 300, - "checks": "Independent #4436 direct flow on raw p7 at 3,394 ranks (121..495,968): exits <= r_max N/m, leaf exits <= r_max^(G+1), exact potential identity; maximum boundary-exit t-potential share below 0.16 (observed 0.1545)." + "checks": "Independent #4436 direct flow on raw p7 at 3,394 ranks: exit rank bound, exact potential identity, exact mirror identity (boundary exits/sources as mirrored windows of one base measure) at 4 ranks, boundary share below the rigorous mirror bound 0.3208, leaf exits dominate (correction), exit coefficient vs eta table." } ] } diff --git a/research/direct-flow-boundary-share/verify.py b/research/direct-flow-boundary-share/verify.py index cd104e64af..44db6538ad 100644 --- a/research/direct-flow-boundary-share/verify.py +++ b/research/direct-flow-boundary-share/verify.py @@ -1,12 +1,16 @@ #!/usr/bin/env python3 -"""Boundary-exit potential share in #4436's direct p7 flow (evidence for a conditional reduction). +"""Boundary-exit potential share in #4436's direct p7 flow: mirror identity, a rigorous uniform bound, and the +correction that leaf exits (not boundary exits) dominate the exit coefficient. Using an independent implementation of #4436's partially matched flow (the same as research/pr4436-direct-flow-check), for every rank 121 <= N <= 3000 and a 1%-geometric grid up to 5*10^5 this computes beta(N) = sum over boundary exits x_e e^t / sum over sources w_s s^t, t = 1 - 0.0026865, -and checks: every exit is at most r_max N / m (r_max = 48, m = 121), every leaf exit is at most r_max^(G+1), the -exact rank-one potential identity holds, and max beta < 0.16 (observed 0.1545). Floating-point shares are -numerical evidence for the README's conditional lemma, not a proof of a uniform bound. +and checks: every exit is at most r_max N / m (r_max = 48, m = 121), the exact rank-one potential identity, and +max beta < 0.16 (observed 0.1545). It also checks EXACTLY, at four ranks, the mirror identity: boundary exits and inner +sources are one base measure seen through windows (1/r, 1/k] and (1/k, 1/r]; this gives the uniform bound +beta <= max_J E_J / S_J ~ 0.3208 over elementary windows J. CORRECTION (README): leaf exits reach ~0.384 N and carry +~85-92% of the t-potential, so the earlier "leaf term vanishes" hypothesis is false; the exit coefficient +kappa(N, z0) is recorded against eta(z0) instead. Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. """ import json @@ -77,28 +81,104 @@ def need(condition, message): raise AssertionError(message) +def mirror_bound(W, P, t): + """max over elementary windows J of E_J / S_J (floats; margins are large)""" + pts = sorted({Q(1, x) for x in list(P) + list(W)}) + best = 0.0 + for lo, hi in zip(pts, pts[1:]): + mid = (lo + hi) / 2 + E = sum(P[r] * W[k] * (r * k) ** t for r in P for k in W if r > k and Q(1, r) < mid <= Q(1, k)) + S = sum(P[r] * W[k] * (r * k) ** t for r in P for k in W if k > r and Q(1, k) < mid <= Q(1, r)) + if E > 0: + need(S > 0, "every exit window is covered by source windows") + best = max(best, E / S) + return best + + +def mirror_identity(N, W, P, m, r): + """exact: BX and S equal the mirrored windows of the base measure mu(z), z = rho c(a)""" + ks = sorted(W) + G = r["G"] + F = [{1: 1}] + for d in range(1, G + 1): + nxt = {} + for rho, cnt in F[d - 1].items(): + for rr, pr in P.items(): + if m * rho * rr <= N: + nxt[rho * rr] = nxt.get(rho * rr, 0) + cnt * pr + F.append(nxt) + mu = {} + for d in range(G): + for rho, cnt in F[d].items(): + for a in multis(len(ks), G - d - 1): + c, u = 1, factorial(sum(a)) + for k, x in zip(ks, a): + c *= k ** x + u = u // factorial(x) * W[k] ** x + mu[rho * c] = mu.get(rho * c, 0) + cnt * u + bx, src = {}, {} + for z, w in mu.items(): + for rr in P: + for k in W: + if rr > k and N < m * z * rr and m * z * k <= N: + bx[rr * k * z] = bx.get(rr * k * z, 0) + P[rr] * W[k] * w + if k > rr and N < m * z * k and m * z * rr <= N: + src[rr * k * z] = src.get(rr * k * z, 0) + P[rr] * W[k] * w + for a in multis(len(ks), G): + c, u = 1, factorial(G) + for k, x in zip(ks, a): + c *= k ** x + u = u // factorial(x) * W[k] ** x + if m * c <= N: + for k in ks: + src[k * c] = src.get(k * c, 0) + W[k] * u + need(bx == {e: v for e, v in r["BX"].items() if v}, f"N={N}: boundary exits are the mirrored windows") + need(src == r["S"], f"N={N}: sources are the mirrored windows plus the top layer") + + def main(): W = {5: 420, 6: 270, 7: 840, 8: 1395, 9: 3195, 25: 448, 41: 448, 57: 448, 121: 224} P = {1: 37305, 2: 10695, 3: 3360, 4: 1530, 5: 300, 8: 1464, 16: 448, 32: 448, 48: 448} m, rmax, surplus = 121, 48, 608 t = 1 - 0.0026865 + savings = (0.002, 0.001, 0.0008) Ns = sorted(set(list(range(121, 3001)) + [int(121 * 1.01 ** k) for k in range(0, 850)])) Ns = [n for n in Ns if n <= 500000] - best, at = 0.0, None + best, at, leaf_min, leaf_rank = 0.0, None, 1.0, 0.0 + kap = {s: {} for s in savings} for N in Ns: r = flow(N, W, P) need(all(e * m <= rmax * N for e in r["X"]), f"N={N}: exits <= r_max N/m") - need(all(e <= rmax ** (r["G"] + 1) or e in r["BX"] for e in r["X"]), f"N={N}: leaf exits <= r_max^(G+1)") need(sum(s * v for s, v in r["S"].items()) - sum(e * v for e, v in r["X"].items()) == surplus * r["col"], f"N={N}: potential identity") + if N in (1089, 3000, 20000, 100000): + mirror_identity(N, W, P, m, r) st = sum(v * s ** t for s, v in r["S"].items()) bt = sum(v * e ** t for e, v in r["BX"].items()) if bt / st > best: best, at = bt / st, N - need(best < 0.16, "max boundary share below 0.16") + if r["G"] >= 1: + leaf = {e: v - r["BX"].get(e, 0) for e, v in r["X"].items() if v != r["BX"].get(e, 0)} + leaf_min = min(leaf_min, sum(v * e ** t for e, v in leaf.items()) / st) + leaf_rank = max(leaf_rank, max(leaf) / N) + if N >= 1000: + for s in savings: + z = 1 - s + kap[s][N] = sum(v * e ** z for e, v in r["X"].items()) / sum(v * x ** z for x, v in r["S"].items()) + bound = mirror_bound(W, P, t) + need(best < 0.16 and best <= bound < 0.33, "boundary share below the rigorous mirror bound") + need(leaf_min > 0.8 and leaf_rank > 0.38, "leaf exits dominate and reach Theta(N): the leaf hypothesis fails") + table = {} + for s in savings: + eta = (1 - s) * m ** (-s) + table[str(s)] = {"eta": round(eta, 6), **{f"sup_kappa_N>={th:g}": round(max(v for N, v in kap[s].items() + if N >= th), 6) for th in (1e3, 1e4, 1e5, 3e5)}} + need(max(v for N, v in kap[0.0008].items() if N >= 3e5) < table["0.0008"]["eta"], "saving 0.0008 passes at N>=3e5") + need(max(v for N, v in kap[0.001].items() if N >= 3e5) > table["0.001"]["eta"], "saving 0.001 still fails at N>=3e5") print(json.dumps({"status": "PASS_DIRECT_FLOW_BOUNDARY_SHARE", "ranks_scanned": len(Ns), "max_N": Ns[-1], - "max_boundary_share": round(best, 6), "at_N": at, "eta_reference": 0.984, - "new_kappa_claimed": False}, indent=1)) + "max_boundary_share": round(best, 6), "at_N": at, "rigorous_mirror_bound": round(bound, 6), + "min_leaf_share": round(leaf_min, 6), "max_leaf_rank_over_N": round(leaf_rank, 6), + "exit_coefficient_vs_eta": table, "new_kappa_claimed": False}, indent=1)) if __name__ == "__main__":