diff --git a/.github/workflows/composite-cyclic-bezout.yml b/.github/workflows/composite-cyclic-bezout.yml new file mode 100644 index 0000000000..da9beecada --- /dev/null +++ b/.github/workflows/composite-cyclic-bezout.yml @@ -0,0 +1,34 @@ +name: Composite cyclic Bezout certificates +on: + pull_request: + paths: + - 'research/composite-cyclic-bezout/**' + - 'research/prime-power-cyclic-inverse/**' + - '.github/workflows/composite-cyclic-bezout.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + exact-check: + runs-on: ubuntu-latest + timeout-minutes: 5 + strategy: + matrix: + python: ['3.11', '3.14'] + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 + with: + python-version: '${{ matrix.python }}' + - name: Check integer certificates and mathematical mutations + run: python -B -I -O research/composite-cyclic-bezout/verify.py --check research/composite-cyclic-bezout/EXPECTED.json + - name: Check arithmetic and CLI failure detection + run: python -B -I research/composite-cyclic-bezout/test_verify.py + - name: Check modular lifting seeds and finite diagnostics + run: python -B -I -O research/composite-cyclic-bezout/verify_lifting.py --check research/composite-cyclic-bezout/LIFTING-EXPECTED.json + - name: Check lifting arithmetic and failure detection + run: python -B -I research/composite-cyclic-bezout/test_lifting.py + - name: Confirm verification leaves the checkout unchanged + run: git diff --exit-code diff --git a/research/composite-cyclic-bezout/CERTIFICATE.json b/research/composite-cyclic-bezout/CERTIFICATE.json new file mode 100644 index 0000000000..43e202f597 --- /dev/null +++ b/research/composite-cyclic-bezout/CERTIFICATE.json @@ -0,0 +1,1094 @@ +{ + "format": "composite-cyclic-bezout-v1", + "coefficient_order": "ascending z, ascending u", + "cases": [ + { + "order": 6, + "denominator": "4603371", + "a": [ + [ + "947808", + "-338786" + ], + [ + "-389805", + "-1107228" + ], + [ + "-1743712", + "718940" + ], + [ + "-1832268", + "1451004" + ], + [ + "-1546350", + "890052" + ] + ], + "b": [ + [ + "-1083477", + "2032716" + ], + [ + "-643125", + "1905759" + ], + [ + "114787", + "777535" + ], + [ + "344337", + "125274" + ], + [ + "257725", + "-148342" + ] + ] + }, + { + "order": 10, + "denominator": "36514130673104413304485467185561", + "a": [ + [ + "7527165863191012340007242370482", + "-2769125238814090990934539010081", + "899744467809964817188841346541", + "-4665409490941814959821610259700" + ], + [ + "-2900080088754999294406702846016", + "-7617731015569565097868363878841", + "-3151416020405235176660750183849", + "-5652705694551020173318258105449" + ], + [ + "-14568739984731768032830348312822", + "3483937310668813316067920204851", + "-6657515628794336601566728741731", + "11375623713146476738605920986846" + ], + [ + "-8316648129198097420480959815262", + "11794396488869384371346906059864", + "-106767663760773818450720363036", + "14683349665499903148845552182348" + ], + [ + "4578799691027905441358304942924", + "6713949545361481863180800477744", + "9189609185594997729468511681816", + "7499244588529172333743375025016" + ], + [ + "1219162089425484044372394753860", + "7013350434526976547006483140070", + "7504139198517906347200780026810", + "6682339358788149177154118460520" + ], + [ + "-23202502333877639889850708803964", + "13699015115399573958226387512358", + "-6747838304257784740208437211382", + "26510156566445673013437852076226" + ], + [ + "-54212944853496727800648306732920", + "8764517716197980904324144196610", + "-25283083142143904738756639615530", + "46557745312100545967877026925240" + ], + [ + "-43134748082962854958754542931020", + "-7812512394901350397446429810120", + "-27687311324397009987560980489400", + "18150707120626637129112315135480" + ] + ], + "b": [ + [ + "-38757527958805710095586956519259", + "27691252388140909909345390100810", + "-8997444678099648171888413465410", + "46654094909418149598216102597000" + ], + [ + "-44243668682521857894235196849981", + "8802218474397967081240361161331", + "-25105332548543389348590899789290", + "37605856254959841496894823116660" + ], + [ + "-13897763701913091497618742297968", + "-13410553858054092172722809041485", + "-16584001679859591391666868537632", + "-4182899249876525266930729505379" + ], + [ + "-2996777555335108897586114465924", + "-16326832751158094768328998820988", + "-13514645344929672100926160693563", + "-16005956640444224296759966321376" + ], + [ + "-8761285151554517805483263346388", + "-11477499929507153267349836285823", + "-14402461503031020939329181965592", + "-5677156625139229517974423253023" + ], + [ + "-15134364397289878579943557081790", + "-2482219427252392644489843586105", + "-10815751405737711816198468240594", + "6954064627957834806549081136163" + ], + [ + "-11417062928763113950805921623011", + "5227671175544004457065409086621", + "-4287022008897667539160702902677", + "11715418471876851786150995165117" + ], + [ + "-1408343222303920081144776117226", + "5763017952023206942307039098615", + "1844974930043432403822672695547", + "5706086745249688720552715410084" + ], + [ + "4313474808296285495875454293102", + "781251239490135039744642981012", + "2768731132439700998756098048940", + "-1815070712062663712911231513548" + ] + ] + }, + { + "order": 12, + "denominator": "2654047882196193704215495532468166540243913", + "a": [ + [ + "332045564305212184722468135859532021988478", + "128861605526833734292130146782547901082085", + "45264718791888066321009711323986980473885", + "-37169497161014167843951561822682834848500" + ], + [ + "118932275479675191254603436799164776146703", + "69347822311036955926429443596867808436114", + "-340056820467488134844282490323608088068906", + "-391473660969800445429284223060244068459437" + ], + [ + "-251479307521948996007240792690153559468858", + "-309725695705721003290379120988629885593414", + "-90777875498069049119706390021815172506874", + "230443294695070325051173721056462766285046" + ], + [ + "-148964587283721694453881986414222156188359", + "-58972182320336496725087151229001861558604", + "287582379566918209034666245969461719172732", + "103851502110337891577248292797233432144675" + ], + [ + "2641699286600223508992537367014171250948", + "-5022092413735205006354749808313819586204", + "-76585148315288129342971754239256797539908", + "-11349939292109645468256063055185058017898" + ], + [ + "-498506264384641326990662454743215152196404", + "-480345678052683432917288582058774212867568", + "164916452111624963860462342880757309755904", + "160908722159739467577046081317392550037644" + ], + [ + "-1157372485466353033236077146046210793160806", + "-892977638702418303658902340239811692220844", + "655824600597917510723678485262083083743952", + "1033246441925900114833008738452619239471890" + ], + [ + "-1585257121250440266912853810148130987274500", + "-1326743874004609306830536243274942045369864", + "1079545926032358867352276390447033312838232", + "1756371530780593265458027697387037149417832" + ], + [ + "-1897793266881963076109714314739855105699604", + "-1907170823683690227784962700729072058869056", + "507539612276884915110614082356789826918264", + "1212650135657139081498934776685036045994508" + ], + [ + "-716523899769995322470859527479521143550312", + "-1881251878122821402646218654189229207388632", + "-1912168533390286258953488590575201274620288", + "-589355223099236820771572257660682589548964" + ], + [ + "1052942901159888244614776764043286976601724", + "-84219440420543475445137235041018597354504", + "-2066540177010626987064284043810507760433688", + "-2065624812095318723358260182177183762668540" + ] + ], + "b": [ + [ + "-1330498889466352512454122097846217723617823", + "-1546339266322004811505561761390574812985020", + "-543176625502656795852116535887843765686620", + "446033965932170014127418741872194018182000" + ], + [ + "1100759543670571796501721669790270952165027", + "-519190831306304390341015865602406864361551", + "-2550509492764528207421932527340042814822904", + "-1919555357352259274728001786757717786706752" + ], + [ + "2291754506564268258975495191741766889914072", + "1412951429173928562016267998154938695157383", + "-2292627178924793745375352853787995711809402", + "-2623995482834398963424228452655359526404345" + ], + [ + "1514916810407032686181015952624955405396116", + "1103915510865603036969939588471028737122425", + "-1001648664880068899720806278210463048276577", + "-1338100019526350768497278121178063305681694" + ], + [ + "510915581189275387915958925913683183123889", + "643256717277341145287190378925462446558589", + "-2078819234339137542314177923298756729793", + "-328391006663878455688363650269786394266386" + ], + [ + "361686638726759026920469451540125672873715", + "678305761489846758297159507967175798155684", + "231174405681876299758216646083380797859482", + "-118026075900257475317981787517485229552914" + ], + [ + "646791723212565037255682494052213470576405", + "587280545282396338517889665522777184052894", + "-118275152694048650285951078116078657064775", + "-384426176552006260079045067351087057696353" + ], + [ + "423703090651272558243753012669874010094964", + "272375655341268959506764834653603550238631", + "-497959388298199326668286792768413133322936", + "-512281217654946539668186858293099306024157" + ], + [ + "-16303249696117988335499499437004454595006", + "-279268604715228634865285615811181768970408", + "-333843508941271531758122934171976687332458", + "-125942702266736098018968937838171781126451" + ], + [ + "-298673330848086444903496597382517297855077", + "-272042532236155254185486070963806924962130", + "78696703130520812790822743600521407761518", + "224987820858829126450808349216901563066854" + ], + [ + "-87745241763324020384564730336940581383477", + "7018286701711956287094769586751549779542", + "172211681417552248922023670317542313369474", + "172135401007943226946521681848098646889045" + ] + ] + }, + { + "order": 14, + "denominator": "1075114750327793955376458246593336860216422328566904681431159073390431112513560167", + "a": [ + [ + "82910351376358711969099867370711195251291662881843062581073147332954360040240086", + "18152798695820968855734476817353516689049903693120918519282047937845903334635242", + "23840338079479778917257798810632410887701354267950813467433595780377761195612336", + "42037871625588559586806113235981894288657981709724193361236187202109038305944477", + "25613165809772580281258988194061605648640418445350830902204590067521622265104364", + "27355494858358756464447001726562695867608724113515524004699490435997382971091430" + ], + [ + "70686051829005435164236960875486398855075332213424472791547065140743950911915426", + "-88582655445966549188965005466197730233207598925553012244636070497550361434781061", + "83209132353263948346787963424092352758192761712932250006991916147687762552157441", + "-95853702928293418473342601890526926385639374782764433406441683853100143523140538", + "37396230011218946705474684932631195986249878973164604317656904303087702487380715", + "-138156831300031661576464188480999619900694085862700737825427720692153107961806481" + ], + [ + "-74975616986898676886454209907489485921269495045313585016279940248615708026107173", + "13980450363994887698797476098689661676416761379439609822385654845915916826750756", + "-45921958076193352277882475905755055709521196521972867618567039975384483968335825", + "20071944087135422633672498479418720795097597368298187821841153614365452135370703", + "-55540937289346721780618399566678762345990942914075626002576575703170895001180448", + "10374268115118502622673015236409857232236892592312886221225542726349983302975943" + ], + [ + "9148991230853484018181685320884248419474504188899220543434867057556059191435375", + "-45020324384956567169997443758810183909231837540451499827890399038172393470453853", + "53488470283321770544116344142477916591799224238383758798575211822669166576994655", + "-50328020899651926068388259104943494016807952440525761828994385931153343705100138", + "-2400039885435644095782808760373453475420291208783330366086717764079430564351287", + "-12512030324082427011699785821986404933337892853149145724813320036549532923391557" + ], + [ + "-79209553227748193559984493095360519615692282322756217430835677395657375729077699", + "-7585533788390923991606084197151325511366369236820521512898779644345677031359304", + "-92592188795703226786028540086039801882657162113853548770680530736866206106783747", + "-36933668781841405216209815144126455805187747812075925469076025672711376682724018", + "-43687639736821117498464437021596251341997577250447135138713763401149329154651441", + "20024249248979789541857046988810623584254470550105512747665069024316610623741353" + ], + [ + "-211878334932171796604130821179666788166590396551046283348731988312958446987818013", + "-15214064735571158533616798887704582218797519102036765049792642561055486115025406", + "-175511601911941630936931346475832598688730581771821887661361201072565818395773219", + "142824830398727564789053479973484495996230022310547793390207821762041546349675483", + "-44622140222177580067271388021577421544993612723172075785712214218906196620105169", + "182224287653598788290328997960840877807574815565372764924130098359080321431463017" + ], + [ + "-305634865360464524888673100786755810091410700135475947901325641429706483150430444", + "106165945415124377728343634930781490327780495009541694290365592131624636346592436", + "-51017983233241931659081660930973964499193432947451585252076210069315114367710800", + "229396610307153367480010225199553175236455388531989871890114252055727261574759692", + "9183855785594219544053906419725872768190553068694778671622304298636939707803896", + "302094489591393585561227388154079560570334567526309560661915670903297419850424208" + ], + [ + "-324882887541969892790701664889308318832894797200127627858897009891051621246173304", + "199973504640792794569587250613364380072541849405462548767047993770538137100767760", + "-111642263938717780478399314656638629303920169616293054062748188821158821163825576", + "326602254602347897519372094178778865102781377869823397604433139505986133265417974", + "-22040766226790405942330357956659793963061732689119676402241948277812407122167312", + "373360651183721310869392034115727659579084165645095505155765830049513458768421596" + ], + [ + "-596707663323826701121275484421321026349903643279914838301253140537044479639581828", + "130753114290857634276375266861416672525560156595841284462300592555702583728204670", + "-406446581998600437544135525743483647350547018744113467949524517665937874272437274", + "425225886468538097450010018052719786838319991154905706672206321182543787099715684", + "-167609935476585159789200100079417995535603133726940885743972760532152838720400950", + "609812270459632318999758872725908905306554783999319041519359370719719191382677626" + ], + [ + "-1131728360498166439105982000321304827077461964301064422309163802162090431742571674", + "-9432025625041901704110265509919113779447587550765280345736427514353604925313508", + "-845880516518370144514878285693029115914759494865537005807644719268698740486329898", + "329057585715406183136358806960507037425741350410130559624993363936077301889248738", + "-346551354873369204485531737099446186288643262173586313050137708266466044736907928", + "922572095276590043332182477795959518158285871093077209774938167165009859377302934" + ], + [ + "-1042246269421580017007901137164846788614884660556457038486253573245230334579522962", + "-388376224744473533656881535945800073723968306983460816664729586928917706953109082", + "-1092750413226765590265374215521539977303715558779882593073669450529610927253976762", + "-110563813470984909738296061595207379031633491887144821069252268802203121516292624", + "-581385468001838616465814188991143672695390052909074547706993663276067045444033586", + "465717854800582358429920020536093556334606880957440193904523871203028947114039374" + ], + [ + "239213431391269497241338845266583460506737474218525517080452230857647831509079466", + "-594039233489044568542214828526813907588414059643723491958217926700451041211166860", + "-288873431675245532103448016348770764105196388535024468652413822553625370860061438", + "-905546924289950408552907810836130837420245745355258685440323724492517532033051428", + "-464668531839109880632169925131998346338012731127485784970252054782204382942055802", + "-878310866209071463656107967225397025327198025066537911043349310948086296307803154" + ], + [ + "941930372717132154666227873359221351706672895767072701142238333964581906216458006", + "-283657388709014163993162990936761481735320953020601625217750757962527714889676656", + "704360137762642106729839285767943038485405320300443687323744481821721493516781514", + "-691443063775704603634933534026353696672176393216704509824859747790527520645345086", + "145855753860000591408883884720683252233178649254864539103882198943509027388476866", + "-1000996942217528219273252238629358364813152554430091779243877113419630863311960230" + ] + ], + "b": [ + [ + "-85630168941228012190939896596619873301660951778898194703864989270929928049801037", + "-254139181741493563980282675442949233646698651703692859269948671129842646684893388", + "-333764733112716904841609183348853752427818959751311388544070340925288656738572704", + "-588530202758239834215285585303746520041211743936138707057306620829526536283222678", + "-358584321336816123937625834716862479080965858234911632630864260945302711711461096", + "-382976928017022590502258024171877742146522137589217336065792866103963361595280020" + ], + [ + "1396997738318463527870941771495977758820345789595444835255981703338401889891694979", + "-389194839983740881615085987431686125701359984756176235479776931070549270121507407", + "627766078554629203163722488332976063581643521416052040995991457710573305508718956", + "-1123438654256864073106360783035114244767990742182633780868722707802342352996712488", + "12460754455556216850210708700034699525300083852903137257946712080475063795468448", + "-1503128969371683846911586642157114261332549287718176102777882993850444153822961452" + ], + [ + "1361603087715849855447420617379091847161870639145191983940244187449065423443332268", + "50059144680988986913875398607021074348964429390934643029699927147721108602998449", + "1129629611932731858118411534634120803277552839412359953878912089360161041013844896", + "-435087836670922201664280522112453623776025826339107307014902886193736572132883167", + "548619111344438935160386781205294578206658008242785605856093824354686515879203502", + "-1025104117017632645000957248835184193774700685999289537268834655590047058972467202" + ], + [ + "413231317685522496810044157676540934927931988416094588446279326675654365189940347", + "332996179285814886300015748358139929015483875421231819230175049871658572414483029", + "654824830975328657378100734382378254694352678885799163305895239288964376132521825", + "299293604339728926107799511525791774283965358102527713130083910435479276985479124", + "494954397165173834150098864298445373860352443126634658308421879977744781335298740", + "-18202323220329817018650578991708223707289220415091371175643731619216154833809004" + ], + [ + "-5825951336745290100792479499179350430478544681095124283781176372784367851387145", + "365681563865134070380449608787823383682213052299769026732417958203289060185766848", + "221279283903661029736196084282697284954987075824883295461878509642086904680868948", + "512737140245510130179629381275777496999567434027767411224752619487158127263408708", + "209572781641048734325789054568319627401135949844259398870332175727106792822013582", + "326712325999028018150226103116074836413516049337651429442025764063168437359951310" + ], + [ + "-10408029631305135235855514237379824663363928336608819691018345549872986662570699", + "196704590887103177360039993440238406209410216961115702041006865787004874413233828", + "165756477756651245337926278121421533069364441198759650207055531825255976848661418", + "224654543328538433454193471704411462573782675640983443033451565894378124932976946", + "91259424106210855446036347236307891022621249543210180849644853597722475073911855", + "156180912782732279378703057477333644276761670976598162798604450276405681856731185" + ], + [ + "-20566015586697879750359855139086931524375845075766824405206235150297046449096093", + "58986443787831980375938462221755122908598652323805722620505926720125879953470936", + "34580284544642452787543835064254795600022212094698513550862662918541158876791327", + "28697513749203584290346050105743741168258148279321979624844716944527560959860383", + "33829710989691953179593627774015773772079286868644519371259257270471934831318475", + "64135461089565494295415082943701854015503399548045646093318235176288582220078845" + ], + [ + "-101206263634559216004215127474211953295811735336909731158075800300592461065506887", + "56255990884529232390170178955996531723442182564226865078929573744878290954874388", + "-77169028070385093006892582813920130329900110286748462623715950218556418579052697", + "110253195869621311193047610003021626143123048454693008034543136129192768279463734", + "-17990966428387953029887909922107176444647339810434549932011452148720471578554483", + "135222673086553603903390738557010719629530722476903112481027468313990881974831182" + ], + [ + "-23682908992598486867717287812772988185546832011043172183169012222450942503827497", + "58501436379054206928030051111007230523422924995834021785009182735984099770174898", + "41380703447245474023066226891298226436980857238562117897671434605822907126739789", + "101048603269648503350527055685740346047556133923196256249667320182767361495812414", + "57817241256616208897743087646187167019686796350603350782178425226660500152880776", + "89428723802913386977030746115640641113051405499245509777341396636371030164914179" + ], + [ + "105552340988538469090428006059067196766119770994018393471429711107675021798972159", + "44287541619264381009668329737514766251405464502407866792459826133849404388230790", + "119360318056970544334930786211039712618408204132495526262877127431887710919819948", + "-16963524351466291806308437615901322704454083140489172461995248724379753488914933", + "58636311781273823315923156379433338747519075216344861930434120260830113434351973", + "-63940978616289343873291105108164209905881328198415422720408742336081142623949774" + ], + [ + "86578239764458200682854249883994796620280959447470047660130366606544946254382412", + "-16633727777441848629593606399254003730531900116701596787848313679864361023568078", + "29465901271803749966817644586272507442830892749043782023194084109954019329645583", + "-88119333099307566214199611888366957590985216989619134138836034441358124141274551", + "-28665388614557661368977631980425024341065020818868148442145454385960294851785986", + "-100362632812831188498545242369787368771333715963727083015054196495849122149007030" + ], + [ + "-50487282175911128237921396853426488788389390184581723501058970947360658437430122", + "-21557427533825962147659902963351733971728961326384042698911678674604540201092213", + "-71944536536897082026039966589527885008032671950467077856790160967069257152689578", + "-40122696611588332033743343711889748131273526499082837858671765754414536499510535", + "-42528212848486743089150477054821216541544248711830362312518845578033959818957618", + "8595115989600817363305558115057255315422726046034442615552398673312718701186481" + ], + [ + "-67280740908366582476159133811372953693333778269076621510159880997470136158318429", + "20261242050643868856654499352625820123951496644328687515553625568751979634976904", + "-50311438411617293337845663269138788463243237164317406237410320130122963822627251", + "49388790269693185973923823859025264048012599515478893558918553413609108617524649", + "-10418268132857185100634563194334518016655617803918895650277299924536359099176919", + "71499781586966301376660874187811311772368039602149412803134079529973633093711445" + ] + ] + }, + { + "order": 15, + "denominator": "21303110977467217422179365304980853459710951108484250839666947703943501024265451274389430764941852454816792740037581", + "a": [ + [ + "10943827027812969078757701702278266309346416613855088301903596515203149829265733833235937572215781736311522966558474", + "-2127109371278119537898703678429387192053839547959287528863882847664488370255697738465769674997987612464504091999137", + "-3184900876165506497671976120857424696361169926230158056848340611051095468733343340168356581615154068128767273824844", + "5473320309052042323566096830543472434342904746826540092126612778813267188202962094722992240415897605025164554760171", + "-5556089388642532929152735825315137827395967452542863044511570030373031594305237090518278678058381562128005626959709", + "3100910911074384933279512901094951481203446201902157060054919908540375189026537826459834665265488308224427507190232", + "1777046229240104845950473108330487301294699141832799456582920101968953969689834705617218946041098023058030652920360", + "-9533594339518813939034888554256631270121375640268913174250728368334400589236302223933830640947262148568569927914930" + ], + [ + "-2540671321600375115857506504709875744742137904820623115987984400944108053532288881419282955825090220818915754241558", + "-6897725285967652508268605398294521966871150541504150459311516145770085819184340357265356783511550962927945919741208", + "-5163198709113950670776397353600070289184223970678558786101774450051043212639780782152929886085385592159665537324902", + "-3598023721680825843668766500375595375869610990336247297705455651322572439312684539573904664802844324751339025113477", + "-5765985303707587497358810703725959254005606913477436438046475001755862067073046990711967992073891888389241786564023", + "-3168152381548071189268907151393649108230928975968855802916835033605556532234093733176318048263923066141961549836093", + "-4694070921780768081157768332714247078787397664931069819786942426308749498287198409855168252881554616821201282226011", + "-4941851277423425636838000047828498108727602095207606984924866854260086124001634132939779747368395093301718983378306" + ], + [ + "-18330335280376332199424354022595336545625855434719016076611933323848365036595534167192366221047769038241740560330439", + "1825922444626067157710510766241034906888692407044272022905607880395112293198462283288993819728309820726477495227087", + "6279270676062054499323725312902278187313322863254752652811026041514013635579658517728384319147551502786309147890034", + "-9632911955230779935635851689421574235247959007115010613302222173674954295170054078224019751364916448033033119733366", + "9566508886901223273716174831753383827197607151674682359107611256797670169259610480399192792064338797340170350121779", + "-4715552970364007393445205398084718711453015584145894079548515575984930998425635011326068418057409438388957806493393", + "-5522402129289376751094389002518337706739905861804077075654072472783123867690421671150344850399630924985436610360774", + "16922124341185736143937218671979070222242592885775039065913395670615307921545827029589984378510041358331633337563170" + ], + [ + "-2287178482666489970096882229250717611188401291483818141775888772049997886371870213583329111096468510776058601234298", + "8653965253218249845191887853462334173037550883627921954504541879184058073090824285924291721255246370640916350547365", + "7856902773821109485830588078090404528489860726232209446401315656386818484061843065380604390543588284811639784170513", + "2949237983087364944797037893467074609033513176269936845891768368405679259552264840467862049814311232263363315536387", + "9771309393487521178735491718460705281125553967958895353680867985044652583205383355055886031968790204008392437615600", + "1342221964921624650022178970624674759541317674324427015267321205306101575849033586658094385130546003920978869574038", + "4524963550427501695078186095189192303631454278830757410717761118399180456745343954926655052883738390505398331618677", + "8312969092304546059885376608071152432779130114375922217633870544393720325627551533427645310706202399068992838567936" + ], + [ + "11688168253891167233060379247054602180759443052367190428865035612468493332776276091287666426699269628717385684654497", + "2901781138681109165849876778956804620927218962331186649108867512764911382693133641299749930329200076341849189441896", + "-1292967271814135591699650721270195404948864915437450659929043035820191756482957143128213517243637176029513658592888", + "11140682044613286606019440828317973578478875686184955940459464417137917315141346377656402045611930440831132627828848", + "-5470052118305088007372266001518745386094710525431918457271794738743740047052651536303402216226698292353869357451030", + "2765353148617552572848137357023953517212395763043901269646403667174800630683305595981244297259301437654563466718527", + "3740272040814301612754416621940631383248713721001754408148986146437772259108157771033462887038143884481676464010574", + "-10464360664088660127270279720018574568308505121626124738582615357894033137448817803862939559814479371509544450104462" + ], + [ + "715588198922698522519731350881446160464731427151318849443526237390216286549394115838752773337393575698395843999783", + "-2359818793561744785077511715001577167313153003072255298840785677626543054289211417283527246275557913643427299027575", + "854314230376279724629274935146133582999008592515139789036348793195202392181257568876435182940697346246234758332856", + "-791444595357292902731791364793401011309535620202518642510929658001180296791860940056562854017875810681594947124383", + "-3132843757952173761995103907743042448686497402165490813418592555666575554856748031297494742641705372948219014558820", + "-2188909334038934954562301649937703690306923653466079313535065767186086090570333229356216576650298421466084314084080", + "-4074443821239671417553029829390052206806265041122832079172022787421583177375993360851037554042118617446170402670249", + "-4251045043556893663507291708619971202563545869810416657901348130829318882791290270287754467180858056046269585581124" + ], + [ + "-915006876133992589860193576150410430042739561792677034827350505751097237688145274943584715527714500155936075958894", + "6466907327672503300662714054521820611120341625092360786836060243018346250748620410503489860997101319500925435642303", + "2164280023266389331315611595146554189058842802498153742076836288954662003157803486457114811152770499561210502178460", + "3909725197528622100898835681311721306245700027463582483560353089106919235409615539803134528637642980346039024961373", + "5569076630582571918500731835909107298275812378104240857411625999300899065324833583070812215132637238770598699396159", + "948617597425315239750669713495894979162125762861308679439689834337378757320656923553727746827832875261769392819950", + "5079300847936150241328670138707364825523715037846446997498069628430886211753139663513067259014453219400943423447676", + "2495312526249291481940016122277503560913253780323650707930920280309615263815874877683456102222767228040264285264983" + ], + [ + "32215624363624450128946098547648945852660384553463364588045317080233651228488024963191188465115598959820641699763346", + "7614003891395851666244267824574503029569408965611599530917339864018707003902502363375646595913492505551107316879522", + "4211950971298727093432055463930953991085317135753702818871444862030014781160937666087612956912489195358860088376737", + "24312143601827217937930931378633167132465606844742430993908971666759558030905325039772745669668398908399304018249390", + "-1943284240930035909217083643838731585981235833235268553511377689617353032545264223609833954725427403865037073693862", + "17700334106956091356324766781534685132417321533401409524207852015445768188097555552227581232759553889453489317966358", + "15937443232054934677791956005191541251902260099968176118421895131643482134481730936529861402767957221403705985479709", + "-15600896628450833481855243579553698632660884623302125488880997434850219703432121282394530683221649351918796272700700" + ], + [ + "63452177341753389206607880630646577744516801955782333138373560459155024065649713376324972363838626390059866503271735", + "8760266674245461878142925664903984227094761294593877203672991437159034488302755332445423211653374075720751712904485", + "-7521715911212217356819587114183779952431966004154587476319037790544350516107447523248395215596503233889696808322495", + "48859554861342717346109701557872923476586773929031139815910979867742192221184772797453555186008251372412928338445865", + "-17714376607466422173024692147388986847402455527535922652409109789334797523388593581851126135016824215745415824213675", + "28282781640413962683732796293807222881087499511157927296228591836668061425090668401248266779838303252077107270020660", + "30261830113319765666677341298553957838108926854058202548798731990835908184633909046346588819180165293450616919167320", + "-47264213360528691624784690812013515230240587574210143857607895135714039209582696650314388731139741456657522128016995" + ], + [ + "59860529150965717691905961973470925754921918601620752110941683222571679351980931135353777690857771606029702114206830", + "18928111205385267335735454206525361355047836106208576251030407618112207060034842154524604783454247728748632125424697", + "14995168909946658849972884602175046431753311064512151473383693966033710992181139968846418121095329172080119563797106", + "50303880558465809329780224925376829636170755276355745464019559466760866516298642220759284216422557003934904461680317", + "3917458329575977411672383172560601523508540779485221913068875058258870579098723260291148781325009331615714220292299", + "39512999637477206745512155123127978369413165776307249740619675734543591693651344847286219705551896299346880330978447", + "35100910384557980343236767748557190731273781995220247470133827961104193228092199636642725831252733411120411417112386", + "-24084013177052685189064253360029973804116778211695661876977907493807640092945811743953253139866111407170254513413498" + ], + [ + "-8417654569991766483043229857389565494925575090038597553481781485394194190523359615693051780086110815034008894592543", + "71736250405349862188281466813297565003081157171288064542392155226454295080215510328996691824347457440639008137096131", + "58641342304189823200801668968693574237884431405926994471340991870960708850284416041438276093704670264231671264676317", + "33033015804257422560082823010602179968158337161664957332627058042236056284688893952194439281272672160533622975668004", + "80883404230348776512007052938510889748833294887175983976403004055732541523725063188211718828732568770160933650843297", + "30218827135357765692972501154436683898212787261708399040264560447230449882129805699945880463610189713302121125339676", + "55348513818586190784259999015297230591214033193296135498505943228146927037301814233466341620478349225242317919662102", + "72695556916265453427466386522193503969429512617051100737130171298148928018221155582598474137594306904525813501146240" + ], + [ + "-145886714501950373426387064455276529157781028966371024690919040987991740507804373897736202139935000717634060889082875", + "84521524748269697313977573199030300163206143601368113307656105282650103329228162663505338109403992317176672296515975", + "107116659859765249511539463689975013379075142253137552164898355324179915209242201951690114971283704628483927966028120", + "-59819463782245818894099466506339619162443300407478129553113276848433251382278239712686948813061106144967166675927295", + "159481533554345675111201807277582954926980790854138997949245296083171181545578052210041277152151882063920533960528005", + "-16780215513473823940980105363398694896635490651142101696644978934798008213427534200272308573441690415647546715043530", + "19755422789125280906508832020890999532955373274357074991424741824518419033290259939391685305516453271844824390040410", + "210608021407415115426958160229355185945979418420780814596470088783421576058889725756910253279577265140280479309175985" + ], + [ + "-213753452574218441911966600045685073411355666244859820071515578792520083982718374612590031269500505350134118295534830", + "9666590042981904106453648259682299409262137385652626264993327928605592364679811638860725722397583925783872287394735", + "46187592949735059358548267638513384253465688936254010618861226190889533928608626357341410310761689975533475535780405", + "-138787013662343258656407547630130546589714748421279475470444082207470779797352507249815055453322662273596920722181265", + "93107778873688405815369468615963256929818339964880351558925483201195540793762259965120990340535610909203538724417185", + "-86880185880236373642031783156025009503211824636678279136939822295768294910506138396082058124273912653762065046807745", + "-64382768575465599703015113687703860533318603233598040926942854171421098298756766470996263968758040516494597104389210", + "181776560326794994616578128477274727094244385069449449801678428954721876821405341503854628593796508775068600690706970" + ], + [ + "-39045684380918233605524458851946815810107113817188308113528138153093807817796908273184892376568710962719405551713040", + "-54328787576810486908266295944678376905247451245022117197565622152637463574234061841194381480666967160671813208126955", + "-33598526871697058897270563342373439922468381814169981894475113845785264765817929365482807834791058386634800966798350", + "-54010293242861200504479140158424488813197836311174281846121392451300598949666221325163360308718705676712906045727200", + "-41325862934056879098040093968549416785858616516002346533529268811207979091619528284875180950592324842162052628176085", + "-48226577434693026428222628747915351970970551389788841371362164748263244271624611307113228296324320505744227178035370", + "-56981019443094744721393344961809380159647411416734227066708886277803266989004386877753414433940407656665593177493285", + "-26588594485655674294410742615838224284219115649224643334705799256508808716238812978051039112409954690530282903108365" + ] + ], + "b": [ + [ + "-142854294439727318759186160229193141180485298099342073688887000024103746414720556224149632818294873589856051758339529", + "31906640569171793068480555176440807880807593219389312932958242714967325553835466076986545124969814186967561379987055", + "47773513142482597465079641812861370445417548893452370852725109165766432031000150102525348724227311021931509107372660", + "-82099804635780634853491452458152086515143571202398101381899191682199007823044431420844883606238464075377468321402565", + "83341340829637993937291037379727067410939511788142945667673550455595473914578556357774180170875723431920084404395635", + "-46513663666115773999192693516424272218051693028532355900823798628105627835398067396897519978982324623366412607853480", + "-26655693438601572689257096624957309519420487127491991848743801529534309545347520584258284190616470345870459793805400", + "143003915092782209085523328313849469051820634604033697613760925525016008838544533359007459614208932228528548918723950" + ], + [ + "-112795798722625875602907890597353238236572805078978155120705195508256936755008330407861428316982227151122123934178906", + "-60541905474624858230999276475099837265793654580572443714007280040583697727396925004700885034649402962081158541874569", + "-22896143642141689982758454877291324540817703208869316871110845547346948141718363612272025042016313788342738678529470", + "-112336140307009445446285312089397036178503315889291811445421665730183527767187185477654492927186352951161247034707275", + "-19183166328705393808882744591437131482353511193585599322210928660357565655599015941029957451199218432161534936638230", + "-81974846527988009706272221835685552331765642624367264766528174932713258398253516381440164163984500063770717783851990", + "-92450821493584889178092400214602725568640875531108014369036786228956084654287104023819171609351467253706482499381865", + "34070918199131887696380698641641214007666832239391666332226289577826030009859670405592194295117251833715843545909935" + ], + [ + "104298393701639226459638208856591475382725865753847001093779956659275679099179134853400502455522819005130848619993025", + "-94442764501422760525706396502926367161906048064393411604159438953303350784028214835927262346005372755275983058458786", + "-90808862943897817056482795481585535347474920756441838774717293523962018601402052347282187449769092871111047414256663", + "23173997640580493271528537049098111248853039519735711842535003082102568627348167121491423466425003976092958233880099", + "-148277226634245596732782064669684966515893222481403782319883353602454767647289100847020052364521888115727201751308415", + "-5262815058800214891020683434049404026125908974994276626666308100844911980516815896055130405443493660942820035520010", + "-51189282909950801409587256808843738336162418828829758765561464370917461258891712880000032979199522396158109049967295", + "-176906664788012600740702039145136682005442729037828069174049014826102640760422412580447064294233251349777744841651395" + ], + [ + "149704127345716215448920055980144465362016837349268441566169423160647002729602556782584259050925986774134604160544845", + "-40557713572470901666392219326792237835937214369643504521246753380514418189591202493632040470122126036166901702610789", + "-56595095031323814270977460777889693440649032615734296214986711900886943611539162341361502732045511757087248229747199", + "77499612920526782493502666484673138962486016755006429385383904482070199571033582947125025856303550178866638620663631", + "-103263435613824137976598795026215460916022708773555434210459455499273789798376536530773602588476676778057493358264531", + "35030382421713490677256092090893434837938317414197593771051408470946588864342679542009013384637295756114278852370515", + "14320641738593720342048012711975380376373753112442499053313580002975827157116094703680206131721558871661988772077569", + "-165005205743794578098416851716638736691352030222225164622795933724980399302888340557179620838806951480897057674672684" + ], + [ + "96146359740939612355185287148880230525126149755111860060147091324581071342688164239807088109766403518179609447318377", + "1966863451595441489800636641340932643587868103714419912933134618065592469350756672536434932133064057459674668332455", + "-8986629393981165814136725046644384086440251501484944805810038222059233367726324187873566370540412763460045652519471", + "64584282713164701189918074304754896625322452678702734052473505872695301559631005545777972670985685811916242168009845", + "-34933410575952519450702108897661062843955117320926515461313786439066871546295593272382769057268003316247631174905350", + "43237043347944062719694148949422897529639406429060465890276984403032765062392143995518539473568286753339357346536417", + "30798479370723125342190383759148365274848626899597933584911400213213981648963129605374365097597159478185104553240959", + "-71964363939714216588137355588354516399361159528741215469116906210509395098440757536405633620045051004907937648921676" + ], + [ + "61193200925805804373002296770541402835660571396864041445007899046378158960118711118396325462228979502759095721333840", + "13130250651151197684559803900521368149531123091825844634284028645896116074616164257656572050836471454897918226025931", + "164352302084138567657354198468228260592319482064613477991737021296036001992714360952617344173180627128662402072183", + "45950365650646669738368030405103221582488246118871466024401579992723147720469990405419401890385849623830380408709065", + "-7953390020986349415589042052701550289748189615339142502596838085652577408907697718348951273261890193891473997827311", + "29070165489773961581116901649689041686484438111731213535794829898954359795530941242796124499083000641747710613035284", + "31762535043164114564174955156964948490736353838159809459755135057194494341546049201178072615536954483646867899711252", + "-38363496742825124409020313576343045789776024448529690688140136868946484786073143265024074667714170607459019169458524" + ], + [ + "38346084847529911022428669979499031686740489778744964758214084861130205773476425384552330787536401798620891219556897", + "-189262550626984445584751824957263115131929031231264879867550910897327600280588445012684510499916293179468713465916", + "-2546658653949495092613609573958048121803335307270857132330219034172287471700011709855284218362853388225435151660657", + "25845936959302172577342486619061503485840117587022399093497028322027872959426943041757018773106147646034994770985952", + "-12530824907137563018927259249668882996076942276162391069910894895942243712813509167988068282613035299886373724785456", + "18021096332316469226118546325912676492389636792550531221434602680167236075698395663211153930851578974605025915004172", + "11746109784726741000916587338959442460081823569865265547439047762555800553464465430743751484095876181643106386768467", + "-27635475932074805581760948052737788633816799495728115756746949645051143092182036681289006217183936493709555658772745" + ], + [ + "5384738132744428979742991763828913748121558817852989168741542636334495338342266564386012780137524780004980270508701", + "289033507602504102607185454479997931581808333014123873598110821078845437175895903212025748548110323933867217191643", + "461756048269783923732837476789226589003443719170726151016694490046810202565253904796597205990490896712886758243478", + "2016530381057852687935831037881447305606297255072976033853113405335481404456348649691040431522099230860204076801361", + "-1733174049733431440860241959650270917449363444025850680580670720029922567560458021097863618716439955746375763023266", + "229033425529981314928357234682187342811391886976823547920893847642984540937877224523764212752306689783936665848253", + "1609396909491710044718380645479782923279049432067219992128180937443461835628829655246912722561501804744797216232080", + "-4442371461933974592326639989938137631505859716138473410849826971279268740867337821248737656950290378722782850585138" + ], + [ + "-5215125938563721366558604590880546986954921686677818768243348835313726948593438647751126117493748898673930228801455", + "6209872774037720338124986656483570821421552730280291875638650418536188425032869638763103437116036834697619980121901", + "9627788879057325731805488921084518104548071174778137876727532725588500660677333385437023045379045900621565915767648", + "-984055763131380708537968532808673119770992648923012767456333270846997623939944058039268785894064861631479419321589", + "7854092182200945969717432684875178505894632521666334317367809735125162480284486468550892057679103919446291933545397", + "195893158339345981692324928043048166900708844563891858429319322252519329694167496666187057579921855008106200078088", + "-354253351982059818348361773905604576216336394112602969373561366035968504242967208701390201381653932929150795395022", + "11025455245270213032853255897068771180338201435061751214380759984069461010193745413997541501877862301156517341414104" + ], + [ + "11655637067469812488009918481985880867387076684055738390763370576892368625693800004746147812011938972387485029562001", + "4609462362525687347108770734683363062330273108887979034649090773459761883969878035686130782768969691119051432094968", + "3970992874937097199185171932307663441328090390462196623918672536655476786244318257305129789846787576561966199832054", + "9621615236401701309009167339908038412367141696889774981765094979804491659583730363218913545959093126486795055534857", + "75575645554850606741636590649570326278002169846954142212531933068723044290468698849644061803285527915433416364120", + "5053617199737822255728237158468170489878055488717324227023330177274159642689351926472328765464783320132417694495079", + "4674633538971255270939953159654475432795248347410891242990944298952720434378830555448451130055524612781665878459253", + "-5550110478199593916489228400355263920118833080729437666953755799464784043596213056365147122214297085661431916496138" + ], + [ + "14191528699283076264771424922170986157667449247240893228252809735815261240058113355853117427224711154271988357985942", + "-4951716680939029254266157360106148164655701360173577031470847826823538498089452274824873416679972224644352520320689", + "-5292261351280851947913787883952036085595921601213966779534064375316358763082112323694703853762436269285539527518194", + "6936770549170813857282856010995631974890821421902402797795011140234388690173524776471304754726745419240912645379156", + "-12205711654147683520766786471083810757323630551379098580525066567754262671341650469458579830369527158503672203643929", + "2675772532016547375391699711350961911276089804512431348630084292899018361577834181016606005286995292429175650919219", + "-1755531397994442655473535709225676437432085466660647761045058108239580342809851280963316770320048453517737510114737", + "-16089939556215380019663889085545951122624844658276339242772349670270122904274422331575252275438268135171148011124481" + ], + [ + "-6903690294077445291774347356856252082993655598998422546372424736548071716739626826812519001641842393576869209104532", + "-5264492158914141459449773857756710461748654629219501261542155221465182244976430450515807183111668291339349475223783", + "-2169045243489926379268040145094463354805841750669748771738472747219686609475549888523492430346614815179075063154793", + "-8464391288581744895781526973503716115252261637809405371188823857618819320233192849682482970961303936632539316319124", + "-3416172410109550369047506370614838264183474644628864848344891907217642510354438841210086738848161259767300795886465", + "-5725116782969136257863907837778786043913234458857705658651081569444598298032150431410159817471475166166832764719651", + "-7525730169053718889147878268875654234822893814904554841730472518416724767411646649646062307199233922817159228813389", + "1222686060437719211043581585258620051641174268785200377257022745720710711665720389231298259845528538361976286287502" + ], + [ + "-12978712091491956630260464299368586543040550877297802965603095270447854251167876498761510333678594112825251771451385", + "3340623669536650500671102879637963558908269724159187810108354568756027617435548607335716020003135720731503033709794", + "4388053134516516876903891279600505025417769029742694856940959577494680739824730671369480229941003454699936246456252", + "-7647105863342145239281587698965203947129778458910749165527962923374287078703417917069192044473692081759112889634731", + "8001365538592044025034194250269383009746508144405076717897335041177342463436312406056753112736436438444841203320141", + "-3578029832773919339677709958895465006686807589734321222078916634423136518916096555831720657067790490006626947419146", + "-1856006985117598832755388693061293589681782792135970257066458832979355130101184517219380442175371988485691616902704", + "14091631361594036229770239931080505557838613793802907044656406326331491011492935134809904571785643471299459101345648" + ], + [ + "2603045625394548907034963923463121054007140921145887207568542543539587187853127218212326158437914064181293703447536", + "3621919171787365793884419729645225127016496749668141146504374810175830904948937456079625432044464477378120880541797", + "2239901791446470593151370889491562661497892120944665459631674256385684317721195291032187188986070559108986731119890", + "3600686216190746700298609343894965920879855754078285456408092830086706596644414755010890687247913711780860403048480", + "2755057528937125273202672931236627785723907767733489768901951254080531939441301885658345396706154989477470175211739", + "3215105162312868428548175249861023464731370092652589424757477649884216284774974087140881886421621367049615145202358", + "3798734629539649648092889664120625343976494094448948471113925751853551132600292458516894295596027177111039545166219", + "1772572965710378286294049507722548285614607709948309555647053283767253914415920865203402607493996979368685526873891" + ] + ] + }, + { + "order": 18, + "denominator": "11186692986735857979845337120253796974449822403416886376595609636244310920090200621768120321671202650050564058189395533", + "a": [ + [ + "-53493252897753294191405674422545959233237295203299673839149450358914761610908009062593079748663100033576062964263406", + "-681243212636239659012041141037866411680690833794625818140347182568056388338487362569116513432363644672641165896223566", + "-478145909830613121247232914201782662520591867888018510934303509965375518548541029661056435201128455951247307356195678", + "407828595665526895206999828067498076164539899113402766267128682053779521970429812691592420668156389396969049682080341", + "579325675365916039910356504096690861824080159115627244604848561226367550008653055922271163843844108121634144096650889", + "665828085634271233380826940078534149295879517558428061972424759537485597758850464457715967067675576524144026139593753" + ], + [ + "-114062823783034734983119907703779394857619685184894333965308892272919908230882204211655916737728001862594798855406201", + "284558715165293168340882849224440747547436421475030789271376658604412037733302226569125883769016396370694623437402551", + "751262625684936129825812481304064578504655374828638563564171875846128065940344156007853885064014997347510286184472098", + "358893553568667974665147276288188028488805656697080076448821032173973020246345330322720559855213090694682854566155675", + "110890417693076844616049915100141476551166859312396097350122620128901888475781237367260195047373382735316327621179899", + "-231067738348001464539655031172729032743483873871020176437102654529407194081964484524996345653936047393617040648699165" + ], + [ + "256057945821435075839655586305850661915823066288806264141009168645868927564242094036852422695814238734781073925881120", + "606137599504749276577533543971157827998661282926849207617449012162642572184767014181794845302375716123767476341724106", + "261425448913211024419464221132500228749463079677041269479516386790006154727254561361519598570536171331192107172754251", + "-50427442266241392329823266625375414389369727168005801656710557920844042828108696546469672558441423951251151237155207", + "-424593840995902528563920022699101632364559242035653032917415296740978571662915701946663089202002551524806918886822664", + "-272710376943429031162408470803989407951895303725170159121661266964548248348584899047480337880422261393598654856402081" + ], + [ + "566021712353967921430760446984419435329668604644971647592302353412574727262881246965891596558355634085149876971719904", + "96146607991282700047040624153265725047838071280748484262027703553824112679347383564676815863236608534233536554173787", + "109130260924605002461139772397876326425309287031107309298446994913534932601599125348283654940188490317299469238014649", + "-931614893063951852999411565938708311689456022144970422736671069698830901203935071611923258216013858370617207469918177", + "-417387976622181121759989848167752283812095054636293339550977188757032878531399885773922233187473887172134868447892118", + "-513601404020219662351999536734973941651658976226148715409305600475366351863517186903195544784050237157884062498541084" + ], + [ + "-754139405136747813467996408597282736380420825262210704736416583499230592240110232999801645957467951948453548867702685", + "-948877497407964447184817734784625083625154291483083135821871036177227614055958675060143470199099106862046470839058215", + "-772786111219837877330988159069992948416690744638092370352493123664607658380571341189641783839926748615448001377656049", + "-164028714400041983836837279929715396069673512705224974048386015115617074627449817624902356567986022928257167499811439", + "-106004939676245496003150129245376503752291816763922469254904306975652388126783692704580161718273051961187139081723805", + "19235744248912465559665188149718839620286442619962571411634509774672131115630190503874667432478091863996868192771328" + ], + [ + "-1419811261254917041388308942921123680855730702552200106319784301977184337754304839971811600653277253846032118948070247", + "-624430297179642068548092673101995475719017428897199600601888945805187059237985795683921642685036174826440571504653179", + "-743874972658037247847083980004778878700103703327630609336885405726207701260330175718181898621034316811964536847540747", + "1119032276881733743908647595079702712889334754060009369383636237980496434582236257255086977065909823659350557566238313", + "767644943534219991254949072679971159808768698271929089290763584627729399884533425542783890699626487100807384740381739", + "1347991545105248210995090792593270413985073681831062713696806771487469424910113737368879874237511507945158442031331816" + ], + [ + "-118824472023058600428264658198455212393288497688760232357722081835336116923781547429932716063664249967010389368727611", + "-43562903445611803541640332593558081782855501013901808419550107052225257371457003216327707728652733868521655470225793", + "580616075611947901559336658313912975486851425640031047787343919312250418213624483761222561991170712862178256344212021", + "799448711489448060054358561599143767205625700133295243498333778312014699528806576853646635700747405083958171759618188", + "893078852812256753920468926922810719663364992748784412424898732478211366680929515626765932297353682414238988137787707", + "647933368336721589917352773157923065047481622151552421704793159656715025797250764167312455787569621457474799314593883" + ], + [ + "-306594632921466236888447597248413621732021291592861627454248971886032281197000877072904792552426197302962289504039434", + "-24613917945408382159816847209813786798079658721600959501845602244807404492940302131558775160819332272407813472893148", + "-169382522146198884396850617374065524627576209552695093804987342318263023537900418640731223635029811258160036689186018", + "373008366461947011613016723817185847659115641524370442922860887478434173266441707720624240034984847515469452922558290", + "614932664607616823916243494203560767109685908650840244431725638932627232225665066449594763830348274672813058961274277", + "518088510303825647168942211715295053563206379420631747261748046511528833856827998447978277288422995612976461358537193" + ], + [ + "-1711560760671234570103510377098471561183949263081456061963524210496449317137012886187127395543071664784617967974994960", + "-1782783507462948731449427237847737456058032017781054516498436542016866230330991696929683111741494608963769466976551804", + "-402245382057442977985236728409188580936219531368374069494094073626251630469878657104924114272682210512347633706416816", + "2041343777420254368832713868781197873715744152884239054648255796716396295131653991124978068266250819455094715330312048", + "2285904891906671494464957795374315977591409734012350532622816758737052522818944810005639654275343374060092327894724708", + "2065369686660511510666647557211843478424704597536191657950150363256993976264148207599925604451275551535913724880035632" + ], + [ + "-2972299173180901661602506670917752798409833626630327255440887871578154504746340039171405186911932539607446912162499092", + "-1543103407041320591068086976415470616440432655962855090897368516514431847967688480036752035764710585934389135699183520", + "251470576194517534607631598970424348679278465470409025913439258614418054718122412461040839812517743160956885991038964", + "4334692534107220062389289684504938816713052078074980937264598340201307754899472541565405460272014344620711413975204666", + "4212533144648571792845129980227794989215372729270047454012133656115649377456059418320822746014256564140626998147941506", + "3585996397859981949677347059712026503098732356868000242338026748621364623302397567307787716963574090390449271890779586" + ], + [ + "-4834201823545789604972329500084617402820196729815518008998138315496075176407998515427968417550094926662567624165623790", + "-2866093754631446847793655534040395896112853198913473790432090096264171257770348930639072130572260899582898713191420178", + "-1429183392910761321108543498684114752960283168241057003563945505999587823493499022442526231634398123516493994441259228", + "5649357663412300046259241714127871464830459367461435770043358760222352167241626664101905892248879152570380254250108558", + "5803145458667214835715218227261279125308669513487075060037889376088060535870164084525961910451791114041020709843368978", + "5663372923784798367280881644681640092955404522096733148171223498649289993823189985736235145012111433945585501905404706" + ], + [ + "-10319030469488857640198400288965831249091220467051706813504571998078973159865485353966693835872036665214359233969012868", + "-10063471382882954762872888398333119388174941131187740621997469071390721048631956763911670200458951934190779968490315660", + "-7152230017499520989749436868101686673685707374720173389569594298635601049306528151314637999240225160527875460325937234", + "6160298567764540350459347615889478204703245001355652582995825421904914145864496972033163922870519352161345150499644886", + "8812176338858882139950953202095448010315990865300706841924500867661631830669780946063792979187240581206406821208512728", + "10171800144105520616454666587595697981296670794947774807478854938077199126494836389293608513382719628070259373743242170" + ], + [ + "-16028101184690073403612582237828309233197637327915832870684618396432848133136860568099223294524753113935115168850316420", + "-16954235641519382912914452848231627650310290311662117671448686776556379875875317317271639864652924333618758928853075614", + "-16274491876711102389778997270612502984425044349957780717649656461332351555746681624849722871056017354793779636662062902", + "2021258637790877059510156474056603909225719461475206717077793633716675534006172845168009870782169292059145946483263110", + "7434733970972786192381846187836191812908614565460496266876757598174041020592218375634058673735012273161075609303880756", + "12471786747153539460985392042621687027079573785373549294681517128791467116109346431607827672528436076960221122651276400" + ], + [ + "-7683152095857106827562789335454709702550625629631154794008079094639257021042733506830529119291380665799540730353326290", + "-14533959539850698145452952408293041003732606247827590420820658472237057073447322111354599213617036873237405078233684598", + "-18785147706381277962132133878474463041622875363982528289319463610924394464636672541720679230050712448645289994294293250", + "-13906327046040686479004167916927202361802619533977239965298371537627456030383198067877179857560204585192698692284751242", + "-6969420511056058015481356588509519531719143681021753193492605705575503555235892172980116334982182936205973667330584582", + "570495107011053732020897291073882168040569063444812215944152654058762966304587101994034787072670761419634152033037448" + ], + [ + "14459136801371935568609895264803242190151318505228213759132607371489102107776407265473868662874785940434606638228040158", + "6373707280281240911572176897541689151956582685209331008818730518585008596403993075215386966749484290212991268077850082", + "-2606049499773649588007321779309126374040132687213710875690285534161259365102775780594041085055239329348977554275512582", + "-25652233008388297765797114623114341738474771938697784657443574162783562020854352998793347140491343246389758472778252150", + "-24340646930015736611317054140325684688244556429619274796104420232188852118951262665153173730618778122989109439618594610", + "-20753416056567111230944755044099255424191149803890807170649916792018816327661929584304412214181904942572699295654247964" + ], + [ + "19307983631513131090380871977680322268291550314918461053905759132167741833551294078750846722999446756164530254631889674", + "19258519362501305324339832474729323059094307634149130294191744569986110569355684089884414691310284921360260637513299398", + "16838265232892544548953782365439465132031752718612506666121184705463213222726981911832134242916816755698871278506676306", + "-6812910485244889531542081320384805572187816701871968203607615971437681057044108691946772567694118772288054661910955208", + "-13574170268654526951691194476578402160782959192691328195158645598091717238284930554291340322177934626254133503422830302", + "-17648102900547028963745574042428887910573879474374276440086520048037731752166108796909886716839760675708762187342550882" + ], + [ + "-230416110897400741032431408049200160645754962304986435403813599292607339339134176210657120292225879703314614512498412", + "3127696348627746017975511126869144318747420157533376248998600252839890669028663089400053611216205731940894484422684496", + "7204415063899950346428280219946154086251433558063696684329409315596954317843705546599891934536447341936517392742405652", + "8459805607755065990735251458518839417499851696006054924069414245430409386267621828132010489841944423369583135083797740", + "6540933834277736411033429453194589769964741221039906726617314057396603026222744004190978644655206377225234293542804734", + "3382330027988786140064616968035536185088888289586215205902281075619268688985041303293755402382529423762572017031774550" + ] + ], + "b": [ + [ + "12149571538895417275290639259859624240648093717076280505700299742704776629086544784894795757147138450654933191546136841", + "12262377827452313862216740538681595410252435008303264726526249286225014990092772526244097241782545604107540986132024188", + "8606626376951036182450192455632087925370653621984333196817463179376759333873738533899015833620312207122451532411522204", + "-7340914721979484113725996905214965370961718184041249792808316276968031395467736628448663572026815009145442894277446138", + "-10427862156586488718386417073740435512833442864081290402887274102074615900155755006600880949189193946189414593739716002", + "-11984905541416882200854884921413614687325831316051705115503645671674740759659308360238887407218160377434592470512687554" + ], + [ + "10773143046195595143560769906277351789612795666190170009034429574998136210044932186299217004381437481845823098350165633", + "15912192881499645233455113879875023020292141864412373686671043472940973681203393641795848702336154837521887409659194225", + "19886706608155282375869222319945360642918977003577682696752928392335338524575639179492143405444132777499354260929853914", + "11993519627861039777734891694950599327067680429332178757683441500632744242743069451120946859887109809017929331608320200", + "5154025794128557909571342851687033281976920108241362714529562855805943249463319693761777855972442704307781966164157242", + "-2205536988325525848672805357667203205424534238578475370266614127525693669341030696930702737755560436604803698180005472" + ], + [ + "-16134398915967715536656209475843057623218108739162868557643864679035406268788349350534837175537878544527307392168418788", + "-8349919146291288365806107129260536682684868135105160307360143895767822232497742694325658548678481396757603117012861903", + "369112655124820431325510748089037287175718847331525635131434776857610419151735761700850042532440626224407339948602032", + "25165205870182309666351400723855440014263804177934531621950404051632925081682819712562598023317877428474251374226712243", + "25014956594784449087901357377071475376797224254387773611004577949335333525363343436072713580682204908835293001844016232", + "21685517009078976949450563522464042246272721269779995090752740455974655629776566779876722432100829891556733269738367734" + ], + [ + "-21844956800933628917801553783662357786838835524021826484989109174176900083939799682842329631312322515761815096515339959", + "-19932986598953440984787216169637463976933983603799011036988540929077853383573324811895925374232921589662741470594316272", + "-16361013417109314987692696329556451845135953042811373903615705323078644070309202077791723311729690999146236336388332566", + "11422367534811206706958820457037742879961525054038797564578104518900794804139285160623861005611546373763419702680491698", + "16894430529563544827186634061428843817349566714944451429053720989010165261014267620418238863280477999037045948270744113", + "20619524489615745405478221714478550526606055771968799078662481362741966581587322562835949908500671862027322087498650585" + ], + [ + "-10039425635931377593914574265783178111817034194921584311235047550123359780791907994257912040214339751655755977043829444", + "-12714107981480981895972341523016800847507422525448208103913153793998691462623153921489079802288155193590355439631346201", + "-14015230873095646010220983334738822254897328826941075139558382345413363902834818029348605123983497690289817801152932791", + "-3530031395786110287708436056074138797664178308486510720836950948553437611246282220660580104662729585818996983928930953", + "1542283267288556660119843291859311857661994780447527714965550792295058454406142629382223895349774333059369844063906615", + "6468149075131868217049968256370434836948687234225392269845712944407560904704826942230061961644176257266187151001393148" + ], + [ + "-2117661041474520728421892084710608079951721265029615656959660478818808686365480669624942101643554922325856256433370390", + "-4945130521377495297043236836676327261673167093773859054882312985473543644797297549631046874814937970984466702423042328", + "-7784821619525331620749169110122167856113530406900657985251112288854190876564634168690358034966118543178659621850929092", + "-6779274730166157378093377343807619134259061030633641290884442110558716725098342439891627782389777320357055756663110333", + "-4410507563787231193855639715879955793719299240275806300690739554684723796459987991005090232214564732431024100175316322", + "-1225805318566446664784446875365583695195951552808804051118829206915158134519053001610811311441118904583069561274195041" + ], + [ + "222017208399543822339555655755240527352414268254112217900808658210547548566418467549733309745161716557026968563827671", + "-1842152540639068577986698719538741624724625842638187030711546347045819453690621282240017475208366499731616868243365865", + "-3115357551389272924978373770702912857602925861090138811609441802591458961134639458904303878116098903049602853193197352", + "-4283881177071700088777279106648725602724084623039888291927877311528010495462550538738617158208120813958952663138733354", + "-3225306921707734871035765092785905367502726934145401011694379088986873509594214199231769588820449339354166202174717162", + "-1526401297304470816409068592425023231356965671387026597869963722696744372503213739015689831557541374067055659650828743" + ], + [ + "1090955687007572180260242722083746475387757707748062978985638547451352405988739520611210303478908917162385612920235807", + "577875797343552994129609246179442138647310257959856734140771443887533719077511780603055901880569314702385347457495325", + "-491212898343381219852922084729346541782864313294106203899672073764857212820239483570828836570214829492924253540585286", + "-2116911704589107226193993120869435000961702848979813837700605976491408259041987727887345207389052159020371621696417598", + "-1907897373654925602756063756712401745143598550923827600971010920296668313471934015537935800134499206114931798580189923", + "-1453842480622793872840391716889830747728718254754008178758256887055004421339695932459708975128357451559360538870169707" + ], + [ + "1327295352820185467354142730071675525091740435609826250465787740176570479397299096373534837864137451654881419318362107", + "694557740414178475211706893909550498259557269982009545964840202628121732084348764016057182487748249354996827865410315", + "-220369918933102458731514098942466590631169740519440220649091439852344958352642201211314568581487009644980022949321058", + "-1818946874024645239962609351105904813655191143933118218223037139615251890775772785353848609793192178777063749100309286", + "-1804644277678874756464930223916217249849456185322666944718612528082670638610175199678320448468034430962078350087084178", + "-1680435698552702363281919809130726835381317996153269017543165056827572987094162191368399847677296177524963644774018271" + ], + [ + "-84582965307812445834507777047338174332859174544446822382669907849979820394498550579680741150686208538654224698250414", + "-610041468151276390679629881160358026424166330822049768949488428117993303355871768908960189175625645636402119136321102", + "-883106117858388267498531954156841183300011034109371864331942327474154108459288691546955816123237433624212027573318091", + "-1100048455088945650478023035284116182221638281037122853410546730731463917120370840996718308731779947475530637215544130", + "-732973705493055311037307947585980183676534523590371885554459614249304885725650928966068107332406762544715130522499856", + "-346671992371750612819803609059426581680872453613193122931990636991023337370267258803211842794159821429176345166760893" + ], + [ + "-553737317942881382863282967716675008954611159439494079878932009365906813314563087328795918273447325107184676079855241", + "-356890092666324227880541510140586852945644852974648485722874463064679523411730092784876923348834552820910739603585982", + "-462335582797994096165364304476746692134736687632237538765898989768117787670121940183495239973170176300017896497767154", + "331441215281288210624191946501803547285710507956932830558944997535628623081612158794633974212016095168115541589492434", + "355060082957127467890412319428470744528590773909604936490675156240444853852397516327557361745802988913452720654887916", + "544774912390617136663335385167052698183340304803034098563983646687633870667247436620883957411742910544410282445894774" + ], + [ + "516071754822982068411384207667427363453599535474051659169533515410700808591998122052952142941271560935059799053784087", + "599127571550487453783097698446429789535674970933107125829575388216434479383575422522810839297848243362754789702255989", + "416455663036578409053006270876409405025796657710892183556521600413292454913876065092094989028612844249703008343142017", + "-184658408917739316866164015120876162032041906553589248865918281265418400018720277571945186582267000855213352036593808", + "-317784793599267479537065258457759729200869292323012537411229255270275689561763999641285635883346247558832142001094970", + "-136886981677825893873715385587431610338191285181295566335639719092982291671352129636973379215901785254100441658922503" + ], + [ + "241777313702868405689255456737153696208568030367200544111667755770606835469624305629137340360384376867492201937819415", + "-45649201018168515945262624249590280925018748685210524020668855402418822897021537826499366729235372051465310296601831", + "-432161725285071197644254450374658478212219408782532669198723505365985161889953970516008226557452246711448556200280866", + "-746199846292369009429925643691173726428865465081643080960811106043208547262913311162837470356416130721300228461035180", + "-545979206624095381447923825427142144571000710511356564961173009747873853793985365840072708923384674368789431007852188", + "-418571643043964170973970990024262560553952073317630922282558871226202667839028043419511729011784593217249033550335748" + ], + [ + "-896717740310125625524955552493423858625000664669358118924339947832622185628357223225301000538430778961690691212422872", + "-793147194518747667748404498878696276881562122079077947489296820474679008556875842874216396087127069983158147530776993", + "-800888362877160364607124626140195373748546605680336748181077665363709610316756346508690361788589104131948094129790737", + "291247744109895957223527265765701245431719177505610122969861331287690687322383021467690834653804404048730928280457244", + "503704618728979445382008097232243023307197681786989205492659360158620447144525699869244584798672537860601502457375965", + "619857924676713710639310223701421815456583631284977808115187964338290748736381262009904956458017144355602350415977793" + ], + [ + "-141513589212211630825444090266985628196558888677727230678828331528882378847717643110343631785580671185747317205382524", + "111484970593560112566761648690142149823852142950712204057991638179691759452000263292472567308509892256492938387271237", + "310080246580695952595530451915240022565015057074235833205660380175958941802452413802315061138281512725232298721478410", + "736189048261305602868188160329289321653095636716591051900142036857721620755406896752743404566826598850736746853358356", + "612704656178043819052585364572137556651711575151716557382316460665810986623681402115256713587068591003499982395760574", + "549657327146688207713060689748768772844960568674786843085121239915523747448569209334293699758567199912192590823695403" + ], + [ + "696382977759105546323984909764060323778233598046898054722770003753070829101396932348105387269394015222842530700792333", + "751854457517787995019445880272886138109002260478357773947560191091893287100396341051784095257904999270564644090549385", + "543010762999261624587907531376618860965323623428929926618523628840048329204272937539220203528476778462488149317944447", + "-289314254992374203973950034650307906650021807021459249542704454763353497251889088432419316830724803779466191237923863", + "-452551913723321385188012744770310504774769121558916930419444311014459118486312690807065657522061885819567176156921631", + "-589235875567080803357036242668720863649274751291388915501270650014454425416855479015860506956006714617744994803106637" + ], + [ + "12800895049855596724023967113844453369208609016943690855767422182922629963285232011703173349568104427961923028472134", + "-173760908257097000998639507048285795485967786529632013833255569602216148279370171633336311734233651774494138023482472", + "-400245281327775019246015567774786338125079642114649815796078295310941906546872530366660663029802630107584299596800314", + "-469989200430836999485291747695491078749991760889225273559411902523911632570423434896222804991219134631643507504655430", + "-363385213015429800612968302955254987220263401168883707034295225410922390345708000232832146925289243179179682974600263", + "-187907223777154785559145387113085343616049349421456400327904504201070482721391183516319744576807190209031778723987475" + ] + ] + } + ] +} diff --git a/research/composite-cyclic-bezout/CLAIM.md b/research/composite-cyclic-bezout/CLAIM.md new file mode 100644 index 0000000000..c49cd2e5ae --- /dev/null +++ b/research/composite-cyclic-bezout/CLAIM.md @@ -0,0 +1,71 @@ +# Sprint claim — independent verification + +- Assignment seed: **82**, generated with Python `secrets.randbelow(100)` + (operating-system randomness) on 2026-10-13 UTC. +- Track: independent verification or formalization (75–84). +- Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Selected frontier at base: #626/#622/#623 with #543, + κ = 51110230636731/31250000000000000. +- Started: 2026-10-13 03:04 UTC. Expected finish: 03:44 UTC. +- Object: the q-Pochhammer cyclic kernel of Ali Romman's #621, + restricted to the non-prime-power radices 6, 10, 12, 14, 15, 18. +- Method: exact cyclotomic polynomial Bezout certificates for the kernel + and its conjugate reciprocal, checked by a separate rational polynomial + implementation. Include mutations that break conjugation or an identity. +- Deliverable: a finite, source-pinned nonvanishing certificate or precise + obstruction, with one reproducible verification command. No new κ claim. + +## Candidate selection and overlap + +Three candidates were considered in this order: + +0. Independent R420 bit scalar-boundary verification. Existing #612 and + the retained independent bit engine already cover closely related checks. +1. Exact non-prime-power cyclic-kernel certificates beyond #621's theorem. + Selected by seed 82 modulo 3 = 1, subject to the overlap check below. +2. K492 cold-helper/owner interface verification. The selected replay already + includes independent owner/moment checking, and #633 audits factored ends. + +Read CONTRIBUTING.md, the selected result, current status, central PR ledger, +the selected K492 construction/review, and preserved negative-result index. +The #621 theorem explicitly claims no non-prime-power result. Its two engines +cover orders 3,4,5,7,8,9,11; they do not certify the composite orders here. +#628 supplies rounded prime-power inversion, including dense and stride checks; +this experiment does not duplicate or certify its rounded implementation. +The prime-subset and other preserved search exclusions concern different +network/side-circuit models, not these polynomial identities. + +All open PR metadata was inspected at claim time, including #628 and #634; +no non-prime-power cyclic Bezout contribution was identified. GitHub's +pinnedIssues query returned an empty list, so this claim is local per the +sprint instructions; no reservation issue was opened. + +Reserve the final quarter of the work window for verification and handoff. +Prepared for Jason Willems (@at1as) with substantial OpenAI Codex assistance. + +## Result — 2026-10-13 03:22 UTC + +Completed: six exact Bézout identities establish unit-circle nonvanishing +for radices 6, 10, 12, 14, 15, 18, symbolically covering all 30 primitive +embeddings. The inherited Fourier argument gives explicit all-length +inverse bounds for these fixed radices. No new κ or general-composite +claim. All six nominated radices completed; no search was left pending. +The independent checker rejects 39 mathematical/coverage controls; eight +focused tests pass. Three Python versions give identical receipts, and +fresh SymPy regeneration reproduces the certificate bytes. See +[VALIDATION.md](VALIDATION.md) for the exact scope of execution. + +Submitted one focused contribution: +[PR #666](https://github.com/CrocSwap/integer-mult-bounds/pull/666), +initial implementation commit `237d7fda614174e0784cbb2a8c22dfe4015efc94`. +The PR's base matches the recorded base exactly. GitHub reported no check +results at this handoff; local verification and remote CI remain distinct. +No pinned coordination issue existed, so this is the single local claim +result update. No other PR was opened or modified, and nothing was merged. + +## Authorized continuation + +The same PR now includes the specified infinite composite families proved +in [LIFTING.md](LIFTING.md), with the original six certificates unchanged. +See [CONTINUATION.md](CONTINUATION.md) for the extended claim, completed +result and final verification handoff. No new κ or all-composite theorem. diff --git a/research/composite-cyclic-bezout/CONTINUATION.md b/research/composite-cyclic-bezout/CONTINUATION.md new file mode 100644 index 0000000000..441e607cb8 --- /dev/null +++ b/research/composite-cyclic-bezout/CONTINUATION.md @@ -0,0 +1,71 @@ +# Continued sprint: modular lifting of the same cyclic kernels + +Authorized continuation on 2026-10-12 America/Los_Angeles, +starting 2026-10-13 03:24 UTC. Branch head at start: +`5020edec5c293cc0c733ff83a742952d1e52ba3b`; upstream remains +`66849e1475c930fd7732b1a0067ffee7e1e95f60`. Retain assignment seed **82** +and its independent-verification track; extend the same PR #666. + +## Narrow claim + +Test the following mechanism: for r=s*p^a, p prime, p not dividing s, +reducing a primitive r-th root modulo p collapses the integral kernel to +`z^(r-s) f_s(z)` and its conjugate reciprocal to `f_s*(z)`. If the two +base polynomials are coprime modulo p, the larger resultant is nonzero +in characteristic zero. A small exact base certificate could consequently +establish a uniform circle bound for infinitely many composite radices. + +Deliverable: a precise written lifting argument or counterexample, a +standard-library modular identity checker with meaningful excluded-prime +controls, exact small-base certificates, and a revision of the existing +PR only if verified. Do not extrapolate from finite checks to all exponents. +Target initial bases s=2,3,4, using their independently checked denominators +3,43,37 respectively; no new multiplication kappa claim. + +Three continuation candidates were considered: additional finite radices +(rejected as more computation without a new mechanism), rounded inversion +(already actively developed in #628 and audited in #663), and modular +lifting (selected as a structural use for the existing certificate method). +The new #668 uses split-prime CRT for prime-power resultants through 27; +its method and domain are distinct and retain credit as concurrent work. +All 488 open PR bodies through #668 were checked for overlap. No pinned +coordination issue exists, so the claim remains local. + +Bound the experiment to roughly one hour, reserving its final quarter for +verification and handoff. Independently, attempt the omitted root +`make verify` with isolated dependencies and installed Boost headers. +Record actual completion or failures without relabelling unrelated failures +as passes. No intermediate speculative revision will be pushed. + +## Completed mathematical result + +Three integral seed identities with d=3,43,37 give the admitted families +r=2*p^a, 3*p^a and 4*p^a for all a>=1 and p not dividing the respective +s*d. LIFTING.md supplies the all-exponent proof, including the reciprocal +degree drop and characteristic-zero reduction. The original six tighter +fixed-radix certificates remain byte-identical. The quantitative bound and +Fourier transfer retain #621's attribution; there is still no new κ. + +The standard-library check passes 54 finite diagnostics, three genuine +excluded-prime modular witnesses, and 173 rejection controls. Both public +receipts and all 16 focused tests pass on Python 3.9.6, 3.11.13 and 3.13.4. +Both optional generator modes reproduce their certificates byte for byte. +Separate Codex agents reviewed the mathematics and checker; this does not +constitute independent human review. Final overlap refresh covered 533 open +PRs through #714, with no duplicate lifting mechanism identified and no +pinned coordination issue. Broader repository execution is recorded in +VALIDATION.md separately from these completed package checks. + +## Handoff — 2026-10-13 04:42 UTC + +The completed proof and checks were pushed to the existing +[PR #666](https://github.com/CrocSwap/integer-mult-bounds/pull/666) in +`8df1b593cb640380a194ac8d599f2ab1cba158a3`; no second PR was opened. +Broader verification continued after that checkpoint. The selected cold +replay passed exactly. The root run stopped on Apple clang's unsupported +OpenMP flag; with the installed libomp and a temporary compiler adapter, +the failed stage and all remaining targets passed, including 84 isolated +test modules and every patch-application check. VALIDATION.md records both +runs without claiming an uninterrupted root invocation. Only this package +and its scoped workflow changed. GitHub has no reported +remote checks or reviews at handoff; the contribution remains open. diff --git a/research/composite-cyclic-bezout/EXPECTED.json b/research/composite-cyclic-bezout/EXPECTED.json new file mode 100644 index 0000000000..9e7b307e65 --- /dev/null +++ b/research/composite-cyclic-bezout/EXPECTED.json @@ -0,0 +1,122 @@ +{ + "status": "PASS", + "scope": "six exact composite-radix Bezout identities; no new kappa", + "cases": [ + { + "order": 6, + "primitive_embeddings_covered": 2, + "bezout_denominator": "4603371", + "bezout_coefficient_l1": "18399030", + "circle_lower_bound": "1534457/36798060", + "circle_lower_bound_dyadic_exponent": -5, + "inverse_infinity_upper_bound": "142236673115931420/2354558284849", + "inverse_infinity_upper_bound_dyadic_exponent": 16, + "negative_controls_rejected": [ + "changed_bezout_coefficient", + "changed_denominator", + "missing_conjugation", + "missing_reversal", + "changed_kernel_constant", + "omitted_second_bezout_term" + ] + }, + { + "order": 10, + "primitive_embeddings_covered": 4, + "bezout_denominator": "36514130673104413304485467185561", + "bezout_coefficient_l1": "925863787894205297762243751731763", + "circle_lower_bound": "36514130673104413304485467185561/9258637878942052977622437517317630", + "circle_lower_bound_dyadic_exponent": -8, + "inverse_infinity_upper_bound": "157849520083656399153950779315892291180312884391408348644127212842180090/1333281738812544555016975073824209360506997688595344518406884721", + "inverse_infinity_upper_bound_dyadic_exponent": 27, + "negative_controls_rejected": [ + "changed_bezout_coefficient", + "changed_denominator", + "missing_conjugation", + "missing_reversal", + "changed_kernel_constant", + "omitted_second_bezout_term" + ] + }, + { + "order": 12, + "primitive_embeddings_covered": 4, + "bezout_denominator": "2654047882196193704215495532468166540243913", + "bezout_coefficient_l1": "61648115702987527570293946750341576440393870", + "circle_lower_bound": "2654047882196193704215495532468166540243913/739777388435850330843527361004098917284726440", + "circle_lower_bound_dyadic_exponent": -9, + "inverse_infinity_upper_bound": "4108635876095170698250758674482478430977844302008685976928931839112283783901219266042395211720/7043970160990100894308232748628996626582452157836907329375606792797387410601533551569", + "inverse_infinity_upper_bound_dyadic_exponent": 30, + "negative_controls_rejected": [ + "changed_bezout_coefficient", + "changed_denominator", + "missing_conjugation", + "missing_reversal", + "changed_kernel_constant", + "omitted_second_bezout_term" + ] + }, + { + "order": 14, + "primitive_embeddings_covered": 6, + "bezout_denominator": "1075114750327793955376458246593336860216422328566904681431159073390431112513560167", + "bezout_coefficient_l1": "39964281454675046295047210316894800109829801405945323783842090603216763185928926807", + "circle_lower_bound": "1075114750327793955376458246593336860216422328566904681431159073390431112513560167/559499940365450648130660944436527201537617219683234532973789268445034684603004975298", + "circle_lower_bound_dyadic_exponent": -10, + "inverse_infinity_upper_bound": "56357556553780766000832113986446975373903712588165603237087132689503659777766338598330703144995183947132896578182423543740679402045882959655569223493531318588287472462866/6839477670842572383902917186536159292916206028914954174463801681491046931751248927176389963410440524794692434985529638883210553436275211156607458137132858751881", + "inverse_infinity_upper_bound_dyadic_exponent": 33, + "negative_controls_rejected": [ + "changed_bezout_coefficient", + "changed_denominator", + "missing_conjugation", + "missing_reversal", + "changed_kernel_constant", + "omitted_second_bezout_term" + ] + }, + { + "order": 15, + "primitive_embeddings_covered": 8, + "bezout_denominator": "21303110977467217422179365304980853459710951108484250839666947703943501024265451274389430764941852454816792740037581", + "bezout_coefficient_l1": "6795212397947091325601266148326804868849519706331401747887899899614599374284366585327847680997819333388437858068108673", + "circle_lower_bound": "21303110977467217422179365304980853459710951108484250839666947703943501024265451274389430764941852454816792740037581/101928185969206369884018992224902073032742795594971026218318498494218990614265498779917715214967290000826567871021630095", + "circle_lower_bound_dyadic_exponent": -13, + "inverse_infinity_upper_bound": "635465599179091235531256590420039632643032326933204997612616294561776659818124833850146862306455263590620069973361200319521545472112703631906312384167289944254939717485147334192882522147513382495000237721946084590641915143633446841773100428255/453822537318284263719368052702449075499604547750765061247332035826580310656887769887248371432112598973340505353641565671587479792502387515858054200474522327168508433833189789280819421835985568865783724978477814325647375925292331561", + "inverse_infinity_upper_bound_dyadic_exponent": 41, + "negative_controls_rejected": [ + "changed_bezout_coefficient", + "changed_denominator", + "missing_conjugation", + "missing_reversal", + "changed_kernel_constant", + "omitted_second_bezout_term" + ] + }, + { + "order": 18, + "primitive_embeddings_covered": 6, + "bezout_denominator": "11186692986735857979845337120253796974449822403416886376595609636244310920090200621768120321671202650050564058189395533", + "bezout_coefficient_l1": "939142197116962788692869277864880762948136872384697322192375915390676607882727849629786550527657260620195441797315203778", + "circle_lower_bound": "3728897662245285993281779040084598991483274134472295458865203212081436973363400207256040107223734216683521352729798511/5634853182701776732157215667189284577688821234308183933154255492344059647296367097778719303165943563721172650783891222668", + "circle_lower_bound_dyadic_exponent": -11, + "inverse_infinity_upper_bound": "15722075864053046650932809134151399835871067852110803178376158435533205168017533782972487727056196410522173689282073456912283604718528943181084638911287445021945732898124730777660496182441156356736439078780915931089592988868647148848296140165804964/13904677775498358977799712358044359875485952426974177203819259219301860744724504164779589253623307398093702113143420923693619460759707351974184936834105830525927349428574467373085160021828978225817144101484653030678386385219610657817121", + "inverse_infinity_upper_bound_dyadic_exponent": 41, + "negative_controls_rejected": [ + "changed_bezout_coefficient", + "changed_denominator", + "missing_conjugation", + "missing_reversal", + "changed_kernel_constant", + "omitted_second_bezout_term" + ] + } + ], + "additional_negative_controls_rejected": [ + "missing_radix", + "duplicate_radix", + "false_unit_root_witness" + ], + "identities": 6, + "primitive_embeddings_covered": 30, + "negative_controls_rejected": 39 +} diff --git a/research/composite-cyclic-bezout/LIFTING-EXPECTED.json b/research/composite-cyclic-bezout/LIFTING-EXPECTED.json new file mode 100644 index 0000000000..da9e707d00 --- /dev/null +++ b/research/composite-cyclic-bezout/LIFTING-EXPECTED.json @@ -0,0 +1,531 @@ +{ + "status": "PASS", + "scope": "exact seed identities and finite checks of a separately proved all-exponent lifting lemma", + "seeds": [ + { + "seed": 2, + "denominator": "3", + "excluded_prime_divisors": [ + 2, + 3 + ] + }, + { + "seed": 3, + "denominator": "43", + "excluded_prime_divisors": [ + 3, + 43 + ] + }, + { + "seed": 4, + "denominator": "37", + "excluded_prime_divisors": [ + 2, + 37 + ] + } + ], + "domain": { + "primes": [ + 2, + 3, + 5, + 7, + 11, + 13, + 17, + 19, + 23, + 29, + 31, + 37, + 43 + ], + "max_exponent": 5, + "max_radix": 512 + }, + "finite_instances": [ + { + "seed": 2, + "prime": 5, + "exponent": 1, + "radix": 10, + "modular_identity_sha256": "e9db250bc070a0cf802c485798234f079dbc1f55cc7d908500c22212e34cc209", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 5, + "exponent": 2, + "radix": 50, + "modular_identity_sha256": "d7a52b0c3b917970585222faa80f9208e9f273ec7bc7fc3e4a1c9ecf4bbe5761", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 5, + "exponent": 3, + "radix": 250, + "modular_identity_sha256": "561f8adaadf8b8cbc07eb502f4a243bfef7fb134de5158f087d8584fff6c4f00", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 7, + "exponent": 1, + "radix": 14, + "modular_identity_sha256": "d11f97465e59fc35159c55d6aa62115c381d6b08273f7a4f596adfcd2e3837b7", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 7, + "exponent": 2, + "radix": 98, + "modular_identity_sha256": "ef399e0b0c35dbaf0330e9c7a7d248285c608f30e44e1524d1b106c294b8c6ec", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 11, + "exponent": 1, + "radix": 22, + "modular_identity_sha256": "2baae05e7d982b119a1de9a63505fced3d8312e73018a0f6fb09508d07395fe6", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 11, + "exponent": 2, + "radix": 242, + "modular_identity_sha256": "cc7deddba3046578cca48d226d7f2fa2406962bff2fff9daac12affea3c24f98", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 13, + "exponent": 1, + "radix": 26, + "modular_identity_sha256": "195723c1250cb27f05cf950784e1193089bbc0432cf28cd5835f900e2fdb8b28", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 13, + "exponent": 2, + "radix": 338, + "modular_identity_sha256": "dcc2a14c4f352b1b9133597ffe82cc7f8c4d2a86cae002dc50084732839ff828", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 17, + "exponent": 1, + "radix": 34, + "modular_identity_sha256": "160fb2bdb0287e8d89b8c0ed6aa413997bccb7d4d9905ed6b5b8ebab9da17e73", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 19, + "exponent": 1, + "radix": 38, + "modular_identity_sha256": "f33bf23a22711731c6e9b1eeb85a721e05a75bf3e077d149f32d79c3438d9d08", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 23, + "exponent": 1, + "radix": 46, + "modular_identity_sha256": "76e10776589bd3c8e1b7ddf8c76b8730ce8008beadfcb5cf47ea1e46565d7f6b", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 29, + "exponent": 1, + "radix": 58, + "modular_identity_sha256": "08b5cb3b42c3e155414cb9bc37f2b43b14fc0b149084265506eb840f27771499", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 31, + "exponent": 1, + "radix": 62, + "modular_identity_sha256": "e882bab83f0ce486e8777341f63c2fa726725fb4f6fa5bb22e9e1ae6a6153645", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 37, + "exponent": 1, + "radix": 74, + "modular_identity_sha256": "e2264ff8a6f1670c27f340d6c3998bb593167de9c080cbf87e5051233b4215ce", + "mutation_controls": 3 + }, + { + "seed": 2, + "prime": 43, + "exponent": 1, + "radix": 86, + "modular_identity_sha256": "2cd8066d73275e45773a75470740c8f3183033457fb950c3fd1dc2ab7f9cd08d", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 2, + "exponent": 1, + "radix": 6, + "modular_identity_sha256": "438a262ab6a80302efa5280f1109e3536fa488176537761e128c7c93e0c2eed2", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 2, + "exponent": 2, + "radix": 12, + "modular_identity_sha256": "3c30c1fb5c49c346d079166bec1234be810a8b406311494d3051fb98f4a0dac5", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 2, + "exponent": 3, + "radix": 24, + "modular_identity_sha256": "455c418c9ef4406f3d9e152aff2137ba57621ac4c3a254032b03ce9613e7ecb7", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 2, + "exponent": 4, + "radix": 48, + "modular_identity_sha256": "854cfdaf8333ed690cd50f843b865e99ef1312d72c8f142b585e535037f2ef35", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 2, + "exponent": 5, + "radix": 96, + "modular_identity_sha256": "8acba0f6dd06a3647f1247b513ec52fa627a8693dbcfd21a06a2b9ba285c38bf", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 5, + "exponent": 1, + "radix": 15, + "modular_identity_sha256": "8775054df6f87eb1a25b978189ec2a43ac8a9519fc62eb776c5a951192f57579", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 5, + "exponent": 2, + "radix": 75, + "modular_identity_sha256": "0f9a86ea241f6cb2c18f8d3c86bc66911468b782cf83fb213e284e07e9f8a9e9", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 5, + "exponent": 3, + "radix": 375, + "modular_identity_sha256": "66f669b1e7941144891d0f50efc0328740728851a7cb2370796c74ee929056e3", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 7, + "exponent": 1, + "radix": 21, + "modular_identity_sha256": "1cf8ecc2bfb7708d4f6822ab7f45f17706aae4a3efec4d9026dc7e5bcf887526", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 7, + "exponent": 2, + "radix": 147, + "modular_identity_sha256": "ff5ab8e7b350b5d18d44b4957b903168a725843fb7f802c5997d8a3fbe4b134e", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 11, + "exponent": 1, + "radix": 33, + "modular_identity_sha256": "b0225f39c0ddb830afd021b8594b075e509cf11601d94401008408c347baa370", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 11, + "exponent": 2, + "radix": 363, + "modular_identity_sha256": "a9c3343fe08caa7143ae149a4cd4b24accf73937b05b1429badfb4df8db6fea1", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 13, + "exponent": 1, + "radix": 39, + "modular_identity_sha256": "2ac61458843d09280202c53060cd394841ce72b7c2f7175506741c690fff9240", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 13, + "exponent": 2, + "radix": 507, + "modular_identity_sha256": "9a4e3d3d726236864e73341435b61d72d95ae9b3de1e7a09518b2f4e86f3fca8", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 17, + "exponent": 1, + "radix": 51, + "modular_identity_sha256": "5f6e53a869052d4ce2ccb8d029ed6cbfc1e44538f9e7aa85000d0325795ff8c4", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 19, + "exponent": 1, + "radix": 57, + "modular_identity_sha256": "2dd5085ca3ba5a3a6bda9d046c4a2a844c85410a762ccb2940737bb6c76dc047", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 23, + "exponent": 1, + "radix": 69, + "modular_identity_sha256": "47e43e27d3a8d520438e59b1a02b76b193f563a6a569396fcc0cdd8cf2f4852b", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 29, + "exponent": 1, + "radix": 87, + "modular_identity_sha256": "e2d6322bb5d217893a620afb76b1bcf93171cb843f5acf0b9f17afca21c3fcf8", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 31, + "exponent": 1, + "radix": 93, + "modular_identity_sha256": "24e6667bcac4eb9168353a330407e0daa68d723f3326381c339729e9bb9e727b", + "mutation_controls": 3 + }, + { + "seed": 3, + "prime": 37, + "exponent": 1, + "radix": 111, + "modular_identity_sha256": "b47d2d028d934ca83326a21fc6a7c905c9c44839cb88b1d656b04a372952ac30", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 3, + "exponent": 1, + "radix": 12, + "modular_identity_sha256": "2db51ebde9e283c553c53300a2252fa68c615ce4aff3e17dff6b984da4cccf6c", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 3, + "exponent": 2, + "radix": 36, + "modular_identity_sha256": "ac64db027ea18d746a80f4b2c1149e9a6ed85a2a8f343e9c555e0842bc9e9d62", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 3, + "exponent": 3, + "radix": 108, + "modular_identity_sha256": "bdb22962544a3b7b9cde4a1d3f03ca37fbd514c5dc250921e3b3719c6345b937", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 3, + "exponent": 4, + "radix": 324, + "modular_identity_sha256": "1cb9ad48362e5081ad53476f7008fd0e20995151b82f3e515b729db48e419602", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 5, + "exponent": 1, + "radix": 20, + "modular_identity_sha256": "2ac21da417e27245a2a643cfff8a2eb7cbd14607fcabacee5f856d74dd261820", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 5, + "exponent": 2, + "radix": 100, + "modular_identity_sha256": "2354c46a5509762f431ba142a5960451e97d53602f6b22b13c35f640f098e146", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 5, + "exponent": 3, + "radix": 500, + "modular_identity_sha256": "7fa53da53eddda29178be7f2440d53bf24d2c70c20c5190855d2de318fb0a1e2", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 7, + "exponent": 1, + "radix": 28, + "modular_identity_sha256": "59b7cf59a5c89bd8920002f7cfbb0b2f638aae7698d87730bab46aa77c958cdb", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 7, + "exponent": 2, + "radix": 196, + "modular_identity_sha256": "3a3003bd70a5322415fad9293bc8f23a336098ba3dc36dabf71c466f3e6d2abc", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 11, + "exponent": 1, + "radix": 44, + "modular_identity_sha256": "9f260aab1a6387d0d590ce7192e44f747e568fe64f48278520fca8e019ae9c39", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 11, + "exponent": 2, + "radix": 484, + "modular_identity_sha256": "5a4916b869f8b8f99845f3a55d0a1e6d75d353836c7794240e94585bf371e14e", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 13, + "exponent": 1, + "radix": 52, + "modular_identity_sha256": "6c528ea70182f92707208496fb0cfeec993e6f600b065b026c110ebcaa2c8176", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 17, + "exponent": 1, + "radix": 68, + "modular_identity_sha256": "116a52ceeacb61b5a868d7ef33f17038ee4ad825c0e9f57b53aade564719da01", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 19, + "exponent": 1, + "radix": 76, + "modular_identity_sha256": "ed6baba7c2347199faf05788f2710b64e4d37b50b60779cce58459c18595ccb1", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 23, + "exponent": 1, + "radix": 92, + "modular_identity_sha256": "5165efca1c9473cb25bb92728edbab2248287fde38e7ba5a6c03c2fc65a1be4c", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 29, + "exponent": 1, + "radix": 116, + "modular_identity_sha256": "a6398554071555e27caa009bc7612ac28e775ea7c28c8516ca4b2fca9df7b567", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 31, + "exponent": 1, + "radix": 124, + "modular_identity_sha256": "87d0c563cce33f0588202cacf9c7b60c9655bb2b59160f1e85138641b091dcf6", + "mutation_controls": 3 + }, + { + "seed": 4, + "prime": 43, + "exponent": 1, + "radix": 172, + "modular_identity_sha256": "309fd264fef64760718e74777528a59af43ac73dee1d7ca95b44391e0515e354", + "mutation_controls": 3 + } + ], + "instances_checked": 54, + "bad_prime_witnesses": [ + { + "seed": 2, + "prime": 3, + "primitive_root": 2, + "common_factor": [ + 2, + 1 + ], + "scope": "common factor after reduction only; no complex-unit-circle counterexample" + }, + { + "seed": 3, + "prime": 43, + "primitive_root": 6, + "common_factor": [ + 24, + 1 + ], + "scope": "common factor after reduction only; no complex-unit-circle counterexample" + }, + { + "seed": 4, + "prime": 37, + "primitive_root": 6, + "common_factor": [ + 15, + 24, + 1 + ], + "scope": "common factor after reduction only; no complex-unit-circle counterexample" + } + ], + "rejected_admission_and_seed_controls": [ + "excluded_prime_s2", + "noncoprime_seed_s2", + "changed_seed_coefficient_s2", + "excluded_prime_s3", + "noncoprime_seed_s3", + "changed_seed_coefficient_s3", + "excluded_prime_s4", + "noncoprime_seed_s4", + "changed_seed_coefficient_s4", + "composite_modulus", + "zero_exponent" + ], + "mutation_controls_checked": 173 +} diff --git a/research/composite-cyclic-bezout/LIFTING-SEEDS.json b/research/composite-cyclic-bezout/LIFTING-SEEDS.json new file mode 100644 index 0000000000..43f1af6fc0 --- /dev/null +++ b/research/composite-cyclic-bezout/LIFTING-SEEDS.json @@ -0,0 +1,74 @@ +{ + "format": "cyclic-lifting-seeds-v1", + "coefficient_order": "ascending z, ascending u", + "cases": [ + { + "order": 2, + "denominator": "3", + "a": [ + [ + "2" + ] + ], + "b": [ + [ + "-1" + ] + ] + }, + { + "order": 3, + "denominator": "43", + "a": [ + [ + "15", + "-3" + ], + [ + "-15", + "-12" + ] + ], + "b": [ + [ + "-2", + "9" + ], + [ + "5", + "4" + ] + ] + }, + { + "order": 4, + "denominator": "37", + "a": [ + [ + "10", + "-2" + ], + [ + "-8", + "-8" + ], + [ + "-8" + ] + ], + "b": [ + [ + "-3", + "8" + ], + [ + "3", + "5" + ], + [ + "2" + ] + ] + } + ] +} diff --git a/research/composite-cyclic-bezout/LIFTING.md b/research/composite-cyclic-bezout/LIFTING.md new file mode 100644 index 0000000000..937e5f46f7 --- /dev/null +++ b/research/composite-cyclic-bezout/LIFTING.md @@ -0,0 +1,162 @@ +# Modular lifting from an integral seed certificate + +## Statement + +Use the kernel f_r=r P_r and its conjugate reciprocal f_r* defined in +[PROOF.md](PROOF.md). Let s>=2. Suppose that, in Z[v,z]/(Phi_s(v)), + + A(v,z) f_s(v,z) + B(v,z) f_s*(v,z) = d, (1) + +where A,B have **integral** coefficients and d is a nonzero integer. +For every prime p not dividing s*d and every integer a>=1, set r=s*p^a. +Then f_r and f_r* have no common root, for every primitive complex r-th +root u. In particular P_r has no unit-circle zero. + +The three independently checked seeds in LIFTING-SEEDS.json give: + +| Seed s | d | Admitted family, a>=1 | Excluded primes in this argument | +|---:|---:|---|---| +| 2 | 3 | r=2*p^a | 2, 3 | +| 3 | 43 | r=3*p^a | 3, 43 | +| 4 | 37 | r=4*p^a | 2, 37 | + +These are sufficient conditions. An excluded prime is **not** a +characteristic-zero counterexample. In particular the separate finite +certificates still cover r=6 and r=18 even though the seed-2 route excludes +p=3; the seed-3 route also covers r=6. No theorem for all composite radices +is claimed. Rational seed coefficients would require clearing and excluding +their denominators as well; (1) has already done so. + +## Cyclotomic reduction + +Since p does not divide s, the cyclotomic factorization gives + + Phi_(s*p^a)(x) = Phi_s(x^(p^a)) / Phi_s(x^(p^(a-1))). + +For example this follows by classifying the orders of roots of the two +polynomials; the numerator has the denominator's roots plus exactly the +primitive s*p^a-th roots. Reducing the polynomial identity modulo p and +using the Frobenius identity yields, after cancellation in F_p[x], + + Phi_r(x) = Phi_s(x)^(p^(a-1)*(p-1)) (mod p). (2) + +The polynomial x^s-1 is separable modulo p. Its cyclotomic factors are +therefore pairwise coprime, so every root of Phi_s modulo p has exact +multiplicative order s. + +Choose a prime ideal over p in a number field containing a primitive +r-th root u. Its residue v is a root of Phi_r, hence by (2) a primitive +s-th root in the residue field. This permits reduction of all integral +coefficients and of (1). + +## Tail products and the reciprocal + +The coefficient of z^j in f_r is + + product_(k=j+1)^(r-1) (1-u^k). + +If j u^-1 to every coefficient, +then reverse the full r coefficients. The same tail-product calculation +with v^-1 gives + + f_r*(v,z) = f_s*(v,z) (mod p), (4) + +with **no shift** on the right. Its constant term is 1. This substitution +is defined before reduction; it does not assert that v -> v^-1 is an +automorphism of an individual residue field or cyclotomic factor. + +Equation (1) reduces to a nonzero scalar d modulo p. Therefore f_s and +f_s* are coprime over the residue field. Since f_s*(0)=1, it is also +coprime to z. Equations (3) and (4) consequently have no common zero. + +## Lift back to characteristic zero + +If f_r and f_r* had a common root alpha, choose a number field containing +u and alpha. The polynomial f_r is monic with algebraic-integer +coefficients, so alpha is an algebraic integer. Reduce the ring of integers +at a prime ideal over p. The image of alpha would be a common zero of +(3) and (4), contradicting their coprimality. This proves the statement +for any primitive complex choice of u. A unit-circle root of f_r would +also be a root of its actual conjugate reciprocal, so none exists. + +For the quantitative argument below, the original 2(r-1) square Sylvester +matrix also remains nonsingular after reduction. Its first polynomial +stays monic of degree n=r-1, even though its second polynomial drops to +degree s-1. If A_0 f_r+B_0 f_r*=0 with both multiplier degrees below n, +coprimality implies f_r divides B_0, forcing B_0=0 and then A_0=0. +Thus the coefficient map is injective between equal finite dimensions. +Degree loss in the reciprocal does not invalidate this determinant claim. + +## Uniform quantitative consequence inherited from #621 + +Put n=r-1, D=phi(r), and H=2^r-1. The preceding argument supplies the +nonzero resultant needed by Ali Romman's [#621](https://github.com/CrocSwap/integer-mult-bounds/pull/621). +The rest of its norm/cofactor proof does not require r to be a prime power. +For clarity, the estimates are repeated here. + +At every embedding, the sum of absolute coefficients of either polynomial +is at most H, so the Sylvester determinant R satisfies |sigma(R)|<=H^(2n). +Its nonzero integral norm has absolute value at least 1. Since r>=3, +the chosen embedding and its distinct complex conjugate have equal +modulus, giving + + |R| >= H^(-n*(D-2)). + +The adjugate matrix gives A_0 f_r+B_0 f_r*=R, where the 2n coefficients +are cofactors of absolute value at most H^(2n-1). On the unit circle this +implies + + |P_r(z)| >= delta_r := 1 / (2*r*n*H^(n*D-1)). (5) + +The Fourier/Parseval argument in PROOF.md then gives, for every L>=1, +integer w and |tau|=1, + + ||P_r(tau Z_L^w)^-1||_infinity + <= delta_r^-1 + 2*n*H/(r*delta_r^2). (6) + +The logarithm of this upper bound is O(r^2 phi(r)), hence O(r^3), along +each admitted family. This dependence is very loose. It is not an +O(p polylog p) precision guard or a paid implementation. At the six +certified fixed radices, the direct rational bounds in EXPECTED.json +are substantially sharper and remain unchanged. + +## What the executable checks establish + +verify_lifting.py verifies (1) for s=2,3,4 with the separate integer +arithmetic engine in verify.py. It then checks 54 admitted instances with +r<=512 over the stated prime/exponent grid, including (2), literal tail +products (3)-(4), and an explicit modular Bezout identity for the lifted +pair. It computes in (F_p[v]/Phi_s(v))[z], without assuming this coefficient +ring is a field. Polynomial division uses only an invertible scalar +leading coefficient. For the lifted identity it uses z*U=1-f_s* and +U^(r-s) modulo f_s* to absorb the shift. + +The finite checks test the implementation; they do not prove all exponents. +The symbolic argument above supplies that conclusion. Neither checker is +a proof assistant or a formal verification of the full multiplication +construction. + +The excluded-prime diagnostics find actual common factors after reduction: + +| s | p | Primitive residue v | Common factor of f_s and f_s* modulo p | +|---:|---:|---:|---| +| 2 | 3 | 2 | z+2 | +| 3 | 43 | 6 | z+24 | +| 4 | 37 | 6 | z^2+24*z+15 | + +The last factor need not have a root in F_37; a nonconstant factor suffices +over its algebraic closure. These witnesses demonstrate the limitation of +this modular route only. See LIFTING-EXPECTED.json for the deterministic +receipt, including rejected corruptions and admission controls. + +Prepared with substantial OpenAI Codex assistance, including a separate +agent review of the written reasoning. No independent human review or +literature-priority claim. Apache-2.0. The kernel, reciprocal method, +norm/cofactor estimate and Fourier transfer retain #621's attribution; +this contribution adds the seed-certificate lifting mechanism and checks. diff --git a/research/composite-cyclic-bezout/NOTICE.md b/research/composite-cyclic-bezout/NOTICE.md new file mode 100644 index 0000000000..af21a50f7d --- /dev/null +++ b/research/composite-cyclic-bezout/NOTICE.md @@ -0,0 +1,38 @@ +# Attribution and assistance + +Prepared for Jason Willems (@at1as) with substantial OpenAI Codex assistance +in selecting the scope, deriving the fixed-radix bounds and modular lifting argument, writing the +programs and documentation, and executing verification. A separate Codex +agent reviewed the lifting proof, and another reviewed its checker. No independent +human mathematical review is claimed. “Independent verifier” refers to +its separate arithmetic implementation, not independent human authorship. + +Ali Romman (@aliromman), PR #621 at +`520774462b19b29af41554b74def31f9d01e997e`, supplied the prime-power cyclic +conditioning theorem, the conjugate-reciprocal strategy and the all-length +Fourier inverse bound. His original package's attribution and AI disclosure +remain in research/prime-power-cyclic-inverse/NOTICE.md. This contribution +adds literal composite-radix certificates, a seed-certificate modular lifting +argument, an integer-only checker and finite modular diagnostics; +it neither replaces that uniform theorem nor claims its methodology as new. + +The kernel definition comes from the OpenAI exact-DFT preprint at +`adc7f1241b42e322a6451854ab7e4b4c146bf78a`, section local.tex, +anchors loc:newton and loc:fourier-factorization. Classical q-Pochhammer +and Newton Fourier factorization is credited there and to Alexey Kuznetsov, +“Using q-calculus to study LDLT factorization of a certain Vandermonde +matrix,” https://arxiv.org/abs/1507.02959v2. No external source code is copied +or executed. The predecessor's SOURCE.json retains the detailed source pins. + +Chafik Boukhalfa's concurrent PR #628 concerns rounded prime-power inversion, +restoration and stride routing. It was inspected for overlap but is neither +a dependency nor a rounded-program claim of this package. + +Scott Woolsey Biggart (@swbiggart), concurrent PR #668 at +`b861542035d612ff844d0a9d1deaa0713329811a`, supplies a split-prime CRT audit +of prime-power resultants through radix 27. Its scope was checked for overlap; +no code or result from that audit is used here. + +SymPy 1.14.0 supplies the optional nomination engine. Verification requires +only Python's standard library. All new files use the repository's +Apache-2.0 license. No all-composite-radix or literature-priority claim. diff --git a/research/composite-cyclic-bezout/PROOF.md b/research/composite-cyclic-bezout/PROOF.md new file mode 100644 index 0000000000..6f5c4a5232 --- /dev/null +++ b/research/composite-cyclic-bezout/PROOF.md @@ -0,0 +1,127 @@ +# Certificate-assisted nonvanishing at radices 6, 10, 12, 14, 15, 18 + +Let r belong to S = {6, 10, 12, 14, 15, 18}. Let u be any primitive +r-th root of unity, n = r−1, and + + h_j = 1 / product_(s=1)^j (1−u^s), + P(z) = sum_(j=0)^n h_j z^j, + f(z) = r P(z). + +Every denominator is nonzero. Evaluating +`(x^r−1)/(x−1) = product_(s=1)^(r−1) (x−u^s)` at x=1 gives +`product_(s=1)^(r−1)(1−u^s)=r`. Consequently + + f(z) = sum_(j=0)^n a_j z^j, + a_j = product_(s=j+1)^n (1−u^s). + +This identity holds for every r≥2, without a prime-power hypothesis. +Each a_j is an algebraic integer. The independent checker constructs these +tail products and separately checks that each a_j times its corresponding +prefix product equals r in Z[u]. + +## The exact obligation + +Define the conjugate reciprocal + + f*(z) = z^n conjugate(f(1/conjugate(z))) + = sum_(j=0)^n conjugate(a_(n−j)) z^j. + +For each r, CERTIFICATE.json supplies a positive integer d and two +polynomials A, B of z-degree less than n, with coefficients in Z[u], such that + + A(z) f(z) + B(z) f*(z) = d. (1) + +Every coefficient is represented in the power basis +`1,u,...,u^(phi(r)−1)`, as signed decimal integers. Both dimensions of the +nested arrays are in ascending order: outer z-powers, inner u-powers. +No numerical embedding is used. The verifier reconstructs Phi_r from +`x^r−1 = product_(s|r) Phi_s(x)` and checks (1) by polynomial multiplication +and reduction modulo Phi_r. Neither a field inverse nor a gcd is needed +to **check** the certificate. + +The generator uses extended Euclid in Q(u)[z] and clears rational +denominators. Its algebra system is not part of the independent checking +path. A nonconstant gcd would have stopped this nomination method; that did +not occur at any of the six stated radices. These six identities alone imply nothing about an untested radix. +[LIFTING.md](LIFTING.md) supplies a separate symbolic extension from three +small seed certificates to specified infinite families. + +## Why all primitive choices are covered + +Every primitive root u is a root of Phi_r. Substitution in the quotient +ring identity therefore gives (1) at **every** primitive embedding. Under +each such substitution, the automorphism `u -> u^(r−1)` used by the checker +is complex conjugation. Thus the polynomial labelled f* is the actual +conjugate reciprocal at that embedding, not just at one chosen root. +The respective numbers of embeddings are 2, 4, 4, 6, 8, 6, totalling 30. + +Write the coefficients of A and B in that power basis and let + + C = sum of the absolute values of all those integer coefficients. + +For |u|=|z|=1, the triangle inequality gives `|A(z)|+|B(z)| <= C`. +Also `|f*(z)|=|f(z)|` on |z|=1. Applying (1), + + 0 < d <= (|A(z)|+|B(z)|)|f(z)| <= C |f(z)|. + +It follows, for every primitive u and every |z|=1, that + + |P(z)| >= delta := d/(r C) > 0. (2) + +The verifier recomputes d, C and the rational delta for each case; stored +bounds are never inputs to the identity check. The dyadic bounds in the +README are rounded outward by exact integer/rational comparisons. +In particular, there is no unit-circle root. This is stronger than +nonvanishing at any finite collection of cyclic eigenvalues. + +## Inherited all-length inverse bound + +This step repeats the Fourier argument of Ali Romman's #621 with the new +certificate-derived delta. It is not a new analytic theorem or a paid +implementation. Tail products give, for every primitive embedding, + + sum_j |a_j| <= H := 2^r−1, + |P'(exp(it))| <= nH/r. + +For `g(t)=1/P(exp(it))`, (2) gives + + |g(t)| <= delta^-1, + |g'(t)| <= nH/(r delta^2). + +Let c_k be its Fourier coefficients, with average-integral normalization. +Parseval applied to g', Cauchy–Schwarz, and +`sum_(k!=0) k^-2 <= 4` imply + + sum_k |c_k| <= delta^-1 + 2nH/(r delta^2) =: M. (3) + +In particular the Fourier series is absolutely convergent; it represents +g and its product with P has Fourier coefficients those of the constant +one. If U = tau Z_L^w, where |tau|=1, L≥1 and w is any integer, then each +integer power of U has induced infinity norm one. The matrix series +`sum_k c_k U^k` converges absolutely, has norm at most M, and multiplying +by P(U) gives the identity. Therefore + + ||P(tau Z_L^w)^-1||_infinity <= M. + +No coprimality condition on w and L is required. This includes w=0 and +negative strides. Exact rational M values and outward dyadic bounds appear +in EXPECTED.json. Finite products inherit the product of these bounds by +submultiplicativity; conjugation by a unit diagonal preserves the norm. +These analytic consequences use only the explicit fixed-radix certificates +and the inherited Fourier argument, not the prime-power ideal argument. + +## Limits and attribution + +The prime-power proof in #621 has a uniform dependence on the radix. +The six literal certificates here give stronger fixed-radix bounds. +The separate lifting proof in LIFTING.md supplies a uniform estimate for +three specified composite families, not all composites. The bounds are sufficient, not optimal. This proves +no running-time, precision, preparation, reversible restoration, or tape +claim, and gives no new integer-multiplication exponent. The finite checker +is not a proof assistant or a formal verification of the full theorem. + +Ali Romman supplies the kernel-conditioning problem, conjugate-reciprocal +approach and Fourier transfer. The kernel comes from the OpenAI exact-DFT +preprint and classical q-Pochhammer/Newton factorization; see the retained +source references and NOTICE.md. Prepared for Jason Willems with substantial +OpenAI Codex assistance. Apache-2.0; no literature-priority claim. diff --git a/research/composite-cyclic-bezout/README.md b/research/composite-cyclic-bezout/README.md new file mode 100644 index 0000000000..5370003a3c --- /dev/null +++ b/research/composite-cyclic-bezout/README.md @@ -0,0 +1,131 @@ +# Composite cyclic inverses: exact certificates and modular lifting + +**Independent verification and a composite-family extension; no new κ.** +This package studies the q-Pochhammer cyclic kernel from Ali Romman's +[#621](https://github.com/CrocSwap/integer-mult-bounds/pull/621). Small +integral Bézout certificates and a modular lifting argument establish +unit-circle nonvanishing for every primitive root choice at these radices: + +| Infinite family, a>=1 | Condition on the prime p | Seed certificate denominator | +|---|---|---:| +| r=2*p^a | p not in {2,3} | 3 | +| r=3*p^a | p not in {3,43} | 43 | +| r=4*p^a | p not in {2,37} | 37 | + +The general sufficient condition is: a seed certificate +`A f_s+B f_s*=d` with coefficients in Z[v] lifts to `r=s*p^a` whenever +p does not divide s*d. The proof reduces the integral tail-product kernel +to `z^(r-s) f_s`, and its reciprocal to `f_s*`, modulo p. Coprimality then +lifts back to characteristic zero. [LIFTING.md](LIFTING.md) proves this +for **all exponents**; the finite replay is an implementation check. +Excluded primes limit this modular argument, not the characteristic-zero +conclusion. No result for all composite radices is claimed. + +Writing n=r-1, D=phi(r), H=2^r-1, the norm/cofactor and Fourier arguments +in #621 give the admitted families the explicit bounds + + delta_r = 1 / (2*r*n*H^(n*D-1)), + |P_r(z)| >= delta_r for |z|=1, + ||P_r(tau Z_L^w)^-1||_infinity + <= delta_r^-1 + 2*n*H/(r*delta_r^2). + +The inverse bound is uniform in L>=1, integer stride w and |tau|=1; +its logarithm is O(r^2 phi(r)), hence O(r^3). These loose analytic +bounds do not supply an efficient rounded implementation or a combined +precision guard. + +## Stronger fixed-radix certificates + +Six separate integer certificates cover all non-prime-power radices +between 3 and 18. They yield substantially sharper bounds than the general +formula, including cases excluded by a particular seed's lifting route: + +| Radix r | Primitive embeddings | Certified circle bound | Certified inverse ∞-norm bound | +|---:|---:|---:|---:| +| 6 | 2 | ≥ 2^-5 | ≤ 2^16 | +| 10 | 4 | ≥ 2^-8 | ≤ 2^27 | +| 12 | 4 | ≥ 2^-9 | ≤ 2^30 | +| 14 | 6 | ≥ 2^-10 | ≤ 2^33 | +| 15 | 8 | ≥ 2^-13 | ≤ 2^41 | +| 18 | 6 | ≥ 2^-11 | ≤ 2^41 | + +The dyadic bounds are rounded outward from exact rational bounds in +[EXPECTED.json](EXPECTED.json). [PROOF.md](PROOF.md) explains why the +identities cover every primitive embedding and the entire unit circle, +and repeats the inherited all-length Fourier transfer. + +## Reproduce without third-party packages + +Run from the repository root with Python 3.11+: + +```sh +python3 -B -I -O research/composite-cyclic-bezout/verify.py --check research/composite-cyclic-bezout/EXPECTED.json +python3 -B -I -O research/composite-cyclic-bezout/verify_lifting.py --check research/composite-cyclic-bezout/LIFTING-EXPECTED.json +python3 -B -I research/composite-cyclic-bezout/test_verify.py +python3 -B -I research/composite-cyclic-bezout/test_lifting.py +``` + +The first two commands report: + +```text +PASS: 6 identities, 30 primitive embeddings, 39 negative controls +PASS: 3 exact seeds, 54 modular lifts, 3 excluded-prime witnesses, 173 controls +``` + +verify.py reconstructs cyclotomic polynomials by exact integer division, +checks prefix/tail identities, and checks Bézout identities using integer +polynomial multiplication and reduction. It imports neither SymPy nor a +#621 checker, and does not trust stored kernel coefficients, bounds, +resultants or the generator. verify_lifting.py reuses that independent +arithmetic for its seeds and computes in `(F_p[v]/Phi_s(v))[z]` for the +finite diagnostics, even when Phi_s is reducible modulo p. It checks the +cyclotomic and tail-product reductions and constructs an explicit lifted +modular Bézout identity. All checks remain active under optimized Python. + +Mutations test corrupted identities, missing or duplicate cases, omitted +shifts, incorrectly shifted reciprocals and invalid admission. Excluded-prime +witnesses show genuine modular common factors at (s,p)=(2,3),(3,43),(4,37); +they do not assert a complex-unit-circle counterexample. The focused tests +also check external corrupted-certificate CLI failure. + +## Optional deterministic regeneration + +Only nomination needs SymPy 1.14.0; the two checkers do not: + +```sh +python3 -m venv /tmp/composite-cyclic-env +/tmp/composite-cyclic-env/bin/python -m pip install -r research/composite-cyclic-bezout/requirements-generate.txt +/tmp/composite-cyclic-env/bin/python -B -I research/composite-cyclic-bezout/generate.py --output /tmp/composite-cyclic-certificate.json +cmp research/composite-cyclic-bezout/CERTIFICATE.json /tmp/composite-cyclic-certificate.json +/tmp/composite-cyclic-env/bin/python -B -I research/composite-cyclic-bezout/generate.py --lifting-seeds --output /tmp/composite-lifting-seeds.json +cmp research/composite-cyclic-bezout/LIFTING-SEEDS.json /tmp/composite-lifting-seeds.json +``` + +The generator applies extended Euclid in Q(u)[z] and clears denominators. +The certificate generator is outside the checking trust boundary. The +written all-exponent proof is not generated by this program. + +## Scope and provenance + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. The selected conditional +bound remains κ = 51110230636731/31250000000000000 (#626/#543). +This package changes no supplier, selected certificate or `upstream/` file. + +#621 proves a uniform prime-power theorem and supplies the kernel, +reciprocal method, norm/cofactor estimates and Fourier transfer used here. +The added result is a seed-certificate lifting mechanism for specified +composite families, plus six direct composite certificates and a separate +checker. #628 concerns rounded prime-power inversion and restoration; +concurrent #668 audits prime-power resultants with split-prime CRT. Neither +is certified or used as a dependency here. No paid coefficient preparation, +precision/error propagation, scratch restoration, tape scheduling or +integer-multiplication improvement is claimed. + +The exact certificates and written proof establish the stated properties +subject to ordinary mathematical review and checker trust. This is not a +proof-assistant formalization or a full multiplication-theorem audit. +[SOURCE.json](SOURCE.json) pins the base and inherited source bytes; +[CLAIM.md](CLAIM.md) and [CONTINUATION.md](CONTINUATION.md) record seed **82**, +task selection, overlap checks and results. [VALIDATION.md](VALIDATION.md) +records execution evidence. Attribution and substantial AI assistance, +including separate agent reviews, are in [NOTICE.md](NOTICE.md). diff --git a/research/composite-cyclic-bezout/SOURCE.json b/research/composite-cyclic-bezout/SOURCE.json new file mode 100644 index 0000000000..3b28e047f7 --- /dev/null +++ b/research/composite-cyclic-bezout/SOURCE.json @@ -0,0 +1,22 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "predecessor": { + "pr": 621, + "author": "Ali Romman (@aliromman)", + "reviewed_head": "520774462b19b29af41554b74def31f9d01e997e", + "scope": "Kernel definition, conjugate-reciprocal method, norm/cofactor lower bound, and Fourier inverse-norm transfer. No producer code is imported." + }, + "generator": { + "python_package": "sympy==1.14.0", + "method": "Extended Euclidean algorithm over Q(u)[z]; clear rational denominators." + }, + "independent_verifier": "Python standard library; integer arithmetic in Z[u,z]/(Phi_r(u)); tail products, no division in Q(u), polynomial gcd or symbolic-library imports.", + "input_sha256": { + "research/prime-power-cyclic-inverse/PROOF.md": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e", + "research/prime-power-cyclic-inverse/SOURCE.json": "81217e4ecbb1da767d6a23f043d66e69d53c9001c056176efc641ddadea275f2", + "research/prime-power-cyclic-inverse/NOTICE.md": "96111c95cfec3c03a6f69c8e02c5d0bceff957d187e638d0534c676d6e3ffd77", + "research/prime-power-cyclic-inverse/verify.py": "40e5e18cbd98d39ba6d0bb036778ccacc077dff009099a54b9c8f441af5d6a56", + "research/prime-power-cyclic-inverse/independent_verify.py": "515d60fbbb28c025251b5a2929231b4b6124dabe357b8526fdb93c1456c847ce" + }, + "lifting_verifier": "Python standard library; reuses the separate integer verifier for seed identities and implements arithmetic in (F_p[u]/Phi_s(u))[z] for finite lifting diagnostics. Excluded-prime witnesses use polynomial gcd only over F_p." +} diff --git a/research/composite-cyclic-bezout/VALIDATION.md b/research/composite-cyclic-bezout/VALIDATION.md new file mode 100644 index 0000000000..22365055f3 --- /dev/null +++ b/research/composite-cyclic-bezout/VALIDATION.md @@ -0,0 +1,143 @@ +# Validation receipt + +Executed on 2026-10-12 America/Los_Angeles (2026-10-13 UTC), on macOS +14.4.1 arm64. Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +This is local contributor validation with substantial OpenAI Codex assistance, +not independent human review or a full multiplication-theorem audit. + +## Completed package checks + +- Standard-library verifier: **6 identities, all 30 primitive embeddings + covered symbolically, 39 rejected mathematical/coverage controls**. +- Public `-B -I -O --check EXPECTED.json` command passed under Python + **3.9.6, 3.11.13 and 3.13.4**, with identical deterministic receipt bytes. +- **8 original focused tests** passed under each of those Python versions. They cover + explicit cyclotomic formulas, conjugation, integer polynomial division, + acceptance of an alternative valid scaled witness, outward dyadic bounds, + corrupted-certificate CLI failures with and without optimization, malformed + domain/encoding rejection, and full receipt recomputation. +- Fresh regeneration using Python 3.9.6 and, after the continuation, + Python 3.11.13 / SymPy 1.14.0 / mpmath 1.3.0: + `CERTIFICATE.json` reproduced byte for byte and the independently checked + receipt matched `EXPECTED.json` exactly. +- The predecessor's standard-library `verify.py` reproduced + `research/prime-power-cyclic-inverse/EXPECTED.json` byte for byte. +- `python3 -B scripts/verify_selected_result.py` passed: selected κ, + source inventory and proof supplements retain their pinned content. +- `upstream/`, selected certificates, supplier code and root Makefile were + unchanged. Only this new package and its scoped workflow are submitted. + +## Continued modular lifting checks + +- The exact seed identities at s=2,3,4 have denominators 3,43,37. + The public isolated, optimized lifting check from the README passed on + **Python 3.9.6, + 3.11.13 and 3.13.4** with identical receipt bytes: **54 admitted finite + lifts, three excluded-prime common-factor witnesses and 173 rejected + mutation/admission controls**. +- **8 additional focused tests** passed on all three versions (16 tests + total). They cover excluded primes, exponent guards, division with + reducible cyclotomic coefficient rings, reciprocal degree loss, rejection + through the positive validation paths, and externally corrupted seed + certificates under normal and optimized Python. +- Fresh `generate.py --lifting-seeds` with Python 3.11.13 / SymPy 1.14.0 + reproduced LIFTING-SEEDS.json byte for byte. The original six-certificate + regeneration also remained byte-identical after adding this option. +- A separate Codex agent reviewed the all-exponent proof in LIFTING.md, + including exact residue order, common-root integrality, Sylvester degree + loss, and the inherited norm/cofactor exponents; no mathematical errors + were found. A second agent reviewed the checker and improved the real + rejection controls and negative-exponent guard. These are AI reviews, + not independent human review or proof-assistant verification. +- Documentation links and whitespace checks pass. All inherited source + pins still pass; the selected record and upstream content are unchanged. + +## Broader repository verification + +The initial sprint did not run root `make verify`. The continuation started +it with Python 3.11.13, NumPy 2.2.6, SciPy 1.15.3, SymPy 1.14.0, mpmath 1.3.0 +and installed Boost headers in an isolated temporary environment: + +```sh +env PATH=/tmp/integer-mult-full-venv/bin:/opt/homebrew/bin:/usr/bin:/bin:/usr/sbin:/sbin BOOST_INCLUDE=/opt/homebrew/include CPATH=/opt/homebrew/include make verify +``` + +The initial invocation passed the community/producer groups, earlier gen4 +construction, selected #543+#626 cold replay, historical certificates, +ternary and research audits, and skip-strips checks. It then exited **2** +in `skip-suffix-producer`: Apple clang rejected the existing `-fopenmp` +option. This was a local compiler configuration failure, not a certificate +failure. No repository source or expected artifact was changed to resolve it. + +The already installed **libomp 19.1.5** was used through a temporary CXX +adapter. It forwards arguments to `/usr/bin/clang++`, translates `-fopenmp` +to `-Xpreprocessor -fopenmp`, and adds the installed runtime's include/library +paths, rpath and `-lomp`. An OpenMP compile/run smoke check passed. The failed +stage and every remaining target were then resumed, preserving the completed +prefix of the original run: + +```sh +env PATH=/tmp/integer-mult-full-venv/bin:/opt/homebrew/bin:/usr/bin:/bin:/usr/sbin:/sbin BOOST_INCLUDE=/opt/homebrew/include CPATH=/opt/homebrew/include CXX=/tmp/integer-mult-openmp-cxx make skip-suffix-verify verify-clones verify-positive verify-joint verify-pair verify-tests +``` + +The resumed command exited **0**, completing **all 84 test modules in +isolated interpreters** and all patch-application checks. Together, the +initial run and resumed tail cover every component of the root verification +sequence. Verification completed at 2026-10-13 **04:42 UTC**. + +The cold selected-composition replay separately returned +`PASS_REBUILT_PR543_PR626_COMPOSITION` with exact +κ = `51110230636731/31250000000000000`. All six steps passed: bit543, +declarations, complex626, independent-owner, helper-interface and bindings. +Its inherited all-size, realization, hosting, precision/tape and analytic +assumptions remain conditional; finite replay does not discharge them. + +Local console-log digests (run identification, not mathematical admission): + +- Initial run, exit 2 at the OpenMP compiler flag: + `d3fca41f0dd3b013c04b0f22144083c3d8639613a2fb345c948faab891d64460`. +- Resumed tail, exit 0: + `8da6eaa07cdf6897776fe82357241f499d5e2a97096ab00fbb9bd026e87f7fc7`. + +After regeneration, Git showed no changed files outside this research +package and its scoped workflow. The workflow requests Linux Python +3.11/3.14 checks, but GitHub reported no remote check results at handoff. + +## Exact artifacts + +- CERTIFICATE.json SHA256: `09623c781498d9c7df554f7e8f6e6c684cf3d9073db4198a4d647dcd2b6d4ab1` +- EXPECTED.json SHA256: `a33ed6b23d43562032fd88ef9969fae069e4817c17c81ab33000fb12fea1c928` +- LIFTING-SEEDS.json SHA256: `63fd8312f93d01818a9f43608f26844c2f1b65ab944a609f07994c4e766e02bb` +- LIFTING-EXPECTED.json SHA256: `4c8aa560141f9b03b42953f2b8ab35bce5866ee90f40e93743543f90fc2319f3` + +These hash immutable submitted artifacts. Admission itself reconstructs and +checks every proof-relevant identity rather than accepting an artifact hash. +A reader can replace the certificate with a different valid witness. + +## Live overlap check + +The initial packaging refreshed **484 open PRs through #664**. +New #661 concerns fixed-order R420 frame optimality, #662 accelerates Clifford +checks, and #663 audits PR628 dirty restoration/leaf counts. Their stated +scopes do not duplicate the six non-prime-power Bézout certificates here. +#621 has no review comments in the inspected issue-comment endpoint; its +retained review and exact source head remain the dependencies. The repository +has no pinned coordination issue, so the claim and result are recorded locally. + +The continuation refreshed **500 open PRs through #680**. New #673 develops +a multiway dirty-echo schedule and phase-alias repair based on #628 and +explicitly distinguishes this composite-nonvanishing package. #668 uses +split-prime CRT for prime-power resultants through 27; it supplies no +composite seed-lifting mechanism. The other new entries concern decoder +obstructions, local XOR circuits, owner maps, exponential intervals, supplier +boundaries, bit moments, selector batching and fixed Clifford words. No +overlapping composite lifting claim was identified. Upstream still points +to the recorded base and the pinned-issue list remains empty. + +At final handoff, **533 open PRs through #714** were refreshed. #692 concerns +weighted-stride closure and bilinear duality and explicitly distinguishes +this composite-lifting result; #695 consolidates selected Linux replay +evidence. Later additions concern other suppliers, local circuits, moment +or wrapper audits, tooling, and dirty-call scheduling. No duplicate +composite seed-lifting mechanism was identified. The upstream base is still +`66849e1475c930fd7732b1a0067ffee7e1e95f60`; there is still no pinned issue. diff --git a/research/composite-cyclic-bezout/generate.py b/research/composite-cyclic-bezout/generate.py new file mode 100644 index 0000000000..167cd3568c --- /dev/null +++ b/research/composite-cyclic-bezout/generate.py @@ -0,0 +1,85 @@ +#!/usr/bin/env python3 +"""Nominate exact composite-radix Bezout witnesses using SymPy 1.14.0. + +The standard-library verifier does not import this file or SymPy. +""" +import argparse +from functools import reduce +from math import gcd +import json +from pathlib import Path + +import sympy +from sympy import Poly, QQ, Symbol, cyclotomic_poly + +ORDERS = (6, 10, 12, 14, 15, 18) + + +def lcm(a, b): + return a // gcd(a, b) * b + + +def nominate(order): + x, z = Symbol('x'), Symbol('z') + field = QQ.alg_field_from_poly(Poly(cyclotomic_poly(order, x), x), alias='u') + u = field([1, 0]) + prefix = field.one + coefficients = [] + for j in range(order): + if j: + prefix *= field.one - u ** j + coefficients.append(field(order) / prefix) + + def conjugate(value): + result = field.zero + for coefficient in value.to_list(): + result = result * u ** (order - 1) + field(coefficient) + return result + + f = Poly.from_list(list(reversed(coefficients)), z, domain=field) + star = Poly.from_list([conjugate(a) for a in coefficients], z, domain=field) + a, b, common = f.gcdex(star) + if common != Poly(1, z, domain=field): + raise ValueError('Nonconstant gcd at order %d: %s' % (order, common)) + if a * f + b * star != common: + raise ValueError('SymPy Bezout identity failed') + + # Encode in ascending powers of z and then ascending powers of u. + rows = [list(reversed(c.to_list())) for p in (a, b) + for c in reversed(p.rep.to_list())] + denominator = reduce(lcm, (int(c.denominator) for row in rows for c in row), 1) + + def encode(p): + return [[str(int(c * denominator)) for c in reversed(value.to_list())] or ['0'] + for value in reversed(p.rep.to_list())] + + result = {'order': order, 'denominator': str(denominator), + 'a': encode(a), 'b': encode(b)} + integers = [int(c) for key in ('a', 'b') for row in result[key] for c in row] + divisor = reduce(gcd, integers, denominator) + result['denominator'] = str(denominator // divisor) + for key in ('a', 'b'): + result[key] = [[str(int(c) // divisor) for c in row] for row in result[key]] + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path, required=True) + parser.add_argument('--lifting-seeds', action='store_true', + help='Generate the three small seeds for the lifting lemma') + args = parser.parse_args() + if sympy.__version__ != '1.14.0': + raise ValueError('Regeneration is pinned to SymPy 1.14.0') + cases = [] + for order in ((2, 3, 4) if args.lifting_seeds else ORDERS): + cases.append(nominate(order)) + print('Nominated order %d' % order, flush=True) + certificate = {'format': ('cyclic-lifting-seeds-v1' if args.lifting_seeds + else 'composite-cyclic-bezout-v1'), + 'coefficient_order': 'ascending z, ascending u', 'cases': cases} + args.output.write_text(json.dumps(certificate, indent=2) + '\n') + + +if __name__ == '__main__': + main() diff --git a/research/composite-cyclic-bezout/requirements-generate.txt b/research/composite-cyclic-bezout/requirements-generate.txt new file mode 100644 index 0000000000..de9542d36e --- /dev/null +++ b/research/composite-cyclic-bezout/requirements-generate.txt @@ -0,0 +1,2 @@ +sympy==1.14.0 +mpmath==1.3.0 diff --git a/research/composite-cyclic-bezout/test_lifting.py b/research/composite-cyclic-bezout/test_lifting.py new file mode 100644 index 0000000000..49c4d84b01 --- /dev/null +++ b/research/composite-cyclic-bezout/test_lifting.py @@ -0,0 +1,117 @@ +#!/usr/bin/env python3 +"""Focused ring-arithmetic and fail-closed tests for modular lifting checks.""" +from copy import deepcopy +import importlib.util +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('lifting_check', HERE / 'verify_lifting.py') +check = importlib.util.module_from_spec(spec) +spec.loader.exec_module(check) + + +class LiftingTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.document = json.loads((HERE / 'LIFTING-SEEDS.json').read_text()) + + def test_excluded_primes_and_composite_moduli_are_rejected(self): + for case, prime in zip(self.document['cases'], (3, 43, 37)): + with self.subTest(seed=case['order'], prime=prime): + with self.assertRaisesRegex(ValueError, 'Seed denominator vanishes'): + check.finite_instance(case, prime, 1) + prime = 3 if case['order'] == 3 else 2 + with self.subTest(seed=case['order'], prime=prime): + with self.assertRaisesRegex(ValueError, 'Prime divides the seed radix'): + check.finite_instance(case, prime, 1) + for prime in (1, 4, 25, True): + with self.subTest(prime=prime), self.assertRaisesRegex(ValueError, 'not prime'): + check.finite_instance(self.document['cases'][0], prime, 1) + + def test_lifting_exponent_must_be_a_positive_integer(self): + for exponent in (0, -1, True, 1.0): + with self.subTest(exponent=exponent): + with self.assertRaisesRegex(ValueError, 'Exponent must be positive'): + check.finite_instance(self.document['cases'][0], 5, exponent) + + def test_modular_power_rejects_negative_exponents_and_allows_zero(self): + mod = check.Modular(3, 7) + modulus = [(1,), (3,)] + self.assertEqual(mod.zpowmod([(0,), (1,)], 0, modulus), [(1,)]) + # z = -1/3 = 2 modulo 1+3z over F_7, so z^5 = 4. + self.assertEqual(mod.zpowmod([(0,), (1,)], 5, modulus), [(4,)]) + for exponent in (-1, True, 0.5): + with self.subTest(exponent=exponent): + with self.assertRaisesRegex(ValueError, 'Power exponent must be nonnegative'): + mod.zpowmod([(0,), (1,)], exponent, modulus) + + def test_division_works_over_reducible_cyclotomic_coefficient_ring(self): + # Phi_3 = (u-2)(u-4) mod 7: the coefficient ring has zero divisors. + mod = check.Modular(3, 7) + left, right = (5, 1), (3, 1) + self.assertNotEqual(left, (0,)) + self.assertNotEqual(right, (0,)) + self.assertEqual(mod.mul(left, right), (0,)) + # Divide (6+3u)+(5+3u)z+4z^2 by 1+3z using only scalar inversion. + quotient, remainder = mod.zdiv([(6, 3), (5, 3), (4,)], [(1,), (3,)]) + self.assertEqual(quotient, [(2, 1), (6,)]) + self.assertEqual(remainder, [(4, 2)]) + with self.assertRaisesRegex(ValueError, 'Nonunit scalar leading coefficient'): + mod.zdiv([(1,), (1,)], [(1,), left]) + self.assertEqual(check.finite_instance(self.document['cases'][1], 7, 1)['radix'], 21) + + def test_reciprocal_preserves_fixed_degree_before_reduction(self): + # At s=3, p=2, r=6, reversal has three trailing zeros after reduction. + mod = check.Modular(3, 2) + reduced = check.literal_reduction(mod, 6) + star = check.literal_reduction(mod, 6, reciprocal=True) + self.assertEqual(reduced, [(0,), (0,), (0,), (1,), (0, 1), (1,)]) + self.assertEqual(star, [(1,), (1, 1), (1,), (0,), (0,), (0,)]) + self.assertEqual(check.base.ztrim(star), [(1,), (1, 1), (1,)]) + self.assertEqual(check.finite_instance(self.document['cases'][1], 2, 1)['radix'], 6) + + def test_mutated_obligations_reach_the_positive_validation_paths(self): + mod = check.Modular(2, 5) + f, star = [(2,), (1,)], [(1,), (2,)] + reduced = [(0,)] * 8 + f + reduced_star = star + [(0,)] * 8 + check.check_reductions(f, star, reduced, reduced_star, 8) + with self.assertRaisesRegex(ValueError, 'Tail-product shift identity failed'): + check.check_reductions(f, star, f, reduced_star, 8) + with self.assertRaisesRegex(ValueError, 'Reciprocal reduction identity failed'): + check.check_reductions(f, star, reduced, [(0,)] * 8 + star, 8) + check.check_modular_identity(mod, f, star, [(2,)], [(4,)], 3) + with self.assertRaisesRegex(ValueError, 'Modular Bezout identity failed'): + check.check_modular_identity(mod, [(2,), (2,)], star, [(2,)], [(4,)], 3) + + def test_cli_rejects_corrupted_seed_even_under_optimization(self): + document = deepcopy(self.document) + a = document['cases'][0]['a'][0] + a[0] = str(int(a[0]) + 1) + with tempfile.TemporaryDirectory(prefix='lifting-bezout-test-') as directory: + path = Path(directory) / 'corrupt.json' + path.write_text(json.dumps(document)) + for flags in (['-B', '-I'], ['-B', '-I', '-O']): + with self.subTest(flags=flags): + result = subprocess.run([sys.executable, *flags, str(HERE / 'verify_lifting.py'), + '--seeds', str(path)], text=True, capture_output=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn('Bezout identity failed', result.stderr) + self.assertNotIn('PASS:', result.stdout) + + def test_public_receipt_is_recomputed_under_optimization(self): + result = subprocess.run([sys.executable, '-B', '-I', '-O', str(HERE / 'verify_lifting.py'), + '--check', str(HERE / 'LIFTING-EXPECTED.json')], + text=True, capture_output=True) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn('PASS: 3 exact seeds, 54 modular lifts, 3 excluded-prime witnesses, 173 controls', + result.stdout) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/composite-cyclic-bezout/test_verify.py b/research/composite-cyclic-bezout/test_verify.py new file mode 100644 index 0000000000..f34d83e3e3 --- /dev/null +++ b/research/composite-cyclic-bezout/test_verify.py @@ -0,0 +1,109 @@ +#!/usr/bin/env python3 +"""Focused mathematical and fail-closed tests for the certificate checker.""" +from copy import deepcopy +from fractions import Fraction +import importlib.util +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('composite_check', HERE / 'verify.py') +check = importlib.util.module_from_spec(spec) +spec.loader.exec_module(check) + + +class CertificateTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.document = json.loads((HERE / 'CERTIFICATE.json').read_text()) + cls.receipt = json.loads((HERE / 'EXPECTED.json').read_text()) + + def test_cyclotomic_moduli_against_explicit_formulas(self): + known = { + 6: (1, -1, 1), 10: (1, -1, 1, -1, 1), + 12: (1, 0, -1, 0, 1), 14: (1, -1, 1, -1, 1, -1, 1), + 15: (1, -1, 0, 1, -1, 1, 0, -1, 1), + 18: (1, 0, 0, -1, 0, 0, 1), + } + for order, coefficients in known.items(): + with self.subTest(order=order): + self.assertEqual(check.cyclotomic(order), coefficients) + + def test_conjugation_and_primitive_root_relation(self): + ring = check.Ring(6) + self.assertEqual(ring.conjugate(ring.u), (1, -1)) + self.assertEqual(ring.mul(ring.u, ring.conjugate(ring.u)), (1,)) + for order in check.ORDERS: + ring = check.Ring(order) + for power in ring.powers: + self.assertEqual(ring.conjugate(ring.conjugate(power)), power) + self.assertEqual(ring.mul(power, ring.conjugate(power)), (1,)) + + def test_constant_and_wrapped_polynomial_division(self): + # (x^4 + 1)/(x^2 + 1) = x^2 - 1 + 2/(x^2 + 1). + self.assertEqual(check.monic_divide((1, 0, 0, 0, 1), (1, 0, 1)), + ((-1, 0, 1), (2,))) + self.assertEqual(check.monic_divide((0,), (1,)), ((0,), (0,))) + with self.assertRaises(ValueError): + check.monic_divide((1, 2), (2,)) + + def test_alternative_valid_scaled_certificate_is_accepted(self): + # Admission checks the identity, not equality to generator bytes. + case = deepcopy(self.document['cases'][0]) + expected = check.check_case(case) + case['denominator'] = str(7 * int(case['denominator'])) + for name in ('a', 'b'): + case[name] = [[str(7 * int(c)) for c in row] for row in case[name]] + actual = check.check_case(case) + self.assertEqual(actual['circle_lower_bound'], expected['circle_lower_bound']) + self.assertEqual(actual['inverse_infinity_upper_bound'], expected['inverse_infinity_upper_bound']) + + def test_outward_dyadic_bounds_and_fourier_constant(self): + for row in self.receipt['cases']: + delta = Fraction(row['circle_lower_bound']) + bound = Fraction(row['inverse_infinity_upper_bound']) + circle = Fraction(2) ** row['circle_lower_bound_dyadic_exponent'] + inverse = Fraction(2) ** row['inverse_infinity_upper_bound_dyadic_exponent'] + self.assertLessEqual(circle, delta) + self.assertLess(delta, 2 * circle) + self.assertLessEqual(bound, inverse) + self.assertGreater(bound, inverse / 2) + r = row['order'] + self.assertEqual(bound, 1 / delta + Fraction(2 * (r - 1) * (2 ** r - 1), r) / delta ** 2) + + def test_certificate_cli_rejects_corruption_even_under_optimization(self): + document = deepcopy(self.document) + a = document['cases'][0]['a'][0] + a[0] = str(int(a[0]) + 1) + with tempfile.TemporaryDirectory(prefix='composite-bezout-test-') as directory: + path = Path(directory) / 'corrupt.json' + path.write_text(json.dumps(document)) + for flags in (['-B', '-I'], ['-B', '-I', '-O']): + result = subprocess.run([sys.executable, *flags, str(HERE / 'verify.py'), + '--certificate', str(path)], text=True, capture_output=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn('Bezout identity failed', result.stderr) + self.assertNotIn('PASS:', result.stdout) + + def test_complete_domain_and_integer_encoding_fail_closed(self): + bad = deepcopy(self.document) + bad['cases'][0]['order'] = True + with self.assertRaises(ValueError): + check.verify(bad) + for value in ('01', '-0', 1.0, True, '1/2'): + with self.subTest(value=value), self.assertRaises(ValueError): + check.integer(value) + + def test_public_receipt_is_recomputed(self): + result = subprocess.run([sys.executable, '-B', '-I', '-O', str(HERE / 'verify.py'), + '--check', str(HERE / 'EXPECTED.json')], text=True, capture_output=True) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn('PASS: 6 identities, 30 primitive embeddings, 39 negative controls', result.stdout) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/composite-cyclic-bezout/verify.py b/research/composite-cyclic-bezout/verify.py new file mode 100644 index 0000000000..74d571b016 --- /dev/null +++ b/research/composite-cyclic-bezout/verify.py @@ -0,0 +1,275 @@ +#!/usr/bin/env python3 +"""Check six exact Bezout certificates without SymPy or producer imports.""" +import argparse +from copy import deepcopy +from fractions import Fraction +from functools import lru_cache +import hashlib +import json +from math import gcd +from pathlib import Path + +ORDERS = (6, 10, 12, 14, 15, 18) +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def trim(values): + values = list(values) + while len(values) > 1 and values[-1] == 0: + values.pop() + return tuple(values or [0]) + + +def add(a, b): + return trim([(a[i] if i < len(a) else 0) + (b[i] if i < len(b) else 0) + for i in range(max(len(a), len(b)))]) + + +def multiply(a, b): + result = [0] * (len(a) + len(b) - 1) + for i, left in enumerate(a): + for j, right in enumerate(b): + result[i + j] += left * right + return trim(result) + + +def monic_divide(a, b): + require(b[-1] == 1, 'Nonmonic integer polynomial divisor') + remainder = list(a) + quotient = [0] * max(1, len(a) - len(b) + 1) + while len(remainder) >= len(b) and trim(remainder) != (0,): + offset = len(remainder) - len(b) + coefficient = remainder[-1] + quotient[offset] = coefficient + for i, value in enumerate(b): + remainder[offset + i] -= coefficient * value + remainder = list(trim(remainder)) + return trim(quotient), trim(remainder) + + +@lru_cache(None) +def cyclotomic(order): + # x^n - 1 = product_(d|n) Phi_d(x); no producer's field representation. + polynomial = (-1,) + (0,) * (order - 1) + (1,) + for divisor in range(1, order): + if order % divisor == 0: + polynomial, remainder = monic_divide(polynomial, cyclotomic(divisor)) + require(remainder == (0,), 'Cyclotomic factorization is not exact') + return polynomial + + +class Ring: + """Z[u] represented as integer coefficients modulo Phi_order(u).""" + def __init__(self, order): + self.order = order + self.modulus = cyclotomic(order) + self.degree = len(self.modulus) - 1 + self.u = self.reduce((0, 1)) + self.powers = [(1,)] + for _ in range(order): + self.powers.append(self.mul(self.powers[-1], self.u)) + require(self.powers[order] == (1,), 'u^order != 1') + require(all(self.powers[j] != (1,) for j in range(1, order)), + 'u is not primitive') + require(self.degree == sum(gcd(j, order) == 1 for j in range(order)), + 'Wrong cyclotomic degree') + + def reduce(self, value): + return monic_divide(trim(value), self.modulus)[1] + + def mul(self, a, b): + return self.reduce(multiply(a, b)) + + def conjugate(self, value): + result = (0,) + for i, coefficient in enumerate(value): + result = add(result, tuple(coefficient * x + for x in self.powers[(-i) % self.order])) + return trim(result) + + def zmul(self, a, b): + result = [(0,)] * (len(a) + len(b) - 1) + for i, left in enumerate(a): + for j, right in enumerate(b): + result[i + j] = add(result[i + j], self.mul(left, right)) + return ztrim(result) + + +def ztrim(values): + values = list(values) + while len(values) > 1 and values[-1] == (0,): + values.pop() + return values or [(0,)] + + +def zadd(a, b): + return ztrim([add(a[i] if i < len(a) else (0,), + b[i] if i < len(b) else (0,)) + for i in range(max(len(a), len(b)))]) + + +def kernel(ring): + # Reconstruct r*P using tail products, without field division or h_j. + order = ring.order + f = [(1,)] * order + for j in range(order - 2, -1, -1): + factor = add((1,), tuple(-c for c in ring.powers[j + 1])) + f[j] = ring.mul(f[j + 1], factor) + require(f[0] == (order,) and f[-1] == (1,), 'Wrong kernel endpoints') + # Independently bind every tail coefficient to the prefix definition r*h_j. + prefix = (1,) + for j in range(order): + if j: + factor = add((1,), tuple(-c for c in ring.powers[j])) + prefix = ring.mul(prefix, factor) + require(ring.mul(prefix, f[j]) == (order,), 'Prefix/tail identity failed') + return f + + +def integer(value): + require(isinstance(value, str), 'Integer coefficients must be strings') + result = int(value) + require(str(result) == value, 'Noncanonical integer encoding') + return result + + +def decode(rows, ring): + require(isinstance(rows, list) and 1 <= len(rows) < ring.order, + 'Wrong z-degree or empty polynomial') + result = [] + for row in rows: + require(isinstance(row, list) and 1 <= len(row) <= ring.degree, + 'Wrong u-degree or empty coefficient') + coefficient = tuple(integer(c) for c in row) + require(trim(coefficient) == coefficient, 'Unreduced coefficient encoding') + result.append(coefficient) + require(ztrim(result) == result, 'Trailing zero z coefficient') + return result + + +def check_identity(ring, f, star, a, b, denominator): + actual = zadd(ring.zmul(a, f), ring.zmul(b, star)) + require(actual == [(denominator,)], 'Bezout identity failed') + + +def reject(name, action): + try: + action() + except ValueError: + return name + raise ValueError('Negative control unexpectedly accepted: ' + name) + + +def check_case(case): + require(set(case) == {'order', 'denominator', 'a', 'b'}, 'Wrong case fields') + order = case['order'] + require(type(order) is int and order in ORDERS, 'Unexpected radix') + ring = Ring(order) + f = kernel(ring) + star = [ring.conjugate(c) for c in reversed(f)] + a, b = decode(case['a'], ring), decode(case['b'], ring) + denominator = integer(case['denominator']) + require(denominator > 0, 'Nonpositive Bezout denominator') + check_identity(ring, f, star, a, b, denominator) + coefficient_sum = sum(abs(c) for p in (a, b) for row in p for c in row) + require(coefficient_sum > 0, 'Empty Bezout bound') + delta = Fraction(denominator, order * coefficient_sum) + inverse_bound = 1 / delta + Fraction(2 * (order - 1) * (2 ** order - 1), order) / delta ** 2 + + circle_bits = 0 + while delta * (1 << circle_bits) < 1: + circle_bits += 1 + inverse_bits = 0 + while (1 << inverse_bits) < inverse_bound: + inverse_bits += 1 + + # Mutate mathematical obligations; no hash check can reject these first. + changed_a = list(a) + changed_a[0] = add(changed_a[0], (1,)) + changed_f = list(f) + changed_f[0] = add(changed_f[0], (1,)) + controls = [ + reject('changed_bezout_coefficient', lambda: check_identity( + ring, f, star, changed_a, b, denominator)), + reject('changed_denominator', lambda: check_identity( + ring, f, star, a, b, denominator + 1)), + reject('missing_conjugation', lambda: check_identity( + ring, f, list(reversed(f)), a, b, denominator)), + reject('missing_reversal', lambda: check_identity( + ring, f, [ring.conjugate(c) for c in f], a, b, denominator)), + reject('changed_kernel_constant', lambda: check_identity( + ring, changed_f, star, a, b, denominator)), + reject('omitted_second_bezout_term', lambda: check_identity( + ring, f, star, a, [(0,)], denominator)), + ] + return {'order': order, 'primitive_embeddings_covered': ring.degree, + 'bezout_denominator': str(denominator), + 'bezout_coefficient_l1': str(coefficient_sum), + 'circle_lower_bound': str(delta), + 'circle_lower_bound_dyadic_exponent': -circle_bits, + 'inverse_infinity_upper_bound': str(inverse_bound), + 'inverse_infinity_upper_bound_dyadic_exponent': inverse_bits, + 'negative_controls_rejected': controls} + + +def validate_document(document): + require(set(document) == {'format', 'coefficient_order', 'cases'}, 'Wrong document fields') + require(document['format'] == 'composite-cyclic-bezout-v1', 'Wrong format') + require(document['coefficient_order'] == 'ascending z, ascending u', 'Wrong coefficient order') + require(isinstance(document['cases'], list), 'Cases must be a list') + require([case['order'] for case in document['cases']] == list(ORDERS), + 'Missing, duplicate, reordered or unexpected radix') + + +def verify(document): + validate_document(document) + cases = [check_case(case) for case in document['cases']] + missing, duplicate = deepcopy(document), deepcopy(document) + missing['cases'].pop() + duplicate['cases'][-1] = duplicate['cases'][0] + controls = [reject('missing_radix', lambda: validate_document(missing)), + reject('duplicate_radix', lambda: validate_document(duplicate))] + # A unit-circle root must never admit a nonzero constant Bezout identity. + # z-1 and its conjugate reciprocal 1-z vanish at z=1 over every field. + ring = Ring(6) + controls.append(reject('false_unit_root_witness', lambda: check_identity( + ring, [(-1,), (1,)], [(1,), (-1,)], [(1,)], [(1,)], 1))) + return {'status': 'PASS', 'scope': 'six exact composite-radix Bezout identities; no new kappa', + 'cases': cases, 'additional_negative_controls_rejected': controls, + 'identities': len(cases), + 'primitive_embeddings_covered': sum(c['primitive_embeddings_covered'] for c in cases), + 'negative_controls_rejected': sum(len(c['negative_controls_rejected']) for c in cases) + len(controls)} + + +def check_sources(): + source = json.loads((HERE / 'SOURCE.json').read_text()) + root = HERE.parent.parent + for path, expected in source['input_sha256'].items(): + require(hashlib.sha256((root / path).read_bytes()).hexdigest() == expected, + 'Changed pinned source: ' + path) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--certificate', type=Path, default=HERE / 'CERTIFICATE.json') + parser.add_argument('--output', type=Path) + parser.add_argument('--check', type=Path, help='Compare the recomputed receipt exactly') + args = parser.parse_args() + check_sources() + result = verify(json.loads(args.certificate.read_text())) + encoded = json.dumps(result, indent=2) + '\n' + if args.check: + require(args.check.read_text() == encoded, 'Receipt differs from expected') + if args.output: + args.output.write_text(encoded) + print('PASS: %d identities, %d primitive embeddings, %d negative controls' % ( + result['identities'], result['primitive_embeddings_covered'], result['negative_controls_rejected'])) + + +if __name__ == '__main__': + main() diff --git a/research/composite-cyclic-bezout/verify_lifting.py b/research/composite-cyclic-bezout/verify_lifting.py new file mode 100644 index 0000000000..a022ac264f --- /dev/null +++ b/research/composite-cyclic-bezout/verify_lifting.py @@ -0,0 +1,288 @@ +#!/usr/bin/env python3 +"""Check exact seed identities and finite instances of the modular lifting lemma. + +The all-exponent conclusion is a written proof, not a finite enumeration. +Only the standard library and this package's integer verifier are imported. +""" +import argparse +from copy import deepcopy +import hashlib +import importlib.util +import json +from math import gcd, isqrt +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('integer_bezout', HERE / 'verify.py') +base = importlib.util.module_from_spec(spec) +spec.loader.exec_module(base) +require = base.require +SEEDS = (2, 3, 4) +PRIMES = (2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 43) +LIMIT = 512 +MAX_EXPONENT = 5 + + +def is_prime(n): + return type(n) is int and n >= 2 and all(n % d for d in range(2, isqrt(n) + 1)) + + +class Modular: + """(F_p[u]/Phi_s(u))[z]; no field assumption on the coefficient ring.""" + def __init__(self, order, prime): + require(is_prime(prime), 'Modulus is not prime') + require(gcd(order, prime) == 1, 'Prime divides the seed radix') + self.ring = base.Ring(order) + self.p = prime + self.order = order + self.powers = [self.reduce(c) for c in self.ring.powers] + + def reduce(self, value): + return base.trim([c % self.p for c in self.ring.reduce(value)]) + + def add(self, a, b): + return self.reduce(base.add(a, b)) + + def neg(self, a): + return self.reduce([-c for c in a]) + + def mul(self, a, b): + return self.reduce(base.multiply(a, b)) + + def zadd(self, a, b): + return base.ztrim([self.add(a[i] if i < len(a) else (0,), + b[i] if i < len(b) else (0,)) + for i in range(max(len(a), len(b)))]) + + def zmul(self, a, b): + result = [(0,)] * (len(a) + len(b) - 1) + for i, left in enumerate(a): + for j, right in enumerate(b): + result[i + j] = self.add(result[i + j], self.mul(left, right)) + return base.ztrim(result) + + def zdiv(self, a, b): + # The constant leading coefficient of f_s* is s, invertible mod p. + b = base.ztrim(b) + require(len(b[-1]) == 1 and b[-1] != (0,), 'Nonunit scalar leading coefficient') + leading_inverse = pow(b[-1][0], -1, self.p) + remainder = list(a) + quotient = [(0,)] * max(1, len(a) - len(b) + 1) + while len(remainder) >= len(b) and remainder != [(0,)]: + offset = len(remainder) - len(b) + coefficient = self.mul(remainder[-1], (leading_inverse,)) + quotient[offset] = coefficient + for j, value in enumerate(b): + remainder[offset + j] = self.add(remainder[offset + j], + self.neg(self.mul(coefficient, value))) + remainder = base.ztrim(remainder) + return base.ztrim(quotient), base.ztrim(remainder) + + def zpowmod(self, value, exponent, modulus): + require(type(exponent) is int and exponent >= 0, 'Power exponent must be nonnegative') + result = [(1,)] + while exponent: + if exponent & 1: + result = self.zdiv(self.zmul(result, value), modulus)[1] + value = self.zdiv(self.zmul(value, value), modulus)[1] + exponent //= 2 + return result + + +def exact_seed(case): + require(set(case) == {'order', 'denominator', 'a', 'b'}, 'Wrong seed fields') + order = case['order'] + require(type(order) is int and order in SEEDS, 'Unexpected seed radix') + ring = base.Ring(order) + f = base.kernel(ring) + star = [ring.conjugate(c) for c in reversed(f)] + a, b = base.decode(case['a'], ring), base.decode(case['b'], ring) + denominator = base.integer(case['denominator']) + require(denominator > 0, 'Nonpositive seed denominator') + base.check_identity(ring, f, star, a, b, denominator) + return ring, f, star, a, b, denominator + + +def admission(case, prime, exponent): + require(is_prime(prime), 'Modulus is not prime') + require(type(exponent) is int and exponent >= 1, 'Exponent must be positive') + require(gcd(case['order'], prime) == 1, 'Prime divides the seed radix') + require(int(case['denominator']) % prime != 0, 'Seed denominator vanishes modulo prime') + + +def literal_reduction(mod, radix, reciprocal=False): + # Direct tail products for f_r, then invert u and reverse for f_r*. + coefficients = [(1,)] * radix + for j in range(radix - 2, -1, -1): + exponent = -(j + 1) if reciprocal else j + 1 + factor = mod.add((1,), mod.neg(mod.powers[exponent % mod.order])) + coefficients[j] = mod.mul(coefficients[j + 1], factor) + return list(reversed(coefficients)) if reciprocal else coefficients + + +def check_cyclotomic_reduction(order, prime, exponent): + radix = order * prime ** exponent + actual = base.trim([c % prime for c in base.cyclotomic(radix)]) + # Deliberately use repeated multiplication, not the integer cyclotomic recursion. + expected = (1,) + for _ in range(prime ** (exponent - 1) * (prime - 1)): + expected = base.trim([c % prime for c in base.multiply(expected, base.cyclotomic(order))]) + require(actual == expected, 'Cyclotomic reduction identity failed') + + +def check_reductions(f, star, reduced, reduced_star, shift): + require(reduced == [(0,)] * shift + f, 'Tail-product shift identity failed') + require(base.ztrim(reduced_star) == star, 'Reciprocal reduction identity failed') + + +def check_modular_identity(mod, f, star, a, b, denominator): + require(mod.zadd(mod.zmul(a, f), mod.zmul(b, star)) == [(denominator % mod.p,)], + 'Modular Bezout identity failed') + + +def finite_instance(case, prime, exponent): + admission(case, prime, exponent) + order = case['order'] + radix = order * prime ** exponent + mod = Modular(order, prime) + _, f, star, a, b, denominator = exact_seed(case) + f, star, a, b = ([mod.reduce(c) for c in p] for p in (f, star, a, b)) + reduced = literal_reduction(mod, radix) + reduced_star = literal_reduction(mod, radix, reciprocal=True) + check_reductions(f, star, reduced, reduced_star, radix - order) + check_cyclotomic_reduction(order, prime, exponent) + check_modular_identity(mod, f, star, a, b, denominator) + require(star[0] == (1,), 'Reciprocal constant is not one') + + # z*U = 1 - star. Thus U^(r-s) is the inverse of z^(r-s) modulo star. + u = [mod.neg(c) for c in star[1:]] + require(mod.zadd([(1,)], [mod.neg(c) for c in star]) == [(0,)] + u, + 'Inverse-of-z identity failed') + inverse_power = mod.zpowmod(u, radix - order, star) + lifted_a = mod.zdiv(mod.zmul(a, inverse_power), star)[1] + difference = mod.zadd([(denominator % prime,)], + [mod.neg(c) for c in mod.zmul(lifted_a, reduced)]) + lifted_b, remainder = mod.zdiv(difference, star) + require(remainder == [(0,)], 'Lifted Bezout quotient is not exact') + check_modular_identity(mod, reduced, star, lifted_a, lifted_b, denominator) + # Feed altered obligations through the same validators as the valid case. + # In particular, unequal arrays alone are not evidence of rejection. + changed = list(reduced) + changed[-1] = mod.add(changed[-1], (1,)) + controls = [ + base.reject('missing_shift', lambda: check_reductions( + f, star, f, reduced_star, radix - order)), + base.reject('shifted_reciprocal', lambda: check_reductions( + f, star, reduced, [(0,)] * (radix - order) + star, radix - order)), + base.reject('changed_leading_term', lambda: check_modular_identity( + mod, changed, star, lifted_a, lifted_b, denominator)), + ] + payload = {'f': reduced, 'star': base.ztrim(reduced_star), 'a': lifted_a, 'b': lifted_b} + return {'seed': order, 'prime': prime, 'exponent': exponent, 'radix': radix, + 'modular_identity_sha256': hashlib.sha256(json.dumps(payload, separators=(',', ':')).encode()).hexdigest(), + 'mutation_controls': len(controls)} + + +def scalar_evaluate(polynomial, at, prime): + value = 0 + for coefficient in reversed(polynomial): + value = (value * at + coefficient) % prime + return value + + +def finite_field_divide(a, b, prime): + a, b = list(base.trim(a)), base.trim(b) + require(b != (0,), 'Zero finite-field divisor') + inverse = pow(b[-1], -1, prime) + quotient = [0] * max(1, len(a) - len(b) + 1) + while len(a) >= len(b) and a != [0]: + offset = len(a) - len(b) + coefficient = a[-1] * inverse % prime + quotient[offset] = coefficient + for j, value in enumerate(b): + a[offset + j] = (a[offset + j] - coefficient * value) % prime + a = list(base.trim(a)) + return base.trim(quotient), base.trim(a) + + +def bad_prime_witness(case, prime): + # A nonconstant common factor witnesses a root in the algebraic closure; + # that root need not lie in F_p itself. No characteristic-zero claim. + order = case['order'] + _, f, star, _, _, denominator = exact_seed(case) + require(denominator % prime == 0, 'Expected excluded prime') + for root in range(1, prime): + if scalar_evaluate(base.cyclotomic(order), root, prime): + continue + fp = tuple(scalar_evaluate(c, root, prime) for c in f) + gp = tuple(scalar_evaluate(c, root, prime) for c in star) + left, right = fp, gp + while right != (0,): + left, right = right, finite_field_divide(left, right, prime)[1] + inverse = pow(left[-1], -1, prime) + common = tuple(c * inverse % prime for c in left) + if len(common) > 1: + require(finite_field_divide(fp, common, prime)[1] == (0,), 'Invalid common factor of f') + require(finite_field_divide(gp, common, prime)[1] == (0,), 'Invalid common factor of f*') + return {'seed': order, 'prime': prime, 'primitive_root': root, 'common_factor': list(common), + 'scope': 'common factor after reduction only; no complex-unit-circle counterexample'} + raise ValueError('Expected modular common-factor witness not found') + + +def verify(document): + require(document['format'] == 'cyclic-lifting-seeds-v1', 'Wrong seed format') + require(document['coefficient_order'] == 'ascending z, ascending u', 'Wrong coefficient order') + require([case['order'] for case in document['cases']] == list(SEEDS), 'Incomplete seed domain') + require([int(c['denominator']) for c in document['cases']] == [3, 43, 37], 'Changed seed exclusions') + rows = [] + seeds = [] + bad = [] + controls = [] + for case, excluded in zip(document['cases'], (3, 43, 37)): + exact_seed(case) + seeds.append({'seed': case['order'], 'denominator': case['denominator'], + 'excluded_prime_divisors': sorted(set([excluded] + [p for p in PRIMES if case['order'] % p == 0]))}) + for prime in PRIMES: + if case['order'] % prime == 0 or int(case['denominator']) % prime == 0: + continue + for exponent in range(1, MAX_EXPONENT + 1): + if case['order'] * prime ** exponent <= LIMIT: + rows.append(finite_instance(case, prime, exponent)) + controls.append(base.reject('excluded_prime_s%d' % case['order'], + lambda: admission(case, excluded, 1))) + dividing_prime = next(p for p in PRIMES if case['order'] % p == 0) + controls.append(base.reject('noncoprime_seed_s%d' % case['order'], + lambda: admission(case, dividing_prime, 1))) + bad.append(bad_prime_witness(case, excluded)) + mutant = deepcopy(case) + mutant['a'][0][0] = str(int(mutant['a'][0][0]) + 1) + controls.append(base.reject('changed_seed_coefficient_s%d' % case['order'], + lambda: exact_seed(mutant))) + controls.append(base.reject('composite_modulus', lambda: admission(document['cases'][0], 25, 1))) + controls.append(base.reject('zero_exponent', lambda: admission(document['cases'][0], 5, 0))) + return {'status': 'PASS', 'scope': 'exact seed identities and finite checks of a separately proved all-exponent lifting lemma', + 'seeds': seeds, 'domain': {'primes': list(PRIMES), 'max_exponent': MAX_EXPONENT, 'max_radix': LIMIT}, + 'finite_instances': rows, 'instances_checked': len(rows), + 'bad_prime_witnesses': bad, 'rejected_admission_and_seed_controls': controls, + 'mutation_controls_checked': sum(row['mutation_controls'] for row in rows) + len(controls)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--seeds', type=Path, default=HERE / 'LIFTING-SEEDS.json') + parser.add_argument('--output', type=Path) + parser.add_argument('--check', type=Path) + args = parser.parse_args() + base.check_sources() + result = verify(json.loads(args.seeds.read_text())) + text = json.dumps(result, indent=2) + '\n' + if args.check: + require(args.check.read_text() == text, 'Lifting receipt differs') + if args.output: + args.output.write_text(text) + print('PASS: 3 exact seeds, %d modular lifts, 3 excluded-prime witnesses, %d controls' % ( + result['instances_checked'], result['mutation_controls_checked'])) + + +if __name__ == '__main__': + main()