diff --git a/research/rank7-restore-carrier-skips/CLAIM.json b/research/rank7-restore-carrier-skips/CLAIM.json new file mode 100644 index 0000000000..47a55a7f68 --- /dev/null +++ b/research/rank7-restore-carrier-skips/CLAIM.json @@ -0,0 +1,229 @@ +{ + "admitted_package_manifest_sha256": "2c367a7afa966a7952303364fbccd6332730e2d3ad48d2ef04a524f35daddb03", + "baseline_head": "e2ca469b08385d3d5e29a918d66dbefaf889e9f3", + "baseline_kappa": "17240352247481048785499999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "baseline_pr": 2969, + "baseline_status": "FINITE_NATIVE_OWNER_AND_MOMENT_CANDIDATE_OUTER_PENDING", + "calls": 666, + "complex_lower": "432434041596978996703/250000000000000000000000", + "declared_edits": { + "count": 2, + "edits_sha256": "ebffcc1e57e59439b9678ff8d9be518c457af22ce77235c2fdb46540ab9b9b79", + "previous_kappa": "0.0017290339826465135177169999999999999999999998999999999999999999999999", + "previous_pr": 2979 + }, + "fill_sha256": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39", + "fixed_inventory_cap": { + "cap_lower": "4324344875160696378107/2500000000000000000000000", + "cap_upper": "17297379500642785512429/10000000000000000000000000", + "realized": "below the fractional optimum by the recorded gap (check_cap.py); the cap basis is fractional at T74" + }, + "gain": "2850470819905554131/500000000000000000000000", + "helpers": 408, + "independent_inputs": 632, + "kappa": "17297361663879159868119999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "kappa_decimal": "0.0017297361663879159868119999999999999999999998999999999999999999999999", + "live_families": 66304, + "local_profile": { + "1": 2433, + "2": 712, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "native_receipt_sha256": "7e982591b1362efe5e8d03fd98f67ff4ef676dd8a5fa3ca765c8ef1370be7019", + "physical_families": 66813, + "previous_claims": { + "pr2942": { + "claim_file": "comparators/PR2942-CLAIM.json", + "gain": "108122601948463419/15625000000000000000000", + "head": "a027b0f6fdb0ab2b42ba10fc31b53960166bf2bf", + "kappa": "17228163198632143279959999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr": 2942 + }, + "pr2957": { + "claim_file": "comparators/PR2957-CLAIM.json", + "gain": "6018751317177815841/1000000000000000000000000", + "head": "b74b25f3ccc84c16e1a801d73b2f47e5ea764c78", + "kappa": "17237174150707381709709999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr": 2957 + }, + "pr2966": { + "claim_file": "comparators/PR2966-CLAIM.json", + "gain": "28509469322319047/5000000000000000000000", + "head": "e62d3eb9005117d82a9babcfa937ecc53237c490", + "kappa": "17240342725234521774119999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr": 2966 + }, + "pr2969": { + "claim_file": "allocation/baseline/CLAIM.json", + "gain": "2850470819905554131/500000000000000000000000", + "head": "e2ca469b08385d3d5e29a918d66dbefaf889e9f3", + "kappa": "17240352247481048785499999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr": 2969 + }, + "pr2979": { + "claim_file": "comparators/PR2979-CLAIM.json", + "gain": "140436748280493819/200000000000000000000000", + "head": "be191346391661f4d35fc0d1508d0a6029572576", + "kappa": "17290339826465135177169999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr": 2979 + } + }, + "profile": { + "1": 1637688, + "2": 474192, + "3": 159468, + "4": 71928, + "48": 28190, + "5": 13716, + "8": 5328 + }, + "release_receipt_sha256": "906d15db82f7b5b8938d1b760f54d9229dc7b6f2dbe84cc9286f2d1015e36743", + "replicas": 74, + "scope": "Conditional finite supplier/outer certificate for PR2979's words (mdumitrean: joint rank-7 end frames, five further paired extractions, fourteen PR2957 rewrites) with one declared literal restore edit (R1, Stack2979 / Jeremy Kothe) and PR2979's literal T74 allocation unchanged (paid profile re-derived). Inherited all-size/compiler/theorem hypotheses remain. No selected-frontier change or independent-human-review claim.", + "source_manifest_sha256": "130650ad8833f6df88528c560e4d1cfbae084f4b15a64788a332ddcaff472a17", + "stages": { + "stage1": { + "frame_edits": 139, + "groups": { + "A": { + "W": [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ], + "helpers": [ + 331, + 450, + 451, + 508, + 509 + ] + }, + "B": { + "W": [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ], + "helpers": [ + 299, + 448, + 449, + 484, + 485 + ] + }, + "C": { + "W": [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ], + "helpers": [ + 452, + 453, + 532, + 533 + ] + }, + "D": { + "W": [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ], + "helpers": [ + 454, + 455, + 556, + 557 + ] + }, + "V45": { + "W": [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + "helpers": [ + 249, + 251, + 265, + 267 + ] + } + }, + "kind": "joint codimension-2 end-frame lowering (frame-only)", + "record_sha256": "5fbfce004330ebc1fbac8de264614fe295f1a074811b478db4892c3bc3852cd3" + }, + "stage2": { + "extractions": [ + { + "helper": 226, + "normal": 42, + "step": 1 + }, + { + "helper": 228, + "normal": 42, + "step": 2 + }, + { + "helper": 230, + "normal": 42, + "step": 3 + }, + { + "helper": 363, + "normal": 7, + "step": 4 + }, + { + "helper": 395, + "normal": 7, + "step": 5 + } + ], + "kind": "rank-8 paired input/output extractions" + }, + "stage3": { + "applier_sha256": "2509f1335e47543f8814b42d6bf83032b30c5899b4f7cc62a6adc03f5138ae13", + "count": 14, + "kind": "declared exactness-preserving gate rewrites (Jeremy Kothe, PR2957), re-addressed", + "rewrites_sha256": "a37ade675876e4f5b00b33066c84f495fccd264863b7eb5d813837b1d01c3e7d" + } + }, + "status": "CONDITIONAL_CANDIDATE_COMPLETE_FINITE_RELEASE", + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + }, + "zero_buffers": 91 +} diff --git a/research/rank7-v45-profile-audit/README.md b/research/rank7-v45-profile-audit/README.md new file mode 100644 index 0000000000..076688beda --- /dev/null +++ b/research/rank7-v45-profile-audit/README.md @@ -0,0 +1,45 @@ +# Independent V45 frame and invoice audit for PR #2979 + +**Result: partial positive audit of one local group, the profile-bearing word stages, and the literal T74 owner allocation, plus an exact negative screen of the audited profile at κ=0.1. It does not independently validate the full supplier or select a new κ.** + +The selected conditional result remains κ = 0.001672660197076918. [PR #2979](https://github.com/CrocSwap/integer-mult-bounds/pull/2979) claims κ ≈ 0.0017290339826465135, about `0.0000563737855695955` above the selected value. It merged into `main` on 2026-10-16, but the selected record still names #1094; this audit does not admit the candidate or change the frontier. It independently reconstructs the V45 rank-7 frame group from the pinned parent words using explicit XOR-span closure, then rebuilds the profile-bearing word sections through the five extraction transforms and fourteen literal rewrites for both providers. It also independently checks the T74 owner allocation, in addition to the published aggregate arithmetic. It does not replay the full admission chain. + +For V45, all 61 edited gate frames are hyperplanes of their old frames, each lies in the shared rank-7 subspace, and every gate touching a lowered helper stays in that subspace. Both parent providers give the same result. The coordinated four-helper lowering changes the exact weighted local profile price by −8,388,172 units and leaves +22,972 after paying for four freed width units. The single-helper control loses: its price delta is −2,038,159 and its margin is −53,141. The five-group positive control independently reproduces all 139 stage-1 edits, the declared stage-1 local profile and the changed width inventory. + +The source replay reproduces the stage-2 profile `{1:2449, 2:710, 3:236, 4:102, 5:18, 8:8}` and the final profile `{1:2445, 2:706, 3:232, 4:108, 5:18, 8:8}`, with the claimed width inventory, for both providers. Its exact weighted stage deltas are −46,150,994, −10,523,403, and −52,350 units, summing to −56,726,747. A missing stage-2 frame change, stale rewrite preimage, and unshifted phase warp are rejected by negative controls. + +The independent T74 owner replay reconstructs all 1,332 replica/child windows from the pinned nine-stage template and the literal `ORDER.json`, then checks every one of the 271,728 `FILL.json.gz` roles against its source window, provider width, family capacity, and bin coordinates. It verifies that repeated rank-level windows sharing one `(replica, pair, side, port)` family are time-disjoint; all 408 helper identities occur exactly once per call; and both dispatched providers reproduce the same 408-width inventory and paid profile. The resulting idle profile is `{1:17310, 3:4956, 5:1728, 48:28190}` and the full profile closes the exact rank-mass identity at 4,816,512. The physical count reconciles as `896×74 + 408 helpers + 8 centres + 91 private cleanup buffers + 2 inherited coefficient guards = 66,813`. These are source-bound finite allocation and stock-count checks, not a recertification of the global native/outer admission. + +A separate 90-digit Decimal evaluation places the full-profile root at approximately `0.00172903398264651351771759`, consistent with the conservative value in the claim and above the selected κ. This is a numerical cross-check, not a new exact root certificate. + +The independently reconstructed #2979 local profile and the newer six-skip profile from [PR #3042](https://github.com/CrocSwap/integer-mult-bounds/pull/3042) both fail the requested `κ=0.1` target under the inherited `m=73`, `w=896/9` recursive moment. The PR #3042 claim is pinned at its exact head in [SOURCES.json](SOURCES.json); [PR #3054](https://github.com/CrocSwap/integer-mult-bounds/pull/3054) reports composing that same six-skip word with a larger T740 allocation, which changes its idle profile but leaves the local profile unchanged. At `κ=1/10`, the retained transfer requires `a=1/9`, and the local child term is `(r/73)^(8/9)`. Integer ninth-root brackets, checked by exact integer powers, give + +```text +(PR #2979) (1/w) Σ n_r (r/73)^(8/9) ≥ 48304277901/44800000000 > 1. +(PR #3042) (1/w) Σ n_r (r/73)^(8/9) ≥ 48295445607/44800000000 > 1. +``` + +Both left sides count only paid local children. They omit idle children and the centre path, whose costs are nonnegative, so no packing, extra unpaid coverage, or centre deletion can bring either **fixed profile** to `κ≥0.1` under that transfer. A different local profile, coverage law, or outer transfer could escape this scoped result; none is supplied here. The verifier checks the #2979 profile from its pinned words, reads the PR #3042 profile from its exact pinned claim, and checks rank-by-rank rational floors and both aggregate inequalities. + +## Reproduce + +From the repository root: + +```sh +python3.12 scripts/research_package.py --package research/rank7-v45-profile-audit --check-only +python3.12 scripts/research_package.py --package research/rank7-v45-profile-audit +``` + +The verifier uses only standard-library arithmetic and JSON/gzip inputs pinned in [SOURCES.json](SOURCES.json). Its target screen uses exact integer ninth-root brackets, not floating-point powers. + +## Limits + +The stage-2/3 replay reconstructs only sections that determine the paid profile; it does not independently prove the extraction or rewrite operator identities, or reconstruct compensation and cleanup semantics. The owner replay checks literal finite rank windows, offsets and the stated stock count, but not the underlying binary frame transitions, global stock/precision/hosting premises, fresh native admission or outer release. The `κ=0.1` screen applies only to the audited local profile and inherited moment/transfer. Consequently, the audit does not certify the complete κ claim or update the selected frontier. + +## Open next questions + +The exact target screens show that the #2979 profile and its newer six-skip successor both need a substantial local-profile change (or a changed coverage/outer transfer) before their other open obligations could matter to `κ≥0.1`. For #2979, the next validation step remains a code-disjoint symbolic replay of the extraction/rewrite identities, compensation updates and inverse cleanup on all 632 independent inputs; a separate complete-stock/native/outer review is needed for its reported κ. See the structured questions in [TASK.json](TASK.json). Do not start another lowering census until those obligations are closed or explicitly handed off. + +## Credit + +The audited construction and its predecessor chain remain credited in `research/rank7-joint-endframes/NOTICE` and its README: Dugongue / Marius-Paul Dumitrean for PR #2979, Jeremy Kothe for the PR #2957 rewrites, and all listed predecessor contributors. This small audit does not replace or absorb those contributions. Prepared with substantial AI assistance by OpenAI Codex; Apache-2.0. diff --git a/research/rank7-v45-profile-audit/SOURCES.json b/research/rank7-v45-profile-audit/SOURCES.json new file mode 100644 index 0000000000..d7ba23ca39 --- /dev/null +++ b/research/rank7-v45-profile-audit/SOURCES.json @@ -0,0 +1,151 @@ +{ + "schema_version": 1, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/rank7-joint-endframes/allocation/DISPATCH.json", + "usage": "input", + "git_blob": "9544fee4e6ee1f202cee22bfaeaf229ee3b2515e", + "sha256": "65e435bd68e97243c003677271b88485a29d4d0fae2dff1354100404a145e74c" + }, + { + "path": "research/rank7-joint-endframes/allocation/FILL.json.gz", + "usage": "input", + "git_blob": "8d4fd644d60ba2c98106dc770803b647afdf0963", + "sha256": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39" + }, + { + "path": "research/rank7-joint-endframes/allocation/ORDER.json", + "usage": "input", + "git_blob": "7409c4df1092241729739596c7648bda504e6aad", + "sha256": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1" + }, + { + "path": "research/rank7-joint-endframes/allocation/PROVIDERS.json", + "usage": "input", + "git_blob": "e1d99e12cfa3ac8375984d85c0b040dc36ea1312", + "sha256": "f2edb7922f3029a5d607437e737775ff3371bca49ebab62e5e2495d16d3bf573" + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz", + "usage": "input", + "git_blob": "7a1db55a4d53ee99280be4f3ab7d29f7b2033adf", + "sha256": "d566cfb87b71639d4138e1f89b543e2dd6a7772070226a2a14c799a6835bf21e" + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz", + "usage": "input", + "git_blob": "114808c32b1799da53524bdc25cea67efb60009e", + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e" + }, + { + "path": "research/rank7-joint-endframes/CLAIM.json", + "usage": "input", + "git_blob": "8ec2ce4e440c0b584ee982c551e526a011c9324c", + "sha256": "436e0d297cbdf195445d3697d496ac675e95210b79e70ce602a6a6667a4c6ce9" + }, + { + "path": "research/rank7-joint-endframes/allocation/PROFILE.json", + "usage": "input", + "git_blob": "46a83eeda67ab67cccbffe8b7ad8e44368b40ea7", + "sha256": "94a819747f3ced41f1544ada0036c983fc0c92847b9644380f877a06cd7931cf" + }, + { + "path": "research/rank7-joint-endframes/certificates/RELAX-CAP.json", + "usage": "input", + "git_blob": "14de38f85eedf4a96500173576184a439348328c", + "sha256": "b272680de5842f7fd5f442cd0aeadfd317fe6af266ddee1a1e0738a919ba856e" + }, + { + "path": "research/rank7-joint-endframes/construction/STAGE-PRICES.json", + "usage": "input", + "git_blob": "b06b369ace05b86377f9f73e13586b62b0b77b98", + "sha256": "dfb7d06724bf95367f3fdb398f4828fc70f803d23030bc0eee0b00541457f546" + }, + { + "path": "research/rank7-joint-endframes/data/PARENT-base.json.gz", + "usage": "input", + "git_blob": "1ca8287d6ae5eb45d87db65b369be8d09ba692b2", + "sha256": "54ca34c749e3228d7e2df3d8dbf7aa1568c2872490166997c5962f12fd03da35" + }, + { + "path": "research/rank7-joint-endframes/data/PARENT-extra.json.gz", + "usage": "input", + "git_blob": "c39913ce24cbce4c841eabcc9b1e5a18e4ccc754", + "sha256": "eded756dfe8f411c3d1f80a3ac16516f0ea5dd6f9866728b2179b157630fa7b6" + }, + { + "path": "research/rank7-joint-endframes/data/REWRITES-2957.json", + "usage": "input", + "git_blob": "7bf1633c93951828159b0d9f17d65eda6877101a", + "sha256": "a37ade675876e4f5b00b33066c84f495fccd264863b7eb5d813837b1d01c3e7d" + }, + { + "path": "research/rank7-joint-endframes/data/STAGE1-FRAME-EDITS.json", + "usage": "input", + "git_blob": "66525d293bd0e615e469b4c2191281e8cafb8788", + "sha256": "5fbfce004330ebc1fbac8de264614fe295f1a074811b478db4892c3bc3852cd3" + }, + { + "path": "research/rank7-joint-endframes/data/TRANSFORM-226.json", + "usage": "input", + "git_blob": "bab8518d199e902d72e3b8ec649b62afb74c4e77", + "sha256": "1732a39728c068f9d663111c7876b4e0b96088f3dd3b8e6ff824551b5a711338" + }, + { + "path": "research/rank7-joint-endframes/data/TRANSFORM-228.json", + "usage": "input", + "git_blob": "0097d9dbb972126bde3551ac11d7421494e9c4ec", + "sha256": "82346e6a5173c4822e16b2dad06ca232111b6795a340079f9aceabe0098797c0" + }, + { + "path": "research/rank7-joint-endframes/data/TRANSFORM-230.json", + "usage": "input", + "git_blob": "11edd2e513f8dfd224c53dd8f5ab6bd000098d3a", + "sha256": "8ad70d545695b5d2246fb9e09d46abcc1e42926c1161884f69b77f978a28f46d" + }, + { + "path": "research/rank7-joint-endframes/data/TRANSFORM-363.json", + "usage": "input", + "git_blob": "9260bdf0b87319f212c0a7527693c511cd45c736", + "sha256": "84d2a609739eb30d4d9356fb6f04b2ff32c8823a978d7a51db1ace1d6d2352cc" + }, + { + "path": "research/rank7-joint-endframes/data/TRANSFORM-395.json", + "usage": "input", + "git_blob": "fb2f6a9d2d72324d7dc7505ed46d566cdf8603c8", + "sha256": "065aa5d7713683942bc2156b543681857e33c6e2f30f32cba47e2cbb9d1bef69" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-base.json.gz", + "usage": "input", + "git_blob": "d9aa96a93fea5f7395e7783aef0bc117c0a0ae89", + "sha256": "abaf67bfcb257528658c906b612f57025617592bd7889828f92b97a5f4f4300d" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "usage": "input", + "git_blob": "74f6cb64595c21f7726ae77e69437868620bdcee", + "sha256": "e0eaf64c4d5d324693d43889bce1b9e53e8da00402105c8c978fd102f208bed7" + }, + { + "path": "research/rank7-restore-carrier-skips/CLAIM.json", + "usage": "input", + "git_blob": "47a55a7f68efc1d5babec487d09a1f45f95c3221", + "sha256": "adb2efbaa7c16bf66aede2ac739e445e6fa974d5defbff8b70324f4f10632aa3", + "pin": "head:84cc406ad91ec53fff329a11a445d7effe564a77:research/rank7-restore-carrier-skips/CLAIM.json" + } + ] +} diff --git a/research/rank7-v45-profile-audit/TASK.json b/research/rank7-v45-profile-audit/TASK.json new file mode 100644 index 0000000000..e41c0f3e74 --- /dev/null +++ b/research/rank7-v45-profile-audit/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "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": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "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.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently reconstruct the V45 rank-7 group and losing single-helper control from both pinned PR2942 parent providers, replay the profile-bearing sections through the five stage-2 extraction transforms and fourteen stage-3 rewrites, reproduce all local profiles and weighted deltas, independently rebuild the literal T74 owner windows/roles/stock count, and apply exact local-only moment floors at kappa=0.1 to the reconstructed PR2979 profile and the exact PR3042 six-skip profile used by the later T740 composition.", + "scope_change_reason": "After the bounded V45 and aggregate audit, a separate literal replay of stages 2/3 closed the missing source-binding for paid profile fields in both providers. The T74 handoff motivated an independent schedule/window and bin checker, using no owner engine or producer imports. The donor's target kappa=0.1 then motivated exact integer-power lower bounds on the reconstructed PR2979 profile and a newer six-skip profile pinned from PR3042; both floors apply only to their fixed local profiles under the inherited moment/transfer. None of these checks certifies compensation, cleanup semantics, operator identities, global stock admission, or outer release.", + "bottleneck_link": "The complex supplier is the selected binding side. An independent frame and price reconstruction tests whether the claimed coordinated group actually changes the local rank/width profile and whether the published T74 aggregate pays that local profile.", + "budget_minutes": 60, + "stop_rule": "Do not run another lowering census or claim a new selected kappa until the extraction/rewrite identities, compensation and cleanup, T74 owner chronology, physical/native admission and outer release receive source-bound review.", + "outcome": "partial", + "evidence": "verify.py independently derives F2 spans by XOR closure, reconstructs the V45 and five-group profiles for both providers, then source-replays the five extraction transforms and fourteen literal rewrites to reproduce the profile-bearing final word sections, all published stage prices, and the final profile/inventory. Omitted-frame, stale-preimage and unshifted-warp controls reject. It independently simulates the T74 call order, derives 1,332 owner-child windows, checks all 271,728 role records and their rank-coordinate packing, rejects malformed chronology/missing roles/family collisions/capacity overflow, and reconciles rank mass 4,816,512 plus the 66,813 physical stock formula. At target kappa=1/10 (a=1/9), verified integer ninth-root floors give the reconstructed PR2979 local profile a moment lower bound 48304277901/44800000000 > 1 and the exact PR3042 six-skip claim profile a lower bound 48295445607/44800000000 > 1, both before idle or centre charges. PR3054 reports composing that unchanged local word with a T740 allocation. The 90-digit Decimal root is only a numerical cross-check. The extraction/rewrite operator identities, compensation/cleanup semantics, global stock/native admission and outer release remain open. Canonical main refreshed successfully at d8e0f83f00191df62174b641e9fff055c357f641, priority revision 6; the new PR3042/3054 lineage was checked before submission. GitHub #2979 is merged for archive only, and selected-result still names #1094. The overlap corpus refreshed 332 open PRs and 1,852 discussions at 2026-10-16 23:43 UTC; it found #3015 and #3042 as closer active descendants, which motivated the second target screen. No current novelty claim is made beyond the exact scoped checks.", + "author": "OpenAI Codex", + "ai_assistance": "Substantial AI assistance by OpenAI Codex for mathematical analysis, independent implementation and verification.", + "open_questions": [ + { + "question": "Can the extraction and rewrite identities, compensation updates, and cleanup be independently checked from the same source records?", + "why_it_matters": "The new replay establishes where the paid profile comes from, but a profile-bearing word alone does not prove that the composed stages preserve the exact borrowing operator or arbitrary dirty-state restoration.", + "first_step": "Use a code-disjoint symbolic action on the 632 independent inputs to check each extraction before/after identity and each literal rewrite, then recompute compensation and inverse cleanup from the reconstructed words.", + "blocked_by": "This package only rebuilds fields that determine local rank pricing; the complete equality semantics require a separate exact checker." + }, + { + "question": "Do the five extraction and fourteen rewrite stages preserve their exact linear actions together with compensation and dirty-state cleanup?", + "why_it_matters": "Matching rank profiles and costs does not establish that the composed stages implement the same operator or restore arbitrary dirty helper state.", + "first_step": "Build a code-disjoint symbolic action on all 632 independent inputs; check every stage's before/after matrix, compensation delta, and inverse cleanup using the exact pinned words and transform/rewrite records.", + "blocked_by": "This verifier reconstructs profile-bearing fields and literal owner arithmetic, not the full operator identities or compensation/cleanup semantics." + }, + { + "question": "Does a fresh complete stock, precision, native and outer replay admit the claimed supplier under its inherited assumptions?", + "why_it_matters": "The local rank-bin assignment and 66,813 register count do not prove the global stock schedule, precision margins, or downstream release obligations.", + "first_step": "On a refreshed canonical main base, run the candidate's registered admission/release workflow from the exact pinned sources and independently inspect the resulting stock and precision ledgers for both providers.", + "blocked_by": "This package is standard-library-only and stops at finite owner windows; complete native and outer admission requires the candidate's pinned replay environment." + }, + { + "question": "What source-bound local-profile or coverage change can lower the inherited moment enough to approach kappa=0.1?", + "why_it_matters": "Both the reconstructed #2979 profile and the newer PR3042 six-skip profile alone have moment greater than one at a=1/9, before idle and centre costs, so repacking or removing centre work cannot reach the donor's target with either fixed profile.", + "first_step": "For any proposed changed local word, derive its exact per-call profile and compute the local-only moment floor at a=1/9 before building owners or running a large search.", + "blocked_by": "No changed word, coverage identity, or outer transfer with a target-scale budget is supplied; these finite floors do not exclude other architectures." + } + ] +} diff --git a/research/rank7-v45-profile-audit/VERIFY.json b/research/rank7-v45-profile-audit/VERIFY.json new file mode 100644 index 0000000000..37f8d15618 --- /dev/null +++ b/research/rank7-v45-profile-audit/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/allocation/DISPATCH.json", + "research/rank7-joint-endframes/allocation/FILL.json.gz", + "research/rank7-joint-endframes/allocation/ORDER.json", + "research/rank7-joint-endframes/allocation/PROVIDERS.json", + "research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz", + "research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz", + "research/rank7-joint-endframes/CLAIM.json", + "research/rank7-joint-endframes/allocation/PROFILE.json", + "research/rank7-joint-endframes/certificates/RELAX-CAP.json", + "research/rank7-joint-endframes/construction/STAGE-PRICES.json", + "research/rank7-joint-endframes/data/PARENT-base.json.gz", + "research/rank7-joint-endframes/data/PARENT-extra.json.gz", + "research/rank7-joint-endframes/data/REWRITES-2957.json", + "research/rank7-joint-endframes/data/STAGE1-FRAME-EDITS.json", + "research/rank7-joint-endframes/data/TRANSFORM-226.json", + "research/rank7-joint-endframes/data/TRANSFORM-228.json", + "research/rank7-joint-endframes/data/TRANSFORM-230.json", + "research/rank7-joint-endframes/data/TRANSFORM-363.json", + "research/rank7-joint-endframes/data/TRANSFORM-395.json", + "research/rank7-joint-endframes/data/WORD-base.json.gz", + "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "research/rank7-restore-carrier-skips/CLAIM.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent XOR-span frame chronology and rank accounting for the V45 positive group and losing single-helper control; five-group stage-1 profile/inventory positive control; source replay of five extraction transforms and fourteen literal rewrites for both providers, matching all paid-profile fields and published stage prices; omitted-frame, stale-preimage and unshifted-warp controls; independent T74 schedule simulation, 1,332 owner windows, 271,728 roles, per-provider widths, family nonoverlap, compact rank-bin packing, four failure controls, full profile/rank-mass identity, 91 private cleanup buffers, and 66,813 stock count; exact integer ninth-root lower bounds at kappa=0.1 for the reconstructed PR2979 local profile and the PR3042 six-skip local profile pinned in its exact claim; high-precision numeric root sanity check. Does not certify the operator identities, compensation/cleanup semantics, exact root, global stock/precision, fresh native admission or outer release. The target floors apply only to these fixed profiles and the inherited moment/transfer." + } + ] +} diff --git a/research/rank7-v45-profile-audit/verify.py b/research/rank7-v45-profile-audit/verify.py new file mode 100644 index 0000000000..3fe95ebc48 --- /dev/null +++ b/research/rank7-v45-profile-audit/verify.py @@ -0,0 +1,804 @@ +#!/usr/bin/env python3 +"""Independent XOR-span reconstruction of #2979's staged profile arithmetic. + +This rebuilds the profile-bearing word sections through stages 1-3 and checks +the pinned T74 aggregate numerically. It does not certify the extraction or +rewrite identities, compensation/cleanup semantics, owners, chronology, native +admission, or the exact outer release. +""" +from collections import Counter +from copy import deepcopy +from decimal import Decimal as D, localcontext +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PKG = ROOT / "research" / "rank7-joint-endframes" + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if raw[:2] == b"\x1f\x8b" else raw) + + +@lru_cache(maxsize=100_000) +def _span(vectors): + """Return an F2 span by explicit closure, independent of RREF implementations.""" + out = {0} + for v in vectors: + old = tuple(out) + out.update(x ^ v for x in old) + return frozenset(out) + + +def span(vectors): + return _span(tuple(vectors)) + + +def rank(vectors): + n = len(span(vectors)) + need(n and n & (n - 1) == 0, "span cardinality is not a power of two") + return n.bit_length() - 1 + + +def inside(a, b): + return span(a).issubset(span(b)) + + +def dot_parity(a, b): + return (a & b).bit_count() & 1 + + +def profile(word): + full = span([1 << i for i in range(9)]) + ends = [full] * 112 + ends += [span(z for z in range(1, 512) if not dot_parity(z, p)) for p in word["ports"]] + ends += [full] * 480 + starts = [span([p]) for p in word["ports"]] + [frozenset()] * 592 + for r, rows in word["start_extra"].items(): + starts[int(r)] = span(rows) + for r, rows in word["helper_final"].items(): + ends[int(r)] = span(rows) + + current = list(starts) + paid = Counter() + + def climb(r, rows): + rows = span(rows) + need(inside(current[r], rows), f"nonmonotone register {r}") + d = rank(rows) - rank(current[r]) + if d: + paid[d] += 1 + current[r] = rows + + def step(gate): + if gate[0] == "warp": + need(current[gate[1]] == span(gate[3]), "warp entry frame") + current[gate[1]] = span(gate[4]) + elif gate[0] == "add": + climb(gate[1], gate[-1]) + climb(gate[2], gate[-1]) + elif gate[0] == "scale": + climb(gate[1], gate[-1]) + else: + raise AssertionError(("unknown gate", gate[0])) + + for gate in word["A"]: + step(gate) + for r, rows in zip(word["centers"], word["center_frames"]): + need(current[r] == span(rows), f"center entry frame {r}") + levels = [] + for cut in word["cut"]: + if cut[2] == r: + levels.append(span(word["target_levels"].get(str(cut[1] - 112), []))) + rows = span(rows) + for target in sorted(set(levels), key=len, reverse=True): + if rows != target: + paid[rank(rows) - rank(target)] += 1 + rows = target + warps = {} + for entry in word["warps"]: + warps.setdefault(entry[0], []).append(entry) + for pos in range(len(word["B"]) + 1): + for entry in warps.get(pos, []): + need(current[entry[1]] == span(entry[3]), "B warp entry frame") + current[entry[1]] = span(entry[4]) + if pos < len(word["B"]): + step(word["B"][pos]) + for gate in word["restore"]: + step(gate) + + live = set(range(704)) - set(word["removed"]) + for r in live: + climb(r, ends[r]) + inventory = Counter(rank(ends[r]) - rank(starts[r]) for r in live if r >= 224) + return dict(sorted(paid.items())), dict(sorted(inventory.items())) + + +def roles(gate): + return set(gate[1:3] if gate[0] == "add" else gate[1:2]) + + +def apply_groups(parent, record, chosen): + out = deepcopy(parent) + changed = [] + for name in chosen: + W, helpers = record["groups"][name] + W = span(W) + for h in helpers: + row = record["helper_final_changes"][str(h)] + need(parent["helper_final"][str(h)] == row["old"], "helper old-frame pin") + need(span(row["new"]) == W and rank(row["new"]) == 7, "shared rank-7 helper endpoint") + need(inside(row["new"], row["old"]), "helper endpoint containment") + out["helper_final"][str(h)] = list(row["new"]) + for edit in record["frame_edits"]: + owners = [name for name, (W, _) in record["groups"].items() if inside(edit["new_frame"], W)] + need(len(owners) == 1, ("unique frame-edit owner", edit["section"], edit["index"], owners)) + name = owners[0] + if name not in chosen: + continue + section, i = edit["section"], edit["index"] + gate = out[section][i] + need(gate[:-1] == edit["gate"] and span(gate[-1]) == span(edit["old_frame"]), "gate preimage pin") + need(rank(edit["new_frame"]) == rank(edit["old_frame"]) - 1, "gate codimension one") + need(inside(edit["new_frame"], edit["old_frame"]), "gate hyperplane containment") + need(inside(edit["new_frame"], record["groups"][name][0]), "gate is inside shared W") + gate[-1] = list(edit["new_frame"]) + changed.append((name, section, i)) + for name in chosen: + W = record["groups"][name][0] + for h in record["groups"][name][1]: + for section in ("A", "B", "restore"): + for i, gate in enumerate(out[section]): + if h in roles(gate): + need(inside(gate[-1], W), ("lowered-helper event outside W", name, h, section, i)) + return out, changed + + +def basis_by_closure(vectors): + """Choose an independent basis by explicit XOR closure, without RREF.""" + accepted = [] + current = {0} + for vector in sorted(set(vectors)): + if vector not in current: + accepted.append(vector) + current.update(value ^ vector for value in tuple(current)) + need(span(accepted) == span(vectors), "closure-selected basis spans its input") + return accepted + + +def apply_extraction(word, transform): + """Rebuild the profile-bearing part of one paired extraction from literal gates.""" + x = deepcopy(word) + helper = int(transform["helper"]) + need(str(helper) not in x["helper_final"] and str(helper) not in x["start_extra"], "new extraction helper") + prelude = int(x["prelude_events"]) + protected = set(map(int, x["helper_final"])) | set(map(int, x["start_extra"])) + protected |= {int(c["source"]) for c in x["initial_corrections"]} + removed = set(map(int, x["removed"])) + + before = transform["before"] + after = transform["after"] + need(before and after, "nonempty paired extraction") + for gate in before: + need(gate[0] in ("add", "scale") and gate[-1] == [], "extraction inputs use zero frames") + involved = gate[1:3] if gate[0] == "add" else gate[1:2] + need(all(224 <= int(r) < 704 and int(r) not in protected and int(r) not in removed + for r in involved), "extraction inputs touch only live unprotected helpers") + + normal = int(transform["normal"]) + hyperplane = [v for v in range(1, 512) if not dot_parity(v, normal)] + end_frame = basis_by_closure(hyperplane) + need(rank(end_frame) == 8 and all(not dot_parity(v, normal) for v in end_frame), + "extraction endpoint is the declared rank-8 hyperplane") + need(all(g[0] in ("add", "scale") and inside(g[-1], end_frame) for g in after), + "extraction outputs lie in the declared hyperplane") + + x["A"] = x["A"][:prelude] + deepcopy(before) + x["A"][prelude:] + x["restore"] += deepcopy(after) + x["helper_final"][str(helper)] = end_frame + seen = set() + for edit in transform["frame_changes"]: + section, index = edit["section"], int(edit["index"]) + need(section in ("A", "B", "restore") and (section, index) not in seen, + "unique extraction frame-change address") + need(0 <= index < len(x[section]) and (section != "A" or index >= prelude), + "extraction frame-change address is live") + seen.add((section, index)) + gate = x[section][index] + need(gate[:-1] == edit["gate"] and span(gate[-1]) == span(edit["old_frame"]), + "extraction frame-change preimage") + need(rank(edit["new_frame"]) == rank(edit["old_frame"]) - 1 and + inside(edit["new_frame"], edit["old_frame"]), "extraction frame change lowers one dimension") + gate[-1] = list(edit["new_frame"]) + return x + + +def apply_literal_rewrites(word, rewrites, shift_warps=True): + """Apply declared stage-3 splices by exact old slices and source indices.""" + x = deepcopy(word) + taken = {section: [] for section in ("A", "B", "restore")} + edits = [] + for rewrite in rewrites: + for edit in rewrite["edits"]: + section, start, stop = edit["section"], int(edit["start"]), int(edit["stop"]) + need(section in taken and 0 <= start <= stop <= len(word[section]), "rewrite slice address") + need(section != "A" or start >= int(word["prelude_events"]), "rewrites preserve prelude") + need(word[section][start:stop] == edit["old"] and edit["old"] != edit["new"], + "rewrite old slice is exact and nonvacuous") + for left, right in taken[section]: + need(stop < left or right < start, "declared rewrite slices are disjoint and separated") + taken[section].append((start, stop)) + edits.append((section, start, stop, edit["new"])) + + for section, start, stop, new in sorted(edits, key=lambda row: (row[0], -row[1], -row[2])): + x[section][start:stop] = deepcopy(new) + + b_edits = [(start, stop, len(new) - (stop - start)) + for section, start, stop, new in edits if section == "B"] + if shift_warps: + for warp in x["warps"]: + pos = int(warp[0]) + need(not any(start < pos < stop for start, stop, _ in b_edits), "warp outside edited B slices") + warp[0] = pos + sum(delta for start, stop, delta in b_edits if stop <= pos and start < pos) + return x + + +def profile_projection(word): + """Fields sufficient to determine the complete paid local profile and inventory.""" + names = ("A", "B", "restore", "warps", "ports", "start_extra", "helper_final", + "centers", "center_frames", "cut", "target_levels", "removed", "prelude_events") + return {name: word[name] for name in names} + + +def replay_stages(parent, record, transforms, rewrites): + """Bind stages 2/3 to source records and return their independently priced profiles.""" + stage1, _ = apply_groups(parent, record, list(record["groups"])) + stage2 = stage1 + step_profiles = [] + for expected_step, transform in enumerate(transforms, 1): + need(int(transform["step"]) == expected_step, "extraction order") + stage2 = apply_extraction(stage2, transform) + step_profiles.append(profile(stage2)) + after2 = profile(stage2) + stage3 = apply_literal_rewrites(stage2, rewrites) + after3 = profile(stage3) + return stage1, stage2, stage3, { + "stage2_step_profiles": step_profiles, + "stage2_profile": after2[0], + "stage2_inventory": after2[1], + "stage3_profile": after3[0], + "stage3_inventory": after3[1], + } + + +def price(profile_, weights): + return sum(weights[r] * n for r, n in profile_.items()) + + +def dec_fraction(value): + q = Q(value) + return D(q.numerator) / D(q.denominator) + + +def decimal_root(profile_, replicas): + """High-precision numerical cross-check; intentionally not an exact certificate.""" + with localcontext() as ctx: + ctx.prec = 90 + denominator = D(73 * 896 * replicas) + + def moment(b): + terms = [] + for r, n in profile_.items(): + base = D(73) / D(r) + terms.append(D(n) * D(r) * (b * base.ln()).exp()) + return sum(terms, D(0)) / denominator + + low, high = D(0), D("0.01") + need(moment(low) < 1 < moment(high), "T74 moment root bracket") + for _ in range(320): + mid = (low + high) / 2 + if moment(mid) < 1: + low = mid + else: + high = mid + root = (low + high) / 2 + return root, moment(root) - 1 + + +def target_local_moment_floor(profile_, m=73, families=896, stages=9, decimal_places=8): + """Exact lower bound on the local-only moment at kappa=1/10 (a=1/9).""" + scale = 10 ** decimal_places + denominator = m ** 8 + lower_sum = 0 + rank_bounds = {} + for r, count in profile_.items(): + need(0 < r < m and count > 0, "positive local ranks below the recursive width") + target = scale ** 9 * r ** 8 + lo, hi = 0, scale + while lo + 1 < hi: + mid = (lo + hi) // 2 + if mid ** 9 * denominator <= target: + lo = mid + else: + hi = mid + need(lo ** 9 * denominator <= target < hi ** 9 * denominator, + "integer ninth-root bracket for local child cost") + lower_sum += count * lo + rank_bounds[r] = {"count": count, "floor_over": scale, "floor_numerator": lo} + + # Since (r/m)^(8/9) is the local child cost at a=1/9, + # lo/scale <= (r/m)^(8/9) by the verified integer-power bracket. + moment_lower = Q(lower_sum * stages, scale * families) + need(moment_lower > 1, "candidate local-only moment exceeds one at target a=1/9") + return { + "kappa_target": "1/10", + "primitive_target_a": "1/9", + "moment_lower_bound": str(moment_lower), + "margin_above_one": str(moment_lower - 1), + "local_profile": dict(sorted(profile_.items())), + "per_rank_rational_floors": dict(sorted(rank_bounds.items())), + "scope": "Fixed local profile, m=73, 896 families/9 stages; excludes all nonnegative idle and centre costs.", + } + + +def audit_t74_allocation(final_words, final_profiles): + """Independently rebuild the T74 owner windows and literal stock assignment.""" + allocation = PKG / "allocation" + template = read(allocation / "vendor/TEMPLATE.json.gz") + plan = read(allocation / "vendor/PLAN.json.gz") + order = read(allocation / "ORDER.json") + raw_dispatch = read(allocation / "DISPATCH.json") + fill = read(allocation / "FILL.json.gz") + claimed_profile = {int(k): int(v) for k, v in read(allocation / "PROFILE.json").items()} + provider_registry = read(allocation / "PROVIDERS.json") + replicas = 74 + calls = 9 * replicas + + def owner_windows(candidate_order): + need(len(candidate_order) == calls, "T74 has exactly nine calls per replica") + blocks = {} + current_stage = None + for event in template["execution_schedule"]: + kind = event["kind"] + if kind in ("bank_padding_cover_sweep", "translate_every_live_family"): + continue + if kind == "local_cover_sweep": + current_stage = int(event["stage"]) + need(current_stage not in blocks, "one source block per local stage") + blocks[current_stage] = [] + need(current_stage is not None, "source event belongs to a local stage block") + blocks[current_stage].append(event) + need(set(blocks) == set(range(9)), "nine ordered local source stages") + + pair_by_stage = {int(e["stage"]): int(e["pair"]) + for e in template["recipe"] if e["kind"] == "local"} + need(set(pair_by_stage) == set(range(9)), "each source stage has one pair class") + child_rank = {} + ports = set() + for item in template["idle_children"]: + child, rank_, port = int(item["child"]), int(item["rank"]), int(item["port"]) + need(child not in child_rank or child_rank[child] == rank_, "consistent child rank across ports") + child_rank[child] = rank_ + ports.add(port) + need(ports == set(range(112)), "template covers all 112 ports") + + progress = [0] * replicas + last_pair_use = {} + windows = {} + for time, call in enumerate(candidate_order): + need(len(call) == 2 and all(type(v) is int for v in call), "integer stage/replica call") + stage, replica = call + need(0 <= replica < replicas and 0 <= stage < 9, "call stage and replica bounds") + need(stage == progress[replica], "each replica advances through source stages in order") + progress[replica] += 1 + for event in blocks[stage]: + kind = event["kind"] + if kind == "local_cover_sweep": + need(int(event["stage"]) == stage, "local sweep is in its declared stage") + last_pair_use[replica, pair_by_stage[stage]] = time + elif kind == "bridge": + last_pair_use[replica, int(event["src"])] = time + last_pair_use[replica, int(event["dst"])] = time + elif kind == "idle_cover_sweep": + pair = int(event["pair"]) + begin = last_pair_use.get((replica, pair), -1) + for child in map(int, event["child_indices"]): + if child not in child_rank: + continue + key = (replica, child) + need(key not in windows, "one owner window per replica/child") + windows[key] = (child_rank[child], begin, time) + elif kind in ("terminal_Y_translations", "terminal"): + pass + else: + need(False, "recognized source schedule event") + need(progress == [9] * replicas, "complete source progression for every replica") + need(len(windows) == replicas * len(child_rank), "complete owner-window coverage") + + # Several rank-level windows reuse the same (replica, pair, side, port) + # family. Check the actual half-open time intervals before sharing stock. + pairs = {int(k): int(v) for k, v in plan["pairs"].items()} + sides = {int(k): int(v) for k, v in plan["sides"].items()} + need(set(pairs) == set(child_rank) and set(sides) == set(child_rank), + "every active child has a pair and side") + need(set(pairs.values()) == set(range(4)) and set(sides.values()) == {0, 1}, + "four pair classes and two sides define eight families") + by_family = {} + for (replica, child), (rank_, begin, end) in windows.items(): + need(rank_ > 0 and begin < end, "positive-capacity nonempty owner interval") + family = (replica, pairs[child], sides[child]) + by_family.setdefault(family, []).append((begin, end, child)) + need(len(by_family) == replicas * 8, "eight distinct physical family classes per replica") + for intervals in by_family.values(): + intervals.sort() + for left, right in zip(intervals, intervals[1:]): + need(left[1] <= right[0], "reused physical family windows do not overlap") + return windows, pairs, sides + + windows, pair_of_child, side_of_child = owner_windows(order) + dispatch = {(int(stage), int(replica)): provider for stage, replica, provider in raw_dispatch} + need(len(dispatch) == len(raw_dispatch) == calls, "unique provider dispatch for every call") + need(set(dispatch) == {tuple(call) for call in order}, "dispatch binds exactly the ordered calls") + provider_to_word = {"gauge44": "base", "extra": "extra"} + need(set(dispatch.values()) == set(provider_to_word), "both declared providers are used") + + widths_by_provider = {} + local_by_provider = {} + word_records = {} + for provider, variant in provider_to_word.items(): + word = final_words[variant] + live_helpers = sorted(set(range(224, 704)) - set(map(int, word["removed"]))) + need(len(live_helpers) == 408, "408 live helper registers in each final word") + widths = [] + for helper in live_helpers: + start_rank = rank(word["start_extra"].get(str(helper), [])) + endpoint = word["helper_final"].get(str(helper)) + end_rank = rank(endpoint) if endpoint is not None else 9 + need(0 < end_rank - start_rank <= 9, "positive helper rank width") + widths.append(end_rank - start_rank) + need(widths == provider_registry[provider]["widths"], "word-derived ordered provider widths") + local = Counter(final_profiles[variant]) + need(local == Counter({int(k): int(v) for k, v in + provider_registry[provider]["actual_paid_profile"].items()}), + "word-derived paid profile matches provider registry") + widths_by_provider[provider] = widths + local_by_provider[provider] = local + word_records[provider] = {"helpers": len(live_helpers), + "width_inventory": dict(sorted(Counter(widths).items())), + "local_profile": dict(sorted(local.items()))} + + need(fill["columns"] == ["time", "helper", "owner_replica", "child", "port", "offset"], + "literal fill columns") + for stage, replica, provider in fill.get("dispatch_overrides", []): + need(dispatch.get((stage, replica)) == provider, "fill override agrees with final dispatch") + rows = fill["rows"] + need(len(rows) == calls * 408, "one owner role per live helper per call") + + def check_assignment(candidate_rows, candidate_order=order, candidate_dispatch=dispatch): + current_windows, pairs, sides = owner_windows(candidate_order) + need(set(candidate_dispatch) == {tuple(call) for call in candidate_order} and + all(provider in widths_by_provider for provider in candidate_dispatch.values()), + "complete known provider dispatch") + helper_masks = [0] * calls + family_sets = [set() for _ in range(calls)] + occupied = {} + for row in candidate_rows: + need(len(row) == 6 and all(type(value) is int for value in row), "integer owner role") + time, helper, owner, child, port, offset = row + need(0 <= time < calls and 0 <= helper < 408 and 0 <= port < 112, + "role coordinate bounds") + need((owner, child) in current_windows, "role points to an assigned owner child") + capacity, begin, end = current_windows[owner, child] + need(begin < time <= end, "owner role is inside its source chronology window") + helper_bit = 1 << helper + need(not helper_masks[time] & helper_bit, "helper appears once per call") + helper_masks[time] |= helper_bit + family = owner * 896 + (2 * pairs[child] + sides[child]) * 112 + port + need(family < replicas * 896, "physical family index is in stock") + need(family not in family_sets[time], "one role per physical family in each call") + family_sets[time].add(family) + provider = candidate_dispatch[tuple(candidate_order[time])] + width = widths_by_provider[provider][helper] + need(offset >= 0 and offset + width <= capacity, "role fits its source-family rank") + key = (owner, child, port) + mask = ((1 << width) - 1) << offset + need(not occupied.get(key, 0) & mask, "no overlapping source-family coordinates") + occupied[key] = occupied.get(key, 0) | mask + full_helpers = (1 << 408) - 1 + need(helper_masks == [full_helpers] * calls, "all 408 helper identities occur in every call") + + idle = Counter() + for (owner, child), (capacity, _, _) in current_windows.items(): + for port in range(112): + used_mask = occupied.get((owner, child, port), 0) + used = used_mask.bit_count() + need(used <= capacity, "source-family bin capacity") + need(used_mask == (1 << used) - 1, "source-family bins are compact prefixes") + if capacity > used: + idle[capacity - used] += 1 + + total = Counter(idle) + provider_calls = Counter() + for call in candidate_order: + provider = candidate_dispatch[tuple(call)] + provider_calls[provider] += 1 + total.update(local_by_provider[provider]) + total = Counter({rank_: count for rank_, count in total.items() if count}) + need(total == Counter(claimed_profile), "literal owner and local profiles match complete T74 claim") + return idle, total, provider_calls + + idle, total_profile, provider_calls = check_assignment(rows) + rank_mass = sum(rank_ * count for rank_, count in total_profile.items()) + need(rank_mass == 65_088 * replicas == 4_816_512, "exact T74 rank-mass identity") + + word = final_words["base"] + buffer_ids = {register for gate in word["cleanup"] + for register in (gate[1:3] if gate[0] == "add" else gate[1:2]) + if register >= 704} + expected_buffers = {704 + int(helper) for helper in word["helper_final"]} + need(buffer_ids == expected_buffers and len(buffer_ids) == 91, "91 private cleanup buffers are charged") + need(len(final_words["extra"]["centers"]) == len(word["centers"]) == 8, + "both final words retain eight centre registers") + center_range = template["private_namespace"]["centers"] + guard_range = template["private_namespace"]["coefficient"] + centers = int(center_range[1]) - int(center_range[0]) + guards = int(guard_range[1]) - int(guard_range[0]) + need(centers == 8 and guards == 2, "inherited private namespace has eight centres and two guards") + physical_families = 896 * replicas + 408 + centers + len(buffer_ids) + guards + need(physical_families == 66_813, "reconciled T74 physical stock count") + + controls = {} + def rejected(name, operation): + try: + operation() + except AssertionError: + controls[name] = True + else: + need(False, "negative control rejected: " + name) + + bad_order = list(order) + bad_order[0] = [1, bad_order[0][1]] + rejected("malformed_replica_chronology", lambda: owner_windows(bad_order)) + rejected("missing_role", lambda: check_assignment(rows[:-1])) + family_collision = [list(row) for row in rows] + family_collision[1][4] = family_collision[0][4] + rejected("same_call_physical_family_collision", lambda: check_assignment(family_collision)) + over_capacity = [list(row) for row in rows] + first = over_capacity[0] + cap = windows[first[2], first[3]][0] + first[5] = cap + rejected("role_exceeds_family_capacity", lambda: check_assignment(over_capacity)) + + return { + "status": "PASS_INDEPENDENT_T74_OWNER_WINDOWS_AND_PHYSICAL_RECONCILIATION", + "replicas": replicas, + "calls": calls, + "roles": len(rows), + "owner_child_windows": len(windows), + "shared_owner_family_classes": len({(owner, pair_of_child[child], side_of_child[child]) + for owner, child in windows}), + "provider_calls": dict(sorted(provider_calls.items())), + "providers": word_records, + "idle_profile": dict(sorted(idle.items())), + "complete_profile": dict(sorted(total_profile.items())), + "rank_mass": rank_mass, + "live_families": 896 * replicas, + "helpers": 408, + "centres": centers, + "private_buffers": len(buffer_ids), + "guards": guards, + "physical_families": physical_families, + "reused_family_intervals_disjoint": True, + "negative_controls": controls, + } + + +def main(): + selected = read(ROOT / "certificates/selected-result.json") + record = read(PKG / "data/STAGE1-FRAME-EDITS.json") + prices = read(PKG / "construction/STAGE-PRICES.json") + claim = read(PKG / "CLAIM.json") + cap = read(PKG / "certificates/RELAX-CAP.json") + allocation = {int(k): int(v) for k, v in read(PKG / "allocation/PROFILE.json").items()} + weights = {int(k): int(v) for k, v in prices["weights"]["c"].items()} + break_even = int(prices["weights"]["break_even"]) + + rows = {} + for variant in ("base", "extra"): + parent = read(PKG / f"data/PARENT-{variant}.json.gz") + parent_profile, parent_inventory = profile(parent) + need(parent_profile == {int(k): v for k, v in parent["report"]["local_profile"].items()}, "independent parent profile") + need(parent_inventory == {int(k): v for k, v in parent["report"]["width_inventory"].items()}, "independent parent inventory") + + stage1, edits = apply_groups(parent, record, list(record["groups"])) + stage1_profile, stage1_inventory = profile(stage1) + need(len(edits) == 139, "all five groups account for 139 frame edits") + need(stage1_profile == {int(k): v for k, v in record["declared_local_profile"].items()}, "five-group local profile") + need(stage1_inventory == {int(k): v for k, v in record["declared_width_inventory"].items()}, "five-group width inventory") + + v45, v45_edits = apply_groups(parent, record, ["V45"]) + joint_profile, joint_inventory = profile(v45) + need(len(v45_edits) == 61, "V45 frame edit count") + only_one = deepcopy(v45) + v45_helpers = record["groups"]["V45"][1] + for h in v45_helpers[1:]: + only_one["helper_final"][str(h)] = deepcopy(parent["helper_final"][str(h)]) + one_profile, one_inventory = profile(only_one) + delta = lambda newer: price(newer, weights) - price(parent_profile, weights) + joint_delta, one_delta = delta(joint_profile), delta(one_profile) + joint_margin = -joint_delta - len(v45_helpers) * break_even + one_margin = -one_delta - break_even + need((joint_delta, joint_margin) == (-8_388_172, 22_972), "V45 coordinated price and margin") + need((one_delta, one_margin) == (-2_038_159, -53_141), "V45 losing single-helper control") + rows[variant] = { + "parent_profile": parent_profile, + "stage1_profile": stage1_profile, + "stage1_inventory": stage1_inventory, + "v45_profile": joint_profile, + "v45_inventory": joint_inventory, + "v45_edit_count": len(v45_edits), + "v45_delta_units": joint_delta, + "v45_margin_units": joint_margin, + "single_helper": v45_helpers[0], + "single_delta_units": one_delta, + "single_margin_units": one_margin, + "single_inventory": one_inventory, + } + need(rows["base"] == rows["extra"], "provider profile agreement") + + final_rows = {} + final_words = {} + for variant in ("base", "extra"): + final = read(PKG / f"data/WORD-{variant}.json.gz") + final_words[variant] = final + final_profile, final_inventory = profile(final) + need(final_profile == {int(k): v for k, v in final["report"]["local_profile"].items()}, "independent final-word profile") + need(final_inventory == {int(k): v for k, v in final["report"]["width_inventory"].items()}, "independent final-word inventory") + final_rows[variant] = (final_profile, final_inventory) + need(final_rows["base"] == final_rows["extra"], "final provider profile agreement") + final_profile, final_inventory = final_rows["base"] + six_skip_claim = read(ROOT / "research/rank7-restore-carrier-skips/CLAIM.json") + six_skip_profile = {int(k): int(v) for k, v in six_skip_claim["local_profile"].items()} + target_screens = { + "PR2979_reconstructed_word": target_local_moment_floor(final_profile), + "PR3042_six_skip_word_claim_pinned_in_PR3054": target_local_moment_floor(six_skip_profile), + } + + transforms = [read(PKG / f"data/TRANSFORM-{helper}.json") + for helper in (226, 228, 230, 363, 395)] + rewrites = read(PKG / "data/REWRITES-2957.json") + stage_replays = {} + for variant in ("base", "extra"): + parent = read(PKG / f"data/PARENT-{variant}.json.gz") + stage1, stage2, stage3, ledger = replay_stages(parent, record, transforms, rewrites) + final = read(PKG / f"data/WORD-{variant}.json.gz") + for name, actual, expected in (("stage2", ledger["stage2_profile"], profile(stage2)[0]), + ("stage3", ledger["stage3_profile"], profile(stage3)[0])): + need(actual == expected, f"{name} replay ledger reports its derived profile") + stage2_delta = price(profile(stage2)[0], weights) - price(profile(stage1)[0], weights) + stage3_delta = price(profile(stage3)[0], weights) - price(profile(stage2)[0], weights) + need(stage2_delta == int(prices["stage2"]["literal_price_units"]), "stage-2 source replay price") + need(stage3_delta == int(prices["stage3"]["literal_price_units"]), "stage-3 source replay price") + need(profile(stage3) == profile(final), "stage-2/3 replay reproduces both final local profile and inventory") + for field in ("A", "B", "restore", "warps", "ports", "start_extra", "centers", "center_frames", + "cut", "target_levels", "removed", "prelude_events"): + need(stage3[field] == final[field], f"stage-2/3 replay final {field} matches pinned word") + need(set(stage3["helper_final"]) == set(final["helper_final"]), "stage-2/3 replay endpoint inventory") + need(all(span(stage3["helper_final"][h]) == span(final["helper_final"][h]) + for h in final["helper_final"]), "stage-2/3 replay endpoints match pinned spans") + stage_replays[variant] = { + "stage1_delta_units": price(profile(stage1)[0], weights) - price(profile(parent)[0], weights), + "stage2_delta_units": stage2_delta, + "stage3_delta_units": stage3_delta, + "stage2_profile": profile(stage2)[0], + "stage2_inventory": profile(stage2)[1], + "final_profile": profile(stage3)[0], + "final_inventory": profile(stage3)[1], + } + need(stage_replays["base"] == stage_replays["extra"], "base/extra source replay agrees across stages 2/3") + need(stage_replays["base"]["stage1_delta_units"] == int(prices["stage1"]["literal_price_units"]), + "stage-1 source replay price") + + # Semantic failure controls for the new source-bound stage-2/3 replayer. + control_parent = read(PKG / "data/PARENT-base.json.gz") + control_stage1, _ = apply_groups(control_parent, record, list(record["groups"])) + omitted_frame = deepcopy(transforms) + omitted_frame[1]["frame_changes"] = [] + wrong_stage2 = control_stage1 + for transform in omitted_frame: + wrong_stage2 = apply_extraction(wrong_stage2, transform) + wrong_stage3 = apply_literal_rewrites(wrong_stage2, rewrites) + need(profile(wrong_stage3) != profile(read(PKG / "data/WORD-base.json.gz")), + "omitting the declared stage-2 frame change is detected by the final paid profile") + + stale_rewrites = deepcopy(rewrites) + stale_edit = next(edit for rewrite in stale_rewrites for edit in rewrite["edits"] if edit["old"]) + stale_edit["start"] += 1 + stale_edit["stop"] += 1 + try: + apply_literal_rewrites(stage2, stale_rewrites) + except AssertionError: + stale_rewrite_rejected = True + else: + need(False, "stale stage-3 rewrite preimage must be rejected") + unshifted_warps = apply_literal_rewrites(stage2, rewrites, shift_warps=False) + try: + profile(unshifted_warps) + except AssertionError: + unshifted_warp_rejected = True + else: + need(False, "unshifted B-phase warp must be rejected by the profile replay") + + total_delta = price(final_profile, weights) - price(rows["base"]["parent_profile"], weights) + stage_delta_sum = sum(int(prices[f"stage{i}"]["literal_price_units"]) for i in (1, 2, 3)) + need(total_delta == stage_delta_sum == -56_726_747, "final frame-price delta equals three published stage deltas") + need(final_inventory == {int(k): v for k, v in claim["width_inventory"].items()}, "claim width inventory matches independently profiled final word") + need(final_profile == {int(k): v for k, v in claim["local_profile"].items()}, "claim local profile matches independently profiled final word") + + t74_audit = audit_t74_allocation( + final_words, + {variant: row[0] for variant, row in final_rows.items()}, + ) + + calls, replicas = int(claim["calls"]), int(claim["replicas"]) + idle = dict(allocation) + for r, n in final_profile.items(): + idle[r] = idle.get(r, 0) - calls * n + need(all(n >= 0 for n in idle.values()), "T74 profile pays all 666 complete local calls") + idle = {r: n for r, n in sorted(idle.items()) if n} + need(sum(r * n for r, n in allocation.items()) == replicas * 65_088, "complete T74 rank-mass identity") + need(sum(r * n for r, n in final_profile.items()) * calls + sum(r * n for r, n in idle.items()) == replicas * 65_088, + "local plus idle profile closes T74 rank mass") + need(allocation == {int(k): v for k, v in claim["profile"].items()}, "T74 profile matches claim") + + root, root_residual = decimal_root(allocation, replicas) + selected_kappa = Q(selected["kappa"]) + claimed_kappa = Q(claim["kappa"]) + cap_lower = dec_fraction(cap["cap_lower"]) + cap_upper = dec_fraction(cap["cap_upper"]) + need(claimed_kappa > selected_kappa, "claimed candidate kappa strictly exceeds selected kappa") + need(root > dec_fraction(claim["complex_lower"]), "numerical T74 root exceeds claimed conservative complex lower bound") + need(root < cap_lower < cap_upper, "numerical T74 root lies below the fixed-inventory cap bracket") + need(D(0) < root - dec_fraction(claimed_kappa) < D("1e-24"), "claim is a conservative floor of the numerical T74 root") + + print(json.dumps({ + "status": "PASS_V45_INDEPENDENT_LOCAL_PROFILE_AND_T74_AGGREGATE_ARITHMETIC", + "v45": rows["base"], + "final_local_profile": final_profile, + "final_width_inventory": final_inventory, + "local_stage_delta_units": total_delta, + "sum_of_stage_deltas_units": stage_delta_sum, + "source_replayed_stages_1_to_3": stage_replays["base"], + "stage_replay_controls": { + "omitted_stage2_frame_change_detected": True, + "stale_stage3_preimage_rejected": stale_rewrite_rejected, + "unshifted_stage3_warp_rejected": unshifted_warp_rejected, + }, + "t74_profile": allocation, + "t74_idle_profile_after_666_calls": idle, + "t74_rank_mass": sum(r * n for r, n in allocation.items()), + "root_decimal_crosscheck_only": str(root), + "root_moment_residual_decimal": str(root_residual), + "claimed_kappa_minus_selected_exact": str(claimed_kappa - selected_kappa), + "t74_owner_and_physical_audit": t74_audit, + "kappa010_local_only_screens": target_screens, + "limitations": [ + "Stage-2/3 replay checks the profile-bearing word sections and prices, not compensation or cleanup semantics.", + "The extracted operator identities and the fourteen rewrite identities are not independently certified here.", + "The local T74 owner assignment and stock arithmetic are independently rebuilt; complete global stock, native admission, and outer release remain separate obligations.", + "The Decimal root is a numeric cross-check, not an exact root certificate." + ] + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()