From df10a6d673cd78abdf1d001bb778c9c3a30df5e2 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 12:54:56 +0000 Subject: [PATCH] feat(research): certify the full forward carried-frame optimum --- .../CERTIFICATE.json.gz | Bin 0 -> 22668 bytes .../IMPLEMENTATION.md | 65 ++++++++ .../pair-consistent-frame-optimum/PROOF.md | 128 ++++++++++++++++ .../pair-consistent-frame-optimum/README.md | 137 +++++++++++++++++ .../SOURCES.json | 66 ++++++++ .../pair-consistent-frame-optimum/TASK.json | 129 ++++++++++++++++ .../pair-consistent-frame-optimum/VERIFY.json | 41 +++++ .../pair-consistent-frame-optimum/model.py | 145 ++++++++++++++++++ .../pair-consistent-frame-optimum/powers.py | 59 +++++++ .../pair-consistent-frame-optimum/verify.py | 145 ++++++++++++++++++ 10 files changed, 915 insertions(+) create mode 100644 research/pair-consistent-frame-optimum/CERTIFICATE.json.gz create mode 100644 research/pair-consistent-frame-optimum/IMPLEMENTATION.md create mode 100644 research/pair-consistent-frame-optimum/PROOF.md create mode 100644 research/pair-consistent-frame-optimum/README.md create mode 100644 research/pair-consistent-frame-optimum/SOURCES.json create mode 100644 research/pair-consistent-frame-optimum/TASK.json create mode 100644 research/pair-consistent-frame-optimum/VERIFY.json create mode 100644 research/pair-consistent-frame-optimum/model.py create mode 100644 research/pair-consistent-frame-optimum/powers.py create mode 100644 research/pair-consistent-frame-optimum/verify.py diff --git a/research/pair-consistent-frame-optimum/CERTIFICATE.json.gz b/research/pair-consistent-frame-optimum/CERTIFICATE.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..2591c96ad650c37a9e2175c02c3a10117cb2b15d GIT binary patch literal 22668 zcmZ^|1y~(H(KLe-22DOJAGXJ6gA6f1cb4^vKA1ux3Ho5v`*2yacShJ z^wJE?>RI=`%>z(UhX7|dOJ8=$+h3;c9QuqFhpEr3kY?mcZ+5Du@vg&2zq_L^cqmY{ zr6sN{G$u6_+WU~d8sHcymwH-^@Mf-9J-)U=&{>o{)CkCz8duG{k~jxi??Pv8KzY7* zQc$-D_!GS1naG*f&^n=+h_iLS=g}T0NEALO` zTS0l8aD%PAG{jRHS*tf0P?`d<@?>i@nC95^+lpR{4@x^rS(#v~(E$=^GY zaXc5mY;hmV2rM?iReEFjn5FwnNq10`oVCftyYp-k)ZxlrU3GH&do?&!&PZYr;!d5t z)iScPqQTL{JelD1Jl{dYG9u%Y=>dbI9W9lEJ^r~^|e z=3A7c{f$k2DMS?bR$MzMfh_SuV7T@)^7juehy@xW`7QI`hurw^Y+74p+OS%#CU?4q z#4Zaoj`}pPp_DJn{9uw~4!W#Ku&R^#k9Leqm&o|4!Lm&uS#xV6sv4kpCVpXJ5%hG{ zRJL#eirGR-Tqb3DB%K%Yi4{)=$F!wENfqK5=1ECtTY`G44==-73D-)Z8uvsx%;w^Y zX=b@hkSQYTg62!A-mpy2zANIY3vDLq5wd14+*nASny}*MG8bWDLWFkq?V8A)_;N#v z77te~>TjN6g+I_MAl82@@hW1OT~YD){G^Og&D`RT;>Fp; zVzR}8zW7D{XqZ-*H}| z$DJwX2!G^6bMIb&zy6-mGKC86WcP9b>TuMpK@}AH!*9 z%V|Yfle?1!1~N7aH4ge`(|=ne6)GiDKZ~L!QU`5*r{TG*6+27*vOXhzuRtXetB@kc z|3W%-I$pi=Z3b7dppraaRb=zPpUe zoOX55U&-?pXfx(+4X4gc)Cq6!x05O^{SiQ~^8CU>YnX|j9Tk2?PTg$rd@|AGF}b`m z7WFZCu-bHP>%xtq43EU?NVDjRhE#l8ra)P&W3`Zd^|WD{q3xT#jBK=((ru27HeVO& zy7akBjyUcvpKNpEu(EIX@ZGEljn-@YV7gtQsvKUiM@h+LL^Pr7M|4e}`9c8DaZLOaK)`RDF9gR3(lTJtqN%U8$sz`gJHO*!R} zzkku1oxnYOFg#8T&iZ^VOD>yK{T$4^!1KO^ihC8i&( zd*PyfzImlUJFiNk3f%xPp1@nKb3U!KNLysN0F9-N-;ri-gv&ugc*7ztRI5vCB_|rp zx)Ka%##t}m50g>bJFTQ#QZHz3AVjr(l*nDtF`deT{8eyXcZ`3jm?=a@t&MR~x&RT!`3o@25We2J=k3uqVJZIQv1fn2o+34BbZkl_5t z2iFQX&s`LcNT!N_y`>}gdFe68mUg}Ktw3bu5vdB>2Tl&JiBGrmQm+|P2+$p3d(K^@ z1}R~Oji1>>Ou79J{K^HEHbA7UX~gk>UrTvSqLLGUkKFieG;|14c|zln^dBrr^g7twS`PdLtNS+`>l2$vvjptL(SA69>_8rdMPkL%9M|RvyG_t#@`P}ivQd#P; z!Z+dzCzbC{44rF2mkZ%ex5{g%x*Vah_6I3W*J$C=X7%8`X2bX{!%qCvV^L5d?)+kI zd(E=IR6dvuhL@9{)da36+i>fd5Ew>~1O9F8uwYXphSI{}Da&bTHZ7`t)>LjSUu;UQ%ur2?q$*fg3P9K8=F~K-2{HX%AMJ>qJv|`zL0*(v$FVzbg>oSOzc(`V#oE3iKfqss9j9a~%V>~5gHhC&Q z|LK&3*{O$NX@*8e!$oJcU0*C!15mOm4-0EtKJ~)n{`XdcSVI@?SH+DAtOQ;R6em>m zDQ0HvOq$$D-nq-FLAB4jbk$28Hb=-AZ2iv4f`$PRxhXUEOQP;78>X&iXG*z)ww`Jo z1v1JXk2NyD6y1s`4TgI;BIQ6euZt*J6iM5ah-dgJn<(?9_k{to%u?47#ZH!mPVKy(+IQvpL;iP zGuSgQ&oJzhZnK^X<;@9Ve^cfIF?Z|wVbj9A=Cd$+d;Dj%c|sfXi_d}Ay0d`C-*xwK zBRy72t3-uN&eMft<;kt!+`4y~<7xtn`!C+sVh$t2f%%NcZyf4zS<8SOMG;5&)<+qYLK&v` z1G>Y1Mt$#`lZ*>aV|wZeWpy-kQukZuHN*|?|CCl@%Rei@M-KjCx6}WTNbboX=-h?* zBVou{AMZonhM{LDK7U)ra&#?O^^G@D?6>NmeEm|=01_jS?(K-4v6Q!+Hz zNE8QTmTN{(WP4mwh6jX(C>muq4ou~;x%d)VphS1aG?E__l62Rc(&#toCr1&wKd14w z{*XEdAMcMX0eClfj){_T>R=^X8>Hiv#HX6k*EmPl4qevsjtvy@Z!y9r?XQ9C zBAJSX6Uec08i|*HQ+yEywjwVKEyIqa;v>1Wi`C;MLoQY}b6un)22|Oy6D|&PwnxSz zi}fI6e(Fegc14jb%3K<(U;I?&D3^9(6$2-fr7`+?m00Asy4V1IY;*P0lz0PcP3cXB zmHi^u_YoO}s66#b(d9_9mjcXb25Ah#0I@A2xAO86JU7FQ#l-oweVtH4M%bJo_I08F z2KU}Aq5yAgeIVrm^+lS#n<@@Qm}T8ejmNvS?F8%DxS5JCT9D$)cSFCJ&o1Dxj9JM< zPXa?@viPiXEoLjFcvzw0y>O;uyE>@3uk|rEUdkWnKB{bn;bHPuy?gkZqRu4 zd$lg9gSMv|@=^t6{jik!NZ%qI5*K4J8O_z|X9Zbk5}^c_TJ_?TE0RM2x&;1tX!9^iqa>&ruib`fu7Cg)Uk%@vdMI5lI8tsaWT z=DN1tbb=jBkG^uq)k|lun(9-!+lEc>PS+?u+d(nuo5t<*VN7vm|8-bZhd_1Hip2(8 z|ACwRAuxrqFumV+vl|VldbT-=e6HtSy%^0n*Oz^C#lw37VfLWSdm_2%JGdpe*=4Y~ z1#A_+_rP|4SUEhTm&s%E^JiJ)XYbs51FLB;y`&D z+5dJTP3hWmFKS`>y+$oGQEJ5BsmumgSQvq6VeBfa_N{O9GCH@BEEXj zmgG|5b!&B-YdyuNZYH-Lw%Z>^X7R0$o-65^Zq8EOIC4($s@W)EQ*^pq9xDuf>CKqE zhqldG?ylZuH8$E zLfys*ROrR}Hp5#fqPR>pnJ;idXD8GP0lZJUUdZ^$JTcP-*|=N?sP&YB9Ee928oAb#LP%bKqC+|jq7 z4$R!NU2QG=)-@5Jy()vcj$I{{{P3*Ww}YCkn~W|MJ-s6P&956B=8FjEKyBSGaU%qd zPJ}GpDw+waRq0V)chB}|;PfZLWa`0d4|*G(TP=;Vy@kt;(1?vC2V(1aIt}Luk4F>j ziTDvUPfW|RG|OC39m6G2{YmK^WsVL*%gwxmEkpXs#t1k7Xj8F#hpF%vW0rJUHYP$D zkh{~hGt_bG`$DA$1L&S;yiae@bV(DpVsMK=Bh~v4O31w%Rqhq%0vAs6p~ZfAI zx9#hwxfT2jy5_%bnZ{MAEecDv*^GADtw{=~zJy8OcXeK#O=(s;!v;z9y{A!jTWPs- zH+6**z_iAj<$WHF{k6h6E2je+pnFO3`RIZ{Kg&P)SA}9j?&sFBOXJW6=EyVpR)rZE zP_pr7t^UT%%Qo7VwSF7Tj7nxhbx9lihP}QSJA@n)l)y=@$8fn%0&YNK%Wl&AWL#`S zd!wuEIKof9y&DMT=G`^WErt~RF2UCg^sk>HMfj|)iQWRH+4!If7bcL*1vFHW#q!(GlNHYz6= ziWc+Oe2HO=)~|l;N35C#jMcRPT%Zb92Yss`(`){CtpTFJh-Ym@9H2Ifmj`aoUnU7os!{xXy(3$Dx zyvs~uFR}|;as27k<9_=DgDK$bxqXbzW%5{tZj-5D<4MgT^g2wY0Tmdtqo9?6$F-*b<<_ z=>?1wdr*9GcQo#TzTUo1{C$fqmvh|vin2HD41aQ@*FD}gGw}@;RO8weVxJ=Gj_>F1 z&nwvUHyio%ijVlssg-RYS_@8~{hLj1<*lV9kGtc9KNn{1_{_Y#WY=DAN7T#EbIAnw zA&xLFx-vGY%-H74)z6 zlv!^tcA~YXVkio0KBq^iBM4lGPE(i(Qa%D^w$A*&(;SrP($d6xpUt>g5$6q7ZYI4pl1OsV#@ zh-(xWO9iE=z1vR63C36ZqK>_{JfGR!2mNq0k<|i6cVN!EJGvxTC6-E!bivOcLaUwB zdU(4AO)Gd?oN&cZ+n+T%teMs8V-LFV9vS>ip2B9W6xF1=a_P!8%}m+(o4n*%`D&@P zF54t*=u51|I^i>(^brL;ztWPRNLpuT*z_c zVc;~4wQ-Mj;7Y!gYS@|+b*fFG$n2GEWQh#E*`ER1+wtTG@9?*%=b9N_?fdSWg757J z7Ma|?I4kro-G8|tsg_XpXq)LcO&y!Cy*h;77o%QN1uv)2A!^entOLgm&U|=pGh${W znFL)7-4nCR)oPgLVtx!N`-m~U^lllhZEm0o)zKC23&?Y?=-=YyRhKqB+6~8hEx#hR zxp_<6YIn+#v!67suMo3PmHQX{n$9*ce@#?ml+|NAuxsG++@@@;NG2*eT3#{hZ{+ZN zb!+MjDyDRjvR~TY^70CiF_qG9KDw%aQe=EgjvEu(;gc@Z*g7w(N`61}AO#fXg4LFpy5Mr`jU0NnQ7@y{HlL1jEVxcyrq3zE6@9p?4W1%_7Jc?pLpdC2 zE9i*NImvH0Mw~P(Auhy$6UvUaJW~+dNLhTaiz8oJD_5FY#1~Kplw+KqPyGMJjPc0P z-C~Z-O%U1}HA`z`#@f5QlEmEM#oUycJ(MN;Ix<{quL;JIUC%*XDaE&xTsKO!V2{l? z`R=O;`fu4+s}EZw3OPg!f34&gIKX@kojl!2%BZEh z(ga+MRCks}>0Ku#KL#WTcuY!4GMBXhE@K?~K1>9PCP)3OjqV}p>)qHdv}|p8*IstP z1bLZ{fUBGWw^kl%_mH0#XASYrzP}>7yXH)^gI)*{+dv+f(XVrn-ixkLmQ@Azm%SjK zCM%UX<>cy7Is8yi@>u3GdP8%^iARa>wqhsdV_@l)?~*V6>rU56hwr2RXynVMy3wh3 z$=jt&*KbZ-|}q0rz%%QQI6#p><-1q{13R$%K22P=IR|l>-xJ*l?RuPINmViMG60y@^x$&+0bAYRliLCFoxfxb05kE{VD^`NjD(iHI zRw@h|O2K{Jx3kgB6Qnxx@R?hi)ox!C%^{Ul+9hKg_lZKo$7Tz_FJUANi1ZY#Ok0IY~MhE!_5^|ukMv{2QPp-Mm6f4kyl zbL7IX5uI-Z*8ok3w1d(6NWy9 zqnS8_a84eze=KwAQ**<;cN(}I&E95RgM)pNPZJo0KiV%~vycu_I-6_jHy*Mv-^B7B zy5fm((}`+V1ymFi2r-MnYTGBo8unR>QTVz)y z-5&%;uO}!Aj1=20WErAsC{k+IVXMy7pD*AWb3^V161V=l--_&G*S%*igt>8zJEew~ zI25Skiz~uTn*c>09>Ir~7Sj7(KQ^nK1qVNs=IN$Whu-I%Cyb>&E4V6u3XAPO1G+Ku zk|G}w=(jNYAaSjWtPUufQxmNB0*yI8^v^VLLFp#}U2#uF6bITLZZQjf^ta(^>nqVX zc@;7ZgEczd3ykSD37b@P(~&mnp~-U^>UHiJZb-1~avc`6LCsbgU3QieYu(o=EyftJ znP*C<8_OF$+Rcq!FD=FDh94I|pWOEt=NTmTsW<)(##AUw56J##O(HQXmU3o?lp9Ag|ZS&yK0jfhR3l`E_VH9sDwZ zU%N*|_ol3)tt0n|C)o6<47a}M+>(-|k7MIkgCG%aaG8&!(e5f$x9HoU_h5iP;HTjY z;to0O=REU*D4>6vnS(LsTIc#HE5Of6His`4r?OVKQo_#j3~~XO`#5zD7@O{UZG71# zgEYT|1rk!Rl~N#ic17u!g_-R9`xwfJ5wJq2AkY}`V<)y-x$qpDAQ%4mV5+S;*08Z4 zi&yE1!`u~Mk9^A3t+|YFXo#ru5rW?2NAZ%Yw}eNxuUUL#(M!ga9#JE|J0aM{ABt-1 zzX6ry`wKPtyA&b01-6sS;zG|pRqHvUzv9p(37;jzaxw%3caL#Xt% zMg?e3J!bpnHHNR`SF4xHxMFYOt@{3vL0JN&%DyW00u3j+Cj&kTh3f+GKsIryh9JTP z6QYqPLT`C-V7Nk0IDbc$Np(i@s)f&l8QH_1xQ#?H_Z9b^? zDGZGbE}b;F2arpPtIhca*MRROE?Y;+c_XXs%*qVRdUsByQ~7-Twkwzph(OdZP0^Op)REqK#1po>tIuus0Na^FGlt znGdDgumpcbQ|}zTrMvrzQDVGDpT^4IZvC4FK#^jSZ8qdxQ`4@Y zyOaUc%N0S`3}P;}08{5ZV#m@H@t?a`g5sGvzqpT^;#wiER>JxF-!W%~OPT$0a@=q0 zm0x$@BU>qYPlE2qac^TOqUmLumJ{s_GD^-{u`0X`JVf2fGdjg@8Durx?hxF7;EHKhE-@|Mhrnl&C(K^)59>Rssn@Kl1oCFd)q~7NfuIA&WcA;bEfL%S8 zPIJ}QC2}9*5$~uz#>@-SRO*%U)|Lb=Hha@lR&l)q-S?xdIXzWZi=^A8VFwo4T~iI# z`o_Y~1rBnKlye%TaC$nF7e)uEj7(?N3&E-gZDXI18_#{lyuh@=Tc@+m-00hS5`oR5 zgHG?IikN3;D@Kt9AJ=y*zoGh-Jn*Xx{LAu9NZyHAk*!HiG)!b-;4L8Fp&;?&@ul5pa87l9Ge3jQFJ;jQfqhu%vw(uIMYbd^yJY-&Hil zA?nN$n}wsglpaZoYdS?N6uAv4~B;)!o930+2Ht7eyexMnJ#Iu*!i!#Wx+(+H

+4#xCy6Z9n6BL_V68?CA>vLE>t zbao${i4v1KZF!?zxmgL`$Mkc@9Vc}n){~ZVqRIJ*)d}1uW>T{#UQ#mdMxvhp1|CDx zMTY)~)4J;^J3}HLZSelX?S6i}7otA@R#HqGDhe^>4f!vB2Zn?8OQ1!j#SYBnwQ+f8 zD4!q2x`PMo$A)ylwQF;4ZHD!Ye)moO@*~dj332(ITj?&6v$g)}4fW$d*von9FVmn; zz>Jy~n?RjjmkNXiQ)}f#do3_F47D1WqqS!%^bu+diewL&;_tYM#>o^27m{H$!E9kNV;~x!gS5Q6@kr*kEF?Zz(8R zUwV*ZR>N74(`w9DH+vJl)l!Q1d@faf@0%q)MTEo9oea2I{!#|GCB&>7o^PDuJWEd2cjM(*c&!gA-k2ZrwrXv!3MOy*b58e4>q-u(HT$xnI#626v zCM9g=9&=F_1dKf8F^FhH>0$Hk)@zB9=c`m#K$jE#EASH$6Q5wwTPO+tr`CLHwpBT- zgtfne#J|Yg6hOM6DBW!Y!qRTs*UxJbbS9?8j-h@h+(hhkvv8WZeu&$8PFJ5vb!Z_5 zg_Ov%Rgbg?fGzV9-P=#=*#{0K4jZm<*RqMKiQcxlUAXW2Km4(9>;=j3tyjr+{eSTD zS=;9Fm(GNNgAN+EFM0m#v4s-9yjfif90w=Ny!m}Tzt66Q4f{bx`|=}=CgQdpHq;v}+Nq1frZ4R-p}A^WKZBIwany0US4q9j*7 zr8ne6Lj@Hd%CNv0>%YeBTJT(CB&V=GZ=D=2(Sg0I_81^NPiU;AgESAoj=wx%O&g}+ zWP5y5eV?fnOmlw8g_{ojB;G6%E zCXI;Du^00IIJW<6!~e~=N`z>6;_fH!*iKAGyRt#S80n&XyU z|7wE2MI35!(6^k{eXE-d_y{MxpsY0*_0H8jP)6w45Pf}GU-9!*U*MQIuU>cW-J@Os z>EX}RZhieIl=#ci)g(3%n)RG-`bdfKng8KV_6M7>-_W$$@ARPS>;OWl`L2VLn}g$q z(4{}t(vz7;AFwT7ZrJSAQuYF5Cd4o0|1He_EAyeZ!(!y#w|sMQ7%X*Hh>paC&ONPr z#n_a|%ba+!EPtO>e*x4mi(~zl3Dwql)(u-|aNccPp%AvL zQCRr5#M~hKEH6Y&h;fKo7hJ$?V;=_t=Me&Sx-XfG8yAb^<~!e!T?Hvs;j`33_raE8 z@}vG;`{t_dI_xA^qhDsk4`}-GZI!9DtK}F30p0$I5mc5a__v^8X$8w3AyRYm!N6dS zV)MN$9J=>>Pazf7Kp(KFcuFx;FQSSCehX{d?HHY#N&o z#H;Hyxg>KKw^TDqTAAAeI>)_j<<;2z^Of4c<7nEw4eeybU$`Oi?Y7Th`~8u;-eZbu zTNk+9jq!JKAeMR@P7TR7BSrRHGuvu2T?d*pRyH$8#wVLabXCnvOzjvCzFZtJE|E_x zc88(Z3;H-T?sEP&Li!T<2}**zzFCYKK-SFfxL{2_O)}0ip3}c{dsEu1kB{rVuimGI zH*XHz&hn4C3T+_xrrwX?GtM{{fhdj+cm_v-h%E_`;eBYtLA& zFz!rlZKlcru~*ybmtLjIR-Jj4II8&9jdbGI`t8qQD%RVtD}0?;ksUL{A8u zbjOFFTAZifJ)wx*M@pBUgAfw0wqw3xP@W+-+qFk;a(lj}Spw6Mxgc?GQL59-02i@a zLU<0Mr}6yoEBlfUZi_c4jvQ>MBkU*c&~%!~ij;&sBJ!ulh0%KI=fsc&@N@q@S#=xP zlyicOi}?BCw=8w9U-IWo+_taAhCV&100cR@mQ{#R>oI-Q!$k(BTPO&FfKDL8!5Mif z`f{3E<~Lgj8r&%ugY>%##$<3{?h=lJuSHzesBt43|BPZfm?fv)W~0Upd5?AIUDRXv zN3_akL*>z=q6U)jSCP$d)eC(?N_}M}9YdyFHe`fx8u4XGj$A`+6%yFzx}DOv5fYds z_nRF=`VBn!TP0MAwUg-)l3aD9vJPjSA0wm!Y)s96p`$fxaOekb8bX~}8eDefapcsGU{o;OURHm^X!SXzv z7mU_$q?(0P*#OY7Y32+m8_b>d_M!EcTpgywa#h&zY+N90bl?7dpRooaGC*(Q=j+r{ zYT@mqMQ$FnHC3&4YMx4kkf){nvu{Lq>GETw;k?f1N3+Su!rS6~pXUk^i zdN0G&7EZf?(+Z7RxfU%o*^lAQeT9`rjIlJHlQ6lYYHPcH`Hf|eL@~sGQA5U55kSL6 zAyayALL<21490NPzrXl2fdcJ7~&Ffi*q=r+f5ie?n==0kLag!C}C2d#< z$vLBbCD|?c4pb;iHhX;RZjI{^8VnQ0=@=c#HX|95KlIe7^sqDS04?_TC ztb2!qPlHbQ%#Q!FmSXCDvQQxMc)LnbS$^W#rs|nh!c=k9ukn5WGkKWwHZ>S`&St(Wo(Le8zD8^+L{{239YtB5}ObCrTx-(OM%VmiB&Dmxr(!c3GLHw zTfZ=NQcb5q7_C{EqNNEd`NxM7#I?(9L3p))ui7oG&nsU4+FTBB?Pk{EKmyjgb|}hE z!;kEY*EbiLPq`Nv9O5sUE8S3qPqcX%tXRHdbQx;&w&4?q8gLlLi=5B*npUbjB?69S z&HRXV;zZMBc~Bt#d@vP@hJ1XAHEYJtc<>}WWCDr>swsTE_+fX6iT|2$iM zckYDol65>$@i9?X)btxuJU3@Bh;jULrax0u^l3C^zUS^**|OQ`cy%zpU(kl@oZVil z!;7OwF;JP2{meVwUe*FONt^Zx>lQf2Q};(dnoRiI-!TCbyK#^u=H)q6@Mjm*6ylfI})Botc%i@4G4$>!PZ)SsN z8d=<)MQp&}KrM$^o6Gdo=?m4nOo*7*v;s*yuSI)S`#uWs!fJ*85lGH{;+BgxzF1IL z?+!gKA>Wz~2X?j2iQT^qJ0*v_h)3%sP+<60WaH6J%r1MyEx1Cu{r(JPvZdWQTu)th zVeQbw#eFE|WEiRM*7k|G^2EUSdeL6;z%61LEEyhReFrv z)T8S5A4cR1OINM5@EZRhlbZU05qM}et_7K9PFYPhAQyuUN{+LYuTg-rL5Z!SvDU5k zYLYfqja{bCT&3yA&9+Sml0x2NiWR$&StnB|4>; zJacGUC&K?M-ZKU_j)|3leZjjTK~q*_{@lf?Lwlqkxky1+>hM6Qh(p?!WT0W!Rb4+i zQ6fQ}Hi1{@dnntYgAtJZ^rF5x!?YPv=XUdyjBi6~MM6K11~(YD% zwyy+BKPucnV`jbAiv;7c+2hBLN=ygMsFgU>l4+JyHVNEgMyepxwO$%~EG@>>^bVUBpLXG2522rW=ubd3Z+dzm zNrrs__jWa2hAIL{W!)w5^eO|iQj?`^H9UpMtoD)qRG)2aR z_NT2tn>YvY3xlGGz}MPYmTqSPl^>hia3c?49ebygmD$=A{3n*1{II;{s}$}jg!sWs zyD25HC>v1UqIV1+R|z77zk~Hz?kUX$zM2FVJUBbFV_~u>Pg^xaVMeTv_4F(|wLh`B z+%MKgN*WihB#jL_W1+3ZbG)o4RI(qzOVJur%z<>}X=^bpDXfcZo61wV%g<(k)a1CH z{lmGI0!*zOVvm8VFy4X%ln%+AsNefnKD);Q# zODvzY05K6s)e`#BNL|K>dJeKT@zNeO*uS0RUeDWE1|~FT9QeF20IeyI<2H5|Qg4<) za=O|5q0vOecKx-=Nstzb^|jZ-*^P|TPWTvHiEB^k%rURx$Jkk3SxSRMg0PZ!7dOzz zm2!0{UQTey@r<(aJJru76oie{a}syvwQX0IVZObFN@A7XOgI$DMW(ElvJ%nNq+MA{ ziuS-1Nmqm@^X@oc8^2n204whw1$AH=UZ>&%QoMP02hc-Mt^PN!$X$n-QERS|jnpzm zk*gkk$4F5cMRn@^JPQT?nft4|*8O_h>qszCRjiWSmA^cvHmgc%n*%jU63O1nY4vO`f@6jaYHb$B%QeRNeIWVyW< z3hM3Fs-2u+CT~Z#3rX_{3Zvg{+Pfyv7?HfBYOay&c$wnBhf7YO;kln92+=nc%K9)b zifZ$lN5hZ)1!-~!X1|S^S%Hspmzb8Cv^fu*e)tBK)`K&G>axR(9bpsI7pEoYO8lg3 zo?n@^ys^u+M9CkHJ7V8xRpjfugn{Iqj0WDyfSi%CE;#tV zz7qRCKMKAd?0i&hJ#7fSKZN}?|1f#5=WKjAh<$c{?Erkf)LLhKu$~KkRQculr#j_a zUcVSxJikBQOkVpxN4_2~Eqt;DSw`8>P+{F~|@Y(eUo~Tn7r;{tD8+VIsig7K43_FOPNDlay&|8}SG7ObkTL+{=x>(iYToAz}~k zMmN9-$>e9KL#)Y@9a2y9UhC}1>41YV*$DG@leF=y~GogIg8gz`AV4uu4qlx~*0s zVUi>Vf=rrw%16WcBkzZhtOqm$#=bEbBH1UT zcY2fz5)q5X%I>!yNqQoPltX<}gF^#T!$U*XgtNW)Z(C5f5UhumrdEemtb6faW93eX zW)btKQlT<2qP1rce#&9lP74u1NN|66l3};z%;Uh^;mz7OYe&OI!%oHz6Ij*h+s%G4 zWsjQ^l7PZR{(k}Uq*5LPMlp*r9tI2wtx-NC5gr2j7cS&Yc1i>}4ou5lF)O*GVKFO5 zC;o#(HluV1M2b*|CEQ)aV|;`xELb1p8;(0TNJFT90LBCb#wUhEGRTunxi=32Y>tE{ zlnuN1b(s)>JwPm4T=Tm=kI%p!{(t5yO*RM!?T!l54tWflhHqpa0EGAlL?NNaLSg^I z^(|(6)rSB;O(HXM^=^IvAWkwchpoa7g+oFnbWonU1&57^#OX+>{72r}y9o)1Om9iE zicAk3{2C$|2s_zSJP33AJxzBKIFzMJVi(v1Gasjv-#b8J^s@j0ea(yAgZ+ykq7TDO z2t5XT4W zpaQA_rHnW4{C@%25J>$%RGxEOHTE(qrKK;PKjT`Vx>24)rb8k1Aq?Ss2ya}8c5W1f|L&BGdxXCw3gkKT z`q%p;>Aq-SO~4&|kt7K}-npCy4j2(jC=UwyI7kuFunZz!2(H(C(3wbhk=&I5?H<11 zKPVgzAy9}MtqdA6TPP0`z6ml=hh!EJIwDYr4Xq3oa!V+WK&TXX9iJNiB~VBh%@Q6G zOE`}lJ_-6?!Zncn4mz*^4Z+e+XdTLs8WGZt6w?DL&D-b-xmk?;3jlSJpZQU1f#^Sy zKp>o_=m;7$E+m6!o;my-(qA=hmMtX?==M;dH8j-m(2Q>gcaT2(lxrpl|BHC`Q;6=s zhluYf=Rq9u2X<1$ajBuC*ZJkU1VidDQsaAt3H?R0B!XNL&GUv&LJfQ%RT6}L2@`_& zW=SF(nn#z%3$gUIOhE|COZq>)q53c0I#S5t8#N>3rI@)8Dj@}?TBk8%z=;s*H)=9S zd9l0*c$aU1tYotiB7t0Az)1Fp(PDWC@Gj_qDrB=V(AIy1n7&a{LQaY0Wx%^&1Ui$= zDu@Ka_VPg;<1)_#;PT4;>#RRZIE{_c8rFC^tuUPu3O+GnimwqO6xA+_SvlX4+EOKt z6wREPKH?h;o+Ygnd#{E{T?%H_iBbSNW}Z?WT@b7m(Rf~80R$}kUA|IYU!Q#-O98=l zfOG)?{tavu21kMMApU>iiO0XvYottsOoWValXesRRbM^;!3{}`6j@zL6l-27g#G`5 z)R>lEj+s~4>06An^C8@lzW^*H@G{~<&5QDJLm-iR2{^M+ej~!*1ps>=eiszwQ(IBX z;6zPddH?bK-fPekzh!r=zwu3T1761 ze?9=)_Tpn~2Q2i;pIVD({?GdiknNwcgwL9Y5-tku&vT^S^-=og(phq(J9sGmexX?A z|AHaRzpKAY`h5sA=KV@8bIF#M{w;N_GV;M6H88VT`Qv#^qMr)aGz+|cqnSC@o%Xr{PZw^8N%4PZp!|$NBvV62CA>Dg zo%0zYxBA7N4Ukla3m<2*;V)^{-&y}S{*Jitw-(8C1`Cgb*S6J~>Woxpa=8~YTt(_P z1k2`fuR(>h@LWEZYkyssCuLKDUlH(oK=@-u>Irgr0Q4QC!al8HNLG#&`wk-Yc>iyP ztO$T^SbL{69lDETC;CN(<@q)H@8D>%P?=TOG(`&IGl{6I{F_x#QFkb{T=$Z6Nn#1vJ?NWY4zH_37AKe zWCfDfO2gu%#Z?3JH9Nj`2GQEgwnsMxW=wDqojb+v0o$9|B| z^Cn5AcaSO@z-jb`6zVkahYf2?sMKyqRo-HJK8~<6y7Q4RW0I71BwycJve{y-qzO&iLFgHP z32-(9(SpJU0mm%uoo||Hb)f7|`1KkAABB+D{fVuR(SApNKNmw_L6Vjaie1PFZ%^sad8nuZapXB> z5CLEyLP_?kX@#h+^agqIl5{Tz&Zhek8!UaBR}*bhC>8Hv~@os z6_UtJkIJtdxI} zx++(3QCkTog1zmYbz3|9<3CKY)-?aVtUr$Z@b6=v-mR_g*cvy_&6MuySX8LJ+| z%kuu0(x}}I2{GEAR(Gp&&C<=))a|dyKVPzpdz^A;w_)hLZ3DOT*TqFcb{ zpz^#$?JmvgJ_o106F=mO<`oN~Gxk|YXuwg4(gw@gAkCFnY4%%E`rZr+=_hYGs?XG3 zJ-~XTJGtrb5%eeYtZrpDAniE4ERha^cJv(BINmv`FqHZ!Z#6$}=4Pr4+CK!BYNawU z3y`y0l~Bn!j37vkD?!s7du6>2NYqhw0%v!3SC!A^Mgww7XYZgBbPvq~?nd%vatJ4# zQ8nPlT^Wi48S5Cw;S2e19lD$V*%*{WWeRBq3W})6YFENXC{)_s30Elio?m+ex+d$h z!VooC_=+1(M5PgCfijFPG-qRL0eK& z?c>`!IqSq+t-8G`@tw1B5-Zy6wkTgAF%xUFC~rEU>lrr_t-je-)-ye)uh`FP{U_&|>Rh{%-vcZjmcgOB8=>0(hNF%(inY*IJt1NnZU z)ni*?I#d69?Li!PN+jWIZ>+-iMxhS)nnAh8IgqNLuS3#<2;vkS9X z>$Pkf$2P5{0;bwH4tbV-4wq^P5+8^cR~7+(L|n6VYG7u3Bi+_&;dMgRq8}u#5*0q( zW=by164%k^1w4}Za2fQr)RyA7)_7hSw5nS|8?Zv2kB<&f_|mN_vO<0pkB(5d-i<5$ zy;@;4OoMsw#(FKqX6F;8==|*A^_eNHrw0|>d7U2WLQ=!n9k_$e%$zukmjAzIg*UJQkjPgw#1n{Z5GMLW384ZA1I>oVF3;e?#r%adcKvzzrV`I~;Eve_jSg}~-sn9G5v)3?pYUmk>m7nZKigmjQ_#TUeYd;TLvLwOy1WG7t2|Lcsd5ESO@rl5HA=aB!tODpN0(1o_c6edb z#0GSVYz(!laP9F2rkwbtGbVsEeH6H8CD#w!UuRk6WPe>=uU?xnB|iDXrIn=MEx0m- zZFP8-bUu#_MeNZM$OnI^1tfEf1j#E(+}j)GMmAEa|f;+#GQ3Og^nl zyNK?lyt}yvxBTk;CNLH^13l0eWOV{>LEu{uI0VcKd(1O?%#b~7sTtj8kLj?-blSrP zQ4`W`+q4ETNqJfU%p|=PF@A^TRnGD#2OYR{OQJv8hkc-&g)0a36!wYrEBbe`Lr$ca z(#Lo^_i!U*ZZ5v_d$^mQ!g0U^FpFY%FWI-k{lm|X}Ax+)zu}?IhdW@x1UD?pIhwS0R9Mb15-Eq zPYPhYzM#JhdoFe5x5mJeyFaLQe!a$asbo7jB|@HobVg(GUEpUwvk14n)?Ams5lAJ6 z2hM$QM#*F?@Wf8H^Nd?g!}s;7rg#k+h{c`~4ToSC3O6?;(~aK%pVJn{Y8Nu_iES~ zReh&n$@{HMbF>R~{#MAg4Ld@Fh{Qd>zWX|&%*Va9u zIT2jAcc)9)o~4wo=O!Cbgf-VZ=w@x{#sJVAUM33J!&d z=7ox8w|s}-0SE6R*CVU6!VlgLok|UzOD(m2U3tXg{fqw<&jQ6g9>2iv1{B|=^!b>d z5UaE!%?uo{t_zOQs2?dJhiZ6_%y{GanphdmTW0-TDppSiRLtH>rGJfZDf>sfrXkL$ z^F#@2hnGsc!qAnTxGl5iFySAda92ABVQ3}nN_(!{X(?U&-L!9c1)n&qte!Zz=@4hl zby-|1mvA3l8T?QC+z?dw1lJdLz|Iv_?Mp9c!zUFG0S`#;n-I3lQSADKN6C1#owgdI z^@xAP2nI*^a=1#`bjN7EhQ@nDdSXU}7KNn{QO$(LP;n=Yv1B583v-c>%Ggf03+_0N zpn-Yr3^JG&whR39*BOYPS6CYWL#Z3oKEeJf8})-e{J0#M3z%0IZ6;Cdyh{Df&ljw7 z)6qSF-7G$|9!6EVj!=a;YI#F*-xl(N%;3LREzo*3>ee;HLi)VtPaZmK1RXSjCXb-0 zBgBJXtg4*1s@%Hr61+T^tJhPum059~yHmU}cr8xt*HR(;xO=aW0W%_lzf-YFseGZZ zGTD9WrUj)s7o8@e*XFntM=yDuQDMR5iIPV}`Y-CmI$FQR?+tz`qU5x>6A{KmU?m-0 zIYI{&QF5M$+qdpN`8#o;(!xyed_~E{!y8PEX2$if;MHTPxUu5lg@?YO-8xCmGrlZptc6!~&^AdX$-{-_;* zc6&O2I@~WQ#3|AGw#lCbT|H)$r+YvDmD!3h@_inK{kdsFh#ukhy;`;0+{xNF5q#=)%n5Rl{uC?`&UTaZR2gXbvK2Js!P8(Ub>Ah`APnc@3H`;8`D{Fc_bT@N( z67Gqt33z>}STJd-@K?cEY;bN#R8?ZE86`3SkKC2qh)FK7xUOf}hzXlin%46usZaMY zsmwWAEI7OHspKl_hsV96)W?>}Ek=)OPQzn+=%-`626)G%s&ReyoArK{MCA&uP+e-C zjYiftyoP2w_e~+c;nmAubkAV>S*?To({olap%)ia+y>{v=cff%gTl@Uz_9#`rUh_*0GiQ=tw1(0js#%V6w+lzz$h z=tI6l(Y?yK+~7ryU_I~48PHpdaqdfU=aqVOqwwTD75s_eD{PYN)IGLWPE6=+WUTo^ zYTvYZa#*N=g+)bhS@F5G4;fzR1u{3Vg|1Q(K1wikEpqL^7+Qr& zNH?l@6E=-wactlnRb?C-aOZ)6TMvqqtLe3;O62J38O<-r<^|{T+xz2o3HKAmEp0|3jPYwX{<=*~k0RYm zy4(ynNj_n6oT#aMR@fc7-kmeW8go~8X?V1tr^LTJ437!cMhm^2P?f@Sv%_JGGNxQANq|F3vZTWL68PI2`u zJ{9s`K_re|T2wz-Y1m^vmytdHKAP8c@m@*Zt;uw~WCSFSXhoULVCen>n)d|aMK3H* z^SEH(0TkSqDYRqfSl@ErfrNF?;}~HQ*zZg*n5(bua^%j#xs^2+Pnj3oa~^%+@>pGH z3=0lE^uuKXvE$;!!Sj@?t%B0QFc*aGEX=wzV~OHNMBc;3UY%d+^R(%aT?6XMXPauk7!89(TU$i(%W&kHt#c zcM^ge$>`j?$Ix7OAC=b`T)YnDaQhsNNTH3C)Nei-n=|$%*{$qff3ayN`S= zp^w&|rWkfV%l|Rb26oFyLF~XT_?5kv0>?~Xa0eN~%d-JrNvpkX+u6LXJkrQ!BXDp}s`n|NYv z-p@j6z{=ZUe&PPU>5dN6HFu5$(5**F_Uo$z*W`Rbv ziUA$SL)=mF&~O@)O3mj@m(Gg^i0e&p4*@)`IF4~r0A0Slg+>PB1-r%~ha1$*?n)IU v#jX8{+4{Jn?bn;2?Qd`Q{VZz}yxh0F_5Ihz$FhZAKa(ZPX;!9xh>QFW#Sl7n literal 0 HcmV?d00001 diff --git a/research/pair-consistent-frame-optimum/IMPLEMENTATION.md b/research/pair-consistent-frame-optimum/IMPLEMENTATION.md new file mode 100644 index 0000000000..627b53287d --- /dev/null +++ b/research/pair-consistent-frame-optimum/IMPLEMENTATION.md @@ -0,0 +1,65 @@ +# Verification boundaries + +`model.py` authenticates eight fixed inputs, reuses the predecessor's frame +construction definitions, and builds the new pair-consistent equality model. +`powers.py` provides directed integer bounds. `verify.py` checks the supplied +primal and symbolic dual, the actual integral frame assignment, and rejection +controls. No scientific predecessor replay or solver executes. + +The certificate is a generated proof witness, not a handwritten receipt. +Its mathematical model hash is regenerated from the complete rows, right-hand +sides, costs, fixed constant, source profile, domains, node variable inventory +and mapped-edge count. Gzip container bytes are not a mathematical invariant; +the decoded certificate and freshly checked equations define acceptance. + +## Power of Ten inspection + +New functions stay within 60 physical lines. All loops range over explicit +finite collections or fixed Taylor truncations. Guards enforce at most 100,000 +source events, 5,000 source frames, dimension nine, 16,000 graph nodes, 30,000 +mapped edges, quotient gap five, 5,000 marginal choices, 25,000 columns and +16,000 equality rows. This is a fixed authenticated input, not a general input +service. Checks raise explicit exceptions and remain enabled under `-O`. +All new data is local to one run. Input files and certificate bytes are read +only; file operations use `Path` methods with normal error propagation. + +Rule 3, managed allocation deviation. CPython, arbitrary-precision arithmetic, +standard containers and the retained frame caches allocate during verification. +These cannot meet a fixed-memory native execution rule. The scope is one bounded +read-only certificate replay, with the enforced inventories above and a 120-second +registered timeout. The largest LP table has 59,077 nonzero coefficients; dual +vectors have five integer entries. No fixed-memory physical caller is claimed. +A native port would need fixed-capacity arithmetic and storage before such use. + +Rule 8, authenticated source-loading deviation. Preserving the pinned source +requires compiling its frame definitions and the single unchanged `construct` +function selected by AST name. The whole native verifier must not run, since +that would spend the assignment on predecessor verification. Eight hashes are +checked before loading. No source text is modified, and no arbitrary module or +callback path is accepted. The retained constructor's globals are explicitly +bound to its original canonical data, Fraction, copy and an exception guard. +The verifier exercises the actual graph produced by those definitions. A future +upstream definition-only module would remove the need for AST extraction. + +Rule 9, managed dispatch deviation. Standard-library operations and the +predecessor's `NativeSchedule` methods dispatch through a fixed, authenticated +module. The eight test-only rejection callables have explicit local targets. +No callback registry, network or subprocess exists in the scientific checker. +Changing the loader to a native static interface would be needed for a literal +no-indirect-call execution model. + +Rule 10. Registered normal and optimized replays enable warnings as errors. +The available interpreter supplies syntax and runtime diagnostics. No separate +static analyzer is installed in the declared standard-library environment. +Frozen predecessor code is preserved; no repository-wide analyzer configuration +or historical suite is changed. + +## Meaningful controls + +Eight controls reject a missing integral pair variable, an invalid index, +a duplicated selected variable, a changed dual coefficient, an omitted dual +row, an omitted model row, a false optimum histogram and an invalid power rank. +They exercise the same acceptance functions as the certificate. The proof's +Taylor remainders and reduced-cost signs are executable acceptance obligations. +The direct stdout receipt records source hashes, exact counts, interpreter, +all rejection reasons and the minimum certified positive sign bound. diff --git a/research/pair-consistent-frame-optimum/PROOF.md b/research/pair-consistent-frame-optimum/PROOF.md new file mode 100644 index 0000000000..547108fc9f --- /dev/null +++ b/research/pair-consistent-frame-optimum/PROOF.md @@ -0,0 +1,128 @@ +# The pair-consistent certificate + +Put `p=4984891121/5000000000` and `f(r)=r^p`, with `f(0)=0`. +All objects below refer to the authenticated forward graph from #4994. +The predecessor's graph/realization and complete marginal-interval theorems +are cited premises. No native endpoint or physical phase theorem is reproved. + +## 1. A relaxation containing every legal frame assignment + +A vertex v carries a binary subspace U_v. Each mapped edge e:u->v imposes +`G_e U_u contained in U_v`. Its paid rank is `dim U_v-dim U_u` because G_e +is invertible. Repeated identical edges retain their multiplicity. Fixed +vertices and eight rank-eight center jobs retain the source charges. + +The predecessor interval theorem gives the least and greatest feasible +subspaces L_v,H_v and proves that every subspace between them is an attainable +single-vertex marginal. Enumerate each complete interval D_v by enumerating +all subspaces of H_v/L_v. This does not assume that arbitrary simultaneous +marginal choices are feasible. + +Introduce nonnegative x_(v,a), for a in D_v, with sum_a x_(v,a)=1. +For every edge with two flexible ends, introduce nonnegative +z_(e,a,b) only for pairs satisfying `G_e a contained in b`. Impose + +```text +sum_b z_(e,a,b) = x_(u,a) for every a in D_u +sum_a z_(e,a,b) = x_(v,b) for every b in D_v. +``` + +When an end is fixed, charge its edge price directly to the remaining +x variable. When both ends are fixed, add its price to the constant. +For a two-flexible-end edge, charge z_(e,a,b) by its multiplicity times +`f(dim b-dim a)`. Include all eight center jobs in the constant. + +Every legal integral frame assignment induces a feasible point by choosing +its one node marginal and compatible edge pair. It has exactly the same bill. +No assumption that every fractional point has a global frame realization is +needed. Therefore the LP minimum is a lower bound on the legal minimum. + +The deterministic builder gives A x=b, x>=0, objective c^T x+c0, with +24,788 columns and 15,524 rows. It retains all 29,790 mapped edges and all +4,684 subspace choices across all 1,339 flexible contacts. This includes the +large component as well as the previously settled small components. + +## 2. Symbolic weak duality + +The certificate gives one vector d_i in Z^5 for every equality row. Set + +```text +y_i = d_i1*f(1) + ... + d_i5*f(5). +``` + +All variable costs use ranks zero through five; the verifier checks that +condition explicitly. The remaining fixed costs are in c0. For each column j +it computes the coefficient vector + +```text +s_j = c_j - sum_i A_ij*y_i. +``` + +Here c_j and s_j denote exact linear combinations of the five prices. +For every distinct nonzero s_j the directed bounds in section 3 prove +`s_j>0` at the stated p. The zero vector evaluates exactly to zero. +Consequently A^T y<=c, so for every feasible x, + +```text +c^T x + c0 >= y^T A x + c0 = y^T b + c0. +``` + +This uses only nonnegativity of x and the explicitly checked equalities. +It does not rely on a solver's status or on LP strong duality. + +The certificate also gives the indices of an integral feasible x. Every row +and index bound is checked exactly, and the associated node assignment passes +every original mapped containment and fixed vertex. Its objective, the dual +objective and the source objective are equal coefficient by coefficient to + +```text +2201*f(1) + 412*f(2) + 510*f(3) + 127*f(4) + 40*f(5) + 8*f(8). +``` + +Thus the LP and legal integral problems both attain this exact minimum. +The attained frame labels need not be unique. This proof says nothing about +other tariffs, the backward graph or different native words/boundaries. + +## 3. Exact directed power bounds + +Let S=2^192. First write r=2^k a with 1<=a<2, and use + +```text +log(a) = 2*sum_(j>=0) t^(2j+1)/(2j+1), t=(a-1)/(a+1). +``` + +The first 128 summands, each rounded down in units 1/S, give a lower bound. +Their total rounding loss is below 128/S. The remaining positive tail is at +most `2*t^257/[257*(1-t^2)]`, which the checker proves is less than 1/S. +Thus adding 129 units gives a rigorous upper bound. The same construction +bounds log(2); combine it with k and multiply by the exact rational p, +rounding the lower product down and the upper product up. + +The resulting interval [l/S,u/S] for p log r lies in [0,3]. Expand its +exponential through degree 256. Recur on integer lower terms with floor +multiplication by l/(S*j), and upper terms with ceiling multiplication by +u/(S*j). Each recurrence encloses the corresponding exact Taylor term. +Their sums therefore enclose the partial series. The positive remaining +series is at most + +```text +(3^257/257!) / (1-3/258) < 1/S, +``` + +which is checked exactly as a rational inequality. Add one unit to the upper +sum. For r=1 use the exact interval [S,S]. This proves every returned power +interval contains S*f(r). + +Evaluate each signed reduced-cost polynomial by using the lower endpoint +for positive coefficients and the upper endpoint for negative coefficients. +All 383 distinct nonzero coefficient vectors have strictly positive lower +bounds. The arithmetic uses integers and Fraction throughout. Finite bound +widths and Taylor remainders are checked, not assumed from decimal precision. + +## 4. What the certificate establishes + +This is a finite exact optimization certificate for a specified source-bound +frame contract. Its consequences for any native schedule use #4994's inherited +graph contract. No predecessor scientific verifier runs. No independent human +review, formal proof kernel, physical implementation, complete supplier invoice +or multiplication theorem is claimed. The current selected frontier is unchanged. diff --git a/research/pair-consistent-frame-optimum/README.md b/research/pair-consistent-frame-optimum/README.md new file mode 100644 index 0000000000..87d9288a5b --- /dev/null +++ b/research/pair-consistent-frame-optimum/README.md @@ -0,0 +1,137 @@ +# Exact full forward carried-frame optimum at the declared tariff + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +Claim type: **finite exact optimization certificate**, with a written +weak-duality argument. For the complete forward contact domain of Cinna Davis / +1337isnot1337's [#4994](https://github.com/CrocSwap/integer-mult-bounds/pull/4994) +and [#5016](https://github.com/CrocSwap/integer-mult-bounds/pull/5016), put + +```text +C = 15108879/5000000000 = .0030217758 +p = 1-C = 4984891121/5000000000 +f(0) = 0, f(r) = r^p for r >= 1. +``` + +The exact global minimum of the stated forward frame bill is + +```text +2201 + 412*2^p + 510*3^p + 127*4^p + 40*5^p + 8*8^p. +``` + +This covers all 1,339 flexible contacts and all 4,684 marginal choices, +including the previously unresolved 1,271-contact component. The scalar word, +carried native maps, fixed entrances/exits and owned-center contacts remain +fixed. The eight rank-eight center jobs are included. The original source +attains the minimum; the certificate also contains an integral attainer with +31 changed contact frames. No uniqueness is claimed. + +The new step answers the forward fixed-tariff part of JoyboyBrian's +[#5091 open question](https://github.com/CrocSwap/integer-mult-bounds/pull/5091). +A genuine pair-consistent relaxation has an exactly matching symbolic dual. +Its 24,788 nonnegative columns satisfy 15,524 equality rows with 59,077 nonzero +coefficients. The dual uses integer coefficients in the five prices +`f(1),...,f(5)`. Directed integer arithmetic proves all 383 distinct nonzero +reduced costs strictly positive. The other reduced-cost polynomial is zero. +The primal and dual objectives agree coefficient by coefficient, with the +source histogram above. [PROOF.md](PROOF.md) explains why this is sufficient. + +This closes a missing exact optimization step. It does not improve kappa or +replay a predecessor's numerical or scientific result. The original +marginal/rank-selector relaxation in #5091 is a different, weaker model; +its fractional witness is not rerun. Chris R / Clear1nsight's +[#5068](https://github.com/CrocSwap/integer-mult-bounds/pull/5068) already settles +18 small components with the large one fixed and rejects an all-concave +extension. Krzysztof Wójt's +[#5024](https://github.com/CrocSwap/integer-mult-bounds/pull/5024) settles the +intact-region model. Those results are cited, not rechecked or claimed here. + +## Reproduce + +From the repository root, with the Python 3.12 standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/pair-consistent-frame-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/pair-consistent-frame-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/pair-consistent-frame-optimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/pair-consistent-frame-optimum --check-source-history +``` + +Another CPython 3.12 path may replace the displayed interpreter. Expected +marker: `PASS_PAIR_CONSISTENT_FRAME_OPTIMUM`. Both registered commands are +read-only. The generated stdout receipt includes the actual interpreter and +SHA256 of every package file. No receipt is handwritten. No solver, NumPy, +SciPy, network or Git is needed by the scientific verifier. + +The checker authenticates eight predecessor inputs, executes only the retained +constructor definition and frame-graph definitions, constructs every marginal +subspace and compatible pair, and checks the entire primal and dual. It also +checks every mapped containment for the integral attainer and eight mutation +controls. The retained native verifier's top-level scientific program is never +executed. Source construction and its frame-contract semantics are inherited +from #4971/#4994. They are not independently audited here. + +Discovery used numerical linear programming to select a basis. Acceptance +uses the committed symbolic certificate and exact arithmetic only. The +22,668-byte compressed certificate is generated data; reproduction reconstructs +the mathematical model and binds it to the certificate by SHA256. + +## Limits and provenance + +This result is for the **forward orientation and this one tariff**. It does +not certify the backward graph, another exponent, a changed scalar/native +word, split ownership, arbitrary frame descents, or a changed boundary. +It prices the source's recursive frame bill, not routing, precision, stock, +absolute phases, the complete physical caller or the multiplication theorem. +The current selected #7000 and its five framework assumptions are unchanged. +The tariff here is historical and is not asserted to be the current supplier's +saving. Native, selected cold-replay, Lean and Docker checks were not run. + +The `p104-side-correction` card is explicitly changed to this optimization +interface. The first source-binding control passed against canonical base +`e54523517d0f03e58352e647c403a5af3e525a57`, whose selected conditional kappa is +`.00363005817`. This is a local obstruction to improving a fixed older word, +not the card's complete changed-helper supplier. Further construction must +change a hypothesis and price its complete invoice. + +The overlap check included live PRs, this account's earlier submissions, the +latest handoffs, active Discussions, batch reservations, merged searches and +main-tree README searches for the full-contact and pair-consistent model. +The broad card cache covered 545 open PRs and 7,207 Discussion records, with +incomplete sparse local coverage. Targeted Git searches also read the omitted +matching packages. These checks exclude neither unpublished work nor arbitrary +unsearched code diffs. The advance claim is +[here](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541785). + +## Open next questions + +1. Does the same exact minimum hold on the backward contact graph? Start by + building its pair-consistent model and seeking a separately checked dual. + This forward certificate does not establish the needed correspondence. +2. On which interval of exponents do the committed reduced-cost polynomials + remain nonnegative? Start with their 383 distinct expressions. The present + directed bounds certify only the stated exponent; #5068 already shows that + an unrestricted all-concave extension fails. +3. Can a changed word or boundary beat this fixed-model bill while preserving + arbitrary-input correctness and paying every new fee? First name the + changed contract and complete productive/paid ledger. Physical delivery, + restoration and supplier admission are unresolved here. + +## Credit + +Cinna Davis / 1337isnot1337 supplies #4994's carried-frame model and interval +completeness theorem and #5016's full-domain numerical screen. JoyboyBrian +supplies #5091's explicit stronger-relaxation question and its original-model +obstruction. Chris R / Clear1nsight #5068 and Krzysztof Wójt #5024 retain their +distinct exact partial optima. Dugongue / David Ganz #4971 supplies the signed +frame-carrying swaps, following Cao Yifan / intqwq's round-three word. Cinna +Davis #4440/#4470, zxv, Jacob Alan Sussman, James Reed and the retained +native/controller/compiler authors keep their predecessor credit. The source +LICENSE and NOTICE are unchanged declared inputs. + +Local marginal polytopes, linear programming duality and directed Taylor bounds +are classical. The new result is the source-bound full-forward certificate, +its exact verifier and the resulting fixed-tariff optimum. No literature-wide +priority for those methods is claimed. Implementation bounds and justified +Power of Ten deviations are in [IMPLEMENTATION.md](IMPLEMENTATION.md). diff --git a/research/pair-consistent-frame-optimum/SOURCES.json b/research/pair-consistent-frame-optimum/SOURCES.json new file mode 100644 index 0000000000..d20f7bb50f --- /dev/null +++ b/research/pair-consistent-frame-optimum/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/carried-warp-frame-intervals/README.md", + "usage": "input", + "git_blob": "15af4809991fc192717bfbf38136f24c34240a6b", + "sha256": "1186b6c09480bd40b2b6d71105ad9d4582d83eb51ff31bfacd69b3a589468cd6" + }, + { + "path": "research/carried-warp-frame-intervals/discovery/README.md", + "usage": "input", + "git_blob": "92e69475bdc1d83c84bab2840938a5195a9fcbd5", + "sha256": "4408fef72b0e1f86ff939b3cc366bbeb95679f6698d760d5bf90a2784a4a587c" + }, + { + "path": "research/carried-warp-frame-intervals/frame_dag.py", + "usage": "input", + "git_blob": "307934bb58765d80043f6901d250f370a95c686f", + "sha256": "2f1277c6467b7219d2a0988138386c2ec5efdfbf6a5c106da6d479b0ede7abd5" + }, + { + "path": "research/full-contact-exact-native-optimum/README.md", + "usage": "input", + "git_blob": "0c065137bdedec8ce9cc2f9890a79b6d610720c6", + "sha256": "73e8a4dc2d7327bb449e9396a355c1bb7653f960745d5dff7d07e46c606dd1b1" + }, + { + "path": "research/native-frame-carrying-swaps/LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "research/native-frame-carrying-swaps/NOTICE", + "usage": "input", + "git_blob": "faa0f8ce7f3dfb9b7095302d60a37469cea91da4", + "sha256": "57d5bcf4f205d6d4c16eb81f37c5a1ab0c99185de26978cab99f0ce82b3147f0" + }, + { + "path": "research/native-frame-carrying-swaps/SOURCE-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/native-frame-carrying-swaps/verify.py", + "usage": "input", + "git_blob": "88aa08b7d54cdae5b2c6696fe96a73a9ae89debf", + "sha256": "9e536497b6bf5a1162a933c1aef0ff079f1ec21996095ccfeda40252e0b7b3dd" + } + ] +} diff --git a/research/pair-consistent-frame-optimum/TASK.json b/research/pair-consistent-frame-optimum/TASK.json new file mode 100644 index 0000000000..1f08bb9831 --- /dev/null +++ b/research/pair-consistent-frame-optimum/TASK.json @@ -0,0 +1,129 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact minimum of the full forward carried-frame contact problem at C=15108879/5000000000 using a genuine pair-consistent LP and an exact symbolic dual.", + "scope_change_reason": "The card is changed from constructing a selected helper split to resolving the full-forward exact optimization question left by PR5091 and PR5016. No native supplier or current-frontier gain is claimed.", + "bottleneck_link": "A fixed source word cannot gain at this tariff by any legal contact-frame assignment in the inherited contract. Changed words, boundaries and complete physical invoices remain open; this historical tariff does not certify the current frontier.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified full-forward finite optimization certificate. Do not extend to the backward graph or other exponents.", + "outcome": "completed", + "evidence": "24,788 nonnegative LP columns, 15,524 equalities and 59,077 nonzero coefficients; integer-coefficient symbolic dual, 383 strict nonzero reduced-cost signs, a matching integral primal, eight controls and all original mapped containments for that attainer.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the same optimum hold on the backward graph?", + "why_it_matters": "A forward certificate does not establish the dual-orientation optimum.", + "first_step": "Build the backward pair-consistent model and seek its own exact dual.", + "blocked_by": "No backward certificate or correspondence is supplied." + }, + { + "question": "For which exponents is this symbolic dual feasible?", + "why_it_matters": "This identifies whether the fixed-tariff obstruction persists under a changed price.", + "first_step": "Certify an interval for the 383 distinct nonzero reduced-cost expressions.", + "blocked_by": "Only one exponent is enclosed here; PR5068 already disproves an all-concave extension." + }, + { + "question": "Can a changed source word or boundary lower a complete signed invoice?", + "why_it_matters": "The fixed-forward model is now exactly closed at the stated tariff.", + "first_step": "Name a changed contract and every new productive and paid fee.", + "blocked_by": "Physical delivery, restoration and full supplier admission are unpriced." + } + ] +} diff --git a/research/pair-consistent-frame-optimum/VERIFY.json b/research/pair-consistent-frame-optimum/VERIFY.json new file mode 100644 index 0000000000..d1a0ffb99e --- /dev/null +++ b/research/pair-consistent-frame-optimum/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/carried-warp-frame-intervals/README.md", + "research/carried-warp-frame-intervals/discovery/README.md", + "research/carried-warp-frame-intervals/frame_dag.py", + "research/full-contact-exact-native-optimum/README.md", + "research/native-frame-carrying-swaps/LICENSE", + "research/native-frame-carrying-swaps/NOTICE", + "research/native-frame-carrying-swaps/SOURCE-WORD.json.gz", + "research/native-frame-carrying-swaps/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Reconstruct all forward domains and compatible pairs; check the complete integral primal, symbolic weak dual, directed power signs, mapped attainer and eight mutations." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Reconstruct all forward domains and compatible pairs; check the complete integral primal, symbolic weak dual, directed power signs, mapped attainer and eight mutations." + } + ] +} diff --git a/research/pair-consistent-frame-optimum/model.py b/research/pair-consistent-frame-optimum/model.py new file mode 100644 index 0000000000..4cb2b50fce --- /dev/null +++ b/research/pair-consistent-frame-optimum/model.py @@ -0,0 +1,145 @@ +"""Pair-consistent carried-frame model. New work produced by Nick Petalas. + +The authenticated construction and frame graph are credited to Cinna Davis; +only their definitions run, without any predecessor scientific replay. +""" +import ast +import copy +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path +from types import ModuleType, SimpleNamespace + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def digest(value): + normalized = json.loads(json.dumps(value)) + raw = json.dumps(normalized, sort_keys=True, separators=(",", ":")).encode() + return hashlib.sha256(raw).hexdigest() + + +def authenticate(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + paths = [row for row in manifest["files"] if row["usage"] == "input"] + need(len(paths) == 8, "Declared input inventory") + result = {} + for row in paths: + payload = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(payload).hexdigest() == row["sha256"], "Input hash") + result[row["path"]] = payload + return result + + +def load_graph(inputs): + prefix = "research/native-frame-carrying-swaps/" + data = json.loads(gzip.decompress(inputs[prefix + "SOURCE-WORD.json.gz"])) + need(data["canonical"]["h"] == 9, "Fixed nine-dimensional source") + need(len(data["programs"]["forward"]) <= 100000, "Source event bound") + frame = ModuleType("authenticated_frame_definitions") + source = inputs["research/carried-warp-frame-intervals/frame_dag.py"] + exec(compile(source, "authenticated_frame_dag.py", "exec"), frame.__dict__) + tree = ast.parse(inputs[prefix + "verify.py"]) + definitions = [node for node in tree.body + if isinstance(node, ast.FunctionDef) and node.name == "construct"] + need(len(definitions) == 1, "Unique retained constructor") + canonical = data["canonical"] + need(len(canonical["frames"]) <= 5000, "Source frame inventory bound") + masks = [frame.space(vectors) for vectors in canonical["frames"]] + spaces = [{x for x in range(512) if mask >> x & 1} for mask in masks] + namespace = {"c": canonical, "spaces": spaces, "Q": Fraction, + "copy": copy, "V": SimpleNamespace(need=need)} + exec(compile(ast.Module(body=definitions, type_ignores=[]), + "authenticated_construct.py", "exec"), namespace) + program, _, _ = namespace["construct"](data["programs"]["forward"]) + schedule = frame.NativeSchedule(canonical, program) + return frame, schedule + + +def domain(frame, lower, upper, cache): + complement, generated = [], lower + for vector in frame.basis(upper): + if not generated >> vector & 1: + complement.append(vector) + generated = frame.join(generated, frame.space([vector])) + gap = len(complement) + need(gap <= 5, "Fixed-source quotient bound") + if gap not in cache: + values = {1} + for vector in range(1, 1 << gap): + values |= {frame.join(value, frame.space([vector])) for value in tuple(values)} + cache[gap] = sorted(values) + return sorted({frame.join(lower, frame.space( + [frame.linear(complement, v) for v in frame.basis(value)])) + for value in cache[gap]}) + + +def compatible_pairs(frame, left, right, columns): + result = [] + for a, av in enumerate(left): + moved = frame.image(columns, av) + for b, bv in enumerate(right): + if moved & bv == moved: + result.append((a, b, frame.dimension(bv) - frame.dimension(av))) + return result + + +def build_model(frame, schedule): + graph = schedule.graph + lower, upper = graph.bounds() + need(len(lower) <= 16000, "Graph node bound") + cache = {} + domains = {i: domain(frame, a, b, cache) + for i, (a, b) in enumerate(zip(lower, upper)) if a != b} + need(sum(map(len, domains.values())) <= 5000, "Marginal domain bound") + counts, rows, rhs, variables = [], [], [], {} + for i, values in domains.items(): + variables[i] = list(range(len(counts), len(counts) + len(values))) + counts.extend({} for _ in values) + rows.append(dict.fromkeys(variables[i], 1)) + rhs.append(1) + edges = Counter((a, b, m) for b, parents in enumerate(graph.parents) for a, m in parents) + need(sum(edges.values()) <= 30000, "Mapped edge bound") + constant = Counter({8: 8}) + for (a, b, columns), multiplicity in sorted(edges.items()): + if a not in domains and b not in domains: + constant[frame.dimension(lower[b]) - frame.dimension(lower[a])] += multiplicity + elif a not in domains or b not in domains: + i = b if b in domains else a + for j, value in zip(variables[i], domains[i]): + rank = (frame.dimension(value) - frame.dimension(lower[a]) if i == b + else frame.dimension(lower[b]) - frame.dimension(value)) + counts[j][rank] = counts[j].get(rank, 0) + multiplicity + else: + pairs = [] + for ia, ib, rank in compatible_pairs(frame, domains[a], domains[b], columns): + pairs.append((ia, ib, len(counts))) + counts.append({rank: multiplicity}) + for side, i in ((0, a), (1, b)): + for k, variable in enumerate(variables[i]): + row = {j: 1 for ia, ib, j in pairs if (ia if side == 0 else ib) == k} + row[variable] = -1 + rows.append(row) + rhs.append(0) + source = Counter({8: 8}) + for (a, b, _), multiplicity in edges.items(): + rank = frame.dimension(schedule.original_values[b]) - frame.dimension(schedule.original_values[a]) + source[rank] += multiplicity + need(len(counts) <= 25000 and len(rows) <= 16000, "LP size bound") + return {"rows": rows, "rhs": rhs, "counts": counts, "constant": dict(constant), + "source": dict(source), "domains": domains, "variables": variables, + "mapped_edges": sum(edges.values())} + + +def mathematical_digest(model): + keys = ("rows", "rhs", "counts", "constant", "source", "domains", "variables", "mapped_edges") + return digest({key: model[key] for key in keys}) diff --git a/research/pair-consistent-frame-optimum/powers.py b/research/pair-consistent-frame-optimum/powers.py new file mode 100644 index 0000000000..9721ccd7a8 --- /dev/null +++ b/research/pair-consistent-frame-optimum/powers.py @@ -0,0 +1,59 @@ +"""Directed integer bounds for r^(4984891121/5000000000), 1 <= r <= 9. + +Produced by Nick Petalas. Only exact integer and rational arithmetic is used. +""" +from fractions import Fraction +from math import factorial + +SCALE = 1 << 192 +NUMERATOR = 4984891121 +DENOMINATOR = 5000000000 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def log_series(value): + require(Fraction(1) <= value <= 2, "Reduced logarithm domain") + t = (value - 1) / (value + 1) + term, lower = t, 0 + for index in range(128): + summand = 2 * term / (2 * index + 1) + lower += summand.numerator * SCALE // summand.denominator + term *= t * t + tail = 2 * term / (257 * (1 - t * t)) + require(0 <= tail < Fraction(1, SCALE), "Logarithm remainder") + return lower, lower + 129 + + +def price_interval(rank): + require(type(rank) is int and 1 <= rank <= 9, "Rank domain") + if rank == 1: + return SCALE, SCALE + shift = rank.bit_length() - 1 + lower, upper = log_series(Fraction(rank, 1 << shift)) + low_two, high_two = log_series(Fraction(2)) + lower = (lower + shift * low_two) * NUMERATOR // DENOMINATOR + upper = ((upper + shift * high_two) * NUMERATOR + DENOMINATOR - 1) // DENOMINATOR + require(0 <= lower <= upper <= 3 * SCALE, "Exponential domain") + term_low = term_high = total_low = total_high = SCALE + for index in range(1, 257): + divisor = SCALE * index + term_low = term_low * lower // divisor + term_high = (term_high * upper + divisor - 1) // divisor + total_low += term_low + total_high += term_high + remainder = Fraction(3**257, factorial(257)) / (1 - Fraction(3, 258)) + require(remainder < Fraction(1, SCALE), "Exponential remainder") + return total_low, total_high + 1 + + +def polynomial_interval(coefficients, prices): + lower = upper = 0 + for rank, value in enumerate(coefficients, 1): + a, b = prices[rank] + lower += value * (a if value >= 0 else b) + upper += value * (b if value >= 0 else a) + return lower, upper diff --git a/research/pair-consistent-frame-optimum/verify.py b/research/pair-consistent-frame-optimum/verify.py new file mode 100644 index 0000000000..79022e5e76 --- /dev/null +++ b/research/pair-consistent-frame-optimum/verify.py @@ -0,0 +1,145 @@ +#!/usr/bin/env python3 +"""Check the full forward pair-consistent frame optimum without a solver. + +Produced by Nick Petalas. Claim type: finite exact optimization certificate. +""" +import copy +import gzip +import hashlib +import json +import platform +from collections import Counter + +from model import HERE, authenticate, build_model, load_graph, mathematical_digest, need +from powers import SCALE, polynomial_interval, price_interval + + +def histogram(counts, selected, constant): + result = Counter(constant) + for variable in selected: + result.update(counts[variable]) + return [result[rank] for rank in range(1, 10)] + + +def primal_check(model, selected): + need(isinstance(selected, list) and len(selected) <= len(model["counts"]), "Primal inventory") + need(all(type(j) is int and 0 <= j < len(model["counts"]) for j in selected), "Primal index") + need(len(set(selected)) == len(selected), "Primal uniqueness") + support = set(selected) + for row, rhs in zip(model["rows"], model["rhs"]): + need(sum(value for j, value in row.items() if j in support) == rhs, "Primal marginal equation") + return histogram(model["counts"], selected, model["constant"]) + + +def dual_remainders(model, dual): + need(len(dual) == len(model["rows"]), "Dual row inventory") + need(all(isinstance(row, list) and len(row) == 5 for row in dual), "Dual price basis") + need(all(type(x) is int and abs(x) <= 256 for row in dual for x in row), "Dual coefficient bound") + reduced = [[hist.get(rank, 0) for rank in range(1, 6)] for hist in model["counts"]] + for row, vector in zip(model["rows"], dual): + for variable, value in row.items(): + for k in range(5): + reduced[variable][k] -= value * vector[k] + return reduced + + +def dual_check(model, dual, prices): + need(all(set(hist) <= set(range(6)) for hist in model["counts"]), "Variable rank basis") + reduced = dual_remainders(model, dual) + distinct = Counter(tuple(row) for row in reduced) + positive = [] + for vector in distinct: + if any(vector): + lower, _ = polynomial_interval(vector, prices) + need(lower > 0, "Dual reduced-cost sign") + positive.append(lower) + objective = [model["constant"].get(rank, 0) for rank in range(1, 10)] + for rhs, vector in zip(model["rhs"], dual): + for k, value in enumerate(vector): + objective[k] += rhs * value + return objective, {"distinct_reduced_costs": len(distinct), + "zero_reduced_cost_columns": distinct[(0, 0, 0, 0, 0)], + "strict_signs": len(positive), + "minimum_positive_lower_over_scale": [min(positive), SCALE]} + + +def certificate_check(model, certificate, prices): + need(certificate["schema_version"] == 1, "Certificate schema") + need(certificate["model_sha256"] == mathematical_digest(model), "Mathematical model digest") + primal = primal_check(model, certificate["primal_ones"]) + dual, signs = dual_check(model, certificate["dual"], prices) + source = [model["source"].get(rank, 0) for rank in range(1, 10)] + need(primal == dual == source, "Coefficientwise primal-dual-source equality") + need(primal == certificate["optimum_histogram"], "Certificate objective") + return primal, signs + + +def rejection(action, message): + try: + action() + except ValueError as error: + need(message in str(error), "Unexpected rejection reason") + return message + raise ValueError("Mutation accepted: " + message) + + +def controls(model, certificate, prices): + results = [] + changed = certificate["primal_ones"][:-1] + results.append(rejection(lambda: primal_check(model, changed), "Primal marginal equation")) + results.append(rejection(lambda: primal_check(model, [-1]), "Primal index")) + changed = certificate["primal_ones"] + certificate["primal_ones"][:1] + results.append(rejection(lambda: primal_check(model, changed), "Primal uniqueness")) + dual = copy.deepcopy(certificate["dual"]) + dual[0][0] += 1 + results.append(rejection(lambda: dual_check(model, dual, prices), "Dual reduced-cost sign")) + dual = copy.deepcopy(certificate["dual"]) + dual.pop() + results.append(rejection(lambda: dual_check(model, dual, prices), "Dual row inventory")) + changed = dict(model) + changed["rows"] = model["rows"][:-1] + results.append(rejection(lambda: certificate_check(changed, certificate, prices), "Mathematical model digest")) + changed = dict(certificate) + changed["optimum_histogram"] = certificate["optimum_histogram"][:] + changed["optimum_histogram"][0] -= 1 + results.append(rejection(lambda: certificate_check(model, changed, prices), "Certificate objective")) + results.append(rejection(lambda: price_interval(0), "Rank domain")) + return results + + +def actual_assignment(schedule, model, selected): + support = set(selected) + values = schedule.original_values[:] + for i, variables in model["variables"].items(): + chosen = [k for k, j in enumerate(variables) if j in support] + need(len(chosen) == 1, "Integral frame marginal") + values[i] = model["domains"][i][chosen[0]] + schedule.graph.check(values) + return sum(a != b for a, b in zip(values, schedule.original_values)) + + +def main(): + inputs = authenticate() + frame, schedule = load_graph(inputs) + model = build_model(frame, schedule) + raw_certificate = gzip.decompress((HERE / "CERTIFICATE.json.gz").read_bytes()) + need(len(raw_certificate) <= 1048576, "Certificate size") + certificate = json.loads(raw_certificate) + prices = {rank: price_interval(rank) for rank in range(1, 10)} + optimum, signs = certificate_check(model, certificate, prices) + changed = actual_assignment(schedule, model, certificate["primal_ones"]) + rejected = controls(model, certificate, prices) + hashes = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(HERE.iterdir()) if path.is_file()} + result = {"status": "PASS_PAIR_CONSISTENT_FRAME_OPTIMUM", "claim_type": "finite exact optimization certificate", + "orientation": "forward", "saving": "15108879/5000000000", "optimum_histogram_ranks_1_to_9": optimum, + "nodes": len(schedule.graph.fixed), "mapped_edges": model["mapped_edges"], + "flexible_contacts": len(model["domains"]), "marginal_choices": sum(map(len, model["domains"].values())), + "columns": len(model["counts"]), "equalities": len(model["rows"]), + "nonzero_coefficients": sum(map(len, model["rows"])), "attainer_changed_frames": changed, + "dual": signs, "controls": rejected, "python": platform.python_version(), "sha256": hashes} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()