From 340e3babf1775f79131d2f4d4633a1241e1ad8c1 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 02:30:22 -0500 Subject: [PATCH] Add bounded R439 five-helper cycle construction --- .../CANDIDATE.json.gz | Bin 0 -> 38444 bytes .../r439-five-cycle-seed9f01/CERTIFICATE.json | 120 + research/r439-five-cycle-seed9f01/README.md | 134 + .../SEARCH-RESULT.json | 2463 +++++++++++++++++ .../r439-five-cycle-seed9f01/SOURCES.json | 145 + research/r439-five-cycle-seed9f01/TASK.json | 70 + research/r439-five-cycle-seed9f01/VERIFY.json | 37 + research/r439-five-cycle-seed9f01/search.py | 231 ++ research/r439-five-cycle-seed9f01/verify.py | 193 ++ 9 files changed, 3393 insertions(+) create mode 100644 research/r439-five-cycle-seed9f01/CANDIDATE.json.gz create mode 100644 research/r439-five-cycle-seed9f01/CERTIFICATE.json create mode 100644 research/r439-five-cycle-seed9f01/README.md create mode 100644 research/r439-five-cycle-seed9f01/SEARCH-RESULT.json create mode 100644 research/r439-five-cycle-seed9f01/SOURCES.json create mode 100644 research/r439-five-cycle-seed9f01/TASK.json create mode 100644 research/r439-five-cycle-seed9f01/VERIFY.json create mode 100644 research/r439-five-cycle-seed9f01/search.py create mode 100644 research/r439-five-cycle-seed9f01/verify.py diff --git a/research/r439-five-cycle-seed9f01/CANDIDATE.json.gz b/research/r439-five-cycle-seed9f01/CANDIDATE.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..9e4ca90ee968cbb9b7d0b66ca0d94dd3c7e9301a GIT binary patch literal 38444 zcmXte1yqyo|Mpiwk&*@x0g2JwN(@k>YqT^agE7{a!*wta4u^+f{^AcYm_WE6 zK?&d7Kou$*ezSvVIA5vTvirvG$V0V~E-Uhen_;5z&3Es-zFrmBS!w=Io^+nLJ?2a! zzO)J5!8sK${0X^$Vk{%{3cPM+ta_0I6NP=OISuDcvzqC4owrsez8}%`ZvIlp>l&H! zt`g`;el1F}_J5+j_q+ZR<+SmdmBxkm(rH8IdcAeM{;97}=KUc{r=IWlSEMBBPkpYk z?^H82wrCRlSLUan6N^=4!E4CmEX`l-JZ#qIwAbc+?_YZT^dafr)&FS$&9%}%Wc)v1 zwbB^bU*#xd{hqQ{0cO(WQs~;wlQ2NhPQ60JvxgUHN@FZ8w~*|Mk2!ykN-3TEiND5O zILDL4uxZ?^r1Jl3U>t8{Vo=YMHo zj0!RPpCcr2R*kzcS5=>m(18C&eqVnamI8%5%}c?~VxX|YS>e=&+(q8>^xuiYNI{*}`+14-Rxx(Afm z`7ZRjrJswL!vvP1RXys?-HiaRFNYlw`JUMyHb@(18oCb$3Nlg{;T->YnqI&6%#>@eya*7m7alC3p}G=(eRl%oot zOrCjA*vFV$7L}9U2em}bMd?oXXfd7CHFHm%+}&a+|rU~L)}hi?5#;X4o1VkdvreqS!!vAe%w{53P;OokvsUJ9zmFXh8_;hpZsD^LP`Mmf zX(;m?P27O0+FcHoIxD1$x6^msFb=)Dzbdy{GCQFZVO0Lu#uR|rumsHfc4w+=`&m}9h z7<2o}mk(nGdizlwOd_9457@KGoWq#F$5d4j3<%Tm7YSPrHaDR1b0=Y*icX$Kx<^sk zj&Cr4VnnaA4K}J*+FqljDS`Bjb86L?MRWO1b{5-%Q+cK1UdNCLX<{M8l)J6Y8Kj9Z zuw`~Dx?&QPVmOReMn@Itqi3f7;2`6GrtfP*9^z8Fq#cS}5OWm>c8Iy_Ct}qm5lgri z>@tvSWfdB<-i)EV^MUMHra$U=no0P@j#I<2Rma2e!_y4dB7UT-26Ukq#sOBP4rne< z3J-z}A7Ic!9`=VF-Y_}jP!9X_tHWPifo8wF+t7t=G!^&o?%*I;nOqnuw3qq}`bgBO zjqCN?SoeNEgyU->i~WO=CDbTpl}d!6W17KIacM(pM#QSjCB>chv(v$wnv~LUyUzzmm?$cm3P&XO z%n|u}By$n-hgB^iSys*PrQ}AhZttGk?!CIw4{*rK){GT@yBC&KZ$;CKre#a@nWX#d zzxh9$#w{*+TkM)To0S5j4h~y_RMrC$FH6#TzphE(qqGP91mPNO>y0k)=pLxA z_jw9RMp8wGw8NO3y-BuDKz8I=Gh6&??5(bdnl;L~A*GIoh|t5(m14x>{_;M5@r7p< zsy9;--4V~{&2%-8>bFdm13w04F?*aZo*zXD9OO*NuUOD{!+2J4Tr(frSY<`69y?Dn z*eOWc8l_v`t;;^xTxr}Jg>@{c#5mlq9Gh0RXI zd!E4Tjnm#5Pv?FfCwf_;q+aNfZZkVVFd|a+CIi2)Y z`__!q=b~nJoCTBTN|lpe$M+LOYz&M1kIr*(_xT{vWv8bY=a4E`s7;5xX}1~p`yEe# z_+Co+_Vb9=PXLek1r=1&*us&%yv*)W$a<_t*n`01%n>z9{|nDA&50qHVqvcV%aYdi zL$%53qw@;|aFA@S`_=ZC2QA_YrC(R&d{vz0-s4TH4*NCRaEzZYZG@~2ehdpdU<}?K zuspp8f6%?n7YrwFR*qcg+o3Tuxd+aq^7Nx?F&nd%pGIu-SxR3Wlq;vk7jIa#6h8d) zynN`9dCs!c*Py=UHBs`zxh@+(%wG(!K9Aa`3y9dDWPoS7z@0kL@9=9flyK3&@hIt` zwxG@b+@3eK*{x6ezR28IS>LS7ez(R-a`Nbxk5R6xTQW zud+KOf8?bp$QX_(o_SgucNBup6RbA$0y4ANSIwiQm#Q1J53E*nxn`?nxevwPQB8*FjkRAnefUCNwL3^uuC}u?$H-}ZqAIA|n5`Pa zzAYg!pt5dL^RsO?JUi~!iET_s4{G1c^58c!(*fnmca+Q+)Ls0YH6O_VaGr_b=z zKA4}6LO5St?Eu}uxjis2p{ME35S0?c^l8M-W!M}lc9JUZ^v!uV5I3X`?w~r&|9HtR z$=Lpm6BRC~1e|XUQglAE8DyEjJJBux&zlviA@^kzYBy*dcfm<{kh%l_>UR-}Z|P*DH#7 z>?yE~$|uXFjAN(Sg60R`-{Yk+lMp>{pE)xXU!j`YL`_bfBLc53TH)6hKW;y)v-^3l zj_y7~&ZmS$jDE<*uic=UZ!QXA$<1f|c3)bbKL|Qan55d?B_siXo7WE?OR_mV?jjfs zZQ?xJvvMZBzmHg%SKi+(3A0)r$z{$O48dNyrlM+6(5F78-vcCLU&?zkcZXlTP#lk3 zAxhuB==gThvD!6yx)c0uD;Vtuyod|PhVuaDHt{Q;E4&6gKYcl~SOQ$;01qnv3ai+E z)Rn{ff>CE*EI0jn$A|B8=bAs9(A3=s>}DSqsdr%WVjHkIvfV$N#2%fVzlm+FUHSF& z+<4C|%#M_TiZ^wrHFI$3(RroZ&}OK#wR~sL%0#)8zIFw}gRT4XJb7(T?L4a$A z!+o#Az@^U**Sea&d1{qhE6aC@D;r zQTuF39~|6`LEybQyWfm@VI{~0&^V++pb>x#c>XhPMOzO?i7`Z-ze+`I^NisSWaNSS z3*B?OJ#NN}98@6#uftAC0_=iqH@^g910LgWoviI(DO7su6dO*3r2rpW-@S>S1`hTq zYU5Zj2{7Q9s2j=l8Qu@aOq}yA6v*{!W*4^+)cqp*^UkG(UGo{Y62oNwkGazB_53q9 z-ZRjE!kzAvBoCN{&CfqGT0&68u54cPoOECjI5GTn5)4eNGn?UU_7G!<)$cGH?j2DW zk6);7Qf%Qo_fyUPyANDl1a~yDRylSN`1U356E3`7aO2z5H}C=7%;Z6yxKK@CV^ zqi{;$V$IrubCS7p_3<=qz?ytnkpLdcjePu72XHQqG`EUG=kI0|c>?xHo*{S*j_Jg; z)9`)1$2kA#-n%eh_xXKihN$58n?3SHs8~M*u~gZMI)MPD-hr!79MKo_V#^w|oS71x*kzvB?OBmrVSQcu z5kNP6oNR$*QS&g-!TA7@RHHA>ni1Xm)8}n^m1GLxi`DF6m+eEE77ycRM^S?Z<0v~{ zoWs9{Fhkh|w_GYgr8@VN{|X3ZJC}w5#ZF1KF+;&4_-`}tJOn1pi{KdQ>}<-@#SzB@ z-+k1zO5@o3kWplaW#ZbCj`y$p6teO{!}h>4cM*b(EDI8g-`{MWjU;BuhkQ}YpA_q4 zpM8=-QjD6_J0{ZEM1@MRUFqCUy^ee0`{MvaNp(B$QJ2m6w}YFV=WVkPw`knhzCP1* zP~W3f>`+je?0NXN*TDI)I-mwol8VIkZsXb>m-OPb^8U< z9WEa1wR!|HW`SxKMK&oBK`&CY2c%Y8`WNor-4)%&lc@Zs-&4LHx$}ksas1!(sj!Sx z^>yHgwo&b8B->bEdlN8cQE}1XgndusEK#&)dqX?Vz>{Uxh|r@DPDma*4QOR6z0b82 zF=x$wU1IHu1fi@;3>-sb`Qe~DWasd3bH92ZzoMM#QGlM6T?zD7m(+g%jOI^oI>fmn z{ntgk%^oE5npXC#OO{t6KC;*~{;a$qZyWgKGNr@aY#KuMH=Bj^fJ=x;-1a2SsgwPVL$nGW_3cytF-iVnepTx3R8ZfQ(&=Ta zS9{P}3O0upcuT%g{AlZa2V0)%CM)pP^`u|}hhOIB;}I7u(?LJPNTbdq;3amcnVO*j z#k)(VzM;0D!6h8LWbJ1ccu}@7Ftr?g8d~euNo4!ex}m+pKxf(8Za9v8d~+&qQ$?EB z<15fj_Kl3d+404|YhaQ27S3DozL(r}ZeV1Q@+*_2N1#>NMXv|h*e9X~W^Bs=yb!ha zU88H(4Z(H@pTB7V9J18WIy)RJuFkrQl9`wz`kq-u61IR_h;ZK5-H5t(fQ6u@_a1d_Jn(vY{r&W`j&)C^D|}3@uOCaVgK0)Bz`f6812|7f zK84L7*6~N+A6E~p*3WDiNp{{lMkvnn)C{F_2Vi^R;s)+DM7myyf$^3;Db32VZAxO+ z>=1Z=hF7fE9?hZ1{1begVm{SoEAU*Q#D>re?50Ae{XSRWh(%q^+?|g=i`Lq#j&EB%H55MLtIB`mzED5&YI8mQd>ma)U9ZmqYgK|PJVk6 zwwu3?>)5)e{JhE(8oxv^e{h&g)N+n4D8f|*4rPXy+Ebi|(Q=Ky9Sp2Dn+-rx-IuW+ z_o#Gmm7Tbb?o+d++mV+;x{dy|yx-gAiL`Ep)Vy^_Bpd+chKQ!m z9XWVjcOwv&`mfke@ppm>1BfMq7$d)pl`hU)&#!!{xuWZ#vbr%=w<7Tj_sa$zhYbv8 zLsgKLn|R=pzp*i9$YCwBu%Z)xQQl|lj6CvW#rQj^SLD;j4nXcC)FEFGGf?2@d|&@C z?z%{pz=56MCd+f4M#3@}f(<0Ew8exoRU008);nxc-L$-2X(WarDaHqPtp}`msJrwa zfpXQUe9kp4iPkfgU#_j)LsRq7BCB4{~(k&@6feYF+_10L;zg(kRByM!1o!d%@}MY-*x zRnQVf_jL#g7j8S2QEORl9xj$lGJ(32T=MrUWRDaD?gJ;I>;}~K)ABDu|8$2B8MQYo zreNQ+OKB@L>?x$5cQ61Myym>Z|A5RmmPJlq1&uYiMLu+0Jii;LlxzXI@bw5?7{%@-n+{RnF5lVjHhh?7O z;E&l05pDHg* zJKV7WIQbghWmAtwNr64f*OqW;)1QI^T;Tz$nn?IFyz|6%nW4M!GxpFLn{SO3?9RO8S`J@1^%qYD zySHzeRO|2OpqeOx#wMd8zK630ja39GMEJ0M#b@YtII#Uqa;g&i@U#{#q8{k`O{~dd zr*or&?b1))yQ_NL`cNOYe<7ljVc@-AvQg6HHD^ntPpSYOoXkfZU;i^>?#^FiXCAL- zweYyNdAUhKXhIy@{Ub~X&W?J%iMR+yu@cOC2c<0s5GA;kTZidE_>+7f4xtZz$y|(A zcLSdWg23F9=0zqQ@PwUUuYIo|{MrLA%yr?-q#!!?tGBwXN;bl_2m_dq?jT3`y7^`k zAA&18aQ_k8Lh1D>de1BCaw$A#f3t-3Y``+SPh64x(y!go+;Z!3dDS)4D}%wWRS~nX zfBD4DHb26-iK|E|SzU%;v-G$2!0J639ZzxZ8J%0N$U>d|l|QhK^}2%`PwQ=BCvm}@ z?0J8SH=vgL>+Y*tUd`;c0Z0jpUIQN$jD| zdQKEH=KFEq^P~kPFg>^yp!eC(F{pk0I`b}eg1@eSjsn1DcJOX` zuDrLGz@jq}{7$#o8TdMoS(il4VD6n46xcQ7-;}EIx^BtzE(&ayH%`^NVwSpux{uI0 zgG^o)4DCSPqfz{%5eh4b$1xLTQ5p`z_wYp*QTZj;bvccrK;Y6OQvRO&qJSxbQTo8$ zV?%I7mp?Bp)|xNh7)%oye}8n{ zt4EbD=R;ek)zQ*YGV|wTUF?&t7vB|>tn*nf;uYW#gH@Jzre><~%?sbFki0yq(PLp3 zMV{Zg=pe6CYs-$Nr6;qMn_Fk1-(%$^^Ys1PEjn_RSQ;ltuG~fR8}Rh!bs}&>Kjc?% z=$n;?h&h*2o^p>Zgly%AeW?C!_tMsM(1@f@SNtwK`$_Zr?yz?7{AMzwoeErfd^#8a zUT(pybpJ-hjK)00=k4k%ca^F)G50H5-|6r*c-jY>J@k>{H`c|q zdg_Yt^B!Gxch3afD%{;@ED@kImtmfF>KGzVOY@e*f!7o0Hc1DIxZ_-IKr7z5dDR%7_ zmo#F`x>`S{?!Ea24mS!HBm|~)YhN@E>K~msq7LU)p`of*YzNhEynac7*^j!1ZHq$z zqoGxGZ|R`=N0zH=B?4w+pqa&Ew<^)!QNCSqgH3nqn=Qp3pXP%Ce7Ax{H(t0}!=yjz zE3H>&)38_7^`i@gMBC>SR9ZeeH*`UM`5f=MzGpj9^H6k8<{vZdV%1Nb6n_KtFHWQC z+joEN>Xxl^h>;)k@>at1zmebUlL|~>;5fnuD=8}^j!eGeZhwO}JzzykwuUMDWqQ{g zyu&GNn(&^b>fEZTjdJG!n}fA~OZtZVckaE&%4z;r7OP4Mt zE{hn4-d$PTACn!&JI>{^f%h-t8Nb$Xuj50X>k^&a^x1p2uo7NXYx9Gkke|DK`CtC( z$Iwxa^Hl_&e}9j#u5^_iSuHZD{KgvqZklb3 z?C#lQXsBawev&tAThpgh7&5ju5;(PNz2e3njFsww?ar08dy_f*QnLe}2AQXC4O8u0 zaV9IODc#3px(P`mP`}K>kKQT3 z5vaMqimmsCjxP(+NXE=r&vC!6g?c~*hrgQ_Rguv9@!gjb zOO`YHZp>O-Z{x9P+^Q*gSfkvXf~#s?Mz*2EB%6(f+qX9!ZYOkzuCvUOsgXp)h|C+_ zc2IW^G9fn1U3~Y$z=QhwR8#M{EJ;W8r_nHEh0b=(GVaSp|JuI)^yi?eNK(fMMZ+!S zHD{htse!$x4%!S5zC+|Y68{&U1nIiVK13n2^UVFf5Kqy)v#Xu@tn<4v=RrdGnY#u? zAT2N6B&v&YmumBOgx99B&#}@x@Vi^Qk{Tg}e}31g zg@M^C-@jEhUy_r)Ggjj?-_os8|K(#Ig$|M71NWKZcp~)3TXw(_(eB8Y`x9iL`+Zk+ zhyCZcToi9ORc&2*o}2~Mn{Q>`i(-F)@fULhY&GFrHi3dnRmfBKZsirT^y4mRPU_0$ z;J(YEM*e!YKkStpZv+h|fH%F?gxS8Ru@_|xV~*X^)%6#u85|otHY>%BrO)^h&T-1m zKcL`~mBK{~_q-~ZDQlSMVXvB(KNo22cR5lJJGu>3`f-;UEqO5zRT}@ZWw&8BdLn%ThVEv_IOv~XCJ-J7x z|BVLj&zYn@Y|UmrZpoZ>dC_BLe$^Cd!Anl=7!L-xJ88~d&femYPiWjNCp#CfHhaR5 z>vUGR1u&Q$DE~y3V$-bCvRBGovZa12AR%1v2HEJeOm!CQ7AQJ3B8Sb|2lE&!KBIKu><%!qM!uDq;VvN+}-wnZUUM4;9x#gsH_0`*fm+8!1<< z*oCEpwpp^-kDo;E%|S($?=@EW489(6md;3dRg$apznaOQCw|aq>8k0Sm#XD+)6bSZ zjCSUftr;2nFblUV;NYNU>LpH(LwCv~RAr=$8yN;dxoG?n(YeB7eq~Kj8>Ki#y(!+~ z#{zuCbEfpuPi}o;WO#W}zHchUUnYm7`6YR`e4wq<*cA~%U0C)69%Yvw{N?5QglXBa z6PQ$3(GNX!DQo(xNEcQ^4mGvi%Cs-?9b{&$r(JDNFGN{OFz8+#xGFNfE)gW4NUpnU z_{~cB)_{1=&xmJBeRu9#?X(mXdENBs`Of!E8_Z%@O5w1UUTm+Ls5KqHd$YbEj)r3T z^MQ_Tdk311iU3o=BpSWdnw4KX8%q{oe|m4FFKhN5x^wStQHrnHfZ9SWR;l8l%vNZc z?}ZWDOLE(2Hj7cN%x0G6%U2X3qd7`j2R_HgSjd}Z#{W)p54XLiOhOwX;ps0El72F} zc9(yQ2Pe9K<=3W}`s&t_Id1;e4oQTO=2h+vG3%!Nn+jOXr!N)l1|4#I$)&ab#SG z6ARx_&eBiL0&T>*_Du>_MR?y_zX>DIqAMz|5-sq!s>`rRB_~x@_4G|7*X@n|5Qf5- z4WGb|?Jj$X-jMf+LK}%wLVqB6+UMC`tx;YoOlQ7NmKK=;?s>}h%0`>AD;5&JJc?FNLnW@<{g>H=u=ZUm;L3hinW8fE%z)*B$*NY{;{hJ9V#$4?MF1uCr zSh(la5I;T}@METm|Hi9V(JS2Eh^}6y{VfSka8Hp?I7D+!xpMgO<|Ca&%jdglhMe`N zALy5lgiqOkOksJxiRc18%gw+naPRio8k^n>?L)&kni^Zl2u?+3gmUAjmpN}2d`JD+ z4jyl^x&3~m-^wT3I@D)qLz^MTFMAKV>k<0h!ze0AV>6E9PLySDiPfDQRu*8-Zwu}k zW_t;}nuNO8tjm{hiVNdRZcd$C6)4+QDSK)0kBQet@;pJO(vDhc3{I^xm9cH&=aar)sT z1MA-tgppHERqtWwLj7Ka(zfD_;~A@Ezg|&mi565j)J%Qu#D0%qFhkBg5@zf;vqFfs zs7xeJeOR=(uL+aQU_Nclb8)p`cI_Q!c(tDXXgy#H*8 z77jNUtCDYhGUDr0EupLYba9s!syE154qugmg$M%E#|t{M#Lh%(7it&F_4pHSYo2^Q zL50N+YI(-bUM~mG=&VcPhGRe^$`TO@Bmrk~GKjC_8;9R_eB1`DHka zVl@BZz%!k9zG4Oa2ZD3Dx8@c3^!2&94SV%6rcJ1FpL$n+5Eo*qKdc;kpzD@mavyTI zvGhPM7y!L%ZH>%=YkFaj?}mTzFc4k#Mcv+=2ub#)6+8`B&i6?_z~1do*s)(~t5TJ& z-!)rOmOiNBPw`w8AomWCB}8J$FDQDnnLP(s+MH!YpH-<#bfYCQ8MVF&`VFypc^tpe zH6}N(d5gn{^JZR7q|a=WaHPN1P{EQe7ByydHp_R;(3LIa)7_G4)7>jK!XB|B$X(JN zcGyv`1@i*6){Ne=lRfR;88Y&hQyBn%gQHH%jMZ9(UeAU0JggzuZ1YT4f_9#Ey_No8 zv?mtuO~m^}?qmB{2DRz^Y5v>Uh|y(Nx?F49v-_Tu&5J8~VWjTacTtNw1)MDom7qZh zo2axkL8~anH7_IDXbBtKx31WWmDlAaoS9&eQTu2jy%-4X@PT6H#X5wm!q`Wa8%9NJ z$n74f_gh`7WhZT!f?J76HhYp7-|D)o&Ll}*CA-w%9}?iuPX_)h{;E0^W65>2w8KN@ z`K~k7jkN5Mt9A1`&aE?e-&N4FX#<`Z97YP92fAtE)W#hvsrRkRP%lRNWiojzSU;^_ zr(2Ey4m=5CGOQ}l_JD5nte23*{A9x!H{1GM>5iSOg_2PUL=zb-7}-rNTCtv9u`W$f zxy{Xk1COZ$c2&UF?|%6^^%7UW-;GjX-^{#luDi$j{B6#7i`%#6IQpCXMRc| z`OxWKp7R(dbt>;*bi;aF<-X&}J-mU!h8y&yI(}}19OawPmROC z;LrN=@66t-$VCy*qslce)dhSZ@N08cr*1LT9O(5aHdlVq_UBSBDtmke->5RNb`4gu zq|Rozp=4U=0yDX>S3XB|yUX;b(V*iOJ|ugRL80(?$b^Ry8gpm@baCv@QYuOcKDQf~ z7JW4G>{gq3lloIY3uiI0rQay$(uacrJfZrHvq^$7c@rVS$>zDg95TT1ar#e#^-2>4 zLw`;%$If=634>N(rl(AZqgtYg5{q52|Dn?NWb(032_A$)#{(;qm7evp5Kq5d({s>d{RtBDgx|7`+W%UqBHU{Rm~ImFo=C z79x++N$KxsszlCI6Z&&sftv`KaCtNr^76oGY%82>Zf zhkVTU!W}m&<(ITDK`oi6r)`Dv1U)}Va=FoonV&}SDk$QMI1!(-BESxjM3#!*N!d@MQzLrS zpRR8f9ZiAG=lMgq8I-EX*d1e1TYJ^*);DX9rYz3Qg+qTcDy5LK|B6XP^{R)iZ+6$X zDi6Co^e{+scttIvb|;5FTK8V>Hl_V^T#d!k`Inp?dNeYPcXI5%&bvfY%JmMi+V`c_ z7;4PhaeL^{%1Dv26h>1T_YMl$_hr;fX(y=Z%vv>Hwk@o-?O>mpy+iV-^dP#ns^ z(w%l{J1qKePl6iFbLWCNT7kNEf|R2>=IfIu!_yqUiD=L%cjWb=Lj_b<88u~-(!kH= z{g3@Pd@p9oCt9e11_<)g4wcI<(H+Jh1#{I^VUF(1uTOM(^?7~+>ChFV7t7HrKD6PF z?Md>|y!3~6dH1O4(F|m7XaFmTy(#LNnO|$_LG$nV_kPm{yd}GM7PC_P;jW3jS$PeM z>F^W5oi>I5B-uqsj6zSZo&yJ=HqF^$7-6+MHDF@BJioW@1eXmNSg@VQdwo`0kNJ#4 z@70P3!6=4!yKraR$nG|gA4}Hhx6nIITJ*HHjs>&c7-}%9hEm!K z#8Hnui6?OMQ_yTA-Ko`#4&qUzpy%*R5PPK-KgHSaPvg*Y2lXO4OHwuWK1Wls7>#;- z5m)~z&Bo~+@$l#o<=&?p_O$P*yEWq9aQAD{ItY@YvZC+lsV?(!m_n#+wc<4a{k60X zwxp=K=zEsEFGV==GO3Al;#qk5@6&C3Bo+T2E$5=TC&jUvOVt?j z_g4*-=itesR@aa3o=lz5F_(pi7`)A4b|W% z{z@GOinr$PZ>M*7N#-LRW1g#erN^;dLd|O&FD%f{#o&-d=A$2D4pR*^;ovE!9x{o? z3G^p2IE<6|xWqYN@g2@tH#X=8PK> z4qpd@ZW3=*Q>*f; z#DY|*p~QSzq_z;+W%DQOP~vA=q&XET=^#}RcjaP;w=REAuJnwN*27YW*wp=}0)T#F zt^dj(N5=d;=`6f>h(7#P_sG zff=;9LV(w;w`JyP5clbY0WY6xDK|pA-T8awL8^^VVqb02;|yA25x`R`t^ZmfN51?$ z2x%#6t+ilE_e|Oo5dgQ1*0&CbcQAj?8Auhi1x{GWBhzF~5W*kI^9fW?XF+$4;h>M3%aDmXN8Y6m~fWUW0{J#-jQr*VOeR8v#H7`eAQTcH^q9to5*I)=88R*nLN98J1akp+Qy@u? zr1MiC9`Ybxl*Y&m7a%niA_N5a{--%Y%?$vjLH1OoF=>$Tryw+==7<|N0P!A@qya($ zG)IcL0dpT9Iy%z&A0a||AYTQ|k^cYyAOx~!2=dj|98mxOMAIP^CekJ8kR&q@+Fo-c z0|3a(faq9)(B7IOKLLQaObCUoG$9kRX9x0)(;N}v0UTyQDqezoGc-qBcmVKE5Dyn= zvuuct8wg#YInv7mP|tx-c!JRFnj?4~fNU;g+()`P7gFH|^8KkfV$KW5{|xa61o^IO zjzD+;sd*5g5NVQp2t^nOjnN!A;00jvA>(gB=-XN&0(<~O0VF9}+O`nl5exEV)f$QB z1L%K&2ql1gg|tS#@d1EEkiBH-<|4>=DhRErHFBRHQ1TU$^bv$M)EY762V_DaI+@Z` z#So!SAYT`)ks5vgp%}843-S%r8rkCq9F{;T3Z$J&AxU3A=wz*tX955-7(}NSgwE9( zi4*{+mq94Xq`S)?d*vYCdaaRV0YG&*q@o(++p9HlPY{q_0r9ApW~zkfG=k9cS|h%K z0Fo*QMJou6&>E={1YoKl;~gOMnbrtW5P+zLBz*&+Z)uP42m$75AUgdZG`;qSgAib- z7D6!$LUU=4mcJ}Ahd+`$f6LSq#lwq2|}xAk1z@YG8-T|(;&2g_6SHA5Z4Hy zm;<40wMSBf0f9}B@kJ2YQ+s4o7~tFtNm>P=!?Z_kivY}8AUYc$bdvUnst7>66+*EM zLg#3Ygo^-V+aTjRAat4bNSg?Nw;htS4??$UkDQ4Bm^vUjC=hyBdqhGMK+*}JI0d2S zv`0Ke0hmt6_&Er@tvymE3P5y0lCD7LQ|*y$QNUa`MC(5gl6XeoX5*l8rLw^;-3;

8)ak0lgbl=UF8`8n#S0tm12gw`ZGxS#()^eC?g1I zqXA3cfI7uO67GYLuQXtT98l9Zh!z_N8L9!h$q9WH4r9jA84VW7j zbUPW6AO}KjX~2rPptC6uEd>zrL<6?L1szOGN_LCbL`w>E>4?+SpVRr%000?9h1VZX*!n6QTr*uey zDF|t;35x|lO*0@`&p}8JO;|4g`YaPdW&=WoXu|LSs7w}Q)E779WhYr7CM#c|y`U*+-07B|&!JhF$ zO`#C23=q;v3l_-_eO3%1%LXCcwP0QRP?-|Q=w}czSPOQ^59KL^Bou;>@3det0#HU6 zL<+7ugN#;ykWE@JqyTig9FkB2LJnxbcm$!d6%efk z5OPKf<{$_id{z0@a(8nU+1l9TS=nK^i=Hj(Y%KPwJh$AvG3VCPnBiS1WwlE^Cos?$ z>r?4%waY$-9BvHot*j7&9@Ig~#zAf}+OR)D(A9c~+YgYNnl_AE7&_4a5tsqF8EeDr zgrQxH5ab-l?S(chR~TB=1Swkrx%q0t=7pho%@8*@$Spz}MlS+QX@LlAg51)yVFn`5 z@Ky+N8|0R+4NDS%dbUBzkRZ1zZP>5~)TSNcb^vng)P@m@LiIWz0%(xixHe2#6spt- zL7sx#max)&;Fo`%=Vk6&eKd3>_v(-2PRLW9s%K(R5Na!Q?vbIpGsUSrJV(dq`(#Ix zMe452*d8gp;x0~z-r!zi&m=7)+Bf~yE2+U719JA-U4`64dSrqU+=V0l8@KO`e)KNM zI}(4IQ|J;EN*YOTFfa1fA$OtkB742D9~W+5KKy;K?p}IRi@e9i0-Z)n<=J?k`nhRR zy@@!aK0i6Dr-Mxx+qL zD!DwFa%$S|<2xfU_+_TTY<}*|V&IzS?p7v?yyo(i*Mp>9qPQ@jQ0MaZ`lDCLQ?V|c zM`r5>b)=3gRkXP}M_5xX$mS?+PoNxy6A;k1Hat3EoM$PN{BJ;%2ixqdv@nK|q(6Ln z0uRhB43gM8_Y{{ICml-bWizWR4u?GMJt>Up5oFmjcu7vhMqKf%moLg@J#qYP^fSfE zeaF}tomgXMnN6ojK?AFS#Zeq5y)S2PLqQ9X!E(>4Xx?kH?lKlqRJEVpexVd<`km18{GJNNh5VT?nwVG?6qMW8smfR7pg2}fd|1BRB+^lfnk!QX@5|QaNgdh{@yLj)r z`VSnpEnV5QK&g5MO1-HK7{5*)UiYd3xQv$(T%Db(3!W-;31 z3;MUpQ=Q2?rN(@?PTR`!Ta*yCHhEV9L~ zR2zk9N!F6l;cKGOPD}%GPsBZs{30EhbF1y)+uZc8SeJWS@BQ+jvi18qo;`EhcxfX$ zTSqkHrkZ|1e%?sM<4{bqH|^B5OLKP=TJ1I#M0t{ey(^f8Uj3)`lF;{w)5)2U(?HBC z0)1C`>u%56yo`5m7wj1ZSSu<~EP%RD@{a~7Pb_zs4`qeKXLuk z2~F>W9)7Ye5_b+@nqBtno}+lyx>8-x!jo73Md$cNfO(Q76mePpFFT1w1C>{DG)(RI zwxNcjv`=V0MnwzM7tqkCB>N`*cWY?z$M3w;Y(-4UapFd{vX5@fejRU1;1r#Y8PvIJ ziZAfq*4?7z9)kv92acPL5AK-{p`e_?*3Yy$AqKbk=I3K&nt!=JtLU8v7q;*iSov9u z7G?g>*)_%PYj%u2+1&1P^}g;qsPGtzy7xXqEkBt_XJM5&GxO13N}6K=y07DYa?+$J zG`4m@bo!HV2fX)45IJrHEg$zy*W7#-Msm)=QnVHn5ab~l`@(RE+UW)njc7(lKq#2T zGU>N=d%>;|@hFzV#P&^wT^G@oG|hXa2O3`sG;W{3U$qy+yN703Qb~Pyf%|bCzPrn- zSFd6m1gMWcPO%j?i#($Vo6@@CFlg0!x_gehf1E@0vjAlrDR>_35DKpJG{*cPlx>K6i7y8z;(EZ&jB#ko>`jBl8H(ID zV39^D478PJ8JU-3Q{)$(I@>JI&OK!z`XU&n?fkY8Oa1UWAe29@X=UUdM)B@I!4lH9 z&3M(fQIsxFL?8e~Ped_A&u%mE5Q?4?zhf!o$chIv`5p3_uw2GD6&A>ds|A|emg5k^9 z4My=~Wpgds;$L;_^0m($-3n*>9wBafd-)Pqi zWLc^h)wa0ifbJb_(B})PJx5BLPUEJ1?~H2Ch>RLI2gGUx3cUc4O3^k4=dZ96-(oZ) z9#$x>)zDdt%2guz7k8*Al0@Rkvdx}zP^40}K{BL7S-(Bw$q?N|_v56L7Woz9ru;_g zM)txv3xX|Soq`slIxg%Q>u;2&-BsGwUu|(e{r<8i&@64WXFM4a8Ai{iyu%}Z^(@h< z5z7V?iA533nF#xIoO8zf?HSog{h9^EZedBeCZpOG9&qe`83{S5r=!~Qp*YMKXDD(& zSR40@Y!QeEkIWT_>5cd}L(zu)FD+l|uW_;4_dzK*r<681f47BBJE*6j-~w1%=^4)n z`)=p>)Vu>w=@}7?h%=4+7Zz>Y7-en@Xe?nB!^}5EtCgN{O`P1qx@BG{MtQ%d-tVFO zGeD8m*V-cP%+7HS#W!Z&8p|;=x$UiO55=|4Jd+&C$O@Eg77u$05<)r7Y%_zh8RR%A zRnALmXcQFBVn{gdx-sgRz_?T9AInM*{=Zh@Xf3C$ z5X!5-Z{HZ@HHGhPZRMJgX~>^t(sO1OBJ-L|igJxMpr5wz(YBJ=2+~a$<^9kWUgyd4 zGA$V>qll^<&>Z9aUhZja&!ot8y2>h78I;c$DDpaZ8zZ{I_`O5qRl(gWiaX#PqRrkY ztZ2%vR!q{b=?_7+u_vbh7M;^$#Fn=%`$G6 zal4G$Wt@5SHltHeT+?!Gb&9*raX_b_7-wyr;`<{T@<7_>@U_AZv>0Vivw#dj+4FhJ zHDAs`@|JOL8TY=wcZlpd6CUY`p4xW!jlv@hPg9IDpHxAS3-T$k>Nt1wg2H;fIai#a z&KYL1Co(`p8&D>$=G^;+BBvD4Q&3z5sNP{ceD{jt4o_)&N*nxK(FRo8GTYVQCqu5S z7zcDX_CLn~#kil$TQB7W0E!%IK-m*ag!Flrai@$sWgI+4>Af1<)4qUmhs+Eof1&d- ziVPl|)7={iuNN%ckvZwv)YH%|XmNI($a?N*P}ZT$&}ZlrG$=Py_Uxr+FFlc`CVUJ) zqoBOQ^Vc0xGcE{E9oL*({-T@D?P1hwTS4&-c2ay8<+xGC4H{?Jm~wX-neMzM3j?9& zaPEZ6jRZZ1Q%abBaMCMtB$&aVxZ~4D|2Cq0ll@ z{BJ%pN;F>+pLG+soD3nAU?|;(;$-riX{TKI=WJ$_MIJQhFjByL5?SSIf;2cJBWHe1 zr3Sj_Lm^MJ@USQ!qO{XtYGwX)MA?R|4Hm)-R%d#jQU6Nfk)#_~5tEmKSHr;q*N-r3 zJZ0pf6bAGHiaa$=D3f9MDh4RD5mcA5$T!)O|Rbc?icX zMA&m77CKdu;?2WXW&XCzB>A$15h7tycxIa1u!}|rbWN=YW77Vo9E@OdXVr#9WMB}J zqq+kE8_Jfq?F4ek!kOu>i)uP$zAyFqf-<`m}#MqJnU+HIQLU>wf5pN5=;R$BC&8PkvyQIILS+yFX;4) zQ}Cf|A?Z`oCk}ZGhe?D;St<|8CPU0mFzXIw;30+_m8MwcEPcr36B#NH%aoZ~sepu~ ztZnRwemFWmIlSN=3MDPbfE^f$Gth1_0S^04NwGn0jfbjQ^kQ2_nU_rgheR zpl=45-|BHw%xlCySoB4FG{P19z}I*=c$>_aRN2Gg;o{c9tZgu*<8uYQEy(&1$g$nl z@Ct+`tK_}g5<={6J(+Eoy>`#d%*Gcm;%`CQ(L6!_cqtwyr z1qqo3aH>xFCnSHtQIXnVrW5}=cv3e{i|9I9NVduxJ~ zMmCtv5)4{uD##K@Zdus&UUqfA%y>;emA+8-Bmr3fVW3OE#pHB*N+4-|h2`|&AhU>A z(p@IO$WLW?|{zB>Ix zlL3|Rf@+e0%mRo%O6`VD9H_XGVC8`WXO;vbPr1XYbFdmUxWdX{1*KC3p#&%OB-4!8 znUzsmodH#NGxhtW$}5X^^8|;g)J-l~hr}?Vs>5*=6gydAPzJ?thF2}MHM^<*mF0BfG>9Fu(e>8 zyatoQjz?jgQ}Ll>x-1 zf|J@SPE-k2+Lq0l+^A?3moZ?EBl{7#&=|Yb578NzUbCq@-C~L;`^Gq6l}gABDkL_j z;8o|M>U6n=fA57g{mkwBrA1#hKfjHvjlIOVeyx zU@QLTR_yZ41A@DcV^3)-j>lFG$*ml`Tk)B;U`TP_;m-)+U*--;)!6}v(!-oZOB=Z+(DO)K8(R{VUe(1=<|Ti4uHv^Jx-!;|OU z=Eu}^=aZ5Qx8iGRrg^)4sFk$Wt$1sj>Gkg1Zl1tBdJ-+U6=QGngt_y*vzsXbn~Ae| z@8Ags1>{W|NaiX72UZe`gHRI74Q9WC>cmAsUh1X!Q8hcwn;0b+EzT6_cyw$fctfAQiIi4sJI%{XTsd(Iuip901n14<>%3Rt5F(nZumU(EM5xHzX12Iwqnz5?*6|$IlXKv33^*8Rnv--?fzo-Ik_~4 zOVjbh-IIyaYy+EDqHuaW|J~=kiiO49`DFLR{ifrWCNgz1cg{}9Frr98E2+j>N&J4L z{=VN4x!aqUg1uKUL+Sk;xEMeyMPFJ8u4^S}Y%6ITU4G7shB?7wN63-_t$1`=DR|S0 zhp>4dams=b+y$3XGu~a2q})7h-Q8hbKfEi%%F#Tuc2|5ylm@qXg7bJkBE&T_#jhRT zUnbXVh3M1FU_I|I&82EuDN@or$iEl4bmas*z3#Yc#irbftE<^bcU;-Zeu3up%KOx2 zd<;2=R5>w@lI6EjDx;OOk2Ri(&j6ZIR#?#kfd{eG4f#CRd>gk?>3|qr7&qXmGAvlDEVY7Y1v)Zn4wGAOx&I* z(QwxUr#@+g^Ki8;VOj2}L0Sm}Z?_QbqV=*v>!K7%S1t|SMMv%yZ-f&xPyQO(48mu3 ztb$Be-%1(WRzh!Fo~<6=dka5#E1vyUTp%u!z0^=ErMGiY>m#gLUAfDpe_APv z&`P>`|NTbXZ)L)=cGHH099-dlY)(~wHfyT)DpvIKx!*0h6?^&FapeY#e4U5_lr~4x-_kMFKC)~4``$GoP0mstK_Z;IWIq_;1oUYJLvtc zL=l}q**^0Ee&O9kMU5zO=Tp>DL2s+F=l)`%(p0XTwHtqHl>jKJP=<-EY;bkFaCqU06b zZ(4A^jqlx7!IfF9@k)lNXm&<-UPSdsc{b1P8>;}b`v)+oET&CyR9rTVBYX=Wv_J>(0MJJm+X-y&RfB zc_**Ww-tFNwC3&GjMeiF-s4~=4tc%#9R#-Ob7&Rh{jg7mr3UBJumZHr>vPrFo#mR1 zR~9sg6MON)Uyf-In^r-r3EW+tqIvYrJ8bNtZr?_@4T%l&&fJb zXmWVJSXoc`H6cxN)sx`dY3nX&KEtgYsW7J z%gME(+U(|+^YZr&6mvazU7Id^Z8|22=HzcWp3K(7L*I02YrAOokVN^My{v+Vc6*ax zxt8#L6}2Mk%D6Qc?T2M@=mkJIgOJ`2oft@q-TW-3B}|qm@zkTNc`%Zq4d36p%9(_} z;v8p@Z{-)u9S^_5;cK3v+ssM&OP($8#l>$ld40N69AyvR1(p5%^wL(|J)UfoZ_`j` z&A+beRn7?UbpXw>|AowY%gO@jFwc$UM1&oox3W7i%2Omby|Dv5b+tBrqf>OnQGONG zJm?(;&lyl?+xWuc?q~h=P1ie|^G|2dx_0f`l(IX8W(7SY+RXbLyT$%Xdgm(N{B@Y- z80W^#-wM|5Th6I*%~5s>(}fqGAL3iFy*S?Q(C%v}zp?V=VCRax5#Lxm3x1W<1fKGo z!sDz^#{+-3a*37MqKs5!wyLR3*~TkY32cPl7OgI3_2H|#U(MWVQc@y;8i>{TsBRQB zuBh=-T_eiWP`ZaQLzIQ0Mp!k7Yy5>0c$D~~>>*`KtJ6~nRLbd6l9xJ9)fJ-77&Rzr zD27twlwYU3Jay+N!A~6)$_G^UvAQ*tov3t0r9dhvQfZQEB3H_%(oL0rss=;lzN%45 zIl4;qRVS#LG41USSmx?XR@1u%erTA8I@;9TrAADR6;p?n8oe~+QR6n%JglxAHOB5W zNuyS0zH%+qq^gc!4R=(Rmxj3R&MQl)0ZJQCN`d`4)8_oUuR7N--)MoyQ4hsJi-;k!ka^KnYd4tj*2#Ik_ugB3MBqXf(h^jixaV-#s+= zP2IFQ7wR(6_(=^o)qqruj@6i9HOXoav&J}U!1WH94U3Gf!(qgUyB=+IZ8&7Hvc9L% zx7Ky4EjQU-(hilbsH{t6YwB9CZ)t#Y zs%{XawZ@wGX5YRQfAep~lzgpbY^(`h58vBqG>sZ>)hMiyj_O2Gv%NZO?d@MUKGhXU z-vgKr2fs^L?d^o4GG>U+&6Q3TBaw2a+kENjD01hxyzx21cX8)#x!jqE4S@Xlp3P*? z0=LoTZuv?vE+*#i80l2`sp>pb-mS@@;c{r%{6Q9Vmp>EEV3R>c2DdN&*lOBFp;0cq z%`Hn`bEDZRn=oXnSs!v}m{Se&{e2l4OQ|uLYRuR9SC=g0(I;!|H+bO`v)^F;*>Ogd zmn8c4ls_zEh?AQwKpeO4uVG^yIRBMl~=IP(|-5sWX+o%2_y2`(M z+OA-3J`How@CfV%*a;ShK=?JV6Kww#d`I}c5RL1!@BT$}vbvsgM|f$~TZt?G?sff! z{Jye#`piB4tq=dUSAO4Hd`(XKroSgO8Qk)8s>@GZ zJR!fwLpDvNN#M8D75aT8n6q~v*i7FQEAE?Plkx`%I>M(V7H>2_q0?{Jw2TSIl*y7o zT1GdHmrKWqn3#|N*atdDkhUH-D5kdVmdp9qXJ;c00MCkDz4`As{LAXL!(%qK%khI? zNp&n@chj%x^)D)|yv9!WW546H_tGy%pK`t?hwycD`#Km_rTL(r8Pv4D@g!54Q77$>_2Q%fmVdQj6ECc*i7mS>Ix4J0{Dcg zd8GFN`8j-dRyhpWJAd}7*Y!N35u4m?v}X<9nWwGiZIpQB$lKSwd<`%EnqS+GhVR6` z`_f}H1k=;Z*_XTVK#(ea&1p_T4ffV3cO?%fEeG14mHKvfH+fxK?H2lFzu3zYfcX&=EII9ZGzMJm^O1&!=_C`DwWLZB#}; z1M(Auek12`c`^L=SuQI!{YJxnr;rz~?E&Alp$$WBG?I%0iFkIN@VkG1-&sc`8h&y8 zzI%7w+9c3Ui_5q=a{m+SRNwh&E(edjv+BZg_&Ya0Q4RW~9{}k zXPbP)*W_Q(KFGzOsTwrpL%gf*b@`5#a{iCWnU26U+d+liv%KRX$r^fzkd(DJOI&qJ zN}+vca{9hNCs1gEk4ZV`DzBeFAJR)kYK1sU_&MTRiMHa0uX;aKtwv`H*H^IbG+JX5 z0n5-FvDR!)!u+2XyS8cJ`yWoR+cn4+vu0F*X269pIz_Q zieGC$v(%^-`(Wshr#S4YQge|+X$;_4g!o^86gU7-1l4&OtD>*2$-1Jd;H z#XqidKX&e2&1dL-?GqB&v>yF;u@@8C!T4Fb-OshlPc5#?#5e46ORmK2wBI~_(i2*H zcik;WVB2Gw%d%!~s%s?H#&q3w*mwS18;^gPi}n@MD#$lt(r5Ua_zC^)Bd`HI_Iu*& zb^Nz{?YE3KdGhJwOL^?e(6iOE@Plic2uw1`eD4oj@BJ3)lX78`Jn-KjPTR-#ljYh9oiX_ItWSULo`0<>-A{PFpXm3vS86G}nf0U( zTVm84c+?8EIJ>;>1RH(kem{RF(zss&x{ zn57u|>YZ2D=k(;D7GlW4j<9i){@1qGd|$m9>hM)X7MZYqZr4;@9}>%Z5?Tyw0n1Mr zomQCZNzjojqn53-jvQ=u(th1iYE*Bt(ljK$q~CDg@A#?TF?9J(+7MYwLmOIQH8nk- zwV~!3(UV${YD1&>_sr66(Ei)}msq*~hE~&jW#8|+`##*#BJ-D)GyT`_@BFWCdxlL6 zT8r+WRX^K z+_t*Xu8K4L_2Dc(+duzswx49H60$`v+8u{$z-+I2kZnNiRVM%ai^ckwZaejzR4q;_ z`(eXcz7~Y`{+3b_ClmKSVAt$OPOB+z_hRq7$u-wz@LQU^vNt+;Ho$M`t3UMqP5S=v zGu6q{FDw_k{(d-DZs=U8Wlr)k4L@g1lP8ez+jQ?ZYl)xz-#quLAF0TEOZEQvTRlj8 zU{81OE!v*wdTn^M!SdHN8NZBq*;M1zw3e7r-65C!&gS&5Bjl6Y!peFQUsHEI9oG}D zZn1s+Ow#XPx1cQSUG|l{*OW@V0drXUygM;QTpXF0u@_|61dU zvuDebQvbD+-!tgR^XC?l(90~#SKFGF7|(3u5;J;r6+2_N=TvnTwU3yTCLcX40mA|& zQitty_E@fc@ZRTsXq{DPA@fK3SgC>FEAM{lcZ*)k_TB47`la#3i)$WFdM84Qdug9L zw9k#|lm69ZaR#-_N9mg$>7Ne$c7|6X?PZd7&#)NYQ+vy^P*@E|&OCJ8ZodF@T}f#Y z9Kdx<@5MQ2TBZ@4b)c&XY1@rhFX6kuoWALORn3aMEWV@RyA1v(l3K|SZe zGWxn6AsN-lF7Cd(Yn9R8AoQHKG7ZA-HvB8NU%+u&1+x!&+Q-2__$T&(za4h{AGSfT z40dOh!T5RG>wllA`;@)uS^?Z5sBeki?J=$G`YP~dz6XW>+)or?QJsG3-^gvLsV~D4 zclRH)031Id+wW(@sb8PPwF~#Kz=W1|ZNy=TS!Qp1 zny<8#nuO{ttL53}cUp^|}y$GMy*?mM(IW=*IDc8q;xn%0IU6?S5? z19P+me#e==rG96ymdv!+gH_Oozd?3GXhw~GXJ#F^T?(4gCLh(c=6Bi^+CS{+LVLN} zjl)ZK(tmYrkgg{OlK{W($ln#a$kjJpJG#6M?9-ROA@uu^e^RB`aR0k{kKi$C?(6dJ z{vki5_*tg2Jqnq7z^C}#mu(;O^C86;V5f9$P+F42ceY8aU!0Am{8;UogVo()KWT^S zq(Ke;vRdv3=X!Y$>6v6Ng{``$o%CEk)JwL}$7jlCCuYNn%pdoDb+-f^Vm(6Y!(Mlp zLyxbr$KC}iX}Z+dKl~J-Rny(mAmmv%X{ij)!sU!Tep>C-&x;*;Ih*Ho??TsJh0|2?CLOQc2Il7Fz8UFm}z$0ShQ zd0ZNWh5U6%w0`WF>mMv>@^iYNlSSEuHg+PM;mRrFN+;TJ;Nfa!&wQG%LAE(;mqyp) z?ivWJY0J4xC#-4aL78q%nQl#Myf*jUMTUJj%TK3|bL575Fjd0~kL5NwbT#XTWLF1+=thJ3wW zHF0GB@$_KD$R67PU-x?A3{%-LW*h9Ohe2y-NY!p!g!eKgh{0~sd=p=?u5jBwUtg`v z&YLt(?svU&)0*#(t_NM7&X_b;Z{<=4o5iIZe#QMG60SFz=?SqMK#52#lFWH2{TQ%fBVjI!mM?lIr4U1i`H(H zm3#W%%-on&=OvGp-*spg#LR{@YdWKExJT#u>T!A~(Idz0Dm%TNo4wM^;a_B#B4!P9 zx`Nd?d>?VH;uh!4x+Usu=@YnXhqZvq&&PgoIg3x_2;m!B?z?iv4LGmMIj_f9_3(x* zw{2YR@uC>EV6*Xg7hi{4jv(u2%J;j2#+yIHzP>x>)eRo^f=uM$#czq#Dg0*iV;ws)P-Gl9vM+-|*$UzDL~1fc0~RAAiSt>CPBY0wh7h`+t0m9{&|Koz+P% zgH(NT_beX&?V9n7y~VgCZ_Yku{Ye`j|TZn$?%jtksZV+Qg>dBLt;Mi$iiuV|hNG19Y zETK&vme)1)Nt}-R%dTLH+xK&=<(Dn)5^6ek<22uAofU*{&yNyGnP| zZnDD`kx6%F`3%NeZ}M*P$*(LqBs^8%V2cGY$ey+%2l$FZ2pb- z1#)CpESmSc6pf9!^NJQNuBeeLs#}RU<5OR)<3Z%rfD(J&k1Db6A`PsK%(tnL&#;=@ zNlPD7v6$wVE0J{>3k3sZpQ^Wh6&hJ(uSTH@p$E2nkKz?s#g81hg;(OXd)lAbQW|8B zZX)%si54j1jpOY{Zh&mCIY}(~c9?vZlw*Q|@HZRfpt^&NS<_gx)yM~H$%2u%G{~w*^#UZummz0pMPuEA zk7PAD`8iv&Iy0j1HjUM{@eiZe&sG-?C>mvsK-1WV-9(;6r$AT6hmq_yL4>=4LcN5#N7$4Va{9CJustk?z1`{!oqtPXs zI#cXw;&SHV8&NGO$1|)L4HcIvwjo7LJIR*iu0^btCcc5IEF|yMZoE~&L{&!Tp<2ut zEzwLGQJFQZ&Cu^`ERAC$XG9{U8SByIhiEL>WGWiOBDpRmACtB2(L|7J#T%7#S-0Z1 zRoiclj*f!q#rPnm;#p+fAqbYE_}33(58h0zIgoz9(mt11ogCc}jI?uzMJ>3ySNz1TxOoYZxzIHKD*3FjrBG5`>6FMBm>FX z?l~KB$}yoyI$Vk*qIUh9kEL0WlSqs?SI5@)B3guMr<}JPf~{kdv+VYU))$O*#pZ6U z`OQ%)S&b)bc4yFxRRDO+$6_s2KauWH)-+b5(+4?!f;qu$uE>})5L^Ex*EJc1Ybq@* zayHFaeo700LjBHG9<^mLdAq)j4pgQ;YgFu$27Y|Wxt3vFqH z1Jp~fviWB6AjWil96{u4@eA&wRJNJ222$*hl25XYhMtyUMdzr4J;^Njq~zKhSrgff zq!&vr!sc>|a;(mtHIq`S#>VS78>P1pWNlU68Zs)a#J8a5gk=<=gDg2q{!osm98J#s zSSkXjWq^0!T-HBZYj?4#H8fGS7H}1WVpU5uJ<0Be)m_COqcJ4ehr#{}sP%eqjg4k4 zC#>^?HK4FQ6xNP{x>8tk3hPl}ttwZ?3Ts?p{VS}E1$DDrO)aRm;HRfFXIjBvCb?dOE9oDgt+8%~Mwo6>6orI;v1()zx2x+N@Z&)zx%`dau3~EO0QaA-mLjv+N_NON%vYT|L{Q zUk4X!Iy^6VW>y!Y868rV^`xC>L0t> z$WS-g)l|lM%Z*yh?koy=<(d z?doh}4Q{N@jkUY6t~b{F#(LmbD;(;GyBgzAf85n3cXi8Sx86C{LdQDkSVP^_SI64x zSeG4Zwqreato4p{;Gssms~_)b%iFs1Sd-q>tA|?ltvdH5{uUs^+WA;lA8YPoJ$|g! z@9OwNjen^B?|K73-vHNB0Q(IXByD+BvzxE>qOe*=1RVBZex>4E(| zTrUvp6M{WNu)hfQ9>KmO*s}!snP9II-v`C^NWuOouD1$SbjF@6(67bya=|_?*aOD( zhk@QP*jEO7&OkpJ*Q*Bl*ti}y*#8E5<6w<{*HZ`j?LaRc?9=0V__+Q)(EF$E3skB^ zLq8$cYY6)gxgJH(zX*F9Vc#R{iG=-qh4+?ulVIL{i zV+#6DVQ(tzTZKKXu-_H-!h$|o*h9S4>~n@a(6B!m_D;jTYS?oP`>|oKHtgeuJ>IbY8}^2CedDmF9Q2#RUUb-} z4tv;Pe>?1bhkfy|XCC&`!(MyXhtKusgZ_Qk+t2m=gPwq{Um)}n#6E-AgAn@@`rd`M zuc7OC2>lSTS0eUN#2$;-e-V2#y1tFj(-HeUVlPPS6X|+LVt+~OJqdj&v1cXrv&3GP z*as7PWMco!MsLmBcN2SZV!uw;%M<#1Vh>R44~o4*v9GA>ISTzqu~(_`{yTYq7U2_PxcPxY#cj zd+B1IUF^Y&{duu>FZT7tp1;@+*!2pAKEkfYF!UeB-o)6q7<(FHzhl=68Tuq+4`uAH zjJ=n!FEjRR#(vJ&>lyn%V~=R;AMJWeL*HraNsaxgT`z0sbB#T)U4LxoosE69vFA4S zo<x*uCrei;K?6r=4*s({u z>)#H&-LdaG_JqfN@z_fq`^;kxdhAb+z3Z{Bz3X|;TwnRi!gYd{{O*iTU0Zr`$=VXh zij(qI<}Y*R`pg+JN1^pw=GmNho4x~uft*hUGv|`MX~d;g<+KzSaPnl8LkNSjT4vKX zOtam^s&A$>Ql7>8ebR3rC*k=G!S3lenH?}4_B_gQ;7PK|asf$)^OAd*^DMLdq|ywz zY)}58`#mxT%d5%KjGi65H<#V;&q*nn9LwjaHXB)Eidl~2jtz==uFx~*eM_=%wgu7I zxMUrjCDknXGp{>xH))nl^SR0L^=3}yIm5}AP^l|Pj$3{s`t~)S(}ekTu~OHbB}aZg zg)E&;z)^JE!nQn}GvOt7k7ur*<=v6rJ=l{Z@6CmyFLeDjhBMeT%6-vS)@-8Td=s6p z|MGbI=eKVt4C(FrpMU=J+h5+kdHel$KfOKPe)r=azx%`6H{XWG|L31vpo_zScM}pU zg;VCaluXNMuu?=E${TCZOGzHoK%tzZ8%p^`4!2oL$PE-!3Rvo!0}{6qYy`oHQz}9$ zMa*+?ha5OC<}^(y!cfw`c4^4K?Igw=>XU-S7D? z9{%CK9{>H1e?PsY8{d6CZ~g0!pZ{t9`|x)^{rNN9{`B2XKb!~2x8Eky++%vokCUZ5 zwnu#IkK+-@diOZF!^s>@-f*&plQW!*;p7V^TbRg>`rvXJ4@yv>NUsOQFj0utgF@9P z>;A#n;17z7q!6tK1#(eF!-FC^DJbv31??XcZcou_4`Rf0dOwH@6SIC03nq^F;IiZ= z>pHp8$#72I@}OW>%4B<-Y?sP?9*>jfo-Fs|xF^Fs`R&PWPi}iM+mqLxtoG!zC!;<2 z?8#X-*Yj(ozCC+{9Vr9_59t=-+2D+=kGz!@PqVZ zphp8e8|dLcPX~HD(DQ)?1R62Xh>7Q>5fhD=Xv9P#CK@r(h>1o_G-9R^GmV%T92zmx zh?z#rG-9R^GmV&O#6lw$8nMubh2MZiEHq-F5eto2Xv9JzRvNL=h?PdHG-BnKrV%TR zSZTycBUT!*(TI&kY&2q{5gU!z7*8}}qY)d8*l0wg5s^kj8WCwkq!E!uL`E%*h%_S7 zh@D34G-9U_JB`?B#7-l28nN?g(1@Kz95mvf5eJPpXv9Gy4jOULh=WEPynty1c?m~e z!;u$p`9;$BRs8ay3o!!(v{Ijn})A+a?6!bKBsG-M5lCRywH`2Y)+r)%4iAcN+FCP zU3p#3DGQcY(|wZU6R$(0v=;w{fxOKxm(<5=WBltsLxD^na@`Ky-nnXXKA zW4f}CnXa3BX0oQN+_Y!X=aaqh_2jv{*Uu|c<;ir9w38oc&z`Ro({)c9Sw8RS^U44C zN?9+XTzPBBl^FdjSE1U65bLaWX1&8~k7uV$wshr#%Ojq9KTe_Y|;eTcGJkrLA@;N?qBW?0OI)sjNJ>;5p<#`;X8;9ID^gncH?df{R zHErkf5KA|9xpC-!&NGYuO`Dvq{0{PYkI?<&`qEB^m*6ogAWb@Z%x;9q)c*y{*&&|SryVz@JRgr+=)T1=@5|5F@4_UJ}1Yg zEAw2sGS^w<^O`=>k;@>SlEhNW5Q!f>4n4%p+0CbRQk?m5D`reAUBtAuGYKc@Ot+`` zk^rUQhlna7p3Ewk>@u1TXcZ1vEMW3X`{R^5P-NLzQkm21pZti%ij!3a_{apgCIl2AXlC&z3hwyNPh}6ny%n9TSR_vhVa)tB3qLf; zTFBhOb|??)6Il25b8wphOPKTTvl-KiM1)RU(5R4z0sgnKW z!3k~j3<+)vNo0rYNZLNTuEnN+9<+AHs9TcPnL_(lc_zt!=d#i=ZD|*gP?{EF6KLqE zgGp!?^e1}bGN=03LG*SK7_C)Q;@)_L0#h4UO1M*|n9$2h zB##9CqF9zumO3p{6kuc}WeH@Z(<()MuU!d37gLBXtyC0%=&?jvx(bQ((n3XnNk}s< zCao0f6nyRp8n@N#fwWlZnY7am=1aTT1uPE`K-{aCxz$GKQ+ek^r)oj0|0JEEXbFd$ zrxUZaT^%Ir)@i$0d#lO#0ecT5J4sCpY~Y*vd(U#V}(#6n^hKT5NVLo zqBDzGnAR-0F%c$`A;E{=eNEI_2rKL8 ztevwAkXA1v{J~5=t?>yREnd>G4@(FM6A7QA9QE>kimZfB#)8mhRD3I@id~|%N!&ID z$mw|{TbOBfVcA!5MwTQx!bWSlp3EU~MMv;x%ycb*%ui&H#)Lg-B#RskiKH>j4XcQ( zWLd%yC6zp9%cN80R{l-%(OkTsX(`hyFIgz5*J0CxV&k`#gHoqTiBDcL3qTUyvGt29YCo%M-DO=+{+ zjkU{`Dl$#%Y%E;n&4?n^vKHwjAM{tt+M3V5ty$JA$6UQ_y|Q*G%*qy#rneOBm9>Oo zS2lKlv$WD)Tua4vabpKSOUO?aSH++r3!HMa}pvCExX-)^VtA2>bs+@0|ffgPRtmbM5B3$s`D_oC92-Rmcm zH|N)uSG6zMg1#tYdHH$ai&C6dW)pp-tV3tQq$FnTf>jk=?KGoZ<+Q&2H7zH&&{CnI z0-;&sw7UHj6~&VF@S=*1khp9(ne$?k*|ldaR26tw@>iEwR3KDL?QHK^U)4-I@B5w= zo}aGAOY56;+AE5AZG}UZqF-BItGgO20BkxDB1KtMeU%itAXL@|B&*9PN?|(Uu65xca}#gf)El@f0+R5{`Z!G=RkK6gdFt!Wn`mRA zXr{9?0lmw~C;D3gI;y_CJXg7sX^Ws970DmeikJ#fh?J6Dt_Px^ zm<>oF47zHwES$`}`-KytSj*bU!X1SsinT$AjcLMK9tuqudP_7R^fsyRycl}3CJG^k zNvBqGg~;WZE;3OVGlm!z7u+VhH6@GOy6W^TnL#$Wp$M5<%^*g0J#a=#UBL*4l_cTW zh9L@;{SQMFOJNhDGA@NvfR}zZ{K9MvFwhBEEQL|z&AjYJCp`>Vl;e? z(qIoj5@Ie;gH*C^iCJni^bnPFqbM;w(L4x;u*b%1LO&wUJMpBm2pP$KlnhNYW8>IR zD;G_zhOR;kfhXN~(uskc%>KP+5}U*-##NS-#5VDeBov6y7IpPUp0zTexr1U-bJ?!i z>u8SkD5f*oS+Qftz4nW#X0nT|P0W{R6Gt&WCcD}$9^@Id6Om|=WpgaXO<4F!pAx0> zz++(&Z-KQU$~#Zxos+DUt&8cMkpu3sHnQBSE{w8nyD*|)s|{JmNVN9FtahfMN$miu z5KvidLq=u6$Fks=hGeVja?4gXrcv>RegCj zosAjqzzH3}^jJP_cU^2|_iNeYnYzWzFd1cWD~p}X*7=Q*vn58K7kfuWzZv(%s_Qc8 z(oAMA?v@EpxZbPT+QE1}$Kw11-aZvhna>T+*Ojv^9bZ#&7YV5=o%3Sr5x3gCEgP}s z!U_rULSvZ-jQG#=Me`m;{I^74=u3!TF?6sLI$$aT`9HD3S$9O1{{zqf*|-cD zh~zsdC2UREKheOfOW(8?x_xbkVb8uIv5Uw_;AX7}s(Bb#K7mA09SEcPHZ5OR6%j5< zH&e%9c?4iNxvCx3*hIHIqiTwv2 z4}mAm5@7a>q)C??hjK0OA4cFG6-@PcNw7kSK3XLBMF5P?ec(}}i#DOCWCq3d9!#es(yC9C(!V7NAvLH?ago;NNA*U7Uhn z@20?i$f`^9WH}2qeQzuDM_ux{EP0mrMZ=YaN11<75OmYp+a%R5}u+lZ2XW^tQ0=XlZI zZb`$48=}8P(a7em7Mo_w(N&@3++@0eeQm_N=YGPyWC9g_9C-Ohg|-#3$Wg(%?;B5tM7?~U7 z$r7%$<^yUj&Oe^30BNUiRDlUng)ER9ET;}ky!q|-B0d%CX@2`voq#K{)hw;=YL~@n z*BnZmc|x9ZR!RsxC%{%zLCH?DRInNCda7V8UZGmMutq93Z`AX3H!5bRpvGfs&4Dn1 z1262BZl%=0_C{Jr8(X3|guW!a%ak9)hedZ3U z!$9r4!Fh=xWQ)+uFx#zLG`7Av7*txzgfOZ&pq8Ob4h2@{5L*4Vh5a1qv`q*5 zXeHP}4&*k5t&D8GnOX^aGByZeG?|~hJkMT+Ri4| zPtST{@I+Q2_Q2JuSvQDv0&uNP-?H(+rt5;+nAq;UDy0B~#V6pl^L6!mtWIWUYH3|c z35OnTb{?Ljn=2d3F*%o`GA|X(bfA)yUf#IR#ZqD&BY=VcAlH*;1I%jtEmi|dc86JA zgc&8r)x?XjY%E5#%Z{9E(^+4EcLD#9$a~pT5{$aogLGsnV3r=9WoxSr=_moynhzs9 z$N>~uWObc7oz2I0NMbiWlL-u{5K)o+2!P-53cou9YGhwjQOYBlW-Vg&tBF^%`9|Z_ z+cdRhY*5(~cvqzd-W)lApxBYKP8IvWDoNOl+$0HOU53eGgB(a6nI)L4m-+wxocX|< zOlI8mY*r50J1H!m^xwJx|E*>>jJ-ZCELZpQ&Nj*BF}ZocAl^DKz#4uDvY#64E7g%v z+^J9CZJrp`h-JPKY*Z~^MWiIbq|6u9TSKaiRFyUi_8%!M2_ zqb;b-%1xbVjKS_&u4>-lXv6x2EFQAG#@MaIUbE@^nO#h6!pKqXM>Tg2H(QO7$?fW; zjyV{O+j>C;#AY!tUPYyg9of*_ie|0@L*|Gp4WBH@SQjb4PXabBQ)zqgmbL5sX4dUj zO-H*77`&f$_nw4dQIroOn_69NHKNaA_So$lW6}De$t2AdfysKTM|XzXlw^A(=19&F z;SIV2widh-*1NkdbGPD&YR#sgwY5`iQ>N(gu+cEW5N9QiUAg$G+;%L<6Jk(Nx9UY! zz73rbel+RHeW>YS$-E<=H!q{ur=l9m29zM|l^uMV;W+su$94fhWBEdTr8aC}x|hIe zIYu;bzIG4J{o;tN^e{P`0-S=vKsU6~#Ui3l&7EglPo9cbm2_^nq(r(J713GE$pOn# zB^NFwsulT0XdD9XF@6HOu;jcMX>c)tHO6*avUpV3$Ov}vJmBaCy;!4jZ761m*^|)C zoXls__-t;EmK!vpauS3#FH1$Wd02}~NAL6Y$lCdE*rKVW zxFmTaJAz1ytiBncUg&iTT$9sjJwO>xP~@6%q^&BEO?g}4xzQF8a6|)3GHT5_iKvC09$e})|ea6 z-oWiv;nwQk&SFqOEBkITF1wn9UxWDuhGT`{9?TUzbOHV%s_5al?75{84Pfb_jp-)T zO+tQc&pqc6ITf`-$89Y4D5FWrFLSm!ddh|A+2D`oyR1`n7w467T?<9Q=AH#n^0TH;xZEoK)!+C8{nE0*9MY%RB<0-OA@am z*^-7a6GEO-K%3{$>DlFk&UZt71J^yMO$i}ioygjO-v@GsG5vtW>Z0`ZL!_ul)o;pUT5$GO$TzO6bFTpK~u^%?&waX|YaRSaZ z3?_8A1mxm1oRzr(q|MQD33Xd#O{pA|y*xeubt`H|56nBLt-`W0*%s^UR;l~2=mPhelyM)q7rf2GT*q$N zC=%mqw6Rdux%XP&mJ{V?b9#i5Acd7c8*y9DBh5O{3W{&HJ!nUob)bFPaiNRbUR+#! z5!xPlFGAybK%2O&4HJ$ka_}JUzMky!06C|V)&YGth~gQ<2FXAY+bfZLO+X!gcm=(^ z$ip76wwBg?^!DNpF95HxjNK|A2GK^F*%-uKAz!QR7W|Us+MRNvwd)_3*I~D36Pj}kAD=2kT zP7ynh+UjlZ2ugK|(ldCU60n80Nf65o%=W0)0(+Abo>FiR!7l3e-Q?Rr@KX-aBi$Z? zqe=U|(E_JUy%z}Xg(#Qv*=iu2AZ2inUIs+wisaoOWgAQefkRhu${!8&gr&i31Z^v* z8r@+}nwoswC~yh+T{_Tqu=^Uoo%lOz&u+#O-fYbCI>1jl1ASe9r5MtJC8A#lvhSg{ z8SL1D7bxPAcys;FE{>m*@bmrlRYA6etv!Bk@duA$&11-H*jZT@j2LTr7+o}^EoyCQ zW<&IqwYb{gLI}VL7kL-<*jO>xDpt`5*LfFBcsGo?I!x7%>`np~(s(yf#MxUHj1IFQ zc|8PQ_7MVr4T1sY8wmcG#1_}r$|Lv&ynjUkF2L>;X77-~Q&7Ji?EBkVQ zBZAyE?S<4P4>0DUg0OCt`Wrc_B|CUAJU1xBR$JaM_QysnN%j6#l#>i#!f|_mSn~iR?6ybR<3cweTer+Od06RCb$ouf#Ac(I= z!3A2o->?c~g9$&!?#GgE8*JMup~c*u;kl|C0me(G;6JM;0gDUp#Cx*fxRVpZm2 z?i|v0Aa`zqr>U|oDPhN0$0pd=K+fxQjnfb5#3uGyXz$?Jr6TNABx#-7>q^qrNOrPC z3)qh&jWsuaUpr7wRS??^kUt=C8X)Zvgeinv;Jrx`A4bP*9NX<@is3ZT+}nB|L&jZ9 z*NN&EXl}v$az!m`j&JxIoxVS}M7S(1TdhC1keYt2uJ-_qhGSda0^$^AZQ*tw?$Jdq zO`STGFBY`35I4|V!@8jjs4}Za?!fOcMU7`1b=-6$(2Ef6z z3>xne!^aWu3jpu8E989?1v^&U-f#}y`K#}?7YX<^ppViG@ClM%uaOJU3D(85w?f8H z*(=A0i>;}Pha8PyD-ZTd1y3-jqImN5Dl89e0i_c6-ZH#laoBdXlXsyR<5s}68!__n zB^>(-$77S8Ke(XGYbf@0x%tsMVd^i&@@*=9p=OV(h<|)d^xmf8 z7jTQ6BcU}7*4}-s&U3H53`Ex~Xn&h4r(>tU=hGt6?`&t#1$wK(+jJ*$QM`t zR;Q3Jrq#R1yx3H?3e& zyfxHM4eqg_o@{8$HZ-Oi>iI&(PY`JBox$H4>ZgYM*icV4G-ewb(+#cpf=(qXT<#41 z)=)n+z+*!_+0dA6XiPV>=F61eR$12pZVmNQ13Wg=lMRj8hQ@S*pD({;y1F}qzctvW zhI-)8e{3+*&oMLj{1wJ@=rY zx3Yv5%k?euSpJU2EqrWfJm-0rVRP=zfVYPFsiAsos3#j5vki^u20tH=tGhEaZw=+% zP>(db+TR-*&*6N*FbGS}?$%I0HB^rc^<+b1wxKcI;OB!gq`EWUt)YHuaE}f3WJ6=N zA$V?MD97Cy{H>vWYH*JY^<+b1wxKcIVCOppk3aqV>GLnY`L`c_{^^uEuudVkfwSoJ z*QuvzEe5^FdzVM@Vtv=!^&6j6HamaMX9z)rA(Dg%O@t>xR5%F9fBxh5pa1;nhu@w! zPFXeC%#dpK?=;g%D{r5E_hrCW8(ResC= z_3snecWmVm>$uC`xfys?^BwCWx{9XS8ohLz*fOlMxj*N5CYWc*Fs=fZj+x9{^nDw= z%PzsX`p#*r&Sl?ia_^>N@cnfx;%qhV;@2Sp9&^02zyma5)_s=$&+;sk-R0*UEf`pl zPV~D>(N>vn1NvFyx!KTPd49@&7m6_zqVf9{{@bVp&}_M58|$JK3gmk%9?~_v$?hsq z>*oUBmiLh2e0PI`$Syxsz~_XMm^{cs)hV& zMdBMLTHsS{{PpM8pI?7|{rU2r#HT<1^7hUDy#4TBpFe%~oA1B-^y$YRKAm??j`Q~K wfBxft{N_J@{6zN8^W&%Q|MHvP{o%(y@n8S<@%ESV8p8knA8-YD)m&);003_#g8%>k literal 0 HcmV?d00001 diff --git a/research/r439-five-cycle-seed9f01/CERTIFICATE.json b/research/r439-five-cycle-seed9f01/CERTIFICATE.json new file mode 100644 index 0000000000..8f136b93c6 --- /dev/null +++ b/research/r439-five-cycle-seed9f01/CERTIFICATE.json @@ -0,0 +1,120 @@ +{ + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "controls": [ + "missing helper preparation edge rejected by D boundary", + "missing inverse restoration edge rejected by D boundary", + "stale injection rejected by D boundary", + "wrong inverse order rejected by D boundary", + "mutated injection coefficient rejected by D boundary" + ], + "exact_precision": { + "local": { + "lhs": "44468459235010318794652647424", + "rhs": "20282409603651670423947251286016" + }, + "nine_stage": { + "lhs": "4676708453903757010070537011688772133559165966010548224", + "rhs": "6277101735386680763835789423207666416102355444464034512896" + } + }, + "new_kappa": false, + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "paid_rank_mass": 5129, + "search": { + "candidates": 1860480, + "optimistic_max_net_ADD_saving": 109, + "positive_saving_candidates": 56, + "selected": { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 59 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 129, + 25 + ], + "saving": 12, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + "supports": 15504, + "sweeps_per_support": 120 + }, + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "status": "PASS_R439_FIVE_CYCLE", + "unrun": [ + "native C++ replay", + "supplier adoption", + "outer assembly replay", + "all-size/compiler and analytic proof obligations" + ], + "word": { + "columns": 661, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "directions": 2, + "exporter": { + "adds": 11488, + "copies": 9, + "erasures": 9, + "forward": 27061, + "payload_bits": 96, + "record_sha256": "10de6f93ba0dcf14aaeb0bfeaea0e35f65ad5ba22de6284fe2828a7ee0504930", + "reverse": 5921344 + }, + "literal": { + "B": 5921344, + "D_adds": 5536, + "F": 27061, + "local_bits": 96, + "native_ADDs": 11488, + "nine_stage_bits": 182 + } + } +} diff --git a/research/r439-five-cycle-seed9f01/README.md b/research/r439-five-cycle-seed9f01/README.md new file mode 100644 index 0000000000..3c699c1b1a --- /dev/null +++ b/research/r439-five-cycle-seed9f01/README.md @@ -0,0 +1,134 @@ +# Five-helper cyclic basis change on the R439 D map + +**Finite local circuit construction; no new κ.** A five-edge directed cycle on +five helpers reduces the pinned R439 D-stage cost by 12 ADDs after paying for +both preparation and restoration. The selected result, accepted bit supplier, +paid rank profile and `upstream/` are unchanged. The selected complex side still +binds. + +## Exact construction + +The source is the source-pinned 11,500-ADD word in +[`research/r439-bsection-stars-seed01/`](../r439-bsection-stars-seed01/README.md), +which combines the R439 helper-star D word with its ten phase-B block programs. +The cycle is applied **after** the old helper preparation. Using local helper +indices, its chronological word is: + +```text +helper[59] ^= helper[148] +helper[148] ^= helper[21] +helper[21] ^= helper[129] +helper[129] ^= helper[25] +helper[25] ^= helper[59] +``` + +The corresponding absolute wire IDs are 281, 370, 243, 351 and 247. Write +`H0` for the original helper basis change, `H1` for this five-operation cycle, +and `J0` for the original 111-by-439 injection. The old helper state at +injection is `H0 s`. The new state is `H1 H0 s`; use the injection +`J0 H1^-1`, then restore `H1^-1` in reverse operation order before the old +`H0^-1`. Thus + +```text +J0 H1^-1 H1 H0 s = J0 H0 s +``` + +for every helper vector `s`, including arbitrary dirty values. The target and +helper D boundary is identical. The existing target preparation/restoration, +other stages, COPY/ERASE records and frame schedule remain in place. + +The five selected injection columns have total weight 92 before the cycle and +70 after it. Their 111-row injection therefore drops from 4,464 to 4,442 ADDs. +The cycle adds five preparation and five restoration ADDs, giving: + +| Quantity | Pinned word | Cyclic word | +|---|---:|---:| +| Injection ADDs | 4,464 | 4,442 | +| Helper cycle preparation and restoration | 0 | 10 | +| Complete D-stage ADDs | 5,548 | 5,536 | +| Complete R439 word ADDs | 11,500 | **11,488** | +| Paid rank mass | 5,129 | 5,129 | + +The complete-word bounds are `F=27,061` and `B=5,921,344`. Exact integer +arithmetic gives + +```text +64 F^3 B^2 = 44468459235010318794652647424 + < 20282409603651670423947251286016 = 2^104 + +2^18 F^5 B^4 = 4676708453903757010070537011688772133559165966010548224 + < 6277101735386680763835789423207666416102355444464034512896 = 2^192 +``` + +## Bounded search and optimistic price + +Rank all 439 injection columns by their total pairwise support overlap, breaking +ties by column weight (larger first) and local helper index (smaller first). +Take the top 20 helpers. For every one of the 15,504 five-element supports, +test all 120 permutations, where each permutation gives the five chronological +cyclic edges `p[i] ^= p[i+1]` with indices modulo five. The search tests exactly +**1,860,480** words and stops there. It finds 56 words with positive complete +ADD savings; four tie at the maximum of 12. The candidate above is the +lexicographically first maximum. + +Before enumeration, a favorable basis bound gave at most 109 net ADDs of +savings in this domain: the highest-ranked five columns have weight 124 and +rank five, while preparation and restoration cost ten. For any invertible +change on five columns, the new injection has at least that rank in nonzero +columns. The cycle search attains 12 of the 109-ADD ceiling. + +The paid profile is unchanged, so the recursive moment and κ gain are exactly +zero. This construction does not enter the selected assembly or establish a +smaller integer-multiplication exponent. It is scoped to the frozen R439 word +and the stated top-20 cyclic-sweep domain; it is not a minimum over other helper +supports, longer cycles, target bases or complete circuits. + +## Verification + +The source-pinned replay uses the standard library and the retained R439 +boundary, owner and exporter checks: + +```sh +python3 -B research/r439-five-cycle-seed9f01/verify.py +python3 scripts/research_package.py --package research/r439-five-cycle-seed9f01 --check-only +python3.12 scripts/research_package.py --package research/r439-five-cycle-seed9f01 +``` + +The first command repeats the full finite search, checks all 661 formal columns +in both directions, verifies the dirty D boundary, replays H1–H5 and the paid +profile, and checks the complete exporter invoice and precision expressions. +It also rejects five controls: a missing preparation edge, a missing inverse +edge, the stale injection, a wrong inverse order, and a changed injection +coefficient. The expected final line is: + +```text +PASS_R439_FIVE_CYCLE candidates=1860480 best_saving=12 ADDs=11500->11488 columns=661 controls=5 no_new_kappa +``` + +The exact candidate, search receipt and replay receipt are +[`CANDIDATE.json.gz`](CANDIDATE.json.gz), +[`SEARCH-RESULT.json`](SEARCH-RESULT.json) and +[`CERTIFICATE.json`](CERTIFICATE.json). `SOURCES.json` pins the task catalogue, +selected result, review, source manifest, assembly certificate and every live +input used by the predecessor replay. The conditional result remains subject +to the inherited all-size/compiler, common-label/mutable-source realization, +whole-call hosting, precision/tape and analytic-transfer assumptions. Native +C++ replay, supplier adoption and outer assembly replay were not run here. + +## Open next questions + +- **Can a six-helper cyclic change save more on the same D map?** A longer cycle + could realize multi-column cancellations unavailable to a five-cycle. First + compute its exact rank-based optimistic ceiling and full six-edge + preparation/restoration bill on a bounded overlap-ranked support family. + Continue only if that ceiling is positive and the precision budget is + favorable. + +## Credit + +The R439 word, helper-star basis, phase-B programs and retained checkers come +from the predecessor packages and PR lineage named in `SOURCES.json` and the +linked README. Those inputs are reused unchanged. Prepared by Cinna Davis +(@1337isnot1337) with substantial OpenAI Codex assistance in the derivation, +search, implementation, checking and writing. No independent human review is +claimed. This package is Apache-2.0. diff --git a/research/r439-five-cycle-seed9f01/SEARCH-RESULT.json b/research/r439-five-cycle-seed9f01/SEARCH-RESULT.json new file mode 100644 index 0000000000..b0cbae6db2 --- /dev/null +++ b/research/r439-five-cycle-seed9f01/SEARCH-RESULT.json @@ -0,0 +1,2463 @@ +{ + "base_injection_adds": 4464, + "best_64": [ + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 59 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 129, + 25 + ], + "saving": 12, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 148 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 21, + 129, + 25 + ], + "saving": 12, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 129, + 131 + ], + "saving": 12, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 21, + 129, + 131 + ], + "saving": 12, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 59 + ] + ], + "injection_weight": 4447, + "new_support_weight": 75, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 131, + 129 + ], + "saving": 7, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 21 + ], + [ + 21, + 59 + ] + ], + "injection_weight": 4447, + "new_support_weight": 75, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 129, + 131, + 21 + ], + "saving": 7, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 148 + ] + ], + "injection_weight": 4447, + "new_support_weight": 75, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 21, + 131, + 129 + ], + "saving": 7, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 21 + ], + [ + 21, + 148 + ] + ], + "injection_weight": 4447, + "new_support_weight": 75, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 129, + 131, + 21 + ], + "saving": 7, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 59 + ] + ], + "injection_weight": 4448, + "new_support_weight": 76, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 131, + 129, + 21 + ], + "saving": 6, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 148 + ] + ], + "injection_weight": 4448, + "new_support_weight": 76, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 131, + 129, + 21 + ], + "saving": 6, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 199 + ], + [ + 199, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4448, + "new_support_weight": 73, + "old_support_weight": 89, + "permutation": [ + 59, + 148, + 21, + 199, + 131 + ], + "saving": 6, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 199 + ], + [ + 199, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4448, + "new_support_weight": 73, + "old_support_weight": 89, + "permutation": [ + 148, + 59, + 21, + 199, + 131 + ], + "saving": 6, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 139 + ], + [ + 139, + 25 + ], + [ + 25, + 119 + ], + [ + 119, + 59 + ] + ], + "injection_weight": 4448, + "new_support_weight": 83, + "old_support_weight": 99, + "permutation": [ + 59, + 148, + 139, + 25, + 119 + ], + "saving": 6, + "support": [ + 25, + 59, + 119, + 139, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 139 + ], + [ + 139, + 25 + ], + [ + 25, + 119 + ], + [ + 119, + 148 + ] + ], + "injection_weight": 4448, + "new_support_weight": 83, + "old_support_weight": 99, + "permutation": [ + 148, + 59, + 139, + 25, + 119 + ], + "saving": 6, + "support": [ + 25, + 59, + 119, + 139, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 25 + ], + [ + 25, + 129 + ], + [ + 129, + 59 + ] + ], + "injection_weight": 4449, + "new_support_weight": 77, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 25, + 129 + ], + "saving": 5, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 25 + ], + [ + 25, + 129 + ], + [ + 129, + 148 + ] + ], + "injection_weight": 4449, + "new_support_weight": 77, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 21, + 25, + 129 + ], + "saving": 5, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 25 + ], + [ + 25, + 139 + ], + [ + 139, + 119 + ], + [ + 119, + 59 + ] + ], + "injection_weight": 4449, + "new_support_weight": 84, + "old_support_weight": 99, + "permutation": [ + 59, + 148, + 25, + 139, + 119 + ], + "saving": 5, + "support": [ + 25, + 59, + 119, + 139, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 25 + ], + [ + 25, + 139 + ], + [ + 139, + 119 + ], + [ + 119, + 148 + ] + ], + "injection_weight": 4449, + "new_support_weight": 84, + "old_support_weight": 99, + "permutation": [ + 148, + 59, + 25, + 139, + 119 + ], + "saving": 5, + "support": [ + 25, + 59, + 119, + 139, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 25 + ], + [ + 25, + 59 + ] + ], + "injection_weight": 4450, + "new_support_weight": 78, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 129, + 21, + 25 + ], + "saving": 4, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 25 + ], + [ + 25, + 148 + ] + ], + "injection_weight": 4450, + "new_support_weight": 78, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 129, + 21, + 25 + ], + "saving": 4, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 112 + ], + [ + 112, + 59 + ] + ], + "injection_weight": 4450, + "new_support_weight": 74, + "old_support_weight": 88, + "permutation": [ + 59, + 148, + 21, + 129, + 112 + ], + "saving": 4, + "support": [ + 21, + 59, + 112, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 112 + ], + [ + 112, + 148 + ] + ], + "injection_weight": 4450, + "new_support_weight": 74, + "old_support_weight": 88, + "permutation": [ + 148, + 59, + 21, + 129, + 112 + ], + "saving": 4, + "support": [ + 21, + 59, + 112, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4450, + "new_support_weight": 78, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 129, + 21, + 131 + ], + "saving": 4, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4450, + "new_support_weight": 78, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 129, + 21, + 131 + ], + "saving": 4, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 199 + ], + [ + 199, + 59 + ] + ], + "injection_weight": 4450, + "new_support_weight": 75, + "old_support_weight": 89, + "permutation": [ + 59, + 148, + 21, + 131, + 199 + ], + "saving": 4, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 199 + ], + [ + 199, + 148 + ] + ], + "injection_weight": 4450, + "new_support_weight": 75, + "old_support_weight": 89, + "permutation": [ + 148, + 59, + 21, + 131, + 199 + ], + "saving": 4, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 125 + ], + [ + 125, + 112 + ], + [ + 112, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4450, + "new_support_weight": 79, + "old_support_weight": 93, + "permutation": [ + 59, + 148, + 125, + 112, + 131 + ], + "saving": 4, + "support": [ + 59, + 112, + 125, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 125 + ], + [ + 125, + 112 + ], + [ + 112, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4450, + "new_support_weight": 79, + "old_support_weight": 93, + "permutation": [ + 148, + 59, + 125, + 112, + 131 + ], + "saving": 4, + "support": [ + 59, + 112, + 125, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 52 + ], + [ + 52, + 58 + ], + [ + 58, + 59 + ] + ], + "injection_weight": 4451, + "new_support_weight": 80, + "old_support_weight": 93, + "permutation": [ + 59, + 148, + 21, + 52, + 58 + ], + "saving": 3, + "support": [ + 21, + 52, + 58, + 59, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 52 + ], + [ + 52, + 58 + ], + [ + 58, + 148 + ] + ], + "injection_weight": 4451, + "new_support_weight": 80, + "old_support_weight": 93, + "permutation": [ + 148, + 59, + 21, + 52, + 58 + ], + "saving": 3, + "support": [ + 21, + 52, + 58, + 59, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 91 + ], + [ + 91, + 113 + ], + [ + 113, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4451, + "new_support_weight": 85, + "old_support_weight": 98, + "permutation": [ + 59, + 148, + 91, + 113, + 131 + ], + "saving": 3, + "support": [ + 59, + 91, + 113, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 91 + ], + [ + 91, + 113 + ], + [ + 113, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4451, + "new_support_weight": 85, + "old_support_weight": 98, + "permutation": [ + 148, + 59, + 91, + 113, + 131 + ], + "saving": 3, + "support": [ + 59, + 91, + 113, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 112 + ], + [ + 112, + 125 + ], + [ + 125, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4451, + "new_support_weight": 80, + "old_support_weight": 93, + "permutation": [ + 59, + 148, + 112, + 125, + 131 + ], + "saving": 3, + "support": [ + 59, + 112, + 125, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 112 + ], + [ + 112, + 125 + ], + [ + 125, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4451, + "new_support_weight": 80, + "old_support_weight": 93, + "permutation": [ + 148, + 59, + 112, + 125, + 131 + ], + "saving": 3, + "support": [ + 59, + 112, + 125, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 21 + ], + [ + 21, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 59 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 59, + 21, + 148, + 129, + 25 + ], + "saving": 2, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 21 + ], + [ + 21, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 148 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 148, + 21, + 59, + 129, + 25 + ], + "saving": 2, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4452, + "new_support_weight": 77, + "old_support_weight": 89, + "permutation": [ + 59, + 148, + 21, + 112, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 112, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4452, + "new_support_weight": 77, + "old_support_weight": 89, + "permutation": [ + 148, + 59, + 21, + 112, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 112, + 131, + 148 + ] + }, + { + "edges": [ + [ + 21, + 59 + ], + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 21 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 21, + 59, + 148, + 129, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 21, + 148 + ], + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 21 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 21, + 148, + 59, + 129, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 21 + ], + [ + 21, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 59, + 21, + 148, + 129, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 21 + ], + [ + 21, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4452, + "new_support_weight": 80, + "old_support_weight": 92, + "permutation": [ + 148, + 21, + 59, + 129, + 131 + ], + "saving": 2, + "support": [ + 21, + 59, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 119 + ], + [ + 119, + 59 + ] + ], + "injection_weight": 4452, + "new_support_weight": 87, + "old_support_weight": 99, + "permutation": [ + 59, + 148, + 129, + 131, + 119 + ], + "saving": 2, + "support": [ + 59, + 119, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 119 + ], + [ + 119, + 148 + ] + ], + "injection_weight": 4452, + "new_support_weight": 87, + "old_support_weight": 99, + "permutation": [ + 148, + 59, + 129, + 131, + 119 + ], + "saving": 2, + "support": [ + 59, + 119, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 58 + ], + [ + 58, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 81, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 112, + 58 + ], + "saving": 1, + "support": [ + 21, + 58, + 59, + 112, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 58 + ], + [ + 58, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 81, + "old_support_weight": 92, + "permutation": [ + 148, + 59, + 21, + 112, + 58 + ], + "saving": 1, + "support": [ + 21, + 58, + 59, + 112, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 129 + ], + [ + 129, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 77, + "old_support_weight": 88, + "permutation": [ + 59, + 148, + 21, + 112, + 129 + ], + "saving": 1, + "support": [ + 21, + 59, + 112, + 129, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 21 + ], + [ + 21, + 112 + ], + [ + 112, + 129 + ], + [ + 129, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 77, + "old_support_weight": 88, + "permutation": [ + 148, + 59, + 21, + 112, + 129 + ], + "saving": 1, + "support": [ + 21, + 59, + 112, + 129, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 199 + ], + [ + 199, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 78, + "old_support_weight": 89, + "permutation": [ + 59, + 148, + 199, + 21, + 131 + ], + "saving": 1, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 199 + ], + [ + 199, + 21 + ], + [ + 21, + 131 + ], + [ + 131, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 78, + "old_support_weight": 89, + "permutation": [ + 148, + 59, + 199, + 21, + 131 + ], + "saving": 1, + "support": [ + 21, + 59, + 131, + 148, + 199 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 91 + ], + [ + 91, + 131 + ], + [ + 131, + 113 + ], + [ + 113, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 87, + "old_support_weight": 98, + "permutation": [ + 59, + 148, + 91, + 131, + 113 + ], + "saving": 1, + "support": [ + 59, + 91, + 113, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 91 + ], + [ + 91, + 131 + ], + [ + 131, + 113 + ], + [ + 113, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 87, + "old_support_weight": 98, + "permutation": [ + 148, + 59, + 91, + 131, + 113 + ], + "saving": 1, + "support": [ + 59, + 91, + 113, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 119 + ], + [ + 119, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 88, + "old_support_weight": 99, + "permutation": [ + 59, + 148, + 131, + 129, + 119 + ], + "saving": 1, + "support": [ + 59, + 119, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 131 + ], + [ + 131, + 129 + ], + [ + 129, + 119 + ], + [ + 119, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 88, + "old_support_weight": 99, + "permutation": [ + 148, + 59, + 131, + 129, + 119 + ], + "saving": 1, + "support": [ + 59, + 119, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 122 + ], + [ + 122, + 59 + ] + ], + "injection_weight": 4453, + "new_support_weight": 87, + "old_support_weight": 98, + "permutation": [ + 59, + 148, + 129, + 131, + 122 + ], + "saving": 1, + "support": [ + 59, + 122, + 129, + 131, + 148 + ] + }, + { + "edges": [ + [ + 148, + 59 + ], + [ + 59, + 129 + ], + [ + 129, + 131 + ], + [ + 131, + 122 + ], + [ + 122, + 148 + ] + ], + "injection_weight": 4453, + "new_support_weight": 87, + "old_support_weight": 98, + "permutation": [ + 148, + 59, + 129, + 131, + 122 + ], + "saving": 1, + "support": [ + 59, + 122, + 129, + 131, + 148 + ] + } + ], + "candidate_gzip_sha256": "286fb2e8b397909bd74257ef911b4a76a633e169493d481a9ca40379ae9072b9", + "candidate_sha256": "b19f7c71997e5d402003b62c7083fc115fec931344ead2667d4e736e0008be2b", + "candidates": 1860480, + "optimistic_max_net_ADD_saving": { + "net": 109, + "old_weight": 124, + "preparation_and_restoration_ADDs": 10, + "rank": 5, + "support": [ + 58, + 113, + 131, + 25, + 139 + ] + }, + "positive_saving_candidates": 56, + "selected_candidate": { + "edges": [ + [ + 59, + 148 + ], + [ + 148, + 21 + ], + [ + 21, + 129 + ], + [ + 129, + 25 + ], + [ + 25, + 59 + ] + ], + "injection_weight": 4442, + "new_support_weight": 70, + "old_support_weight": 92, + "permutation": [ + 59, + 148, + 21, + 129, + 25 + ], + "saving": 12, + "support": [ + 21, + 25, + 59, + 129, + 148 + ] + }, + "stopping_rule": "complete all 15,504 five-subsets of the top 20 helpers and all 120 directed cyclic sweeps per subset", + "supports": 15504, + "sweeps_per_support": 120, + "top_helpers": [ + 58, + 113, + 131, + 25, + 139, + 129, + 52, + 239, + 122, + 199, + 119, + 125, + 274, + 100, + 21, + 59, + 148, + 91, + 43, + 112 + ], + "top_scores": [ + 1849, + 1810, + 1657, + 1577, + 1535, + 1511, + 1408, + 1401, + 1400, + 1385, + 1374, + 1372, + 1370, + 1346, + 1318, + 1304, + 1304, + 1277, + 1270, + 1256 + ] +} diff --git a/research/r439-five-cycle-seed9f01/SOURCES.json b/research/r439-five-cycle-seed9f01/SOURCES.json new file mode 100644 index 0000000000..1bc4bcfacb --- /dev/null +++ b/research/r439-five-cycle-seed9f01/SOURCES.json @@ -0,0 +1,145 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "usage": "input", + "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350", + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "input", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/r439-bsection-stars-seed01/CERTIFICATE.json", + "usage": "input", + "git_blob": "2cff2738f7869abb58b95cc7eec533c46c4a591a", + "sha256": "252cf7c4981be1c9dcfb7654d917d51a0303a21eee036988b74f9ef436f9c287" + }, + { + "path": "research/r439-bsection-stars-seed01/README.md", + "usage": "input", + "git_blob": "188175a52bb2a3ad65c701b3bd218ae3fc0bdfde", + "sha256": "3a32ecbf886d6605eb7441c63ca934c6aab0942d0e7e570c3dd0795d1cf00336" + }, + { + "path": "research/r439-bsection-stars-seed01/SOURCES.json", + "usage": "input", + "git_blob": "8c02baa7fcc9e04abb8f7fc81299c708b3dfeb42", + "sha256": "779a4d0d1ca0d578026d0f4ce0f8f16466cc6e866b7d80193ef9e7eb2a2d6cfe" + }, + { + "path": "research/r439-bsection-stars-seed01/build.py", + "usage": "input", + "git_blob": "0c9e3253e527f3a409406797914a3aaa8cb36814", + "sha256": "15ceb1d806fcd4f903324d3c2aaf7655c08073f2bfa56bd39cbcfd49a0757fa6" + }, + { + "path": "research/r439-bsection-stars-seed01/candidate.json.gz", + "usage": "input", + "git_blob": "9a17b4920334878d6c949191f6931bd97126fe3c", + "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee" + }, + { + "path": "research/r439-bsection-stars-seed01/candidate_search.json", + "usage": "input", + "git_blob": "97f5d9f0d3a153feb2b38a39daf826d959364e8f", + "sha256": "488741d5ad803372b622495972d754ab2998a8afb0b84ef755edc337b20d0af0" + }, + { + "path": "research/r439-bsection-stars-seed01/inputs/PR1015-CANDIDATE.json", + "usage": "input", + "git_blob": "16532f2d8d4fb16fde803cecf32e3ce11369ea56", + "sha256": "388c2a0db00dbe77b67649af7293e577cf3869da7ae0d0341e17ecff2b16c84c" + }, + { + "path": "research/r439-bsection-stars-seed01/verify.py", + "usage": "input", + "git_blob": "be296a579cef6722786d589652f73662a92252fb", + "sha256": "eb387243b9071a0309e04248bc088fe6f33067e39f87d9fcd1785866020b97ee" + }, + { + "path": "research/r439-frame520/RECEIPT.json", + "usage": "input", + "git_blob": "f9feff1bf28ea44ff3d63e4b1527a0137972606c", + "sha256": "449b4c698edf4ba377bf41582c4cb8245aee6888b45e48c823270fbe9392bcfb" + }, + { + "path": "research/r439-frame520/candidate.json", + "usage": "input", + "git_blob": "f26a59896f5da6043e759f072232fb8a66c17f41", + "sha256": "18cb7f41f6451f3af3559e8c09fb323ec6d1003de82ab4f0cff5d59c070ed208" + }, + { + "path": "research/r439-helper-stars-seed19/CERTIFICATE.json", + "usage": "input", + "git_blob": "8eba4f44a484b047b82d48d4d87a356b67315555", + "sha256": "35bdbd763e29791e4fa43d99d764d536fa284e89023bb9da482d2f3ba80ce333" + }, + { + "path": "research/r439-helper-stars-seed19/build.py", + "usage": "input", + "git_blob": "c7a3a8355fa9362499ad52e2572d747ca912f0c6", + "sha256": "c14c75c73fab605ab9fc133d6c146bd3d14a5e8a0ed85db1247981c4959f9ac7" + }, + { + "path": "research/r439-helper-stars-seed19/candidate.json.gz", + "usage": "input", + "git_blob": "8b0210d8b8e9524182e5f54f9bf93c28f4719735", + "sha256": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8" + }, + { + "path": "research/r439-helper-stars-seed19/common.py", + "usage": "input", + "git_blob": "bced44f0b254eac7b3f832648ce0f0090f07930b", + "sha256": "a596d898017d8832e7bcb987fc12cccbd2c88a7ad760c10a1329b0a8ea21edec" + }, + { + "path": "research/r439-target-compensation/candidate.json.gz", + "usage": "input", + "git_blob": "7f1f188f516ca4661f419dc72114751abf3cc920", + "sha256": "ac30266144f8772ec8cd629153993aa9eb692fe745a9f95015a1b7fa88977a2e" + } + ] +} diff --git a/research/r439-five-cycle-seed9f01/TASK.json b/research/r439-five-cycle-seed9f01/TASK.json new file mode 100644 index 0000000000..0a7eac1614 --- /dev/null +++ b/research/r439-five-cycle-seed9f01/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Five-step directed cyclic helper basis changes applied after the pinned R439 helper preparation, with injection J0 H1^-1 and reverse restoration, exhaustively priced on all five-subsets of the top 20 overlap-ranked helper coordinates.", + "scope_change_reason": "The originally suggested helper-star/quartet instances already have source-pinned constructions and searches in main; a fresh overlap scan found no current claim for a five-helper cyclic sweep. The second eligible bit task is covered broadly by fresh PRs #1333 and #1662. This changes the mixing topology and checks the exact dirty-boundary identity for the new word rather than auditing the predecessor.", + "bottleneck_link": "The resulting word retains the same rank/copy/frame profile, so it changes no recursive moment or kappa and cannot unbind the selected complex side. It is a fully charged local bit-circuit reduction that may provide a lower-cost R439 implementation if the inherited supplier and hosting obligations are later accepted.", + "budget_minutes": 60, + "stop_rule": "Exhaust exactly 15,504 five-helper supports among the overlap-ranked top 20 and all 120 directed cyclic sweeps per support; certify the selected maximum-saving candidate under the exact D/full-word, paid-profile, exporter and precision checks. Stop without searching other support cutoffs, cycle lengths, target bases or supplier assembly.", + "outcome": "completed", + "evidence": "SEARCH-RESULT.json records all 1,860,480 candidates and the 109-ADD optimistic ceiling. CANDIDATE.json.gz is the deterministic 12-ADD winner. verify.py checks source pins, the 661-coordinate dirty endpoint, the complete R439 word in both directions, paid profile, exporter and five boundary failure controls.", + "author": "Cinna Davis (@1337isnot1337)", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical scoping, derivation, search implementation, exact checking and package writing. No independent human review is claimed.", + "assignment": { + "seed": "9f01e96180d88ff08d00037f7d9b9abc", + "track": "bit-mechanisms", + "scope_key": "3475f46c8358c6a9211b/five-helper-cycle/r439-dirty-boundary", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1695", + "claim_expires_utc": "2026-10-14T09:20:00Z", + "selected_record_kappa": "836330098538459/500000000000000000", + "selected_record_binding": "complex" + }, + "open_questions": [ + { + "question": "Can a six-helper cyclic basis change lower the same R439 injection cost beyond the five-helper result?", + "why_it_matters": "A longer cycle could expose multi-column cancellations that a single five-cycle cannot realize.", + "first_step": "Compute the exact six-column rank lower bound and full six-edge preparation/restoration charge on a seed-selected overlap-ranked support family before enumerating cyclic words.", + "blocked_by": "A positive fully charged ceiling and a bounded support family whose exact endpoint and precision can be replayed." + } + ] +} diff --git a/research/r439-five-cycle-seed9f01/VERIFY.json b/research/r439-five-cycle-seed9f01/VERIFY.json new file mode 100644 index 0000000000..a52063c7fe --- /dev/null +++ b/research/r439-five-cycle-seed9f01/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/r439-bsection-stars-seed01/CERTIFICATE.json", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-bsection-stars-seed01/SOURCES.json", + "research/r439-bsection-stars-seed01/build.py", + "research/r439-bsection-stars-seed01/candidate.json.gz", + "research/r439-bsection-stars-seed01/candidate_search.json", + "research/r439-bsection-stars-seed01/inputs/PR1015-CANDIDATE.json", + "research/r439-bsection-stars-seed01/verify.py", + "research/r439-frame520/RECEIPT.json", + "research/r439-frame520/candidate.json", + "research/r439-helper-stars-seed19/CERTIFICATE.json", + "research/r439-helper-stars-seed19/build.py", + "research/r439-helper-stars-seed19/candidate.json.gz", + "research/r439-helper-stars-seed19/common.py", + "research/r439-target-compensation/candidate.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Replays all 1,860,480 cyclic candidates; verifies the exact dirty D map, full 661-column word, paid profile, exporter invoice, precision guards and five negative controls." + } + ] +} diff --git a/research/r439-five-cycle-seed9f01/search.py b/research/r439-five-cycle-seed9f01/search.py new file mode 100644 index 0000000000..7af80a778b --- /dev/null +++ b/research/r439-five-cycle-seed9f01/search.py @@ -0,0 +1,231 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exhaust the declared five-helper cyclic-sweep domain on the pinned R439 word.""" +import gzip +import hashlib +import itertools +import json +import gzip +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE_WORD = ROOT / "research/r439-bsection-stars-seed01/candidate.json.gz" +TOP = 20 +WIDTH = 5 + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def load_word(path=BASE_WORD): + return json.loads(gzip.decompress(path.read_bytes())) + + +def split_d(word): + """Identify helper prep, target prep, injection, target restore, helper restore.""" + v, base = word["v"], 2 * word["v"] + parts = {"helper_prep": [], "target_prep": [], "injection": [], + "target_restore": [], "helper_restore": []} + stage = "helper_prep" + for gate in word["D"]: + frame, dest, srcs = gate + if frame != 0: + raise ValueError("D gate left frame zero") + dest_target = v <= dest < 2 * v + dest_helper = dest >= base + src_targets = bool(srcs) and all(v <= s < 2 * v for s in srcs) + src_helpers = bool(srcs) and all(s >= base for s in srcs) + if stage == "helper_prep" and dest_target: + stage = "target_prep" + if stage == "target_prep" and dest_target and src_helpers: + stage = "injection" + if stage == "injection" and dest_target and src_targets: + stage = "target_restore" + if stage == "target_restore" and dest_helper: + stage = "helper_restore" + if stage == "helper_prep": + if not (dest_helper and src_helpers and len(srcs) == 1): + raise ValueError("malformed helper preparation") + parts[stage].append(gate) + elif stage in ("target_prep", "target_restore"): + if not (dest_target and src_targets and len(srcs) == 1): + raise ValueError("malformed target basis change") + parts[stage].append(gate) + elif stage == "injection": + if not (dest_target and src_helpers): + raise ValueError("malformed D injection") + parts[stage].append(gate) + else: + if not (dest_helper and src_helpers and len(srcs) == 1): + raise ValueError("malformed helper restoration") + parts[stage].append(gate) + expected = {"helper_prep": 236, "target_prep": 306, "injection": 111, + "target_restore": 306, "helper_restore": 236} + if {k: len(vv) for k, vv in parts.items()} != expected: + raise ValueError("unexpected D block lengths") + return parts + + +def injection_columns(word, injection): + v, R, base = word["v"], word["R"], 2 * word["v"] + columns = [0] * R + seen_targets = set() + for _, dest, srcs in injection: + row = dest - v + if row in seen_targets or not 0 <= row < v: + raise ValueError("duplicate or invalid injection target") + seen_targets.add(row) + if len(set(srcs)) != len(srcs): + raise ValueError("duplicate injection source") + for src in srcs: + columns[src - base] |= 1 << row + if seen_targets != set(range(v)): + raise ValueError("injection does not cover all target rows") + return columns + + +def ranking(columns): + scores = [sum((columns[i] & columns[j]).bit_count() + for j in range(len(columns)) if j != i) + for i in range(len(columns))] + return sorted(range(len(columns)), + key=lambda i: (-scores[i], -columns[i].bit_count(), i)) + + +def rank_bits(vectors): + pivots = {} + for x in vectors: + while x: + bit = x.bit_length() - 1 + if bit in pivots: + x ^= pivots[bit] + else: + pivots[bit] = x + break + return len(pivots) + + +def apply_cycle(columns, permutation): + """Return J H^{-1}; H is the chronological five-edge helper sweep.""" + out = columns.copy() + edges = [(permutation[k], permutation[(k + 1) % WIDTH]) + for k in range(WIDTH)] + # A prep edge h_dest ^= h_src left-multiplies H by T. Right multiplication + # of J by H^{-1} updates its source column by its destination column. + for dest, src in edges: + out[src] ^= out[dest] + return out, edges + + +def optimistic_ceiling(columns, top): + best = None + for support in itertools.combinations(top, WIDTH): + old = sum(columns[i].bit_count() for i in support) + rank = rank_bits([columns[i] for i in support]) + # Any invertible basis has at least rank(J|support) nonzero output columns. + # Pay ten ADDs for the five-edge preparation and inverse restoration. + ceiling = old - rank - 2 * WIDTH + item = (ceiling, support, old, rank) + if best is None or item > best: + best = item + return best + + +def search(): + word = load_word() + parts = split_d(word) + columns = injection_columns(word, parts["injection"]) + total = sum(col.bit_count() for col in columns) + top = ranking(columns)[:TOP] + ceiling = optimistic_ceiling(columns, top) + + best_key = None + best = [] + candidates = 0 + positive = 0 + for support in itertools.combinations(top, WIDTH): + support_weight = sum(columns[i].bit_count() for i in support) + for permutation in itertools.permutations(support): + candidates += 1 + changed, edges = apply_cycle(columns, permutation) + new_weight = total - support_weight + sum(changed[i].bit_count() for i in support) + saving = total - new_weight - 2 * WIDTH + if saving <= 0: + continue + positive += 1 + # Retain the best 64 by exact completed D ADD saving, then stable IDs. + key = (-saving, tuple(sorted(support)), permutation) + if best_key is None or key < best_key: + best_key = key + item = {"saving": saving, "support": list(sorted(support)), + "permutation": list(permutation), "edges": [list(e) for e in edges], + "old_support_weight": support_weight, + "new_support_weight": sum(changed[i].bit_count() for i in support), + "injection_weight": new_weight} + best.append((key, item)) + if len(best) > 64: + best.sort(key=lambda x: x[0]) + best.pop() + best.sort(key=lambda x: x[0]) + return word, parts, columns, { + "top_helpers": top, + "top_scores": [sum((columns[i] & columns[j]).bit_count() + for j in range(len(columns)) if j != i) for i in top], + "supports": 15504, + "sweeps_per_support": 120, + "candidates": candidates, + "positive_saving_candidates": positive, + "base_injection_adds": total, + "optimistic_max_net_ADD_saving": { + "net": ceiling[0], "support": list(ceiling[1]), + "old_weight": ceiling[2], "rank": ceiling[3], + "preparation_and_restoration_ADDs": 10}, + "best_64": [x[1] for x in best], + "stopping_rule": "complete all 15,504 five-subsets of the top 20 helpers and all 120 directed cyclic sweeps per subset", + } + + +def candidate_for(word, parts, columns, item): + out = json.loads(json.dumps(word)) + v, base = out["v"], 2 * out["v"] + permutation = item["permutation"] + changed, edges = apply_cycle(columns, permutation) + prep = [[0, base + dest, [base + src]] for dest, src in edges] + restore = [[0, base + dest, [base + src]] for dest, src in reversed(edges)] + target_order = [gate[1] for gate in parts["injection"]] + injection = [] + for dest in target_order: + srcs = [base + i for i, col in enumerate(changed) if (col >> (dest - v)) & 1] + injection.append([0, dest, srcs]) + out["D"] = (parts["helper_prep"] + prep + parts["target_prep"] + injection + + parts["target_restore"] + restore + parts["helper_restore"]) + return out + + +def main(): + word, parts, columns, result = search() + best = result["best_64"] + if best: + candidate = candidate_for(word, parts, columns, best[0]) + payload = canonical(candidate) + (HERE / "CANDIDATE.json.gz").write_bytes(gzip.compress(payload, mtime=0)) + result["candidate_sha256"] = hashlib.sha256(payload).hexdigest() + result["candidate_gzip_sha256"] = hashlib.sha256((HERE / "CANDIDATE.json.gz").read_bytes()).hexdigest() + result["selected_candidate"] = best[0] + else: + result["candidate_sha256"] = None + result["candidate_gzip_sha256"] = None + result["selected_candidate"] = None + (HERE / "CANDIDATE.json.gz").unlink(missing_ok=True) + (HERE / "SEARCH-RESULT.json").write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print("PASS_R439_FIVE_CYCLE_SEARCH candidates=%d positive=%d best_ADD_saving=%d ceiling=%d" % ( + result["candidates"], result["positive_saving_candidates"], + best[0]["saving"] if best else 0, + result["optimistic_max_net_ADD_saving"]["net"])) + + +if __name__ == "__main__": + main() diff --git a/research/r439-five-cycle-seed9f01/verify.py b/research/r439-five-cycle-seed9f01/verify.py new file mode 100644 index 0000000000..0c907fb332 --- /dev/null +++ b/research/r439-five-cycle-seed9f01/verify.py @@ -0,0 +1,193 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Replay the exact five-helper cyclic search, endpoint and priced word.""" +import gzip +import hashlib +import json +import argparse +import runpy +import subprocess +import tempfile +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = "research/r439-bsection-stars-seed01/" +BASE_WORD = ROOT / (BASE + "candidate.json.gz") +BASE_PACKAGE_VERIFY = ROOT / (BASE + "verify.py") + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def verify_source_rows(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + base = manifest["base_commit"] + for row in manifest["files"]: + path = row["path"] + pinned = subprocess.check_output(["git", "show", base + ":" + path], cwd=ROOT) + blob = subprocess.check_output(["git", "rev-parse", base + ":" + path], cwd=ROOT).decode().strip() + need(blob == row["git_blob"], "source Git blob changed: " + path) + need(hashlib.sha256(pinned).hexdigest() == row["sha256"], "source provenance digest changed: " + path) + if row["usage"] == "input": + live = (ROOT / path).read_bytes() + need(live == pinned, "live input differs from pinned base: " + path) + old = runpy.run_path(str(BASE_PACKAGE_VERIFY)) + builder = old["Bd"] + builder["pins"](ROOT) + return manifest, old + + +def d_boundary(old, word): + return old["d_rows"](word) + + +def require_bad_control(label, candidate, old_rows, old): + need(d_boundary(old, candidate) != old_rows, "negative control accepted: " + label) + + +def controls(base_word, candidate, parts, old): + expected = d_boundary(old, base_word) + n0 = len(parts["helper_prep"]) + n1 = len(parts["target_prep"]) + n2 = len(parts["injection"]) + n3 = len(parts["target_restore"]) + prep_start = n0 + injection_start = n0 + 5 + n1 + restore_start = injection_start + n2 + n3 + report = [] + + bad = json.loads(json.dumps(candidate)) + del bad["D"][prep_start] + require_bad_control("missing helper preparation edge", bad, expected, old) + report.append("missing helper preparation edge rejected by D boundary") + + bad = json.loads(json.dumps(candidate)) + del bad["D"][restore_start] + require_bad_control("missing inverse restoration edge", bad, expected, old) + report.append("missing inverse restoration edge rejected by D boundary") + + bad = json.loads(json.dumps(candidate)) + bad["D"][injection_start:injection_start + n2] = parts["injection"] + require_bad_control("stale injection J0", bad, expected, old) + report.append("stale injection rejected by D boundary") + + bad = json.loads(json.dumps(candidate)) + edges = candidate["D"][prep_start:prep_start + 5] + bad["D"][restore_start:restore_start + 5] = edges + require_bad_control("wrong inverse order", bad, expected, old) + report.append("wrong inverse order rejected by D boundary") + + bad = json.loads(json.dumps(candidate)) + gate = bad["D"][injection_start] + source = gate[2][0] + if source in gate[2]: + gate[2].remove(source) + else: + gate[2].append(source) + require_bad_control("mutated injection coefficient", bad, expected, old) + report.append("mutated injection coefficient rejected by D boundary") + return report + + +def verify(write_certificate=False): + manifest, old = verify_source_rows() + search = runpy.run_path(str(HERE / "search.py")) + base_word = search["load_word"]() + parts = search["split_d"](base_word) + columns = search["injection_columns"](base_word, parts["injection"]) + word, got_parts, got_columns, replay = search["search"]() + need(canonical(word) == canonical(base_word), "search loaded a different source word") + need(got_parts == parts and got_columns == columns, "D source decomposition changed") + + candidate_path = HERE / "CANDIDATE.json.gz" + candidate_bytes = candidate_path.read_bytes() + candidate = json.loads(gzip.decompress(candidate_bytes)) + selected = replay["best_64"][0] + expected_candidate = search["candidate_for"](base_word, parts, columns, selected) + need(canonical(candidate) == canonical(expected_candidate), "candidate is not the exact search winner") + need(selected["saving"] == 12 and selected["injection_weight"] == 4442, + "selected five-cycle cost changed") + + expected_search = dict(replay) + expected_search["candidate_sha256"] = hashlib.sha256(canonical(candidate)).hexdigest() + expected_search["candidate_gzip_sha256"] = hashlib.sha256(candidate_bytes).hexdigest() + expected_search["selected_candidate"] = selected + stored_search = json.loads((HERE / "SEARCH-RESULT.json").read_text()) + need(stored_search == expected_search, "bounded search receipt differs") + need(replay["candidates"] == 1_860_480 and replay["positive_saving_candidates"] == 56, + "bounded search coverage changed") + need(replay["optimistic_max_net_ADD_saving"]["net"] == 109, + "optimistic fully charged ceiling changed") + + need(d_boundary(old, candidate) == d_boundary(old, base_word), "D arbitrary-input endpoint changed") + controls_found = controls(base_word, candidate, parts, old) + + original = old["load"](old["ROOT"] / old["WORD"]) + helper_star = old["load"](old["ROOT"] / "research/r439-helper-stars-seed19/candidate.json.gz") + reference_owner_all = old["owner"](helper_star) + reference_owner = {k: reference_owner_all[k] for k in ("hypotheses", "conclusions")} + with tempfile.TemporaryDirectory(prefix="r439-five-cycle-") as temp: + checks = old["word_checks"]("five_cycle", candidate, original, reference_owner, Path(temp)) + + baseline_owner = old["owner"](base_word) + candidate_owner = old["owner"](candidate) + need(candidate_owner["profile"] == baseline_owner["profile"], "paid profile changed") + need(sum(r * c for r, c in candidate_owner["profile"].items()) == 5129, + "paid rank mass changed") + need(checks["literal"]["D_adds"] == 5536, "complete D ADD invoice changed") + need(checks["literal"]["native_ADDs"] == 11488, "complete word ADD invoice changed") + need(checks["literal"]["F"] == 27061 and checks["literal"]["B"] == 5921344, + "F/B evidence changed") + need(checks["literal"]["local_bits"] <= 104 and checks["literal"]["nine_stage_bits"] <= 192, + "precision guard failed") + local_bound = 64 * checks["literal"]["F"]**3 * checks["literal"]["B"]**2 + nine_stage_bound = (1 << 18) * checks["literal"]["F"]**5 * checks["literal"]["B"]**4 + need(local_bound < (1 << 104) and nine_stage_bound < (1 << 192), + "exact precision inequality failed") + + report = { + "status": "PASS_R439_FIVE_CYCLE", + "base_commit": manifest["base_commit"], + "selected_record_sha256": manifest["selected_record_sha256"], + "search": { + "supports": replay["supports"], "sweeps_per_support": replay["sweeps_per_support"], + "candidates": replay["candidates"], "positive_saving_candidates": replay["positive_saving_candidates"], + "optimistic_max_net_ADD_saving": replay["optimistic_max_net_ADD_saving"]["net"], + "selected": selected, + }, + "word": checks, + "exact_precision": { + "local": {"lhs": str(local_bound), "rhs": str(1 << 104)}, + "nine_stage": {"lhs": str(nine_stage_bound), "rhs": str(1 << 192)}, + }, + "paid_profile": candidate_owner["profile"], + "paid_rank_mass": 5129, + "controls": controls_found, + "new_kappa": False, + "unrun": ["native C++ replay", "supplier adoption", "outer assembly replay", "all-size/compiler and analytic proof obligations"], + } + # JSON object keys (including paid-profile ranks) are strings in the receipt. + report = json.loads(json.dumps(report)) + certificate_path = HERE / "CERTIFICATE.json" + if write_certificate: + certificate_path.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n") + else: + stored = json.loads(certificate_path.read_text()) + need(stored == report, "certificate differs from replay") + print(json.dumps(report, sort_keys=True)) + print("PASS_R439_FIVE_CYCLE candidates=1860480 best_saving=12 ADDs=11500->11488 columns=661 controls=5 no_new_kappa") + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-certificate", action="store_true") + args = parser.parse_args() + verify(write_certificate=args.write_certificate)