From 82575f429d817f1730c28537e669e56a8016e3a7 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 13 Oct 2026 11:30:40 -0700 Subject: [PATCH] Research: certify CK grid-preserving coefficient circuits Finite construction; no new kappa. Substantial OpenAI Codex assistance. --- .../ck-grid-synthesis-seed24/CENSUS.json.gz | Bin 0 -> 24235 bytes research/ck-grid-synthesis-seed24/CLAIM.json | 21 + .../ck-grid-synthesis-seed24/EXPECTED.json | 833 ++++++++++++++++++ .../ck-grid-synthesis-seed24/OVERLAP.json | 133 +++ research/ck-grid-synthesis-seed24/PROOF.md | 69 ++ research/ck-grid-synthesis-seed24/README.md | 103 +++ .../ck-grid-synthesis-seed24/SOURCES.json | 28 + .../ck-grid-synthesis-seed24/VALIDATION.md | 37 + .../ck-grid-synthesis-seed24/independent.py | 188 ++++ research/ck-grid-synthesis-seed24/synth.py | 37 + .../ck-grid-synthesis-seed24/test_package.py | 98 +++ research/ck-grid-synthesis-seed24/verify.py | 257 ++++++ 12 files changed, 1804 insertions(+) create mode 100644 research/ck-grid-synthesis-seed24/CENSUS.json.gz create mode 100644 research/ck-grid-synthesis-seed24/CLAIM.json create mode 100644 research/ck-grid-synthesis-seed24/EXPECTED.json create mode 100644 research/ck-grid-synthesis-seed24/OVERLAP.json create mode 100644 research/ck-grid-synthesis-seed24/PROOF.md create mode 100644 research/ck-grid-synthesis-seed24/README.md create mode 100644 research/ck-grid-synthesis-seed24/SOURCES.json create mode 100644 research/ck-grid-synthesis-seed24/VALIDATION.md create mode 100644 research/ck-grid-synthesis-seed24/independent.py create mode 100644 research/ck-grid-synthesis-seed24/synth.py create mode 100644 research/ck-grid-synthesis-seed24/test_package.py create mode 100644 research/ck-grid-synthesis-seed24/verify.py diff --git a/research/ck-grid-synthesis-seed24/CENSUS.json.gz b/research/ck-grid-synthesis-seed24/CENSUS.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..b293518489e7623458ff3f21cd7c416a1b5506d8 GIT binary patch literal 24235 zcmcG#1yEekwk_H?!3pl}PH^|&!M%atp5X5865QS0f=h6B4HmqC;I6NebME`^-22aa z@BgYx%^GvAG1gprch#=$&Dd*`M8X69{6S*;?)(`;ITCOCAe5s#g_T=&m^F2U0|ysK zzLIL^H-{WIkPU(Va;BOFvcj%z(=4`>H2KgVt3S;6J+eJ$RnqA=nd`R zb-!JFH|RR`eK~u3y$C%IRT`Y4yE>!Wfm>jC&b@rzd$_RodF2rlQk)`L8XCHI*tx%7 zzTTK4$rBI~+TD10P<^_#{MOwzN&?(tutN`D<&$NhDU`}qP<{>3)`k$|$v zT%)_JRIuVPOX2s*0`I|$RgMrcyAs~K*NngR{`b#0($0?hI&V~2a5`NV53=)-Vh@@&c3(N3056bo%nBr634S zq9RaGzf&UiP3vb4rr|?{P`qmkSR%91$Fj19ga=7Yr;P>YjU?wkxB#wAHIWd4-qN#h2CPf3fs0(qB~%1B{h5=vB>!5P1e&VOc!jCK?GrAjl=Ln(WmDK`teG-^3M4vQD254Gc$r(@voc&_hwis%rC^y0;KcgId^ zNx4pTPtX3|^wDUuxT7n&vCB)S>dWO#@#ccV>oa*y)Kw(o2#$6lOTE*ZB=$n&_? z@(0UQ$?s-A%!T`poUb4k@^5P7-=xT|R^;|dx}Wz_5O-PLE@HtKUSHDXbq)zjs!W7; zk$1L{O(0_NVbF3-!Pym`3cJz$jpkCx+p|;j#N#T1Kht{0X!07B)kt38Hd@nmT+=q1 z%_j#|CSDUJ-b{o6!HHjMK*U4k66wezrKTfR7vGE%rA=`c3mq3)9WXje>o}L{IMaer zw_JRtTzs)yd`0K?$Rk;X3vvDJzKMdcNw@L^zmMYc>!tXjov=yY?@*iPXK@V}`kFve z5{Nqu&&ETg!o#?tL#3j9w4!~bqFtrJ-RZ(@G;YjLa;#8hm{3ZX&@M8bC{VkeN6^rP z!U&o42$|&{%(EQnE!>T3+%;5ju+VV`Q*js;cWB{EdPw9Gcw0&nUUrPJ(u}ckrQs~j z>CJ9?4N=wX4Dq4J%eq`%nxh($Se3Z7pfVm2Q@=;oYL%tXF zCt=-!LvlOw7?Cx92C{ItWL>xt*@arP6Yrwrx!`W2#B&i@TG#SN*#-96@-4&mauM0g z9Y-tFaC3ETXgL>Rkyojoq4;YMSu7lvtFw@35}7Y(ep#@`7Gz_2Tx9}>q;I7Hs^pYL zWXxr8aFMOH)?@PD)Ye?<^xM$#?3bbCYOhLDV394aRvT9>M-{a*6E!C|s;JbfsG6AQ z%52j#)3FoE!Lb-Wn(Pi^Qdq2BSgu~!Ttu#3MUGYV2mcXCcS`XQ8u6FO5o*n9lsRYj zUI!nte|7xAn^cjMRgoMepjU~fS4pNN&jY^?Gk=?y|dSiu}rKaU<)oh_| zkxYZ^I%@@orH18fh05lMdKox{XiEOBc=2X$Ca)PGH=g_EPj6ho-b_EF@X7Gnresv2 zVYISw)c!A3HL`rIraZ-v5%s5fZXQ`q2UmEJ*~zZFI7jTw%*MxHIQ!0AGs0XW!{l$# zSvY3xFk|$%vy&^#^D+VbKhPC02e)IMsbes*-g8+KiVju>{|rP)ugH?CxrQDuBkmd)_0&NveML>_YvA%GAVR zQYTA9Vdvx`tul0|G9=9(O;m4pf>xLiUzl*=rgS(o+Ie#`C5W1nx@SKKWiT~h!@YSd zm*ZENf;32BWhoYSlP|g$2}=f24@CK$n4r(~wYjb#I?MLN#@L*I|L5|`;3nBmty8a> zER|J@5)PN-eB45IZ8NBqTb;2E#l7nAlX+9>E~^h1u|FjMhrYN-d{Aw2v%rMY1gDh3 zcFJ`s5VMS{%s;8?0g3-v|Eqkd>nbza>701s=K5)G6;_~FX7*DJ<%?5y4UkfjGax~p z;h8KT_oxE4%WCWYGn_x^b1HRH9?eAY$uh0_qCIRjlZ)~LOx<-d+?qJzPmM^t==W9Y zY6P)<)`aUX{kps=%C3LWk0I!pTUAOl`MMHGkLO1!qi+y;t;(HKD=IJ^s)VPZ#V3 zr-Qj|M=&MhSPF!Rn>K+QnfLf5kw%Q?bk~P8b*!~Ln+z)zVS^(j z$9ze(7c!WI`}f|#>0`)*5@Xy=CAWB~_LK96agQ%L<3p!1H6&Dm#|j>c8KkorDudZ0 z9oA$NwrS%Pi)?MlY@?p3;~Cg&+sPvxHfiIcKT37284THDb$-z5{211yc8p^kU2H>0 z9aoUU)t18r>Bh7E$e@bqsH;vW3_>poia(XZRhGdmri^m(1X8W*FHOk);OSy`M`4pX zJ{K|~V3#_6Q!ktJKEyV4{0cnoTrt@w4EU_lTS`EEMST;=coW(Dnf*+qGfbt^0!%SC zMUpo~G8aV_7e$K8;wa1Fc=wqK6+%211r;7^ZyBXehV0FbeDn{$)!k9FWtW2$$de6Cm7qsNgCI@O*Wn)HA~P;H@~GfgGt;tgWG z={Vpg;Xh6zlTXjc%;|~h0Hyn;p1R_ZTf76xF_Ee{xswDS%-+xj^gGN2zAk&Bdl7eM zVCGAzjIM_GWDE6y5Hnwk(L1du9(Q8Mlb9`@$VU7kZFqbH52LgtU75QOsEaXdv&0&UfANK~=^+eYWzOakl&gUUc zJC*J6)gr8-!L&v>2ATK|sPR{VvdRW&GsiYk-TLB1>t4uMU&k<6qZtu2m*l4KlC%A- zU6^IS_wWXec15lXFPe?Bn%`&JlQycZ|BkthidYOLWDUB~le*fHUhhncraWZYMyWt` z*_9ZZNuUSuymgBv8e|8P+yMPo(dBbU;s7!Ag$B#xhn-T8fW3-Ca4|-e^lXRiT*SEQ>FPQhXZN4;ZzLaggaBaR9R!B92=YQbdR?}GRpY>nj zKf!Y8AnoR7PN@f!3bt}hV>iwaP2*?g3buMX6jnuH8t$EI(p!}?&4h0_54;lV09L(6-kQpYJ+Dt5Rvlt>0_8{ zu%l|XYp`zg`|eTeRu|sGDOZc`(`ldYWB%VAuL+jEtZ_FxdOiJqK5F`T@R)Vn9P``7 z5mxJ0XIW!xlia%O%vfND!0k67?S5Hr&B$Auf=R=RkMTa{k zKDpGsO3mJN&E7T5o3Z?Wh8kGbIKP^jL!1K5PwqE~|L^cpT~V?->7jr@O`wiKF>bQ& zKE>0NO|AZrTec^d-lg|gE?AYe%*)WoMkmio^V}BkfPSz4B>t?C?xe3o8YxyRRC$TG!qstJ;_FgVfS)~6VA*yHUE7opHM3*H&o zFhplzY?yScpZ~?5Ec3fH@5hs^V&5RYwRVdDx6)RU#n@Qln}B*QD+&*!NYiI*#uG1P zP51((t=ydFda@Z;iAR(I3IKypg`}|pKcigQj(i&AR1j9qK=m=dMZaS{1$m)p@zP{p zeX;wi4uU{0zMXWf5Q!P^@;SzI(4JV-3i9F#!+sY7CfksWdpveMa^@3-knlnc1$`;W z22T$GoZAlI3*mXYCE;|3y&pHq`5?sqLvKYx{U_4ztkquRg_!`3;|t+`sHymHhjW@d z-hp$+A2FCJD;d}*78d2W$^22#@)cN{YwsJYHKKDi4ShQqB@it{OC%b_zE>V*m3;c@ z;U?cpzSBm}iKzB~$_a{j`Rsk3J$ zadO|%&DD?r3HI6&*5j|28M#N%pC=<9YTb|~b2hiGJ&=QJP%Azec~wVaiJE^B#XmK$ zyJmFXV^)59wqTZ-+JACNJDUSq#ke4*Yj~}fpJ{l1KYEj@d^}Rc%P9KZva9d;pqe%D zT&8dL>NCU7F3>b+rK4kJV_$jFgL#&M9QowI){3?Xt`B=j3E(*`zitt`F4mbCTga&ZojuSrKnc@?y*N25?KT{(4Ap*fW}T?F66OXEzy6#; z#(bzmy1OtJKC~6Kp0d?a9u~wkw{6eTNRj9D>GRzDYbid;&-qA@i@6NW7+B?I*WpE%A!Taz3ArM!@%Vc8sTH={OUQ!O6qb@fP3e5*rVBXiu@=9gC=h0mh z9g4$2=nz3J!OCjT^;eN%a4N&0HRZ7FdfK}Z$2r7Pi(1YfiN07I>;<>};2J~YBnxBe zv%m;i4imG9#C4rDCOeXh;E#l{s8!9QIHac`tfRvJ4Lu;5Y}gnsV-sI}DebSiZ59t% z(mz2CqlncmwM<&jKT)g6MP+A(*{Zw?n`8(})!rQTK@vQs;^ht9r1 z1bk^^z~DQ`t}!a@`jewN)rrqk6U~#p*mVg@+aI(g+B( zA`De3fNBx?U&K(M0;m+Bt58`K%0lIj=7rN^h0%vnmvaEhg9LMBr$v%b1d?*y>5<*& zMX%KOw$y$QD^gix%0i`&=2_BXS461m^toy=f{CMf%Jj%e^r2E^^LL_Ugl7RNW%xz2oH9jT3JC~# z^|4H9E}P`0cQs)uAl=lHX2}sdUD~9sf#FkdYL*^m1WqU43)DCW+HG^|e!}8C{iaPKSEg4;P^+gb7NG|^sFm-Q zI)y9Ky)T%hk}Q&qklpkvbsABkOUTP7_+lEaG~@j}g0l1)*)PJbO`S@(NX|<({yvcz zM5jKd8bjnUN(QcesJ5AuV2&t)-e;+B^6f2)mJq(rn&sf#i`z{sAE67SEa5;_Ld%CKH0>?3lmbu0>|TPY%|)kEpir4yFA(BiE7OVANr4Z9E##Q^i03<8 z$zq7MVJMTBtP}`K4<|C*n{e6&O~^r5WXS{WCRW$#L%}y80#M;JB0B(sQPZPlIq>$@ zfOD-qQfM5aUN>~9`}t1MlDrr69%`Z+aOP5e1AzmNY?CMjI{Y4)2gJPFd1um|qq=UPpXRE%)VboSq$vHKF;?+0pvA zFnGEO(ZIJo_{yiDHANMh-5XE`g4ti-yk7>UgyJ%~u?P(g84zR7_tMC8jShtIx`ZnA zf-I+rCOCBLZn9(6KO0gYRW@r?-mcWOqhPaB&*6O&9fS_~%#NGU+)|0M4`w+eGH+?}`5)IO{)s_}lHsPJ;MTr2-_Liz7g zx$FpYco++osrpsLVraC4d1Bv+*iBEW8MI5UgRM;EOXSs}#25J0P8;UoqUR1h$me)5 zuo%-O(@Mz^=u1ntM;pHf$+nfkMnw$DKP8pXM~^O-o=)`GD+ z3RVNj74@pg5jr1942-I+%kNEFzg#aH;OKoE&MGbBKUxd78Y~;mET5%N6IWj6#~M{N z^$rSPE?+M(^38{mpp~U~6@iAtLPx=-{IN3yfQK<+Mk^!>n8{>C>yIX#?w2ig%Op|4 z?(ZVik_tMK|6yPG98=c~>m!jRgRUHeM%m98u4FH&mI%*D)DH~jOCzsEj5mZQ!f%SNUFT3!O3YP$y_d7Ob5|!ha6Jlv9G2nXZQhVSb)TP%H^+m&)ZLZ>Iu; zqw&WWI);_VDXB%m3k2+wnXy33!YKPNJfGPEenDbTYJ^czhLIVeVyIbC=-3Cd#Xtcz zQ%T#!Bq&9x(8be8yT#^B1Jb?vEvbQ$A^nO*UgTIDqEv(lAH&rnoaUglvEQqOw?-r` zCLKTW_(|8kd(TujK|S0UXCa5ASGZ4|TSu1WYWg6ALi+e6zzOkPUq7W(gna-zkdlf< zx;1Vv(`hoe$6QQ;LXA(fmm{F!opbcp6KM5K_$_J^Zm}+m=@2wZ#ls8K+Dig}vqVYv z<4}bn+8vh<-%UyO`y8|r?<2e!1J39}8b87Jeu4nEJ)=yKszh|Cv}7!3cPcdZfv}GE z;PC5k7_di63*sS+|B4w;9*fC46KiQNo2v<#rx`WPAa#gEaV<-F9f9sah2}v8@YvhV zr{oJD=Z?s%9cqlAUuKXx!J@d8CB2P6_Z$f8H0sxX*RRiJR09nT!y3I*jJBzF>ED^} z2zoUkdo`oB82q;wAhsAZ3DrgwrUmNtDzB3wm&BYWve1wPXJBb0p zb)!jZp~-8ZNo(~sMX}bQCv>wuO2H?Kz++QD%aKCM0ieeu`SXU~d3LmQN8vL1<1$Ji zC5s>>1CWvt%f#X_Zc_=}7=rd5QScpq?8DF_qxelw#BN7?{Y{jt;8VN*sn$6oEO_dU;K{DU?ht2WAn39oRdw0{Cz@Mo6(;lT0+9MWA;$)Axfj7)0D)p?8x z;@WLy^-hNMgy|!*{v!?+)PMS`;~5nwwA-lbofJ$!_`|ataYfd|a&rR7#qNyiS6b=& zbsQ7MApD_Oj+i2Ae7Pl#-TbVl*z?1jOyRC(y8k> z6u?6NEJs+8HHzFEVRA7qqq-w_salSS&z9+ZDx9H3mMC%ygvsT+jFOI8<@>d2|5eyX zT57-a(9}O0^{ip2S=HRIdIS|zq$sePaYWINF6Vbp6+|frx7?`e7qsR_DRkT9M=^~q zCwM6y;S~C09I@|FIx;J0%CR?74l#`^JCWx%U?XRYv2$e!nBrwH*Nt3u)?jooZZ@?M zwhk|Ie5f7fHjiI2iC-#ItaQe%MvssjET(}{AJj0lQIE;U?m1kEVdk%9XIP*d2S40$ zSWAym_=I)Sp`t685v4Ho1q?Xj9K6OebC=8qV!**gQ=7Ktma(U*G3)vBZGf$Y7yumeaAw zdS7;FIH@?E0f?c=hX!6s4}W`PhVFF?`!8 zRnHMreLr@s8gk9|E2*WRL{SoGD{Ip@ zy0pneBz7wH(D;lf9bdf0eA2)Sh|)7L^V5Cuo3BeJlfK{+Y(!+uU+L!L-iK3YDg|ZLl4fDzC8(Se- zPN#<9f5N9!DaN1+lsF0ueDeK~^lBpcW+6ItYa{xmv?IiLNb>qpn@gZQjcP@KUm9(Z z%awm>=E~jPzOp`XYUkqG(4Mire)8W$-TDS(0DVxx6G7m!D|yb6zi?f<$T>N8ukSn1 zbh-D+8O|QDmhWPuFi7S|W&}{OUO!ZhNA{MjW(Q#x%s0&F{AN0j|1q&(D z(%oRl5s`;tHsO8$Uw4Wz(-^DyBcI8|*KE1rt*K9uRQ;2CrUT^Q-xbQ9A}wP0E#dCC8qo8vyRkY_OasD74Q zJ0_1i!u#SjCY~F?JDcyC?OY0~Te{77Eqc&9K5D2|6{w*@39>I2`SdJ#Da1W}?2}D# z>j)(&RN`S9#S31Lcfq>kcf_FAN^r?L6i#&PcpeF7}EiN3H&lIbajY zE|)B4u8sYbGI3#mw}PPrDj@{?OEYR2Q%IKM*v1}`c~rlhIh(|`n>aJTTfksEPL~(y zD5g1>iWA{Ac`(X@Rpe-|_$Qk>+E4C}-czW2*2w(UDlnLd(6F63wl_B<8$VU1C&X0k z)HIa_wx_bUW{3|Ym}A*W1ehn?!GxlvUglg2xS<|wA=$fUM#vuTWcKelLaiS-qNMyW z^fG@GvF#`R7~l<-`)g;Fe6@^fo$(eb`3h>}np*&8%P8KY#i74?nHa+)ogTh13YN|v z#|qb>d^!SbK}mTf_73m{${oPsU-AYL=m3$x-d!(p6|;(|H`u{)YnuQWft{_qc}W$p z8`q1R$DE*qbAV)b=oJ6g+7d60q?`jUKtP|R3~LTHv!;+)_qoi!UaX18`-AEC|Desy zKLglc_K_wh(;-wF1nbl zY};y@Um{7lr3jCXs?gYAjyj@7kC0_Mqsotv%R4m~6Ckk5FtA3#BAn2$M*Je?-$j@} zOY*@-V7>!0m~`(kL8P<^5SV2c7$affPG}f(?=e86)GCzJDt~cSRK8GJzEI>Z2Bu2K zr%J=I#UrIkXT?cNNf!pjNyo=Y!;!_4lf^^+MHDe|NilMmzep4$5fLQ82OnPnAk2zlQbHl9 z(7-34LxV`+6Cj|=FrY^K{O8~KV*>o=;s0W|pNWXb5wr+9fYf=L1ZE5TEcXvO{~&?s zA>sT7_K*NiNP&ahiP3s+BGW{YAyC0>D;*)K)=m??;8eSjFgJymtVh8qI1Z)|?i{W2R{y@wL?YS$XEZp!(vY`cCX*PX170*tfP~ zYY5V;_G6K7>}v0M7NyQ+*0^#r@MksdY?l(GicXZlze#k;4N9Kx3BrMtv%>C+tajC7 zm6kM)Ya1k0j}|?`4^-oTEwe^anZYeAW|P)7j!PdT#rod}R``L5oUmnqUB%#yp$D^$}DanIh(XSR3Iidt8}x!D8l#Fky&ZRe=;jjn_e4N^@`65~(_y_lH2k$a(I)!IWFxWjDAwHJF7Fg2kkgJppJ; zq%g>##neQ#xspJUfI%JA40Nsd0wHSA3gvlPDhos{fF+~FD@BusKb5kM7&3le1`D>gXEk&B=iEm1Ko@MTH7#-?kG|^R7}J?UUdouu|2s48 zin1)~htr^hGk&pVMHw12!pG9-eh&Er`u}Xj8K+ap+(;BVQqya(XMIqX#8gvK9!RqM z@-E3q85tKVI_;K0RUJR6PI*1UeRSX~83M=AeE6t*LGz?Ck@ftwEq!9}4;}jc=v5u*q%Jjl`KEs55=FI2`GpBJ z6e0*p8JHz>2O4@%44-R$x;;I6N%=MWf|A;uV(_J!Hc4J?q}5&7a?T+DJz_RY7!5*D zGAOWACLu_PbRSX_pB#7M9hB%AJfwnz1)e-DqLBd_BZZhV^)DXsxYl>~=+4xV66j)a zXbqHN12D?Ut>S@gQGI-OZT*z2MZHXmvLd^i12tNY} zc#1-;05R!+WGd+r_{d}@KFKvs$R_j^CJ5=EWqarh3O-;!y3Y0{I%_Pv=Q}s%{&P9N z0ky1QKxPC_5HvI8?B{?>n;^RC`vH3ZfB>UV9X^;ciZXx(?9IV{msg641xyr<4aLpK zsD0Y?qo(y2U!QqjiL}{;ZpFS#`KH*6b|J51(JxI?nkc2l*;|Dknw7go z5dRYzBvt7OIgXa!he4?yM)OH$Pz;ifZ7#k(TVz-)!82qR(egrDP8+_ECP+~1tbzHx zM77W2m|xiGR9h^e3!I+|B*`PH*YB8j!a|Cdf8SCddBGSha2LCu7s$)(#1MMEQauhr z$-?LmZRQ@ng0tHTbfGwav-U{s06wg}0#7=>#s6~#$0s6#rKj&96^X3PXI{tcNsvtak< zq22tZ--!xjy&1Ijhk#0$fJ!{k#VAs1skkPQI8KUT9nxVP!0_t8hk~cf!~AWxn-3xZ|0@?l)gRwaeCy3fqrS-S)rUUnYF3|0;n}=OChUw@+RGn!g@m zkRGC+9zWRqYY~alv!Z*2WEwUor8W<)2L84GO3N(yh{Z_)RKbrtXN!pG&f%wS zq%}Q)7>H`g#<4nGY;&zMXSvE5fxo~s2YBcDy{J6~L5kHE&1W5&=heImYv9gOTX7Ai zg26F<*CIrhi^aVT-2H0aFYAK?G`g*?d63V+hAm3^uaLBQv_RjP#a)>0MNaQ3%SWB1 z^Cpz@Ch@){zMdr%i8&I!lL5)ic(>Z%gUaHO|QT*7zNZ9Bx%s=Q?v+O~t*| zK*y!@{c7iE;4yytBByhe<&npq9#Et2vSND)3u0IKNg|Z0RiYG?o7^!j&nffyQ5W zGH0nMvyuv@V|({)ZhnN;IPx+%ik<6aYw?r&#MYmxKAgRo)>!V6x6B~!(YD;3Qf6Nd zzaZVjMkYo#p$;S=Va}9JpJ8gl=RV5L1(eI!^E9CG((bb6bS(s%euORmYWiu9{8!U& zKT<6%$!ga*sZO2OPGPXPB*H_#%$g5u|NS-nGzYo<#q`4`pWS;|+~Zu?<1C{>t4gtO z8O|SYiq<~HZ&>6st+E`|S&C~yiE9!UU*r>6L_r1%^^2UwRhEM~OJPkYVNK!`i+rSu zDA8KS_;rh%pQ|i?=q&j)RYO<t?_FXIrOWnI&|jTnu;&1fO8A!#TCxT zn#cIni=4Vumd!d#7ELG?P2vR$e7OrK(Hh72Rg0Y3RhIQSONLD-hE3vu3w(YHD99T8 zbS7wJ%nrzYizP|l0l9IxoFxD|=EFtI#%C-J8cGXGr%f*ov$i@xrz? zP7#WCI)24i)<-nW)!}dx8vJ*mUz?Z-MWm=n0C;ev6+f*M;PGo*PEi9ZU>*REf-7v0 zjHuASEqucp2#-6MENqx89GEOzf3grHj_DOvks+e`YiN-f*iL|Ht-fS6Wj&j+t4v_X z$NBDAQdRaWIy@6u6BG(=yqkNDLtaT(ZYc7qUX{w;Ri?CSB#lty;A>`J9@L3_K)L}C-|r77eTlN z`^R1zC5;bY-Ymx1k;kx7V7c}W%@(+uhI$Dsd+U^Iye1=&LqBq)66-`jKhh5UDnb-c z!}PG4@CRmHo0_lngY|M=ujW2nqu#njtUhDD^elS_NcJ7%uKGpa$*75Dw|TrdvBmEa;;ahsd}0-5D`Lc^;M*1Z8|Q(JI* z;=ThfhkNJB%&U9K%*(p~Z&Sv-b1wQzF5Z`>9Z!Lyvzr~y4yjYlUC)mEQ|DcR{ybf# z2Uy!fjZa;o_-zY`EGJHT1VMSawhzQ*PwFA+igeI)71KuMf%Hw%+DGc+wLmMw)Tyjo>%Bwn)99_5fyC~wlhY3+1Q>omUSg99;%VHo;o(`b4Fv?*co??%Z()i zgMv(pw~foSB?H8|IySC!i$z)~M!<*{pj@4;c*Jjh*^|10{tzOnMVG|omV*9bA}X#k z+B(yZ;Z^*yHb0ea|VVy77DRGO0@#2iXgd)GF2OT1^@o=8GQe`5ds1=apse9vm| z8~s-*(N-$zX{(>H6gYy6UHpvoKbpkRCYBhOKV~408k|i$C*?4M;@EfZhnQVBNp4m&8AmVyYhmv^D8WybE>={0h|o!+ z#BcX84aX4-<&U8UIRM7`oADt2_e6OOr$shB^!{v!er!`U7D1tU>4h4Q#v0%W9}jiC z%GPSd^u{6ez{^2Gd_cXADbgtd;9T+L{|J(B&B4+dN74dIr$%fwXSwJ(kx`Qr5nTf* z^we?^1LGnC9bExiaa8}@$#^aAK}SijJt;dNFESv|z0HMn_2=xUXu?GXDggt8`Ev*Z z@&K?xKEot*V13}qs5B0(G=2>K{zMc>H!l@EH+4yKE!YTOj15DC4ZMqyk@e7S6*2-3 zBEsDp1_G*J#ufSz<=hk&N^+nltu>J(C-zf8&zEm({PAoQ@ofBYY>4q}1o3Rq!>L5W zsaZX#(LJeBhU2h?<6?&6vWDX#e``g(aalci3T87HW;3$CLHf4_Gc$VQ7szsW#xo}4 zl_RM;@d~(CDCpMd1EYiEJ%dO+gX8JZ+J4b#Tq~*C4QvFpY~Rd`vrD*_4G@3GnSNdC zGp3Fnvhf>=!jE+~`ham#L*+xBv`J|a(;&{Lk^3%?S=0bG?ch|qMyAhdP(gOz-9>OB zf0CV>7fe2e6cw{`r|kULaM0sv)=GnrrAW|^`B@pob8V&Pj;dp}WNmL5nfy-9-rJhW zE;f1Pnon;n-!z#?$82%ztFtv8%CmqnOCMGzQp)#d0U4IQq$*RM^Q%<-kTDNDX4?n% zd~l^Z_H}g%W0zfTRV!qSVC<_5bDv}@QpzbypJWq~xfLGsx_*e<_ZI5BUvW&$ne%x2&uK;<+tjvW6UY=HuDU3)8v^7pK~a&cD}LoG9O_rkH#&64 z9u6WZHhx&HvmSvV67i`WVN+yQE&JkCD11|7yk7BBLp5-nM5`L{x!u(OiRfi7Mm*@O zo9Xoa`VjlT&1Ai8 zHq$?Gbq&lR#_lUCqh$JCb9^O|8UrHdvh& zJ8#*g@7rZRS@+@Nbz+-q&8&fs@9}k{yxHTYyd(G2OH+8%iA$t#jn&D%`y)chm#-eS zRg`kuN1spd+aFj3)0vk^HTNRcZSdROv-LOIOpt(Cg+OC&l10_I-<3jcy292yFT2Gr z7te1?#6L-LPFf4{8HJLb2IuSvLN~br*Kae*COSaUuec{_g5XX4b|J@{w0F!s$1K^z zz84%X1AU-F=A5^0zR{+ro>%pu#1H5D?E7xMyT5O%-Y*Q3800N4)5<@ed ziT2Eb)2V2W4Jst|EvexUHgqLF)Ht5uB)}0i^+Qh=0#v0fYtJJJTlAX zZ4^jGaJoc+tUMv@IRdBO^Q6~A(93m!0K}Y+elq&YRro<4Wy>*^jST20d{tKZI!KB1 ztE3HH22ZZa9=6A$<5^LOSW%bI`G$ZU12gbf(}1h5M0tq)IId1eLGBiQ?kzEZ7{t0( zjd5|9@jmzd8HhNMFnS|LChYrTcv4OxiBi6>`Noz>d_!V-Lt@y~GN_U=sGRa+BsaD_ ztR4ZAXm{2g0W~oG_?Mb8+MVZaY3HY(;yiigpI5LNv`}B4UN*c>ck2SKI6rvTX-^0x5kE|}q5qKRhr}iX+ zlPa14-<$O{W!kERMlJ$vcBmi8WLBuGSE$Z%N$L}U^-{u#MAzc+^>T}cq4cIH#WSet z`6LNa!W`i~hxjkkl#gWA*WxLMq5jI#=g;(^XwK!k99?thvIJGQPN;W4h@5@zrC> z?bT8Xdl7}lmDiz_AXM1v(0mYT!Sbb_&OB7ahuHEJETs&03w0~>v%yzU&G?-2E$99)ni|4H?fYAh32F9+;ym!CkNa3%nUhV30W)j>T8;F;&ff_WCa-Ko@p6LBYYp-=mNBCp9xP#Ct z4p}B~g02@=LJmyq0G60v;MW!i2O}xmpS@~X2~y36DLY%rho;~Nnn5?Es6uB8nXi{= z8XP-s25Gb1=TouGPM*}DRmoXF-Uwtykg4^`&_mngl5;?G&Tx z9a@(u>aUEuHFitXUj*P$bLcs;C;X=I7~9-;_%2(-t)GNj#{dJkd+`6|5M2f^Te{qU zE@!B%_MKD^|NVwB+$Mp`d1rIrSu}Xm7*#9E6~n|PPT0gwOHLnCFjh`Fd;@a|epi+@Eg(t&BTiFPSpFY=MAk+z9N zJ8tt9!DIE;P6f?WN0!%x%c}kNkBJjwPZwS%u1ta}Hl$$(;{;Yuw#~G9|G1Hb_!6~Z zfTDrclYcMh4f!9^fBd6pVYWscjx<3Ng@L%)9u8(oD%cMtXB)-pEmHwaI)3?4*X$ zE?ew{iwr~Mn@#A5@)v4pwFwzD#e9eNN#9B{CH5%kX_R@xNB=8zL_np?`M+oj+!Fca zo1Ee0K1-D4x4^*C$GeFqzkAKlqOB7p$8%X=>(AC zy?`i$5{Q(5NKHZ$jC6QM^m_06-uL5;amLKtbIrB(K6{)W8RzUJ#%CDcEjnCWkW?Hu z_vLav$+^se=bBKjZTi(0UpDi7@0Qi7M81*h``tZQ@Y-fZDyhc$CT&wmNJOIP;?cpa zEUVo2civlb*{!Dk^~Q~YdwQ?+$>>jrbkePLU$N}siWJ+_iah*MJeuq1z7kSaC*S!w zGw`(H%DIgoL>ujaz|xv#!QoFT2&{$zwxW)tDV} zKcxt9qLjlo3NO{V>rkr4&FhTcxM%Gnp|8fxjCG$Xdu>Qq*|cdhrLGWM2F3+rl$I~v zOO&NwVN7d%hwutj+QGP{$cLU9Z|O!DhidFJb|dQ4>AgNW4G208O0O~4>J40t9%ZXd zK)~o$_I{s#|JYiPp|+bPN@@A@JukQ>Ul2pB8(cFhXnDg0u4xC1ykay}ee1S}ORy>m%YXcz%n6=uw4wDisz-eaa+wh@K+HzMZta-rlIFB`XA+WOF?-sGlhcUM;8c|xNnXVIRJFo$L1DoI`4)y)K@GX!2J&{)tVRgK9muY~B+Y zl^1A5yuPp1TpwM(RTZt|1)|V(vNM>TQ;S*$$dhSDntY?YhF1t~xpz56IZ5==5%KhzzY{?nC<7Iy3qwM~$gZ>wl zdu5v;<(%Puu1@&(>aqhwbAoN{Rew7{X!uAv5B9~yF~C>a|nEX0aPoOUwc z2rlShSDz7y4=zIGY>&B_h@(aC0c}=-ZUC74*2O_|mv|6(DQ;5Izwn|mZ$M#BY}bot zA`;Pomw@BB7fUq3p@^+u#FomJvzCY++W6p~z#6xYkeJkRiWqpouA?fzp)&7FL~QM7 zt!>ig`X>7~eiYu&KfUsiNg$c{fb08S zfR5+-Apk`#>*f+Qu+TbJ%s5c*rHCoCP9jdtdR#Nv^5+b?y)z=mMb1iX=z~Lx_SA;L z1*QD|t!@FQb-X!LsOt*N=hBI)OYX{;@xFUH54PacuNCRzeyt3ck5*Suazhi?o{PV3 zqUf#e(2NMtHyQeUo#zGQp0jY@gkSERc?P{AD$uWgO#QDE^7l)^FKc_sQ{ortA3!Sv zmVut8jT^}gMtWv*MQ?fLeQ&5_o3ps4{-OJhNW?1gs!RN;kU{oLztJS(#0<|$P)xDm}pj^rI z>kYvL!luyI5}1$dgoW70YUXptkSrHyF!RjfN+CzT8Jpgl z4>W)|G2`)Qz{*u^*nT6Bns+QmFX@zPY9~*z?+vMJ^OL{mpaqGB@v1UEG*1Y)I8^?Q z<9J+dD?<2|G_IZ7&}=p5n#9#b@j@utdd^ox1|K8$aL__p8ZV&jEQTqy1JwJ8rp!0W zs!>zg{v4;A89le;cbSdF+v{$S7XoN-1RDRCXx4VEgPO-6z&@sRwG049zkqf>O&)v1 zDIi17_s_Z|J2p5H68=lgz+)h(p_$37NpcW@C2+z6`4h# zCM;k5!L$g=G|-yn1Vppyz^xM})!J{Jh*JeVM7h}^YGuvF>%Rg1JOcH>@>R+)(>hpY zS#rgfQ=zy613zHC=fCxkOhng@6kH) z%{p7vWK0?apR=5~>Wtsw9TUJLL*O?8;oi=8m{2o%;-ey=3+)4YO~%ARhK-jotGDq` z*5(qskJf}vv=^+3jERB_GcWJj9AVHCctye+G1l&^uEEHKjwp_y(C=+v z#)0J?)#i}2cv9xFCEhs?BR7Fl94kS;mxDo+%E;AvkQ8+i#?u_{0>{Yl0U-qX{UOx2 zzSN^y6(~r|^fbXc`(Whkh7}2!XmURkqFh48$U}z1i5PD~e7+1Jzj+9@WDvB3213PT zj09v@9SGgT=Zg~ZRe_Lx&{6^rDvF7K8gCVnF#-@gVF|$lY|0XX8!}w6l(~8x43of= z@C_;w;ApZE)VLv^jA4S{jh8U1TEH%2&~^hbLX`KZa2&VS(8f%)`w)y4gWkg`5+c#$ zZvl{?Jk`iJ76mOtl_w{HXRZ3eC~T`KAZV#OeTJoVEPQnmasoA9>Ec&SoC<(6+3syKnLAbOt+#lZS5<&j&O|r)!<+;$i<3=l^*R;wgNV@n_)WdD z4(qSb;&>|KMHT{dbyDc_BmQ0}i%XJDGVDc57yVTFNFP6RxCw~&V<~-1u^cLm%x9#A zV^g(6>Rt>qd#m7K-AyH`{V;+rnj8_ZXgWB1GWS9`%?14;BMA%oSPsrhX7g`trTvxy z0~QZ2pgB87P&kj^p8ScvoV>Tz_QJr?Fbm^nTH-EAH+h^btnf8lG@vErpe3Nz;c59I zixNwz7^}Em6jJbgJGj~=3`Fo*-RJKFov4YLf7v^Ulii|n9eg9a})h|Qx=Jeu4ISea68;J+`1rf3xLf3}ZZfL1xQmnRS+lXdV4kS}R1iN~b_n969T-^VBKw3HK0+ z?t35(k;3?sN^AXfXfV#7M_vqwKBEvFc}7-2%i5kMos-&#y$F2l;?%koJC3>IAhbto z`I}Zq+PPMPBnL75N`}XVUnl91^=VkuZ}9uVf2#)Bh;K?-uf1tB43C%a!_UT_d2fg@ zu7us!pTRfh!JjFJbye!h(b2eVGBF=dZBP%QLd+8A2i zv-b%}c;?{$gaIU9h|Zq#!A`fmtooumv3F$XB?{Ct(jqc>SrxmiRJP?Z9-SN40u(K#7?1^Q(-F&7qP*oVZpCpl$>lso_d{^>|%)%XJ;ZyRl;k)}f zhqk#xc>lYVF6S#j{@_TlXW-7&rLg@PA#CKV#I-ke?W)$r zZlZ><*x!R%s#ovhdp=h*tMP0(Pp0^pcB%hEjv%$G?u9Ts*l_S#u)c;EDe^2$Q(sv~ z)o{ZmHR(%}eK^r4g{IcRXTU(+T!zAugL8tLkeIKQb<^kIR23`|IeE*1mI?)#zM8KM z+)%%JuW$+xA7V6cqg98SayI{I2wa>rh=>h=3z9BsvQp^PaiSEnwE=Cy)mk$j;3v~N ze+tS3Lt)?{BkH({C2^9mvU$U+ETl5wI^nr@!4!-Y_7n&XtK<5htQ52z(r!Q&m*t)B zJ)qr6%JH{UzKsVcr zcgOfkA=-X-y8TQ4#oryL-#o^Db3l=@$cW{`7)=hico|aw)*M#NmG8^Z(7uaV~%YVD&Nn;+eQ0$6&!`9@~e~|7;hn1}9R`_RPWFv9(UR9U?5=C=?FJm zzzyWtoV67NcaR8&X+LWM${#FYcRNBFlGe<5(vQh{b?OzfhD?wTo*qva|5R7G(npz?{|1rpv<|PrOO0L} z^jkTYPfn$BSC(<02@{C#WEqo*Dy$>8RIU+F@bQ>W=6+!)x%*c9(V>TQHd|ztm1#h>h5n_+)({!?@+>N!5gW z7E+L{8+`xz!-?UF#*2jNc;aZkZJXCC%3?f_{d%;r)XvzXp&;A4E}m$UF8HXxjNB9F-;C@-&Ne4mYe_`Y5Z?X;EfP7#W=<@5NZY_IY7~-KwLH zyMb<`S`69A_r|+vN7F2Rm)Y?vpN0=(`TApdJ8zBCR>o~JH4$%1edd{kruH9W`BEO7 zpI$eAGc$ak9A@Qn-_mCr8hR$l+fer?}?xdIO>Ni%0 zft+)5(asmd!6TFM2Pa4bNq7LHD$I z=#w~nI>&d@qb5AmTDoQl9%>x&vs|w#BB!P(^fQ#tZePn1<}f<5kmk+or>sZ*xaZb% z%>g)N2wn50v5M<*#IP_~@qz>G?04AYLq?hJ^)_8ryHpsq)iHa;V1!nXVy+?Y)C8`t zvC)kPNmS2Rf!?m#xA6LA{8i<*CFZK#KF(IZZv|1`YF_xRqNf!>4&}<+l>VCOhk5V{ zm)3xw)`(B@77lXr{|Banno`v^D>&cyE!Y``CFVT+&@bE}yK$5GT|hD|L+nng%bV9V jAF^(1o6nQi4Z94>4fYfqch`<)k50V7NG0*CgQ)%oRuyAI literal 0 HcmV?d00001 diff --git a/research/ck-grid-synthesis-seed24/CLAIM.json b/research/ck-grid-synthesis-seed24/CLAIM.json new file mode 100644 index 0000000000..70f4829a8e --- /dev/null +++ b/research/ck-grid-synthesis-seed24/CLAIM.json @@ -0,0 +1,21 @@ +{ + "track": "complex supplier", + "assignment_seed": 24, + "random_source": "Python secrets.randbelow(100), operating-system randomness", + "seed_generated_utc": "2026-10-13T18:06:08.791009+00:00", + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "claimed_utc": "2026-10-13T18:17:00Z", + "coordination": "No pinned sprint issue found; local claim and live PR overlap checks.", + "object": "All 103 absolute coefficient magnitudes in frozen PR626 CK forward/backward scalar streams; shortest single-scratch preparation with the original numerator magnitude and dyadic grid retained.", + "method": "Complete finite integer-state shortest paths, separate Bellman certificate check, exact macro and full scalar replay. Every COPY, source ADD/SUB, DOUBLE, HALF, accumulation and final dirty-work clear paid.", + "deliverable": "Scoped CK circuit construction or certified negative result, complete coefficient census and source-bound receipt; no new kappa.", + "expected_finish_utc": "2026-10-13T18:36:08Z", + "candidates": [ + "Canonical signed-digit fixed-macro lowering: rejected for overlap with PR723/734/787.", + "Same-source adjacent coefficient reuse: rejected for overlap with PR722/739/769/811.", + "CK grid-preserving single-scratch minima: selected; PR882 covers JP8, PR1036 covers source/target mutation." + ], + "stopping_rule": "Enumerate every vertex/edge for all 103 CK magnitudes once; finish one receipt and focused verification. Do not reopen the JP8 search or claim unrestricted circuit optimality.", + "time_note": "Fresh clone required because the old clone reported a truncated pack; orientation exceeded the intended first 20 percent. Remaining implementation is bounded and final 25 percent reserved for verification/handoff.", + "contributor": "Eva Ayala / ToikY, with substantial OpenAI Codex assistance" +} diff --git a/research/ck-grid-synthesis-seed24/EXPECTED.json b/research/ck-grid-synthesis-seed24/EXPECTED.json new file mode 100644 index 0000000000..e29417ff75 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/EXPECTED.json @@ -0,0 +1,833 @@ +{ + "comparisons": { + "1": { + "best_four_horner": 2, + "bounded_class_cost": 3, + "copy_binary": 2, + "installed": 2 + }, + "1/16": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "1/2": { + "best_four_horner": 4, + "bounded_class_cost": 4, + "copy_binary": 4, + "installed": 4 + }, + "1/4": { + "best_four_horner": 5, + "bounded_class_cost": 5, + "copy_binary": 5, + "installed": 5 + }, + "1/64": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "1/8": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 6, + "installed": 6 + }, + "10": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "11": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "11/4": { + "best_four_horner": 9, + "bounded_class_cost": 8, + "copy_binary": 10, + "installed": 8 + }, + "12": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "125": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 14, + "installed": 12 + }, + "126": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 14, + "installed": 11 + }, + "128": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "13": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "13/2": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "13/4": { + "best_four_horner": 9, + "bounded_class_cost": 8, + "copy_binary": 10, + "installed": 8 + }, + "130": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "134": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 12, + "installed": 12 + }, + "14": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "15": { + "best_four_horner": 8, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "15/2": { + "best_four_horner": 9, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "15/4": { + "best_four_horner": 10, + "bounded_class_cost": 9, + "copy_binary": 11, + "installed": 9 + }, + "15/8": { + "best_four_horner": 9, + "bounded_class_cost": 8, + "copy_binary": 12, + "installed": 8 + }, + "16": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "17": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "17/2": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "17/4": { + "best_four_horner": 10, + "bounded_class_cost": 9, + "copy_binary": 10, + "installed": 9 + }, + "17/8": { + "best_four_horner": 9, + "bounded_class_cost": 8, + "copy_binary": 11, + "installed": 8 + }, + "18": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "19": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "19/2": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "19/4": { + "best_four_horner": 11, + "bounded_class_cost": 10, + "copy_binary": 11, + "installed": 10 + }, + "2": { + "best_four_horner": 4, + "bounded_class_cost": 4, + "copy_binary": 4, + "installed": 4 + }, + "20": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "21": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "21/4": { + "best_four_horner": 11, + "bounded_class_cost": 10, + "copy_binary": 11, + "installed": 10 + }, + "22": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "23/2": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "23/8": { + "best_four_horner": 11, + "bounded_class_cost": 9, + "copy_binary": 13, + "installed": 9 + }, + "24": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "247/2": { + "best_four_horner": 14, + "bounded_class_cost": 15, + "copy_binary": 17, + "installed": 15 + }, + "249": { + "best_four_horner": 13, + "bounded_class_cost": 13, + "copy_binary": 15, + "installed": 13 + }, + "252": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 15, + "installed": 12 + }, + "255": { + "best_four_horner": 12, + "bounded_class_cost": 13, + "copy_binary": 17, + "installed": 13 + }, + "256": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "257/2": { + "best_four_horner": 13, + "bounded_class_cost": 13, + "copy_binary": 13, + "installed": 13 + }, + "26": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "260": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 12, + "installed": 12 + }, + "27": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "27/2": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "28": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "29": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "29/2": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "29/8": { + "best_four_horner": 11, + "bounded_class_cost": 10, + "copy_binary": 13, + "installed": 10 + }, + "3": { + "best_four_horner": 5, + "bounded_class_cost": 5, + "copy_binary": 5, + "installed": 5 + }, + "3/2": { + "best_four_horner": 5, + "bounded_class_cost": 5, + "copy_binary": 6, + "installed": 5 + }, + "3/4": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 7, + "installed": 6 + }, + "3/8": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 8, + "installed": 7 + }, + "30": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 10, + "installed": 9 + }, + "31": { + "best_four_horner": 9, + "bounded_class_cost": 10, + "copy_binary": 11, + "installed": 10 + }, + "31/2": { + "best_four_horner": 10, + "bounded_class_cost": 11, + "copy_binary": 12, + "installed": 11 + }, + "31/4": { + "best_four_horner": 11, + "bounded_class_cost": 12, + "copy_binary": 13, + "installed": 12 + }, + "31/8": { + "best_four_horner": 11, + "bounded_class_cost": 10, + "copy_binary": 14, + "installed": 10 + }, + "32": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "33/2": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "34": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "35/8": { + "best_four_horner": 12, + "bounded_class_cost": 11, + "copy_binary": 13, + "installed": 11 + }, + "36": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "38": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "39/2": { + "best_four_horner": 11, + "bounded_class_cost": 12, + "copy_binary": 12, + "installed": 12 + }, + "39/8": { + "best_four_horner": 12, + "bounded_class_cost": 11, + "copy_binary": 14, + "installed": 11 + }, + "4": { + "best_four_horner": 5, + "bounded_class_cost": 5, + "copy_binary": 5, + "installed": 5 + }, + "40": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "48": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "5": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 6, + "installed": 6 + }, + "5/2": { + "best_four_horner": 7, + "bounded_class_cost": 6, + "copy_binary": 7, + "installed": 6 + }, + "5/4": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 8, + "installed": 6 + }, + "5/8": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 9, + "installed": 7 + }, + "512": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 12, + "installed": 12 + }, + "52": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "54": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "58": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "6": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 6, + "installed": 6 + }, + "60": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 11, + "installed": 10 + }, + "62": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 12, + "installed": 10 + }, + "63": { + "best_four_horner": 10, + "bounded_class_cost": 11, + "copy_binary": 13, + "installed": 11 + }, + "63/2": { + "best_four_horner": 11, + "bounded_class_cost": 12, + "copy_binary": 14, + "installed": 12 + }, + "64": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "65": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "67": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "67/2": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 12, + "installed": 12 + }, + "68": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "7": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "7/2": { + "best_four_horner": 8, + "bounded_class_cost": 7, + "copy_binary": 8, + "installed": 7 + }, + "7/4": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 9, + "installed": 7 + }, + "7/8": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 10, + "installed": 7 + }, + "72": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "76": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "8": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 6, + "installed": 6 + }, + "9": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "9/2": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "9/4": { + "best_four_horner": 8, + "bounded_class_cost": 7, + "copy_binary": 9, + "installed": 7 + }, + "9/8": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 10, + "installed": 7 + } + }, + "controls": { + "endpoint_neutral_finer_grid": "fractional grid", + "endpoint_neutral_growth": "magnitude envelope", + "missing_clear": "macro endpoint", + "missing_copy": "dirty work initialization", + "uncharged_redundant_ops": "macro cost", + "wrong_accumulation": "macro endpoint" + }, + "graphs": { + "census_sha256": "8c94db25fd01b1220253d1f330665d4f6e5ff982e3af0f09854ba870d7e83826", + "coefficients": 103, + "labelled_edges": 96929, + "negative_controls": [ + "wrong_bound", + "missing_vertex", + "duplicate_vertex", + "wrong_distance", + "boolean_distance", + "wrong_word", + "unknown_primitive", + "wrong_cost", + "wrong_terminal_sign" + ], + "preparation_operations": 617, + "relaxation_rounds": 1609, + "signed_dirty_macro_columns": 618, + "source_payload_sha256": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900", + "vertices": 16251 + }, + "magnitudes": 103, + "programs": { + "backward": { + "baseline_real_primitives": 169634, + "best_four_horner_complete_real_primitives": 168504, + "changed_coefficients": { + "11/4": 1, + "125": 1, + "126": 4, + "13/4": 1, + "15/4": 4, + "15/8": 3, + "17/4": 3, + "17/8": 1, + "19/4": 4, + "21/4": 2, + "23/8": 5, + "247/2": 1, + "249": 1, + "252": 2, + "255": 1, + "29/8": 1, + "3/2": 89, + "3/4": 259, + "3/8": 9, + "30": 5, + "31": 1, + "31/2": 2, + "31/4": 1, + "31/8": 4, + "35/8": 1, + "39/8": 2, + "5/2": 49, + "5/4": 18, + "5/8": 5, + "60": 4, + "62": 2, + "63": 5, + "63/2": 1, + "7/2": 26, + "7/4": 6, + "7/8": 2, + "9/4": 5, + "9/8": 3 + }, + "charged_payload_bits": 192, + "columns": 725, + "dirty_helpers": 492, + "net_saving_vs_complete_four_horner": 180, + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "primitive_sha256": "247423364c6cf48ffe178c5a4ceed808df465d5762e84455581bf29b1a20fbad", + "primitive_tags": { + "add": 24194, + "clear": 42934, + "copy": 30452, + "double": 9740, + "halve": 38998, + "negate": 696, + "subtract": 21310 + }, + "replacement_real_primitives": 168324, + "retained_original_envelope": "146068000389976309073/32", + "saving": 1310, + "selected_occurrence_saving_vs_four_horner": 234, + "strictly_beyond_four_horner": { + "11/4": 1, + "13/4": 1, + "15/4": 4, + "15/8": 3, + "17/4": 3, + "17/8": 1, + "19/4": 4, + "21/4": 2, + "23/8": 5, + "29/8": 1, + "31/8": 4, + "35/8": 1, + "39/8": 2, + "5/2": 49, + "7/2": 26, + "9/4": 5 + } + }, + "forward": { + "baseline_real_primitives": 169618, + "best_four_horner_complete_real_primitives": 168488, + "changed_coefficients": { + "11/4": 1, + "125": 1, + "126": 4, + "13/4": 1, + "15/4": 4, + "15/8": 3, + "17/4": 3, + "17/8": 1, + "19/4": 4, + "21/4": 2, + "23/8": 5, + "247/2": 1, + "249": 1, + "252": 2, + "255": 1, + "29/8": 1, + "3/2": 89, + "3/4": 259, + "3/8": 9, + "30": 5, + "31": 1, + "31/2": 2, + "31/4": 1, + "31/8": 4, + "35/8": 1, + "39/8": 2, + "5/2": 49, + "5/4": 18, + "5/8": 5, + "60": 4, + "62": 2, + "63": 5, + "63/2": 1, + "7/2": 26, + "7/4": 6, + "7/8": 2, + "9/4": 5, + "9/8": 3 + }, + "charged_payload_bits": 192, + "columns": 725, + "dirty_helpers": 492, + "net_saving_vs_complete_four_horner": 180, + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "primitive_sha256": "a189dfbdb7f3b8d61bfdff1c264cfd905a54350b17c87e8cd8cc2ca3958d25ed", + "primitive_tags": { + "add": 23796, + "clear": 42918, + "copy": 30468, + "double": 9740, + "halve": 38998, + "negate": 696, + "subtract": 21692 + }, + "replacement_real_primitives": 168308, + "retained_original_envelope": "920709848294", + "saving": 1310, + "selected_occurrence_saving_vs_four_horner": 234, + "strictly_beyond_four_horner": { + "11/4": 1, + "13/4": 1, + "15/4": 4, + "15/8": 3, + "17/4": 3, + "17/8": 1, + "19/4": 4, + "21/4": 2, + "23/8": 5, + "29/8": 1, + "31/8": 4, + "35/8": 1, + "39/8": 2, + "5/2": 49, + "7/2": 26, + "9/4": 5 + } + } + }, + "status": "PASS_CK_GRID_SYNTHESIS" +} diff --git a/research/ck-grid-synthesis-seed24/OVERLAP.json b/research/ck-grid-synthesis-seed24/OVERLAP.json new file mode 100644 index 0000000000..29cd0aa5bb --- /dev/null +++ b/research/ck-grid-synthesis-seed24/OVERLAP.json @@ -0,0 +1,133 @@ +{ + "checked_utc": "2026-10-13T18:28:00Z", + "open_issues": [ + { + "number": 913, + "title": "All size/compiler is retained" + }, + { + "number": 650, + "title": "Can we turn on Discussions?" + } + ], + "latest_open_prs": [ + { + "number": 1113, + "title": "Research: exclude a finite precision neighborhood of R439 matching optima" + }, + { + "number": 1112, + "title": "Independent verification: selected PR1042 finite invoice, 9 guards, 14 bootstrap steps and 94 outer slacks (seed 81, no new kappa)" + }, + { + "number": 1111, + "title": "Conditional κ = 0.001672780159952542: reverse one entrance promotion to fill T16 gaps" + }, + { + "number": 1110, + "title": "Research consolidation: reconcile PR225 five-stage pricing with exact intervals (no new kappa)" + }, + { + "number": 1108, + "title": "Research: exact compact-control boundary cancellation obstruction (no new kappa)" + }, + { + "number": 1107, + "title": "Conditional κ = 0.001672765980186726: rank-seven helper ends and T16 owner packing on the seven-slot k8 word" + }, + { + "number": 1106, + "title": "Mathematical audit: PR1064 nine-shift factory gauge is unique" + }, + { + "number": 1105, + "title": "Mathematical audit: raw endpoint independence does not justify target-feedback cleanup" + }, + { + "number": 1104, + "title": "Conditional κ = 0.001672691689152441: rank-seven helper ends and T16 owner packing on the seven-slot k8 word" + }, + { + "number": 1103, + "title": "Research: rectangular output borrowing and complete minimum-word census (no new kappa)" + }, + { + "number": 1102, + "title": "Audit: two inputs optimally detect all PR967 single-ADD omissions" + }, + { + "number": 1101, + "title": "Tooling: overlap bit589 and complex741 in the #741 ancestry replay, 17% (50% with --complex-jobs 3) less wall time (no new kappa)" + }, + { + "number": 1100, + "title": "Research: give short donor certificates for R439 class exclusions" + }, + { + "number": 1099, + "title": "Tooling: accelerate exact frame-pair enumeration with unchanged D/E/H checks" + }, + { + "number": 1098, + "title": "Independent verification: label-free P112 Gram support spectra (no new kappa)" + }, + { + "number": 1097, + "title": "Research consolidation: checked P111 minrank and fitting-matrix uniqueness proofs" + }, + { + "number": 1096, + "title": "Finite precision audit: PR589 bank envelope uses 132 bits versus a 177-bit bound" + }, + { + "number": 1095, + "title": "Certify exact prefix-monomial costs for 168 historical complex boundaries" + }, + { + "number": 1094, + "title": "Conditional kappa 0.001672660197076918: rare-pattern T16 exchanges" + }, + { + "number": 1093, + "title": "Research: tighten fixed precision for a complete signed inverse word" + }, + { + "number": 1092, + "title": "Tooling: exact Clifford state reuse with independent controls (no new kappa)" + }, + { + "number": 1091, + "title": "Research audit: independent owner-map check of all 15 open T16 claims on the seven-slot k8 word (no new kappa)" + }, + { + "number": 1090, + "title": "Conditional κ = 0.001672404744903063: rank-seven helper ends on the k8 word" + }, + { + "number": 1089, + "title": "Finite bit construction: R480 Q-node5 saves 20 ADDs (no new kappa)" + }, + { + "number": 1088, + "title": "Research: exact weighted optimum for signed 3x3 connector repairs (no new kappa)" + } + ], + "refreshed_heads": [ + { + "pr": 882, + "head": "e698981e0ffa680b6c5896dace1609025b97ad70", + "state": "closed" + }, + { + "pr": 1036, + "head": "c4ad801099d0813ffac56f0b517a908cd8ae0c6a", + "state": "open" + }, + { + "pr": 999, + "head": "fd38a824adb3a5c60c101a86c950a6d590454adf", + "state": "open" + } + ], + "distinction": "CK complete grid-bounded single-scratch graphs, not PR882 JP8, PR1036 source/target mutation, PR999 multiple target updates or already-covered signed-Horner/work-sharing. No pending implementation consumed." +} diff --git a/research/ck-grid-synthesis-seed24/PROOF.md b/research/ck-grid-synthesis-seed24/PROOF.md new file mode 100644 index 0000000000..30803c1793 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/PROOF.md @@ -0,0 +1,69 @@ +# Finite class, complete cost and inherited prefix bounds + +The source and target are distinct and never written during preparation. +Private work may be arbitrarily dirty. For reduced `|q|=a/D`, where `D` is a +power of two, the searched word has one initial COPY, an arbitrary finite +preparation, one target ADD/SUB, and one final CLEAR. Preparation may use +unit source ADD/SUB, DOUBLE, HALF, NEGATE, COPY and CLEAR on work only, while +its coefficient remains in `D^-1 Z` and has absolute value at most `a`. +The unit macro's cheaper direct two-instruction lowering is outside this +mandatory-copy form and is retained. + +Write `W=(x/D)S`. Every admissible preparation is exactly a walk on the full +integer vertex set `[-aD,aD]`, starting at `D` and ending at either `a` or `-a`. +The unit-cost transitions are `x+D`, `x-D`, `2x`, `-x`, `0`, `D`, and `x/2` +when `x` is even; only destinations in the vertex set are admitted. This +describes all words of arbitrary length in this class. Any repeated-state +cycle can be removed without increasing cost. The three instructions outside +the walk are all paid, giving complete cost `3+min(d(a),d(-a))`. + +The construction uses breadth-first search from `D`. A separately implemented +synchronous Bellman recurrence rebuilds every label. Every edge `x -> y` +satisfies `d(y)<=d(x)+1`; telescoping from `d(D)=0` lower-bounds every path's +length by its endpoint label. Every noninitial vertex has an attaining +predecessor, and the submitted witness explicitly attains the lesser goal +label. These exact obligations prove optimality in the declared finite graph. +They do not prove optimality with extra registers, changed source/target, +multiple target updates, different initialization, a finer grid, a larger +envelope, macro reuse or physical tape instructions. The frozen inventory +from both CK programs is compared to all 103 certificate records. + +After COPY, induction gives `W=(x/D)S` for arbitrary inputs. Adjusting the +target accumulation sign for the witness's terminal sign produces exactly +`T+qS`, with unchanged `S`; CLEAR leaves zero work. Testing all three formal +columns establishes the entire linear map, including dirty work and +correlated inputs. Applying the real-coefficient identity to each complex +component proves the same complex boundary map. Substitution at every +original macro boundary preserves subsequent states by induction. Paid +events, frames and recursive children are retained, rather than commuted or +omitted. The scalar projection does not execute physical frame operators. + +The original binary preparation reaches `aS` before terminal halvings. Every +candidate prefix has `|W|<=a|S|`, so its work magnitude and row-L1 norm are +bounded by that original attained state. Source and target values before +and after the single update, initial private dirt and final zero also match +the original boundary values. This proves maximum-row/prefix domination; +it does not claim literal prefix containment or entrywise domination of +simultaneous transfer matrices. The verifier separately reconstructs the +original nonnegative Horner envelope from every event and matches the pinned +independent receipt: `920709848294` forward and +`146068000389976309073/32` backward, within the retained 192-bit allowance. +Candidate macro checks certify the local bound used in this substitution +argument, and complete sparse primitive replay certifies both endpoints. + +For fractional depth, a prefix work coefficient is `x*s_j/D` for each source +row coefficient `s_j`. If `D>1`, reduced `a` is odd, so its denominator depth +is no larger than that of the original attained terminal coefficient +`a*s_j/D`. For `D=1` the multiplier is integral, so the original leading +source state already bounds its denominator depth. All other register states +are unchanged at boundaries. Thus these substitutions need no finer scalar +prefix grid than original/copy binary Horner. This is not a full physical +rounding, overflow, tape or compiler precision certificate. + +The net saving against PR837 is a complete instruction recount, including +cost increases at some coefficients. It is not obtained by summing only +strict improvements. More source additions can replace shifts, and each is +charged; no physical memory-traffic or runtime inference follows. Paid ranks +and assembly choices stay fixed, so these finite circuits give no new kappa. +Inherited all-size and physical interfaces remain assumptions, and finite +graph/column verification is not a formal multiplication theorem proof. diff --git a/research/ck-grid-synthesis-seed24/README.md b/research/ck-grid-synthesis-seed24/README.md new file mode 100644 index 0000000000..93a85eece4 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/README.md @@ -0,0 +1,103 @@ +# CK grid-preserving single-scratch coefficient circuits + +Finite complex-supplier construction and scoped optimality certificate; **no +new kappa**. This supplies a CK companion to Philipp / @mightyOil's JP8 search +in [PR882](https://github.com/CrocSwap/integer-mult-bounds/pull/882). It covers +all 103 magnitudes in the historical PR626 CK streams, including numerators +through 512 and denominators through 64, rather than reopening the JP8 domain. + +| Complete CK scalar projection | PR696 copy/unit | Best four PR837 Horner choices | This construction | +| --- | ---: | ---: | ---: | +| Forward | 169,618 | 168,488 | 168,308 | +| Backward / inverse-transpose | 169,634 | 168,504 | 168,324 | + +The saving is **1,310 real-component primitives per orientation against +PR696**, or **180 net against the complete four-Horner comparator**. At the +individual occurrences that strictly beat every Horner choice the saving is +234; other occurrences cost 54 more than that comparator, giving the stated +net 180. All original magnitude envelopes and coefficient grids are retained. +These are finite instruction counts, not measured runtime improvements. + +Run offline with standard-library Python 3.11+: + +```sh +python3 -B -I research/ck-grid-synthesis-seed24/verify.py +python3 -B -I research/ck-grid-synthesis-seed24/independent.py +python3 -B -I research/ck-grid-synthesis-seed24/test_package.py +``` + +Main expected marker: + +```text +PASS_CK_GRID_SYNTHESIS magnitudes=103 programs=2 columns=725 savings=1310,1310 no_new_kappa +``` + +The default verifier writes nothing and compares its complete deterministic +receipt to [EXPECTED.json](EXPECTED.json). `--write-certificate` explicitly +regenerates that receipt after all checks. [CENSUS.json.gz](CENSUS.json.gz) +contains every graph distance and chosen preparation witness; equality is on +decoded JSON, not gzip packaging. [SOURCES.json](SOURCES.json) binds the seven +consumed inputs by payload SHA256 and records their immutable Git blobs. + +For `q = +/-a/D`, preparation starts with one paid `COPY W <- S`, stays on +the grid `D^-1 Z` with `|W/S| <= a`, and ends at either signed coefficient +`+/-a/D`. Every source ADD/SUB, DOUBLE, HALF, NEGATE, COPY or CLEAR costs one. +One signed target accumulation and one final CLEAR complete the map +`(T,S,W) -> (T+qS,S,0)`, including arbitrary initial work. The accepted unit +macro costs two and is kept separately. Every primitive uses the original +macro frame; source, helper count, paid children and event boundaries stay +fixed. No additional source access, frame change, copy, restoration or child +is hidden in these counts. Only a strictly shorter complete word replaces +the PR696 word. + +The complete finite search comprises 16,251 vertices and 96,929 labelled +edges, with no depth cap, sampled coefficients or unresolved search nodes. +A separately written synchronous Bellman implementation checks every label, +edge inequality and shortest witness. This is independent AI implementation, +not independent human review. The primitive replay checks all 725 formal +input columns in both complete scalar programs: 224 data, 492 arbitrary dirty +helpers, eight dirty private centers and dirty coefficient work. Helpers are +restored and private cells erased. Nine graph controls, six macro controls +and focused whole-word/source/certificate tests check meaningful failures. +The [proof](PROOF.md) states exactly which minimum and prefix claims follow. + +Exact base: `ba82555c64e1879e4b7decce28186f208fcb8262`. OS assignment seed +**24**, complex-supplier track. The local [claim](CLAIM.json) records candidate +selection, stopping rule and timing. The old clone reported a truncated pack, +so this sprint used a fresh shallow clone and isolated `codex/complex-seed24` +branch. Orientation exceeded the intended first 20 percent; implementation +then stayed bounded and the final quarter was reserved for verification and +handoff. + +At this base the actual selected result is **PR1042**, conditional kappa +`1672188119205421/10^18 = 0.001672188119205421`, with reviewed source head +`7e8ef087c02a77038a28a337a7ee3a77039cac0d`. The selected record, manifest, +assembly, batch1047 review, mutable-leaver/slot construction and T16 owner +package were read. This contribution deliberately concerns historical CK, +not transport to that newly selected word. The paid profile is unchanged, +so no exponent improvement follows. + +PR723/734/787 already cover forward signed-digit recoding; PR837 supplies the +four-Horner comparator and PR866 explains the fractional-grid obligation. +PR722/739/769/811 reuse work across macros and are not composed here. +[PR1036](https://github.com/CrocSwap/integer-mult-bounds/pull/1036), by Hanson +Sun / @bbMisk, obtains larger CK savings in a distinct source/target mutation +class. Its two-register exclusion does not settle this single-scratch class; +we claim no stronger unrestricted circuit result. PR999 permits multiple +target accumulations and is also distinct. No pending implementation is a +code dependency, and no savings from these packages are added together. + +Credit Sagar Thakrar / @thakrarsagar's PR696 copy/unit lowering (also used in +the verifier adaptation), Gareth Davidson / @bitplane's PR837 comparator, +Philipp / @mightyOil's PR882 graph method and grid proof, Chris Pagolu's PR734, +Hanson Sun's PR1036, and the retained icekylinx / Jeremy Kothe / Chafik +Boukhalfa / DreamingOfClouds / Rohan Arun / eumemic construction lineage. +Prepared for **Eva Ayala / @ToikY with substantial OpenAI Codex assistance** +in selection, implementation, proof, verification and separate AI review. +Apache-2.0; no elementary shift/add synthesis priority is claimed. + +Production/native phase admission, complete global invoice and owner replay, +transport to PR1042 and all-size compiler/realization/hosting/precision/tape/ +analytic obligations remain separate. Full repository, supplier cold replay, +Lean and hosted CI passes are not claimed. `upstream/`, the production emitter +and selected frontier are unchanged. diff --git a/research/ck-grid-synthesis-seed24/SOURCES.json b/research/ck-grid-synthesis-seed24/SOURCES.json new file mode 100644 index 0000000000..212cd08978 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/SOURCES.json @@ -0,0 +1,28 @@ +{ + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "git_blobs": { + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/INDEPENDENT-LOCAL-REPLAY.json": "ec8d742c3d932160fac10d0d9befdd2056cb240e", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-CHECKS.json": "d2b8854114b19b88e14d2af0dd84ad79e9eedbaa", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz": "61ef73c1f958e0d26f3e7a3a82bc3826b7098c93", + "research/complex-dyadic-lowering/EXPECTED.json": "6cdc73b8867b8e06f24a1c84d23baabfc7671cbf", + "research/complex-dyadic-lowering/lower.py": "a2c2889e5be41a0fc30d4dfa5dfcebb03d6d47f8", + "research/dyadic-horner-direction/lower.py": "a7855d2a87b77913bac097e1ece8ee35119bae28", + "research/dyadic-horner-direction/vendor/pr696_lower.py": "a2c2889e5be41a0fc30d4dfa5dfcebb03d6d47f8" + }, + "historical_pr626_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "payload_sha256": { + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/INDEPENDENT-LOCAL-REPLAY.json": "ecefb9e661301d8081522be68bbe6640e175c011eb1177f643383d193c6fb2f0", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-CHECKS.json": "059c4e59142bdf5c19dc7c0afebcddfec28e6e60cbc7299b8bdcc624afbc0cbe", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900", + "research/complex-dyadic-lowering/EXPECTED.json": "81ec6ec0cbeeae16ee72fcfa956b42ff761eadd5985cf495714f323081440782", + "research/complex-dyadic-lowering/lower.py": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753", + "research/dyadic-horner-direction/lower.py": "6a7ae3f2aff61077ce4b3f179f7ccc2024f5176b5894547250eb14105b14f5e2", + "research/dyadic-horner-direction/vendor/pr696_lower.py": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753" + }, + "pr1036_head": "c4ad801099d0813ffac56f0b517a908cd8ae0c6a", + "pr622_head": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "pr696_head": "5a3f983715027c4fd83f50bc9001d4b18463bed1", + "pr837_head": "0a2977195efc8fb2a918fbfb694ec8d294387f08", + "pr882_head": "e698981e0ffa680b6c5896dace1609025b97ad70", + "pr883_head": "b31a870a3842b37f6ab97767c506ce91783632a2" +} diff --git a/research/ck-grid-synthesis-seed24/VALIDATION.md b/research/ck-grid-synthesis-seed24/VALIDATION.md new file mode 100644 index 0000000000..ca2e7e5101 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/VALIDATION.md @@ -0,0 +1,37 @@ +# Validation and handoff + +2026-10-13, macOS, bundled CPython 3.12.14, standard library only. +Base `ba82555c64e1879e4b7decce28186f208fcb8262`. + +Passed: + +```sh +python3 -B -I research/ck-grid-synthesis-seed24/verify.py --write-certificate +python3 -B -I -O research/ck-grid-synthesis-seed24/verify.py +python3 -B -I research/ck-grid-synthesis-seed24/independent.py +python3 -B -I -O research/ck-grid-synthesis-seed24/test_package.py +``` + +- Both complete literal primitive streams, all 725 formal columns, exact + endpoints, 492 restored helpers, private cleanup and unchanged paid profiles. +- All 103 magnitudes, 16,251 graph vertices and 96,929 labelled edges; separate + BFS and synchronous Bellman engines agree on every distance and signed witness. +- Nine graph and six macro controls; two complete-word controls reject a wrong + target sign and omitted work clear; two admission controls reject altered + source semantics and an understated certificate cost. Gzip repackaging passes. +- Isolated optimized replay from a minimal offline relocated checkout whose + path contains spaces, invoked from a different working directory, passes. +- Current selected certificate SHA256 and exact kappa agree with the record. + This small check is explicitly **not** the complete selected-record source + inventory check; the sparse research checkout omits unrelated packages. +- Staged whitespace and one-package scope checked before commit. + +No new dependency, native supplier regeneration, complete selected cold replay, +full repository suite, hosted CI, Lean or physical runtime benchmark was run. +Those passes are not claimed. The prefix/grid claim combines exact local macro +checks with the written substitution argument and reconstructed pinned original +envelopes; it is not an independent full physical precision certificate. + +The immediate overlap refresh through PR1113 is recorded in OVERLAP.json. +The closest input/comparison heads remained unchanged. No pinned coordination +issue existed. A local claim result will record the single published PR link. diff --git a/research/ck-grid-synthesis-seed24/independent.py b/research/ck-grid-synthesis-seed24/independent.py new file mode 100644 index 0000000000..5b5b0278db --- /dev/null +++ b/research/ck-grid-synthesis-seed24/independent.py @@ -0,0 +1,188 @@ +"""Independent integer-grid distance and dirty-macro checks for frozen CK words. + +Eva Ayala / ToikY, with substantial OpenAI Codex assistance; Apache-2.0. +No constructor imports. Distances use synchronous Bellman relaxation rather +than the construction's breadth-first queue. Optimality is only in the stated +bounded, single-work-register graph with paid COPY before preparation. +""" +import argparse +import copy +from fractions import Fraction +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def inventory(): + payload = gzip.decompress(SOURCE.read_bytes()) + programs = json.loads(payload) + require(set(programs) == {'forward', 'backward'}, 'source orientations') + values = set() + for events in programs.values(): + for event in events: + if event[0] == 'scalar' and event[1][0] == 'add': + q = abs(Fraction(event[1][3], event[1][4])) + require(q > 0, 'source coefficient zero') + values.add(q) + require(len(values) == 103, 'frozen CK coefficient inventory') + return values, hashlib.sha256(payload).hexdigest() + + +def transitions(x, denominator, bound): + """Enumerate every labelled graph edge; duplicate endpoints stay distinct.""" + destinations = { + 'add': x + denominator, 'subtract': x - denominator, + 'double': x * 2, 'negate': -x, 'clear': 0, 'copy': denominator, + } + if x % 2 == 0: + destinations['halve'] = x // 2 + return {tag: y for tag, y in destinations.items() if -bound <= y <= bound} + + +def dirty_macro(word, a, denominator, sign, terminal_sign): + """All three arbitrary input columns, represented in integer units 1/D.""" + source = [0, denominator, 0] + target = [denominator, 0, 0] + work = source.copy() # Paid COPY overwrites the arbitrary dirty work column. + for tag in word: + if tag == 'clear': + work = [0, 0, 0] + elif tag == 'copy': + work = source.copy() + elif tag == 'halve': + require(all(v % 2 == 0 for v in work), 'macro leaves the grid') + work = [v // 2 for v in work] + elif tag == 'double': + work = [2 * v for v in work] + elif tag == 'negate': + work = [-v for v in work] + elif tag in ('add', 'subtract'): + multiplier = 1 if tag == 'add' else -1 + work = [v + multiplier * s for v, s in zip(work, source)] + else: + raise ValueError('unknown preparation primitive') + target = [t + sign * terminal_sign * w for t, w in zip(target, work)] + work = [0, 0, 0] # Paid final CLEAR. + require(target == [denominator, sign * a, 0], 'dirty target map') + require(source == [0, denominator, 0] and work == [0, 0, 0], 'dirty restoration') + + +def check_record(q, record): + require(type(record) is dict and set(record) == {'a', 'D', 'bound', 'states', 'word', 'cost', 'terminal_sign'}, 'record schema') + a, denominator = q.numerator, q.denominator + for key, value in (('a', a), ('D', denominator), ('bound', a * denominator)): + require(type(record[key]) is int and record[key] == value, 'parameter ' + key) + bound = record['bound'] + vertices = list(range(-bound, bound + 1)) + require(type(record['states']) is list, 'state list') + labels = {} + for state in record['states']: + require(type(state) is dict and set(state) == {'x', 'distance'}, 'state schema') + x, distance = state['x'], state['distance'] + require(type(x) is int and type(distance) is int and distance >= 0, 'state integer labels') + require(x not in labels, 'duplicate state') + labels[x] = distance + require(set(labels) == set(vertices), 'complete vertex inventory') + edges = [(x, tag, y) for x in vertices for tag, y in transitions(x, denominator, bound).items()] + + # Complete synchronous shortest-distance recurrence. Each iteration admits + # one further edge, so convergence requires at most |V| iterations. + infinity = len(vertices) + 1 + distances = {x: infinity for x in vertices} + distances[denominator] = 0 + for rounds in range(1, len(vertices) + 1): + following = distances.copy() + for x, _tag, y in edges: + following[y] = min(following[y], distances[x] + 1) + if following == distances: + break + distances = following + else: + raise ValueError('Bellman relaxation did not converge') + require(all(d < infinity for d in distances.values()), 'unreachable graph vertex') + require(labels == distances, 'independent distance labels') + + # Explicit certificate obligations: edge lower bounds and attainment. + require(labels[denominator] == 0, 'start distance') + attained = {denominator} + for x, _tag, y in edges: + require(labels[y] <= labels[x] + 1, 'Bellman edge inequality') + if labels[y] == labels[x] + 1: + attained.add(y) + require(attained == set(vertices), 'shortest predecessor attainment') + require(type(record['word']) is list, 'word list') + x = denominator + for tag in record['word']: + require(type(tag) is str and tag in transitions(x, denominator, bound), 'witness edge') + x = transitions(x, denominator, bound)[tag] + terminal_sign = record['terminal_sign'] + require(type(terminal_sign) is int and terminal_sign in (-1, 1), 'terminal sign') + require(x == terminal_sign * a, 'witness endpoint') + shortest = min(labels[a], labels[-a]) + require(len(record['word']) == shortest, 'witness minimum length') + require(type(record['cost']) is int and record['cost'] == shortest + 3, 'paid copy/add/clear cost') + for sign in (1, -1): + dirty_macro(record['word'], a, denominator, sign, terminal_sign) + return len(vertices), len(edges), rounds, len(record['word']) + + +def negative_controls(census): + q = Fraction(1, 64) + original = census[str(q)] + mutations = {} + for name in ('wrong_bound', 'missing_vertex', 'duplicate_vertex', 'wrong_distance', 'boolean_distance', 'wrong_word', 'unknown_primitive', 'wrong_cost', 'wrong_terminal_sign'): + mutations[name] = copy.deepcopy(original) + mutations['wrong_bound']['bound'] += 1 + mutations['missing_vertex']['states'].pop() + mutations['duplicate_vertex']['states'].append(mutations['duplicate_vertex']['states'][0].copy()) + mutations['wrong_distance']['states'][0]['distance'] += 1 + mutations['boolean_distance']['states'][0]['distance'] = True + mutations['wrong_word']['word'].pop() + mutations['unknown_primitive']['word'].append('unpaid_halve') + mutations['wrong_cost']['cost'] -= 1 + mutations['wrong_terminal_sign']['terminal_sign'] *= -1 + rejected = [] + for name, mutation in mutations.items(): + try: + check_record(q, mutation) + except ValueError: + rejected.append(name) + else: + raise ValueError('accepted negative control: ' + name) + return rejected + + +def check(census): + values, source_hash = inventory() + require(type(census) is dict and set(census) == {str(q) for q in values}, 'complete coefficient census') + totals = [0, 0, 0, 0] + for q in sorted(values): + result = check_record(q, census[str(q)]) + totals = [x + y for x, y in zip(totals, result)] + return {'coefficients': len(values), 'vertices': totals[0], 'labelled_edges': totals[1], + 'relaxation_rounds': totals[2], 'preparation_operations': totals[3], + 'signed_dirty_macro_columns': 6 * len(values), 'source_payload_sha256': source_hash, + 'census_sha256': hashlib.sha256(json.dumps(census, sort_keys=True, separators=(',', ':')).encode()).hexdigest(), + 'negative_controls': negative_controls(census)} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('certificate', nargs='?', type=Path, default=HERE / 'CENSUS.json.gz') + args = parser.parse_args() + raw = args.certificate.read_bytes() + if args.certificate.suffix == '.gz': + raw = gzip.decompress(raw) + result = check(json.loads(raw)) + print(json.dumps(result, sort_keys=True)) + print('PASS_INDEPENDENT_CK_GRID coefficients=103 vertices=' + str(result['vertices'])) diff --git a/research/ck-grid-synthesis-seed24/synth.py b/research/ck-grid-synthesis-seed24/synth.py new file mode 100644 index 0000000000..c63fd34e25 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/synth.py @@ -0,0 +1,37 @@ +"""Finite CK single-scratch grid synthesis. Eva Ayala / ToikY + Codex; Apache-2.0.""" +from collections import deque + + +def edges(x, denominator, bound): + options = [('add', x + denominator), ('subtract', x - denominator), + ('double', 2 * x), ('negate', -x), ('clear', 0), + ('copy', denominator)] + if x % 2 == 0: + options.append(('halve', x // 2)) + return [(tag, y) for tag, y in options if abs(y) <= bound] + + +def solve(a, denominator): + if type(a) is not int or type(denominator) is not int or a <= 0 or denominator <= 0: + raise ValueError('positive integer parameters required') + if denominator & (denominator - 1): + raise ValueError('dyadic denominator required') + bound = a * denominator + distance, parent = {denominator: 0}, {} + pending = deque([denominator]) + while pending: + x = pending.popleft() + for tag, y in edges(x, denominator, bound): + if y not in distance: + distance[y] = distance[x] + 1 + parent[y] = (x, tag) + pending.append(y) + goal = min((a, -a), key=lambda x: distance[x]) + word, x = [], goal + while x != denominator: + x, tag = parent[x] + word.append(tag) + return {'a': a, 'D': denominator, 'bound': bound, + 'states': [{'x': x, 'distance': distance[x]} for x in sorted(distance)], + 'word': word[::-1], 'terminal_sign': 1 if goal > 0 else -1, + 'cost': distance[goal] + 3} diff --git a/research/ck-grid-synthesis-seed24/test_package.py b/research/ck-grid-synthesis-seed24/test_package.py new file mode 100644 index 0000000000..bb5d2fdc95 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/test_package.py @@ -0,0 +1,98 @@ +"""Focused admission and complete-word failure controls; Apache-2.0. + +Eva Ayala / ToikY, with substantial OpenAI Codex assistance. +Run from any directory with Python 3.10+ and its standard library. +""" +import copy +import gzip +import importlib.util +import json +from pathlib import Path +import tempfile +from unittest import mock + +spec = importlib.util.spec_from_file_location('ck_grid_audit', Path(__file__).resolve().parent/'verify.py') +audit = importlib.util.module_from_spec(spec) +spec.loader.exec_module(audit) + + +def rejects(action, expected): + try: + action() + except ValueError as error: + if expected not in str(error): + raise ValueError('unexpected rejection: ' + str(error)) from error + else: + raise ValueError('accepted failure control: ' + expected) + + +def run(): + census = audit.read(audit.HERE / 'CENSUS.json.gz') + reference = audit.load(audit.ROOT / 'research/complex-dyadic-lowering/lower.py', 'control_reference') + programs = audit.read(audit.DATA / 'LOCAL-PROGRAMS.json.gz') + checks = audit.read(audit.DATA / 'LOCAL-CHECKS.json')['forward'] + inherited = audit.read(audit.DATA / 'INDEPENDENT-LOCAL-REPLAY.json')['local']['forward'] + + # Alter the final target-writing addition rather than a preparation that + # could be cancelled by a later inverse. The complete map must reject it. + altered = copy.deepcopy(programs['forward']) + indices = [i for i, event in enumerate(altered) + if event[0] == 'scalar' and event[1][0] == 'add' + and event[1][1][0] == 'L' and 112 <= event[1][1][1] < 224] + if not indices: + raise ValueError('no forward target addition') + altered[indices[-1]][1][3] *= -1 + rejects(lambda: audit.replay('forward', altered, census, reference, checks, inherited), + 'full scalar endpoint') + + original_emit = audit.emit + + def omit_clear(op, *args): + word = original_emit(op, *args) + return word[:-1] if op[0] == 'add' else word + + with mock.patch.object(audit, 'emit', omit_clear): + rejects(lambda: audit.replay('forward', programs['forward'], census, reference, checks, inherited), + 'work survived macro') + + # Pin admission happens before mathematical replay. A semantic source edit + # must reject; a gzip-container change with the same payload remains valid. + source_names = audit.read(audit.HERE / 'SOURCES.json')['payload_sha256'] + with tempfile.TemporaryDirectory(prefix='ck-grid-source-control-') as temporary: + root = Path(temporary) + changed_name = 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz' + for name in source_names: + path = root / name + path.parent.mkdir(parents=True, exist_ok=True) + if name == changed_name: + changed_programs = copy.deepcopy(programs) + changed_programs['forward'][indices[-1]][1][3] *= -1 + path.write_bytes(gzip.compress(audit.canonical(changed_programs), mtime=7)) + else: + path.symlink_to(audit.ROOT / name) + with mock.patch.object(audit, 'ROOT', root): + rejects(audit.verify, 'source pin ' + changed_name) + + with tempfile.TemporaryDirectory(prefix='ck-grid-census-control-') as temporary: + here = Path(temporary) + (here / 'SOURCES.json').symlink_to(audit.HERE / 'SOURCES.json') + (here / 'synth.py').symlink_to(audit.HERE / 'synth.py') + changed = copy.deepcopy(census) + changed['1/64']['cost'] -= 1 + (here / 'CENSUS.json.gz').write_bytes(gzip.compress(audit.canonical(changed), mtime=0)) + with mock.patch.object(audit, 'HERE', here): + rejects(audit.verify, 'census mismatch') + + # Same semantic census under a different gzip timestamp is accepted by + # the payload reader and the independent checker. + (here / 'CENSUS.json.gz').write_bytes(gzip.compress(audit.canonical(census), mtime=123)) + recompressed = audit.read(here / 'CENSUS.json.gz') + if recompressed != census: + raise ValueError('gzip recompression changed semantic census') + independent = audit.load(audit.HERE / 'independent.py', 'recompression_independent') + independent.check(recompressed) + print('PASS_CK_GRID_PACKAGE full_word_rejections=2 admission_rejections=2 recompression=1') + + +if __name__ == '__main__': + run() diff --git a/research/ck-grid-synthesis-seed24/verify.py b/research/ck-grid-synthesis-seed24/verify.py new file mode 100644 index 0000000000..97d9561875 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/verify.py @@ -0,0 +1,257 @@ +"""CK grid-preserving finite scalar construction; ToikY + substantial Codex assistance. + +Sparse primitive interpreter adapted from Sagar Thakrar's PR696 verify.py. +Apache-2.0. Independent graph certificate checker is in independent.py. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +DATA = ROOT / 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck' +WORK = ('W', 0) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def step(rows, op): + tag, target = op[:2] + if tag == 'clear': + rows[target] = {} + elif tag == 'copy': + rows[target] = rows[op[2]].copy() + elif tag in ('double', 'halve', 'negate'): + factor = {'double': Q(2), 'halve': Q(1, 2), 'negate': Q(-1)}[tag] + rows[target] = {j: factor*x for j, x in rows[target].items()} + elif tag in ('add', 'subtract'): + row = rows[target] + for j, x in rows[op[2]].items(): + value = row.get(j, Q(0)) + (x if tag == 'add' else -x) + if value: + row[j] = value + else: + row.pop(j, None) + else: + raise ValueError('unknown primitive') + + +def emit(op, census, reference): + baseline = reference.lower(op) # Retains all domain and alias checks. + if op[0] != 'add' or abs(Q(op[3], op[4])) == 1: + return baseline + q = Q(op[3], op[4]) + entry = census[str(abs(q))] + if entry['cost'] >= len(baseline): + return baseline + source, target = tuple(op[2]), tuple(op[1]) + word = [('copy', WORK, source)] + for tag in entry['word']: + word.append((tag, WORK, source) if tag in ('add', 'subtract', 'copy') else (tag, WORK)) + word.extend([('add' if q*entry['terminal_sign'] > 0 else 'subtract', target, WORK), ('clear', WORK)]) + return word + + +def macro_check(q, word, expected_cost=None): + t, s = ('T', 0), ('S', 0) + rows = {t: {0: Q(1)}, s: {1: Q(1)}, WORK: {2: Q(1)}} + a, denominator = abs(q.numerator), q.denominator + for index, op in enumerate(word): + step(rows, op) + require(rows[s] == {1: Q(1)}, 'source restoration') + if index < len(word)-2: + require(rows[t] == {0: Q(1)}, 'early target update') + coefficient = rows[WORK].get(1, Q(0)) + require(set(rows[WORK]) <= {1}, 'dirty work initialization') + require(abs(coefficient) <= a, 'magnitude envelope') + require((coefficient*denominator).denominator == 1, 'fractional grid') + require(rows == {t: {0: Q(1), 1: q}, s: {1: Q(1)}, WORK: {}}, 'macro endpoint') + if expected_cost is not None: + require(len(word) == expected_cost, 'macro cost') + + +def replay(orientation, events, census, reference, checks, inherited): + n = 716 + rows = {('L', r): {r: Q(1)} for r in range(n)} + rows.update({('C', r): {n+r: Q(1)} for r in range(8)}) + rows[WORK] = {724: Q(1)} + env = {register: Q(1) for register in rows} + peak = Q(1) + paid, tags, changed = Counter(), Counter(), Counter() + old = macros = new = 0 + word_hash = hashlib.sha256() + for event in events: + if event[0] == 'climb': + paid[event[5]] += 1 + elif event[0] == 'center': + paid[event[4]] += 1 + elif event[0] != 'scalar': + require(event[0] in ('phase', 'adapter', 'residual_adapter'), 'unknown event') + else: + op, frame = event[1:] + target = tuple(op[1]) + baseline, word = reference.lower(op), emit(op, census, reference) + old += 2*len(baseline) + new += 2*len(word) + macros += 1 + if len(word) < len(baseline): + changed[str(abs(Q(op[3], op[4])))] += 1 + if op[0] == 'add': + source, q = tuple(op[2]), Q(op[3], op[4]) + peak = max(peak, abs(q.numerator)*env[source]) + env[target] = env[target] + abs(q)*env[source] + elif op[0] == 'scale': + env[target] *= abs(Q(op[2], op[3])) + elif op[0] == 'clear': + env[target] = Q(0) + elif op[0] == 'copy': + env[target] = env[tuple(op[2])] + peak = max(peak, env[target]) + for primitive in word: + step(rows, primitive) + tags[primitive[0]] += 2 + word_hash.update(canonical([frame, primitive])+b'\n') + if op[0] == 'add': + require(not rows[WORK], 'work survived macro') + for r in range(n): + wanted = {r: Q(1)} + if orientation == 'forward' and 112 <= r < 224: + wanted[r-112] = Q(1) + if orientation == 'backward' and r < 112: + wanted[r+112] = Q(-1) + require(rows[('L', r)] == wanted, 'full scalar endpoint') + require(all(not row for register, row in rows.items() if register[0] != 'L'), 'private cleanup') + require(dict(paid) == {int(k): v for k, v in checks['paid_profile'].items()}, 'paid profile') + require(macros == checks['scalar_macros'], 'macro inventory') + require(peak == Q(inherited['prefix_l1_upper']), 'original envelope') + require(peak < 2**inherited['charged_payload_bits'], 'charged magnitude budget') + return {'columns': 725, 'dirty_helpers': 492, 'baseline_real_primitives': old, + 'replacement_real_primitives': new, 'saving': old-new, + 'changed_coefficients': dict(sorted(changed.items())), + 'primitive_tags': dict(sorted(tags.items())), 'primitive_sha256': word_hash.hexdigest(), + 'paid_profile': dict(sorted(checks['paid_profile'].items())), + 'retained_original_envelope': str(peak), + 'charged_payload_bits': inherited['charged_payload_bits']} + + +def controls(census, reference): + q = Q(5, 2) + op = ['add', ['T', 0], ['S', 0], 5, 2] + word = emit(op, census, reference) + bad = { + 'missing_copy': word[1:], 'missing_clear': word[:-1], + 'wrong_accumulation': word[:-2]+[('subtract', ('T', 0), WORK)]+word[-1:], + 'endpoint_neutral_growth': word[:1]+[('double', WORK)]*5+[('halve', WORK)]*5+word[1:], + 'endpoint_neutral_finer_grid': word[:1]+[('halve', WORK)]*2+[('double', WORK)]*2+word[1:], + 'uncharged_redundant_ops': word[:1]+[('negate', WORK)]*2+word[1:], + } + rejected = {} + for name, candidate in bad.items(): + try: + macro_check(q, candidate, len(word)) + except ValueError as error: + rejected[name] = str(error) + else: + raise ValueError('accepted control '+name) + require(rejected['endpoint_neutral_growth'] == 'magnitude envelope', 'growth reason') + require(rejected['endpoint_neutral_finer_grid'] == 'fractional grid', 'grid reason') + require(rejected['uncharged_redundant_ops'] == 'macro cost', 'cost reason') + return rejected + + +def verify(): + for name, sha in read(HERE/'SOURCES.json')['payload_sha256'].items(): + path = ROOT/name + raw = path.read_bytes() + if path.suffix == '.gz': + raw = gzip.decompress(raw) + require(hashlib.sha256(raw).hexdigest() == sha, 'source pin '+name) + reference = load(ROOT/'research/complex-dyadic-lowering/lower.py', 'pr696') + horner = load(ROOT/'research/dyadic-horner-direction/lower.py', 'pr837') + programs = read(DATA/'LOCAL-PROGRAMS.json.gz') + qs = sorted({abs(Q(e[1][3], e[1][4])) for es in programs.values() + for e in es if e[0] == 'scalar' and e[1][0] == 'add'}) + solve = load(HERE/'synth.py', 'synth_ck').solve + census = {str(q): solve(q.numerator, q.denominator) for q in qs} + require(canonical(census) == canonical(read(HERE/'CENSUS.json.gz')), 'census mismatch') + independent = load(HERE/'independent.py', 'independent_ck') + graph = independent.check(census) + comparisons = {} + for q in qs: + op = ['add', ['T', 0], ['S', 0], q.numerator, q.denominator] + word = emit(op, census, reference) + macro_check(q, word) + negative = ['add', ['T', 0], ['S', 0], -q.numerator, q.denominator] + macro_check(-q, emit(negative, census, reference)) + four = horner.candidates(op) + comparisons[str(q)] = {'copy_binary': len(reference.lower(op)), + 'best_four_horner': min(map(len, four.values())), + 'installed': len(word), 'bounded_class_cost': census[str(q)]['cost']} + checks = read(DATA/'LOCAL-CHECKS.json') + inherited = read(DATA/'INDEPENDENT-LOCAL-REPLAY.json')['local'] + result = {orientation: replay(orientation, programs[orientation], census, reference, + checks[orientation], inherited[orientation]) + for orientation in ('forward', 'backward')} + baseline_receipt = read(ROOT/'research/complex-dyadic-lowering/EXPECTED.json') + for orientation, events in programs.items(): + require(hashlib.sha256(canonical(events)).hexdigest() == checks[orientation]['sha256'], + 'program semantic hash') + require(result[orientation]['baseline_real_primitives'] == + baseline_receipt['programs']['ck/'+orientation]['new_real_primitives'], + 'copy binary complete baseline') + for orientation, events in programs.items(): + saving = 0 + four_total = 0 + cases = Counter() + for event in events: + if event[0] == 'scalar': + four_total += 2*min(map(len, horner.candidates(event[1]).values())) + if event[0] == 'scalar' and event[1][0] == 'add': + q = str(abs(Q(event[1][3], event[1][4]))) + c = comparisons[q] + if c['installed'] < c['best_four_horner']: + saving += 2*(c['best_four_horner']-c['installed']) + cases[q] += 1 + result[orientation]['selected_occurrence_saving_vs_four_horner'] = saving + result[orientation]['strictly_beyond_four_horner'] = dict(sorted(cases.items())) + result[orientation]['best_four_horner_complete_real_primitives'] = four_total + result[orientation]['net_saving_vs_complete_four_horner'] = four_total-result[orientation]['replacement_real_primitives'] + return {'status': 'PASS_CK_GRID_SYNTHESIS', 'magnitudes': len(qs), 'graphs': graph, + 'programs': result, 'comparisons': comparisons, 'controls': controls(census, reference)} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-certificate', action='store_true') + args = parser.parse_args() + result = verify() + if args.write_certificate: + (HERE/'EXPECTED.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: + require(canonical(result) == canonical(read(HERE/'EXPECTED.json')), 'receipt mismatch') + print('PASS_CK_GRID_SYNTHESIS magnitudes=103 programs=2 columns=725 savings='+ + ','.join(str(p['saving']) for p in result['programs'].values())+' no_new_kappa')