From 93a8127b990f9755d0c80e729b40c969d6c611e4 Mon Sep 17 00:00:00 2001 From: woklerx <338878655+woklerx@users.noreply.github.com> Date: Tue, 13 Oct 2026 09:05:11 -0700 Subject: [PATCH] Verify the U8 supporting inequality uniformly through exponent one third Extend the pointwise all-replica owner relaxation with an analytic interval proof, two independent exact checkers, a quantitative residual bound, pinned sources, and corruption controls. No new kappa. Prepared with substantial OpenAI Codex assistance. --- .../u8-supporting-uniform/CERTIFICATE.json | 975 ++++++++++++++++++ research/u8-supporting-uniform/CLAIM.json | 43 + research/u8-supporting-uniform/NOTICE.md | 32 + research/u8-supporting-uniform/PROOF.md | 258 +++++ research/u8-supporting-uniform/README.md | 114 ++ research/u8-supporting-uniform/SOURCES.json | 23 + research/u8-supporting-uniform/VALIDATION.md | 45 + .../independent_check.py | 175 ++++ research/u8-supporting-uniform/test_verify.py | 138 +++ research/u8-supporting-uniform/verify.py | 194 ++++ 10 files changed, 1997 insertions(+) create mode 100644 research/u8-supporting-uniform/CERTIFICATE.json create mode 100644 research/u8-supporting-uniform/CLAIM.json create mode 100644 research/u8-supporting-uniform/NOTICE.md create mode 100644 research/u8-supporting-uniform/PROOF.md create mode 100644 research/u8-supporting-uniform/README.md create mode 100644 research/u8-supporting-uniform/SOURCES.json create mode 100644 research/u8-supporting-uniform/VALIDATION.md create mode 100644 research/u8-supporting-uniform/independent_check.py create mode 100644 research/u8-supporting-uniform/test_verify.py create mode 100644 research/u8-supporting-uniform/verify.py diff --git a/research/u8-supporting-uniform/CERTIFICATE.json b/research/u8-supporting-uniform/CERTIFICATE.json new file mode 100644 index 0000000000..e1c6f4d286 --- /dev/null +++ b/research/u8-supporting-uniform/CERTIFICATE.json @@ -0,0 +1,975 @@ +{ + "attainable_residuals": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 43, + 44, + 48 + ], + "base_commit": "407d52ff15b2217b6e22bce44728b4c3907b6515", + "cube_root_48_numerators": [ + 3634241185664, + 3634241185665 + ], + "equality_profile": { + "minimum_replicas": 37, + "rank_1": 6, + "rank_48": 11086 + }, + "exponent_interval": "0 < b <= 1/3", + "legal_patterns": 1163, + "legal_patterns_by_capacity": { + "16": 27, + "32": 215, + "48": 915, + "8": 6 + }, + "method": "generating-function census and integer cube-root endpoint bounds", + "per_replica": { + "credit_required": 150, + "residual_mass": 14382, + "signed_price": -3892 + }, + "root_denominator": 1000000000000, + "rows": [ + { + "credit": 0, + "maximizing_bin": { + "capacity": 8, + "counts": [ + 0, + 0, + 0, + 1, + 0 + ] + }, + "rank": 0, + "upper_price": 0 + }, + { + "credit": 925, + "maximizing_bin": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 0, + 3 + ] + }, + "rank": 1, + "upper_price": 19 + }, + { + "credit": 650, + "cube_root_numerators": [ + 2884499140614, + 2884499140615 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 1, + 2 + ] + }, + "rank": 2, + "scaled_margin_lower": "354813327890730/526848237133", + "upper_price": 13 + }, + { + "credit": 375, + "cube_root_numerators": [ + 2519842099789, + 2519842099790 + ], + "maximizing_bin": { + "capacity": 16, + "counts": [ + 1, + 0, + 0, + 0, + 1 + ] + }, + "rank": 3, + "scaled_margin_lower": "645944276458020/526848237133", + "upper_price": 7 + }, + { + "credit": 100, + "cube_root_numerators": [ + 2289428485106, + 2289428485107 + ], + "maximizing_bin": { + "capacity": 8, + "counts": [ + 1, + 0, + 0, + 0, + 0 + ] + }, + "rank": 4, + "scaled_margin_lower": "901492255265140/526848237133", + "upper_price": 1 + }, + { + "credit": 1025, + "cube_root_numerators": [ + 2125317138365, + 2125317138366 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 0, + 3 + ] + }, + "rank": 5, + "scaled_margin_lower": "500898909926300/526848237133", + "upper_price": 20 + }, + { + "credit": 750, + "cube_root_numerators": [ + 2000000000000, + 2000000000001 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 1, + 2 + ] + }, + "rank": 6, + "scaled_margin_lower": "714863822150250/526848237133", + "upper_price": 14 + }, + { + "credit": 475, + "cube_root_numerators": [ + 1899828503185, + 1899828503186 + ], + "maximizing_bin": { + "capacity": 16, + "counts": [ + 0, + 0, + 0, + 0, + 1 + ] + }, + "rank": 7, + "scaled_margin_lower": "915024998986400/526848237133", + "upper_price": 8 + }, + { + "credit": 200, + "cube_root_numerators": [ + 1817120592832, + 1817120592833 + ], + "maximizing_bin": { + "capacity": 8, + "counts": [ + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 8, + "scaled_margin_lower": "1103968829964760/526848237133", + "upper_price": 2 + }, + { + "credit": -75, + "cube_root_numerators": [ + 1747160929472, + 1747160929473 + ], + "maximizing_bin": { + "capacity": 16, + "counts": [ + 0, + 0, + 1, + 0, + 0 + ] + }, + "rank": 9, + "scaled_margin_lower": "1283536565355855/526848237133", + "upper_price": -4 + }, + { + "credit": 850, + "cube_root_numerators": [ + 1686865330603, + 1686865330604 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 0, + 2 + ] + }, + "rank": 10, + "scaled_margin_lower": "822879860052500/526848237133", + "upper_price": 15 + }, + { + "credit": 575, + "cube_root_numerators": [ + 1634115881286, + 1634115881287 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 1, + 1 + ] + }, + "rank": 11, + "scaled_margin_lower": "987488082065535/526848237133", + "upper_price": 9 + }, + { + "credit": 300, + "cube_root_numerators": [ + 1587401051968, + 1587401051969 + ], + "maximizing_bin": { + "capacity": 16, + "counts": [ + 1, + 0, + 0, + 0, + 0 + ] + }, + "rank": 12, + "scaled_margin_lower": "1145975864229060/526848237133", + "upper_price": 3 + }, + { + "credit": 25, + "cube_root_numerators": [ + 1545607779548, + 1545607779549 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 1, + 0, + 1, + 1, + 0 + ] + }, + "rank": 13, + "scaled_margin_lower": "1299015503884615/526848237133", + "upper_price": -3 + }, + { + "credit": 950, + "cube_root_numerators": [ + 1507894882258, + 1507894882259 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 0, + 2 + ] + }, + "rank": 14, + "scaled_margin_lower": "814941919771870/526848237133", + "upper_price": 16 + }, + { + "credit": 675, + "cube_root_numerators": [ + 1473612599456, + 1473612599457 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 1, + 1 + ] + }, + "rank": 15, + "scaled_margin_lower": "958652403425625/526848237133", + "upper_price": 10 + }, + { + "credit": 400, + "cube_root_numerators": [ + 1442249570307, + 1442249570308 + ], + "maximizing_bin": { + "capacity": 16, + "counts": [ + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 16, + "scaled_margin_lower": "1098319433255520/526848237133", + "upper_price": 4 + }, + { + "credit": 125, + "cube_root_numerators": [ + 1413396805261, + 1413396805262 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 0, + 1, + 1, + 0 + ] + }, + "rank": 17, + "scaled_margin_lower": "1234276922904220/526848237133", + "upper_price": -2 + }, + { + "credit": -150, + "cube_root_numerators": [ + 1386722548701, + 1386722548702 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 0, + 2, + 0, + 0 + ] + }, + "rank": 18, + "scaled_margin_lower": "1366813322744280/526848237133", + "upper_price": -8 + }, + { + "credit": 775, + "cube_root_numerators": [ + 1361954332251, + 1361954332252 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 0, + 1 + ] + }, + "rank": 19, + "scaled_margin_lower": "863962094084190/526848237133", + "upper_price": 11 + }, + { + "credit": 500, + "cube_root_numerators": [ + 1338865900164, + 1338865900165 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 1, + 0 + ] + }, + "rank": 20, + "scaled_margin_lower": "990379712040300/526848237133", + "upper_price": 5 + }, + { + "credit": 225, + "cube_root_numerators": [ + 1317267512016, + 1317267512017 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 1, + 0, + 1, + 0, + 0 + ] + }, + "rank": 21, + "scaled_margin_lower": "1114043430827235/526848237133", + "upper_price": -1 + }, + { + "credit": -50, + "cube_root_numerators": [ + 1296998634496, + 1296998634497 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 1, + 2 + ] + }, + "rank": 22, + "scaled_margin_lower": "1235126854255370/526848237133", + "upper_price": -7 + }, + { + "credit": 875, + "cube_root_numerators": [ + 1277922354108, + 1277922354109 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 0, + 1 + ] + }, + "rank": 23, + "scaled_margin_lower": "721567409238165/526848237133", + "upper_price": 12 + }, + { + "credit": 600, + "cube_root_numerators": [ + 1259921049894, + 1259921049895 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 1, + 0 + ] + }, + "rank": 24, + "scaled_margin_lower": "837940519249560/526848237133", + "upper_price": 6 + }, + { + "credit": 325, + "cube_root_numerators": [ + 1242893002381, + 1242893002382 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 0, + 1, + 0, + 0 + ] + }, + "rank": 25, + "scaled_margin_lower": "952154458943900/526848237133", + "upper_price": 0 + }, + { + "credit": 50, + "cube_root_numerators": [ + 1226749707593, + 1226749707594 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 1, + 0, + 0, + 0, + 2 + ] + }, + "rank": 26, + "scaled_margin_lower": "1064323681665680/526848237133", + "upper_price": -6 + }, + { + "credit": -225, + "cube_root_numerators": [ + 1211413728554, + 1211413728555 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 1, + 0, + 0, + 0 + ] + }, + "rank": 27, + "scaled_margin_lower": "1174552427482155/526848237133", + "upper_price": -12 + }, + { + "credit": 700, + "cube_root_numerators": [ + 1196816961177, + 1196816961178 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 1, + 0, + 0, + 0, + 0 + ] + }, + "rank": 28, + "scaled_margin_lower": "650718092903760/526848237133", + "upper_price": 7 + }, + { + "credit": -775, + "cube_root_numerators": [ + 1182899222918, + 1182899222919 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 1, + 0, + 1, + 1, + 0 + ] + }, + "rank": 29, + "scaled_margin_lower": "1389561714733145/526848237133", + "upper_price": -24 + }, + { + "credit": 150, + "cube_root_numerators": [ + 1169607095285, + 1169607095286 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 0, + 2 + ] + }, + "rank": 30, + "scaled_margin_lower": "862292143261800/526848237133", + "upper_price": -5 + }, + { + "credit": -125, + "cube_root_numerators": [ + 1156892967713, + 1156892967714 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 1, + 1 + ] + }, + "rank": 31, + "scaled_margin_lower": "965637199475680/526848237133", + "upper_price": -11 + }, + { + "credit": 800, + "cube_root_numerators": [ + 1144714242553, + 1144714242554 + ], + "maximizing_bin": { + "capacity": 32, + "counts": [ + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 32, + "scaled_margin_lower": "435229726207360/526848237133", + "upper_price": 8 + }, + { + "credit": -675, + "cube_root_numerators": [ + 1133032669885, + 1133032669886 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 0, + 1, + 1, + 0 + ] + }, + "rank": 33, + "scaled_margin_lower": "1167787009712700/526848237133", + "upper_price": -23 + }, + { + "credit": -950, + "cube_root_numerators": [ + 1121813787760, + 1121813787761 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 0, + 2, + 0, + 0 + ] + }, + "rank": 34, + "scaled_margin_lower": "1266714550286750/526848237133", + "upper_price": -29 + }, + { + "credit": -25, + "cube_root_numerators": [ + 1111026448575, + 1111026448576 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 1, + 0, + 0, + 0, + 1 + ] + }, + "rank": 35, + "scaled_margin_lower": "732067460451450/526848237133", + "upper_price": -10 + }, + { + "credit": -300, + "cube_root_numerators": [ + 1100642416298, + 1100642416299 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 1, + 0, + 0, + 1, + 0 + ] + }, + "rank": 36, + "scaled_margin_lower": "828332963684580/526848237133", + "upper_price": -16 + }, + { + "credit": -575, + "cube_root_numerators": [ + 1090636022289, + 1090636022290 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 1, + 0, + 1, + 0, + 0 + ] + }, + "rank": 37, + "scaled_margin_lower": "923341308919680/526848237133", + "upper_price": -22 + }, + { + "credit": -2050, + "cube_root_numerators": [ + 1080983869874, + 1080983869875 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 2, + 0, + 0, + 0 + ] + }, + "rank": 38, + "scaled_margin_lower": "1649355491336870/526848237133", + "upper_price": -53 + }, + { + "credit": 75, + "cube_root_numerators": [ + 1071664579674, + 1071664579675 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 0, + 1 + ] + }, + "rank": 39, + "scaled_margin_lower": "477546324562935/526848237133", + "upper_price": -9 + }, + { + "credit": -200, + "cube_root_numerators": [ + 1062658569182, + 1062658569183 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 1, + 0 + ] + }, + "rank": 40, + "scaled_margin_lower": "569043059373400/526848237133", + "upper_price": -15 + }, + { + "credit": -475, + "cube_root_numerators": [ + 1053947861260, + 1053947861261 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 0, + 1, + 0, + 0 + ] + }, + "rank": 41, + "scaled_margin_lower": "659447440295275/526848237133", + "upper_price": -21 + }, + { + "credit": -1025, + "cube_root_numerators": [ + 1037347490357, + 1037347490358 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 1, + 0, + 0, + 0 + ] + }, + "rank": 43, + "scaled_margin_lower": "837118728851260/526848237133", + "upper_price": -33 + }, + { + "credit": -100, + "cube_root_numerators": [ + 1029428498400, + 1029428498401 + ], + "maximizing_bin": { + "capacity": 48, + "counts": [ + 1, + 0, + 0, + 0, + 0 + ] + }, + "rank": 44, + "scaled_margin_lower": "292232800689300/526848237133", + "upper_price": -14 + }, + { + "credit": 0, + "maximizing_bin": { + "capacity": 48, + "counts": [ + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 48, + "upper_price": -13 + } + ], + "scope": "Exact finite endpoint certificate plus a written continuum proof; fixed whole-helper ledger only. No owner feasibility, outer assembly, new kappa, or full multiplication theorem is certified.", + "scope_counterexample": { + "exponent": "1", + "rank": 32, + "scaled_margin": "-22800/47" + }, + "status": "PASS_U8_SUPPORTING_UNIFORM", + "strict_ranks_checked": 42, + "support": { + "minimum_scaled_margin_lower": "292232800689300/526848237133", + "rank_one_credit": 925, + "scaled_uniform_margin": 554, + "worst_endpoint_rank": 44 + } +} diff --git a/research/u8-supporting-uniform/CLAIM.json b/research/u8-supporting-uniform/CLAIM.json new file mode 100644 index 0000000000..6d0a2a96f4 --- /dev/null +++ b/research/u8-supporting-uniform/CLAIM.json @@ -0,0 +1,43 @@ +{ + "track": "Independent verification or formalization", + "assignment_seed": 77, + "seed_source": "System.Security.Cryptography.RandomNumberGenerator; rejection sampling of UInt32 below 4294967200, modulo 100", + "base_commit": "407d52ff15b2217b6e22bce44728b4c3907b6515", + "claimed_at_utc": "2026-10-13T15:50:00Z", + "expected_finish_utc": "2026-10-13T16:24:00Z", + "candidate_tasks": [ + "Independent nullspace check of PR845 fixed-coordinate reader obstruction", + "Independent algebraic replay of historical phase identity (overlaps PR712/PR948)", + "Uniform verification of U8 signed-bin supporting inequality over 0 < b <= 1/3" + ], + "selection": "77 modulo 3 = 2 selects candidate index 2; inspection found existing pointwise T37 proof and a different fixed-72-call SW4/X4 continuum result, but no U8 all-replica continuum verification", + "object": "c_b(r) >= c_b(1)*(48*u(r)+13*r)/925 for every attainable residual rank and every real 0 < b <= 1/3", + "method": "Independent finite generating-function bin census; analytic monotonic ratio reduction; exact integer cube-root enclosures at b=1/3; adversarial negative controls", + "expected_deliverable": "Standalone standard-library verifier, exact certificate, interval proof, pinned sources, scoped handoff; no new kappa", + "coordination": "Public issue listing on 2026-10-13 shows issues #913 and #650 and no pinned sprint coordination issue. Claim recorded locally; no reservation issue opened.", + "overlap_checks": [ + "Read CONTRIBUTING.md, selected-result.json, current-status.md, pr-ledger.md and community-batch952-review.md at base", + "Read actual complex-t37-owners/PROOF.md and ALL-T-PROOF.md and complex-t21-owner-bound/PROOF.md", + "Curiosity Bot github/issues queries for open verification, owner bound, bin prices, generating function, partition; U8 uniform search returns no records", + "PR795/PR890 signed prices and PR942 pointwise all-T bound are predecessors; PR850 fixed-72-call SW4/X4 uniform owner optimum is distinct" + ], + "delegation": "One read-only worker independently checks the ratio proof and fixed-family overlap; stays within the chosen inequality.", + "status": "completed locally; verified independent research package ready for focused PR", + "completed_coverage": { + "legal_bin_patterns": 1163, + "attainable_residual_ranks": 45, + "strict_endpoint_inequalities": 42, + "real_exponent_interval": "0 < b <= 1/3 via written monotonicity proof", + "replica_domain": "all positive integer T via ledger argument" + }, + "result": "Uniform scaled margin >554; quantitative residual-count bound; equality profile requires37 dividing T; no new kappa.", + "final_overlap_check": { + "utc": "2026-10-13T16:02:00Z", + "upstream_head": "8bddbee377e2f3ce1f1247196c4b290d55767d20", + "queries": [ + "repo:CrocSwap/integer-mult-bounds is:pr (U8 uniform)", + "repo:CrocSwap/integer-mult-bounds is:pr (supporting inequality OR supporting line OR quantitative residual)" + ], + "results": "First query returned no records; second returned predecessor PR942 only. PR850 and concurrent PR962 inspected separately. All five pinned source inputs unchanged at refreshed upstream." + } +} diff --git a/research/u8-supporting-uniform/NOTICE.md b/research/u8-supporting-uniform/NOTICE.md new file mode 100644 index 0000000000..54fb2b04db --- /dev/null +++ b/research/u8-supporting-uniform/NOTICE.md @@ -0,0 +1,32 @@ +# Attribution and license + +Prepared for **@woklerx** with substantial **OpenAI Codex assistance** in +mathematics, implementation, independent computational checking, tests, and +writing. Two delegated Codex workers stayed within the supporting-inequality +scope: one checked the mathematics and wrote the proof and independent checker; +another reviewed the proof and implementations. No independent human peer +review or proof-assistant verification is claimed. + +New files in this directory are contributed under the repository's +**Apache-2.0** license. No upstream source or predecessor notice is replaced. + +- **Chafik Boukhalfa (@chafreaky), PR795 and PR890:** signed helper prices, + capacity bonuses, fixed-family inventory, and owner-relaxation ledger. +- **Jonathan Capalbo (@jon314159), PR942:** the pointwise supporting inequality, + formal T37 equality profile, all-replica bound, and separately verified T37 + owner construction. This package extends the inequality to a real interval; + it does not repeat the owner construction or claim its kappa improvement. +- **Charles Bethin (@cbethin), PR850:** the earlier continuum result for the + fixed 72-call (T=8) integer owner optimum. Its stronger fixed-T conclusion + remains distinct from this package's all-T fractional envelope. +- **Joel Pulikkan (@GamingPuzzled), concurrent PR962:** independent T37 owner + reconstruction inspected for overlap. This package does not consume its code + or depend on its pending review status. +- The retained U8/T16/T21 family credits **Jeremy Kothe, Hao Yan, icekylinx, + NewBArch**, and the earlier controller, supplier, and arithmetic contributors + identified in `research/complex-t37-owners/NOTICE.md`. Their construction + results are inherited context, not newly reproduced evidence here. + +Source bytes and relevant dependency heads are recorded in `SOURCES.json`. +The two new checkers use only the Python standard library and import neither +the predecessor arithmetic engines nor one another. diff --git a/research/u8-supporting-uniform/PROOF.md b/research/u8-supporting-uniform/PROOF.md new file mode 100644 index 0000000000..f56bfa624b --- /dev/null +++ b/research/u8-supporting-uniform/PROOF.md @@ -0,0 +1,258 @@ +# A uniform supporting inequality for the U8 owner relaxation + +This is an independently checkable extension of the pointwise signed-dual +argument in `research/complex-t37-owners/ALL-T-PROOF.md` (PR942). For every real +`0 < b <= 1/3`, the same formal residual profile is a lower bound on the idle +moment for every positive integer replica count. A quantitative inequality +also bounds the number of positive residuals having ranks other than 1 or 48. +This result supplies no new kappa, owner construction, or unconditional +multiplication theorem. + +## Model and inherited ledger + +One replica has nine calls. Each call supplies whole helpers of widths +`(4,5,7,8,9)` with multiplicities `(80,32,54,122,216)`. The bin inventory per +replica consists of 672 capacity-8 bins and 448 bins of each capacity 16, 32, +and 48. A helper occupies its complete width in one bin. The residual rank of +a bin is its unused capacity. Timing, identities, owner geometry, and execution +constraints are relaxed. + +The signed helper prices and bin bonuses are inherited from chafreaky's PR795 +and PR890: + +``` +width: 4 5 7 8 9 +price: -1 -20 -8 -2 4 + +capacity: 8 16 32 48 +bonus: 2 4 8 -13 +``` + +For each attainable residual rank r, let u(r) be the maximum bonus plus helper +price among legal fills leaving r. Enumeration gives 1,163 legal width-count +vectors over the four capacities, with attainable ranks + +``` +0,1,...,41,43,44,48. +``` + +In particular, `u(0)=0`, `u(1)=19`, and `u(48)=-13`. Let +`v(r)=48*u(r)+13*r`; thus `v(0)=v(48)=0` and `v(1)=925`. + +For T replicas, write n_r for the number of bins with residual rank r. +The inventory fixes the residual mass and actual signed price: + +``` +sum r*n_r = 14382*T, +sum u(r)*n_r >= -3892*T. +``` + +The second inequality follows because u(r) bounds each actual bin's signed +price from above. Combining these two statements gives + +``` +C := sum v(r)*n_r >= 150*T. +``` + +The count of rank-zero bins does not affect these inequalities or the moment. +The theorem below also applies directly to nonnegative real n_r satisfying +these ledger constraints; actual whole-helper packings form a smaller class. + +## Monotonicity reduces the continuum to one algebraic endpoint + +For b>0, define + +``` +phi_b(r) = r*(73/r)^b (r>0), +c_b(r) = 48*phi_b(r)-r*phi_b(48), +q_b(r) = c_b(r)/c_b(1) + = r*((48/r)^b-1)/(48^b-1) (00, the function `h_b(x)=x/(1-exp(-b*x))` is strictly increasing +on x>0. Its derivative has the sign of + +``` +1-(1+b*x)*exp(-b*x), +``` + +which is positive because `exp(t)>1+t` for t>0. Thus q_b(r) is strictly +decreasing in b whenever 1= q_(1/3)(r) for 0 554/925. (1) +``` + +Here is the exact integer recipe reproduced by `independent_check.py` for +checking (1). The primary verifier uses the equivalent expression +`r*(cuberoot(48/r)-1)/(cuberoot(48)-1)` and stores its rational lower bounds +in `CERTIFICATE.json`. Neither checker imports the other or a retained moment +engine. Set `D=10^12`, and define + +``` +A = 3634241185665, +L_r = floor(cuberoot(48*r^2*D^3)). +``` + +Check the integer cube inequalities + +``` +(A-1)^3 <= 48*D^3 < A^3, +L_r^3 <= 48*r^2*D^3 < (L_r+1)^3. +``` + +Then `cuberoot(48)=L_r/D`. Each +`L_r-r*D` is positive, so + +``` +q_(1/3)(r) > (L_r-r*D)/(A-D). +``` + +For every relevant rank, the certificate verifies the strictly positive integer + +``` +E_r = 925*(L_r-r*D)-(v(r)+554)*(A-D). +``` + +The least such integer is + +``` +E_44 = 1794386594565 > 0. +``` + +Therefore (1) follows by division by the positive integer `925*(A-D)`. +This calculation treats negative v(r) correctly: v(r) is subtracted exactly, +and no signed coefficient is multiplied by an incorrectly directed interval. + +Combining (1) with monotonicity proves, uniformly for 0 ((v(r)+554)/925)*c_b(1) + for every attainable r other than 0,1,48. (2) +``` + +At r=48 both the excess cost and v are zero. Rank zero contributes zero by +definition. Thus the unstrengthened supporting inequality +`c_b(r)>=v(r)*c_b(1)/925` holds at every rank, with equality only at 0, 1, +and 48. + +## The all-replica lower envelope and quantitative residual bound + +Let `K=sum_(r not in {0,1,48}) n_r`. Sum (2), using its weaker non-strict +version, and use the definition of C: + +``` +sum c_b(r)*n_r >= (c_b(1)/925)*(C+554*K). +``` + +The mass identity gives + +``` +sum phi_b(r)*n_r + = (14382*T/48)*phi_b(48) + (1/48)*sum c_b(r)*n_r. +``` + +Define the formal lower envelope + +``` +F_b(T) = (T/37)*(6*phi_b(1)+11086*phi_b(48)). +``` + +The coefficients have total residual mass `14382*T`, and their credit is +`150*T`, since `925*(6/37)=150`. Subtraction yields the quantitative bound + +``` +sum phi_b(r)*n_r - F_b(T) + >= c_b(1)/(48*925) * (C-150*T+554*K) + >= (554*c_b(1)/(48*925))*K. (3) +``` + +In particular, F_b(T) is a lower bound for every positive integer T, uniformly +on the entire stated exponent interval. If an idle moment is at most +`F_b(T)+epsilon` for epsilon>=0, then (3) gives + +``` +K <= 48*925*epsilon/(554*c_b(1)). +``` + +The analogous per-replica estimate is obtained by dividing both epsilon and K +by T. This is a bound in the unnormalized idle moment; a complete normalized +moment has its own positive normalization factor. + +Equality with F_b(T) requires K=0 and C=150*T. The only positive residual +ranks are then 1 and 48, and the ledger equations force + +``` +n_1 = 6*T/37, +n_48 = 11086*T/37. +``` + +Conversely, these residual counts attain equality in this relaxation. For +integer counts and positive integer T, equality therefore requires T to be +a positive multiple of 37. This divisibility condition and these formal +counts do not by themselves establish a realizable owner assignment. + +Any fixed local paid profile adds the same moment contribution to every +owner assignment being compared. A positive normalization also preserves +the inequality. Hence this idle lower envelope transfers to those moment +comparisons, without certifying any changed local circuit or full recurrence. + +## Relationship to the earlier results and limits + +PR795 and PR890 supply the signed prices, bonuses, and fixed inventory +ledger. PR942's retained `ALL-T-PROOF.md` establishes the rank-one supporting +inequality at one certified saving endpoint and derives the all-T relaxation +bound there. The present result verifies that supporting inequality over the +whole interval 0 554/925 (0 < b <= 1/3). +``` + +The formal idle lower bound for every positive replica count T is +`(T/37)*(6*phi_b(1)+11086*phi_b(48))`. Equality in the integer relaxation +requires `37 | T`; this is not an owner-feasibility certificate. The proof also +bounds the number of other positive residuals in any near-equality profile. + +## Reproduce + +From the repository root, with Python 3.10+ and a writable temporary directory: + +```sh +python -B research/u8-supporting-uniform/test_verify.py +``` + +Expected: **8 tests, OK**. This runs both standalone checks under `-O -S -B`, +checks the inherited literal model without executing it, and rejects nine +corrupted mathematical certificates plus a changed pinned source. Each +certificate control must fail for its expected reason, not an earlier error. +There are no third-party dependencies or network requests. + +The two standalone commands are: + +```sh +python -B research/u8-supporting-uniform/verify.py +python -B research/u8-supporting-uniform/independent_check.py +``` + +Expected output starts with `PASS_U8_SUPPORTING_UNIFORM` and +`PASS_U8_SUPPORTING_INDEPENDENT`, respectively. Regenerate to a **new** file: + +```sh +python -B research/u8-supporting-uniform/verify.py --write /path/to/new-certificate.json +``` + +The output must equal [CERTIFICATE.json](CERTIFICATE.json) byte for byte. +Sources use exact committed-byte SHA-256 pins, so clone with +`git -c core.autocrlf=false clone ...` on Windows. The moving selected-result +pointer is recorded only as context at the base; it is not a runtime dependency. + +## Evidence and independence + +- `verify.py` multiplies a finite bivariate generating function to enumerate + all 1,163 legal width-count vectors. It uses integer bisection to enclose + `(48/r)^(1/3)` at denominator `10^12`. +- `independent_check.py` recursively enumerates the vectors and uses integer + Newton iteration on the different radicand `48*r^2`. It validates the + primary certificate as well as the independent proof integers. +- The capacity census is `8:6, 16:27, 32:215, 48:915`. All 45 attainable ranks + are retained, including zero, rank one, rank 48, and negative-credit ranks. + The primary minimum scaled margin is `292232800689300/526848237133 > 554`, + at rank 44. The independent minimum proof integer is `1794386594565 > 0`, + also at rank 44. +- The written proof shows the cost ratio decreases with b. Exact checks at + `b=1/3` therefore cover the continuum; a finite exponent sample is not being + called a proof. The certificate also records the exact failure + `-22800/47` at rank 32, b=1, for an unjustified broader interval. + +Neither implementation imports a retained search or moment engine or the +other implementation. They intentionally share the stated mathematical model +and source pins. Independent computational implementation does not imply +independent human peer review or proof-assistant formalization. + +## Provenance, overlap, and scope + +Exact base: `407d52ff15b2217b6e22bce44728b4c3907b6515`. +Assignment seed **77** selects independent verification. [CLAIM.json](CLAIM.json) +records candidate tasks, selection, bounded domain, and local coordination. +[SOURCES.json](SOURCES.json) freezes the inherited sources and dependency heads. +At the base, the selected conditional result is PR942's +`kappa = 1661960547713947/10^18`; this contribution does not change it. + +The prices and ledger are due to Chafik Boukhalfa's PR795/PR890. Jonathan +Capalbo's PR942 supplies the pointwise all-T supporting argument being extended. +Charles Bethin's PR850 proves a stronger **integer** optimum for the fixed +72-call (T=8) instance over the same exponent interval. The present fractional +all-T lower envelope does not supersede that result. Joel Pulikkan's concurrent +PR962 independently reconstructs the T37 owner composition; no code or owner +data from that pending PR is used here. Full credits and disclosure are in +[NOTICE.md](NOTICE.md). + +This package changes only its research directory. It proves no new supplier, +owner assignment, cost recurrence, outer bound, kappa, runtime speedup, or +largest possible exponent interval. All-size/compiler, common-label and +mutable-source realization, whole-call hosting, precision/tape, analytic +transfer, and bit-interface obligations remain inherited. It does not replay +the native supplier or certify the full multiplication theorem. + +The experiment has no stochastic search: seed 77 selects the object; the final +domain is every legal bin count vector at capacities 8/16/32/48 and every +attainable residual. Enumeration stops only after exhausting that finite +domain. The real exponent interval is discharged by the written argument. + +See [VALIDATION.md](VALIDATION.md) for the executed checks and their limits. diff --git a/research/u8-supporting-uniform/SOURCES.json b/research/u8-supporting-uniform/SOURCES.json new file mode 100644 index 0000000000..2266885142 --- /dev/null +++ b/research/u8-supporting-uniform/SOURCES.json @@ -0,0 +1,23 @@ +{ + "base_commit": "407d52ff15b2217b6e22bce44728b4c3907b6515", + "hash_policy": "SHA-256 of exact committed bytes; use an LF checkout (git core.autocrlf=false).", + "dependency_heads": { + "PR890": "4b3bd8cbe8e3e81c44161017c9b72c905a8040a8", + "PR942": "1960cfa919a0945d0ca4cb14ea96237000037903" + }, + "runtime": "Python 3.10+ standard library; no source module imports", + "files": { + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b", + "research/complex-t37-owners/independent/all_t_bound.py": "3f8637a90baaa11ef18eab9e739d17b32fcff18fbc50c355f9ef32727a92e4f6", + "research/complex-t21-owners/data/CLAIM.json": "433d7bc4a371aaffeee35c12a1db6ea974722a85b799233626e1a57dcfdcb121", + "research/owner-profile-uniform/README.md": "c4c8f79477c39247b21c1a3ff0133c1f53e7226cd9190be555ffff3739948dd1" + }, + "selected_context_at_base": { + "path": "certificates/selected-result.json", + "sha256": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3", + "kappa": "1661960547713947/1000000000000000000", + "runtime_pin": false, + "note": "Observation at exact base only; this moving selected pointer is not an input to the standalone research verifier." + } +} diff --git a/research/u8-supporting-uniform/VALIDATION.md b/research/u8-supporting-uniform/VALIDATION.md new file mode 100644 index 0000000000..1bb477eade --- /dev/null +++ b/research/u8-supporting-uniform/VALIDATION.md @@ -0,0 +1,45 @@ +# Executed validation + +Executed on 2026-10-13, Windows, CPython **3.14.5**, against base +`407d52ff15b2217b6e22bce44728b4c3907b6515`. Both implementations use only the +standard library. The claimed minimum supported version is Python 3.10 based +on language/API usage; that minimum-version interpreter was not tested. + +| Check | Observed result | +|---|---| +| `python -B research/u8-supporting-uniform/verify.py` | `PASS_U8_SUPPORTING_UNIFORM`; 1,163 patterns, 42 strict ranks, uniform scaled margin greater than 554 | +| `python -B research/u8-supporting-uniform/independent_check.py` | `PASS_U8_SUPPORTING_INDEPENDENT`; independent proof integer minimum 1,794,386,594,565 at rank 44 | +| `python -B research/u8-supporting-uniform/test_verify.py` | 8 tests pass; observed duration 4.026 seconds, not a performance comparison | +| Optimized standalone execution | Both scripts pass under `-O -S -B`; checks use exceptions and do not disappear under optimization | +| Nine corrupted certificates | Both implementations reject all nine; the independent CLI must report the specific expected failure | +| Changed pinned source | Rejected with `source drift` | +| Regeneration to a fresh file | Byte-identical certificate; SHA-256 below | +| `python -B scripts/verify_selected_result.py` | Pass for base selected `1661960547713947/10^18` | +| Refreshed upstream source compatibility | All five pinned inputs unchanged at `8bddbee377e2f3ce1f1247196c4b290d55767d20` | +| Separate scoped review | No actionable mathematical or implementation issue found; AI review, not human peer review | + +Certificate SHA-256: + +``` +3ffa4e686f92ece0ba53206068377e4ae27912a17d491463632ebd39d77ee16a +``` + +The controls alter rank-one price, a negative credit, worst-rank coverage, +negative-credit coverage, a cube lower endpoint, the denominator upper +endpoint, a claimed margin, equality mass, and the exponent scope. The exact +rank-32 failure at b=1 is additionally derived from a different rational +formula, rather than by corrupting the computed answer. + +The first test run could not write fixture files under the desktop sandbox's +default TEMP directory. Directing TEMP/TMP/TMPDIR to a writable workspace +directory resolved this environmental error. A later run caught a source-list +mismatch after moving the changing selected frontier into context-only +metadata; both source inventories were reconciled, and rejection tests were +tightened to check the intended failure message. The final suite passes with +all mathematical coverage retained. + +Repository-wide `make verify`, native selected-supplier cold replay, hosted CI, +and proof-assistant verification were **not run**. This addition changes only a +standalone research package; none of the inherited generators, construction +artifacts, selected frontier, or `upstream/` files are changed. The scoped checks +above do not certify those larger systems. diff --git a/research/u8-supporting-uniform/independent_check.py b/research/u8-supporting-uniform/independent_check.py new file mode 100644 index 0000000000..05b8624433 --- /dev/null +++ b/research/u8-supporting-uniform/independent_check.py @@ -0,0 +1,175 @@ +"""Independent recursive census and Newton-root check of the U8 certificate. + +Imports only the Python standard library. All checks remain active under -O. +The analytic continuum argument is supplied separately by PROOF.md. +""" +from __future__ import annotations + +import argparse +from fractions import Fraction +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = "407d52ff15b2217b6e22bce44728b4c3907b6515" +WIDTHS = (4, 5, 7, 8, 9) +PRICES = (-1, -20, -8, -2, 4) +BINS = ((8, 672, 2), (16, 448, 4), (32, 448, 8), (48, 448, -13)) +HELPERS = (80, 32, 54, 122, 216) +D = 10**12 + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def newton_cube_root(n: int) -> int: + """Integer Newton iteration from an upper bound; return floor(cuberoot(n)).""" + need(type(n) is int and n >= 0, "nonnegative integer root input") + if n < 2: + return n + current = 1 << ((n.bit_length() + 2) // 3) + while True: + following = (2 * current + n // (current * current)) // 3 + if following >= current: + need(current**3 <= n < (current + 1)**3, "Newton root postcondition") + return current + current = following + + +def recursive_census() -> tuple[dict, dict, set]: + upper, totals, patterns = {}, {}, set() + for capacity, _, bonus in BINS: + totals[capacity] = 0 + + def visit(index: int, space: int, price: int, counts: tuple) -> None: + if index == len(WIDTHS): + totals[capacity] += 1 + patterns.add((capacity, counts)) + upper[space] = max(upper.get(space, price), price) + return + for count in range(space // WIDTHS[index] + 1): + visit(index + 1, space - count * WIDTHS[index], + price + count * PRICES[index], counts + (count,)) + + visit(0, capacity, bonus, ()) + need(totals == {8: 6, 16: 27, 32: 215, 48: 915}, "recursive census counts") + need(len(patterns) == sum(totals.values()) == 1163, "recursive pattern coverage") + need(sorted(upper) == list(range(42)) + [43, 44, 48], "attainable ranks") + need((upper[0], upper[1], upper[48]) == (0, 19, -13), "boundary prices") + return upper, totals, patterns + + +def check_pins() -> None: + pins = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + need(pins["base_commit"] == BASE, "source base commit") + expected_paths = { + "research/complex-t21-owner-bound/PROOF.md", + "research/complex-t37-owners/ALL-T-PROOF.md", + "research/complex-t37-owners/independent/all_t_bound.py", + "research/complex-t21-owners/data/CLAIM.json", + "research/owner-profile-uniform/README.md", + } + need(set(pins["files"]) == expected_paths, "complete source-pin inventory") + for relative, expected in pins["files"].items(): + actual = hashlib.sha256((ROOT / relative).read_bytes()).hexdigest() + need(actual == expected, "source drift: " + relative) + + +def check_bracket(pair: list, rank: int) -> tuple[int, int]: + need(isinstance(pair, list) and len(pair) == 2, "two root endpoints") + lower, higher = pair + need(type(lower) is int and type(higher) is int and higher == lower + 1, + "consecutive integer root endpoints") + need(0 <= lower and rank * lower**3 <= 48 * D**3 < rank * higher**3, + "certificate root bracket at rank " + str(rank)) + return lower, higher + + +def check(candidate: dict) -> None: + check_pins() + upper, counts, patterns = recursive_census() + need(candidate["status"] == "PASS_U8_SUPPORTING_UNIFORM", "certificate status") + need(candidate["base_commit"] == BASE, "certificate base commit") + need(candidate["exponent_interval"] == "0 < b <= 1/3", "exponent scope") + need(candidate["root_denominator"] == D, "root denominator") + need(candidate["legal_patterns"] == 1163, "certificate pattern count") + need(candidate["legal_patterns_by_capacity"] == {str(k): v for k, v in counts.items()}, + "certificate per-capacity counts") + need(candidate["attainable_residuals"] == sorted(upper), "certificate rank coverage") + rows = candidate["rows"] + need([row["rank"] for row in rows] == sorted(upper), "complete ordered unique rows") + root48_lower, root48_upper = check_bracket(candidate["cube_root_48_numerators"], 1) + need(root48_lower == newton_cube_root(48 * D**3), "independent root of 48") + need(root48_upper == 3634241185665, "proof's root upper numerator") + need(root48_upper > D, "positive ratio denominator") + + margins, proof_integers = {}, {} + bonuses = {capacity: bonus for capacity, _, bonus in BINS} + for row in rows: + rank = row["rank"] + credit = 48 * upper[rank] + 13 * rank + need(row["upper_price"] == upper[rank] and row["credit"] == credit, + "independent price and credit at rank " + str(rank)) + witness = row["maximizing_bin"] + capacity, vector = witness["capacity"], tuple(witness["counts"]) + need((capacity, vector) in patterns, "legal maximizing witness") + need(capacity - sum(w * n for w, n in zip(WIDTHS, vector)) == rank, + "witness residual rank") + need(bonuses[capacity] + sum(p * n for p, n in zip(PRICES, vector)) == upper[rank], + "witness attains independent maximum") + expected_keys = {"rank", "upper_price", "credit", "maximizing_bin"} + if rank not in (0, 1, 48): + expected_keys |= {"cube_root_numerators", "scaled_margin_lower"} + lower, _ = check_bracket(row["cube_root_numerators"], rank) + need(lower >= D, "nonnegative endpoint numerator") + margin = Fraction(925 * rank * (lower - D), root48_upper - D) - credit + need(row["scaled_margin_lower"] == str(margin) and margin > 554, + "certificate's exact margin at rank " + str(rank)) + margins[rank] = margin + # Different algebraic radicand from the primary certificate: + # q(r) = (cuberoot(48*r*r)-r)/(cuberoot(48)-1). + root = newton_cube_root(48 * rank * rank * D**3) + need(root > rank * D, "positive independent numerator") + value = 925 * (root - rank * D) - (credit + 554) * (root48_upper - D) + need(value > 0, "independent proof inequality at rank " + str(rank)) + proof_integers[rank] = value + need(set(row) == expected_keys, "row fields at rank " + str(rank)) + need(len(margins) == candidate["strict_ranks_checked"] == 42, "42 strict inequalities") + need(min(proof_integers, key=proof_integers.get) == 44 + and proof_integers[44] == 1794386594565, "proof's minimum exact integer") + need(candidate["support"] == { + "rank_one_credit": 925, "scaled_uniform_margin": 554, + "worst_endpoint_rank": min(margins, key=margins.get), + "minimum_scaled_margin_lower": str(min(margins.values()))}, "support summary") + + mass = sum(c * n for c, n, _ in BINS) - 9 * sum(w * n for w, n in zip(WIDTHS, HELPERS)) + signed = sum(n * p for _, n, p in BINS) + 9 * sum(p * n for p, n in zip(PRICES, HELPERS)) + need((mass, signed, 48 * signed + 13 * mass) == (14382, -3892, 150), "ledger arithmetic") + need(candidate["per_replica"] == {"residual_mass": mass, "signed_price": signed, + "credit_required": 150}, "certificate ledger") + rank_one = Fraction(150, 925) + rank48 = (mass - rank_one) / 48 + need(rank_one == Fraction(6, 37) and rank48 == Fraction(11086, 37), "equality arithmetic") + need(candidate["equality_profile"] == {"minimum_replicas": rank_one.denominator, + "rank_1": rank_one.numerator, "rank_48": rank48.numerator}, "integer equality profile") + false_margin = Fraction(925 * (48 - 32), 47) - (48 * upper[32] + 13 * 32) + need(false_margin == Fraction(-22800, 47) < 0, "outside-interval counterexample") + need(candidate["scope_counterexample"] == {"exponent": "1", "rank": 32, + "scaled_margin": str(false_margin)}, "certificate scope counterexample") + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--certificate", type=Path, default=HERE / "CERTIFICATE.json") + args = parser.parse_args() + check(json.loads(args.certificate.read_text(encoding="utf-8"))) + print("PASS_U8_SUPPORTING_INDEPENDENT: 1163 recursive patterns; 42 exact inequalities; " + "proof minimum 1794386594565 at rank 44") + + +if __name__ == "__main__": + main() diff --git a/research/u8-supporting-uniform/test_verify.py b/research/u8-supporting-uniform/test_verify.py new file mode 100644 index 0000000000..14a6f8a72a --- /dev/null +++ b/research/u8-supporting-uniform/test_verify.py @@ -0,0 +1,138 @@ +"""Mathematical corruption controls and source-model binding checks.""" +import ast +import copy +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest + +import verify as V + + +class SupportingCertificateTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.expected = V.build_certificate() + + def test_committed_certificate_and_source_pins(self): + V.source_pins() + candidate = json.loads((V.HERE / "CERTIFICATE.json").read_text(encoding="utf-8")) + V.check_certificate(candidate, self.expected) + + def test_model_matches_pinned_predecessor_literals(self): + # Parse literal data only. Never execute the predecessor's code. + path = V.ROOT / "research/complex-t37-owners/independent/all_t_bound.py" + literals = {} + names = {"WIDTHS", "PRICES", "CAPACITIES", "INVENTORY"} + for node in ast.parse(path.read_text(encoding="utf-8")).body: + if isinstance(node, ast.Assign) and len(node.targets) == 1: + target = node.targets[0] + if isinstance(target, ast.Name) and target.id in names: + literals[target.id] = ast.literal_eval(node.value) + self.assertEqual(literals, { + "WIDTHS": V.WIDTHS, "PRICES": V.PRICES, + "CAPACITIES": V.CAPACITIES, + "INVENTORY": dict(zip(V.WIDTHS, V.HELPERS)), + }) + + def test_cube_floor_across_exact_cube_boundaries(self): + for k in (0, 1, 2, 3, 10, 48, 10**12, 3634241185664): + for n in (k**3, k**3 + 1, (k + 1)**3 - 1): + result = V.cube_floor(n) + self.assertLessEqual(result**3, n) + self.assertLess(n, (result + 1)**3) + with self.assertRaisesRegex(ValueError, "nonnegative"): + V.cube_floor(-1) + + def test_equality_profile_requires_replicas_divisible_by_37(self): + # Modular arithmetic proves the all-T statement; these check boundaries + # and the explicit representative without asserting a finite search proof. + from fractions import Fraction + self.assertEqual(Fraction(150, 925), Fraction(6, 37)) + self.assertEqual(48 * 11086 + 6, 14382 * 37) + self.assertEqual(19 * 6 - 13 * 11086, -3892 * 37) + for replicas in (1, 8, 21, 36, 37, 38, 74, 10**6): + self.assertEqual((6 * replicas) % 37 == 0, replicas % 37 == 0) + + def test_false_broadening_to_b_equal_one(self): + # At b=1, the *unstrengthened* supporting inequality already fails. + from fractions import Fraction + rank = 32 + v = next(r["credit"] for r in self.expected["rows"] if r["rank"] == rank) + self.assertEqual(Fraction(925 * (48 - rank), 47) - v, Fraction(-22800, 47)) + + def test_source_mutation_is_rejected(self): + pins = V.source_pins() + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + for relative in pins["files"]: + destination = root / relative + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_bytes((V.ROOT / relative).read_bytes()) + V.source_pins(root) + target = root / "research/complex-t21-owner-bound/PROOF.md" + target.write_bytes(target.read_bytes() + b"\nchanged source\n") + with self.assertRaisesRegex(ValueError, "source drift"): + V.source_pins(root) + + def test_mathematical_certificate_mutations(self): + def row(data, rank): + return next(item for item in data["rows"] if item["rank"] == rank) + + def omit(data, rank): + data["rows"] = [item for item in data["rows"] if item["rank"] != rank] + + changes = { + "wrong_rank_one_price": lambda d: row(d, 1).__setitem__("upper_price", 18), + "wrong_signed_credit": lambda d: row(d, 38).__setitem__("credit", 2050), + "omit_worst_rank": lambda d: omit(d, 44), + "omit_negative_credit_rank": lambda d: omit(d, 38), + "false_cube_lower": lambda d: row(d, 2)["cube_root_numerators"].__setitem__( + 0, row(d, 2)["cube_root_numerators"][0] + 1), + "false_denominator_upper": lambda d: d["cube_root_48_numerators"].__setitem__( + 1, d["cube_root_48_numerators"][0]), + "inflated_margin": lambda d: row(d, 44).__setitem__("scaled_margin_lower", "1000"), + "wrong_equality_mass": lambda d: d["equality_profile"].__setitem__("rank_48", 11087), + "unproved_exponent_interval": lambda d: d.__setitem__("exponent_interval", "0 < b <= 1"), + } + reasons = { + "wrong_rank_one_price": "independent price and credit at rank 1", + "wrong_signed_credit": "independent price and credit at rank 38", + "omit_worst_rank": "complete ordered unique rows", + "omit_negative_credit_rank": "complete ordered unique rows", + "false_cube_lower": "consecutive integer root endpoints", + "false_denominator_upper": "consecutive integer root endpoints", + "inflated_margin": "certificate's exact margin at rank 44", + "wrong_equality_mass": "integer equality profile", + "unproved_exponent_interval": "exponent scope", + } + independent = V.HERE / "independent_check.py" + self.assertTrue(independent.is_file(), "independent implementation must be present") + with tempfile.TemporaryDirectory() as directory: + for name, change in changes.items(): + with self.subTest(control=name): + candidate = copy.deepcopy(self.expected) + change(candidate) + with self.assertRaisesRegex(ValueError, "certificate differs"): + V.check_certificate(candidate, self.expected) + path = Path(directory) / (name + ".json") + path.write_text(json.dumps(candidate), encoding="utf-8") + process = subprocess.run( + [sys.executable, "-O", "-S", "-B", str(independent), + "--certificate", str(path)], capture_output=True, text=True) + self.assertNotEqual(process.returncode, 0, name) + self.assertIn("ValueError: " + reasons[name], process.stderr, process.stderr) + + def test_optimized_standalone_runs(self): + for filename in ("verify.py", "independent_check.py"): + result = subprocess.run( + [sys.executable, "-O", "-S", "-B", str(V.HERE / filename)], + capture_output=True, text=True) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_U8_SUPPORTING_", result.stdout) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/u8-supporting-uniform/verify.py b/research/u8-supporting-uniform/verify.py new file mode 100644 index 0000000000..ceda9fb1dc --- /dev/null +++ b/research/u8-supporting-uniform/verify.py @@ -0,0 +1,194 @@ +"""Exact finite certificate for the U8 supporting inequality on 0 < b <= 1/3. + +Standard library only. No retained search, moment or interval engine is imported. +The continuum step is the analytic argument in PROOF.md, not finite sampling. +""" +from __future__ import annotations + +import argparse +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WIDTHS = (4, 5, 7, 8, 9) +PRICES = (-1, -20, -8, -2, 4) +CAPACITIES = {8: (672, 2), 16: (448, 4), 32: (448, 8), 48: (448, -13)} +HELPERS = (80, 32, 54, 122, 216) +SCALE = 10**12 +BASE = "407d52ff15b2217b6e22bce44728b4c3907b6515" + + +def require(ok: bool, message: str) -> None: + if not ok: + raise ValueError(message) + + +def cube_floor(n: int) -> int: + """Floor cube root by integer bisection, with no floating-point estimate.""" + require(n >= 0, "cube root input must be nonnegative") + lo, hi = 0, 1 << ((n.bit_length() + 2) // 3) + while hi - lo > 1: + middle = (lo + hi) // 2 + if middle**3 <= n: + lo = middle + else: + hi = middle + return lo + + +def root_bracket(rank: int, scale: int = SCALE) -> tuple[int, int]: + """Numerators enclosing (48/rank)^(1/3) with denominator scale.""" + require(0 < rank <= 48 and scale > 0, "root bracket domain") + lo = cube_floor(48 * scale**3 // rank) + hi = lo + 1 + require(rank * lo**3 <= 48 * scale**3 < rank * hi**3, + "invalid exact cube-root enclosure") + return lo, hi + + +def bin_census() -> dict: + """Multiply five truncated bivariate generating-function factors. + + Product_w sum_{j=0}^{floor(48/w)} x^(w*j) y^(price(w)*j). + Each coefficient counts width-count vectors, not orderings of helpers. + Negative powers of y are dictionary keys. Truncating x above 48 is exact + because all widths are positive. Keep one lexicographic witness per key. + """ + polynomial = {(0, 0): (1, ())} + for width, price in zip(WIDTHS, PRICES): + product = {} + for (fill, value), (multiplicity, witness) in polynomial.items(): + for count in range((48 - fill) // width + 1): + key = (fill + width * count, value + price * count) + vector = witness + (count,) + old_count, old_witness = product.get(key, (0, vector)) + product[key] = (old_count + multiplicity, min(old_witness, vector)) + polynomial = product + + upper, witnesses, counts = {}, {}, {} + for cap, (_, bonus) in CAPACITIES.items(): + counts[cap] = 0 + for (fill, value), (multiplicity, vector) in sorted(polynomial.items()): + if fill > cap: + continue + counts[cap] += multiplicity + rank, price = cap - fill, value + bonus + if rank not in upper or price > upper[rank]: + upper[rank] = price + witnesses[rank] = {"capacity": cap, "counts": list(vector)} + require(sum(counts.values()) == 1163, "complete 1163-pattern census") + require((upper[0], upper[1], upper[48]) == (0, 19, -13), "boundary prices") + for rank, witness in witnesses.items(): + vector, cap = witness["counts"], witness["capacity"] + require(cap - sum(w * n for w, n in zip(WIDTHS, vector)) == rank, + "witness residual") + require(CAPACITIES[cap][1] + sum(p * n for p, n in zip(PRICES, vector)) == upper[rank], + "witness price") + return {"upper": upper, "witnesses": witnesses, "counts": counts} + + +def source_pins(root: Path = ROOT) -> dict: + pins = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + require(pins["base_commit"] == BASE, "source base commit") + require(set(pins["files"]) == { + "research/complex-t21-owner-bound/PROOF.md", + "research/complex-t37-owners/ALL-T-PROOF.md", + "research/complex-t37-owners/independent/all_t_bound.py", + "research/complex-t21-owners/data/CLAIM.json", + "research/owner-profile-uniform/README.md", + }, "complete source-pin inventory") + for relative, expected in pins["files"].items(): + path = root / relative + actual = hashlib.sha256(path.read_bytes()).hexdigest() + require(actual == expected, "source drift: " + relative) + return pins + + +def build_certificate() -> dict: + census = bin_census() + upper = census["upper"] + mass = sum(cap * n for cap, (n, _) in CAPACITIES.items()) - 9 * sum( + w * n for w, n in zip(WIDTHS, HELPERS)) + signed = sum(n * bonus for n, bonus in CAPACITIES.values()) + 9 * sum( + p * n for p, n in zip(PRICES, HELPERS)) + require((mass, signed, 48 * signed + 13 * mass) == (14382, -3892, 150), + "per-replica mass and signed-price accounting") + require(Q(150, 925) == Q(6, 37), "rank-one equality demand") + require(48 * 11086 + 6 == 37 * mass, "T37 equality profile mass") + require(-13 * 11086 + 19 * 6 == 37 * signed, "T37 equality profile price") + + root1_lo, root1_hi = root_bracket(1) + denominator = root1_hi - SCALE + require(denominator > 0, "positive ratio denominator") + rows, margins = [], {} + for rank in sorted(upper): + row = {"rank": rank, "upper_price": upper[rank], + "credit": 48 * upper[rank] + 13 * rank, + "maximizing_bin": census["witnesses"][rank]} + if 1 < rank < 48: + lo, hi = root_bracket(rank) + require(lo >= SCALE, "nonnegative ratio numerator") + # Lower numerator / upper positive denominator is a lower bound. + # Credit is subtracted exactly; its sign never affects rounding. + margin = Q(925 * rank * (lo - SCALE), denominator) - row["credit"] + require(margin > 554, "uniform strict margin failed at rank " + str(rank)) + row.update(cube_root_numerators=[lo, hi], + scaled_margin_lower=str(margin)) + margins[rank] = margin + rows.append(row) + require(set(margins) == set(upper) - {0, 1, 48}, "all strict ranks covered") + worst = min(margins, key=margins.get) + + # Exact counterexample to extending the same supporting line to b=1. + # c_1(r)/c_1(1) = (48-r)/47; the cube-root proof is not used here. + false_extension = Q(925 * (48 - 32), 47) - (48 * upper[32] + 13 * 32) + require(false_extension == Q(-22800, 47) < 0, "b=1 scope counterexample") + return { + "status": "PASS_U8_SUPPORTING_UNIFORM", + "base_commit": BASE, + "method": "generating-function census and integer cube-root endpoint bounds", + "exponent_interval": "0 < b <= 1/3", + "root_denominator": SCALE, + "cube_root_48_numerators": [root1_lo, root1_hi], + "legal_patterns_by_capacity": {str(k): v for k, v in census["counts"].items()}, + "legal_patterns": sum(census["counts"].values()), + "attainable_residuals": sorted(upper), + "strict_ranks_checked": len(margins), + "per_replica": {"residual_mass": mass, "signed_price": signed, "credit_required": 150}, + "support": {"rank_one_credit": 925, "scaled_uniform_margin": 554, + "worst_endpoint_rank": worst, + "minimum_scaled_margin_lower": str(margins[worst])}, + "equality_profile": {"minimum_replicas": 37, "rank_1": 6, "rank_48": 11086}, + "scope_counterexample": {"exponent": "1", "rank": 32, + "scaled_margin": str(false_extension)}, + "rows": rows, + "scope": "Exact finite endpoint certificate plus a written continuum proof; fixed whole-helper ledger only. No owner feasibility, outer assembly, new kappa, or full multiplication theorem is certified.", + } + + +def check_certificate(candidate: dict, expected: dict) -> None: + require(candidate == expected, "certificate differs from complete exact recomputation") + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--certificate", type=Path, default=HERE / "CERTIFICATE.json") + parser.add_argument("--write", type=Path, help="write regenerated certificate to a new file") + args = parser.parse_args() + source_pins() + expected = build_certificate() + if args.write: + with args.write.open("x", encoding="utf-8", newline="\n") as stream: + stream.write(json.dumps(expected, indent=2, sort_keys=True) + "\n") + else: + candidate = json.loads(args.certificate.read_text(encoding="utf-8")) + check_certificate(candidate, expected) + print("PASS_U8_SUPPORTING_UNIFORM: 1163 bin patterns; " + f"{expected['strict_ranks_checked']} strict ranks; 0 < b <= 1/3; scaled margin > 554") + + +if __name__ == "__main__": + main()