From fd9f28beff7d03464d5a07cbdb00c38f431a1613 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 15:29:20 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20check=20#4580's=20p3=20H-branch?= =?UTF-8?q?=20budget=20(322/397)=20with=20own=20certified=20powers;=20note?= =?UTF-8?q?=20two=20rounded=20bracket=20endpoints=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/pr4580-budget-check/README.md | 45 +++++ research/pr4580-budget-check/SOURCES.json | 102 ++++++++++ research/pr4580-budget-check/TASK.json | 100 +++++++++ research/pr4580-budget-check/VERIFY.json | 35 ++++ research/pr4580-budget-check/verify.py | 234 ++++++++++++++++++++++ 5 files changed, 516 insertions(+) create mode 100644 research/pr4580-budget-check/README.md create mode 100644 research/pr4580-budget-check/SOURCES.json create mode 100644 research/pr4580-budget-check/TASK.json create mode 100644 research/pr4580-budget-check/VERIFY.json create mode 100644 research/pr4580-budget-check/verify.py diff --git a/research/pr4580-budget-check/README.md b/research/pr4580-budget-check/README.md new file mode 100644 index 0000000000..8e3c0ca10e --- /dev/null +++ b/research/pr4580-budget-check/README.md @@ -0,0 +1,45 @@ +# Independent arithmetic check of #4580: the p3 H-branch boundary budget + +**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.** + +Matarener's #4580 (head `62545a03`) prices zxv's p3 H branch at the #4470 frontier, κ = 0.00302015. At most **322** complex and **397** BIT rank-one boundary calls are affordable, and the direct correction (672 and 666 calls) fails even at `s = 0`. #4580 also gives saving roots for one and two shared head conjugations, and checks the native H112's low-rank structure and the distinct query lines. + +This package recomputes all of that arithmetic with its **own** certified powers `r^(1−s)`, using atanh logarithms and range-reduced exp series in exact rationals, rounded outward on a `2^−256` grid. It never uses the sources' `h_interval`. The H112 checks use its own exact elimination. Only the signed rank profiles and H112 are read from the same main sources (16 inputs, SHA256-pinned). + +## Results + +| | complex | BIT | +|---|---:|---:| +| raw surplus | 616 ✓ | 645 ✓ | +| budget at κ = 0.00302015 (budget + 1 certified negative) | **322** ✓ | **397** ✓ | +| direct bill fails at `s = 0` | 672 ✓ | 666 ✓ | +| own certified root, no extra bill | 0.0063799044338 | 0.0079333534813 | +| root, one head (224 / 222) | 0.0040422293244 | 0.0051761597317 | +| root, two heads (448 / 444) | 0.0017248833468 | 0.0024471105557 | + +The native H112 has `rank(H − I) = 8`, every one of its 112 rows and 112 columns is nonzero, and `H² = I`. There are 112 distinct complex query lines, and 111 distinct BIT lines up to sign. + +**One reporting note, not a defect in the conclusions.** #4580's `RESULT.json` prints its bisection endpoints to 10 decimals. Every printed `positive_at` is certified positive, and every printed `negative_at` lies within #4580's bisection width (`0.02/2^26 ≈ 3·10^−10`) of the root. But two printed `negative_at` values fall **just below** the root, where the moment is still positive: +- complex, no extra bill: printed `0.0063799044`, root `0.00637990443…`; +- BIT, bill 222: printed `0.0051761597`, root `0.00517615973…`. + +They are roundings of valid exact endpoints, not certified brackets themselves. The budgets, roots to the stated 7 digits, and the negative result are unaffected. + +## Verify + +```text +python3 -B research/pr4580-budget-check/verify.py +``` + +This runs in about 20 s with the standard library only. + +## Limitations + +- **Not covered.** The decoder lower-bound argument of #4580 §4 (gather decoders need one request per port line) is a written argument, and only its finite inputs (line counts and support) are checked here. The H-branch profiles themselves are the sources'. +- **Raw rank screen.** As #4580 says, these budgets omit outer rows, tails and compiler gates. + +## Open next questions + +- None new from the arithmetic. #4580's own open question, changing the local family or line structure, is untouched. + +Credit: Matarener / Mark (#4580); zxv (#4359 H branch); the #4431, #589 and kappa-rebuild lineage. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4580-budget-check/SOURCES.json b/research/pr4580-budget-check/SOURCES.json new file mode 100644 index 0000000000..c9d7b330fb --- /dev/null +++ b/research/pr4580-budget-check/SOURCES.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "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" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "usage": "input", + "git_blob": "8b40135a84e7f0f0cd44bed69655801310b916a7", + "sha256": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/native_common.py", + "usage": "input", + "git_blob": "df276cc71f954b72ac4de4f07d2172d547772ba6", + "sha256": "ca1f913d6c104d456fdbebcecfdaf9a1ea12d647d74fe009b69689b9e678f0a4" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/kappa-rebuild/architecture/controller_tariff.py", + "usage": "input", + "git_blob": "21fe4799f7d9db9f32f0e92db8ae3c1c925dcb76", + "sha256": "62d2479c41c64a58275857b884f1eb68d36ee4f755d7d393363ba8cc233251f3" + }, + { + "path": "research/kappa-rebuild/architecture/identity_mixed_certificate.py", + "usage": "input", + "git_blob": "f4b51b358eff3cc43ea200503d16e7b75f67c7bc", + "sha256": "e1795294fa4d3100352bfda787ecb1efc2468ff11cbcbaca2476eb642b8d2a0a" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_forest_search.py", + "usage": "input", + "git_blob": "9b5213bf3f164664a36f81592740801f79b3c97d", + "sha256": "2dcec76840b437c67125af5b6d3529577f8c38851c792d0ffd9fa928c473e23b" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + { + "path": "research/kappa-rebuild/bit/PR589-H-GLOBAL-PROBE.json", + "usage": "input", + "git_blob": "cbebedba1df5297a3eb98783cc1814bd3773f8a5", + "sha256": "15c1a7912a4d5ee463459ca9a5fc24ee37674eaa0c1650438ffc302c0d0cd05e" + }, + { + "path": "research/kappa-rebuild/bit/complex_controller_factor.py", + "usage": "input", + "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947", + "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497" + }, + { + "path": "research/kappa-rebuild/bit/mixed_productive_bit.py", + "usage": "input", + "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96", + "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e" + }, + { + "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/kappa-rebuild/complex/rebuild_native.py", + "usage": "input", + "git_blob": "78a7b1b0e6e43a1347fb361f45c6e0eaff8dd27b", + "sha256": "f94c527cc02215de49350d477618188c4c0da48bc8fb05b4e37b24c482cad7d5" + }, + { + "path": "research/kappa-rebuild/transfer-audit/h-branch/BIT-MINIMUM-COMPLETION-AUDIT.json", + "usage": "input", + "git_blob": "553d3a166e13530ef1350a2947ed959694a8c36e", + "sha256": "c5203c00dc7f6cc20e36113cf87998fec0a6afc4c3927950d207309938fe02ff" + } + ] +} diff --git a/research/pr4580-budget-check/TASK.json b/research/pr4580-budget-check/TASK.json new file mode 100644 index 0000000000..7e3c52ce8c --- /dev/null +++ b/research/pr4580-budget-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "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": "unchanged", + "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "scope_change_reason": null, + "bottleneck_link": "Independent arithmetic for a negative screen that closes the p3 H branch at the current frontier.", + "budget_minutes": 30, + "stop_rule": "Stop at #4580's arithmetic.", + "outcome": "completed", + "evidence": "Own certified powers: surpluses 616/645, budgets 322/397 (budget+1 negative), direct bills fail at s=0, own root brackets (width <= 1e-12) for all six bills; H112 rank 8, full support, H^2=I; 112/111 distinct lines. Note: two printed negative_at endpoints lie just below the root (rounding).", + "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": "None new from the arithmetic.", + "why_it_matters": "#4580's own open questions (changed local family/line structure) remain.", + "first_step": "See #4580.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4580-budget-check/VERIFY.json b/research/pr4580-budget-check/VERIFY.json new file mode 100644 index 0000000000..6405e6c177 --- /dev/null +++ b/research/pr4580-budget-check/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/native_common.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/certificate.json.gz", + "research/kappa-rebuild/architecture/controller_tariff.py", + "research/kappa-rebuild/architecture/identity_mixed_certificate.py", + "research/kappa-rebuild/architecture/mixed_forest_search.py", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/kappa-rebuild/bit/PR589-H-GLOBAL-PROBE.json", + "research/kappa-rebuild/bit/complex_controller_factor.py", + "research/kappa-rebuild/bit/mixed_productive_bit.py", + "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz", + "research/kappa-rebuild/complex/rebuild_native.py", + "research/kappa-rebuild/transfer-audit/h-branch/BIT-MINIMUM-COMPLETION-AUDIT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Own certified r^(1-s): surpluses, budgets 322/397, budget+1 negative, own root brackets vs reported, direct bills; own exact H112 rank/support/H^2=I; distinct lines." + } + ] +} diff --git a/research/pr4580-budget-check/verify.py b/research/pr4580-budget-check/verify.py new file mode 100644 index 0000000000..d3f9b9caf0 --- /dev/null +++ b/research/pr4580-budget-check/verify.py @@ -0,0 +1,234 @@ +#!/usr/bin/env python3 +"""Independent arithmetic check of PR #4580 (Matarener): the p3 H-branch boundary budget at kappa = 0.00302015. + +The signed complex and BIT rank profiles are taken from the same main sources #4580 uses (controller_tariff.geometry(3, +43) with kernel H; the BIT probe with the three-row minimum completion). Everything else is recomputed here with this +file's own exact arithmetic, never the sources' h_interval: + * certified powers r^(1-s) from atanh logarithms and range-reduced exp series, rounded outward on a 2^-256 grid; + * raw surpluses 616 / 645; budgets 322 / 397 at s = 0.00302015 (largest k with certified moment - k > 0), and + budget + 1 certified negative; + * own certified saving-root brackets (width <= 1e-12) for bills 0, 224/222, 448/444: every reported positive_at is + certified positive and every reported negative_at lies within #4580's bisection width (0.02/2^26, about 3e-10) of the root, but two printed negative_at + strings (complex bill 0, BIT bill 222) are 10-decimal roundings that fall just below the root, where the moment is + still positive; the direct bills 672 / 666 fail at s = 0; + * the native H112 from main's rebuild_native: own exact rank(H - I) = 8, all 112 rows and columns of H - I nonzero, + H^2 = I; + * 112 distinct complex query lines and 111 distinct BIT lines up to sign. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +import gzip +import importlib.util +import json +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +KR = ROOT / "research/kappa-rebuild" +DEP = ROOT / "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime" +sys.path[:0] = [str(KR / "architecture"), str(KR / "bit"), str(DEP / "bit-compression/carrier-reuse/reference")] +RECORD = Q("0.00302015") +GRID = Q(1, 2 ** 256) +REPORTED = { # #4580 RESULT.json brackets (head 62545a03) + "complex": {0: ("0.0063799042", "0.0063799044"), 224: ("0.0040422291", "0.0040422294"), + 448: ("0.0017248833", "0.0017248836")}, + "bit": {0: ("0.0079333532", "0.0079333535"), 222: ("0.0051761594", "0.0051761597"), + 444: ("0.0024471104", "0.0024471107")}, +} + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def down(x): + return Q((x / GRID).__floor__()) * GRID + + +def up(x): + return Q((x / GRID).__ceil__()) * GRID + + +def ln_bounds(n, terms=90): + n = Q(n) + k = 0 + while n >= 2: + n /= 2 + k += 1 + + def series(y): + z = (y - 1) / (y + 1) + s, p = Q(0), z + for j in range(terms): + s += 2 * p / (2 * j + 1) + p *= z * z + return down(s), up(s + 2 * p / ((2 * terms + 1) * (1 - z * z))) + + a, b = series(n) + c, d = series(Q(2)) + return a + k * c, b + k * d + + +def exp_bounds(x): + """Outward bounds for exp(x), x >= 0 rational.""" + k = 0 + while x > Q(1, 2): + x /= 2 + k += 1 + t, s = Q(1), Q(1) + for n in range(1, 40): + t = t * x / n + s += t + lo, hi = down(s), up(s + 2 * t * x / 40) + for _ in range(k): + lo, hi = down(lo * lo), up(hi * hi) + return lo, hi + + +_CACHE = {} + + +def power(r, s): + """Certified [lo, hi] for r^(1-s), r >= 1.""" + key = (r, s) + if key not in _CACHE: + if r == 1: + _CACHE[key] = (Q(1), Q(1)) + else: + a, b = ln_bounds(r) + _CACHE[key] = (exp_bounds((1 - s) * a)[0], exp_bounds((1 - s) * b)[1]) + return _CACHE[key] + + +def moment(signed, s): + lo = hi = Q(0) + for r, n in signed.items(): + a, b = power(r, s) + lo += n * (a if n >= 0 else b) + hi += n * (b if n >= 0 else a) + return lo, hi + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def profiles(): + import controller_tariff as T + import mixed_forest_search as F + windows, targets, _ = T.geometry(3, 43) + case = F.verify(3, 6, T.simple_p3(), "H", custom_windows=windows, custom_targets=targets) + cx = Counter(case["signed"]) + probe = json.loads((KR / "bit/PR589-H-GLOBAL-PROBE.json").read_text()) + audit = json.loads((KR / "transfer-audit/h-branch/BIT-MINIMUM-COMPLETION-AUDIT.json").read_text()) + bt = Counter({int(r): n for r, n in probe["targets"].items()}) + bt.subtract(Counter({int(r): n for r, n in audit["p3"]["raw_paid"].items()})) + return {"complex": cx, "bit": bt} + + +def side(name, signed): + margin = sum(r * n for r, n in signed.items()) + need(margin == {"complex": 616, "bit": 645}[name], f"{name} raw surplus") + lo, hi = moment(signed, RECORD) + budget = lo.numerator // lo.denominator + if Q(budget) == lo: + budget -= 1 + need(budget == {"complex": 322, "bit": 397}[name], f"{name} budget") + need(hi - (budget + 1) < 0, f"{name}: budget + 1 certified negative") + roots, mislabelled = {}, [] + for bill, (pos, neg) in REPORTED[name].items(): + prof = Counter(signed) + prof[1] -= bill + lo_s, hi_s = Q(0), Q("0.02") + need(moment(prof, lo_s)[0] > 0 and moment(prof, hi_s)[1] < 0, "outer bracket") + while hi_s - lo_s > Q(1, 10 ** 12): + mid = (lo_s + hi_s) / 2 + a, b = moment(prof, mid) + if a > 0: + lo_s = mid + elif b < 0: + hi_s = mid + else: + break + need(hi_s - lo_s <= Q(1, 10 ** 12), "own certified bracket width <= 1e-12") + need(moment(prof, Q(pos))[0] > 0, f"{name} reported positive_at certified positive (bill {bill})") + need(abs(Q(neg) - hi_s) < Q(4, 10 ** 10), f"{name} reported negative_at within #4580's bisection width of the root (bill {bill})") + if not moment(prof, Q(neg))[1] < 0: + mislabelled.append(bill) # the printed 10-decimal endpoint lies just below the root + roots[str(bill)] = [f"{float(lo_s):.13f}", f"{float(hi_s):.13f}"] + need(mislabelled == {"complex": [0], "bit": [222]}[name], f"{name}: rounded negative_at endpoints identified") + direct = {"complex": 672, "bit": 666}[name] + prof = Counter(signed) + prof[1] -= direct + need(moment(prof, Q(0))[1] < 0, f"{name}: direct bill fails at s = 0") + return {"raw_surplus": int(margin), "budget": int(budget), "moment_at_record": [float(lo), float(hi)], + "certified_root_brackets": roots, "reported_negative_at_not_negative_for_bills": mislabelled} + + +def rank(rows): + rows = [list(r) for r in rows] + rk, cols = 0, len(rows[0]) + for c in range(cols): + piv = None + for i in range(rk, len(rows)): + if rows[i][c] != 0: + piv = i + break + if piv is None: + continue + rows[rk], rows[piv] = rows[piv], rows[rk] + pv = rows[rk][c] + for i in range(len(rows)): + if i != rk and rows[i][c] != 0: + f = rows[i][c] / pv + rows[i] = [x - f * y for x, y in zip(rows[i], rows[rk])] + rk += 1 + return rk + + +def native(): + n = load(DEP / "direct-decoder/native_common.py", "chk_native_common") + reb = load(KR / "complex/rebuild_native.py", "chk_rebuild_native") + packet, _ = n.load_sources() + H = reb.geometry(packet)["H"] + size = len(H) + h = [[Q(row.get(j, 0)) for j in range(size)] for row in H] + m = [[h[i][j] - (1 if i == j else 0) for j in range(size)] for i in range(size)] + need(size == 112 and rank(m) == 8, "rank(H - I) = 8") + need(all(any(r) for r in m) and all(any(m[i][j] for i in range(size)) for j in range(size)), "full support") + for i in range(size): + for j in range(size): + need(sum(h[i][k] * h[k][j] for k in range(size)) == (1 if i == j else 0), "H^2 = I") + return {"ports": size, "rank_H_minus_I": 8} + + +def lines(): + phases = json.loads((DEP / "direct-decoder/sources/DATA-PHASES.json").read_text()) + qs = [r["q"] for r in phases["recipes"]] + need(len(qs) == 112 and len(set(qs)) == 112, "112 distinct complex query lines") + word = json.loads(gzip.decompress((KR / "bit/sources/pr589-regenerated/WORD.json.gz").read_bytes())) + ls = [tuple(Q(x) for x in q) for q in word["lines"]] + need(len(ls) == 111 and len({max(q, tuple(-x for x in q)) for q in ls}) == 111, "111 distinct BIT lines") + return {"complex": 112, "bit": 111} + + +def main(): + for r in range(2, 200): + a, b = power(r, Q(0)) + need(a <= r <= b and b - a < Q(1, 10 ** 50), "power control at s = 0") + p = profiles() + report = {"status": "PASS_PR4580_BUDGET_CHECK", "complex": side("complex", p["complex"]), "bit": side("bit", p["bit"]), + "native_H112": native(), "distinct_lines": lines(), "new_kappa_claimed": False} + print(json.dumps(report, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())