From bf87e110106c997392645f76b429ab3cc4410419 Mon Sep 17 00:00:00 2001 From: davidNbreslauer Date: Tue, 13 Oct 2026 07:42:16 -0700 Subject: [PATCH] Add independent T21 binomial moment audit --- research/t21-binomial-audit/CERTIFICATE.json | 80 ++++ research/t21-binomial-audit/CLAIM.json | 85 +++++ research/t21-binomial-audit/README.md | 169 +++++++++ research/t21-binomial-audit/SOURCES.json | 25 ++ research/t21-binomial-audit/VALIDATION.json | 64 ++++ .../t21-binomial-audit/inputs/ASSEMBLY.json | 344 ++++++++++++++++++ research/t21-binomial-audit/inputs/CLAIM.json | 30 ++ research/t21-binomial-audit/inputs/PROOF.md | 123 +++++++ .../inputs/selected-result.json | 170 +++++++++ research/t21-binomial-audit/test_package.py | 104 ++++++ research/t21-binomial-audit/verify.py | 252 +++++++++++++ 11 files changed, 1446 insertions(+) create mode 100644 research/t21-binomial-audit/CERTIFICATE.json create mode 100644 research/t21-binomial-audit/CLAIM.json create mode 100644 research/t21-binomial-audit/README.md create mode 100644 research/t21-binomial-audit/SOURCES.json create mode 100644 research/t21-binomial-audit/VALIDATION.json create mode 100644 research/t21-binomial-audit/inputs/ASSEMBLY.json create mode 100644 research/t21-binomial-audit/inputs/CLAIM.json create mode 100644 research/t21-binomial-audit/inputs/PROOF.md create mode 100644 research/t21-binomial-audit/inputs/selected-result.json create mode 100644 research/t21-binomial-audit/test_package.py create mode 100644 research/t21-binomial-audit/verify.py diff --git a/research/t21-binomial-audit/CERTIFICATE.json b/research/t21-binomial-audit/CERTIFICATE.json new file mode 100644 index 0000000000..a512f2fef7 --- /dev/null +++ b/research/t21-binomial-audit/CERTIFICATE.json @@ -0,0 +1,80 @@ +{ + "arity": 73, + "assignment_seed": 69, + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "child_count": 681782, + "conservative": { + "endpoint": "1664724473541313810689/1000000000000000000000000", + "lower_residual_interval": [ + "-526825226012241273767532986651546614167917669673029893633726326727871/189600358521368422407583654804722585933447296973722670396029561460711028162560000000000000000", + "-526825226012241273767532986545324448164731068686253653307311743456799/189600358521368422407583654804722585933447296973722670396029561460711028162560000000000000000" + ], + "successor": "166472447354131381069/100000000000000000000000", + "successor_residual_interval": [ + "1002513433561922366026390346187232403779166744600723795266956622711/5925011203792763200236989212647580810420228030428833449875923795647219630080000000000000000", + "64160859747963031425688982368427205848239873600863346517914131234241/379200717042736844815167309609445171866894593947445340792059122921422056325120000000000000000" + ], + "terms": { + "1": 7743, + "2": 3845, + "3": 2546, + "4": 1896, + "48": 101, + "5": 1506, + "8": 921, + "fallback": 7743 + } + }, + "controls": { + "algebraic_comparisons": 450, + "mathematical_controls": 5, + "redistributed_minus_original_interval": [ + "-30611254125507706510269204255614715512780285837491562546149107708127/1213442294536757903408535390750224549974062700631825090534589193348550580240384", + "-61222508251015413020538408511229431025557852350359115694150584663389/2426884589073515806817070781500449099948125401263650181069178386697101160480768" + ], + "rejected_inputs": 11 + }, + "deficit": 6720, + "live_stock": 18816, + "native": { + "endpoint": "1664724476433282815289/1000000000000000000000000", + "lower_residual_interval": [ + "-261428779639035688672010186268399165805829457776969323/808961529691171935605690260500149699982708467087883393689726128899033720160256", + "-32678597454879461084001273226898073758113208166698527/101120191211396491950711282562518712497838558385985424211215766112379215020032" + ], + "successor": "166472447643328281529/100000000000000000000000", + "successor_residual_interval": [ + "2123235352137840560200160598288155896009491039226008749/808961529691171935605690260500149699982708467087883393689726128899033720160256", + "530808838034460140050040149685342617937603707919107627/202240382422792983901422565125037424995677116771970848422431532224758430040064" + ], + "terms": { + "1": 7743, + "2": 3845, + "3": 2546, + "4": 1896, + "48": 101, + "5": 1506, + "8": 921 + } + }, + "physical_stock": 19330, + "profile": { + "1": 481575, + "2": 63882, + "3": 84295, + "4": 30618, + "48": 6292, + "5": 13608, + "8": 1512 + }, + "rank_mass": 1366848, + "scope": "Arithmetic consequence of the pinned T21 paid profile and fallback formula. Physical construction, owner windows, invoice, outer 47 inequalities, all-size compilation and the multiplication theorem are not replayed or proved.", + "selected_kappa_unchanged": "1661957774647029/1000000000000000000", + "source_files_sha256": { + "inputs/ASSEMBLY.json": "190110b509dc87d38b72ad37c3290efcc245ce26df4cae3d7e2d6dcf0bac2c43", + "inputs/CLAIM.json": "433d7bc4a371aaffeee35c12a1db6ea974722a85b799233626e1a57dcfdcb121", + "inputs/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def", + "inputs/selected-result.json": "41fb066ff0f43ce472323195e9088d6d888715c13c54eae7b42e357ed5bfc726" + }, + "status": "PASS_T21_BINOMIAL_MOMENT" +} diff --git a/research/t21-binomial-audit/CLAIM.json b/research/t21-binomial-audit/CLAIM.json new file mode 100644 index 0000000000..ab692c8cb9 --- /dev/null +++ b/research/t21-binomial-audit/CLAIM.json @@ -0,0 +1,85 @@ +{ + "status": "Completed independent arithmetic audit; prepared for public submission", + "date": "2026-10-13", + "assignment_seed": 69, + "seed_origin": "Retained OS-random assignment from the preliminary setup session; not rerolled", + "track": "Adversarial mathematical audit", + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "candidates": [ + "T21 native and conservative moment accounting", + "T21 partial-bank coordinate complement", + "Retained outer assembly arithmetic" + ], + "selected_scope": "Numerical consequence of the PR890 T21 paid profile and inherited fallback formula, using a separate positive-binomial-series implementation", + "method_prior_art": "PR678 introduced the same enclosure method for the historical PR543 bit moment. No new numerical method is claimed.", + "hypothesis": "Both recorded complex lower endpoints are strictly accepted and their adjacent 10^-24 successors are strictly rejected.", + "result": "Confirmed for both models by exact rational enclosures. No counterexample to this numerical claim and no new kappa.", + "coordination": "The two open issues inspected did not identify a sprint claim thread. The scope and result were recorded locally.", + "stopping_rule": "One completed audit with proof, source bindings, certificate and adverse controls; no search for a stronger construction.", + "overlap_checked_at": "2026-10-13T14:41:40.728825+00:00", + "overlap_scope": "Initial complete focused search responses for T21 (3), binomial (9), and moment PRs updated on October 13 (73). Submission refresh returned four T21 PRs and identified PR957; its source at the recorded head was inspected. This is not an exhaustive duplicate audit of all open PR contents.", + "overlap_heads": [ + { + "number": 678, + "title": "Independent verification of the #543 bit moment using binomial enclosures", + "state": "open", + "merged_at": null, + "head_sha": "bdc9317efd6d928a0f050159670d1316ba5f4c5b", + "author": "0x-chad", + "updated_at": "2026-10-13T03:47:52Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/678" + }, + { + "number": 706, + "title": "Independent verification: selected complex moments via integer root bounds", + "state": "open", + "merged_at": null, + "head_sha": "0f7dbb54948775c010b5e5bc8ab3cf92a52a9b25", + "author": "arkfx", + "updated_at": "2026-10-13T04:34:41Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/706" + }, + { + "number": 813, + "title": "Independent verification: Bernstein certificates for all 47 outer inequalities", + "state": "closed", + "merged_at": "2026-10-13T14:10:26Z", + "head_sha": "5d3b961fca28c77cec74f5237a59acd361c8e851", + "author": "bitplane", + "updated_at": "2026-10-13T14:10:26Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/813" + }, + { + "number": 942, + "title": "Conditional \u03ba = 0.001661960547713947: T37 whole-owner packing and all-T bound", + "state": "open", + "merged_at": null, + "head_sha": "1960cfa919a0945d0ca4cb14ea96237000037903", + "author": "jon314159", + "updated_at": "2026-10-13T13:52:33Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/942" + }, + { + "number": 947, + "title": "Scoped negative result: exact constant-row center shear optimum (no new kappa)", + "state": "open", + "merged_at": null, + "head_sha": "b6f6418bdcae748b267cea72a5949d551feb7bb2", + "author": "RossRichardson", + "updated_at": "2026-10-13T14:16:22Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/947" + }, + { + "number": 957, + "title": "Adversarial audit: frontier890 endpoint certification, reduction and surcharge stakes (no new kappa)", + "state": "open", + "head_sha": "65c931415587c444a7a1f48939842c4cf0aa0411", + "author": "navinor", + "updated_at": "2026-10-13T14:38:32Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/957" + } + ], + "overlap_conclusion": "PR957 concurrently audits PR890 endpoints, reduction and surcharge attribution by transcribing the two retained log/exp engines plus a direct Decimal calculation. This package corroborates its complex endpoint conclusions with a different exact binomial enclosure method, without claiming priority. No other T21 binomial audit was identified. PR678 and PR706 concern historical profiles; PR813 concerns outer inequalities; PR942 and PR947 are distinct constructions or research.", + "assistance": "Prepared for David Breslauer with substantial OpenAI Codex assistance. Final continuation reviewed with GPT-6 Astra at Max effort; no independent human review.", + "license": "Apache-2.0" +} diff --git a/research/t21-binomial-audit/README.md b/research/t21-binomial-audit/README.md new file mode 100644 index 0000000000..cb1f0e3462 --- /dev/null +++ b/research/t21-binomial-audit/README.md @@ -0,0 +1,169 @@ +# Independent arithmetic audit of the selected T21 recurrence + +**Status: independent finite verification; no new kappa.** + +This confirms both the native and conservative complex moment brackets used +by the PR890 construction selected at the pinned base. Each lower endpoint is strictly below +the recurrence threshold, and its adjacent `10^-24` successor is strictly +above it. The implementation uses only positive generalized-binomial terms, +integer outward rounding and a geometric tail. It imports no production +logarithm, exponential, supplier or owner implementation. + +The exact contribution base is `007664306fff84fbb1c9a1b4053b69f439764034`. The selected +conditional kappa remains `1661957774647029/10^18`. This is an arithmetic +audit of its paid profile, not a fresh physical replay or a proof of the +complete multiplication theorem. The preliminary package used +`47481c89fd30a43f8f882eb4b391e89c29273fd0`; its assembly and selected-record +inputs are byte-identical at the contribution base. + +## Reproduce + +Python 3.11+ and the standard library suffice. From the repository root: + +```sh +python3 -I -B research/t21-binomial-audit/verify.py +python3 -I -O -B research/t21-binomial-audit/test_package.py +``` + +Expected first marker: + +```text +PASS_T21_BINOMIAL_MOMENT four strict endpoint decisions; 450 algebraic comparisons; 5 mathematical controls; 11 rejected inputs. +``` + +The second command prints `PASS_T21_BINOMIAL_PACKAGE controls=10`, followed +by successful relocation, regeneration and failed-run output-preservation markers. +`--write-certificate` regenerates the exact certificate; the default recomputes +it and requires an identical result. No network or third-party library is used. +The package also runs from an unrelated current directory after relocation. + +In the pinned repository, add `--repository .` to the first command to compare +all eight source files with the checkout. This checks source bytes without +importing or executing the production arithmetic. It does not require the +current Git head to equal the base if those source bytes are unchanged. +An explicit check against a later, changed selection is expected to fail; +the default command continues to audit the frozen inputs. + +## Exact arithmetic argument + +For a child rank r, ambient arity m, and rational saving a in `[0,1]`, put +`x = 1-r/m`. The positive binomial expansion is + +`(m/r)^a = sum_(k>=0) t_k`, with +`t_0=1` and `t_(k+1)=t_k*(a+k)*x/(k+1)`. + +For `0 <= a <= 1`, `(a+k)/(k+1) <= 1`, so every ratio is at most x. +Consequently the tail after term k is bounded +above by `t_(k+1)/(1-x)`. The checker stores lower and upper term values as +integers over `2^240`, rounding every recurrence product outward. Positivity +allows summing those bounds directly; the rounded-up geometric tail is added +only to the upper sum. The stopping rule bounds that tail by `2^-170` per +power factor. Each returned interval is rational and explicitly encloses +the infinite series. Zero saving and a full-rank power factor are exact +special cases. + +Dividing the inherited recurrence sum `sum_r c_r*r^(1-a)` by +`18816*73^(1-a)` gives the native normalized moment + +`M(a) = sum_r c_r * r/(73*18816) * (73/r)^a`. + +The conservative variant charges `32*73^2/10^16` additional rank-one +calls per paid child. Applying the same normalization gives the fallback + +`32*73*sum_r(c_r)/(10^16*18816) * 73^a`. + +The factor `73/r` is greater than one for every paid rank, and every weight +is positive. The moment is therefore continuous and strictly increasing in a, +so the two strict endpoint decisions bracket its unique root on the relevant +grid. This numerical statement takes the recurrence/fallback contract as an +input; it does not justify its construction-level realization. + +## Profile and checked obligations + +The proof's single-call profile `{1:2548,2:338,3:446,4:162,5:72,8:8}` is +multiplied by 189. Adding idle children `{48:6292,3:1,1:3}` reconstructs the +committed assembly profile exactly. There are 681782 children. The 21 replicas +use `9*21=189` local calls, live stock `8*112*21=18816`, and physical stock +`18816+504+8+2=19330`. These values are checked against the pinned construction +claim. Its rank mass is 1366848 and its deficit +is `73*18816-1366848=6720=21*320`. + +| Price | Accepted lower endpoint | +| --- | --- | +| Native | `1664724476433282815289/10^24` | +| Conservative | `1664724473541313810689/10^24` | + +Both successors at `+10^-24` are rejected. `CERTIFICATE.json` supplies the +exact residual intervals and term counts. `SOURCES.json` pins the assembly, +selected record, construction claim and proof. The assembly and proof hashes +are also checked against the selected record. Four additional source references +identify the pricing entrypoint and formula; both arithmetic-engine hashes +must match the assembly's recorded inputs. These source files are not imported. + +The 450 algebraic checks use exact integer-power inequalities to verify the +enclosures at rational exponents with denominators at most three. They cover +every rank through arities 2, 3, 5, 7 and the actual arity 73, including the +slowest-decaying series at rank one. The five +model controls cover the zero-saving mass identity, an omitted rank-48 +child, a dropped conservative surcharge, physical versus live-stock +normalization, and a redistribution preserving both call count and rank +mass. In the last case two rank-48 children become rank-47 and rank-49 +children. The moment strictly decreases, as expected from concavity, despite +the unchanged totals. These are deliberately altered models; no defect in +the selected production checker is alleged. + +Package controls use actual disposable copies. Corrupting any of the four +pinned inputs or the recorded certificate rejects. Deleting the geometric +tail or upper rounding fails the exact algebraic comparisons; undercharging +the fallback fails the strict endpoint test. These three implementation +mutations run with `--write-certificate`, so they cannot pass merely by +rejecting an old receipt. Every rejection is checked for its specific error, +and failed runs must preserve the existing certificate. Two synthetic +repository-fixture controls reject changed and missing reference files. +All ten controls run under `-O`; a relocated positive and exact certificate +regeneration also pass. + +## Provenance, overlap and limits + +OS-random assignment seed **69** selects the mathematical-audit track. +Candidate tasks considered: the complex moment accounting, the partial-bank +complement, and the outer assembly arithmetic. The first was selected for a +small, independent calculation with exact source binding. The scope and result +were recorded locally; no sprint coordination issue was identified. + +[#678](https://github.com/CrocSwap/integer-mult-bounds/pull/678) by **0x-chad** +previously introduced binomial enclosures for the historical PR543 bit moment. +[#706](https://github.com/CrocSwap/integer-mult-bounds/pull/706) by **arkfx** +checks historical PR626 complex moments using integer roots, and +[#813](https://github.com/CrocSwap/integer-mult-bounds/pull/813) by +**Gareth Davidson / bitplane** independently checks the outer inequalities. +This contribution does not claim a new enclosure technique. It supplies a +separate implementation and exact native/conservative evidence for the +PR890 complex profile. The October 13, 2026 submission refresh identified +**navinor**'s concurrent +[#957](https://github.com/CrocSwap/integer-mult-bounds/pull/957), pinned at +`65c931415587c444a7a1f48939842c4cf0aa0411`. It transcribes the two retained +logarithm/exponential engines, adds a direct Decimal evaluation, and audits +endpoint-to-kappa reduction and surcharge attribution. This package corroborates +its complex endpoint conclusions using a different exact enclosure method; +it does not claim priority for the T21 endpoint audit. The focused search found +no other T21 binomial audit. PR942's pending T37 extension and PR947's +constant-row center-shear bound are distinct. PR813 has been incorporated for +its historical checkpoint. Search results are an overlap check, not an +exhaustive certification of all open work. + +Construction credit belongs to **Chafik Boukhalfa** (PR890), **Jeremy Kothe** +(PR869/870), **Hao Yan** (PR858), **DreamingOfClouds**, **eumemic**, +**Rohan Arun**, **icekylinx**, and the repository's cumulative lineage. +Prepared for **David Breslauer** with substantial **OpenAI Codex** assistance, +under Apache-2.0. There is no independent human-review claim. + +The preliminary subset was checked against a complete source checkout with +shallow Git history. `make selected-record-check` passes; this binds the +selection, its original source inventory and proof supplements. The separate +arithmetic audit and its controls also pass. See `VALIDATION.json` for the +recorded environment, commands and scope. No full `make verify`, supplier cold replay, +physical tape/owner audit, bit-supplier replay, 47-inequality outer replay, +Lean run or hosted CI success is claimed. All-size compilation, common-label +and mutable-source realization, whole-call hosting, precision/tape and +analytic-transfer obligations remain inherited. diff --git a/research/t21-binomial-audit/SOURCES.json b/research/t21-binomial-audit/SOURCES.json new file mode 100644 index 0000000000..ff55fbdad5 --- /dev/null +++ b/research/t21-binomial-audit/SOURCES.json @@ -0,0 +1,25 @@ +{ + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "source_repository": "CrocSwap/integer-mult-bounds", + "files": { + "inputs/ASSEMBLY.json": "190110b509dc87d38b72ad37c3290efcc245ce26df4cae3d7e2d6dcf0bac2c43", + "inputs/selected-result.json": "41fb066ff0f43ce472323195e9088d6d888715c13c54eae7b42e357ed5bfc726", + "inputs/CLAIM.json": "433d7bc4a371aaffeee35c12a1db6ea974722a85b799233626e1a57dcfdcb121", + "inputs/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def" + }, + "provenance": { + "inputs/ASSEMBLY.json": "research/community-frontier890-audit/ASSEMBLY.json", + "inputs/selected-result.json": "certificates/selected-result.json", + "inputs/CLAIM.json": "research/complex-t21-owners/data/CLAIM.json", + "inputs/PROOF.md": "research/complex-t21-owners/PROOF.md" + }, + "method_predecessor": "PR678 by 0x-chad: binomial arithmetic for the historical PR543 bit profile; this is a separate implementation auditing the current PR890 complex native and conservative profile.", + "preliminary_base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "references": { + "research/complex-t21-owners/price.py": "b4510dd0d86322be627ff500e76a22f53cafa8405a699d04646dc3039167d569", + "research/complex-t21-owners/vendor/pr870/independent/price_profile_t16.py": "53f8e62dcf27bee032c1bee0245d126a9c8a12ebcf24f6aaff65ea3122fffe29", + "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + "reference_scope": "Read to identify the inherited normalized moment and fallback formula; never imported or executed by this package. --repository checks their bytes." +} diff --git a/research/t21-binomial-audit/VALIDATION.json b/research/t21-binomial-audit/VALIDATION.json new file mode 100644 index 0000000000..799e57e925 --- /dev/null +++ b/research/t21-binomial-audit/VALIDATION.json @@ -0,0 +1,64 @@ +{ + "status": "PASS_SCOPED_LOCAL_VALIDATION", + "verified_at": "2026-10-13T14:36:45.020100+00:00", + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "branch": "research/t21-binomial-audit", + "checkout": "Complete source checkout with shallow Git history", + "environment": { + "python": "3.14.5", + "implementation": "CPython", + "system": "Darwin", + "release": "25.6.0", + "machine": "arm64" + }, + "checks": [ + { + "command": "python3 -I -B research/t21-binomial-audit/verify.py --repository .", + "returncode": 0, + "elapsed_seconds": 0.404, + "stdout": "PASS_T21_REPOSITORY_BINDINGS files=8\nPASS_T21_BINOMIAL_MOMENT four strict endpoint decisions; 450 algebraic comparisons; 5 mathematical controls; 11 rejected inputs.\n", + "stderr": "" + }, + { + "command": "python3 -I -O -B research/t21-binomial-audit/test_package.py", + "returncode": 0, + "elapsed_seconds": 3.459, + "stdout": "PASS_T21_BINOMIAL_PACKAGE controls=10 relocated_optimized=PASS regeneration=PASS failure_preserves_certificate=PASS\n", + "stderr": "" + }, + { + "command": "make selected-record-check", + "returncode": 0, + "stdout": "python3 -B scripts/verify_selected_result.py\nPASS selected record, exact kappa, original source inventory and proof supplement: 1661957774647029/1000000000000000000\n", + "evidence": "Passed earlier in this continuation, before final standalone-audit edits. No tracked pre-existing repository files have changed since that check." + } + ], + "source_files_sha256": { + "CERTIFICATE.json": "ad122270a276f772f17d39b27f122a845a6e93c7a645f1fd32e10eccca372075", + "CLAIM.json": "6f080af561955b7c425a02036cb4b991bc9dffe42045cf3228c169eb9c211172", + "README.md": "2bd2ceaff95288933a7f36358fbbebf7d9e328264edc0f189a590b70bcabe92f", + "SOURCES.json": "28ea8e30ea59924639f0b8e92d51417eb145400de45e8d7e976673b4724f06fb", + "inputs/ASSEMBLY.json": "190110b509dc87d38b72ad37c3290efcc245ce26df4cae3d7e2d6dcf0bac2c43", + "inputs/CLAIM.json": "433d7bc4a371aaffeee35c12a1db6ea974722a85b799233626e1a57dcfdcb121", + "inputs/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def", + "inputs/selected-result.json": "41fb066ff0f43ce472323195e9088d6d888715c13c54eae7b42e357ed5bfc726", + "test_package.py": "5840d30eabbdf4322d462a0af8a73b5899d183810606f65940c81978548c8030", + "verify.py": "080fa1343c62ecd3cbdaacca322028e590bc0c18d0c0e3878ba081587ef7b34a" + }, + "not_run": [ + "full make verify", + "selected supplier cold replay", + "physical owner/tape admission", + "bit supplier replay", + "all 47 outer inequalities", + "Lean", + "hosted CI", + "independent human review" + ], + "publication": "This verification receipt was prepared before public submission; publication status is recorded separately.", + "scope": "Exact arithmetic audit of pinned PR890 T21 profile and inherited fallback formula. Selected kappa unchanged; all construction and all-size assumptions remain inherited.", + "publication_preparation": { + "updated_at": "2026-10-13T14:41:40.728825+00:00", + "changes": "Documentation and local scope record updated to credit concurrent PR957; source-file hashes for those two documents refreshed. Mathematical code, pinned inputs and certificate unchanged." + } +} diff --git a/research/t21-binomial-audit/inputs/ASSEMBLY.json b/research/t21-binomial-audit/inputs/ASSEMBLY.json new file mode 100644 index 0000000000..e78b030732 --- /dev/null +++ b/research/t21-binomial-audit/inputs/ASSEMBLY.json @@ -0,0 +1,344 @@ +{ + "status": "PASS_GAUGE44_NATIVE_EXACT_GLOBAL_ASSEMBLY", + "kappa": "1661957774647029/1000000000000000000", + "kappa_decimal": "0.001661957774647029", + "complex_lower": "1664724476433282815289/1000000000000000000000000", + "complex_decimal": "0.001664724476433282815289", + "bit_lower": "1733427039589844234749/1000000000000000000000000", + "bit_decimal": "0.001733427039589844234749", + "binding": "complex", + "gain_over_pr635_percent": "1.571667326972541941863966018065760058471413072548499771819389461580810", + "complex_profile": { + "1": 481575, + "2": 63882, + "3": 84295, + "4": 30618, + "5": 13608, + "8": 1512, + "48": 6292 + }, + "provider_counts": { + "gauge44": 189 + }, + "surcharge_model": { + "complex": false, + "bit": true + }, + "conservative_complex_lower": "1664724473541313810689/1000000000000000000000000", + "conservative_complex_decimal": "0.001664724473541313810689", + "conservative_kappa": "207744721470583/125000000000000000", + "conservative_kappa_decimal": "0.001661957771764664", + "conservative_moments": [ + { + "side": "conservative_complex", + "surcharge": true, + "endpoint": "1664724473541313810689/1000000000000000000000000", + "accept": true, + "mercator": [ + "-74911145247643999993244809455966449308556595/26959946667150639794667015087019630673637144422540572481103610249216", + "-74911145247643999993244809455966449308556593/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two": [ + "-27786094502229532823821/10000000000000000000000000000000000000000000000", + "-13893042251114766411839/5000000000000000000000000000000000000000000000" + ] + }, + { + "side": "conservative_complex", + "surcharge": true, + "endpoint": "166472447354131381069/100000000000000000000000", + "accept": false, + "mercator": [ + "4454716771224717353694205645725701893089/26328072917139296674479506920917608079723773850137277813577744384", + "2280814986867055285091433290611559369261569/13479973333575319897333507543509815336818572211270286240551805124608" + ], + "base_two": [ + "845997749068113830803/5000000000000000000000000000000000000000000000", + "1692005498136227661749/10000000000000000000000000000000000000000000000" + ] + } + ], + "conservative_bootstrap": [ + { + "exponent": "1662017191105286357838278306690768868073019487843785479016773171277394875244774563353469345279/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "2707282436027452850719028584757590613169823156214520983226828722605124755225436646530654721/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "4911739996835" + }, + { + "exponent": "1664719966661985767241964832280843146940777092552512664894030159656318066520377373166953026731757310813090175242659846656159144871278618112769/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "4506879328043447032502994683311745412218447487335105969840343681933479622626833046973268242689186909824757340153343840855128721381887231/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "1772354698204234947" + }, + { + "exponent": "1664724466038601493997639829609898757460561875911227750762504718303158803650404177764850217051771155701362306140196771875255294827980671796653420283768709574017118331575932745794035080412159/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "7502712316691357505665627701225627435088772249237495281696841196349595822235149782948228844298637693859803228124744705172019328203346579716231290425982881668424067254205964919587841/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "639537348937705590945353" + }, + { + "exponent": "1664724473528823861877461384253601177978049102302940425957426599745068416704999137688314070797510330408784027540203359935428370385570432912720442781472804151509442534139663985727733299260019939381929988025560681970848719429140670980232449/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "12489948811535951021925280708140208697059574042573400254931583295000862311685929202489669591215972459796640064571629614429567087279557218527195848490557465860336014272266700739980060618070011974439318029151280570859329019767551/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "230770974399582120753950391985" + }, + { + "exponent": "1664724473541293018365537493131354447272768547458155223285097190870258576318267671908645177120522575321320913091515085938847226993974673140577783158016423875092565396234957446107658052574713967023353522875675575510527618135982700486202353786589121223967726400970764600031639040799152639/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "20792323459842144172011413420763541844776714902809129741423681732328091354822879477424678679086908484914061152773006025326859422216841983576124907434603765042553892341947425286032976646477124324424489472381864017299513797646213410878776032273599029235399968360959200847361/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "83271512936330378803053262199104855" + }, + { + "exponent": "1664724473541313776075507609889104493619079235795439876612262767332134578532485597869746737548734117113261727752857558593844438461146037299680614377161910401038037160019335011112931846602733740757993374691898472487031879587798035603832357284661613704252667193795288425310275846609625128242202162618698359913414026052631694100739241729/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "34613489725386421965067110075204560123387737232667865421467514402130253262451265882886738272247142441406155561538853962700319385622838089598961962839980664988887068153397266259242006625308101527512968120412201964396167642715338386295747332806204711574689724153390374871757797837381301640086585973947368305899260758271/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "30047734056445505696549919178219878412889" + }, + { + "exponent": "1664724473541313810631375411815004872634543961788865875194974945061655003030374955971932692337055311745493176745271578767639424486125196721375075334186022755569824877774011956941672497922069671951731066915946037242330157206184934144019798747962676899663195996542600081780653056978117105644443426647331128775927334665869646855627226067427425360137397459020109362581946190754684958719/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "57621923460521586051645349211134124805025054938344996969625044028067307662944688254506823254728421232360575513874803278624924665813977244430175122225988043058327502077930328048268933084053962757669842793815065855980201252037323100336804003457399918219346943021882894355556573352668871224072665334130353144372773932572574639862602540979890637418053809245315041281/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "10842439269924266725931907792709943469648067775" + } + ], + "conservative_outer": { + "bit_positive": "1664724473541313810631375411815004872634543961788865875194974945061655003030374955971932692337055311745493176745271578767639424486125196721375075334186022755569824877774011956941672497922069671951731066915946037242330157206184934144019798747962676899663195996542600081780653056978117105644443426647331128775927334665869646855627226067427425360137397459020109362581946190754684958719/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "complex_above_bit": "57624588184995127365456038211134124805025054938344996969625044028067307662944688254506823254728421232360575513874803278624924665813977244430175122225988043058327502077930328048268933084053962757669842793815065855980201252037323100336804003457399918219346943021882894355556573352668871224072665334130353144372773932572574639862602540979890637418053809245315041281/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "complex_below_one_over32": "29585275526458686189311/1000000000000000000000000", + "beta_positive": "1/1000000000000000000000000", + "beta_below_one": "999999999999999999999999/1000000000000000000000000", + "leaf_saving_above_bit": "57622923460521586051645349211134124805025054938344996969625044028067307662944688254506823254728421232360575513874803278624924665813977244430175122225988043058327502077930328048268933084053962757669842793815065855980201252037323100336804003457399918219346943021882894355556573352668871224072665334130353144372773932572574639862602540979890637418053809245315041281/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "q_positive": "832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "q_below_internal": "1664724473541313810631375411815004872634543961788865875194974945061655003030374955971932692337055311745493176745271578767639424486125196721375075334186022755569824877774011956941672497922069671951731066915946037242330157206184934144019798747962676899663195996542600081780653056978117105644443426647331128775927334665869646855627226067427425360137397459020109362581946190754684958719/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "q_below_leaf": "28813126454734334339633305980978877407385162013134287350687716988978715486475374502209383560056547671492033250114146910891229972331474747411808936188328207551919320863842938036091408214524903448506873127974448874027342956175867735102546021527447921786573134706937989777860067329391413729141977110491823903315162893620953189578156897716012746134387042020116540749862581946190754684958719/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "c_positive": "832362236770656905315811041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "c_below_one": "499167637763229343094684188958816971104996538650480978877407385162013134287350687716988978715486475374502209383560056547671492033250114146910891229972331474747411808936188328207551919320863842938036091408214524903448506873127974448874027342956175867735102546021527447921786573134706937989777860067329391413729141977110491823903315162893620953189578156897716012746134387042020116540749862581946190754684958719/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "q_below_reservations": "1/4000000000000000000000000", + "lambda_above_tau": "1664724473541313810631375411815004872634543961788865875194974945061655003030374955971932692337055311745493176745271578767639424486125196721375075334186022755569824877774011956941672497922069671951731066915946037242330157206184934144019798747962676899663195996542600081780653056978117105644443426647331128775927334665869646855627226067427425360137397459020109362581946190754684958719/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "lambda_above_sigma": "57626252909468668679266669586545939809897689482306785835500239003012369317947718629462795187420758287672321007051548550203692305238463369626896497301322229081083071902808102060225874756551884827341794524881981802017443582194529285270948023256147880896246606217879436955638354005725849341178309777557000475501549859907240509509458168205958064843413946642774061390362581946190754684958719/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "lambda_above_internal": "1664724473541313810631375411815004872634543961788865875194974945061655003030374955971932692337055311745493176745271578767639424486125196721375075334186022755569824877774011956941672497922069671951731066915946037242330157206184934144019798747962676899663195996542600081780653056978117105644443426647331128775927334665869646855627226067427425360137397459020109362581946190754684958719/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "lambda_prime_above_lambda": "1664724473541313810631375411815004872634543961788865875194974945061655003030374955971932692337055311745493176745271578767639424486125196721375075334186022755569824877774011956941672497922069671951731066915946037242330157206184934144019798747962676899663195996542600081780653056978117105644443426647331128775927334665869646855627226067427425360137397459020109362581946190754684958719/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "compact_leaf": "28813126454734334339633305980978877407385162013134287350687716988978715486475374502209383560056547671492033250114146910891229972331474747411808936188328207551919320863842938036091408214524903448506873127974448874027342956175867735102546021527447921786573134706937989777860067329391413729141977110491823903315162893620953189578156897716012746134387042020116540749862581946190754684958719/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "compact_reservations": "1/4000000000000000000000000", + "lambda_prime_below_one": "832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "epsilon_positive": "499999999999999999999999500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000/500832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281", + "epsilon_below_one": "832362236770656905316186041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281/500832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281", + "guard_width": "832362236770656905316186041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281/500832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281", + "K_geometry": "375832362236770656905315811041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281/500832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281000000000000000000000000", + "K_dominates_log": "832362236770656905315810208820792124346556033707979939563719834525516193628189690396183297647811976185507605418658938803882468959269413145656441519701775366735101955041644123922828090945093250292116143704795960394431162963433765650876105550697260239346328005815508254081161967839083537670061719243743293208847800749575505488098566248356157302245746417446880874818802536136781175262883552440851265431582030862581946190754684958719/500832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281000000000000000000000000", + "record_suffix": "832362236770656905316186041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281/500832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281", + "phase_local": "6658897894165255242528987497101994389370785480466127797712023700433576182173375671473332289242484354670041920498263105103438236208470384769417831713381452134852439401723346671059392844898192684039476286203121636254883051067612623532684704857466186093628505855123372801575150024890517609225041247938003397104853960976132738164892425993009484975198648133434791651878093241995965390013845478817515982636870997862581946190754684958719/4006658897894165255242525488329464231160027690796152168980740918703894925701194498264088170276108197003982324931519547618628063733999086824712870160221348202020705528510493374339584645433089256495711268734283800772411945014976204409007781256350593058119179631827780416625707414922344496081777119461364868690166864183116065408773478696851032374483374744818271898030924903663839067674001099344430473962520330248000000000000000000000000", + "phase_boundary": "1331779578833051048505396833530609461348632843544392613119288737317635621217777060202796068355926751484181975282625010200987249009200924999121703536302890518288016593328647199391676498426787487470461298776081018325327039086649096326459699776991739598284800392899039501009218087014920743803345678846108444971362614483280411146109468512183585388498852278817273227138170310924711250812966003273136812620606799462581946190754684958719/801331779578833051048505097665892846232005538159230433796148183740778985140238899652817634055221639400796464986303909523725612746799817364942574032044269640404141105702098674867916929086617851299142253746856760154482389002995240881801556251270118611623835926365556083325141482984468899216355423892272973738033372836623213081754695739370206474896674948963654379606184980732767813534800219868886094792504066049600000000000000000000000", + "gamma_sublinear": "1/2000000000000000000000000", + "cell_above_band": "999999999999999999999998499167637763229343094684313958816971104996538650480978877407385162013134287350687716988978715486475374502209383560056547671492033250114146910891229972331474747411808936188328207551919320863842938036091408214524903448506873127974448874027342956175867735102546021527447921786573134706937989777860067329391413729141977110491823903315162893620953189578156897716012746134387042020116540749862581946190754684958719/2003329448947082627621262744164732115580013845398076084490370459351947462850597249132044085138054098501991162465759773809314031866999543412356435080110674101010352764255246687169792322716544628247855634367141900386205972507488102204503890628175296529059589815913890208312853707461172248040888559730682434345083432091558032704386739348425516187241687372409135949015462451831919533837000549672215236981260165124000000000000000000000000", + "prime_interval_packing": "832362236770656905316186041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281/500832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281", + "alpha_positive": "1664724473541313810631871250003821019350017383352001062156334672512381906277501973407204582161336601683298221858602391132390435709155266234765211547370300619323293018853315916370908770081250312256024735490271056945924289835459316776848762594521392504243781984288060332294588833132145547892201651914351879479705823639083681584783403354735204112667589519730868128684415494116664634513020970494660510746623311862581946190754684958719/1001664724473541313810631372082366057790006922699038042245185229675973731425298624566022042569027049250995581232879886904657015933499771706178217540055337050505176382127623343584896161358272314123927817183570950193102986253744051102251945314087648264529794907956945104156426853730586124020444279865341217172541716045779016352193369674212758093620843686204567974507731225915959766918500274836107618490630082562000000000000000000000000", + "alpha_below_one": "999999999999999999999999500832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281/1001664724473541313810631372082366057790006922699038042245185229675973731425298624566022042569027049250995581232879886904657015933499771706178217540055337050505176382127623343584896161358272314123927817183570950193102986253744051102251945314087648264529794907956945104156426853730586124020444279865341217172541716045779016352193369674212758093620843686204567974507731225915959766918500274836107618490630082562000000000000000000000000", + "alpha_below_one_fourth": "248751456644844014642025971770587693428151713291407509499139972746481050950047154168098306060095425711065597086361369335031863547665787660309789173466463962006970802513052519979853131569486828218725929560402466491329822273600553458786137565927390673628204945004948215706812124599514385457218868314420952413655723187805670406463559015198454319292543332031411125498248390984873277095112047738532244111910897328637418053809245315041281/1001664724473541313810631372082366057790006922699038042245185229675973731425298624566022042569027049250995581232879886904657015933499771706178217540055337050505176382127623343584896161358272314123927817183570950193102986253744051102251945314087648264529794907956945104156426853730586124020444279865341217172541716045779016352193369674212758093620843686204567974507731225915959766918500274836107618490630082562000000000000000000000000", + "delta_positive": "1/8000000000000000000000000", + "delta_below_one_eighth": "999999999999999999999999/8000000000000000000000000", + "short_record_fallback": "499166252109442939392471034848313316114250134254583983208272378189307524869389196786311068454003871638363565073667442854566897062166646758788175230586903686271597650140641045878312702032764525488102192186548771052998199058798407284251362480294772923341142124540136984090929370771350787400236435326699293133434343174557778568497083898983131054301960391766264722813034639533891381497022881289597081717033630973232881843193942536430058013647486929729882685629072964837572548559417169158433520869887573539650176079300570380996556407568182796097355492472080375078864450622471571808570988799908093787137476435313054041949177339074947387741138862798113754130077639828104833239971326478608502810358427238626395859702434453031764080885755118070275015398466012570428035670498547379208048136698734120961/500832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "small_field_exposure": "1/1000000000000000000000000", + "artificial_boundary": "28053271183153322041940209409132800559592192242316275475395014034641543454166619353890549876169462713979795448485220234489598386365364543917533318267294685865823203495410257077722252921229287243400705527218512443587766746011535410628487539705284125081030090432540214464478056114071117904071873190331199545400520944131348321282013588387382327664391526248600686503384539660576241848243970556352282665639813019734412254161427735945123843/4006658897894165255242525488329464231160027690796152168980740918703894925701194498264088170276108197003982324931519547618628063733999086824712870160221348202020705528510493374339584645433089256495711268734283800772411945014976204409007781256350593058119179631827780416625707414922344496081777119461364868690166864183116065408773478696851032374483374744818271898030924903663839067674001099344430473962520330248000000000000000000000000", + "literal_scalar_guard": "1", + "row_product_gap": "23971789/25", + "balanced_prefix_above_kappa": "61586275478495855277543387203031290113944530035665247171993720864597646011585438078964042931098423570673647575246209893058289690829486282424188513157077074016387562700517241406125408771872024248656302918629867256049800227305061305013112089636005088650853480390644426630472667988975534093642266276030439630341229766551755679448202822191112719903145777646238150075050807695091696599283124950600887084327863177/62604045279596332113164460755147878611875432668689877640324076854748358214081164035376377660564190578187223827054992931541063495843735731636138596253458565656573523882976458974056010084892019632745488573973184387068936640859003193890746582130478016533112181747309069009776678358161632751277767491583826073283857252861188522012085604638297380851302730387785498406733201619747485432406267177256726155664380160125000000000000000", + "coordinate_movement_above_kappa": "2766701776649810631375411815004872634543961788865875194974945061655003030374955971932692337055311745493176745271578767639424486125196721375075334186022755569824877774011956941672497922069671951731066915946037242330157206184934144019798747962676899663195996542600081780653056978117105644443426647331128775927334665869646855627226067427425360137397459020109362581946190754684958719/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "compact_phase_layer_above_kappa": "492689702995604605449690192308564279728527345281860627856928644324166330105817791982400060437766104051864555104179062704522865198127923509507655016147846564462575249015946867437331477726895514853093361385130346262923305266947363568079345591115383665382695578227701434571229265698377407456076119986103584372121251861556022546077446480844064652846119410748062098316419207695120614814381540354669678620813660100958719/500832362236770656905315686041183028895003461349519021122592614837986865712649312283011021284513524625497790616439943452328507966749885853089108770027668525252588191063811671792448080679136157061963908591785475096551493126872025551125972657043824132264897453978472552078213426865293062010222139932670608586270858022889508176096684837106379046810421843102283987253865612957979883459250137418053809245315041281000000000000000000000000", + "bulk_exposure_above_kappa": "2766701776649810631375411815004872634543961788865875194974945061655003030374955971932692337055311745493176745271578767639424486125196721375075334186022755569824877774011956941672497922069671951731066915946037242330157206184934144019798747962676899663195996542600081780653056978117105644443426647331128775927334665869646855627226067427425360137397459020109362581946190754684958719/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "Gaussian_arithmetic_above_kappa": "788303825292384710781898450883114472275461089453053814282498504474235030961427894761427466507038537191098063465360870191202655714109457665143759879301816519741235549978429626186733439831881231246643615394553709091962346358011657832142283621368208090906792284102794682397498072045459971105558998111049694597759154741004449807428820027361405708381219143450005218676663084631560758490940540117553936625587403350558719/801331779578833051048505097665892846232005538159230433796148183740778985140238899652817634055221639400796464986303909523725612746799817364942574032044269640404141105702098674867916929086617851299142253746856760154482389002995240881801556251270118611623835926365556083325141482984468899216355423892272973738033372836623213081754695739370206474896674948963654379606184980732767813534800219868886094792504066049600000000000000000000000", + "scalar_work_above_kappa": "3941521129791372500992119875678316526109421027279114469488577012741634506754602324404386464579277824009588819317966816715787087884579155325262211752944162709380278760244912386180354368951728872777846324828402912601712117996030796648813622610731668629830490480103789325877698673081007316700043031443808203671230118788454340595176804523546376967422282958937398502519264438620255624374236537588319355343173998012958719/4006658897894165255242525488329464231160027690796152168980740918703894925701194498264088170276108197003982324931519547618628063733999086824712870160221348202020705528510493374339584645433089256495711268734283800772411945014976204409007781256350593058119179631827780416625707414922344496081777119461364868690166864183116065408773478696851032374483374744818271898030924903663839067674001099344430473962520330248000000000000000000000000", + "dimension_above_kappa": "62395954720403667948421689723347976665667954534341412473620453180916888957912556829221268351021247500776819104043430639132584079402474161422151094576027716767614989274100615042331552615625221773379920197898839861587366277770864062159053645174583288479999907888696019641076802032482793879194900497391708020358409023169251108329144161913458298596900091803327221496412576026490664642644540517834970443618744790475887084327863177/62604045279596332113164460755147878611875432668689877640324076854748358214081164035376377660564190578187223827054992931541063495843735731636138596253458565656573523882976458974056010084892019632745488573973184387068936640859003193890746582130478016533112181747309069009776678358161632751277767491583826073283857252861188522012085604638297380851302730387785498406733201619747485432406267177256726155664380160125000000000000000" + }, + "conservative_controls": [ + "next_grid", + "zero_eta", + "zero_beta", + "unit_beta" + ], + "model_controls": [ + "native_complex_endpoint_rejected_with_old_surcharge", + "omitting_bit_surcharge_would_fail_next_endpoint_rejection" + ], + "native_correction_gain": "2.882365E-12", + "template_sha256": "d7074fb509f61cf6d62bda4b3bec2419d5baaafcb8ceeed8c5ce295db6f5b82d", + "input_sha256": { + "owner_audit": "a180f6a1c146683b802f9c494249a19c87b1a8d2d8deb7c59e248a500153b740", + "fresh_invoice": "7ca2d8fb3936d48fb2b9238b7fde6b1e57d55a09fab3b6d544544d0988bd6d87", + "package:inputs/PR589-EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "engines/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", + "engines/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, + "bit_supplier": { + "pr": 589, + "repository": "CrocSwap/integer-mult-bounds", + "commit": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "merged_as": "b3eb785ac5b4b1ca2beea0f80db078a505626a90", + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "git_blob_sha1": "e293ddc557742637f9f679f083a1a282d87b1b13", + "word": { + "v": 111, + "decoder_constant": 63, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ] + }, + "derived_deficit": 10272, + "deficit_formula": "T(2Kv-L*cst), L=9 T=32 K=4 M=64", + "replay_scope": "Cited unchanged supplier; this assembly reprices its full profile and does not rebuild its bit circuit." + }, + "moments": [ + { + "side": "bit", + "surcharge": true, + "endpoint": "1733427039589844234749/1000000000000000000000000", + "accept": true, + "mercator": [ + "-43100600330766044577088869872467188970742291/26959946667150639794667015087019630673637144422540572481103610249216", + "-43100600330766044577088869872467188970742289/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two": [ + "-799345163337715793503/500000000000000000000000000000000000000000000", + "-3197378653350863173989/2000000000000000000000000000000000000000000000" + ] + }, + { + "side": "bit", + "surcharge": true, + "endpoint": "6933708158359376939/4000000000000000000000", + "accept": false, + "mercator": [ + "22502934905675809315035333485365686073718547/13479973333575319897333507543509815336818572211270286240551805124608", + "5625733726418952328758833371341421518429637/3369993333393829974333376885877453834204643052817571560137951281152" + ], + "base_two": [ + "8346798366759439729359/5000000000000000000000000000000000000000000000", + "16693606733518879458833/10000000000000000000000000000000000000000000000" + ] + }, + { + "side": "complex", + "surcharge": false, + "endpoint": "1664724476433282815289/1000000000000000000000000", + "accept": true, + "mercator": [ + "-8712535389683307555990582570207835629468437/26959946667150639794667015087019630673637144422540572481103610249216", + "-8712535389683307555990582570207835629468435/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two": [ + "-161583/500000000000000000000000000000", + "-64633/200000000000000000000000000000" + ] + }, + { + "side": "complex", + "surcharge": false, + "endpoint": "166472447643328281529/100000000000000000000000", + "accept": false, + "mercator": [ + "8845029978943766580636456482703766986765687/3369993333393829974333376885877453834204643052817571560137951281152", + "35380119915775066322545825930815067947062749/13479973333575319897333507543509815336818572211270286240551805124608" + ], + "base_two": [ + "2624643/1000000000000000000000000000000", + "656161/250000000000000000000000000000" + ] + } + ], + "bootstrap": [ + { + "exponent": "1662017193987737924111273772831049885872555589772868738448988081673819950695374847238307846479/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "2707282445544891177723562444473680844629121227131261551011918326180049304625152761692153521/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "4911739962300" + }, + { + "exponent": "1664719969553931098552537234223089383583028340239399220149409519496208250128213748863941244009348587674496128851150320621985949585120073982569/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "4506879351716736460101052434183134156370760600779850590480503791749871786251136058755990651412325503871148849679378014050414879926017431/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "1772354679584936601" + }, + { + "exponent": "1664724468930570446154380157624025367073007045736946503434062345448591051766849769841133765516772211126263258754926166373622984049234463078852407889045107725832125114274741142880541367302559/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "7502712369134617177651498199644177665263053496565937654551408948233150230158866234483227788873736741245073833626377015950765536921147592110954892274167874885725258857119458632697441/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "639537339997092785093291" + }, + { + "exponent": "1664724476420792866368460194783394847539468303028251185369144200780704840732542677502904391938842288840957660986223773226859092525068729961427738062013263725340698265496409844567339176478508997964348130466741615160366572624637824625975449/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "12489948920537140492128719177716407971748814630855799219295159267457322497095608061157711159042339013776226773140907474931270038572261937986736274659301734503590155432660823521491002035651869533258384839633427375362175374024551/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "230770970371653623203571880616" + }, + { + "exponent": "1664724476433262022965319915638448163247526793249429515148932201755339848361937250460932167740939584614190960594633508983096227716812489839949761352934656237312561978995132812482877557783185887863554437586507974866467513192995858496411493923908177215657912123477721176670980019484160239/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "20792323677419637075403469657917750570484851067798244660151638062749539067832259060415385809039405366491016903772283187510160050238647065343762687438021004867187517122442216814112136445562413492025133532486807004141503588506076091822784342087876522278823329019980515839761/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "83271511193571156577312847008652168" + }, + { + "exponent": "1664724476433282780675507187551768664903512770871340864901589720632768444262613963683270045068399876229364877432868780740269483324057260075425888094049303800655580067633458483324520751493508051305589593977815222760343745522723412659046236555608269969956546648584277889934671897583818966399074757399024033369496345121925214104084905929/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "34613490147723754901813671940128659135098410279367231555737386036316729954931600123770635122567131219259730516675942739924574111905950696199344419932366541516675479248506491948694410406022184777239656254477276587340953763444391730030043453351415722110065328102416181033600925242600975966630503654878074785895915094071/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "30047733323189209922169488978628724269702" + }, + { + "exponent": "1664724476433282815231375411011825545787326793746327784420186909328000714054177940846451683861524595662733149708009456423902440435510905010516389128178221582916730142077347975538912678035869893900415695276316028452462395904394768926976694666358711481976536969199429021332507830626059034459171167301601505757454287739571270956904388470647416857875428392829301862104183879992152051519/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "gap": "57621924263698020929857917253672215579813090671999285945822059153548316138475404337266850291990543576097559564489094989483610871821778417083269857922652024461087321964130106099584304723683971547537604095605231073023305333641288518023463030800570978667492169373940965540828832698398494242545712260428729043095611529352583142124571607170698137895816120007847948481/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "cutoff_log2": "10842438967664605363124742529348764315980600770" + } + ], + "outer": { + "bit_positive": "1664724476433282815231375411011825545787326793746327784420186909328000714054177940846451683861524595662733149708009456423902440435510905010516389128178221582916730142077347975538912678035869893900415695276316028452462395904394768926976694666358711481976536969199429021332507830626059034459171167301601505757454287739571270956904388470647416857875428392829301862104183879992152051519/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "complex_above_bit": "57624588988174454212673206253672215579813090671999285945822059153548316138475404337266850291990543576097559564489094989483610871821778417083269857922652024461087321964130106099584304723683971547537604095605231073023305333641288518023463030800570978667492169373940965540828832698398494242545712260428729043095611529352583142124571607170698137895816120007847948481/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "complex_below_one_over32": "29585275523566717184711/1000000000000000000000000", + "beta_positive": "1/1000000000000000000000000", + "beta_below_one": "999999999999999999999999/1000000000000000000000000", + "leaf_saving_above_bit": "57622924263698020929857917253672215579813090671999285945822059153548316138475404337266850291990543576097559564489094989483610871821778417083269857922652024461087321964130106099584304723683971547537604095605231073023305333641288518023463030800570978667492169373940965540828832698398494242545712260428729043095611529352583142124571607170698137895816120007847948481/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "q_positive": "832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "q_below_internal": "1664724476433282815231375411011825545787326793746327784420186909328000714054177940846451683861524595662733149708009456423902440435510905010516389128178221582916730142077347975538912678035869893900415695276316028452462395904394768926976694666358711481976536969199429021332507830626059034459171167301601505757454287739571270956904388470647416857875428392829301862104183879992152051519/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "q_below_leaf": "28813126856325443747744190002247119615452332662793389300695449763683486069951756346574271597679133312644442515394255504198229338351324719446645445350454190452126577712207130397767691274520021643662702463497891852540105129216548653780658492094951848045228061223939682199435748857029873180307315301381666123053563218964031142333242707973819716364765935432316803542362104183879992152051519/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "c_positive": "832362238216641407615811040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "c_below_one": "499167637761783358592384188959218563660389151834502247119615452332662793389300695449763683486069951756346574271597679133312644442515394255504198229338351324719446645445350454190452126577712207130397767691274520021643662702463497891852540105129216548653780658492094951848045228061223939682199435748857029873180307315301381666123053563218964031142333242707973819716364765935432316803542362104183879992152051519/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "q_below_reservations": "1/4000000000000000000000000", + "lambda_above_tau": "1664724476433282815231375411011825545787326793746327784420186909328000714054177940846451683861524595662733149708009456423902440435510905010516389128178221582916730142077347975538912678035869893900415695276316028452462395904394768926976694666358711481976536969199429021332507830626059034459171167301601505757454287739571270956904388470647416857875428392829301862104183879992152051519/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "lambda_above_sigma": "57626253712650887495488437629083227405358877998793032273606479340457644139189458515207696743674405100693222297638802998940034774262213927988280374311780202682670238694272183447559843636362007417431504511300507389051757796037192912792390007495237337378974145910910164969850165206229120301580171431596030644601368983640322713395528511559168785312673995436240777782862104183879992152051519/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "lambda_above_internal": "1664724476433282815231375411011825545787326793746327784420186909328000714054177940846451683861524595662733149708009456423902440435510905010516389128178221582916730142077347975538912678035869893900415695276316028452462395904394768926976694666358711481976536969199429021332507830626059034459171167301601505757454287739571270956904388470647416857875428392829301862104183879992152051519/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "lambda_prime_above_lambda": "1664724476433282815231375411011825545787326793746327784420186909328000714054177940846451683861524595662733149708009456423902440435510905010516389128178221582916730142077347975538912678035869893900415695276316028452462395904394768926976694666358711481976536969199429021332507830626059034459171167301601505757454287739571270956904388470647416857875428392829301862104183879992152051519/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "compact_leaf": "28813126856325443747744190002247119615452332662793389300695449763683486069951756346574271597679133312644442515394255504198229338351324719446645445350454190452126577712207130397767691274520021643662702463497891852540105129216548653780658492094951848045228061223939682199435748857029873180307315301381666123053563218964031142333242707973819716364765935432316803542362104183879992152051519/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "compact_reservations": "1/4000000000000000000000000", + "lambda_prime_below_one": "832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "epsilon_positive": "499999999999999999999999500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000/500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481", + "epsilon_below_one": "832362238216641407616186040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481/500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481", + "guard_width": "832362238216641407616186040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481/500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481", + "K_geometry": "375832362238216641407615811040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481/500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481000000000000000000000000", + "K_dominates_log": "19357261353875381572460702521376700534173036039225862766237396662535839835963352690433701784265989403462220746181556666025858233927380050579885658281190480809508343090206608392385880672866005117591226996559481175894597565213799596918175314732230577770027768558376217872172691149640753784939820845837938389752904282194585835042316676473285354403090240595102308085264567390939329541333820013536173027087256357258236834418422140733/11647264238098061428084085721878638054409554608499947741404291806217144339783704756982239918928605773108219202986100485271798966453130366151065157457247643611175659408247663856035997056332274252781447262993615813450147379012476793212731625462111243054563240500183838329115227254390140937623268936073092328530690527551130658927370847367000836485062017611442469308921749629408550772010642741763165581577859267000000000000000000000000", + "record_suffix": "832362238216641407616186040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481/500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481", + "phase_local": "6658897905733131260928987493889252500245377708295982261640041727849487387841556017342864774233775249922855590902053003450600806451117553645547477937631917638682340635425704827707706824947788307272048921930417539057828778059708139699700802628970074267646584603345514432186829290866974637356362054371822238497223677024695528045444674555603052243000181389772661233113014849784173545480819531294895495100391390362104183879992152051519/4006658897905733131260925488326251490716886785323982023043076381338697652885594436401890532111440385949227405827218566933498844459876845955966414165293189402244426836437196366476382987378302342956817858469803839826850698380292016865179679158966267610769754732063240385215638175510208482542404514009143761014557541477588946671015571494248287750861334058336209442269081872516541465571661103166528960062783587848000000000000000000000000", + "phase_boundary": "1331779581146626252185396832888059926735949449110363827178936656891365079366006895830439085081466490540930929127199456651525238549640788872416145703080395843140871485668611646601316922305913941817762146087345677577270073826094647555957475455955985651842798952753206259676288882700188603432750847056813426851190494953538191232987479156972851553932934720805107417847516836551001088151936998071727444873521111962104183879992152051519/801331779581146626252185097665250298143377357064796404608615276267739530577118887280378106422288077189845481165443713386699768891975369191193282833058637880448885367287439273295276597475660468591363571693960767965370139676058403373035935831793253522153950946412648077043127635102041696508480902801828752202911508295517789334203114298849657550172266811667241888453816374503308293114332220633305792012556717569600000000000000000000000", + "gamma_sublinear": "1/2000000000000000000000000", + "cell_above_band": "999999999999999999999998499167637761783358592384313959218563660389151834502247119615452332662793389300695449763683486069951756346574271597679133312644442515394255504198229338351324719446645445350454190452126577712207130397767691274520021643662702463497891852540105129216548653780658492094951848045228061223939682199435748857029873180307315301381666123053563218964031142333242707973819716364765935432316803542362104183879992152051519/2003329448952866565630462744163125745358443392661991011521538190669348826442797218200945266055720192974613702913609283466749422229938422977983207082646594701122213418218598183238191493689151171478408929234901919913425349190146008432589839579483133805384877366031620192607819087755104241271202257004571880507278770738794473335507785747124143875430667029168104721134540936258270732785830551583264480031391793924000000000000000000000000", + "prime_interval_packing": "832362238216641407616186040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481/500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481", + "alpha_positive": "1664724476433282815231871249200634462580288715309464979332755723826247723645728715924965690653485788002301220488127803326467461543483086670736853967739865955362213307528429970420466291221031089658655069577537668919804992840695490814941433404269366190330535555915225520458197658210612730552976547514001477579067568832985524783766053869387239096999637637615579531301610462378074366734992156398175448012700504362104183879992152051519/1001664724476433282815231372081562872679221696330995505760769095334674413221398609100472633027860096487306851456804641733374711114969211488991603541323297350561106709109299091619095746844575585739204464617450959956712674595073004216294919789741566902692438683015810096303909543877552120635601128502285940253639385369397236667753892873562071937715333514584052360567270468129135366392915275791632240015695896962000000000000000000000000", + "alpha_below_one": "999999999999999999999999500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481/1001664724476433282815231372081562872679221696330995505760769095334674413221398609100472633027860096487306851456804641733374711114969211488991603541323297350561106709109299091619095746844575585739204464617450959956712674595073004216294919789741566902692438683015810096303909543877552120635601128502285940253639385369397236667753892873562071937715333514584052360567270468129135366392915275791632240015695896962000000000000000000000000", + "alpha_below_one_fourth": "248751456642675037888575971771190083707225135367439411460859518109842355581703923559193192566311538333824411643713032630017210317198819785577164031363084471684914463969796342934353470419922865345142461084785202320258363655927555563258788514031122359482779135198037298555519188311177417428347305578057483585830778773516323642154707164521130745331833741008397510610516006569905767231493826791509884555911273736137895816120007847948481/1001664724476433282815231372081562872679221696330995505760769095334674413221398609100472633027860096487306851456804641733374711114969211488991603541323297350561106709109299091619095746844575585739204464617450959956712674595073004216294919789741566902692438683015810096303909543877552120635601128502285940253639385369397236667753892873562071937715333514584052360567270468129135366392915275791632240015695896962000000000000000000000000", + "delta_positive": "1/8000000000000000000000000", + "delta_below_one_eighth": "999999999999999999999999/8000000000000000000000000", + "short_record_fallback": "499166252107992140558588172574016551450528958219740944399933245190335888613519490828418926736229321321779573361265817782115521588996952256106910198276506362537129587589780540813470304851899353860533367811076373587130553918370401680846960895306386519199235474468381032241453140977076522854821206147310208547702084048479855228456556282946708102389134699762341054627338276305746163495263584335855287806271995114509777252892311928429130040950062105544099367044572641145158543305488716446873364162004593282798845925065922039629852868840360445739251374761432051777278708964081457818100503294111489081669761073028457677188925822927507574065188599898713856722085832310937516233671499479469328731664315173142462987453564625065497332669406417585527206939578972965297738954768716810480217735360430207361/500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "small_field_exposure": "1/1000000000000000000000000", + "artificial_boundary": "28053271183245865050087409409107098640385018505438914306688920069542125719578014132368767258903142919691732897326698077258135486639291952854693913384412187671772648178902882916757089740686482407603180296402050985478184195849033061097877368340742033495664362298885607694075459442739692384054380567937465904444641285222404326797034952413064356102745674097528985881260561553132603600651829676237933874205318292156913687448360023543845443/4006658897905733131260925488326251490716886785323982023043076381338697652885594436401890532111440385949227405827218566933498844459876845955966414165293189402244426836437196366476382987378302342956817858469803839826850698380292016865179679158966267610769754732063240385215638175510208482542404514009143761014557541477588946671015571494248287750861334058336209442269081872516541465571661103166528960062783587848000000000000000000000000", + "literal_scalar_guard": "1", + "row_product_gap": "23971789/25", + "balanced_prefix_above_kappa": "158025997773288288180728065040280988183927787830683559640800559124006543533838762767044999226166228184527699664020290247114408208228279209017144601395307566532599985869652847736384745662119613836105944292437779244854769089737617187235465593362035731520408268076855303248177528357272830397945122145726806515351812855769096059817406139203349318920797418554931025095558552791762570616136296633699492708448287051/500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481000000000000000000", + "coordinate_movement_above_kappa": "2766701786253815231375411011825545787326793746327784420186909328000714054177940846451683861524595662733149708009456423902440435510905010516389128178221582916730142077347975538912678035869893900415695276316028452462395904394768926976694666358711481976536969199429021332507830626059034459171167301601505757454287739571270956904388470647416857875428392829301862104183879992152051519/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "compact_phase_layer_above_kappa": "158025496940926049964086657424594947402491448219835394143047678739458876196632152067740448989849714254479456010594561844793541520872721724411400105593536904883924705316298293086838936114246191548313074690205470519374790733400319650733357445902140860736956921857513795343129376402500891621884804345162555372381686036076411361199072262256912537884828560888173733069378269156528506048453100176061596892328279203051519/500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481000000000000000000000000", + "bulk_exposure_above_kappa": "2766701786253815231375411011825545787326793746327784420186909328000714054177940846451683861524595662733149708009456423902440435510905010516389128178221582916730142077347975538912678035869893900415695276316028452462395904394768926976694666358711481976536969199429021332507830626059034459171167301601505757454287739571270956904388470647416857875428392829301862104183879992152051519/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "Gaussian_arithmetic_above_kappa": "252841095604899022872523496448763540312848120918245529927528014213862802316935409727967448525549451165196075809006735993062186445809689249821686866430721444803484696838090001728669783511517959849976641265668138066287652187242889963074636801919362299649201882703626977292035893416864589860651877632598639281592773749537868997089515945778922129237307012021132348126713400831586048418134878156281292517397251433651519/801331779581146626252185097665250298143377357064796404608615276267739530577118887280378106422288077189845481165443713386699768891975369191193282833058637880448885367287439273295276597475660468591363571693960767965370139676058403373035935831793253522153950946412648077043127635102041696508480902801828752202911508295517789334203114298849657550172266811667241888453816374503308293114332220633305792012556717569600000000000000000000000", + "scalar_work_above_kappa": "1264207481353944067229183112706561864689985963034620311628651592607504680933503491437055443573013311546173353658736593574594398978470676187531412315360689870612124606403868227241532155749083488401054684737269925233358174361563639961381616599436390981379814798395500918080372074903410704407500659365250200979844376026460083779920915236680357770330410490772690908738288138698866500361407176611958045851466288560051519/4006658897905733131260925488326251490716886785323982023043076381338697652885594436401890532111440385949227405827218566933498844459876845955966414165293189402244426836437196366476382987378302342956817858469803839826850698380292016865179679158966267610769754732063240385215638175510208482542404514009143761014557541477588946671015571494248287750861334058336209442269081872516541465571661103166528960062783587848000000000000000000000000", + "dimension_above_kappa": "499167637761783358750409311732506851841117216874783235303543240163346353030101254573770227019908714523391573497763907317840344106535684502618606437566630533736591246840658020723052112447365054866782513353394133857749606994901277136707309194866833735889246251854130683368453496138079242930376964106129860271125429461028188181474866418988060090959739381911323138637162184490363341899100914895946450608288348152699492708448287051/500832362238216641407615686040781436339610848165497752880384547667337206610699304550236316513930048243653425728402320866687355557484605744495801770661648675280553354554649545809547873422287792869602232308725479978356337297536502108147459894870783451346219341507905048151954771938776060317800564251142970126819692684698618333876946436781035968857666757292026180283635234064567683196457637895816120007847948481000000000000000000" + }, + "controls": [ + "next_grid", + "zero_eta", + "zero_beta", + "unit_beta" + ], + "scope": "Conditional native exact-complex witness after complete conservative admission, moment and outer checks; PR559 exact-cover recurrence correction only, bit bad-residue surcharge and H1-H5 retained. The new source-branch gauge and retired-basis completion, the gauge44-barch U8 local word and all 72 cold helper ends, and explicit all189 whole-owner dispatch with a T16 plus T5 nine-role trade are composed with the cited unchanged merged PR589 bit supplier (PR555 punctured R439 word; derived bit deficit T(2Kv-L*cst)), replacing the PR543 supplier of PR635; This is a new T21 composition of the PR870 U8 and PR589 suppliers. All-size compiler, common-label/mutable-source realization, whole-call hosting, precision/tape and analytic transfer remain assumptions. No unconditional theorem or full Lean certification." +} diff --git a/research/t21-binomial-audit/inputs/CLAIM.json b/research/t21-binomial-audit/inputs/CLAIM.json new file mode 100644 index 0000000000..ec036987fb --- /dev/null +++ b/research/t21-binomial-audit/inputs/CLAIM.json @@ -0,0 +1,30 @@ +{ + "kappa": "1661957774647029/1000000000000000000", + "kappa_decimal": "0.001661957774647029", + "baseline870_kappa": "1661956299899884/1000000000000000000", + "complex_lower": "1664724476433282815289/1000000000000000000000000", + "bit_lower": "1733427039589844234749/1000000000000000000000000", + "replicas": 21, + "calls": 189, + "roles": 95256, + "live": 18816, + "physical": 19330, + "rank_mass": 1366848, + "deficit": 6720, + "prefix_bits": 491, + "row_coefficient": 16469, + "idle": { + "1": 3, + "3": 1, + "48": 6292 + }, + "local_profile": { + "1": 2548, + "2": 338, + "3": 446, + "4": 162, + "5": 72, + "8": 8 + }, + "scope": "Conditional finite U8/T21/PR589 composition. All-size compiler, common-label/mutable-source realization, whole-call hosting, precision/tape, analytic transfer and bit H1-H5 remain inherited hypotheses." +} diff --git a/research/t21-binomial-audit/inputs/PROOF.md b/research/t21-binomial-audit/inputs/PROOF.md new file mode 100644 index 0000000000..64e611cce1 --- /dev/null +++ b/research/t21-binomial-audit/inputs/PROOF.md @@ -0,0 +1,123 @@ +# The T21 owner composition + +## Fixed suppliers and the new finite object + +The complex local supplier is the U8 word from PR869/PR870, pinned to PR870 +head `b734850dc348800942f0ffd1f0723fdec7539b2b`. Its paid profile is +`{1:2548,2:338,3:446,4:162,5:72,8:8}`; the 504 helper residual widths are +`{4:80,5:32,7:54,8:122,9:216}`, of total width 3778. Both exact scalar +orientations, all literal frames, normalized wrappers and all phase edges are +replayed before the controller uses them. The bit supplier is the unchanged, +blob-pinned PR589 word, with its original exceptional-residue surcharge. + +The new finite object is a literal owner for every one of `189*504 = 95256` +whole-helper roles. No helper is split. The owner includes invocation, physical +family, idle child, port, residual offset and full width. Each call uses 504 +distinct helper families, disjoint from its 224 active data families. + +`data/T5-OWNERS.json.gz` is an explicit 45-call, 22,680-role witness. Its +independent replay checks every role and obtains idle profile `{48:1498,6:1}`. +It was discovered using an integer aggregate packing followed by bipartite +matching decomposition. The solver and this discovery history are not premises: +the published literal map is checked directly, using integer and rational +arithmetic, without NumPy/SciPy or an optimizer in the owner construction. + +Hao Yan's unchanged PR858 constructor reproduces the T16 witness from PR799's +literal T8 map, including its eleven omitted-edit controls. T16 contributes +`{48:4793,44:1,2:1,1:2}`. Relabel T5's replicas by adding 16. The combined +pre-trade idle profile is `{48:6291,44:1,6:1,2:1,1:2}`. + +## Interleaving and the nine-role trade + +The initial order expands each original `(stage,r)` to available copies +`r,r+8,r+16`, omitting third-copy labels above 20. Preserve the T16 and T5 +subsequences separately. Place each T16 call at integer time `2*j`. If a T5 +call originally followed `j` T16 calls, give it sort key `2*(j+4)-1`. Stable +sorting gives the final 189-call order. This is a four-call placement delay, +not additional execution. Every replica still projects exactly to the original +30 source events, with both global tail events after all replica-local work. + +`data/EDITS.json` lists nine exact before/after locations. An early width-four +role leaves a cap-48 bin containing only that role and replaces a later +width-four role in a full cap-48 bin. The later role joins two cap-32 bins +previously filled to 26 and 30. They are repacked to 29 and 31; all offsets +remain contiguous prefixes. Thus + +``` +idle (44,6,2) -> (48,3,1) +``` + +and the two existing rank-one remainders remain. The resulting profile is +`{48:6292,3:1,1:3}`. Offset-only changes count among the nine recorded edits. +The rank mass is unchanged by this trade. Every omitted edit is rejected; +removing the placement delay is rejected after recomputing that alternative +schedule's actual windows. + +For each idle child, the independent audit locates the previous touch of its +physical pair, including bridges, and its idle event. A helper's entire call +must lie strictly between those events. The checker independently reconstructs +the orthogonal 73-axis port basis and the residual/spectator coordinate +permutation for every occupied chart. It checks full widths, no repeated family +within a call, no overlapping slices, and exact coverage of all invocation/helper +identities. These checks establish the same whole-call hosting interface as the +predecessor constructions; they do not establish its all-size realization. + +## The partial bank group + +An auxiliary dedicated-bank envelope uses groups of 8, 8 and 5 replicas. +Data stock is `896*21=18816`; three groups of nine 504-family banks add 13608 +families. The envelope therefore has live stock 32424 and physical stock 32938, +including the same 514 restored private families. It preserves the exact data +recipes, local programs and source helper routes. + +A width-w helper in local lane r occupies axes `wr,...,w(r+1)-1`. A group of +a active lanes consequently occupies the prefix `[0,aw)`. Its padding is +exactly `[aw,73)`, with literal standard orthogonal axes. `check_parent.py` +derives those occupied coordinates from the calls, checks disjointness and +the complement independently, and verifies all translated namespaces and +event multiplicities. Eight targeted mutations are rejected. + +The five-lane group's largest auxiliary padding rank is 53. These are **not +selected recursive children**: every bank and padding child is deleted by the +hosted controller. The dedicated-bank object is used only as the conservative +geometry/work envelope in the inherited invoice. Its number of padding children +is unchanged per bank. The emitted recursive profile has maximum rank 48 and +passes `73^2 > 2*48^2`. The independent final audit also requires empty bank +families and the hosted data-only namespace. No rank-53 halving claim is made. + +## Cost, prefix and exact price + +Multiply the unchanged local profile by 189 and add the idle profile. Its rank +mass is 1366848, giving deficit `73*18816-1366848=6720=21*320`. +Physical stock after hosting is `18816+504+8+2=19330`. The fresh invoice +recounts scalar primitives, Horner coefficient work, paid children, wrappers, +bridges, shifts, moves, private streams and final corrections. Only the +replication-dependent source constants change. The 144 elementary factors per +wrapper and scalar adapter multiplier 16 remain unchanged. + +The checked local prefix bound is 72. With 189 complete calls and 189 bridges, +the global prefix is `72+37+189+189+4=491<512`. The physical row coefficient is +16469, below the retained 20161. All logical/router/literal, mass, precision, +tape, row and halving inequalities are independently recounted and checked. + +Two unchanged rational moment engines certify the complex lower endpoint + +``` +b = 1664724476433282815289 / 10^24. +``` + +Both accept the lower endpoint and reject its successor at `b+10^-24`. +The bit lower endpoint remains `1733427039589844234749/10^24`. The retained +seven-step outer assembly satisfies all 47 strict inequalities and gives + +``` +kappa = 1661957774647029 / 10^18. +``` + +Conservative complex admission, its surcharge price and outer checks run +before selecting the inherited native-complex correction. Omitting the bit +surcharge or advancing the final kappa grid point is rejected. + +The result retains the predecessor all-size compiler, common-label/mutable- +source, whole-call hosting, precision/tape and analytic-transfer hypotheses, +and the bit H1–H5 interface. This finite composition does not discharge them. diff --git a/research/t21-binomial-audit/inputs/selected-result.json b/research/t21-binomial-audit/inputs/selected-result.json new file mode 100644 index 0000000000..5dbfac5424 --- /dev/null +++ b/research/t21-binomial-audit/inputs/selected-result.json @@ -0,0 +1,170 @@ +{ + "status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status", + "kappa": "1661957774647029/1000000000000000000", + "decimal": "0.001661957774647029", + "source_prs": [ + 890, + 870, + 869, + 858, + 799, + 741, + 699, + 685, + 676, + 664, + 660, + 659, + 656, + 655, + 653, + 658, + 649, + 645, + 635, + 589, + 555, + 545, + 626, + 623, + 622, + 620, + 617, + 615, + 604, + 601, + 596, + 592, + 591, + 593, + 599, + 588, + 543, + 584, + 586, + 583, + 582, + 579, + 576, + 575, + 574, + 571, + 569, + 568, + 567, + 564, + 562, + 561, + 559, + 558, + 552, + 550, + 548, + 541, + 535, + 510, + 503, + 531, + 523, + 493, + 514, + 507, + 484, + 496, + 505, + 522, + 520, + 472, + 458, + 445, + 442, + 425, + 433, + 370, + 361, + 315 + ], + "source_manifest": "research/community-frontier890-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier890-audit/ASSEMBLY.json", + "certificate_sha256": "190110b509dc87d38b72ad37c3290efcc245ce26df4cae3d7e2d6dcf0bac2c43", + "proof": "docs/research/community-frontier890-review.md", + "proof_supplements": { + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/complex-571-free4fc8/NOTICE.md": "a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97", + "research/complex-multicold/proof/CONSTRUCTION.md": "27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f", + "research/complex-multicold/vendor/pr559/PROOF.md": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453", + "research/structural-gain/frontier-composition/README.md": "70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887", + "research/complex-joint-prefix/proof/CONSTRUCTION.md": "a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105", + "research/kernel-frame-coalescing/PROOF.md": "fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b", + "research/complex-571-hpeq5/README.md": "4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b", + "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9", + "docs/research/community-hyperplane599-review.md": "3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c", + "research/complex-571-cold14-b3/README.md": "1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96", + "research/complex-571-cold14-b3/PROOF-NOTE.md": "1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d", + "scripts/verify_cold617_interface.py": "95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a", + "docs/research/community-cold617-review.md": "b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046", + "research/complex-k492-owner-repair/README.md": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902", + "research/complex-k492-owner-repair/PROOF-NOTE.md": "337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "scripts/verify_frontier626.py": "2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444", + "scripts/verify_frontier626_bindings.py": "cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280", + "scripts/verify_frontier588_bindings.py": "6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d", + "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "docs/research/community-frontier741-review.md": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a", + "research/complex-sw4-frame8/PROVENANCE.md": "c7648719b01dd93af2c3a2c6e951a54711d13892dc4bd4339d16edb4c37c9bf0", + "research/e8-bit-p111-tuned/tune/README.md": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d", + "scripts/verify_frontier741.py": "215ee6a12de8dc2392e6811a1b8f2140035f6b2d2a0d2100ff4bd2fdcb8bb39b", + "scripts/verify_frontier741_bindings.py": "eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "scripts/verify_frontier799.py": "19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99", + "scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036", + "docs/research/community-frontier890-review.md": "cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea", + "scripts/verify_frontier890.py": "88ea38dbef62dd7c0dd46e212618520cc89213edddb2032800e5509993958175", + "scripts/verify_replay_coverage.py": "babe5941d7e6dac4248613ef01f950ee7bb6199e7355021aea4cf854fd1b91c5", + "scripts/verify_frontier741_bridge_coverage.py": "9a14f26762b6126eb54ed43db90371773374fe98733ada80ee871a74afa3b836", + "certificates/replay-coverage/pr741-sw4-v1.json": "7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756", + "research/complex-t21-owners/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def", + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/gauge44-barch/PROOF-NOTE-BARCH.md": "c24f211b09358b25d6cf47dd18e4bbd8bcf4ecf279e6f1c6c90613cfa230818d", + "research/complex-double-replica-owners/PROOF.md": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc" + }, + "review": "docs/research/community-frontier890-review.md", + "validation": "docs/research/community-frontier890-integration.json", + "reproduce": "make frontier890-verify", + "scope": "U8/T21 finite composition with complete source-bound baseline coverage; explicit reused ancestry recorded. Inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape, analytic and bit H1-H5 obligations remain. Not a full Lean multiplication theorem; Linux integration CI tracked separately.", + "previous_kappa": "1661634653669567/1000000000000000000", + "previous_record": "certificates/checkpoints/frontier799.json", + "audited_source_head": "4b3bd8cbe8e3e81c44161017c9b72c905a8040a8", + "reviewed_dependency_heads": { + "588": "6d0e53b66c29abd17981881a09eaff41ac862d85", + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90", + "569": "1424da81263a5305b35e4cf74ef686c275f03f3f", + "571": "b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3", + "575": "eac6f7e378ab622dac50a2fd4b7ef6eab014de44", + "583": "89be768f0157f5a3d8e4db69cf1748768605eac9", + "586": "4846fee5b06af770e9b3a10c36200f673d656725", + "591": "f622547244bf6d895a571a7b035142ba66279806", + "592": "1f471c445c06a45a32e2c47e8d74c8264b68356b", + "593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4", + "596": "7732dd5e46863ff294b5e443661cb9d99abf4e01", + "599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32", + "601": "529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550", + "604": "1b795c5d7dea746ba310572585c0ef067574b4a6", + "615": "bf8a49a34350599763cced8592db81dc62c2c1c0", + "617": "904d62855723c00f8acef9a287a10768598fdeb2", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "741": "e516b1463606840a15f80aac1995d64ce0092e89", + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60", + "858": "ae2e25fee91540c83ceee5a60e3b07422ce21c7d", + "869": "73e86f69bf9a391e3c334999f7bbe3825dc42759", + "870": "b734850dc348800942f0ffd1f0723fdec7539b2b", + "890": "4b3bd8cbe8e3e81c44161017c9b72c905a8040a8" + } +} diff --git a/research/t21-binomial-audit/test_package.py b/research/t21-binomial-audit/test_package.py new file mode 100644 index 0000000000..6ae5235bcc --- /dev/null +++ b/research/t21-binomial-audit/test_package.py @@ -0,0 +1,104 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Disposable on-disk mutation tests, preserving the original package.""" +from pathlib import Path +import hashlib +import json +import runpy +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def run(package, cwd, *arguments): + return subprocess.run( + [sys.executable, '-I', '-O', '-B', str(package/'verify.py'), *arguments], + cwd=cwd, capture_output=True, text=True, timeout=60) + + +def main(): + completed = 0 + mutations = ( + ('inputs/ASSEMBLY.json', '1664724476433282815289', '1664724476433282815290', + 'Pinned input changed: inputs/ASSEMBLY.json'), + ('inputs/selected-result.json', '1661957774647029', '1661957774647030', + 'Pinned input changed: inputs/selected-result.json'), + ('inputs/CLAIM.json', '"calls": 189', '"calls": 188', + 'Pinned input changed: inputs/CLAIM.json'), + ('inputs/PROOF.md', '1366848', '1366849', + 'Pinned input changed: inputs/PROOF.md'), + ('CERTIFICATE.json', 'PASS_T21_BINOMIAL_MOMENT', 'UNVERIFIED', + 'Recorded certificate differs from fresh independent computation'), + ('verify.py', 'Q(su + tail, D)', 'Q(su, D)', 'Algebraic enclosure failed'), + ('verify.py', 'nu = ceil_div(tu * numerator, denominator)', + 'nu = tu * numerator // denominator', 'Algebraic enclosure failed'), + ('verify.py', 'Q(32*m*sum(profile.values()), 10**16*live)', + 'Q(31*m*sum(profile.values()), 10**16*live)', + 'Claimed successor does not have a strict rejection certificate'), + ) + with tempfile.TemporaryDirectory(prefix='t21-binomial-controls-') as temporary: + root = Path(temporary) + pristine = root/'relocated' + shutil.copytree(HERE, pristine, ignore=shutil.ignore_patterns('__pycache__')) + ok = run(pristine, root) + if ok.returncode != 0 or 'PASS_T21_BINOMIAL_MOMENT' not in ok.stdout: + raise RuntimeError('Relocated optimized positive failed: '+ok.stderr) + certificate = (pristine/'CERTIFICATE.json').read_bytes() + regenerated = run(pristine, root, '--write-certificate') + if regenerated.returncode != 0 or (pristine/'CERTIFICATE.json').read_bytes() != certificate: + raise RuntimeError('Exact certificate regeneration failed: '+regenerated.stderr) + for number, (name, before, after, expected_error) in enumerate(mutations): + package = root/str(number) + shutil.copytree(pristine, package) + path = package/name + text = path.read_text() + if before not in text: + raise RuntimeError('Mutation target missing: '+name) + path.write_text(text.replace(before, after, 1)) + before_certificate = (package/'CERTIFICATE.json').read_bytes() + # Code defects must fail their mathematical checks even when allowed + # to regenerate the receipt; a stale-certificate mismatch is insufficient. + arguments = ('--write-certificate',) if name == 'verify.py' else () + bad = run(package, root, *arguments) + if bad.returncode == 0 or 'ValueError: '+expected_error not in bad.stderr: + raise RuntimeError('Mutation missed its expected rejection: '+name+'\n'+bad.stderr) + if (package/'CERTIFICATE.json').read_bytes() != before_certificate: + raise RuntimeError('Rejected run overwrote the certificate: '+name) + completed += 1 + # Exercise optional repository comparisons offline. The four input + # copies are real; the separately pinned reference is a synthetic fixture. + check_repository = runpy.run_path(str(pristine/'verify.py'))['repository_bindings'] + pins = json.loads((pristine/'SOURCES.json').read_text()) + repository = root/'repository-fixture' + for local, remote in pins['provenance'].items(): + destination = repository/remote + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(pristine/local, destination) + reference = repository/'reference.txt' + reference.write_bytes(b'Independent source reference fixture\n') + pins['references'] = {'reference.txt':hashlib.sha256(reference.read_bytes()).hexdigest()} + if check_repository(repository, pins) != 5: + raise RuntimeError('Repository binding positive failed') + reference.write_bytes(b'Changed reference\n') + for remove, expected_error in ( + (False, 'Repository source changed: reference.txt'), + (True, 'Missing repository source: reference.txt')): + if remove: + reference.unlink() + try: + check_repository(repository, pins) + except ValueError as error: + if str(error) != expected_error: + raise RuntimeError('Unexpected repository rejection: '+str(error)) from error + else: + raise RuntimeError('Changed repository reference accepted') + completed += 1 + print('PASS_T21_BINOMIAL_PACKAGE controls='+str(completed)+ + ' relocated_optimized=PASS regeneration=PASS failure_preserves_certificate=PASS') + + +if __name__ == '__main__': + main() diff --git a/research/t21-binomial-audit/verify.py b/research/t21-binomial-audit/verify.py new file mode 100644 index 0000000000..2b29eeaaac --- /dev/null +++ b/research/t21-binomial-audit/verify.py @@ -0,0 +1,252 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent T21 recurrence audit using positive binomial series. + +Prepared for David Breslauer with substantial OpenAI Codex assistance. +No production arithmetic, logarithm or exponential implementation is imported. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +D = 1 << 240 +TAIL_LIMIT = 1 << 70 # At most 2^-170 per power factor. + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def ceil_div(n, d): + return -(-n // d) + + +def power_interval(r, m, a): + """Enclose (m/r)^a for 0 <= a <= 1, with exact integer arithmetic. + + t_0 = 1; t_(k+1) = t_k * (a+k)/(k+1) * (1-r/m). + Subsequent exact ratios are at most x = 1-r/m, hence the tail + after t_k is at most t_(k+1)/(1-x). Each recurrence operation is + rounded outward on the fixed dyadic lattice with denominator D. + """ + require(type(r) is int and type(m) is int and 0 < r <= m, 'Invalid rank or arity') + require(isinstance(a, Q) and 0 <= a <= 1, 'Saving must be a rational in [0,1]') + if a == 0 or r == m: + return Q(1), Q(1), 0 + p, q = a.numerator, a.denominator + tl = tu = sl = su = D + for k in range(20000): + numerator = (p + k*q) * (m-r) + denominator = q * (k+1) * m + nl = tl * numerator // denominator + nu = ceil_div(tu * numerator, denominator) + tail = ceil_div(nu * m, r) + if tail <= TAIL_LIMIT: + return Q(sl, D), Q(su + tail, D), k+1 + tl, tu = nl, nu + sl, su = sl + tl, su + tu + raise ValueError('Series did not reach the prescribed tail bound') + + +def moment(profile, m, live, a, surcharge=False): + require(type(live) is int and live > 0, 'Invalid live stock') + require(type(m) is int and m > 1 and profile, 'Invalid arity or empty profile') + lower = upper = Q(0) + terms = {} + for r, count in sorted(profile.items()): + require(type(r) is int and type(count) is int and 0 < r < m and count > 0, + 'Invalid child rank or multiplicity') + l, u, steps = power_interval(r, m, a) + weight = Q(r*count, m*live) + lower += weight*l + upper += weight*u + terms[str(r)] = steps + if surcharge: + l, u, steps = power_interval(1, m, a) + weight = Q(32*m*sum(profile.values()), 10**16*live) + lower += weight*l + upper += weight*u + terms['fallback'] = steps + return lower, upper, terms + + +def brackets(profile, m, live, endpoint, surcharge): + lower = moment(profile, m, live, endpoint, surcharge) + upper = moment(profile, m, live, endpoint + Q(1, 10**24), surcharge) + require(lower[1] < 1, 'Claimed lower endpoint does not have a strict acceptance certificate') + require(upper[0] > 1, 'Claimed successor does not have a strict rejection certificate') + return { + 'endpoint': str(endpoint), + 'successor': str(endpoint + Q(1, 10**24)), + 'lower_residual_interval': [str(x-1) for x in lower[:2]], + 'successor_residual_interval': [str(x-1) for x in upper[:2]], + 'terms': lower[2], + } + + +def controls(profile, endpoint, conservative): + count = 0 + # Exact algebraic comparison for rational exponents p/q: + # L^q <= (m/r)^p <= U^q, with no floating-point reference. + for m in (2, 3, 5, 7, 73): + for r in range(1, m+1): + for a in (Q(0), Q(1, 3), Q(1, 2), Q(2, 3), Q(1)): + l, u, _ = power_interval(r, m, a) + exact = Q(m, r)**a.numerator + require(l**a.denominator <= exact <= u**a.denominator, 'Algebraic enclosure failed') + count += 1 + require(moment(profile, 73, 18816, Q(0))[:2] == + (Q(1366848, 73*18816), Q(1366848, 73*18816)), 'Zero-saving mass identity failed') + # Underpricing controls: a removed child and dropped exceptional fallback + # wrongly admit the next saving tick. These are deliberately changed + # models, not defects alleged against the selected production checker. + omitted = dict(profile) + omitted[48] -= 1 + require(moment(omitted, 73, 18816, endpoint + Q(1, 10**24))[1] < 1, + 'Omitted child control failed') + require(moment(profile, 73, 18816, conservative + Q(1, 10**24))[1] < 1, + 'Dropped conservative surcharge control failed') + wrong_stock = moment(profile, 73, 19330, endpoint + Q(1, 10**24)) + require(wrong_stock[1] < 1, 'Physical-stock normalization control failed') + # Same rank mass AND same child count; strict concavity still changes + # the numerical price. Replace two rank-48 children by ranks 47 and 49. + redistributed = dict(profile) + redistributed[48] -= 2 + redistributed[47] = redistributed[49] = 1 + require(sum(redistributed.values()) == sum(profile.values()) and + sum(r*c for r,c in redistributed.items()) == 1366848, 'Control mass changed') + original = moment(profile, 73, 18816, endpoint) + changed = moment(redistributed, 73, 18816, endpoint) + require(changed[1] < original[0], 'Mass-preserving redistribution not distinguished') + rejection_count = 0 + for args in ((0, 73, Q(1,2)), (74,73,Q(1,2)), (1,0,Q(1,2)), + (1,73,Q(-1,2)), (1,73,Q(3,2)), (True,73,Q(1,2))): + try: + power_interval(*args) + except ValueError: + rejection_count += 1 + else: + raise ValueError('Invalid enclosure input accepted') + for bad in ({1:0}, {73:1}, {1:True}, {1:-1}, {}): + try: + moment(bad, 73, 18816, endpoint) + except ValueError: + rejection_count += 1 + else: + raise ValueError('Invalid profile accepted') + return {'algebraic_comparisons':count, 'mathematical_controls':5, + 'rejected_inputs':rejection_count, + 'redistributed_minus_original_interval': + [str(changed[0]-original[1]),str(changed[1]-original[0])]} + + +def repository_bindings(root, pins): + """Compare source bytes without importing or executing supplier code.""" + root = root.resolve() + sources = {remote: pins['files'][local] + for local, remote in pins['provenance'].items()} + sources.update(pins['references']) + for relative, expected in sources.items(): + path = (root/relative).resolve() + require(path.is_relative_to(root) and path.is_file(), + 'Missing repository source: '+relative) + require(hashlib.sha256(path.read_bytes()).hexdigest() == expected, + 'Repository source changed: '+relative) + return len(sources) + + +def audit(repository=None): + pins = json.loads((HERE/'SOURCES.json').read_text()) + required = {'inputs/ASSEMBLY.json', 'inputs/selected-result.json', + 'inputs/CLAIM.json', 'inputs/PROOF.md'} + require(set(pins['files']) == set(pins['provenance']) == required, + 'Incomplete pinned source inventory') + for name, expected in pins['files'].items(): + require(hashlib.sha256((HERE/name).read_bytes()).hexdigest() == expected, + 'Pinned input changed: '+name) + if repository is not None: + checked = repository_bindings(repository, pins) + print('PASS_T21_REPOSITORY_BINDINGS files='+str(checked)) + assembly = json.loads((HERE/'inputs/ASSEMBLY.json').read_text()) + selected = json.loads((HERE/'inputs/selected-result.json').read_text()) + claim = json.loads((HERE/'inputs/CLAIM.json').read_text()) + require(hashlib.sha256((HERE/'inputs/ASSEMBLY.json').read_bytes()).hexdigest() == + selected['certificate_sha256'], 'Selected certificate binding changed') + require(pins['files']['inputs/PROOF.md'] == + selected['proof_supplements'][pins['provenance']['inputs/PROOF.md']], + 'Selected proof binding changed') + require(Q(selected['kappa']) == Q(assembly['kappa']), 'Selection and assembly disagree') + require(Q(claim['kappa']) == Q(assembly['kappa']) and + Q(claim['complex_lower']) == Q(assembly['complex_lower']), + 'Construction claim and assembly disagree') + for engine in ('moment.py', 'base_two_moment.py'): + source = 'research/complex-k492-owner-repair/vendor/multicold/engines/'+engine + require(pins['references'][source] == assembly['input_sha256']['engines/'+engine], + 'Assembly arithmetic source binding changed: '+engine) + replicas, m = 21, 73 + calls, live = 9*replicas, 8*112*replicas + physical = live+504+8+2 + require(assembly['provider_counts'] == {'gauge44':calls}, 'Assembly call count') + local = Counter({1:2548,2:338,3:446,4:162,5:72,8:8}) + idle = {48:6292,3:1,1:3} + require({int(r):c for r,c in claim['local_profile'].items()} == dict(local) and + {int(r):c for r,c in claim['idle'].items()} == idle, + 'Construction claim profiles disagree with the proof accounting') + for name, expected in (('replicas',replicas), ('calls',calls), ('live',live), + ('physical',physical), ('rank_mass',1366848), ('deficit',6720)): + require(type(claim[name]) is int and claim[name] == expected, + 'Construction claim accounting changed: '+name) + derived = Counter({r:c*calls for r,c in local.items()}) + derived.update(idle) + profile = {int(r):c for r,c in assembly['complex_profile'].items()} + require(dict(derived) == profile, 'Local + idle profile does not match committed assembly') + require(sum(profile.values()) == 681782, 'Child count') + require(sum(r*c for r,c in profile.items()) == 1366848, 'Rank mass') + require(m*live - 1366848 == 6720 == replicas*320, 'Deficit') + native = Q(assembly['complex_lower']) + conservative = Q(assembly['conservative_complex_lower']) + result = { + 'status':'PASS_T21_BINOMIAL_MOMENT', + 'base_commit':pins['base_commit'], + 'assignment_seed':69, + 'source_files_sha256':pins['files'], + 'selected_kappa_unchanged':assembly['kappa'], + 'profile':{str(r):c for r,c in sorted(profile.items())}, + 'child_count':681782, 'arity':m, 'live_stock':live, 'physical_stock':physical, + 'rank_mass':1366848, 'deficit':6720, + 'native':brackets(profile,m,live,native,False), + 'conservative':brackets(profile,m,live,conservative,True), + 'controls':controls(profile,native,conservative), + 'scope':'Arithmetic consequence of the pinned T21 paid profile and fallback formula. ' + 'Physical construction, owner windows, invoice, outer 47 inequalities, ' + 'all-size compilation and the multiplication theorem are not replayed or proved.' + } + return result + + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument('--write-certificate', action='store_true') + p.add_argument('--repository', type=Path, + help='Also compare all pinned sources with this repository checkout') + args = p.parse_args() + result = audit(args.repository) + text = json.dumps(result,indent=2,sort_keys=True)+'\n' + path = HERE/'CERTIFICATE.json' + if args.write_certificate: + path.write_text(text) + else: + require(path.read_text() == text, 'Recorded certificate differs from fresh independent computation') + print(result['status'], 'four strict endpoint decisions;', + result['controls']['algebraic_comparisons'], 'algebraic comparisons;', + result['controls']['mathematical_controls'], 'mathematical controls;', + result['controls']['rejected_inputs'], 'rejected inputs.') + + +if __name__ == '__main__': + main()