diff --git a/research/pr1407-complex-moment-audit-seed39/CLAIM.json b/research/pr1407-complex-moment-audit-seed39/CLAIM.json new file mode 100644 index 0000000000..bd4cb09de6 --- /dev/null +++ b/research/pr1407-complex-moment-audit-seed39/CLAIM.json @@ -0,0 +1,36 @@ +{ + "run": 4, + "assignment_seed": 39, + "track": "complex supplier", + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "started_utc": "2026-10-14T00:18:11Z", + "planned_finish_utc": "2026-10-14T01:08:11Z", + "verification_start_utc": "2026-10-14T00:55:41Z", + "status": "completed", + "candidate_tasks": [ + { + "scope": "PR1094 neutral-then-strict two-bin whole-helper path search.", + "overlap": "Dropped after live refresh found PR1407 covering neutral whole-helper hosting paths." + }, + { + "scope": "PR1387 operator-preserving subset of simultaneous idle-axis optimum.", + "overlap": "Open PR #1387 and completed discussion #1339 already cover this optimum and counterexample." + }, + { + "scope": "Independent arithmetic audit of PR1407 complex profile and kappa receipts.", + "overlap": "Selected as explicitly complementary second audit; no separate arithmetic-audit claim found at refresh." + } + ], + "object": { + "pr": 1407, + "head": "d8640f5b7ae99b43f5d56146cb94ca62b8b3835d", + "candidate_profile_delta": "+e1 - 7e7 + 3e16" + }, + "method": "Third code-disjoint exact interval implementation using binary-reduced atanh log bounds and positive Taylor exponential with geometric tail; verify primary and conservative complex endpoint signs, exact kappa grid, rank mass/deficit, unchanged bit endpoint and failure controls. Does not replay the construction.", + "expected_deliverable": "Small registered research package and one focused independent-verification PR if the final replay remains green.", + "finish_time_utc": "2026-10-14T01:08:11Z", + "coordination": "No pinned sprint issue exists; local claim recorded. PR #1407 itself has two exact moment engines and pending cross-vendor/fresh-context review; this audit uses an independent third implementation.", + "completed_utc": "2026-10-14T00:42:32Z", + "result": "The exact Fraction replay certified the selected and PR1407 primary and conservative complex root endpoint signs, profile delta and conservation, unchanged bit endpoint, and primary/conservative kappa grids; four deliberate mutation controls rejected.", + "reproduction": "python3.12 scripts/research_package.py --package research/pr1407-complex-moment-audit-seed39" +} diff --git a/research/pr1407-complex-moment-audit-seed39/README.md b/research/pr1407-complex-moment-audit-seed39/README.md new file mode 100644 index 0000000000..7f22c69cb9 --- /dev/null +++ b/research/pr1407-complex-moment-audit-seed39/README.md @@ -0,0 +1,108 @@ +# Independent arithmetic audit of PR #1407's complex profile + +**Status: completed, scoped independent verification. No new construction or κ claim.** + +PR #1407 proposes a neutral whole-helper hosting construction for the selected +PR1094 owner map. I do not repeat its search or replay its owner paths. This +package independently checks the resulting profile arithmetic with a third, +code-disjoint exact interval engine: the primary and conservative complex root +brackets, the unchanged bit ceiling, and the published κ grid. The upstream PR +reports two exact moment engines; this audit adds a separate rational +atanh/Taylor implementation while leaving its construction proof and native +admission as inherited claims. + +## Frozen data and exact result + +The research/source base is +`bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. Before publication, `main` +advanced to `410026dc5513b87db92ae98571d1d5984c69a983` through three +reconciliation commits. The selected certificate and the seven other pinned repository +inputs/provenance files have identical Git blobs at both commits; the audit +branch is based on the refreshed `main`, while `TASK.json` and `SOURCES.json` +retain the exact research base. The selected record binds at +`κ = 836330098538459/500000000000000000`, with complex endpoint +`67018507072324140917/40000000000000000000000` and bit endpoint +`1733427039589844234749/10^24`. The source construction and maintainer review +are pinned by `SOURCES.json`. + +The external candidate snapshot is PR #1407 at exact head +`d8640f5b7ae99b43f5d56146cb94ca62b8b3835d`. `REFERENCE.json` contains the +candidate profile, endpoint receipts and the original SHA256 and Git blob +identifiers for PR #1407's `PROFILE.json`, `RESULT.json` and `ASSEMBLY.json`. +I fetched that exact PR commit through the upstream pull ref and independently +recomputed all three Git blob IDs and content SHA256 values; all six matched +the recorded pins. Its snapshot hash is also pinned in `SOURCES.json`. + +The candidate profile changes from the selected +`{1:349604, 2:60192, 3:62585, 4:20448, 5:11808, 7:7, 8:1152, 48:4866}` +to +`{1:349605, 2:60192, 3:62585, 4:20448, 5:11808, 8:1152, 16:3, 48:4866}`. +The exact delta is `+e1 - 7e7 + 3e16`: rank mass and deficit stay fixed, +while the positive-rank call count drops by three. The priced parameters are +`m=73`, `W=14336`; the primary complex moment has no added surcharge. The +conservative check includes the inherited term +`32*m*N/(10^16*W) * m^a`. + +| profile and moment | lower endpoint (`M(a)-1` scaled by `10^32`) | upper endpoint (`M(a)-1` scaled by `10^32`) | +|---|---:|---:| +| selected primary | `[-130421533, -130421532]` accepted | `[162472375, 162472376]` rejected | +| PR #1407 primary | `[-159548291, -159548290]` accepted | `[133342011, 133342012]` rejected | +| selected conservative | `[-281245180, -281245179]` accepted | `[11648729, 11648730]` rejected | +| PR #1407 conservative | `[-171561767, -171561766]` accepted | `[121328535, 121328536]` rejected | + +Each displayed integer interval is divided by `10^32`. The exact brackets +reproduce the receipts. The candidate's primary and conservative complex +brackets both move above the selected brackets, and both remain below the +unchanged bit endpoint. Exact flooring of `a/(1+a)` to the repository's +`10^-18` κ grid reproduces the candidate and conservative κ values. The +primary κ difference is exactly `161104813/7812500000000000`. + +## Independent interval method + +`verify.py` uses only Python's standard library and `Fraction` arithmetic. It +computes logarithms after binary range reduction with 48 positive atanh terms +and the explicit geometric tail +`2*z^(2N+1)/((2N+1)*(1-z^2))`, where `0 <= z <= 1/3`. It encloses each +positive exponential with 32 Taylor terms and a geometric bound on the +remaining tail. The verifier does not import either moment engine used by +PR #1407 or the selected assembly. + +Failure controls mutate one rank-16 count, swap accepted and rejected endpoint +labels, change κ by one grid unit, and omit the conservative surcharge. Every +mutation is rejected. The saved exact replay is [RESULT.json](RESULT.json). + +Reproduce from the repository root with Python 3.12: + +```sh +python3.12 scripts/research_package.py --package research/pr1407-complex-moment-audit-seed39 +``` + +Expected: `PASS_REGISTERED_RESEARCH_PACKAGE research/pr1407-complex-moment-audit-seed39 outcome=completed`. + +## Scope and limits + +This confirms the finite arithmetic receipts derived from the two histograms. +It does not verify PR #1407's 24 owner moves, its all-input dirty-state +argument, strict source-event windows, native T16 execution, controller, +invoice, all 47 outer inequalities, or full ancestry. The audit does not +establish that the published reassignment realizes the candidate histogram. +PR review and hosted-workflow status are mutable. This package pins the +candidate content at the exact head above and makes no claim that its +construction, CI or review gates are approved. + +## Open next questions + +The next useful step is a fresh, independent replay of PR #1407's native path +and a role-by-role check of its eleven neutral-then-concentrating paths. That +matters because profile arithmetic alone cannot establish physical admission. +The open blocker is the draft PR's pending review and workflow approval. + +## Credit + +PAI (@pai-scaffolde) supplies PR #1407's candidate profile and receipts. Rohan +Arun's PR #1094 supplies the selected owner map; Jeremy Kothe and Hao Yan / FanPUYen +supply the retained packing and controller lineage. The selected construction +and its maintainer review remain the pinned baseline. Prepared by Cinna Davis +(@1337isnot1337) with substantial OpenAI Codex assistance in review, exact +arithmetic design, implementation and writing. This is a code-disjoint audit, +not independent human review. New material is Apache-2.0. diff --git a/research/pr1407-complex-moment-audit-seed39/REFERENCE.json b/research/pr1407-complex-moment-audit-seed39/REFERENCE.json new file mode 100644 index 0000000000..a9d16f4fae --- /dev/null +++ b/research/pr1407-complex-moment-audit-seed39/REFERENCE.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "source": { + "repository": "CrocSwap/integer-mult-bounds", + "pr": 1407, + "head": "d8640f5b7ae99b43f5d56146cb94ca62b8b3835d", + "files": [ + { + "name": "profile", + "path": "research/astra-ultra-hosting-20261013/data/PROFILE.json", + "git_blob": "54c3e1076c6cccbe6c6a90b39b2aba7b800762e6", + "sha256": "e3f778d24ce02c1ddc21b4632c3e0d99e064d8db359b03b019fd8b37baf815b5" + }, + { + "name": "result", + "path": "research/astra-ultra-hosting-20261013/RESULT.json", + "git_blob": "6505aafdcafeb1bcd37aa2ccbf0bd9c5eeab99e0", + "sha256": "6be31e95e41bcc83577b364b01a0339d16a8f6f09277b9d8d964c0ea4c1f158c" + }, + { + "name": "assembly", + "path": "research/astra-ultra-hosting-20261013/receipts/ASSEMBLY.json", + "git_blob": "997cce16c3362b27250c3d0de0a29192c9dd4376", + "sha256": "fe9dd283cdc5034b74fcca6d2f344da08a876ef1fde6a4db35626a680a12183f" + } + ] + }, + "candidate_profile": { + "1": 349605, + "2": 60192, + "3": 62585, + "4": 20448, + "5": 11808, + "8": 1152, + "16": 3, + "48": 4866 + }, + "result": { + "kappa": "836340409246491/500000000000000000", + "kappa_decimal": "0.001672680818492982", + "baseline_kappa": "836330098538459/500000000000000000", + "delta": "161104813/7812500000000000", + "complex_lower": "837741683691654218469/500000000000000000000000", + "complex_decimal": "0.001675483367383308436938", + "bit_lower": "1733427039589844234749/1000000000000000000000000", + "conservative_complex_lower": "837741682260907314779/500000000000000000000000", + "conservative_kappa": "1672680815641053/1000000000000000000", + "conservative_kappa_decimal": "0.001672680815641053", + "profile": { + "1": 349605, + "2": 60192, + "3": 62585, + "4": 20448, + "5": 11808, + "8": 1152, + "16": 3, + "48": 4866 + }, + "live": 14336, + "rank_mass": 1041408, + "deficit": 5120 + }, + "complex_moments": [ + { + "surcharge": false, + "endpoint": "837741683691654218469/500000000000000000000000", + "accept": true + }, + { + "surcharge": false, + "endpoint": "1675483367383308436939/1000000000000000000000000", + "accept": false + } + ], + "conservative_complex_moments": [ + { + "surcharge": true, + "endpoint": "837741682260907314779/500000000000000000000000", + "accept": true + }, + { + "surcharge": true, + "endpoint": "1675483364521814629559/1000000000000000000000000", + "accept": false + } + ], + "surcharge_model": { + "complex": false, + "bit": true + } +} diff --git a/research/pr1407-complex-moment-audit-seed39/RESULT.json b/research/pr1407-complex-moment-audit-seed39/RESULT.json new file mode 100644 index 0000000000..e7059326cb --- /dev/null +++ b/research/pr1407-complex-moment-audit-seed39/RESULT.json @@ -0,0 +1,101 @@ +{ + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "base_conservative_bracket": [ + { + "accept": true, + "endpoint": "1675462673946628390003/1000000000000000000000000", + "moment_minus_one_interval_scaled_1e32": [ + "-281245180", + "-281245179" + ] + }, + { + "accept": false, + "endpoint": "418865668486657097501/250000000000000000000000", + "moment_minus_one_interval_scaled_1e32": [ + "11648729", + "11648730" + ] + } + ], + "base_primary_bracket": [ + { + "accept": true, + "endpoint": "67018507072324140917/40000000000000000000000", + "moment_minus_one_interval_scaled_1e32": [ + "-130421533", + "-130421532" + ] + }, + { + "accept": false, + "endpoint": "837731338404051761463/500000000000000000000000", + "moment_minus_one_interval_scaled_1e32": [ + "162472375", + "162472376" + ] + } + ], + "bit_endpoint_unchanged": "1733427039589844234749/1000000000000000000000000", + "call_delta": -3, + "candidate_conservative_bracket": [ + { + "accept": true, + "endpoint": "837741682260907314779/500000000000000000000000", + "moment_minus_one_interval_scaled_1e32": [ + "-171561767", + "-171561766" + ] + }, + { + "accept": false, + "endpoint": "1675483364521814629559/1000000000000000000000000", + "moment_minus_one_interval_scaled_1e32": [ + "121328535", + "121328536" + ] + } + ], + "candidate_primary_bracket": [ + { + "accept": true, + "endpoint": "837741683691654218469/500000000000000000000000", + "moment_minus_one_interval_scaled_1e32": [ + "-159548291", + "-159548290" + ] + }, + { + "accept": false, + "endpoint": "1675483367383308436939/1000000000000000000000000", + "moment_minus_one_interval_scaled_1e32": [ + "133342011", + "133342012" + ] + } + ], + "conservative_kappa_grid": "1672680815641053/1000000000000000000", + "construction_scope": "Arithmetic only; no owner/window/path, native compiler, controller, all-47-outer-constraint or full ancestry replay.", + "exact_kappa_gain": "161104813/7812500000000000", + "external_head": "d8640f5b7ae99b43f5d56146cb94ca62b8b3835d", + "external_source_sha256": { + "assembly": "fe9dd283cdc5034b74fcca6d2f344da08a876ef1fde6a4db35626a680a12183f", + "profile": "e3f778d24ce02c1ddc21b4632c3e0d99e064d8db359b03b019fd8b37baf815b5", + "result": "6be31e95e41bcc83577b364b01a0339d16a8f6f09277b9d8d964c0ea4c1f158c" + }, + "failure_controls": [ + "added rank-16 child", + "swap accepted/rejected endpoint labels", + "one-grid-unit kappa mutation", + "omit conservative surcharge" + ], + "interval_method": "standard-library Fraction; 48-term binary-reduced atanh logarithm bounds and 32-term positive Taylor exponential with geometric tail", + "primary_kappa_grid": "836340409246491/500000000000000000", + "profile_delta": { + "1": 1, + "7": -7, + "16": 3 + }, + "rank_mass_delta": 0, + "status": "PASS_PR1407_COMPLEX_PROFILE_ARITHMETIC_INDEPENDENT_AUDIT" +} diff --git a/research/pr1407-complex-moment-audit-seed39/SOURCES.json b/research/pr1407-complex-moment-audit-seed39/SOURCES.json new file mode 100644 index 0000000000..a72ad30ba8 --- /dev/null +++ b/research/pr1407-complex-moment-audit-seed39/SOURCES.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/REPLAY.json", + "usage": "input", + "git_blob": "2cfb7fffa7cd78f418be16c13224c3206b6d0183", + "sha256": "ce0678fa7abaab221de74baeace0c6696d5ea23a36719a58cff230215a06aae7" + }, + { + "path": "research/community-batch1099-audit/check_frontier1094.py", + "usage": "provenance", + "git_blob": "1c171898e4f58fbdeca81424c9932ec2c6bbb9c8", + "sha256": "2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py", + "usage": "provenance", + "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/outer.py", + "usage": "provenance", + "git_blob": "43007488ad2c43187c77cc6798beff8b1cd76ad2", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + } + ], + "external_sources": { + "repository": "CrocSwap/integer-mult-bounds", + "pr": 1407, + "head": "d8640f5b7ae99b43f5d56146cb94ca62b8b3835d", + "snapshot": "REFERENCE.json", + "snapshot_sha256": "3e1657810dc9ceff2e36fc0cd030c2a03f7457e55ba9bad3cd7d49fb58e6ca5c", + "files": [ + { + "name": "profile", + "path": "research/astra-ultra-hosting-20261013/data/PROFILE.json", + "git_blob": "54c3e1076c6cccbe6c6a90b39b2aba7b800762e6", + "sha256": "e3f778d24ce02c1ddc21b4632c3e0d99e064d8db359b03b019fd8b37baf815b5" + }, + { + "name": "result", + "path": "research/astra-ultra-hosting-20261013/RESULT.json", + "git_blob": "6505aafdcafeb1bcd37aa2ccbf0bd9c5eeab99e0", + "sha256": "6be31e95e41bcc83577b364b01a0339d16a8f6f09277b9d8d964c0ea4c1f158c" + }, + { + "name": "assembly", + "path": "research/astra-ultra-hosting-20261013/receipts/ASSEMBLY.json", + "git_blob": "997cce16c3362b27250c3d0de0a29192c9dd4376", + "sha256": "fe9dd283cdc5034b74fcca6d2f344da08a876ef1fde6a4db35626a680a12183f" + } + ] + } +} diff --git a/research/pr1407-complex-moment-audit-seed39/TASK.json b/research/pr1407-complex-moment-audit-seed39/TASK.json new file mode 100644 index 0000000000..8c95603188 --- /dev/null +++ b/research/pr1407-complex-moment-audit-seed39/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently recompute the primary and conservative complex moment root brackets and exact kappa rounding reported for PR1407 from its published histogram, using a code-disjoint standard-library rational interval implementation.", + "scope_change_reason": "The live refresh found PR1407 claiming the neutral whole-helper paths proposed for this run. To avoid repeating its construction search, the scope changed to a narrowly independent arithmetic audit. PR1407 reports two exact engines and pending cross-vendor review; this third implementation checks profile-to-root and root-to-kappa receipts only.", + "bottleneck_link": "The complex supplier binds the selected conditional kappa. Independent exact root and transfer checks can authenticate the proposed profile improvement without treating owner-path or native admission as proved by arithmetic.", + "budget_minutes": 50, + "stop_rule": "Rebuild the candidate and selected profiles from pinned receipts; certify accepted/rejected endpoints for both primary and conservative complex moments; verify the kappa grid and binding side with exact fractions. Stop after this arithmetic scope or on the first mismatch; do not replay the neutral-path construction.", + "outcome": "completed", + "evidence": "The independent atanh/Taylor Fraction engine certifies both endpoints of the base and PR1407 primary complex root brackets and both conservative brackets with the claimed signs. It verifies the exact profile delta, conserved rank mass and deficit, unchanged bit ceiling, and both exact kappa roundings and delta. Four deliberate failure controls reject a mutated histogram, inverted endpoint labels, a one-grid-unit kappa change and omission of the conservative surcharge.", + "author": "Cinna Davis (@1337isnot1337)", + "ai_assistance": "Substantial OpenAI Codex assistance in overlap review, exact arithmetic design, implementation, verification and writing.", + "open_questions": [ + { + "question": "Do PR1407\u2019s 24 owner moves satisfy the full source-window, same-deadline dirty-state argument and exact native/controller path on a fresh review?", + "why_it_matters": "This audit verifies the price of the published profile but does not establish that the proposed reassignment produces that profile in the construction.", + "first_step": "Re-run the pinned PR1407 verify-native path in a clean temporary output, then inspect each of the eleven neutral-then-concentrating paths against its frozen source-event intervals.", + "blocked_by": "PR1407 is a draft; its independent cross-vendor review and hosted workflows are pending maintainer approval." + } + ] +} diff --git a/research/pr1407-complex-moment-audit-seed39/VERIFY.json b/research/pr1407-complex-moment-audit-seed39/VERIFY.json new file mode 100644 index 0000000000..0d0a7d4f38 --- /dev/null +++ b/research/pr1407-complex-moment-audit-seed39/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/REPLAY.json", + "research/community-batch1099-audit/check_frontier1094.py", + "research/pr1407-complex-moment-audit-seed39/REFERENCE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Uses only standard-library Fraction arithmetic and a code-disjoint atanh/Taylor interval engine; verifies pinned selected profile agreement, the PR1407 profile delta, primary and surcharge-inclusive complex root brackets, kappa rounding and four rejection controls." + } + ] +} diff --git a/research/pr1407-complex-moment-audit-seed39/verify.py b/research/pr1407-complex-moment-audit-seed39/verify.py new file mode 100644 index 0000000000..ee6a66ca23 --- /dev/null +++ b/research/pr1407-complex-moment-audit-seed39/verify.py @@ -0,0 +1,244 @@ +#!/usr/bin/env python3 +"""Code-disjoint exact interval check of PR1407's complex moment receipts.""" +from collections import Counter +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PKG = Path(__file__).resolve().parent +REFERENCE_SHA256 = "3e1657810dc9ceff2e36fc0cd030c2a03f7457e55ba9bad3cd7d49fb58e6ca5c" +M, W = 73, 14336 +LOG_TERMS, EXP_TERMS = 48, 32 +PRINT_SCALE = 10**32 + + +def require(ok, message): + if not ok: + raise AssertionError(message) + + +def atanh_log(z): + """Enclose 2*atanh(z) with a positive rational tail bound.""" + require(0 <= z <= F(1, 3), "range-reduced atanh input") + total = F(0) + for j in range(LOG_TERMS): + total += 2 * z ** (2*j + 1) / (2*j + 1) + tail = 2 * z ** (2*LOG_TERMS + 1) / ((2*LOG_TERMS + 1) * (1-z*z)) + return total, total + tail + + +def ln_integer(n): + """Exact interval for ln(n); binary reduction keeps the series ratio <=1/9.""" + require(type(n) is int and n >= 1, "positive integer logarithm input") + if n == 1: + return F(0), F(0) + k = n.bit_length() - 1 + reduced = F(n, 1 << k) + z = (reduced - 1) / (reduced + 1) + ln2 = atanh_log(F(1, 3)) + ln_reduced = atanh_log(z) + return k*ln2[0] + ln_reduced[0], k*ln2[1] + ln_reduced[1] + + +def ln_ratio(n, d): + """Exact interval for ln(n/d), from independently enclosed integer logs.""" + nl, nu = ln_integer(n) + dl, du = ln_integer(d) + return nl-du, nu-dl + + +def exp_positive(xl, xu): + """Exact interval for exp(x), 0<=xl<=xu<1/10, with a geometric tail.""" + require(0 <= xl <= xu < F(1, 10), "small positive exponential domain") + + def partial_and_tail(x): + s = t = F(1) + for j in range(1, EXP_TERMS): + t *= x / j + s += t + next_term = t * x / EXP_TERMS + tail = next_term / (1 - x/(EXP_TERMS+1)) + return s, s + tail + + return partial_and_tail(xl)[0], partial_and_tail(xu)[1] + + +def moment_interval(profile, alpha, surcharge): + """Enclose the pinned complex moment, with the inherited optional envelope.""" + require(0 < alpha < F(1, 50), "complex exponent interval") + lower = upper = F(0) + for r, count in profile.items(): + require(type(r) is int and 0 < r < M and type(count) is int and count > 0, + "positive paid profile with ranks below width") + ll, lu = ln_ratio(M, r) + pl, pu = exp_positive(alpha*ll, alpha*lu) + scale = F(count*r, M*W) + lower += scale*pl + upper += scale*pu + if surcharge: + ml, mu = exp_positive(alpha*ln_integer(M)[0], alpha*ln_integer(M)[1]) + factor = F(32*M*sum(profile.values()), 10**16*W) + lower += factor*ml + upper += factor*mu + return lower, upper + + +def parse_bracket(rows, surcharge): + rows = [x for x in rows if x["surcharge"] is surcharge] + require(len(rows) == 2, "published lower and upper endpoint rows") + return [(F(x["endpoint"]), x["accept"]) for x in rows] + + +def verify_bracket(profile, rows, surcharge, label): + result = [] + for endpoint, accepts in parse_bracket(rows, surcharge): + lo, hi = moment_interval(profile, endpoint, surcharge) + if accepts: + require(hi < 1, f"{label}: accepted endpoint has strict upper moment < 1") + else: + require(lo > 1, f"{label}: rejected endpoint has strict lower moment > 1") + result.append({"endpoint": str(endpoint), "accept": accepts, + "moment_minus_one_interval_scaled_1e32": scaled_interval(lo-1, hi-1)}) + require(F(result[0]["endpoint"]) < F(result[1]["endpoint"]), f"{label}: ordered root bracket") + return result + + +def scaled_interval(lo, hi): + lower = (lo.numerator*PRINT_SCALE)//lo.denominator + upper = -((-hi.numerator*PRINT_SCALE)//hi.denominator) + return [str(lower), str(upper)] + + +def floor_grid(x, scale): + return F((x.numerator*scale)//x.denominator, scale) + + +def must_reject(fn, label): + try: + fn() + except AssertionError: + return label + raise AssertionError("failure control unexpectedly passed: " + label) + + +def main(): + ref_path = PKG / "REFERENCE.json" + ref_raw = ref_path.read_bytes() + require(hashlib.sha256(ref_raw).hexdigest() == REFERENCE_SHA256, + "immutable reference snapshot hash") + ref = json.loads(ref_raw) + require(ref["source"]["pr"] == 1407 and + ref["source"]["head"] == "d8640f5b7ae99b43f5d56146cb94ca62b8b3835d", + "external PR head pin") + require(ref["surcharge_model"] == {"complex": False, "bit": True}, + "candidate surcharge convention") + + selected_record = json.loads((ROOT / "certificates/selected-result.json").read_text()) + selected = json.loads((ROOT / "research/community-frontier1094-audit/ASSEMBLY.json").read_text()) + replay = json.loads((ROOT / "research/community-frontier1094-audit/REPLAY.json").read_text()) + require(selected_record["kappa"] == selected["kappa"] == replay["kappa"], + "selected record, assembly and replay agree") + require(replay["complex_profile"] == selected["complex_profile"], + "selected replay profile matches its assembly") + check_path = ROOT / "research/community-batch1099-audit/check_frontier1094.py" + if check_path.exists(): + require("live=14336" in check_path.read_text(), "selected live width provenance") + base = {int(r): int(n) for r, n in selected["complex_profile"].items()} + candidate = {int(r): int(n) for r, n in ref["candidate_profile"].items()} + advertised = {int(r): int(n) for r, n in ref["result"]["profile"].items()} + require(candidate == advertised, "reference profile equals published result profile") + delta = Counter(candidate) + delta.subtract(base) + delta = Counter({r: n for r, n in delta.items() if n}) + require(delta == Counter({1: 1, 7: -7, 16: 3}), "exact advertised profile delta") + require(sum(r*n for r, n in delta.items()) == 0, "rank mass conserved") + require(sum(delta.values()) == -3, "three zero-rank child calls removed") + require(sum(r*n for r, n in candidate.items()) == 1041408, "candidate rank mass") + require(M*W - sum(r*n for r, n in candidate.items()) == 5120, "candidate deficit") + require(ref["result"]["live"] == W and ref["result"]["rank_mass"] == 1041408 and + ref["result"]["deficit"] == 5120, "published capacity receipt") + + base_primary_rows = [x for x in selected["moments"] if x["side"] == "complex"] + candidate_primary_rows = [x for x in ref["complex_moments"]] + base_primary = verify_bracket(base, base_primary_rows, False, "base complex") + candidate_primary = verify_bracket(candidate, candidate_primary_rows, False, "candidate complex") + base_conservative_rows = [x for x in selected["conservative_moments"] + if x["side"] == "conservative_complex"] + candidate_conservative_rows = ref["conservative_complex_moments"] + base_conservative = verify_bracket(base, base_conservative_rows, True, "base conservative complex") + candidate_conservative = verify_bracket(candidate, candidate_conservative_rows, True, + "candidate conservative complex") + + # Both endpoint intervals move strictly upward, including the reserved envelope. + require(F(candidate_primary[0]["endpoint"]) > F(base_primary[1]["endpoint"]), + "candidate primary lower root exceeds base upper root") + require(F(candidate_conservative[0]["endpoint"]) > F(base_conservative[1]["endpoint"]), + "candidate conservative lower root exceeds base upper root") + + result = ref["result"] + require(result["complex_lower"] == candidate_primary[0]["endpoint"], "primary endpoint receipt") + require(result["conservative_complex_lower"] == candidate_conservative[0]["endpoint"], + "conservative endpoint receipt") + bit = F(result["bit_lower"]) + candidate_a = F(result["complex_lower"]) + conservative_a = F(result["conservative_complex_lower"]) + require(result["bit_lower"] == selected["bit_lower"], "candidate retains selected bit endpoint") + require(bit == F(selected["bit_lower"]), "unchanged selected bit supplier value") + require(F(candidate_primary[1]["endpoint"]) < bit, "complex bracket is below unchanged bit endpoint") + require(F(candidate_conservative[1]["endpoint"]) < bit, + "conservative complex bracket is below unchanged bit endpoint") + + k_primary = floor_grid(candidate_a/(1+candidate_a), 10**18) + k_conservative = floor_grid(conservative_a/(1+conservative_a), 10**18) + base_k = F(selected["kappa"]) + require(k_primary == F(result["kappa"]), "primary complex-to-kappa grid") + require(k_conservative == F(result["conservative_kappa"]), "conservative complex-to-kappa grid") + require(F(result["baseline_kappa"]) == base_k, "published baseline kappa") + require(F(result["delta"]) == k_primary-base_k, "published exact kappa delta") + + controls = [] + wrong = Counter(candidate) + wrong[16] += 1 + controls.append(must_reject(lambda: require(wrong == advertised, + "reference profile equality"), + "added rank-16 child")) + wrong_labels = [dict(row) for row in candidate_primary_rows] + for row in wrong_labels: + row["accept"] = not row["accept"] + controls.append(must_reject(lambda: verify_bracket(candidate, wrong_labels, + False, "mutated endpoint labels"), + "swap accepted/rejected endpoint labels")) + controls.append(must_reject(lambda: require(floor_grid(candidate_a/(1+candidate_a), 10**18) + == k_primary+F(1,10**18), "bad kappa grid"), + "one-grid-unit kappa mutation")) + controls.append(must_reject(lambda: require(moment_interval(candidate, + F(candidate_conservative[1]["endpoint"]), False)[0] > 1, + "missing inherited envelope"), "omit conservative surcharge")) + + output = { + "status": "PASS_PR1407_COMPLEX_PROFILE_ARITHMETIC_INDEPENDENT_AUDIT", + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "external_head": ref["source"]["head"], + "external_source_sha256": {x["name"]: x["sha256"] for x in ref["source"]["files"]}, + "profile_delta": dict(sorted(delta.items())), + "rank_mass_delta": 0, + "call_delta": -3, + "base_primary_bracket": base_primary, + "candidate_primary_bracket": candidate_primary, + "base_conservative_bracket": base_conservative, + "candidate_conservative_bracket": candidate_conservative, + "bit_endpoint_unchanged": str(bit), + "primary_kappa_grid": str(k_primary), + "conservative_kappa_grid": str(k_conservative), + "exact_kappa_gain": str(k_primary-base_k), + "interval_method": f"standard-library Fraction; {LOG_TERMS}-term binary-reduced atanh logarithm bounds and {EXP_TERMS}-term positive Taylor exponential with geometric tail", + "failure_controls": controls, + "construction_scope": "Arithmetic only; no owner/window/path, native compiler, controller, all-47-outer-constraint or full ancestry replay." + } + print(json.dumps(output, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()