diff --git a/research/pr4436-direct-flow-check/README.md b/research/pr4436-direct-flow-check/README.md new file mode 100644 index 0000000000..53f9980b21 --- /dev/null +++ b/research/pr4436-direct-flow-check/README.md @@ -0,0 +1,74 @@ +# Independent check of #4436's direct flow for overlapping ranks + +**Claim type:** an independent re-implementation, checked against #4436's recorded flows, plus +exact recurrence values and a local trend. **No new κ.** The object is zxv's +[#4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436), at head `56003680`, §2: the +partially matched integer lockstep flow for the case where paid ranks overlap target ranks +(`max paid < ambient`). In it: + +- a parent round's issued jobs at point `b` are matched to the child demand + `D(b) = Σ W_k·u(b − e_k)` over present child points; +- the remaining `u(b) − D(b)` jobs become paid boundary exits; +- child target slots that have no parent point become new sources. + +## Results + +`verify.py` implements the flow separately. It checks: + +- **All 9 recorded finite flows.** The separated control at `n = 20, 40, 80`, the strict overlap at + `n = 20, 40, 80`, and the source-open equality case at `n = 20, 40, 80` are reproduced exactly: + sources, exits, boundary exits, column mass, unit count and matched jobs. #4436's + `RESULT.json` values are copied into `VECTORS.json` with its SHA256. +- **Every rank on raw p7.** At every rank `121 ≤ N ≤ 1000`, all sources lie in `(N/m, N]`, all exits + are below `N`, and the rank-one potential identity `Σ S_s·s − Σ X_e·e = 608 × (column mass)` holds + exactly. +- **The exact leaf recurrence.** `L(1000) = 995.6296444195137…` lies inside #4436's printed interval. + The effective saving there is `1 − log L/log N = 0.000634`, which confirms #4436's statement that + rank 1,000 misses the target. + +**Local trend.** `trend_local.py` computes the same recurrence in floating point. This is local +evidence and is not part of the verifier. + +| `N` | `L(N)` | effective saving | +| --- | --- | --- | +| 1,000 | 995.6296 | 0.000634 | +| 3,000 | 2,982.0507 | 0.000750 | +| 10,000 | 9,926.6191 | 0.000800 | +| 30,000 | 29,742.7603 | 0.000835 | + +For comparison, the separated p3 compiler of #4359, checked in my #4404, reached 0.001193 at +`N = 10⁴` against its limit of 0.002304. The direct p7 flow is climbing more slowly, toward a raw +root near 0.0027. These finite values neither prove nor refute an asymptotic direct exponent, which +#4436 leaves open. + +## Not covered + +- #4436's size bounds `B_N ≤ exp(O(N log N))`, its nested batching and its resource envelopes. +- Native premises. +- The asymptotic direct saving. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/pr4436-direct-flow-check --check-only +python3.12 -B scripts/research_package.py --package research/pr4436-direct-flow-check +``` + +The verifier prints `PASS_PR4436_DIRECT_FLOW_CHECK` in under a second, using only the standard +library. + +## Open next questions + +1. **Does the direct flow's complement-plus-exit recurrence admit a uniform estimate?** This is + #4436's exponent gate. + - *Why it matters:* it would remove the tensor and padding step. + - *First step:* fit the measured exit mass as a function of `N`, and test whether the boundary + exits carry a vanishing share of the `t`-potential. + +## Credit + +- The direct flow, the size bounds and the recorded flows are zxv's (#4436). +- The multinomial 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/pr4436-direct-flow-check/SOURCES.json b/research/pr4436-direct-flow-check/SOURCES.json new file mode 100644 index 0000000000..9124bb10fe --- /dev/null +++ b/research/pr4436-direct-flow-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/pr4436-direct-flow-check/TASK.json b/research/pr4436-direct-flow-check/TASK.json new file mode 100644 index 0000000000..255f54a627 --- /dev/null +++ b/research/pr4436-direct-flow-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": "Independently check #4436's partially matched direct flow for overlapping ranks: recorded flows, potential identity, exact L(1000), and a local saving trend.", + "scope_change_reason": "The card asks for independent coverage of new mechanisms; #4436 had no review.", + "bottleneck_link": "A direct flow would remove the tensor/padding step behind the kappa ~0.0027-0.0030 claims.", + "budget_minutes": 30, + "stop_rule": "Stop at the flow, identity and recurrence; do not audit size bounds or native premises.", + "outcome": "completed", + "evidence": "verify.py: 9/9 recorded flows reproduced exactly; potential identity and rank ranges at every p7 rank to 1000; L(1000)=995.6296444195137 inside #4436's interval. Local float trend: effective saving 0.000634 (1e3) .. 0.000835 (3e4).", + "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": "Does the direct flow's complement-plus-exit recurrence admit a uniform estimate?", + "why_it_matters": "It would remove the tensor/padding step.", + "first_step": "Fit the measured exit mass versus N and test whether boundary exits carry a vanishing share of the t-potential.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4436-direct-flow-check/VECTORS.json b/research/pr4436-direct-flow-check/VECTORS.json new file mode 100644 index 0000000000..d64806c78f --- /dev/null +++ b/research/pr4436-direct-flow-check/VECTORS.json @@ -0,0 +1,359 @@ +{ + "source": "PR #4436 research/direct-mixed-flow/RESULT.json at head 56003680aee2871773de408e5f01cc5dd46b144c", + "source_sha256": "da04256f6f2ef61530f1d642ff1137a2274fd642782a72ef4bf3f1b65395c270", + "finite_flows": [ + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 18, + "exits": { + "1": 16, + "2": 16, + "4": 4 + }, + "height": 1, + "matched_jobs": 18, + "minimum_source": 9, + "n": 20, + "rank_one_surplus": 2, + "source_count": 9, + "sources": { + "12": 4, + "16": 1, + "9": 4 + }, + "unit_count_upper": 9, + "units": 9 + }, + "literal_classes": 7, + "paid": { + "1": 4, + "2": 2 + }, + "rule": "separated-control", + "targets": { + "3": 2, + "4": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 180, + "exits": { + "1": 64, + "2": 96, + "4": 48, + "8": 8 + }, + "height": 2, + "matched_jobs": 132, + "minimum_source": 12, + "n": 40, + "rank_one_surplus": 2, + "source_count": 42, + "sources": { + "12": 16, + "16": 4, + "24": 8, + "27": 8, + "32": 2, + "36": 4 + }, + "unit_count_upper": 63, + "units": 58 + }, + "literal_classes": 43, + "paid": { + "1": 4, + "2": 2 + }, + "rule": "separated-control", + "targets": { + "3": 2, + "4": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 244, + "exits": { + "1": 64, + "2": 96, + "4": 48, + "8": 8 + }, + "height": 2, + "matched_jobs": 162, + "minimum_source": 27, + "n": 80, + "rank_one_surplus": 2, + "source_count": 27, + "sources": { + "27": 8, + "36": 12, + "48": 6, + "64": 1 + }, + "unit_count_upper": 63, + "units": 63 + }, + "literal_classes": 43, + "paid": { + "1": 4, + "2": 2 + }, + "rule": "separated-control", + "targets": { + "3": 2, + "4": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": { + "16": 1 + }, + "column_mass": 28, + "exits": { + "1": 8, + "16": 5, + "4": 12 + }, + "height": 2, + "matched_jobs": 8, + "minimum_source": 5, + "n": 20, + "rank_one_surplus": 1, + "source_count": 14, + "sources": { + "10": 2, + "20": 5, + "5": 4, + "8": 3 + }, + "unit_count_upper": 19, + "units": 11 + }, + "literal_classes": 13, + "paid": { + "1": 2, + "4": 1 + }, + "rule": "strict-overlap", + "targets": { + "2": 1, + "5": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": { + "32": 5 + }, + "column_mass": 132, + "exits": { + "1": 16, + "16": 12, + "32": 5, + "4": 32 + }, + "height": 3, + "matched_jobs": 40, + "minimum_source": 10, + "n": 40, + "rank_one_surplus": 1, + "source_count": 30, + "sources": { + "10": 8, + "16": 3, + "20": 10, + "25": 4, + "40": 5 + }, + "unit_count_upper": 65, + "units": 35 + }, + "literal_classes": 40, + "paid": { + "1": 2, + "4": 1 + }, + "rule": "strict-overlap", + "targets": { + "2": 1, + "5": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": { + "40": 4, + "64": 5 + }, + "column_mass": 872, + "exits": { + "1": 32, + "16": 80, + "4": 80, + "40": 4, + "64": 29 + }, + "height": 4, + "matched_jobs": 132, + "minimum_source": 20, + "n": 80, + "rank_one_surplus": 1, + "source_count": 106, + "sources": { + "20": 36, + "25": 8, + "32": 15, + "40": 10, + "50": 8, + "80": 29 + }, + "unit_count_upper": 211, + "units": 119 + }, + "literal_classes": 121, + "paid": { + "1": 2, + "4": 1 + }, + "rule": "strict-overlap", + "targets": { + "2": 1, + "5": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 322, + "exits": { + "1": 216, + "2": 216, + "4": 72, + "8": 8 + }, + "height": 2, + "matched_jobs": 512, + "minimum_source": 8, + "n": 20, + "rank_one_surplus": 1, + "source_count": 128, + "sources": { + "12": 48, + "18": 10, + "8": 64, + "9": 6 + }, + "unit_count_upper": 129, + "units": 128 + }, + "literal_classes": 73, + "paid": { + "1": 6, + "2": 2 + }, + "rule": "source-open-equality", + "targets": { + "2": 4, + "3": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 4362, + "exits": { + "1": 1296, + "16": 16, + "2": 1728, + "4": 864, + "8": 192 + }, + "height": 3, + "matched_jobs": 5040, + "minimum_source": 16, + "n": 40, + "rank_one_surplus": 1, + "source_count": 670, + "sources": { + "16": 256, + "18": 84, + "24": 256, + "27": 6, + "36": 68 + }, + "unit_count_upper": 1157, + "units": 1142 + }, + "literal_classes": 585, + "paid": { + "1": 6, + "2": 2 + }, + "rule": "source-open-equality", + "targets": { + "2": 4, + "3": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 55372, + "exits": { + "1": 7776, + "16": 480, + "2": 12960, + "32": 32, + "4": 8640, + "8": 2880 + }, + "height": 4, + "matched_jobs": 45088, + "minimum_source": 27, + "n": 80, + "rank_one_surplus": 1, + "source_count": 3572, + "sources": { + "27": 36, + "32": 1024, + "36": 744, + "48": 1280, + "54": 96, + "72": 392 + }, + "unit_count_upper": 9881, + "units": 9732 + }, + "literal_classes": 4681, + "paid": { + "1": 6, + "2": 2 + }, + "rule": "source-open-equality", + "targets": { + "2": 4, + "3": 1 + } + } + ], + "p7_leaves_per_array_n1000": { + "lower": "24890741110487842821/25000000000000000", + "upper": "995629644419513712841/1000000000000000000" + } +} diff --git a/research/pr4436-direct-flow-check/VERIFY.json b/research/pr4436-direct-flow-check/VERIFY.json new file mode 100644 index 0000000000..5b6023d6ed --- /dev/null +++ b/research/pr4436-direct-flow-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": 120, + "checks": "Nine #4436 recorded flows reproduced exactly by a separate implementation; raw p7 ranks 121..1000: source range, exits < N, exact potential identity; exact L(1000) inside #4436's printed interval." + } + ] +} diff --git a/research/pr4436-direct-flow-check/trend_local.py b/research/pr4436-direct-flow-check/trend_local.py new file mode 100644 index 0000000000..c9c735fd36 --- /dev/null +++ b/research/pr4436-direct-flow-check/trend_local.py @@ -0,0 +1,11 @@ +import math, time, sys +exec(open('overlap_flow.py').read()) +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=121; NMAX=int(sys.argv[1]); L=[0.0,1.0]; t=time.time() +marks={1000,3000,10000,30000,100000,200000} +for N in range(2,NMAX+1): + if N 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(): + vec = json.loads((HERE / "VECTORS.json").read_text(encoding="utf-8")) + for f in vec["finite_flows"]: + W = {int(k): v for k, v in f["targets"].items()} + P = {int(k): v for k, v in f["paid"].items()} + fl = f["flow"] + r = flow(fl["n"], W, P) + need(r["S"] == {int(k): v for k, v in fl["sources"].items()}, f"{f['rule']} n={fl['n']}: sources") + need(r["X"] == {int(k): v for k, v in fl["exits"].items()}, "exits") + need(r["BX"] == {int(k): v for k, v in fl["boundary_exits"].items()}, "boundary exits") + need((r["col"], r["units"], r["matched"]) == (fl["column_mass"], fl["units"], fl["matched_jobs"]), "mass, units, 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} + m = 121 + surplus = sum(k * w for k, w in W.items()) - sum(r * p for r, p in P.items()) + need(surplus == 608, "p7 rank-one surplus") + L = [Q(0), Q(1)] + for N in range(2, 1001): + if N < m: + L.append(Q(N)) + continue + r = flow(N, W, P) + need(all(m * s > N and s <= N for s in r["S"]) and all(e < N for e in r["X"]), f"N={N}: ranks") + 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") + tot = sum(r["S"].values()) + L.append((sum(v * L[N - s] for s, v in r["S"].items()) + sum(v * L[e] for e, v in r["X"].items())) / tot) + lo, hi = (Q(vec["p7_leaves_per_array_n1000"][k]) for k in ("lower", "upper")) + need(lo <= L[1000] <= hi, "L(1000) inside #4436's printed interval") + print(json.dumps({"status": "PASS_PR4436_DIRECT_FLOW_CHECK", "recorded_flows_reproduced": len(vec["finite_flows"]), + "p7_ranks_checked": "121..1000", "L_1000": f"{float(L[1000]):.13f}", + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())