Skip to content

Independent verification: T37 positive-binomial moments, all-T lemma, and 1024-bit reduction (seed 78, no new kappa) #1052

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 2 commits into from
Oct 13, 2026
Merged

Independent verification: T37 positive-binomial moments, all-T lemma, and 1024-bit reduction (seed 78, no new kappa) #1052

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1bf7197
Independent verification: T37 positive-binomial moments, all-T lemma,…
steph4n-gh Oct 13, 2026
e7f0319
Record submitted PR #1052 link in CLAIM.json and VALIDATION.json
steph4n-gh Oct 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
222 changes: 222 additions & 0 deletions research/t37-binomial-endpoint-audit-seed78/CERTIFICATE.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,222 @@
{
"all_t_supporting_lemma_binomial": {
"certified_exponent": "1664727258740678855773/1000000000000000000000000",
"credit_per_replica": 150,
"dual_bin_vectors": 1163,
"equality_ratio": "6/37",
"mass_per_replica": 14382,
"minimum_strict_margin_interval": [
"595251138690295459954095412968124864075333478608180372230668385479068449/2042916918650006881080687735233999533925528255762434420328107170244591616",
"595251138690295459954095412968124864075333478608420974336491494378566609/2042916918650006881080687735233999533925528255762434420328107170244591616"
],
"minimum_strict_margin_rank": 2,
"multiplier_interval": [
"34293538513857524176002565657377815154376721830613572565541633671138229/102145845932500344054034386761699976696276412788121721016405358512229580800",
"4286692314232190522000320707172226894297090228827299697783306424883369/12768230741562543006754298345212497087034551598515215127050669814028697600"
],
"realized_remainders": 45,
"remainder_trade_bridge": {
"t16_dual_tight": true,
"t21_dual_tight": true,
"trade_moment_reduction_decimal": "1.008788191942442874856013035077546796038937068752235014386435086450637E-8",
"trade_moment_reduction_interval": [
"228000199681199502566919928059551892869968568102477746458978515158355965/22601394574432946527432448298463366107680161049863517672678266744138309446926336",
"798000698884198258984219748208431625044889988359638849030786692166393171/79104881010515312846013569044621781376880563674522311854373933604484083064242176"
],
"traded_rank_credits": {
"2": 650,
"3": 375,
"44": -100,
"sum": 925
},
"traded_ranks": [
2,
3,
44
]
},
"signed_price_per_replica": -3892,
"strict_rank_inequalities_certified": 42
},
"assignment_seed": 78,
"audited_pr": 942,
"audited_source_head": "1960cfa919a0945d0ca4cb14ea96237000037903",
"base_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0",
"bit_supplier_accounting": {
"arity": 64,
"child_count": 904896,
"derived_deficit": 10272,
"git_blob_sha1": "e293ddc557742637f9f679f083a1a282d87b1b13",
"live_stock": 28416,
"rank_mass": 1808352
},
"conservative_kappa": "83098027241579/50000000000000000",
"conservative_kappa_decimal": "0.00166196054483158",
"controls": {
"algebraic_comparisons": 770,
"mathematical_controls": 8,
"redistributed_minus_original_interval": [
"-8746087210709628165738148931306907828030512622956302090084205337237/610848502011701257498174278336847732640004352699013991153466668760494849916928",
"-61222610474967397160167042519148354796208797196160377156292933031609/4275939514081908802487219948357934128480030468893097938074266681323463949418496"
],
"rejected_inputs": 14,
"untraded_residual_at_native_endpoint_interval": [
"43135172912659363912921498380808847749099389399529318911867366123635617/4275939514081908802487219948357934128480030468893097938074266681323463949418496",
"6162167558951337701845928340115549678442770256442738074937223729936169/610848502011701257498174278336847732640004352699013991153466668760494849916928"
]
},
"gain_over_pr890_t21_decimal": "0.000000002773066918",
"gain_over_pr890_t21_grid_ticks": 2773066918,
"moment_brackets": {
"bit_surcharged": {
"endpoint": "1733427039589844234749/1000000000000000000000000",
"lower_residual_interval": [
"-8164977726660319484683715511910052609627089137376241533831481541/5107292296625017202701719338084998834813820639406086050820267925611479040000000000000000",
"-204124443166507987117092887715267121610531980048075286508088661/127682307415625430067542983452124970870345515985152151270506698140286976000000000000000"
],
"overlaps_recorded_mercator_and_base_two": true,
"successor": "6933708158359376939/4000000000000000000000",
"successor_residual_interval": [
"341036479082498025331223485906619312344032545629041956416772927/204291691865000688108068773523399953392552825576243442032810717024459161600000000000000",
"8525911977062450633280587150964850553806623575685123863071597409/5107292296625017202701719338084998834813820639406086050820267925611479040000000000000000"
],
"terms": {
"1": 6784,
"2": 3366,
"3": 2226,
"4": 1656,
"42": 101,
"5": 1314,
"6": 1086,
"7": 923,
"fallback": 6784
}
},
"complex_conservative": {
"endpoint": "1664727255848707292019/1000000000000000000000000",
"lower_residual_interval": [
"-1024554351587832158915801992420819872763116410427697165986171883880689/668115549075298250388628116930927207575004760764546552824104168956791242096640000000000000000",
"-73182453684845154208271570860465217721264404456127598656975048002029/47722539219664160742044865495066229112500340054610468058864583496913660149760000000000000000"
],
"overlaps_recorded_mercator_and_base_two": true,
"successor": "83236362792435364601/50000000000000000000000",
"successor_residual_interval": [
"944919440753882074236218177653797101322228610552124365607458131597773/668115549075298250388628116930927207575004760764546552824104168956791242096640000000000000000",
"944919440753882074236218178028103925987643358576352021645643271210791/668115549075298250388628116930927207575004760764546552824104168956791242096640000000000000000"
],
"terms": {
"1": 7743,
"2": 3845,
"3": 2546,
"4": 1896,
"48": 101,
"5": 1506,
"8": 921,
"fallback": 7743
}
},
"complex_native": {
"endpoint": "416181814685169713943/250000000000000000000000",
"lower_residual_interval": [
"-102682206773527733400761451721708791737489072081802853/305424251005850628749087139168423866320002176349506995576733334380247424958464",
"-718775447414694133805330160854179701134683631215549081/2137969757040954401243609974178967064240015234446548969037133340661731974709248"
],
"overlaps_recorded_mercator_and_base_two": true,
"successor": "1664727258740678855773/1000000000000000000000000",
"successor_residual_interval": [
"697942586008414853022659031722582037313325045766156001/267246219630119300155451246772370883030001904305818621129641667582716496838656",
"5583540688067318824181272254978438139534340239480309535/2137969757040954401243609974178967064240015234446548969037133340661731974709248"
],
"terms": {
"1": 7743,
"2": 3845,
"3": 2546,
"4": 1896,
"48": 101,
"5": 1506,
"8": 921
}
}
},
"native_correction_gain": "2.882367E-12",
"native_correction_gain_grid_ticks": 2882367,
"outer_reduction_1024": {
"accepted_absorption_gap": "6557617028213798864657563815835253324572044775952061536037244806485964573382313019438847718517433221854794233024643983438981758998766811887159826631397377418574129671610269897894152287448350965181400939289760280157165852766240594433448174768318992608869549102850776227624526630753646328096515675160759173487408727805367572859088758279475715209714756719033318339547341553045837955218683064707488672973238303999/7642095392293858939023699732275615597522482014517635374883248634618996214470752759797106100963701024482866251866941275961954971649917727004479626396516439120769390929194270427307609982012932952599384180104872691387129988962554463302434494226096612054806168654736311219108618931376985755805875886135513931202778162363927747033553531962074773003315009476932668226727048487248825949602202789014200814696001000000000000000000000000",
"accepted_bootstrap_steps": 7,
"accepted_outer_controls": [
"next_grid",
"zero_eta",
"zero_beta",
"unit_beta"
],
"accepted_outer_strict_constraints": 47,
"conservative_absorption_gap": "496658653044703417316248259922429050968719099139786330271931405239022348151359541426489458001871057362032768793676136721623676436577446141205393489167294045949578526901330104617539501725630582885899424568174063869073690664592351019509245630185952001776845154201949149623942603168321582059124808125260583385984408742531372375154490190892701874790201002675785581447950792955508571894399911333679828534929023718132959/500832363627924353645980685654816341422188848789118867321951631352707340876514937763970127086658872935315950331177975587350076142629842991366517997042099217691101001196646376882871210858299557545014400780914406793189809416128410660950676904684878829187835530616278265407456178970284914387666840362506681096065901299550463570258864587739489650181230421971276053376197335607211242270875834474912173021501867041000000000000000000000000",
"conservative_bootstrap_steps": 7,
"conservative_outer_controls": [
"next_grid",
"zero_eta",
"zero_beta",
"unit_beta"
],
"conservative_outer_strict_constraints": 47,
"min_quadratic_over_1024_linear_cutoff_margin_accepted": 4910947306998,
"min_quadratic_over_1024_linear_cutoff_margin_conservative": 4910947341530
},
"scope": "Independent standard-library verification of the selected PR #942 (T37) native complex, conservative complex, and PR589 bit moment brackets plus all 42 strict rank inequalities of the all-T signed-dual supporting lemma using positive generalized-binomial enclosures on 2^-240, together with the 8-role 44+3+2 -> 48+1 remainder trade, 1024-bit reserve/bootstrap cutoffs, 94 strict outer slacks, and surcharge stakes. Physical circuit replay, owner window sweep, and inherited all-size/compiler/H1-H5 assumptions remain separate.",
"selected_kappa_decimal": "0.001661960547713947",
"selected_kappa_unchanged": "1661960547713947/1000000000000000000",
"source_files_sha256": {
"inputs/ASSEMBLY.json": "4b2894956e594e408e111d806c842f2ed2c32aefcadff93fad69ff0b46f1991a",
"inputs/CLAIM.json": "a383da34ee22da831fa436ad3483568ae1fcd62cd76581f2c2dd2b6473b346fb",
"inputs/EDITS.json": "cd28d8014fe6576a56a640d9a94b6b3fbd7715ea1a6c2858c1597b3c9fb51576",
"inputs/PR589-EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4",
"inputs/selected-result.json": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3"
},
"status": "PASS_T37_BINOMIAL_AND_ENDPOINT_AUDIT",
"t37_accounting": {
"C0_exponent_cap": 210000,
"admissible_payload_interval": [
780,
2356
],
"calls": 333,
"charged_prefix_bits": 1024,
"child_count": 1201234,
"deficit": 11840,
"global_prefix_bits": 779,
"historical_512_prefix_rejected": true,
"live_stock": 33152,
"local_prefix_bits": 72,
"physical_row_coefficient": 17495,
"physical_stock": 33666,
"physical_stock_bits": 2643,
"rank_mass": 2408256,
"remainder_trade": {
"after_remainders": {
"1": 1,
"48": 1
},
"before_remainders": {
"2": 1,
"3": 1,
"44": 1
},
"edits_count": 8,
"traded_idle": {
"1": 6,
"48": 11086
},
"untraded_idle": {
"1": 5,
"2": 1,
"3": 1,
"44": 1,
"48": 11085
}
},
"replicas": 37,
"required_C0_bits": 200012,
"retained_row_coefficient_cap": 20161,
"roles": 167832
}
}
57 changes: 57 additions & 0 deletions research/t37-binomial-endpoint-audit-seed78/CLAIM.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
{
"status": "Submitted independent verification PR #1052; no new kappa",
"submitted_pr": 1052,
"submitted_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1052",
"date": "2026-10-13",
"contributor": "steph4n-gh",
"assignment_seed": 78,
"seed_origin": "Generated via OS randomness (/dev/urandom) at session start",
"track": "75-84: Independent verification or formalization",
"base_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0",
"audited_pr": 942,
"audited_source_head": "1960cfa919a0945d0ca4cb14ea96237000037903",
"candidates_considered": [
"Candidate 1 (Selected): Independent positive-binomial enclosure verification of the selected PR #942 (T37) moment brackets, all 42 strict rank inequalities of the all-T signed-dual supporting lemma, the exact T21/T16/T37 remainder-trade margin bridge, and the complete 1024-bit endpoint-to-kappa reduction.",
"Candidate 2: Lean 4 formalization of binary/signed connector walks (PR #934 / #943 / #944) -- deferred because standard-library Python runs deterministically inside the isolated sandbox without external toolchain paths.",
"Candidate 3: Independent verification of dyadic-run BIT query batching (PR #953) -- deferred because research/dyadic-query-runs/verify.py already ships a standalone standard-library checker."
],
"selected_scope": "Independent standard-library verification of the selected PR #942 (T37) native complex, conservative complex, and PR589 bit moment brackets plus all 42 strict rank inequalities of the all-T signed-dual supporting lemma using positive generalized-binomial enclosures on 2^-240 (importing no production log/exp or outer engine), together with the 8-role 44+3+2 -> 48+1 remainder trade, 1024-bit reserve/bootstrap cutoffs, 94 strict outer slacks, and surcharge stakes.",
"hypothesis": "All 6 supplier moment endpoint decisions (T37 native complex, T37 conservative complex, PR589 bit) and all 42 strict rank inequalities of the PR #942 all-T signed-dual supporting lemma at z = 1664727258740678855773/10^24 hold under an independent positive generalized-binomial enclosure without importing either retained log/exp engine; the 8-role 44+3+2 -> 48+1 remainder trade reduces the T37 moment by the exact sum of the supporting-lemma margins at r in {44, 3, 2} divided by 48*73*33152; and the 1024-bit 7-step bootstrap and 94 strict outer slacks reduce the certified endpoints to kappa = 1661960547713947/10^18 (accepted) and 83098027241579/50000000000000000 (conservative).",
"result": "Confirmed across all 6 moment decisions, 42 all-T rank inequalities, 14 bootstrap steps, 94 outer slacks, 770 exact integer-power algebraic comparisons, 8 mathematical model controls, 14 invalid-input rejections, and 12 disposable package mutation controls under Python -I -O -B. No counterexample to the selected PR #942 arithmetic claims and no new kappa.",
"coordination": "Open issues #913 and #650 were inspected; no pinned sprint coordination issue exists. Claim and results are recorded locally in this file.",
"stopping_rule": "One self-contained, deterministically reproducible verification package with exact source pins, certificate, and fail-closed controls.",
"prior_and_concurrent_work": [
{
"pr": 942,
"author": "Jonathan Capalbo (jon314159)",
"role": "Selected T37 whole-owner construction and all-T signed-dual relaxation bound (conditional kappa = 1661960547713947/10^18)."
},
{
"pr": 960,
"author": "David Breslauer",
"role": "Merged in batch970 (research/t21-binomial-audit): audited only the historical PR #890 (T21) complex moment brackets using positive binomial series; did not audit T37, the PR589 bit moment, the 42 all-T supporting-lemma rank inequalities, or the 1024-bit outer reduction."
},
{
"pr": 957,
"author": "Aaron Wang (navinor)",
"role": "Merged in batch970 (research/audit-frontier890-endpoint-seed73): audited only the historical PR #890 (T21) 512-bit endpoint-to-kappa reduction by transcribing the retained log/exp engines."
},
{
"pr": 678,
"author": "0x-chad",
"role": "Introduced positive generalized-binomial enclosures for the historical PR #543 bit moment."
},
{
"pr": 1051,
"author": "Sagar Thakrar (thakrarsagar)",
"head_sha": "3b8fab9b48d54160d0765c316eed45078f32aa5e",
"role": "Concurrent Track 75-84 PR checking T37 moment endpoints and the binding kappa margin via prime-atanh logarithms and Taylor exponentials. By its stated scope, PR #1051 does not check the 42 all-T supporting-lemma rank inequalities, the 8-role 44+3+2 -> 48+1 remainder trade or its exact T21/T16/T37 supporting-margin decomposition, the 14 1024-bit bootstrap cutoff steps, the full 94 strict outer slacks, or the 1024-bit reserve/stock/C0/row bounds, and uses a two-stage log+exp method rather than single-stage positive generalized-binomial series."
},
{
"open_prs_checked": [962, 974, 991, 992, 995, 1000, 1006, 1009, 1010, 1012, 1019, 1051],
"note": "PRs #995 and #1000 study uniform z-interval bounds for the supporting lemma via cube-root or integral bounds without auditing the T37 moment brackets, PR589 bit bracket, 1024-bit bootstrap cutoffs, 94 outer slacks, or the exact T21/T16/T37 remainder-trade margin decomposition. PR #1019 refines the outer grid by calling existing moment/outer engines."
}
],
"assistance": "Prepared for steph4n-gh with substantial Google Gemini assistance.",
"license": "Apache-2.0"
}
Loading