From db410cbd344bcf58f754689ae893d4c31a01f32d Mon Sep 17 00:00:00 2001 From: Hanson Sun Date: Tue, 13 Oct 2026 21:40:50 -0400 Subject: [PATCH] Research: common rounding dominates static Gaussian helper gauges Add a scoped scalar-cost theorem, exact one-helper census, literal-circuit cross-checks and source-bound negative controls. Prepared with substantial OpenAI Codex assistance; no new kappa or supplier admission. --- .../CENSUS.json.gz | Bin 0 -> 18115 bytes .../CERTIFICATE.json | 570 ++++++++++++++++++ .../INDEPENDENT.json | 32 + .../README.md | 247 ++++++++ .../SOURCES.json | 60 ++ .../TASK.json | 132 ++++ .../VALIDATION.json | 55 ++ .../VERIFY.json | 47 ++ .../independent.py | 170 ++++++ .../k8-gaussian-unit-rounding-seed24/model.py | 400 ++++++++++++ .../test_package.py | 101 ++++ .../verify.py | 237 ++++++++ 12 files changed, 2051 insertions(+) create mode 100644 research/k8-gaussian-unit-rounding-seed24/CENSUS.json.gz create mode 100644 research/k8-gaussian-unit-rounding-seed24/CERTIFICATE.json create mode 100644 research/k8-gaussian-unit-rounding-seed24/INDEPENDENT.json create mode 100644 research/k8-gaussian-unit-rounding-seed24/README.md create mode 100644 research/k8-gaussian-unit-rounding-seed24/SOURCES.json create mode 100644 research/k8-gaussian-unit-rounding-seed24/TASK.json create mode 100644 research/k8-gaussian-unit-rounding-seed24/VALIDATION.json create mode 100644 research/k8-gaussian-unit-rounding-seed24/VERIFY.json create mode 100644 research/k8-gaussian-unit-rounding-seed24/independent.py create mode 100644 research/k8-gaussian-unit-rounding-seed24/model.py create mode 100644 research/k8-gaussian-unit-rounding-seed24/test_package.py create mode 100644 research/k8-gaussian-unit-rounding-seed24/verify.py diff --git a/research/k8-gaussian-unit-rounding-seed24/CENSUS.json.gz b/research/k8-gaussian-unit-rounding-seed24/CENSUS.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..9f58e3291fdd33edb529e17601d713c55e08c43d GIT binary patch literal 18115 zcmV(vK`|O=eNxUpBF8=o~|M}Zr{?GsW?VrE@@*ltc_b>nZkH7ubAOHO2 zKLFzEm%sk~FMs|0kH7!>&%gct`@eqq4-fwJ%Rheq{m=jT$G`sl`RTWRg#dr5|F^&V z_V?fa`ulJH{^Rq5zyA6TuN>T;UcbKKg&Fq$fqwW`_X^woU;m13|1Z3XbAQ@@%m4lN z{xSai@8ACVw?F^uZ~yqOKRzD=)9aUi{_)%2_;0$`=eO4XOZOK)f5@f!hdko(huraJ zN;&>YDEt36ywc}W{ONyQS5uQV)urB4*qmi*s(<+NH#V%F;P~O))R>OXfT@0n3}Bk- z7fcOM$W(td)jL;hjd<7^KYzBfHEUa=KGv;Rwr-JZO`dE$e)#hdVyGV?yK3v_J4DOa z;1-OHiN95!uEyqieImkPZ26peXKYc%LTGH=KkeAk&*u+xZ|N*^A@eMwqI+u7e)lhy zs0+F2L-H$cFJ*pv5&O4S|71O^&xOqO%iE4OnO;66`!T}G4dqwwV{>S!9vb@kcaz`0 zReY7O|2Kbr`tz3BZzH(D^Ni|w7PP*NSm@gb{B0aRynh>XWiixGm5yinxk@?JZzF#0 zviV-|`L_X?->bVG{6?+`s%wgX^-Bo*C2PL~Kll=|`Vyk~ZqxBf4lhXubNuk}jtO1KnVQc$Ru}yF%6;N9rDq<<@Z&~(E;2gX;tduo zW?!6}vvr9sGF@O$fhXX=r>Rp8Xujg?$XHB{zH|!n;?uTdUf{5DfeYsmp>bVwu9%dE zickDCY=&*S_d9I+oan|Uy77r_WF!DxW7f%3(Ye%qUyR3mxZvZa@i*WSeK73w#RMzTrYTH&`Fni@{-1P->=2&W=PUN~up+Jq<4oz<5MHf2n(io4FL6Y;z z$5YrtlS-e1&ayV`zOx;k1K)Yz6VG(#J>B_8;W;PUiLJP8zFO%Tj6LvqJ2G9p^HE-= zE_d+G_Fqo%jOW1=jUG9%dw-d3jl8CV<@z7?^6poKivfu7)>wPv3l8(?P z&=a@jef`^?^b+WvCw^*3zO|N2?C0P(Ys>81CD{J;-t#KMqvga&F#B_W>v;xlG5cUI8Rmcl@4TVU~ynSJV|a zyzAKf0`$d4@7iEOSAZOg4;0pX@8D6VExCR1pMMRe{i$$Z=NvUiSfgN5bJfq4DD^=e zzwPr`YId`I{`Y7)`cF>XejV_77yCA#+y=>T+7|)!79PLj^AV~?M5;=+AlI9m9|02fJ18-+$&%ob$+c$KkDC%6 zq(G42JBclF_3!8}maEB`!73H}bXt>r|MHWW*&#zPHHq2J7TX68l*v~}< zPYWSG^9vK~&o`zcg_+!Y^5}0L`R6M${dktdj;=YCYm`;f9S3~;s6RLKcrupz=DQ70 zni%Hkde`?>?{#M>3@mlpo!K6|2GSk*FI`x#b^7Oc6Mx-wyl&#o7LGRtac5k#HrNwN zLetqiz?xG3f+sP{xelQ~aIFKcPnuyFI4-zZtu4hY&RRAO*l;aXWBqfP(x%V{uQ))S z!1Xz7G)?!8(V1Mxb}CstVW*CeW%@P0*0*QoC<~{ZuylA(3#uY_T6&uYSsA9z=EL(C zHUrzd@qJ6&a;gZ8qX&3#U^W^9{ds@hsh_y8#CcH~LdkD>;yx?KJxElbuU8IW$LMac z^Guu}i@PR7RZtg~T|p;A5aCkvExBhczi<k+ad37N1G?IIqgNkOS8;O$2Wk!j zRVHx(iu@c>n#42D@k|c5!Q793dn9iakg4SX9yvhwedv6q#6DR~=1V6K>Y7gpFheCV zWKLjdxBVIig?WBvj|d)Jg_RR8t{%*vcvjqTtgdV$P6+F{eiP4ZWRI*T^w40;~Bujc{?}AUS=sebPbKe zyI#{5`Ua@U0-l^V=&CHG+gfD`Hf`B)B;n*$n$`?LGX!5i*h5cCm5((x0w3kh2^j<% zcV4I~Pk^VgJ>N1v_TXbCIvYpx92sPc!bRf?ffT|h(TVOc;bU(h*w}MSg7~_j@kC!z zZHJ_@yP})P$;O;f(mM{^jJVhC{ps2QCDOZ#vz~lfDAg!K*q;+c(T4n!tk|a0wv5WP z*-g~I^gC(vWOi-jQn_F#whND-UE2g%%Q!;NDMxs#L(L-+Q&2g(nS^CVF(a2@A+-pa zmoPPj>(R=T#Q?N~0Xk%t4M4T95;Cxd|r6ws;iS}bP5r#ppFiqGG ze1$+N&cZF~9Z1r4CVGpy3%rh$qopgfRiWEFVZu}At;0F$N=>a;vh5D5M{AT%$X8nSO9 zY1UjhzVZ=Q{r(yCd$?tTxEUcPOFNM3Fa}gBF~(C-!W}Hmws1zRR^*Vql6*k_%FUO7 zXV2hsH;%U%4}h-w0v@$W?8g!Mf*5SrN-uTBebkw1GJU zzTpsrD*zK;rRMSn2UUG9IzndUH=$UB^dLAPC6cvbJ1aM|p$Wf2PWKI+mH7w?Y%K$F z2=wVW*e%jeoMcK!q$d{{bn)$D55!2Qq2m)Z#R=l1Z5DOH9wuW3{2@Zi5uxX{Q3q?Q z4j>)p{yFdClkMjnRNK7Z6D}m!HGAQ7TKqG?VbWaNxNS;oh4LLnq(4bx*ZiFw4`DO) z8%T;YQ*<4lu)pUHZ9cbSvr7w+QMpce0`n&J7*L&3N*u9gPa&+ZBSRXnVK+w=EBV4y zgF)Qr?fam3u_fJO8{lo1xN*mEOMMxiQrk+WB4q#X0-}MFQZ`DTfB~I`Hgf#i1J6)a zk1F`SRWZ2=xd>LtWe*bvBKba>*bW1-7^cbi*sx#zRy5F3?r8gy=(Z>NrRyRJI>kYa zzR$hI`VG=P3I(N^7Gvs*x~rRelHc1bSEiCj9!n6kMQ{g{d4X@F^XP^J3^Jdvw{L`{ zZ|YW>etBamV`5wjIV~xCE2%=wlP;ld36(NQ(Oui3<6^uBnWr-n@2KfCA7kB8*B_$C zW~c_XBr^fuAfksN&c*452!n*G;Mn4W*J$$(=?E`lsyrM9#6J{11E#OMMrky3>2+f6 zU8OOo^Gvs{)YaaFRdq`)-7)WK!^4yN;VIU%Gf&fF-#WFJCn;O7jQb5hqXj!Dy0ck_ zkE{|*i^XvDd-P3L${i1qGKb|8;PM0)#D&DUopmH|)l&kU>L^82;NUizD^SS+nhtkk zpf?LIrSIsW6Hd-?w83s>eSTJ_&33sQ`EWxs+W4lrDAQc$UdA_82dASJL>GxRbK2J?*z?8P-b~Tv*j?$$y+qcgCEIp{U|-C z*S8$hn9fjmfN4)!(kJvO2?JBID;f9#2y#a{(Eau3R#0x7)c2`$)4^^0dE=EX`?<+3 zm;Q?w6v7TwK2h#D@Y1g=oYT{hJEFyg$#{&1rF54Y3E-ehck6?7%FIDIt1^no1o9?n zA?Lm9mLs#>$xCf^JF37B405)@0TkvG%lQx`=)=v{a|!~Q;U>8bu|vv~xZ51;2b*9a z%#@_VXrCAzqcS&qUK)uqZe>!;KLSQT7z0k4rbif!&nf%+@XaLK70HK|{}UkvGFkU>WYT2FW%L@4f3iQvo(>XxxN8ejY_xc5J$LrRP2FVzV`npNlkxbt5=uE{ zccbIP@9?FcAPzo00a5M7@TUf#XPTKTDQvOQpdhO3G!b}O?La=Ls^J1*a{1k#?x1Cb=a!X1YhnZ4G3ShfCm9Mr4LSNed75g zVsmWI2MlI&qD{-M48}wE|8_PGntbuOYdX7}+*1nVF91*1WZI@*C`@ciWA2rTDd6sG zauxF#-_e-mxHwB7qBIrTQ~YG1$cBbYM@Q6i6av5G-Xgfr0p1!3Bs% zk_sB)<#S?)2PPOm*7o=^$+{bRXnIrGQ|^0T-f9kTQ~#0%3OjcqS+vy9Vs=sP#>P4` zw1Z3iHS?R@sy+!Nshx74lyV``*W~|UqM9`T z(!egr<2eN04&~R2td3|Po0V0G6YQKKrVbosjAdbpXSg{X3=H%8z zwuq|>Pjnfu+05RrV7uP69pLWcj~uhA$ZYT+Vo!D~Z8?p$!~FQMYR!5vw|&x_0Twbf`CwMEn~^{IgGF=`&e$Px`yrOe#)=8cH>5>y!S?F$0DxZC%sppQCiG zuUF0y;dZXo)vwLK@*87l*LPWZZkLOyaCM#VUh|yA8~P4l|vx1trX@@Tknc_|nsefV!eQ2#YUWQjb)K z!iqv>W+?0g{Rt~!Z#7Aimk<)3YHZR=@6_q)*isZr7MR~NV$xFj$?}_ejSO##m}Gi z%Gs7%0CUE2#8>gGktHfI!L{grKo&z}$!GT%zkJWCy3b>aBGN`K(le0pZXT>FyC2z%9 zWb`3E*SVUrc`uOOh|T*}HV!IARC7GRgrmJ@)@lhd`<5D&X%_Q}6ZE~T=%O`2xn^#_I)rk?h6I0SiB9iT@t;ufth3D#IyWV=OANG6&c<6yMrvM{`0M7@U)E!Qb@?JBlCgvDQ z-pf*D+1*n826=Co)H2xCpe!%kTQr!3Reck?I1@@QtLoN4P@a9Sk|Soiu)=WjLxvlf zrQoTdPDy?|<6HJd;&D@R9l!bfPw`W3r+SmJXf<&M^d!P@*3WXYbe9qZ`fZZ=K3CW! z_Q>(6GT(2~y9kWb013~%>52Ekw6)d>2m7G?_U`penCfikva%{Ivbf5HYDJX+g4Db} zkA(#qO6m;J>b=$YiA_zN~H9y&Scnn~?}mXb+Ynvv}GzE3M7L(RA>^Fjg@ zHl^0=v7ZkJ0~L=2Rg)_`%Y?B`!er8P8cCM~8~*PAB}!O|vIy_`PB0sIh+L`3G8-vY z8H4aw=?XlCPM$WR=5igPDA%jPid@GrlF&sv^Y@>_{N5t zbKOl>X~*qp_9T&sAFH*${wrp%1%z-m}bY9=9% zDl0XUV3X9nXJ%{>2_tUorM7m&i7MVeeP%M-mpJj_wSnzypJv7m1QxPFa_seRQT7#z zhB6OmQh5LqDT(+a>e~&xEX8+kmM(fyP_HZ9?*Wq_>ameCg-OB{R=OM0k^60Xy_Bwk%hbF zrk_qQ$S5ARJx!PZkYQvj~^fO>4Q&ppPn`8Gh@Y(2!R1wo;yw$p({Owvo~Lg zo+|gMOFIw<$WFml_S`Y|zr)#f!nSF`9(aN{_KY@|fgM5?X`(O%;kPlM9%Y>28fkqvp%_uFXXxY%v*dX#6LAQiDPAD>x54Xh`_xAd2 zusF~)$SPL^dx{u(Y7_H-@;7D_`wF_}-QhsK;6NUpZI{@!+@vK#y+)#D$u0?)3?B|A zGGLPKZf%Jo`|F@LYJ@B*qwMgdR63cR%~IYl;lPH0QF+!HZ?}LDVP5gGaU?qs^s*DX zdB*NH@+=Ut7&f>2VTorJC*89~8KwTHP7HA%F_3yy|6&i%oC_*wc!sr+sb@9;MS~7p zlQZ%yeSsw+vbuNiPK3$N()P$h4S`|agq^+=Jl0sN>znnZ=G_EwxGF-CWN#jA4Qs zDujk=ll@cTusmLQFyE)z z$uKp|zJ5R#{b)q5N9v>b%o0~e5|Ig>XKnb2E@T+Y<;~`9T2XA)*L?RC82a1dA8ZBu z>y*C;KDkq==3&VXlg(<)j`#Y5odMyly#>dwFg}0kx(PnD)ajXC)u3*igx@w;alzR8 z2!D&(PB4o`sFO>o%qclEN(7Va&u_3Y1bUHy84ZDgGBMtpXr_SIr7*G>WotE3I2YVq z{(_0Ks*$z4p%sji)la>N=`JU9(@|uZbM>wT(l+?Qj&&e^s)l=1*A9KYooMot>^32` zBor3nER0E($5Ts3U4c*8xt{j`pmO5nfl1ccVAWD1hK=wdQ^UaAZd(dN|@|K-oE^H|ouFOm%f@XWm1cZV#SfUwhI|ZnOZh2_OkV$(waLwY7E!+`spfMD~4uk^3jw;QNn4t4FrWibyy}GNWG2Fu$AY#qF0B%?32B^rLB16eV1H&nj6FM;h!2dukgRvD zbnvKApGpbrlC0rz;}+Pd1X^G5rbQk;su%bOF0sc;WRCM3W5qTi^6Ec_E3ipKd%i?Q zY5ZUg;~kYF-R?vE1P&LvIn({bvdEUXm0%xd-HJvsob2h3EVu`R0t+mOyV5z=L8AA` z3fhFY@{w(@#Iq{4lPNf!Q01y$hlYWwQR(si&Ge&NqOq_PT(@35K+6i*n4n!&NFnx4 zR2j2w7VP10Cu+~R#gWcYc;4kWsWvqA;d5%c9O=0@+7c^Y-ceKCW##e) z8Ay*eST(>Y5AH*^=Z9|dqzmfOV{TmEcA~V(t4>YOxklHe=Jz)~9^khk!W{fqJ*EHN zX3wq=t~?W;ni)Ffmqp@0{|eK?WRC@!+o4*rhj!rDqYwk_+cTvrDluM!B}=ayLY1V^BR+gYM>D4vNb1!c|R zS8@UvDW<7T%Rt*D^f^v4Qvz!05%@yAh9gagvr)=~k6rcEGZTGxPX`V+lpOo^!plh zvr5XiFtyTc{N(ZULlUP{)xDyCiGdDH*A;wENu_e7JTuZ+B%9^;Hq*N267!wo_o60! zoTPG`1L2vVl!?4OgHIXZCGL1q(D#u8fqiBx*}8|pQa0r`6Wkq=ovi}}ugei}lI|*a zJdr$GI-#Ui{*Pkjz0{PJy{exGDr32^G6gC@n<5wAsmQPFava^(@OEuNvB3 zN@pP6pIC8bq$2==Nf@WZ>d&4Ne_%HpL&WqTA1wBCipTb~5c0r_S3ED>rakwxw&CM? zZ68t63V6At0e1PWf6dc^Yf_o`_)C=z4@7gY&rh~V9Vsga>&M`JEOjtyFlQ_PXQJ8# zAIq&M*pKFADah59RE3M9mc_(@h7R^Knf9Cnh{7z5fXYMxpSUBF(?TT;6VhBuw*t84 zY1|A`P}D#}C+LC3Nu9%mwHMJ*=3)60@L;W(ich8QBy9Benm!=m#~l7rz2Bg(^Y$RN z&rlx6zLnlJJumN2Qn;TE9G6-ZI%<1s%|Iq-F{ra-pRgG?s0VJQz*mC0uogNQ#m=5V zl2TSKrBn}RlG0zwBDBYPDa(;!XFJ7S+9=E4V;EEuq(WY!F!KDsr+VwR9AYkap#9qh ziUW03J|Bmho|Fb}XSV$izMt7Dd$s3BdRs8elIg$^q=AR%NU>ZfcK&0n&9TcXNQ5Y# zT^&riRwj*w1JM=;4_nliB#np^<+4r1*UhokSuMyowjxi}lBkNifliCQcEz5h=6;K0 z*VM2ey$>6Yh)XaY3;^(6a|{O(EumlkVdpKEpoR_lVABNBf&fMny3{FzyS@q~6L&Q> zPa80FZLMQ-j}twYQNms`wh{SAe3Z+vPI0qwiG2lv7sch^6)giwhSl^}Z@lwlzv) z2l5qqNx|fhm}()>h23yD_2T?g7JNlE%d_}vgkJf<4-}Dc8yS#LuDXT2E&H5D;102XvZl$*% z+<7yitXS?08deKmuFEEnFZi*j#zDhz=A9{cXUYs;IUREguS_!h@`KMKs81e$oG$?! z=>^#PCQG6xM?n9{^OFo~;+#^K9Qw;Tq@T~Q5>8fN#=(58o(!~=)gupLhtQ3&2Y1(; z7!3s0UY?~H*77DDd8A(MI1UCnAw4ZTfWH5;-jG(IUDU?~6u;Th(W8aY-#!DNhsK04=2^wGByoBzVM-aKJYpFBT-6(-0RYajU1x3d^2 ziue^YfqT8pLO>ozQm$z*lBhDiS?f`#bev>3cNY5bu*L036=#%GTm4UiIx z?4CY^2_?8oSNkhb5nr;h5-_jcldloRj=KDlc@xn24{E;ZX0 zv--+Mgp)p{vuWVod4re#_}*VIJE*B{-YzKF>*o9x8;j2fS^I-tw|nT5YpwEEvq^djI(G z<-K=I%PmP>e_z7N0!B4%FA2(s)q4fyOLE7~_Q zAowS1(c}Fp0ui|<8Dyl~H%<0+t<1Tg5a(OjMVb)bgF$B*JlKuoOp%?Oc#U*P{nkrf z4#?ZBB5&0G#*!rDTOE!K6?F=N(Sk+;nwK1dGCe$4FA?q6j_2MaR>+WXQfS1{)pH=1@TXeOI^PNN@sxn zeDvx@50p^S(|r|wXK3-3Sd`T_tcT5;0}|`)Pga3F$4+)`Ew5J#0@E~TTx3z)K3oq5 zkhg8+{br6$g_l5!6Jwf&q?G)kNzW(Za|z&iYznlgH;2UggWX8|hL)p2QBS+vEzWdx z9?{UEV!bUCF+$IhrF8A7)}FL={kFhNkGudl2&UM8_^f@H)KlMX_tv_)!o#@V!Slde z?1fB&XY3crpFLk;JHOu>k5D2v)mrHhhB87AQo&$M*awwK!-KshAd=Qpxg#-16Mfkm z5YjipP6wQ1hA^QpH7hfjJ@K(0fNO}Q-v z3yV3 zoXTnAWHSnfZK+u4BOrB$Bi-&yq13wxQiDH25yv68T9br?%H%LQ7r)+VYL6O;Sne%~~g`J~^?Yi7Hvpygh`^~rn8x0~m9oX5E3kh(cmhFHaM z)0o2s_;~f)VF^yCFp14=7yAYV?h!OOB(?inFh*XqV3;f?}v40e=8wy1}((Uce{3nHsMy_CD5`rtZLfr*D|1$ z3<_JEjFB=&^3)+sjoNdd4-;{%c#XE~*qhlb@3utaMJc6!8R>o-z#;!;$2pERL6k=b zl}D1wPmb5j!Q*uR^A;LUf($d4-p3`l1tocRy`fw!>9|xTB4N!Tohxt3VKN0*?`*AL zg;Ks}3u5pH)bueDr*VwgwCYO)$k*+7wY%JXB|5h$QKhcQ<~+(5Q8;bo6+js}e8!RB zm94?F!UyJ5s^$2D;L%4$gX$^clQMNSn#(AmXu?qQi`&FOLQh#LNhf^Ix5v>iyt9h1 zfzrxWRE)Dah)1J`y*O~=RK`qr?}l_03G+!5+KMe>2hNR>nHeHaHCZ6>i~Y;MGs9`V z4#tHE|B2d-r`y7XJJVJok6rf~HpbhK#zl#-g*BVqW;Gk?FT+OY1IvVP=k486w@zBf zVZ2J^Q@*8#u$ZXDj^rdKb=vlI0LIgbtbM_4Atvwhy?IB=0VYxc+?Ifm)g&MulR9#p z?G@E?J!|R4)H6xB^=qBrZR8tBg9WLL#V8w^yh1V``16(Em@PC=*eHqST7$V!K$1=`XODTT;0 z40+(o3fzUOcY#rS)<*iftwnE`tt|rS=E!z8?w*p3NGWGZxA?JIUv#|0N$SbUP4BjQ z%18?}Fk?UK40({CIo%quu_a`fR2Z(Df(8oDk!DjfJ)#XJ;c5joA5v<06=opGn$%Bc zK*rmH_Vx8yxH&Ct`edg_K|65J7HxarZE8^3!!PLzyIc295jWyfo}G&{QeNUUZv6&w z$mzZ<2KHWfeGQ=LJeRb6&=5=3;#74&yi}ILH@}3BZ z%Kj}pmnJhj@NP2sj0TA;KkKQ?9t_e|m2xidF5q(`QR40*Js93-HHmxAyDP_osXZm+ zrCsn!tyBv;O`3JVK139E+fsekC7$Mkp=rC%gDJ#l!jpE(--HY$5bK86O_dz{i5msK z&}a2WZ;zj^@1dK}R(X{65fdRQCc;2}DQl++_QDH(q*CPpaN{u%VB;R|#F--Wd059P z(!fB=$b(AX%|dW-I{HE_^x|y^GUKYg8$5G_ovw2cHn#?-jprusoRcONfdAB7VGB>t= zego05ZPVvyuc%?FA@D>8&*=o;og=s}P~0zha4dty3hQizq7F1Zd6PEvHK1ZhP*KE# zW;_bJpX<-R$v`807kXcZRPg4*K9Fqb-lh85`!Fb7G-V!MGQa_{Y&mzd5Q?a&l*e9n zI>F$#UZxnz0CNipI^T38$vXSAND=$WSK#`BGfi0|!am$Hht?OIDe-%I9qj8E=)*SH$#UA zv?`44LvW832yOey!H{XMY?C_3lFvTR4Gx}Q<7S6@cM&{^Arjzci2jXVh&34J8&4D>Ei_>Vt~ep-wW2{fcEIM?}}D9TP}VDQ@@ldJhX} z@cvi%kF^OgP-`1O8H#t?<2ivhUajnM7azshKDp#b_bqMkh3)Z|p2Rj%DNvB#p@q;# zpG}bz!el|FJYa11mkPX>?1#IeAuOO-D>J1GD))?GT7Y51)5s8R6r`%d>yV~EnQd6o z0)5!i&U%Y~k~)m!Eg)`e=f-#fwX5QScXuew9H9ewn{uR38tD4$Z+&C>^@OQM9J0`> zkp>S>n6r}-2U#8FEOB@q5V^!D_jJk;$6&&y^wOrp!OO&6Y$5n?+i<4o4U0{=Nv}#~ zJczV-LahY#O?C_~2;=Tu?l{`B#B=MQ5(pn3fv?3j^Yc4Z0$gNty|hp(jT(OH3bzEc zdYp~6GNdgk>Tlm9g;cF84n-JfTlQdjuzl6Rm__zh;-rB2u`Ow8roOPC9kY{SMKzwO z?`6;q^lj67Cc#zS(eOo42;TN+fxOy7kTO|F1O zTu?aYlCcLy%ve&be1)HtTe)yf2k7>xbO-PWxB5_!wh&Jt9CO%k&i+zT;nOsenc+})X|c@K5$g2P?&5E6es5z2sKQod~w0ag&`q@ zIrgd;7>IO5EhV1p5GzuROuiunahNFS`vr;5t(}JIU(HB(%jueJhBI)(Cdi;?M=YIb z5#f@PelytGx@o_u#}prxqPAHme)=?vx^2{*$t-A@)=E(<_j2#;_>#OPr_4-`W>xK- zhrwe<_71cd8mSVUv`dHPO-RoYj+%r>pWOf`0@Vu+&Stv-4Q}9zc%s6c07_x`7aZqF z&T+zfjw`g#PyAr65f4iSo*3c-?s^j>DA_9v1$2*^#*=ocpn#mb1m4Rh~eHlSLWAsatap=N1U2vyv}R+v*BT`KE`+JKQ}@E>?{xtUC(Z zZ(&eRX@}*^y-LCLbKh{5g*-lHmWK;s=TtY@7LotYviP&`c zxw89|I1F|4QBi_@w)%%7fgaRjMRuhX8B7-1DGOmova*mP@qVJ!Usl>p+#~f3$AJ>< z*y~z^fhx}c3!KPz@W2=dBb}Bnnuw@c4@Hlb!7Ud-{AeJt;KA^ep{#_iV!Kx~!kl z-!vifj?&*?mp4M%Xg33+vT87&tGg|eJ@q^lEsl>>tXKsYZ33uY+H^9K0TjZVKCY3H zN`5+djHHQjT?i0;zi*K8d*sd?@xZgA%XGM=#FIvO?|V-4RTe6MbY7)2l*uI~7EPAc z#x+tI9f>bQRG0Q^yH{Fql@n#eSuSV+nV{7Y(CSABvu*HxWw)Mpptr07$(Dtv%p1%l z70r4uX_U#a@~7N;5hR3G{dzWq@qF(gasn5K`rq)uTsPd?85@2|ZROIQQX(rz47Ax| zoROwVD7P}7@6f|domF_-q6+p%g^aRXlr@Co2fnRck!PG1dR9{&4^U@*r6^yr0xFh5P6!boj0_kUIpY^=YP6>-)P%sqtM^WOAG)9v8d7~qn)8SEOwg8b6h(>BTOM}lS{O~z#;d1!Jbx+qcg zA=8LWHz?I7$RKos793-dz?4L;eI{-L12ZQ8A-})IM$&^&vUOn~dXY8B)0O)HHh{LZ z7sx~`Oao~kF%hy*CS3_wN&!bZYk>ZW<~RMJ*YMT59A0>x<+YtE&(gS z+F5*F7#!eoth6AYlX>#aKpiHMd%D#Cn561ycfn0t+(`HnIf#ML7!5l8Cy6<}CrLb4sH<4ooV zFC^P0)ucP2Bx1rq=pk!p$6hpf&K^zZsY3rn4kX2zU!se(GD(dp5(ZoWgWNX`CNr?w1Rx-7u8>%6}fEd)}#3vK2Gc{z_ z4|g)0%B0wYUzskKe%TyO9Vj3SoQRF4g71gmgv`uBkQ2mV#fym8W$BdCI)loi=VnhU zo~;YOcEC+2mAq+SLWdYVw+XG~th;e22B31Rff&F5A$1Q(mZ9%KG08HP#|Y_6+v(J} z!%n55v&cU=IBzRB$Sw>oZ!7fE|7!=9?6pX;DM2*t8c9aAzA+5M4N_Xj8PBDPrO6os z@yv0u-y^KFCU7)bnt8HRnH6qZpkVut>u>;HKLk;f{Q1^rUvKJn6rc3-gUwb(5#XX75sZ+{B;HNtVIDI_vD{X8k~%AUlm}+47%TPcoNo3NIZBEO}%HFU5p| z84mJJgPkj^D6@Vt>zYdE4Si(V48u&eH(XgjE;INdrP{PeI4cHa;k~>~ zsADe18H#h1p(7S-4!ldd+)ndu0}0nOK_*$@=G`tBp-Hx&g7-*bVSr4=$+|=--LR#- zAu;ZS;9b_XO-#C)LU`-inj15`yTinRoaX4mX$IrT%7WWcJs0(Xo!0zi5s4*h5rP@()2C4A;th!B2qZJ?f1Yhg42INN0) z+c}^mSoifb`dgUb@P@Vz5q>B&e^`rZrYR6cesPjdHFalECWO20*dBV#6u!u28TRza zwe5+CC=ZN^%*nY3ryzBWzs{t4*cYZKDfX0e;Qa%c_Z^mHanYMuBhlVzmG(C`)}}!p z9~e1F5y7V}MHHvVeTsOl!C5hKR${_v!4)``q*RwP-DZq_HUcfUJ>ziT?}ux{LeJK> z$p+0LKo6Iq&-c?(Fv)#MybNBae@`8^1s{(@)e>Yfl!|Aef-~kX`troAt=#q_gn)${ zwn+Di=&*;B+>(7W_#RI2oT5k|p~jNd&H>U9{KB@HptjY7z%0lj)0&mOK4B-N(H_wW zA5yqxz9mHRwnSA@55!1%;hgZY7s>HdsMOOwK|^SrNe?LM)t>fF^8GSiji~Ssc(4*N z*o5S3*DUt(Y}~3KcFmMoHb{;qMfD{KNnKSv+$@3v*_EYbLxLNh%Z4cX5pr3^TQRl~ zjbgUnlDl^Am_{3Z9SK7^W$k?@BUJBfSnKSpHXb9a?EnHjM+9|s z@s_X~UN(%(%CVkz9&jyp94OYs$q(tek8-oNmP5V06Cpm)xr7N`BHL~{9#bIWkOlzj z3fM0QU2@jhYE;oK;Hob0`6{(5O?NW9$EN3W8}hx3MRS6NNff!B3i001b>Bm_u2R-P z$oEnPf&AK#Igh-*h@hdsj_#xkFvmjJ$rHJaIDk=t3H~D^Q=h-e-tHY_%n4$eHH8tL zVJo)Jku{tdy6`BSIa-D@nIs*?kx4SgtrgG{?LmuN;Yf7|w2?OU=VWJHZzK~9?I1bK z0cK=+3CPXU>}#dqo{$yteM>b%htcw$;Nu5y*M-M5PFHynEqu`zd*?b(Tq>$< zFqwzoi7?qzKwbVo**GTNpT)yzZi#eaZ;9QlE#r-_yj>AsJlBmQ1*WjlEJ=N{ga_e( z6rvHIt1rCg;v&M5}~<}FN+_>hK+`H>_Y?Q0eVSS%Luvd$=WzjZOXk6ovDO)&2cz^V+A)J zqnV^QD;?x^6p5yRK;hH_btc_NPNuFNCsM@QC)Ms&Nl(KM|(doP~yV$0j>s7`84Z0lRfWSsw$6a2Acvi zl6&@(<#26=KvY<-!puNS3-qcNXJ54-qS>V1>WXaSlZRFG?Z)s8ayc9hqQTBVrRAWQgepOf$4=ifv_r zyy0n<@lqkg{9rV&*h0bL)99&sqPOsJrrGe)N=DG|YI!tJp@jo=nV=FJYuY98AZK{7 z{x-KN2#>MVHWDuQ>BJM2;l(QVZ|OI=VNwwFF@^NlAzb-LEG?ouL%NVp#zy7^-mqu> zT^Q}CNLIcu5Yj=FFId;ny8{t8z%?Se1SX$fG~-Bo!-sS4sF~xr1!C>z&sY7s9cA0- zCe;lM2MJ-IB~&@-9?hyc(E&&nb+TKI1)2cX6ZyR^qNVtJdxSb z+_dl>T13Il7jyYRm&#k``srj$aCb(N3_hNEY^Ul#>W;|${1L^IMOskrH&T4Mfu;|t z8Vlfd2#EQ&o;YS6iY&E0B%|yXRu)dG?YoeK2Q|wTd_7S1(Fa!SM{K* z`c&jN%%vxpqPd@FA6>$_X`9B~kcT1zCy_utf_~5Cb%8C|S<(W+xqpm0cNBRx7)c8L zV3v$9&rMy>L6WHw8EXP6GRBHLA9UsFioP#}K^CX?X526MToER+2mx}UdufQI5qV9O z3j?_yRHLHB6c?j~kAaJz>xt8A?4u7dwh%Tv!CRah{NHfG|OC;6Pdi!qe`y53~UH(%z<=hxixX zCOI!{^NV?qoT@I(Ku|{Ax?;LUJ|Pk#q5dsvLwUPFvvTX2=fi-xVyF$2WP;jcVlSZ* z<}xD{6t=xhzFQH{@4{5~(ZgL6hVu&J?Yq)p{WR7vskxWBFV_Q5?|mS)0ex`Ic0l6l zhTwt>4TNa>EnLA`ujwx#F$y0TNNjX4xHFNEi&&1QB#d7(>*d>TVFd$kiZilA!K?!{ z4bbFwJE!F}9iChNO#P)IW`mRZYdr6Ttss)lO1B?d@UAmXKNhuH!33->0_R-1lTCbF z(y}mLPFx8s2}WuZk(br>Ilwk3r`71)gnPn)jAc*&MN_~Elt0QiQEaGzSV&NF`<8}F zdBuP|c0(7gR_v>zbW4C)4}pf#|}3gm_DQ=8pKKdpVhX91eD-`vH=+ z{_Dr*;$VP(CBx)eo(fyaFuk3G#Rb+cpGGsI+A|B|U{W9Y>c^f60pUt=OL=RlF?O{Y z7nI&TkG(eIs6CG^4#x8#KSf=x2|qMN={KBmPf}19DSnk`v6XYn@)!6OFv)l0U<`ef zYuRz0_hLwUm=i^tX1kPYxk;uN2XnoHDa7!gi6QFnJVa0PqcNnV>BHIvH2jk2HMf%g zzR$hlV1yLX<0`~s*Jk88#NK|jvag_(*-#(-_AR)hJhIZp)L~2R&K0e^g{Cdv3xveM zxTpHoCm-FnyW6(2IRCS)EL7A1(RgmcPLo72(SJuvT)&&Gy))rYa4Zy zwg=gtckVVMFr{1aKbupOe^g>vefn_EzJpgbKYVVp3n3EPQb)->Clz-T;y!te_@wbT z`|70x=dYeR9X^(?fWu|>)el%g;c+SvXrbRgtX-Jac5KVTVPHEq;uK6or|`m0P`a0K zz!(}7M3ep^^p?3Ba!qzCRCQTt;X0yvXGXaLr`*hn&~GB7`pzy=(}I^`CzZw@{Q*PR zo;dd?9F5enCMF%;vc7HGk3al?;S=!rhmW8>{9SuG!}=FLY){7#Uq$75cCjN@zr$z= zSp!>T@ (T+zS,S,0)`; it assumes neither clean work nor independent data. +The cost is for this explicit lowering, not a lower bound for all Gaussian +ADD circuits. + +**3. Standalone boundaries have an exact minimum.** The real matrix of +multiplication by `g_h` has determinant `2^(2a_h+b_h)`. Signed additions and +negation do not change the determinant's power of two; each doubling or halving +changes it by one. Each boundary therefore costs at least `|2a_h+b_h|` such +operations. If `b_h=1`, all four matrix entries are nonzero, requiring at least +two additions: diagonal operations and one shear cannot make both off-diagonal +entries nonzero. Entry and exit together cost at least + +\[ +B(a,b)=2|2a+b|+4b. +\] + +The lower bound is attained at phase zero. For `a≥0`, first scale both +coordinates by `2^a`, then apply +`y+=x; x*=2; x-=y`, which multiplies by `1+i`. For `a≤-1`, first scale by +`2^(a+1)`, then apply `x-=y; x/=2; y+=x`, which multiplies by `(1+i)/2`. +Reverse the word and invert each elementary operation for the exit. Real +gauges use direct scaling and its inverse, costing `4|a|`. Other unit phases +cannot beat the lower bound and have identical internal ADD costs, so phase +zero suffices for the optimum. + +**4. Round all odd gauges with the same bit.** Discard unit phases and define +two real assignments `g_h^(θ)=2^(a_h+θ b_h)`, for a single common `θ=0,1`. +An original coefficient `q` on `source -> target` becomes `q g_target/g_source`. +If both endpoints have the same `b`, their factor of `1+i` cancels and the two +rounded costs equal the Gaussian cost. If the `b`s differ, the Gaussian +coefficient is a unit phase times `r(1±i)`, while the two rounded coefficients +have magnitudes `|r|,|2r|`. Consequently their average complex cost is + +\[ +c(r)+c(2r)\le 2c(r)+2, +\] + +the charged Gaussian cost. Shared edges between two gauged helpers are included; +rounding helpers independently would invalidate the equal-parity case. + +For a real gauge, boundary costs are unchanged. For an odd gauge, the average +rounded boundary cost is `2|a|+2|a+1|=2|2a+1|`, since `a` is integral. Its +Gaussian boundary costs at least four more. Sum over all ADDs and helpers, +then add the unchanged scalar costs, to obtain the stated inequality. +At least one of the two rounded complete assignments is no more expensive than +their average. The real assignments are themselves in the Gaussian-unit class, +so the unconstrained scalar-cost infima agree. This does not prove that an +external admissibility predicate is closed under rounding. + +## Finite coverage and verification + +For one helper, the real objective is `4|k|` plus its incident real-ADD deltas. +The odd objective is `2|2a+1|+4` plus the incident shared-product deltas. Both +are affine between integer coefficient-exponent breakpoints; unit discounts +only lower breakpoint values. The odd boundary kink is at `-1/2`, so include +both `-1,0`. The two outward tail slopes are `4+2d`, where `d` is the number of +incident ADDs. Every integer minimum is therefore attained in the recorded +finite breakpoint set. No heuristic cutoff or random search is used. + +[CERTIFICATE.json](CERTIFICATE.json) records 5,166 breakpoint evaluations across +both orientations, the complete minima, actual emitted primitive-stream hashes, +unchanged paid histograms, and eight simultaneous common-rounding fixtures. +The baseline, real winner and odd winner each pass all 712 formal complex input +columns (equivalently 1,424 real columns), including 480 arbitrary dirty helpers +and eight private centers. All 464 distinct macro fixtures check six real input +columns, including both arbitrary dirty work registers; 66 boundary pairs check +their exact maps and inverses. The complete literal positive envelopes remain +52 bits forward and 68 backward for all three variants; the inherited 192-bit +charge is retained. These finite envelopes do not discharge the all-size +precision/tape obligation. + +[independent.py](independent.py) separately reconstructs the helper domain and +incident coefficients, enumerates all integers in a provably sufficient interval, +and prices them by the literal pinned PR696 lowerer. It uses neither the +producer's cost formula nor its breakpoint search. [INDEPENDENT.json](INDEPENDENT.json) +records 13,684 grid evaluations, 1,115,016 incident-term evaluations, 2,532 +literal coefficients, and 3,488 distinct Gaussian inputs classified by checking +their actual reciprocal (64 units, 3,424 nonunits). Both implementations are by +the same AI-assisted author; this is not independent human review. + +Sixteen controls reject missing product initialization, omitted accumulation, +wrong cross-channel sign, uncleared dirt, missing/inaccurate inverse boundaries, +aliasing, invalid coefficient support, nondyadic coefficients, Gaussian nonunits, +zero factors, a false unit-cost inequality, false independent rounding, and +missing or modified source bindings. Certificates are compared canonically; +compressed output equality is based on decompressed content. + +## Reproduce + +From the repository root, with Python 3.12 and no third-party dependencies: + +```sh +python3.12 scripts/research_package.py --package research/k8-gaussian-unit-rounding-seed24 +``` + +The three registered commands print: + +```text +PASS_GAUSSIAN_UNIT_COMMON_ROUNDING helpers=237 orientations=2 real_saving=332 odd_saving=58 controls=16 +PASS_INDEPENDENT_LITERAL_GAUSSIAN_GRID +PASS_GAUSSIAN_PACKAGE_CONTROLS read_only_export=2 corrupted_artifacts=3 equivalent_gzip=1 +``` + +Direct `python3 -I -O -B research/k8-gaussian-unit-rounding-seed24/verify.py` +and the corresponding `independent.py` command are also supported. Default +replay is read-only and offline. `--write` on either script regenerates only +this package's own receipts. Metadata/provenance checking uses full Git history; +direct replay needs only the package and the pinned input files. + +This is a scalar circuit result and a scoped cost obstruction. Native/global +admission, the selected cold replay, compiler/realization, whole-call hosting, +roundoff, tape, recovery and analytic obligations have not been newly verified. +No supplier is installed, no selected certificate is changed, and no κ gain, +arbitrary-circuit optimum or Lean multiplication theorem is claimed. + +## Open next questions + +Can sharing a coefficient product **across distinct ADD macros**, while restoring +all dirty state and respecting chronological frames, break the inequality used +here? A useful first test would be an explicit two-ADD word whose complete bill +beats the sum of the two macro bills. That needs a new local interface and full +frame/precision accounting; a larger static Gaussian exponent search adds no +new evidence within this class. + +Can a joint boundary circuit across multiple helpers reduce the sum of the +standalone determinant charges? Opposite determinant exponents make this a +different problem. Start with two helpers and an exact four-real-register +boundary map; all source restoration and subsequent coefficients must be priced. +Neither possible escape is asserted to work. Structured questions and the +changed catalogue scope are in [TASK.json](TASK.json). + +## Credit and disclosure + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance in the argument, +implementation, verification and writing. New work is Apache-2.0. Credit +Sagar Thakrar's PR696 coefficient lowering; woklerx's +[PR1161](https://github.com/CrocSwap/integer-mult-bounds/pull/1161) +at `d210969d3158a1e6c505e41f67dd84e555c88564`; Hanson's +[PR1214](https://github.com/CrocSwap/integer-mult-bounds/pull/1214) +at `26162c56ec9c50a80e49949f36d4dd9a137a76a6`; and the retained complex-supplier +lineage of icekylinx, Jeremy Kothe, Rohan Arun and the other contributors credited +in Douglas Colkitt's PR1094 review. No pending predecessor implementation is +vendored or required. Source licenses and frozen evidence remain unchanged. diff --git a/research/k8-gaussian-unit-rounding-seed24/SOURCES.json b/research/k8-gaussian-unit-rounding-seed24/SOURCES.json new file mode 100644 index 0000000000..922baea812 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "input", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1042-audit/RESULT.json", + "usage": "input", + "git_blob": "8182d0818c0cbda7e52c10120f15b2c3a2c8f933", + "sha256": "bf12c6ed3b412539638b76addb40591a631609b2ab9e5ee0db1f6bbe067d0ec0" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/community-frontier1094-audit/RESULT.json", + "usage": "input", + "git_blob": "131d9c96a54632ae385ced4138fd7f30ad448a3e", + "sha256": "1e3e47e9ec24bcb6fb5f703b7fce0aab658d84ff72bfae5da3ae429d17b6e752" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-dyadic-lowering/README.md", + "usage": "input", + "git_blob": "18999b7d252471054af43dea926d81efdf292c2b", + "sha256": "798209e9869d1612a2c34412ef2eb87c0eb0dcebcbed9963a45e0fe248326c2f" + }, + { + "path": "research/complex-dyadic-lowering/lower.py", + "usage": "input", + "git_blob": "a2c2889e5be41a0fc30d4dfa5dfcebb03d6d47f8", + "sha256": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753" + } + ] +} diff --git a/research/k8-gaussian-unit-rounding-seed24/TASK.json b/research/k8-gaussian-unit-rounding-seed24/TASK.json new file mode 100644 index 0000000000..14032c27eb --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/TASK.json @@ -0,0 +1,132 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 2, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract, not another mixture already covered by the frozen catalogue.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the frozen catalogue bound exclusions and select one genuinely different helper endpoint inventory.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the complete optimistic child histogram and reject it immediately if even the relaxation has insufficient headroom.", + "bottleneck_link": "Helper inventory changes can improve the moment; repacking a covered cost interface cannot evade its scoped bound.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Static Gaussian-dyadic unit helper gauges with shared-product macro lowering and independent two-real-register boundaries; common-rounding cost theorem and exact k8 single-helper census.", + "scope_change_reason": "The user explicitly assigned the complex-supplier track and permits scoped circuit negative results. This is a scalar-circuit side result rather than the catalogue card's changed paid helper inventory; the recursive profile stays fixed.", + "bottleneck_link": "Rules out Gaussian unit coefficient-field extension as an intrinsic scalar-cost improvement within this lowering/boundary class. It does not improve the paid recursive moment or approach kappa > 0.01.", + "budget_minutes": 60, + "stop_rule": "Stop after the complete unit normal-form and rounding argument, all 237 eligible single-helper integer domains in both orientations, exact finite circuit checks, independent literal census, controls and one PR. No heuristic search or arbitrary Gaussian circuit synthesis.", + "outcome": "negative-result", + "evidence": "Written argument in README.md; exact CERTIFICATE.json and CENSUS.json.gz; separately implemented literal grid in INDEPENDENT.json.", + "author": "Hanson Sun (@bbMisk)", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, code, verification and writing. Separate implementations by the same AI-assisted author; no independent human review or formal proof assistant.", + "open_questions": [ + { + "question": "Can product reuse across two distinct Gaussian ADD macros beat the sum of their macro-local bills?", + "why_it_matters": "This would change the key edge-cost premise of the rounding theorem.", + "first_step": "Exhibit one exact two-ADD word and complete dirty-state primitive invoice.", + "blocked_by": "Requires chronological frame legality, source restoration and precision/hosting costs; no such improvement is claimed." + }, + { + "question": "Can joint boundaries across helpers beat the independent two-register determinant charges?", + "why_it_matters": "Opposite determinant exponents may permit a different boundary interface.", + "first_step": "Synthesize one exact four-real-register entry/exit pair and price all conjugated ADDs.", + "blocked_by": "The present theorem excludes cross-helper boundary sharing; a circuit and full interface proof are missing." + } + ], + "assignment_seed": 24, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "started_at_utc": "2026-10-14T01:00:55.081120+00:00", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18912584", + "track": "Complex supplier, user allocation 20-39", + "candidate_tasks": [ + { + "task": "Gaussian-dyadic unit extension of static helper rescaling", + "decision": "selected by 24 mod 3 = 0; new coefficient class and common-rounding method" + }, + { + "task": "Temporal two-helper gauge composition", + "decision": "deferred; overlaps PR1380/1408" + }, + { + "task": "Masked P112 rank-eight extension", + "decision": "deferred; active Discussion1411 and PR1419/1425" + } + ], + "predecessors": [ + { + "pr": 1161, + "head": "d210969d3158a1e6c505e41f67dd84e555c88564", + "credit": "woklerx; one-helper real dyadic optimum and source binding" + }, + { + "pr": 1214, + "head": "26162c56ec9c50a80e49949f36d4dd9a137a76a6", + "credit": "Hanson Sun; eligible two-helper dyadic domain" + }, + { + "pr": 696, + "path": "research/complex-dyadic-lowering/lower.py", + "credit": "Sagar Thakrar; exact copy-initialized coefficient lowering, pinned on main" + } + ], + "outcome_description": "Scoped negative result with attained odd-class finite witnesses; real single-helper record independently corroborated.", + "overlap": { + "initial_complete_open_pr_snapshot": { + "records": 823, + "fetched_at": "2026-10-14T01:04:22.002089+00:00" + }, + "final_discussions": { + "fetched_at": "2026-10-14T01:33:43.603581+00:00", + "complete_pagination": true, + "records": 173 + }, + "full_pr_refresh_limitation": "The overlap helper and REST full pagination returned HTTP 500. The earlier complete snapshot was supplemented by the newest 50 open PRs ordered by updated_at.", + "fresh_updated_prs": { + "records": 50, + "fetched_at": "2026-10-14T01:38:25Z", + "oldest_updated_at": "2026-10-14T00:51:37Z", + "newest_updated_at": "2026-10-14T01:37:49Z", + "covers_updates_since_initial_snapshot": true, + "snapshot_sha256": "4d76f270eff9cef016bd5a16bc01582d5995be505baf4aca51074d759a43746e" + }, + "terms": [ + "Gaussian unit", + "Gaussian-unit", + "Gaussian helper", + "static Gaussian", + "shared-product", + "common rounding" + ], + "disposition": "No matching external scope found. Own package/claim match. Discussion1462 concerns truncation commuting with linear maps, not helper gauge cost. PR1469/1474 concern masked decoder rigidity; PR309/1172 concern physical response/owner gauges. Searches do not cover arbitrary code diffs or establish novelty." + } +} diff --git a/research/k8-gaussian-unit-rounding-seed24/VALIDATION.json b/research/k8-gaussian-unit-rounding-seed24/VALIDATION.json new file mode 100644 index 0000000000..e55aca66d0 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/VALIDATION.json @@ -0,0 +1,55 @@ +{ + "status": "PASS_LOCAL_SCOPED_VERIFICATION", + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "registered_python": "3.12.13", + "host_platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "registered_replay": { + "command": "python3.12 scripts/research_package.py --package research/k8-gaussian-unit-rounding-seed24", + "exit_code": 0, + "elapsed_seconds": 64.488, + "output": "CHECK Exact Gaussian primitive circuits, complete selected-word scalar columns/invoices, breakpoint certificate and sixteen rejection controls.\nPASS_GAUSSIAN_UNIT_COMMON_ROUNDING helpers=237 orientations=2 real_saving=332 odd_saving=58 controls=16\nCHECK Separate literal-lowerer integer census, source domain, tails and reciprocal unit membership.\nPASS_INDEPENDENT_LITERAL_GAUSSIAN_GRID\nCHECK Optimized read-only relocated export, actual source/certificate/census corruptions and canonical gzip equivalence.\nPASS_GAUSSIAN_PACKAGE_CONTROLS read_only_export=2 corrupted_artifacts=3 equivalent_gzip=1\nPASS_REGISTERED_RESEARCH_PACKAGE research/k8-gaussian-unit-rounding-seed24 outcome=negative-result\n" + }, + "optimized_default_python": { + "command": [ + "/opt/homebrew/opt/python@3.14/bin/python3.14", + "-I", + "-O", + "-B", + "research/k8-gaussian-unit-rounding-seed24/verify.py" + ], + "python": "3.14.6 (main, Jun 10 2026, 10:03:53) [Clang 21.0.0 (clang-2100.0.123.102)]", + "exit_code": 0, + "elapsed_seconds": 12.725, + "stdout": "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING helpers=237 orientations=2 real_saving=332 odd_saving=58 controls=16\n", + "stderr": "" + }, + "additional_checks": { + "ruff": "pass", + "git_diff_check": "pass", + "selected_result_checker": "pass; selected certificate unchanged", + "optimized_python314_independent_grid": "pass" + }, + "upstream_compatibility": { + "fetched_main": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "base_to_main_diff_on_live_inputs_selected_record_AGENTS_CONTRIBUTING_and_replay_runner": "empty" + }, + "scientific_artifacts_sha256": { + "model.py": "246803b9ca3f14984d9460173923f3f726bdcf15307b28a64fb5ecb3a761c9fe", + "verify.py": "a1630c4492bd35b86d624f3dcc60b18e468d6abdd16645a5442a0482155b88d3", + "independent.py": "7fb0f45c5dada54a2df3f6053279aa688ec83561f7c6e944e76b9157acbad2be", + "test_package.py": "f9cc696ceb9a24afd17d73ea8b0d1276feabb909e9afd93c514c1de7eb5f00d7", + "CERTIFICATE.json": "1135b004e367aa7c4b6bc953b7f0b21ceb5c22953584391d105e7f9f8c70907c", + "CENSUS.json.gz": "551606e065f1436de6568b83bbebc3988226dcc54e30052481142699ccdc84ad", + "INDEPENDENT.json": "3b0ee5801584db9cb5f99dd5a412e128ed5971962478d4ba1d2951f45674e0e0", + "SOURCES.json": "4cd986939bc423341b7e1469f82652a4469249d46fff370b3d71f1296f28a037", + "VERIFY.json": "a8ff996c8e1c0040f06a59a98d89f0fa3fe33743bb305ca73f57ad7da53bad99" + }, + "not_run": [ + "Selected full native/global cold replay", + "Native Gaussian supplier admission", + "New global assembly or kappa certification", + "Lean formalization", + "Hosted CI (separate from these local results)" + ], + "writing": "Argument and scope independently checked against executable evidence; substantial AI assistance disclosed." +} diff --git a/research/k8-gaussian-unit-rounding-seed24/VERIFY.json b/research/k8-gaussian-unit-rounding-seed24/VERIFY.json new file mode 100644 index 0000000000..976451f9bb --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/community-batch1099-review.md", + "research/community-frontier1042-audit/RESULT.json", + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/community-frontier1094-audit/RESULT.json", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/complex-dyadic-lowering/README.md", + "research/complex-dyadic-lowering/lower.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact Gaussian primitive circuits, complete selected-word scalar columns/invoices, breakpoint certificate and sixteen rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 240, + "checks": "Separate literal-lowerer integer census, source domain, tails and reciprocal unit membership." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 600, + "checks": "Optimized read-only relocated export, actual source/certificate/census corruptions and canonical gzip equivalence." + } + ] +} diff --git a/research/k8-gaussian-unit-rounding-seed24/independent.py b/research/k8-gaussian-unit-rounding-seed24/independent.py new file mode 100644 index 0000000000..e604c56192 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/independent.py @@ -0,0 +1,170 @@ +#!/usr/bin/env python3 +"""Literal-lowerer grid audit, separately implemented by the same AI-assisted author. + +It shares source authentication with model.py, but not its cost formula, helper +selection, incidence extraction, breakpoint search, Gaussian lowering or replay. +Hanson Sun with OpenAI Codex; Apache-2.0. PR696 lowerer: Sagar Thakrar. +""" +from fractions import Fraction +from functools import lru_cache +import gzip +import importlib.util +import json +from pathlib import Path +import sys +import tarfile + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import model + + +def insist(ok, message): + if not ok: + raise ValueError(message) + + +def run(): + model.check_sources() + root = model.ROOT + with tarfile.open(root / model.ARCHIVE1042) as archive: + programs = json.loads(gzip.decompress(archive.extractfile("slots/local/LOCAL-PROGRAMS.json.gz").read())) + word = json.loads(gzip.decompress(archive.extractfile("slots/local/CANONICAL-WORD.json.gz").read())) + spec = importlib.util.spec_from_file_location("independent_pr696", root / model.LOWER) + lowerer = importlib.util.module_from_spec(spec) + spec.loader.exec_module(lowerer) + census = json.loads(gzip.decompress((model.HERE / "CENSUS.json.gz").read_bytes())) + certificate = json.loads((model.HERE / "CERTIFICATE.json").read_bytes()) + + @lru_cache(maxsize=None) + def literal(q): + return len(lowerer.lower(["add", ("target",), ("source",), + q.numerator, q.denominator], work=("work",))) + + def two(k): + return Fraction(2 ** k) if k >= 0 else Fraction(1, 2 ** -k) + + # Reconstruct the exclusion contract register by register, not by using the + # producer's domain routine or the supplied helper list. + eligible = [] + for h in range(224, 704): + if h in word["centers"] or word["start"][h] != 0 or word["final"][h] != 1: + continue + blocked = False + for events in programs.values(): + for event in events: + if event[0] == "residual_adapter" and event[2] == h: + blocked = True + elif event[0] == "scalar" and event[1][0] in ("copy", "clear") and ["L", h] in event[1][1:]: + blocked = True + if not blocked: + eligible.append(h) + insist(eligible == certificate["eligible_helpers"] and len(eligible) == 237, "independent helper domain") + summary = {"helper_count": len(eligible), "orientations": {}} + for orientation, events in programs.items(): + target_terms = {h: [] for h in eligible} + source_terms = {h: [] for h in eligible} + baseline = 0 + for event in events: + if event[0] != "scalar": + continue + op = event[1] + baseline += 2 * len(lowerer.lower(op)) + if op[0] == "add": + q = Fraction(op[3], op[4]) + if op[1][0] == "L" and op[1][1] in target_terms: + target_terms[op[1][1]].append(q) + if op[2][0] == "L" and op[2][1] in source_terms: + source_terms[op[2][1]].append(q) + insist(baseline == certificate["orientations"][orientation]["programs"]["baseline"]["invoice"]["complex_scalar_primitives"], "literal full baseline") + rows = {r["helper"]: r for r in census[orientation]} + grid_evaluations = 0 + term_evaluations = 0 + critical_rows = [] + for h in eligible: + incoming, outgoing = target_terms[h], source_terms[h] + all_terms = incoming + outgoing + exponents = [] + for q in all_terms: + n, d, exponent = abs(q.numerator), q.denominator, 0 + while n % 2 == 0: + n //= 2 + exponent += 1 + while d > 1: + insist(d % 2 == 0, "dyadic source") + d //= 2 + exponent -= 1 + exponents.append(exponent) + radius = max([abs(e) for e in exponents] + [0]) + 3 + lo, hi = -radius, radius + original = 2 * sum(literal(q) for q in all_terms) + + def r(k): + return 4 * abs(k) + 2 * sum(literal(q * two(k)) for q in incoming) + 2 * sum(literal(q / two(k)) for q in outgoing) - original + + def g(a): + # Two copies of the exact predecessor coefficient circuit, + # one extra target accumulation each, and optimal boundaries. + return 2 * abs(2 * a + 1) + 4 + sum(2 * literal(q * two(a)) + 2 for q in incoming) + sum(2 * literal(q / two(a + 1)) + 2 for q in outgoing) - original + + real_grid = [(k, r(k)) for k in range(lo, hi + 1)] + odd_grid = [(a, g(a)) for a in range(lo, hi + 1)] + def key(pair): + return pair[1], abs(pair[0]), pair[0] + insist(list(min(real_grid, key=key)) == rows[h]["real_best"], "independent real minimum") + insist(list(min(odd_grid, key=key)) == rows[h]["odd_best"], "independent odd minimum") + for k, value in rows[h]["real_candidates"]: + insist(lo <= k <= hi and r(k) == value, "real breakpoint receipt") + for a, value in rows[h]["odd_candidates"]: + insist(lo <= a <= hi and g(a) == value, "odd breakpoint receipt") + slope = 4 + 2 * len(all_terms) + for cost in (r, g): + insist(cost(lo - 1) - cost(lo) == slope and cost(hi + 1) - cost(hi) == slope, + "independent outward tails") + for a in range(lo, hi + 1): + insist(2 * g(a) >= r(a) + r(a + 1) + 8, "single-helper common rounding") + grid_evaluations += len(real_grid) + len(odd_grid) + term_evaluations += (len(real_grid) + len(odd_grid)) * len(all_terms) + critical_rows.append([h, lo, hi, min(real_grid, key=key), min(odd_grid, key=key)]) + summary["orientations"][orientation] = { + "complete_scalar_baseline": baseline, "integer_grid_evaluations": grid_evaluations, + "incident_term_evaluations": term_evaluations, + "grid_rows_sha256": model.sha(model.canonical(critical_rows))} + + # Independently decide unit membership by computing the actual reciprocal, + # then compare the normal-form implementation on a finite exact domain. + units = nonunits = 0 + seen = set() + for denominator_exponent in range(4): + for re in range(-16, 17): + for im in range(-16, 17): + z = Fraction(re, 2 ** denominator_exponent), Fraction(im, 2 ** denominator_exponent) + if z == (0, 0) or z in seen: + continue + seen.add(z) + norm = z[0] * z[0] + z[1] * z[1] + reciprocal = z[0] / norm, -z[1] / norm + is_unit = all(q.denominator & (q.denominator - 1) == 0 for q in reciprocal) + try: + coordinates = model.unit_coordinates(z) + except ValueError: + insist(not is_unit, "unit wrongly rejected") + nonunits += 1 + else: + insist(is_unit and model.gauge(*coordinates) == z, "nonunit or wrong normal form") + units += 1 + summary["unit_membership_grid"] = {"distinct_nonzero_inputs": len(seen), "units": units, "nonunits": nonunits, + "numerators": [-16, 16], "common_denominator_exponents": [0, 3]} + summary["literal_distinct_coefficients"] = literal.cache_info().currsize + summary["status"] = "PASS_INDEPENDENT_LITERAL_GAUSSIAN_GRID" + return summary + + +if __name__ == "__main__": + result = run() + path = model.HERE / "INDEPENDENT.json" + if sys.argv[1:] == ["--write"]: + path.write_text(json.dumps(result, indent=2) + "\n") + else: + insist(sys.argv[1:] in ([], ["--json"]), "arguments") + insist(result == json.loads(path.read_bytes()), "independent receipt mismatch") + print(json.dumps(result, indent=2) if sys.argv[1:] == ["--json"] else result["status"]) diff --git a/research/k8-gaussian-unit-rounding-seed24/model.py b/research/k8-gaussian-unit-rounding-seed24/model.py new file mode 100644 index 0000000000..72bc4d22de --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/model.py @@ -0,0 +1,400 @@ +"""Static Gaussian-unit gauges, Hanson Sun with OpenAI Codex, Apache-2.0. + +The real macro lowering is Sagar Thakrar's PR696; the local word is the +source-bound PR1094/1042 k8 word. No pending PR implementation is imported. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import lru_cache +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = "410026dc5513b87db92ae98571d1d5984c69a983" +ARCHIVE1042 = "research/community-frontier1042-audit/selected-replay.tar.gz" +ARCHIVE1094 = "research/community-frontier1094-audit/selected-replay.tar.gz" +LOWER = "research/complex-dyadic-lowering/lower.py" +INPUTS = frozenset((ARCHIVE1042, ARCHIVE1094, LOWER, + "research/community-frontier1042-audit/RESULT.json", + "research/community-frontier1094-audit/RESULT.json", + "research/complex-dyadic-lowering/README.md", + "docs/research/community-batch1099-review.md")) +MEMBERS = ("CANONICAL-WORD.json.gz", "LOCAL-PROGRAMS.json.gz", + "INDEPENDENT-LOCAL-REPLAY.json", "LOCAL-CHECKS.json") +ZERO = (Q(0), Q(0)) +ONE = (Q(1), Q(0)) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":"), + allow_nan=False).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def check_sources(manifest=None, reader=None): + manifest = manifest or json.loads((HERE / "SOURCES.json").read_bytes()) + reader = reader or (lambda p: (ROOT / p).read_bytes()) + require(manifest["base_commit"] == BASE, "base commit") + rows = [r for r in manifest["files"] if r["usage"] == "input"] + require(len(rows) == len(INPUTS) and {r["path"] for r in rows} == INPUTS, + "source inventory") + for r in rows: + data = reader(r["path"]) + require(sha(data) == r["sha256"], "source SHA256: " + r["path"]) + blob = hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + require(blob == r["git_blob"], "source Git blob: " + r["path"]) + return manifest + + +def load(): + check_sources() + raw = {} + with tarfile.open(ROOT / ARCHIVE1042) as archive: + for name in MEMBERS: + raw[name] = archive.extractfile("slots/local/" + name).read() + with tarfile.open(ROOT / ARCHIVE1094) as archive: + for name in MEMBERS: + actual = archive.extractfile( + "candidate/strict/global8/base/providers/gauge44/" + name).read() + require(actual == raw[name], "selected provider alias: " + name) + objects = {n: json.loads(gzip.decompress(b) if n.endswith(".gz") else b) + for n, b in raw.items()} + word, programs, replay, checks = (objects[n] for n in MEMBERS) + old = (ROOT / "research/community-frontier1042-audit/RESULT.json").read_bytes() + current = json.loads((ROOT / "research/community-frontier1094-audit/RESULT.json").read_bytes()) + require(current["baseline_receipt_sha256"] == sha(old), "baseline receipt binding") + require(json.loads(old)["status"] == "PASS_COMPLETE_PR1042_COMPOSITION" and + current["status"] == "PASS_COMPLETE_PR1094_COMPOSITION", "retained receipt status") + require(replay["canonical_word_sha256"] == sha(raw[MEMBERS[0]]) and + replay["local_programs_sha256"] == sha(raw[MEMBERS[1]]), "native receipt binding") + require((word["v"], word["h"], word["R"]) == (112, 9, 480), "source geometry") + require(set(programs) == {"forward", "backward"}, "orientations") + bindings = {n: {"archive_member_sha256": sha(b), + "payload_sha256": sha(gzip.decompress(b) if n.endswith(".gz") else b)} + for n, b in raw.items()} + return word, programs, bindings, replay, checks + + +def domain(word, programs): + excluded = set(word["centers"]) + for events in programs.values(): + for event in events: + if event[0] == "residual_adapter": + excluded.add(event[2]) + if event[0] == "scalar" and event[1][0] in ("copy", "clear"): + excluded.update(r[1] for r in event[1][1:] + if isinstance(r, list) and r[0] == "L") + return [h for h in range(224, 704) if h not in excluded + and word["start"][h] == 0 and word["final"][h] == 1] + + +def power(e): + return Q(2 ** e) if e >= 0 else Q(1, 2 ** -e) + + +def parts(q): + q = Q(q) + p = abs(q.numerator) + require(p > 0 and q.denominator & (q.denominator - 1) == 0, "nonzero dyadic") + twos = (p & -p).bit_length() - 1 + return p >> twos, twos - (q.denominator.bit_length() - 1) + + +def c_parts(p, e): + require(p > 0 and p % 2 == 1, "positive odd numerator") + return 2 + p.bit_length() - 1 + p.bit_count() + abs(e) - int(p == 1 and e == 0) + + +def c(q): + return c_parts(*parts(q)) + + +def mul(x, y): + return x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0] + + +def inv(x): + d = x[0] ** 2 + x[1] ** 2 + require(d != 0, "nonzero Gaussian factor") + return x[0] / d, -x[1] / d + + +def gauge(a, odd, phase=0): + require(odd in (0, 1) and phase in range(4), "Gaussian-unit parameters") + return mul((power(a), power(a) if odd else Q(0)), + (ONE, (Q(0), Q(1)), (Q(-1), Q(0)), (Q(0), Q(-1)))[phase]) + + +def gaussian_add_cost(z): + if z[0] == 0 or z[1] == 0: + return 2 * c(z[0] or z[1]) + require(abs(z[0]) == abs(z[1]), "axis or diagonal Gaussian coefficient") + return 2 * c(z[0]) + 2 + + +def unit_coordinates(z): + """Normal form for units of Z[1/2,i]; rejects nonunits.""" + require(z != ZERO, "nonzero Gaussian unit") + if z[0] == 0 or z[1] == 0: + p, a = parts(z[0] or z[1]) + require(p == 1, "Gaussian dyadic unit norm") + phase = (0 if z[0] > 0 else 2) if z[1] == 0 else (1 if z[1] > 0 else 3) + return a, 0, phase + require(abs(z[0]) == abs(z[1]), "Gaussian dyadic unit diagonal") + p, a = parts(z[0]) + require(p == 1, "Gaussian dyadic unit norm") + phase = {(True, True): 0, (False, True): 1, + (False, False): 2, (True, False): 3}[z[0] > 0, z[1] > 0] + return a, 1, phase + + +def terms_by_helper(events): + terms = defaultdict(list) + for event in events: + if event[0] == "scalar" and event[1][0] == "add": + g = event[1] + require(g[1] != g[2], "distinct ADD operands") + p, e = parts(Q(g[3], g[4])) + for r, sign in ((g[1], 1), (g[2], -1)): + if r[0] == "L": + terms[r[1]].append((p, e, sign)) + return terms + + +def real_delta(terms, k): + return 4 * abs(k) + 2 * sum(c_parts(p, e + s * k) - c_parts(p, e) + for p, e, s in terms) + + +def odd_delta(terms, a): + # The two-register boundary minimum is attained by boundary_word below. + return 2 * abs(2 * a + 1) + 4 + sum( + 2 * c_parts(p, e + s * a - int(s < 0)) + 2 - 2 * c_parts(p, e) + for p, e, s in terms) + + +def census(events, helpers): + by_helper = terms_by_helper(events) + rows = [] + for helper in helpers: + terms = by_helper[helper] + real_points = sorted({0} | {-s * e for p, e, s in terms}) + odd_points = sorted({-1, 0} | {-s * e - int(s < 0) for p, e, s in terms}) + real = [[k, real_delta(terms, k)] for k in real_points] + odd = [[a, odd_delta(terms, a)] for a in odd_points] + rows.append({"helper": helper, "incident_adds": len(terms), + "real_candidates": real, "odd_candidates": odd, + "real_best": min(real, key=lambda x: (x[1], abs(x[0]), x[0])), + "odd_best": min(odd, key=lambda x: (x[1], abs(x[0]), x[0])), + "outward_tail_slope": 4 + 2 * len(terms)}) + return rows + + +def boundary_word(a, odd, target=("X",)): + """Exact minimum for phase-zero gauge and its inverse; no work register.""" + x, y = tuple(target) + (0,), tuple(target) + (1,) + if not odd: + e = a + result = [] + elif a >= 0: + e = a + result = [("add", y, x), ("double", x), ("subtract", x, y)] + else: + e = a + 1 + result = [("subtract", x, y), ("halve", x), ("add", y, x)] + scales = [("double" if e > 0 else "halve", r) + for r in (x, y) for _ in range(abs(e))] + forward = scales + result + inverse_tag = {"add": "subtract", "subtract": "add", "double": "halve", "halve": "double"} + backward = [(inverse_tag[g[0]], *g[1:]) for g in reversed(forward)] + expected = 2 * abs(2 * a + 1) + 4 if odd else 4 * abs(a) + require(len(forward) + len(backward) == expected, "boundary determinant/shear lower bound") + return forward, backward + + +@lru_cache(maxsize=1) +def real_lowerer(): + spec = importlib.util.spec_from_file_location("pinned_pr696_lower", ROOT / LOWER) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module.lower + + +def lower_gaussian(z, target=("T",), source=("S",)): + """Share each source-channel product across both targets, then clear work. + + Uses exactly the two existing real coefficient-work registers. Each may be + arbitrarily dirty on entry. Target/source complex registers must be distinct. + """ + require(tuple(target) != tuple(source), "distinct complex operands") + require(z != ZERO, "nonzero Gaussian ADD") + require(z[0] == 0 or z[1] == 0 or abs(z[0]) == abs(z[1]), "Gaussian support") + out = [] + for channel, coefficients in enumerate(((z[0], z[1]), (-z[1], z[0]))): + src = tuple(source) + (channel,) + work = ("W", channel) + entries = [(tuple(target) + (i,), q) for i, q in enumerate(coefficients) if q] + dst, q = entries[0] + word = real_lowerer()(["add", dst, src, q.numerator, q.denominator], work=work) + if len(entries) == 2: + other, coefficient = entries[1] + require(abs(coefficient) == abs(q), "shared product magnitude") + operand = src if abs(q) == 1 else work + word.insert(len(word) - 1, + ("add" if coefficient > 0 else "subtract", other, operand)) + out.extend(word) + require(len(out) == gaussian_add_cost(z), "Gaussian primitive invoice") + return out + + +def transformed(events, gauges): + """Return scalar Gaussian macros; non-scalar events remain unchanged.""" + factors = {("L", h): gauge(a, odd) for h, (a, odd) in gauges.items()} + stream = [] + for event in events: + if event[0] != "scalar": + stream.append(copy.deepcopy(event)) + continue + g = event[1] + tag, target = g[0], tuple(g[1]) + if tag == "add": + source = tuple(g[2]) + z = mul((Q(g[3], g[4]), Q(0)), + mul(factors.get(target, ONE), inv(factors.get(source, ONE)))) + op = [tag, list(target), list(source), [z[0].numerator, z[0].denominator], + [z[1].numerator, z[1].denominator]] + elif tag == "scale": + op = [tag, list(target), [g[2], g[3]], [0, 1]] + else: + require(tag in ("clear", "copy"), "scalar opcode") + require(not any(tuple(r) in factors for r in g[1:] if isinstance(r, list)), + "no gauge on copy/clear carrier") + op = copy.deepcopy(g) + stream.append(["scalar", op, *event[2:]]) + return stream + + +def replay(stream, gauges, orientation): + """Exact complex-linear maps: 712 complex columns = 1424 real columns.""" + rows = {("L", i): {i: ONE} for i in range(704)} + rows.update({("C", i): {704 + i: ONE} for i in range(8)}) + + def scale(target, z): + rows[target] = {i: mul(v, z) for i, v in rows[target].items()} + + for helper, (a, odd) in gauges.items(): + scale(("L", helper), gauge(a, odd)) + for event in stream: + if event[0] != "scalar": + continue + g = event[1] + tag, target = g[0], tuple(g[1]) + if tag == "clear": + rows[target] = {} + elif tag == "copy": + rows[target] = dict(rows[tuple(g[2])]) + elif tag == "scale": + scale(target, (Q(*g[2]), Q(*g[3]))) + elif tag == "add": + source = tuple(g[2]) + require(source != target, "distinct replay operands") + z = Q(*g[3]), Q(*g[4]) + for i, value in rows[source].items(): + delta = mul(value, z) + old = rows[target].get(i, ZERO) + new = old[0] + delta[0], old[1] + delta[1] + if new == ZERO: + rows[target].pop(i, None) + else: + rows[target][i] = new + else: + raise ValueError("Gaussian scalar opcode") + for helper, (a, odd) in gauges.items(): + scale(("L", helper), inv(gauge(a, odd))) + for i in range(704): + expected = {i: ONE} + if orientation == "forward" and 112 <= i < 224: + expected[i - 112] = ONE + if orientation == "backward" and i < 112: + expected[i + 112] = (Q(-1), Q(0)) + require(rows["L", i] == expected, "all-column endpoint " + str((orientation, i))) + require(all(not rows["C", i] for i in range(8)), "private centres cleared") + return {"complex_input_columns": 712, "equivalent_real_input_columns": 1424, + "dirty_helper_columns": 480, "all_helpers_restored": True, + "private_centres_cleared": True} + + +def primitive_stream(stream, gauges): + for h, (a, odd) in sorted(gauges.items()): + yield from boundary_word(a, odd, ("L", h))[0] + for event in stream: + if event[0] != "scalar": + continue + g = event[1] + if g[0] == "add": + yield from lower_gaussian((Q(*g[3]), Q(*g[4])), tuple(g[1]), tuple(g[2])) + else: + for channel in range(2): + target = tuple(g[1]) + (channel,) + if g[0] == "scale": + require(g[3] == [0, 1], "real original SCALE") + op = ["scale", target, *g[2]] + elif g[0] == "copy": + op = ["copy", target, tuple(g[2]) + (channel,)] + else: + require(g[0] == "clear", "primitive opcode") + op = ["clear", target] + yield from real_lowerer()(op, work=("W", channel)) + for h, (a, odd) in reversed(sorted(gauges.items())): + yield from boundary_word(a, odd, ("L", h))[1] + + +def invoice(stream, gauges): + env = {("L", i, channel): Q(1) for i in range(704) for channel in range(2)} + env.update({("C", i, channel): Q(1) for i in range(8) for channel in range(2)}) + env.update({("W", channel): Q(1) for channel in range(2)}) + peak, count = Q(1), 0 + digest = hashlib.sha256() + for g in primitive_stream(stream, gauges): + count += 1 + digest.update(canonical(g) + b"\n") + tag, target = g[:2] + if tag in ("add", "subtract"): + env[target] += env[g[2]] + elif tag == "copy": + env[target] = env[g[2]] + elif tag == "clear": + env[target] = Q(0) + elif tag == "double": + env[target] *= 2 + elif tag == "halve": + env[target] /= 2 + else: + require(tag == "negate", "invoice primitive") + peak = max(peak, env[target]) + require(env["W", 0] == env["W", 1] == 0, "coefficient work cleared") + require(peak < 2 ** 192, "inherited 192-bit local envelope") + paid = Counter() + for e in stream: + if e[0] == "climb": + paid[e[5]] += 1 + elif e[0] == "center": + paid[e[4]] += 1 + return {"complex_scalar_primitives": count, "primitive_stream_sha256": digest.hexdigest(), + "positive_prefix_l1": str(peak), + "positive_prefix_bits": peak.numerator.bit_length() - peak.denominator.bit_length() + 1, + "inherited_charged_bits": 192, "paid_profile": dict(sorted(paid.items()))} diff --git a/research/k8-gaussian-unit-rounding-seed24/test_package.py b/research/k8-gaussian-unit-rounding-seed24/test_package.py new file mode 100644 index 0000000000..dc47638141 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/test_package.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Exercise the actual portable commands and corrupted artifacts, without pytest. + +Hanson Sun with OpenAI Codex assistance; Apache-2.0. +""" +import gzip +import hashlib +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FILES = ("model.py", "verify.py", "independent.py", "CERTIFICATE.json", + "CENSUS.json.gz", "INDEPENDENT.json", "SOURCES.json", "TASK.json", + "VERIFY.json", "README.md") + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def run(script, root, expected, success=True): + env = dict(os.environ, PYTHONHASHSEED="24") + result = subprocess.run([sys.executable, "-I", "-O", "-B", str(script)], + cwd=root, env=env, text=True, capture_output=True, timeout=240) + require((result.returncode == 0) == success and expected in result.stdout + result.stderr, + "subprocess outcome: " + expected + "\n" + result.stdout[-2000:] + result.stderr[-2000:]) + + +def inventory(root): + return {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob("*") if p.is_file()} + + +def writable(root): + for p in [root, *root.rglob("*")]: + p.chmod(0o755 if p.is_dir() else 0o644) + + +def main(): + manifest = json.loads((HERE / "SOURCES.json").read_bytes()) + with tempfile.TemporaryDirectory(prefix="gaussian-unit-package-") as temporary: + root = Path(temporary) + package = root / "research" / HERE.name + package.mkdir(parents=True) + for name in FILES: + shutil.copyfile(HERE / name, package / name) + for row in manifest["files"]: + if row["usage"] != "input": + continue + path = root / row["path"] + path.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / row["path"], path) + try: + before = inventory(root) + for p in root.rglob("*"): + p.chmod(0o555 if p.is_dir() else 0o444) + root.chmod(0o555) + run(package / "verify.py", root, "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING") + run(package / "independent.py", root, "PASS_INDEPENDENT_LITERAL_GAUSSIAN_GRID") + require(inventory(root) == before, "read-only export was changed") + writable(root) + + path = package / "CERTIFICATE.json" + original = path.read_bytes() + bad = json.loads(original) + bad["orientations"]["forward"]["odd_winner"]["delta"] -= 1 + path.write_text(json.dumps(bad)) + run(package / "verify.py", root, "certificate mismatch", success=False) + path.write_bytes(original) + + path = package / "CENSUS.json.gz" + original = path.read_bytes() + payload = json.loads(gzip.decompress(original)) + # Header, compression and JSON whitespace are not mathematical data. + path.write_bytes(gzip.compress(json.dumps(payload, indent=1).encode(), compresslevel=1, mtime=123456)) + run(package / "verify.py", root, "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING") + payload["forward"][0]["odd_best"][1] -= 1 + path.write_bytes(gzip.compress(json.dumps(payload).encode(), mtime=0)) + run(package / "verify.py", root, "census mismatch", success=False) + path.write_bytes(original) + + lower = root / "research/complex-dyadic-lowering/lower.py" + original = lower.read_bytes() + lower.write_bytes(original + b"\n# source mutation must be rejected before import\n") + run(package / "verify.py", root, "source SHA256", success=False) + lower.write_bytes(original) + require(inventory(root) == before, "mutation fixtures were not restored") + finally: + writable(root) + print("PASS_GAUSSIAN_PACKAGE_CONTROLS read_only_export=2 corrupted_artifacts=3 equivalent_gzip=1") + + +if __name__ == "__main__": + main() diff --git a/research/k8-gaussian-unit-rounding-seed24/verify.py b/research/k8-gaussian-unit-rounding-seed24/verify.py new file mode 100644 index 0000000000..7e3d9b8c88 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/verify.py @@ -0,0 +1,237 @@ +#!/usr/bin/env python3 +"""Exact replay. Hanson Sun with substantial OpenAI Codex assistance; Apache-2.0.""" +import argparse +import copy +from fractions import Fraction as Q +import gzip +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import model as m + + +def primitive_map(word, registers): + rows = {r: [Q(int(i == j)) for j in range(len(registers))] + for i, r in enumerate(registers)} + for op in word: + tag, target = op[:2] + if tag in ("add", "subtract"): + sign = 1 if tag == "add" else -1 + rows[target] = [a + sign * b for a, b in zip(rows[target], rows[op[2]])] + elif tag == "copy": + rows[target] = rows[op[2]].copy() + elif tag == "clear": + rows[target] = [Q(0)] * len(registers) + else: + m.require(tag in ("double", "halve", "negate"), "primitive matrix opcode") + factor = {"double": Q(2), "halve": Q(1, 2), "negate": Q(-1)}[tag] + rows[target] = [factor * a for a in rows[target]] + return rows + + +def check_macro(z, word=None): + registers = [(name, c) for name in ("T", "S", "W") for c in range(2)] + word = m.lower_gaussian(z) if word is None else word + rows = primitive_map(word, registers) + expected = { + ("T", 0): [1, 0, z[0], -z[1], 0, 0], + ("T", 1): [0, 1, z[1], z[0], 0, 0], + ("S", 0): [0, 0, 1, 0, 0, 0], + ("S", 1): [0, 0, 0, 1, 0, 0], + ("W", 0): [0] * 6, ("W", 1): [0] * 6, + } + m.require(rows == expected, "six-column dirty Gaussian macro") + m.require(len(word) == m.gaussian_add_cost(z), "macro cost") + + +def check_boundary(a, odd, forward=None, backward=None): + honest_f, honest_b = m.boundary_word(a, odd) + forward = honest_f if forward is None else forward + backward = honest_b if backward is None else backward + registers = [("X", 0), ("X", 1)] + z = m.gauge(a, odd) + expected = {registers[0]: [z[0], -z[1]], registers[1]: [z[1], z[0]]} + m.require(primitive_map(forward, registers) == expected, "boundary forward map") + m.require(primitive_map(forward + backward, registers) == + {registers[0]: [1, 0], registers[1]: [0, 1]}, "boundary restoration") + + +def total_gauge_cost(events, assignments): + """Complete scalar cost, with phase-zero optimal boundary circuits.""" + factors = {("L", h): m.gauge(a, odd) for h, (a, odd) in assignments.items()} + cost = sum(2 * abs(2 * a + 1) + 4 if odd else 4 * abs(a) + for a, odd in assignments.values()) + for ev in events: + if ev[0] != "scalar": + continue + g = ev[1] + if g[0] == "add": + z = m.mul((Q(g[3], g[4]), Q(0)), + m.mul(factors.get(tuple(g[1]), m.ONE), + m.inv(factors.get(tuple(g[2]), m.ONE)))) + cost += m.gaussian_add_cost(z) + elif g[0] == "scale": + q = Q(g[2], g[3]) + p, e = m.parts(q) + m.require(p == 1, "original dyadic SCALE") + cost += 2 * (abs(e) + int(q < 0)) + else: + m.require(g[0] in ("copy", "clear"), "full invoice opcode") + cost += 2 + return cost + + +def rounding_checks(events, helpers): + results = [] + for pattern in range(4): + assignments = {h: ((h * (pattern + 1) + 24) % 9 - 4, + int((h + pattern) % (pattern + 2) == 0)) for h in helpers} + odd_count = sum(b for a, b in assignments.values()) + gaussian = total_gauge_cost(events, assignments) + low = total_gauge_cost(events, {h: (a, 0) for h, (a, b) in assignments.items()}) + high = total_gauge_cost(events, {h: (a + b, 0) for h, (a, b) in assignments.items()}) + gap_twice = 2 * gaussian - low - high + m.require(gap_twice >= 8 * odd_count, "common rounding dominance") + results.append({"pattern": pattern, "odd_helpers": odd_count, + "gaussian_cost": gaussian, "low_cost": low, "high_cost": high, + "twice_gap_above_average": gap_twice}) + return results + + +def reject(label, fn, expected): + try: + fn() + except ValueError as exc: + m.require(expected in str(exc), "wrong rejection for " + label + ": " + str(exc)) + return label + raise ValueError("control unexpectedly accepted: " + label) + + +def controls(): + result = [] + def add(label, fn, reason): + result.append(reject(label, fn, reason)) + mixed = (Q(3, 2), Q(3, 2)) + word = m.lower_gaussian(mixed) + second = next(i for i, g in enumerate(word) if g[:2] == ("add", ("T", 1))) + add("missing_shared_target", lambda: check_macro(mixed, word[:second] + word[second + 1:]), "six-column") + wrong = list(word) + wrong[second] = ("subtract", *wrong[second][1:]) + add("wrong_cross_channel_sign", lambda: check_macro(mixed, wrong), "six-column") + add("missing_product_initialization", lambda: check_macro(mixed, word[1:]), "six-column") + unit_word = m.lower_gaussian((Q(1), Q(1))) + add("dirty_work_not_cleared", lambda: check_macro((Q(1), Q(1)), unit_word[:-1]), "six-column") + f, b = m.boundary_word(-3, 1) + add("missing_inverse_boundary", lambda: check_boundary(-3, 1, f, []), "boundary restoration") + broken = list(f) + broken[0] = ("double", *broken[0][1:]) + add("wrong_boundary_shift", lambda: check_boundary(-3, 1, broken, b), "boundary forward") + add("operand_alias", lambda: m.lower_gaussian(mixed, ("T",), ("T",)), "distinct complex") + add("outside_gaussian_support", lambda: m.lower_gaussian((Q(1), Q(2))), "Gaussian support") + add("nondyadic_coefficient", lambda: m.c(Q(1, 3)), "nonzero dyadic") + add("gaussian_nonunit", lambda: m.unit_coordinates((Q(2), Q(1))), "unit diagonal") + add("zero_factor", lambda: m.unit_coordinates(m.ZERO), "nonzero Gaussian unit") + add("false_one_step_lipschitz", lambda: m.require(m.c(2) <= m.c(1) + 1, "unit discount jump"), "unit discount") + # Ten repeated edges disprove independent rather than common rounding. + gaussian_toy = 10 * 2 * m.c(1) + 12 + independent_mean = 10 * (4 * m.c(1) + 2 * m.c(2) + 2 * m.c(Q(1, 2))) // 4 + 4 + add("false_independent_rounding", lambda: m.require(gaussian_toy >= independent_mean, "rounding must be common"), "common") + manifest = json.loads((m.HERE / "SOURCES.json").read_bytes()) + missing = copy.deepcopy(manifest) + missing["files"] = [r for r in missing["files"] if r["path"] != m.LOWER] + add("removed_source_pin", lambda: m.check_sources(missing), "source inventory") + altered = copy.deepcopy(manifest) + altered["base_commit"] = "0" * 40 + add("wrong_base", lambda: m.check_sources(altered), "base commit") + add("modified_lowerer", lambda: m.check_sources(reader=lambda p: + (m.ROOT / p).read_bytes() + (b"\n# changed\n" if p == m.LOWER else b"")), "source SHA256") + return result + + +def compute(): + word, programs, bindings, _, _ = m.load() + helpers = m.domain(word, programs) + m.require(len(helpers) == 237, "eligible helper count") + census = {} + result = {"status": "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING", + "base_commit": m.BASE, "assignment_seed": 24, + "eligible_helpers": helpers, "seed_selected_probe_helper": helpers[24], + "source_members": bindings, "orientations": {}} + coefficients = set() + for orientation in ("forward", "backward"): + events = programs[orientation] + rows = m.census(events, helpers) + census[orientation] = rows + entry = {"census_rows": len(rows), + "integer_breakpoint_evaluations": sum(len(r["real_candidates"]) + len(r["odd_candidates"]) for r in rows), + "rounding_fixtures": rounding_checks(events, helpers)} + variants = [("baseline", {})] + for name in ("real", "odd"): + key = name + "_best" + winner = min(rows, key=lambda r: (r[key][1], r["helper"], abs(r[key][0]), r[key][0])) + a, delta = winner[key] + entry[name + "_winner"] = {"helper": winner["helper"], "a": a, "delta": delta, + "incident_adds": winner["incident_adds"]} + variants.append((name, {winner["helper"]: (a, int(name == "odd"))})) + prices = {} + for name, assignments in variants: + stream = m.transformed(events, assignments) + m.require([e for e in stream if e[0] != "scalar"] == + [e for e in events if e[0] != "scalar"], "non-scalar stream unchanged") + endpoint = m.replay(stream, assignments, orientation) + price = m.invoice(stream, assignments) + m.require(price["complex_scalar_primitives"] == total_gauge_cost(events, assignments), + "formula versus emitted complete invoice") + for ev in stream: + if ev[0] == "scalar" and ev[1][0] == "add": + coefficients.add((Q(*ev[1][3]), Q(*ev[1][4]))) + prices[name] = {"endpoint": endpoint, "invoice": price, + "gaussian_macro_stream_sha256": m.sha(m.canonical(stream)), + "assignments": {str(h): [a, b] for h, (a, b) in assignments.items()}} + before = prices["baseline"]["invoice"] + m.require(before["complex_scalar_primitives"] == (149002 if orientation == "forward" else 149018), "retained baseline invoice") + for name in ("real", "odd"): + after = prices[name]["invoice"] + m.require(after["paid_profile"] == before["paid_profile"], "paid profile unchanged") + m.require(after["complex_scalar_primitives"] - before["complex_scalar_primitives"] == + entry[name + "_winner"]["delta"], "census versus materialized winner") + entry["programs"] = prices + result["orientations"][orientation] = entry + for e in (-16, -3, -1, 0, 1, 2, 16): + for p in (1, 3, 5, 7): + for phase in range(4): + coefficients.add(m.mul((p * m.power(e), p * m.power(e)), m.gauge(0, 0, phase))) + for z in sorted(coefficients): + check_macro(z) + for a in range(-16, 17): + for odd in (0, 1): + check_boundary(a, odd) + result["local_primitive_checks"] = {"distinct_gaussian_macros": len(coefficients), + "formal_columns_per_macro": 6, + "boundary_pairs": 66} + result["rejection_controls"] = controls() + result["census_payload_sha256"] = m.sha(m.canonical(census)) + result["scope"] = "Written common-rounding theorem for the specified macro-local lowering and separate two-register boundaries; finite exact k8 evidence. No native hosting, new paid profile, kappa or full multiplication theorem." + return result, census + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate this package's own certificates") + parser.add_argument("--json", action="store_true") + args = parser.parse_args() + result, census = compute() + if args.write: + (m.HERE / "CERTIFICATE.json").write_text(json.dumps(result, indent=2) + "\n") + (m.HERE / "CENSUS.json.gz").write_bytes(gzip.compress(m.canonical(census), mtime=0)) + else: + m.require(m.canonical(result) == m.canonical(json.loads((m.HERE / "CERTIFICATE.json").read_bytes())), "certificate mismatch") + m.require(m.canonical(census) == m.canonical(json.loads(gzip.decompress((m.HERE / "CENSUS.json.gz").read_bytes()))), "census mismatch") + print(json.dumps(result, indent=2) if args.json else + "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING helpers=237 orientations=2 real_saving=332 odd_saving=58 controls=" + str(len(result["rejection_controls"]))) + + +if __name__ == "__main__": + main()