From 4e7022aa9128c8673d3e2024052b2deaa18cb6e4 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 06:48:19 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20check=20#4436=20=C2=A73=20on=20?= =?UTF-8?q?raw=20p7:=20width=20factor,=20exact=20routing-slot=20identity,?= =?UTF-8?q?=20N=20log=20N=20growth=20(no=20new=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- research/direct-flow-width-check/README.md | 56 +++++++++ research/direct-flow-width-check/SOURCES.json | 18 +++ research/direct-flow-width-check/TASK.json | 100 ++++++++++++++++ research/direct-flow-width-check/VERIFY.json | 18 +++ research/direct-flow-width-check/verify.py | 107 ++++++++++++++++++ 5 files changed, 299 insertions(+) create mode 100644 research/direct-flow-width-check/README.md create mode 100644 research/direct-flow-width-check/SOURCES.json create mode 100644 research/direct-flow-width-check/TASK.json create mode 100644 research/direct-flow-width-check/VERIFY.json create mode 100644 research/direct-flow-width-check/verify.py diff --git a/research/direct-flow-width-check/README.md b/research/direct-flow-width-check/README.md new file mode 100644 index 0000000000..c6db026010 --- /dev/null +++ b/research/direct-flow-width-check/README.md @@ -0,0 +1,56 @@ +# Independent check of #4436 §3 on raw p7: widths, routing slots and growth + +**Claim type:** an independent finite check plus an exact counting identity. **No new κ.** It covers §3 +("Nested divisible widths and complete count bounds") of zxv's +[#4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436), which my #4456 left uncovered. It uses +the same independent flow implementation as #4456. + +## What is checked, for every rank 121 ≤ n ≤ 2000 + +Let `W = Σ_k W_k = 7688` and `P = Σ_r P_r = 55998` be the unit's target and paid multiplicities, and +`h = G(n)`. + +1. **The width factor.** `S_n` (total source weight) is at most `C = W(W+P+1)^{h+1}`. The worst ratio + is `S_n/C = 1.6·10⁻⁵`, so the bound is very loose. +2. **An exact slot identity.** + + sources + exits + 2·matched = U·(W + P). + + Each unit's `W` target slots are either matched or sourced, and its `P` paid positions are either + matched or exits. So #4436's routing count (sources, exits, unit target slots and unit paid positions) + equals `2(W+P)U − 2·matched` **exactly**. That is at most `2(W+P)U`, with equality only when nothing + is matched. +3. **Growth.** `log B_N = Σ log S_n` grows like `N log N`. The ratio `log B_N/(N log N)` is 1.094, 1.756, + 1.965 and 2.033 at `N` = 500, 1,000, 1,500 and 2,000. A local run gives 2.066 at `N = 3,000`, so the + ratio is levelling off near 2. + +## Not covered + +- §3's telescoping `B_N·N − P_N = Δ·Qcol_N`, which needs the fully expanded program. The per-flow + identity is in #4456. +- The record and description bounds. +- Native premises. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/direct-flow-width-check --check-only +python3.12 -B scripts/research_package.py --package research/direct-flow-width-check +``` + +The verifier prints `PASS_DIRECT_FLOW_WIDTH_CHECK`, using only the standard library. + +## Open next questions + +1. **Tighten the constructive width (#4436 open question 3).** + - *Why it matters:* the observed `S_n` sits about 10⁵ times below `C`. + - *First step:* replace `C` by the exact `S_n` recurrence from the flow, and bound it by + `(W+P)·(units at the top layer)`. + +## Credit + +- The construction and the bounds are zxv's (#4436). +- 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-width-check/SOURCES.json b/research/direct-flow-width-check/SOURCES.json new file mode 100644 index 0000000000..9124bb10fe --- /dev/null +++ b/research/direct-flow-width-check/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-width-check/TASK.json b/research/direct-flow-width-check/TASK.json new file mode 100644 index 0000000000..3186769cf0 --- /dev/null +++ b/research/direct-flow-width-check/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": "Independent check of #4436 section 3 width/routing bounds on raw p7.", + "scope_change_reason": "Covers the part of #4436 left out of #4456.", + "bottleneck_link": "Side result: checks the explicit compiler-size bounds of the direct-flow route.", + "budget_minutes": 20, + "stop_rule": "Stop at per-rank checks to 2000.", + "outcome": "completed", + "evidence": "S_n/C <= 1.6e-5; exact identity S+X+2*matched = U(W+P) at every rank; log B_N/(N log N) = 2.03 at 2000 (2.07 at 3000 locally).", + "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": "Tighten the constructive width.", + "why_it_matters": "Observed S_n is ~1e5 below C.", + "first_step": "Bound S_n by the exact flow recurrence.", + "blocked_by": "None." + } + ] +} diff --git a/research/direct-flow-width-check/VERIFY.json b/research/direct-flow-width-check/VERIFY.json new file mode 100644 index 0000000000..d9b91f131c --- /dev/null +++ b/research/direct-flow-width-check/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": 180, + "checks": "#4436 section 3 on raw p7, ranks 121..2000: width factor S_n <= W(W+P+1)^(h+1), exact slot identity S+X+2*matched=U(W+P) (routing bound), log B_N/(N log N) < 2.1." + } + ] +} diff --git a/research/direct-flow-width-check/verify.py b/research/direct-flow-width-check/verify.py new file mode 100644 index 0000000000..c014cd5079 --- /dev/null +++ b/research/direct-flow-width-check/verify.py @@ -0,0 +1,107 @@ +#!/usr/bin/env python3 +"""Independent check of #4436 section 3 on raw p7: width, routing-slot and growth bounds. + +Uses an independent implementation of #4436's direct overlapping flow (the same as research/pr4436-direct-flow-check). +For every rank 121 <= n <= 2000, with W = sum_k W_k = 7688 and P = sum_r P_r = 55998 (the unit's target and paid +multiplicities) and h = G(n), it checks: + * S_n = total source weight <= C = W (W+P+1)^(h+1) (#4436's width factor bound); + * the exact slot identity S + X + 2 * matched = U (W + P), so the routing count + sources + exits + U (W + P) = 2 (W+P) U - 2 matched <= 2 (W+P) U (sharpens #4436's bound); + * log B_N = sum_n log S_n grows like N log N: the ratio log B_N / (N log N) stays below 2.1 through N = 2000. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import json +import math +import sys + +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) + + +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} + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def main(): + Wt, Pt = sum(W.values()), sum(P.values()) + need((Wt, Pt) == (7688, 55998), "unit multiplicities") + worst, logB, ratios = 0.0, 0.0, {} + for n in range(121, 2001): + R = flow(n, W, P) + S, X, U, M = sum(R["S"].values()), sum(R["X"].values()), R["units"], R["matched"] + C = Wt * (Wt + Pt + 1) ** (R["G"] + 1) + need(S <= C, f"n={n}: width factor bound") + worst = max(worst, S / C) + need(S + X + 2 * M == U * (Wt + Pt), f"n={n}: exact slot identity") + need(S + X + U * (Wt + Pt) <= 2 * (Wt + Pt) * U, f"n={n}: routing bound") + logB += math.log(S) + if n in (500, 1000, 1500, 2000): + ratios[n] = round(logB / (n * math.log(n)), 4) + need(max(ratios.values()) < 2.1, "log B_N / (N log N) below 2.1") + print(json.dumps({"status": "PASS_DIRECT_FLOW_WIDTH_CHECK", "ranks": "121..2000", "max_S_over_C": f"{worst:.3e}", + "logB_over_NlogN": ratios, "slot_identity": "S + X + 2*matched = U*(W+P)", + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())