From 108428fd916ab5c08fbd8acb40583104c433488e Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Fri, 23 Oct 2026 19:21:41 +0200 Subject: [PATCH] Prove fixed chart heights cannot improve productive helper invoice --- .../.gitattributes | 2 + .../PATHS.json.gz | Bin 0 -> 10677 bytes .../PROOF.md | 117 +++++++ .../README.md | 125 ++++++++ .../RESULT.json | 131 ++++++++ .../SOURCES.json | 48 +++ .../TASK.json | 77 +++++ .../VERIFY.json | 32 ++ .../calibrate.py | 50 +++ .../check.py | 303 ++++++++++++++++++ .../verify.py | 28 ++ 11 files changed, 913 insertions(+) create mode 100644 research/productive-helper-dimension-floor/.gitattributes create mode 100644 research/productive-helper-dimension-floor/PATHS.json.gz create mode 100644 research/productive-helper-dimension-floor/PROOF.md create mode 100644 research/productive-helper-dimension-floor/README.md create mode 100644 research/productive-helper-dimension-floor/RESULT.json create mode 100644 research/productive-helper-dimension-floor/SOURCES.json create mode 100644 research/productive-helper-dimension-floor/TASK.json create mode 100644 research/productive-helper-dimension-floor/VERIFY.json create mode 100644 research/productive-helper-dimension-floor/calibrate.py create mode 100644 research/productive-helper-dimension-floor/check.py create mode 100644 research/productive-helper-dimension-floor/verify.py diff --git a/research/productive-helper-dimension-floor/.gitattributes b/research/productive-helper-dimension-floor/.gitattributes new file mode 100644 index 0000000000..44a23d1fe3 --- /dev/null +++ b/research/productive-helper-dimension-floor/.gitattributes @@ -0,0 +1,2 @@ +* text eol=lf +*.gz binary diff --git a/research/productive-helper-dimension-floor/PATHS.json.gz b/research/productive-helper-dimension-floor/PATHS.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..cb5c70f1c685ac5605c578a71a4cc5c6a9020e5c GIT binary patch literal 10677 zcmajFWmsEVv^89(rAR4IN{|#UR*GA&LUDq-7k76GZE+|Bmr?@7f);lxh2rjRK^i;| z+}_PO=icW&-=B~C$WF5MSTkeJG3I<$07pE&bNhD>dnau+%B0)r=VDID7WH6=R|2ld z+t`^zBZtUg&@7qmP=nwNTlXI=eSYc`j=T5ZPlK#$H8d(XsA-UwH%GmDe&<&$*OQ8i z*ZXTBEq-Sw>3(NO!{*C<|LgO$E%5c)7EI*k`s4<^Gdl@f6bfUSjxba@!e4Ca@Mcmk z9#bXm6MS$Z_$K^8mj7n7GpWS?dTmzGaI_GcN-2-0c^)et&@*HXCcMWquo}kDE_pV2^ z*7ZqmruHzZP;@}cMlb%MjsMwsI#Tzm6jjhA`hAN#uH{E^_(?pNNSFj#j*-%tiSxdGaI#Yb$r;O@3CKw1qAJI zbA2=mJ50-6Y+g0-SQh6BgPEj%0pBnP<6TGjkNH@Bf*pwooBJoh%wVvyB@-TBA|G7v zML29SA!p2l&VSR+jM1u9s!8N*s%hCoF%edi5Dc3K``QM>7IcL>=)hG0iU-4jXeUQm zvREweM>2BqS>+`o5?nmtW2v*3dk1AZ=rXWxQ6g;mfW3nl%r>`w9)Tyksn}FpMCZ3o zv)9(SYJWpN>rx~?5Hjeydez48jw{;F9M`TXu?Pst(M$+JDs-(tUA;_t|-SJ6B%#;sDFo zeR0MQ*h|im)7P^G(ze8tA~dYV`ea-!$M~#>z`8!su+YWDwXCR4JaDg5FR@Fnx(}uC z^a&79Z;!R+#OT#ajT7V#&BzC(GLj|r_4VMkADUTBU`6lo6Jmga!Gp5a)~Fz4nIpMx zpQGalHW)l!xbxFM!N;x5dLb!)`ux7RLu~~8B0@F9zH=4OOL{@F+uO@ZWAi(5+%6pElKv?{cq&V@qFpk zqXfFef`EbawJbLj^TwZ1V~?#3+GZc#uW?JGZ~wHFI#+O|n$o=JKFc`VKy#h_uy}vu z5+fBIg0tx=O&<}*Ld-TzhM$(V>i#l>R44e-^d#fb)I-y+C-L&suS)#`7YM5Bai@V_YjB3qVt}e@nH;S*{2o&sl!M zoK?ZxYqhrFAh>8@hNeejr71yQW#8e+Ofxn@$|+u7VH%<%Nr=iTVn|SCgLE8Bi@yp=d7z(5rv(Kv8TS-ctce(Ye_CseCMR9NH zZ0<5cx_ZEBFC708=wv{4rqFm>bH<$}7E&P(_dG$TpuRJoQ{}gnyjGW}@fGbzY?AIX7rz9*P&@z&o&zpZI;jShkCY zm24}Yj_%H$TW?5uAit)5PHU?^ehQBrOZH|@_WXHmltrR{+E}jdHZ~N|y7|X>B;sjg z&&A)@d)rOcEq0W-71B_tKIzQMB)s~%3`CT zzT3>gl+E@P=sCymjoh5HLJD7%PM&S;`D{GA598fwQk@zD=HjDJf7dz900c@I-r+6P z+0!*YRJIJVIATwhzOeEaN=Z_L2yvN3ba${p1t!>vG!|O^YE`JDn!4HQqo%f|F$?QD zwtft$35kd@VT1`5R@e^H2t5;+3x&rDtscsFsPkS(IHWP|%R}{V+doHEt8hR+eBWF_ zUMsqFJe^Rpib*%COGqS-uNuKOlWYeOlqG7V0+#0z#3M{vPFbZK5KQ%)fS-KqLd?t< z4@6xl${at)oUSH3JkJgkj$f}5+#T-jw^2&=-fLz<^{U!9Ekg1tSPhd(=n%yjvWiGp z4GCJU5uA~KgA87s%zBjdt*9ma^Ei#>UlQJrLgm-o#0}+ejW><%3oWLk3K+Ts)x@%O z^+a^0m@1~mA>#D{i)8v_>>|AKO(uk77^iqhIB)yyAAdBG87@Q#SqP7aNjLe_v%cDR z`ik*=y{Yt%CxSJ)42h#LA>S#-0#QF9r?qQA;Ne=!iUEcNPgQLbF5~8z{C*wA^8kl~ zq23Q>hf=h>9yWIMsXt|K2d^&s z0~`|(%k86$_49MBs=5RtTVaU8ZRm9sc5%ywm?KYEJQnpDW1G|(1&wm082W*WS2S#T zUMSUT@Bp&uB3t7|F@bOCWtJ1K`#!XS8JSN_Tg3Ek?nhx-@#7~Nnief1<5GcD(>Sht zW*MU+0YiAgC^6FknwSI8Y)C(gR5C-^yD}bdab>Ru^UkGtj=tdKr%hH~sE56_X|Jch z`m}0#{&t!2H{bA)RrPp!a$>4}bI5N-WK0reyJSw9^QyRFzs|F>Pv!VnlQUVoCUz&4 zmNVt?a|Bdz?k%X_riz9qg`<-W>g0bkoW66+*CceSIq5a=Iy645ZvXpxRfAx$-gvL; zC(6s5zINKw%)|`^rt6rd9RJckzb3wbY$F(V9zJO8P(Ck!R_P;++nB4}E%>I>YNT~I z3|s|Il~}=04;3b6VXhM{aIhu|9?@$J6Ui)Pv7tPhUf4v{nxdOs`kB(nspFK-z>E)~ zevdNAmoHOgL6UQX@f!ij2Gto7LTj>D_?>(G8ORPlYRtT5ob`%}+$M?n zsarJKu{Pyf!O=e6vxS1@_TU9mFw03>(Wzf~vAy&Aogu9*RdzY+SQ)fj76i|6AOgo(5{I+n=ETc7B`>7 zO%zMexOV*v#rVwbytfKcqG&*6zf%?&z@N&m^4hP8gWQ5~s$x~q!pf=)bM0$Kd0v}| zVBRQj{z+u!q!#X-8H|(=E3?kK1pCVabCfk>EK_%<=9+{)#&ucmM{(E(m7vk1=Il)| z-MrccO5<)HP(6i;*^#XPYI;gT#VxW`+21X$z%RC-GP=Mf&~jfud%BBZT1!@4SmQ;* z$c!O>(0GrtbONV}8S}DSDDy=`lfR0%W_EZoyk13ulgMs9H&`;313>^ zH$_Nttajp7NmRAkY$CPd^Ij2eRxUWyK8o!{?MZ^B97X?XDMd_05%sjw-OY)gOiAQw z-cCv%RdU*xJ`$^YWLgrAJLGMO5h*Caz2TC=u*={Ftc`}Jjr)FU7BV*(MG3^p-MeEi ze)O!Uz3)So765&h^&H3Xg*4G9xB0D zID2tgJ?@S?Q*9DuEL5F}@)4Q#S(Ic7$EMJ<$cOkRc5yO5)m9_`@s1O(pt|+ zp5N!F6dmq?H^5!ShdZNm4Tz5fs_ViP6M+tn7ir`UF~2lf1Z3DYTpRrY}+gOuJ!&*Vgt3JFwLJ(Wc5ce&s40iT=B{;9@mvJOhH_i)j<+5^xJCryHS%7FKqOAG#rzMnTymMt7QeS0fXf*f3I96&lN+1V`Z8Y+&5lJB$R1IAN8qg!Ub0qJ$x>yg7L;0# z9mdyR7E8p_Amhv;vy{fYgEcG>PkU(W&XlbhwuUE#VAr4;-???#8Yr2O%tB`X@w2*HBhhIJ;QO%0**FR##TnUuR~2O{f{t zgc~)$x7fXX6s2}_RzY19MG6}8!vkfM!?GGHC2Hg|!JLdG?3T-MzZu*%i=~=8{U;+z zd<+@|cYoUYq8Feu7Hbak5N?Nak}0AJ=NJO`-i>|YUoDw(r*E{JYjKdgsIB^ug(P>` zcCBem<`OrX?$evn9%&UF*;tQ3xsmN+G0o*as@ejt>tzp?eWhjuK!r~CH#bCWUn>p1 z@Zvl$&n{z}z$-bses5ls;~KuHs&uSvzF9W1P=d(wQ;@R~%si)uK0GX{ z%*m+~+MD-qB_>RTD0hn*w)WlUml4g7<>;G=MnFS(X&j>1)_-&2O}{TmMiTW)0Us~3|y}G!YpT$#A^`)feaU#YxMVPS! z3^}O1qcA{lUbE0r`YCT6r}oW~;)rVEh$=pc{aU}MUv^Ny;K~*O=TZ<|q_zCa(~Zl? zM_$DRGT^k7jEyHy=D-Wb>8@AoGmt5!5tr6Vr!;((cx>sRTQ@tueo{aC+ll1V+H8rO zBG1m)X>kSHeIU7)0i~@*GjM{yp=B20X^Wk)j)lsFV3N-*dFG1r)HDW95ExHpp)(?i zeH)ZlJsX}r$7_z&7%Hcaw#+ z!kQUMHsUh(aAAyg-vUHh`~Gz?rc&Hne&@TO)CV7Z8AU$RUs`NbopCrUIUCkF+(^RG zWpgtv8AajD`?)<&=(SPWl32ce2HvG^$$2mCab!>BpA*JV?v{L|B?!Y+4bDrzo9Z1) zrlUWmjeHz~F}jM5+mRn5|IId*;@ycti)6>VQbB{ZjPuY!qAuiqH1t!^Qkv^NGeCbgV!k+qnw z2$w%@+t{427FPEkQ^!K=bza5oT)AwPTgl6P zqL{=pRZci2c^^z_D6L1IzY}54VX>Nt zqeTtBtZ5-b+WT;ONo~KKl1W9R@RluDYdO4dt(7!jCtZFzx*D>g+LMvGfn;nn(r&r!~YwMxi+UcS2)i)SkKjisbfMbHv3o%cN%Ef{|=zV%qY? zwND^g^(iSSweA;v^7VH551&3mg4eBHv6Jd#oEn;DA!vuUzRgsI9E=H#KJw;*QtWo* z&l-FeI1~3S!gUQN*I3jX8O1|A(eQ@qFed`?dQsUw0LT1_{+xp$KS}Q&=uma9ZYb5! z#zU1|PcjN_O-xVk+kT%>O?Z~~7)-?Iq`K&6p`buh7>b=DYWKAnX9D&iOz%%@g3K_l zDSw_EGl+y4<;As2zT1(edlq6o8fdi9UOQU!6SN}h9hE@;g%EngQbu1B3#Zw&t*GdG z$jeb$o&j^1m2dyl&&#YySUk&~GB=PIV65Stc&)iVsQJrTHzo-eL${>M@5|g7uZAdq ziJ8#|`X0UAGNvYuh_T|u&@q^E)A?<@#m)C%mH!d{N1vSHcrI+dKRjmN5+X1cDOJg@boc0ssGdQ zA}fVMgk)Dxz^!}MWiObo;sk@CH($w>+(~%cCe=fo! zPL(`hac#=1?nI}qnMx;K3F^jXsSOfRgmsJi}_ja+kXlq&S@tzus<5a?$Ci9mLPYXUovUwqw41 z#Sq!oe1UqqF6ch-K#qN6gMO5^dE9ZnI#@X}sxhJp6qv>_qlk)&w#?vo&n{1!0G7+5 zsgbeSNn68KE_OIBFY~OdH(vYW2<1Ds4d!FzzU%jIr{xiz7N$&GDGxpd4xe8Z(CiB+Wd3ffv4{O34N6swsP zRmyup4z5?OQM;cnHZ(JPP<#8Jrne2Qf2zt@=a}R@9z1z9FvriU9y>wNczkG|;{DlP zkKQ!tsJ)K3WKR;NNw`6|e6*uy(YrNTtdv;u&OoN0CN0N&>K9P0ett!Ryl*;OhcUDj6kw<}!aF$wY==gZZA=&}d*PqaJJ zjP|jNf3=IQ!QK)+m8J82w%(2N_vY0TCgtIW)W#{#NWjLRI&gNK(n}5%T9wK!>$fvl z=2d-0;aBRLCF^&Ij|!L4*Y74=`Wta|uf>L2CVsg=HS?T^u!su#rRGBYXwnfkW-e%^zzfujJ8m&NZwIL&W>~|*J&)) zhxaIqil#jk?HVbU6!!KGbxxaah7ZrBg=ibgkeM+R@2K)Bqg1L|KWW?-* zK*Q9ND({;)HtwK@e+A%w^M6@cXu`jsdVgpMi&ZoLtg_4TI%mNQPa3yNCWbmXj8Xm7 zeK8ka%g;l6Jo@KM#VYq>e%l6s1t<>IOvj|P-#&xl^)7{k+r7l*J#E$E!wniWl8p=^ zyEJ+`w-mDdrlZY@Z*ECSEj38eH=kd|1jR*dzc0QXwq9nPSg_m2b^2pW26U-(52|_@ z-=PoyW_qMlR@t#$Frn*GJhBwhb1=@Iks@uiFHXm>*`T}}Ym}mPO@ApwtdD&zarh<> znfOQqSQb3`1fK=hFS`{#;S5_-_Rkt{11mNttEdAG?7)u;ygYmZtW%;KSqfTzlQ*r) zX*M$D|3fmT?8f>^qoRBNM0o5DyyLo1T@JYqe8RnW`^k>H$;~+5ci?S&MY}kw?G^!{ z(JB9`s6sK#t9I*8nlL}m1-zr#rt;lC&xo=;YrEl6A@0CP8>>r)M$ThMq>$#J7o`up zQ`qLWC*{R=;905ioAJTa2IQC@cGYjk-WIo6EBI+!x7DlW9rKYVa|Rah9OgS+Lm zov$-74ld3;f*h-*&2NUO_j*(M)5y>Geg@-)&+5;wRK{(m) zZpbkQtVu1-htemd(_p>f7yv^?UU=d5pzSrl%*JRDr4lx*yKWuWnlEuuBx zn^w~D7wn^n&?GZ5^oRqEL5E#??>?x#_wkC^BjZ8RIqcHL#)b^dM(&lIS;@wt+0Y~} zU}4iEbgZ^gk0$@YQm3BzI@!5<%D^Q6Vnv4L06-=HkYiB0oVg66;Lgl z&VvOIy4>#H&zmDXwG9G1pI~#bt1I!|BPjXNF`VZ#vcK>TO1bSntK?1ql+rh0A%^Tt zR}cFIl|%`o16#OP%z#*2fmr;2{eW1W+j5`t%t^FlJ1a+}W;|}Kp?&p<*!7hGD3A;$ zxF=SQ{`1PK!6I zQPl)&Z9FSx3zCg2C1Q=3M`-5(0oagl8jkl4*2YHrgS(ybch{{y^&v!Et^>6-S~^)q zN53k>Zp8ZwsLPj};1;tOzU{r`=Rf``BRxq0%q;-Z8+T=`UHUtv#U1qXr<2S1rj3Jo zi$E3tCW8T{0VbybCbgHB+S&dLq@6ytj1g!`Tme>a04oxK6}12suwq)Qj<$fexx%t# zfK#~sfHO4d6^_6^Kb&;z42vw&o$R4wQ$)m7Xaj~c{|a(YoYV^yh$*}ox(0IMMusl8 zr!lDh7j3$RfDLK$jIA~1z8kR@x^J6iHA7%VTOpN=yXsxzgX!m$9wnl%|nj*mI4h>RZlU03uELsmc3jTm^4dH$oY3r_fARDh}{!YnVMQ&-BSwD+j zls+JaqlotDmOP2UGd3Y2NZ){JG=D3r6|O0?luhS;3gKno#Az_*L4eZ@P^<9W+n7A)%CAXLeF{n*UA?Y-C& zW`V%nt$AuPNr<<-s^8Wadjy`bon;@$>;UpSA@fX*L_{Le5EKykw>*qy_q23ElQQ%Q zhI%<;ra4VC>JOU;*hYc!nwD(b2DF6c4oyOt9LFoz28Dfg5pQgVm3SU|?i(%1e-Fx< zWC@6x5^J=5WdKcIAZzapi%$mX>%UsPW%RbbQc6Ox-h58`oW6xRIWU_rAGT->+1n-Ca``g+()cO{%^RqHnao4kY@kUetK_{g|lSg2$GO$+G`s5ue*iYyb z#-@}OfJgx)9RHWnFn*mMT9KH)bWD#yZgvh|J+%Ry9RfsnK3vI}3E;W}-5xpDA5&12 z6D}@r+O=~cyEtW}>#Qw&&>Cq|9!}XbkFs zO@P{%1|X3Dq!;drnM81O!56iJu(WW@r(aNsHdQ*3U)9)sCouT|XuiUO@yEfSV$U8; zGxJr`T&6VvG%HP4qV+g4zoKui(K9wL#9`&37lOa!urk0lUr+zXn|!4bHEdE-+$EBS ziz*|Avg>h>VIb`z*SYkScbcI}qjAsJ#_u6IXsC3dbG?rhfMP%pK>E5yA5)sITCD;n ziNJ%g_S^X+_cScH0XR9r` z+;fBOq_qrkS9-$mj*4M36T!KGZKrTVq0XmY2)Ng+YS{%!9< z0+r`^%Q+Lx^_%VDzP9<7|$MOW5&<$unVwO4(2RTbD0k4(vqkn%Gx(pOtQu z_@XwpH@_hH1qb-C@7*z3&=MQ#K1qA8xA?joL?PpZ4o(k;2DSkIF`&v_ELEklMHPt= zZsz@`Ki>AF{~BrVtTyn7zX0hUz!VcFVuQ zN9;8aw<9ErvABzlsB_5}*7%qBq@FtK483a0XKW1TbPUhF%AOD7RZhE#Cqxc$4Vy5; z+VX}brL&uoe!7dzdMr;zqLUB+NMGo2DZFB}HRNci?L6%5mc4ZO;rA|$DC^K?p0@rD z|K#|#rQB*B(4sAn<7~ko{vhE&KjOE|U8sOqWUG2+xoAej_Y}TiHnCu{X6p~lOze?? zBHzm3omS{Q!1MmQf9l^^00oF}ib?**etQd~A{*j_Gia)AXnr$VX*|^GwP_^Wy7*34 zYCnwTdCCZ;K3M>NLGRuUqpE7G1$S5nGUCfqMeeYcjKgNu6*BzCCCh=tkm=QHl_#4I7MY zDorP^o3`_Dzn~fE5@r}0S4|&xYFDCQS5w4M&j|w>{H;1}8$2+1{Ev(MWm<`WH!5e8 z7_EQ)g@yl$KZKO*9vN_Kx!T{}_*Vi;E)xM!PW^qyR!03JK!5eW^!*=+Z9nQJ1yl5y>CJSVfo=e^uvtkJv(1&$cDxx&~^ZG`v>E;cL9NXytS4^ zQ_G+)$F5@d;wQA(Of)i2Dt|u+o_gqDzhdC-*cMG?dnhc_{OooV0Ic=@BTS*!NnO!W z!4PR70A-#(YbD3`FyXRDQ_B^#uJMgvmdvB^n^=U?#}+5VSY<9|niT%f=| zY`s-h*cr&o2pncyp|{tPjC})u4n4eju85mWNq>CDkPg*)?(~Zrx#`-}^q;e?3N{)>pz-X9^2 zw-pT7%55GlfUge>T79=JRUO{-jP%Fb;ii0~$LL}GtFX^bzc8tMsE2jW{DqeWv4T?v z2{uNb|4z4%)gI|X)JQhs0Cfg*`P-Io+iZX?FK7QV5E8@sgs?Ehz*ODOChHfp_EpZ8 z+;{fZ;con8sxdEJReDvuPrW2TfG^#8+^x-*15+Q6i?&;jtK;C1sHT;VU*{>qAsdN{ zru;?HCD|E9EXf1f9t(u9KNTMd5DNTQ+<^oFU;zRENW8_l?Mc9-+-n`367!t*2-jm` zjEk@>%qwq+B)7MJje%!5p6oB?cbBtLm;qM?2I!=>T?Odaw>9_?z-R^r%}uf*@cHxo zV)Et$6ODrVG~=IfMPkx_7lrWC+!@~^_>|f53i3n~ua7}syN<9Sm6&EP;-3a}YXtvS z$fA9+_u@P6b|e4xx_IgmYKAja?K!m_FwB+uwZdW{VkyO#j(_^}Z6a?OXpHbYd$uz5 zXoU_Gx-B%MfVV_XvK}A!cvFw#v1`yp6m(v?I-&97S3-Y}m7y3rI}BWJzl;8!{(F&b z2wlz>fZB>Yo3XkZZt>9vPGD^>rRRDXjB@jc+%INko!7*#D38|J+45u(t8D=X42Q z57s05i@^Pb7Aen@qu|ei>= |d(L,Z)-d(M,Z)| = |k(L)-k(M)|. + +For completeness, triangle inequality follows from +dim(L intersect N) >= dim(L intersect M)+dim(M intersect N)-n: the two +intersections are subspaces of the n-dimensional M, and their intersection +lies inside L intersect N. This proves the needed metric statement without +any isotropy assumption beyond the common dimension. + +This metric is standard: Koetter and Kschischang, *Coding for Errors and +Erasures in Random Network Coding*, section 3.1, Lemma 1, proves the subspace +metric dim(A)+dim(B)-2dim(A intersect B). On equal n-dimensional spaces the +distance used here is half that metric. The source-specific path accounting, +not the metric identity, is the new application: + (v2, 25 March 2008). + +If k(L)=0, then L=Z. Consequently a helper with zero entrance projection has +rank k(M), regardless of its exit's quadratic form or projection direction. + +The original paid edges are nested canonical charts, so their original ranks +r are the nonnegative differences of the source frame dimensions. Arbitrary +new Lagrangians with the same per-node projection dimensions have paid ranks +r+delta with delta>=0. In contrast to the canonical theorem, delta need not +be even. Every original native rank is zero, so arbitrary changes of native +maps cannot decrease their cost. Owned costs are held fixed. + +## Incremental concavity pays each helper credit + +Let H be any nondecreasing concave function on all nonnegative reals, with H(0)=0. +For r_i,delta_i>=0 put R=sum r_i and D=sum delta_i. Diminishing increments +of a concave function imply, with s_i=sum_{j= H(R+s_i+delta_i)-H(R+s_i), + +because r_i<=R+s_i. Summing telescopes and proves + + sum_i [H(r_i+delta_i)-H(r_i)] >= H(R+D)-H(R). + +For a paid-only source-geodesic helper wire, R equals its original residual +rank. The metric triangle inequality bounds its new residual q by R+D. +Monotonicity of H then shows that the increase in the wire's paid tariffs is +at least H(q)-H(R), its entire additional helper credit. This remains true +if q= |k(L)-k(M)|` shows that every original nested paid edge +already has the smallest possible rank at its endpoint heights. Changing +charts at fixed heights cannot make any such edge cheaper. Source native +transitions have rank zero and cannot get cheaper either. + +Of 408 helpers, 358 have height-zero entrances, whose charts are necessarily +`Z`; their residual ranks remain fixed. Each of the other 50 has a paid-only +entry-to-exit wire whose source rank sum equals its original helper residual. +These paths share no charged edge occurrence. Every old-zero edge is retained. + +If a path's source ranks are `r_i` and their increases are `delta_i >= 0`, +concavity gives + +```text +sum_i [H(r_i+delta_i)-H(r_i)] + >= H(sum_i r_i + sum_i delta_i) - H(sum_i r_i). +``` + +The metric triangle inequality bounds the new helper residual by the new +path rank sum. Thus each path pays for its helper's entire additional credit; +edge-disjointness prevents reuse of that payment. All other costs are +nondecreasing. [PROOF.md](PROOF.md) gives the full argument for any +nondecreasing concave tariff on nonnegative reals with `H(0)=0`. + +## Reproduction + +Python 3.12, standard library only: + +```sh +python3 -B scripts/research_package.py --package research/productive-helper-dimension-floor --check-only +python3 -B scripts/research_package.py --package research/productive-helper-dimension-floor +python3 -I -O -B research/productive-helper-dimension-floor/verify.py +``` + +The direct replay prints `PASS_PRODUCTIVE_HELPER_DIMENSION_FLOOR`; the +registered runner also prints `PASS_REGISTERED_RESEARCH_PACKAGE`. + +The checker authenticates the compressed source and its complete JSON +payload, reconstructs both chronological graphs, validates every source +native rank and the full paid/helper invoices, and records all 50 paths per +orientation in the deterministic `PATHS.json.gz` receipt, bound by +[RESULT.json](RESULT.json). Each orientation has 1,016 selected +paid edge occurrences. All 448 source adapters touch only main roles. + +Eight corruption controls reject source changes, missing old-zero edges, +double-counted debt, and native transitions inserted into paid-only paths. +A separate finite calibration enumerates all Lagrangians in dimensions one +through three and checks the height/rank convention on 18,459 ordered pairs. +These checks remain active under `python -O`. The checker imports no +predecessor graph builder, compiler, optimizer or numerical library. + +Parent and independent agents checked the source paths and the argument +separately. This is not independent human or proof-kernel acceptance. No +new physical word is emitted, and no new phase, compiler, precision, supplier +or outer-theorem admission is asserted. + +## Scope, sources and credit + +The only live input is Cao Yifan's round-three word from +`research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz`, pinned in +[SOURCES.json](SOURCES.json) at canonical main +`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. This original-source theorem does +not depend on the compression or finite fusion certificate in +[PR #5301](https://github.com/CrocSwap/integer-mult-bounds/pull/5301). + +Each node may choose any Lagrangian chart of its original projection +dimension, including a different projection direction and quadratic form. +Compatible shared native maps may change. The proof even allows independent +native maps at different occurrences and independent chart choices between +orientations; actual physical constraints may narrow this relaxation. +Owned-center tariffs and helper contracts remain fixed. Changed projection +dimensions, owned costs, scalar/contact graphs, helper contracts and other +supplier mechanisms are outside the theorem. + +Related path-floor work includes Matarener's +[PR #5060](https://github.com/CrocSwap/integer-mult-bounds/pull/5060), Cinna +Davis's [PR #5136](https://github.com/CrocSwap/integer-mult-bounds/pull/5136) +and [PR #5140](https://github.com/CrocSwap/integer-mult-bounds/pull/5140), and +zxv's arbitrary-Clifford owned-tree extension in +[PR #5283](https://github.com/CrocSwap/integer-mult-bounds/pull/5283). +Those concern owned-center or other constrained path costs. The contribution +here is the source-specific 50-helper path census and complete-invoice +accounting at fixed heights. [PR #5144](https://github.com/CrocSwap/integer-mult-bounds/pull/5144) +provides distinct nonmonotone owned/shared-map context. The subspace metric +and concavity principles are standard; the proof credits the metric's +Koetter–Kschischang reference and the retained inverse-chart grammar. + +Overlap checks read the start/handoff/native discussion context and an initial +800 most-recently-updated PRs, followed by a 100-PR delta on 2026-10-23 ending +at 13:09 UTC. This is bounded coverage, not a census of unpublished work or +all open PRs. Canonical main was refreshed before this package. + +Credit Cao Yifan's #4610 source word, Cinna Davis's canonical/native and helper +accounting lineage, Dugongue's chart contract, zxv's supplier, and all retained +scalar/Clifford/compiler authors. Prepared by flyingviper with substantial +OpenAI Codex assistance and independent agents. Apache-2.0. + +## Open next questions + +Can a coordinated change of contact heights and native interfaces lower the +complete invoice? Start with a concrete source-derived dimension change and +its full signed paid/helper polynomial, then optimize the coupled native +interfaces while charging every old-zero edge. A favorable exact invoice +still needs one compatible shared map per operator and the applicable dual +native, phase, compiler and outer checks. [TASK.json](TASK.json) records this +scope change, first step and blockers. diff --git a/research/productive-helper-dimension-floor/RESULT.json b/research/productive-helper-dimension-floor/RESULT.json new file mode 100644 index 0000000000..b481b5e249 --- /dev/null +++ b/research/productive-helper-dimension-floor/RESULT.json @@ -0,0 +1,131 @@ +{ + "status": "PASS_FIXED_PROJECTION_HEIGHT_CLIFFORD_OBSTRUCTION", + "source_sha256": "cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd", + "directions": { + "forward": { + "program_sha256": "03e406a5672ada3e1762011d667c79ec04a55d7d1163a9423d0005720234d2ca", + "nodes": 19197, + "paid_edge_occurrences": 34398, + "native_edge_occurrences": 240, + "source_native_ranks_all_zero": true, + "source_main_adapter_occurrences": 448, + "source_adapters_touch_no_helper": true, + "helper_dimension_census": { + "0->4": 26, + "0->8": 6, + "0->9": 326, + "1->8": 6, + "1->9": 41, + "2->9": 1, + "5->9": 2 + }, + "rigid_zero_entrance_helper_count": 358, + "paid_only_nonzero_entrance_helper_count": 50, + "selected_paid_edge_occurrences": 1016, + "paths_edge_occurrence_disjoint": true, + "source_geodesic_rank_census": { + "4": 2, + "7": 7, + "8": 41 + }, + "owned_center_profile_fixed": { + "8": 8 + }, + "baseline_paid_profile": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "baseline_helper_profile": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + } + }, + "backward": { + "program_sha256": "a4ff7b7ca8f23c858f8e6f1044bc6abf92168ab17abd2aa420ad384f58a519d3", + "nodes": 19197, + "paid_edge_occurrences": 34398, + "native_edge_occurrences": 240, + "source_native_ranks_all_zero": true, + "source_main_adapter_occurrences": 448, + "source_adapters_touch_no_helper": true, + "helper_dimension_census": { + "0->4": 26, + "0->8": 6, + "0->9": 326, + "1->8": 6, + "1->9": 41, + "2->9": 1, + "5->9": 2 + }, + "rigid_zero_entrance_helper_count": 358, + "paid_only_nonzero_entrance_helper_count": 50, + "selected_paid_edge_occurrences": 1016, + "paths_edge_occurrence_disjoint": true, + "source_geodesic_rank_census": { + "4": 2, + "7": 7, + "8": 41 + }, + "owned_center_profile_fixed": { + "8": 8 + }, + "baseline_paid_profile": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "baseline_helper_profile": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + } + } + }, + "rank_metric": "d(L,M)=9-dim(L intersect M), L(F)=F^-1(Z)", + "fixed_height": "k(L)=dim(proj_x L)=d(L,Z)", + "path_debt_inequality": "sum(H(r_i+delta_i)-H(r_i)) >= H(sum(r_i)+sum(delta_i))-H(sum(r_i))", + "proof_domain": "H(x)=x^t, H(0)=0, 0>n)).bit_count()+((b&mask)&(a>>n)).bit_count())%2 + layer={()} + for k in range(n): + nxt=set() + for rows in layer: + old=span(rows) + for v in range(1,1<<(2*n)): + if v not in old and all(pairing(v,x)==0 for x in rows):nxt.add(basis((*rows,v))) + layer=nxt + return sorted(layer) + +def calibrate(): + results=[] + for n,count in [(1,3),(2,15),(3,135)]: + charts=all_lagrangians(n);need(len(charts)==count,'complete small Lagrangian count') + mask=(1<=abs(k-l),'arbitrary phase chart projection lower bound') + results.append({'dimension':n,'lagrangians':len(charts),'ordered_pairs':len(charts)**2}) + return results diff --git a/research/productive-helper-dimension-floor/check.py b/research/productive-helper-dimension-floor/check.py new file mode 100644 index 0000000000..44805ea4d9 --- /dev/null +++ b/research/productive-helper-dimension-floor/check.py @@ -0,0 +1,303 @@ +"""Source-bound fixed-projection-height Clifford invoice obstruction. + +For an inverse-image Clifford chart L=F^-1(Z), its x-projection height is +k(L)=d(L,Z), where d(L,M)=9-dim(L intersect M) is the Fourier-rank metric. +Fixing each node's source height makes every paid rank at least its original +nested rank. The 358 zero-entrance helpers have fixed residual rank. Each of +the other 50 helpers has a native-free paid wire path whose source rank sum +equals its residual rank. These paths share no paid edge occurrence. + +If one path has source ranks r_i, increases delta_i>=0, and R=sum(r_i), +concavity of H(x)=x**t (0= H(R+sum(delta_i))-H(R). +The rank triangle inequality bounds the changed helper residual by +R+sum(delta_i), so its entire additional credit is funded by that path. +Source native costs are zero, and owned-center tariffs remain fixed. +Therefore neither frozen orientation has a cheaper complete invoice, even +with arbitrary quadratic Clifford charts of the fixed projection heights. + +This verifies source incidences and the hypotheses of the written proof; +it is not a proof-kernel certificate or a new physical supplier admission. +Only the Python standard library is used. All checks survive python -O. +""" +from pathlib import Path +from collections import Counter +import argparse +import copy +import gzip +import hashlib +import json + + +SOURCE_SHA256 = 'cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd' +EXPECTED_PAID = Counter({1: 2201, 2: 412, 3: 510, 4: 127, 5: 40, 8: 8}) +EXPECTED_HELPERS = Counter({4: 28, 7: 7, 8: 47, 9: 326}) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def span(vectors): + result = {0} + for vector in vectors: + result |= {x ^ vector for x in tuple(result)} + return frozenset(result) + + +def dimension(space): + need(len(space) > 0 and not len(space) & (len(space)-1), 'subspace cardinality') + return len(space).bit_length()-1 + + +def map_vector(columns, vector): + result = 0 + for bit, column in enumerate(columns): + if vector >> bit & 1: + result ^= column + return result + + +def inverse(columns): + values = {map_vector(columns, x): x for x in range(512)} + need(len(values) == 512, 'invertible native map') + return tuple(values[1 << i] for i in range(9)) + + +def canonical_hash(value): + raw = json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + return hashlib.sha256(raw).hexdigest() + + +def source_graph(payload, direction='forward'): + """Reconstruct chronological contacts and every persistent wire incidence.""" + need(direction in ('forward', 'backward'), 'known program orientation') + program = payload['programs'][direction] + canonical = payload['canonical'] + frames = list(map(span, canonical['frames'])) + need(canonical['h'] == 9 and len(canonical['start']) == len(canonical['final']) == 632, + 'source dimensions') + need(all(dimension(s) == len(b) for s, b in zip(frames, canonical['frames'])), + 'independent canonical frame bases') + maps = {w['op']: tuple(w['G_columns']) for w in canonical['warps']} + maps.update({-op: inverse(g) for op, g in list(maps.items())}) + nodes, edges, adapter_roles = [], [], [] + paths = [[] for _ in range(632)] + + def node(label): + index = len(nodes) + nodes.append(label) + return index + + def edge(kind, start, end, role, rank, event): + index = len(edges) + edges.append({'kind': kind, 'a': start, 'b': end, 'role': role, + 'rank': rank, 'event': event}) + paths[role].append(index) + + current = [node(label) for label in canonical['start']] + entrances = current[:] + for event_index, event in enumerate(program): + kind = event[0] + if kind == 'scalar': + gate, label = event[1:] + refs = gate[1:3] if gate[0] in ('add', 'copy') else gate[1:2] + contact = node(label) + for role_kind, role in refs: + if role_kind != 'L': + continue + old = nodes[current[role]] + need(frames[old] <= frames[label], 'every source paid edge nested') + edge('paid', current[role], contact, role, + dimension(frames[label])-dimension(frames[old]), event_index) + current[role] = contact + elif kind == 'warp': + _, role_ref, op, source, target = event + need(role_ref[0] == 'L', 'persistent native occurrence') + role = role_ref[1] + left, right = node(source), node(target) + old = nodes[current[role]] + need(frames[old] <= frames[source], 'source paid pre-warp nesting') + edge('paid', current[role], left, role, + dimension(frames[source])-dimension(frames[old]), event_index) + need(frozenset(map_vector(maps[op], v) for v in frames[source]) == frames[target], + 'source native rank zero') + edge('native', left, right, role, 0, event_index) + current[role] = right + elif kind == 'adapter': + need(len(event) == 4 and event[1] in ('old_to_new', 'new_to_old') + and type(event[2]) is int and 0 <= event[2] < 224, + 'source adapters touch only main roles') + adapter_roles.append(event[2]) + else: + need(kind in ('climb', 'center', 'phase'), 'known source event') + + exits = [] + for role, label in enumerate(canonical['final']): + final = node(label) + exits.append(final) + old = nodes[current[role]] + need(frames[old] <= frames[label], 'source final nesting') + edge('paid', current[role], final, role, + dimension(frames[label])-dimension(frames[old]), len(program)) + + paid = Counter(e['rank'] for e in edges if e['kind'] == 'paid' and e['rank']) + emitted = Counter(e[5] for e in program if e[0] == 'climb') + need(paid == emitted, 'all positive source paid occurrences reconstructed') + centers = Counter(e[4] for e in program if e[0] == 'center') + need(centers == Counter({8: 8}) and paid+centers == EXPECTED_PAID, + 'complete source invoice') + need(Counter(adapter_roles) == Counter({role: 2 for role in range(224)}), + 'both source main adapter boundaries') + + nonzero_entrances, zero_entrances = [], [] + helper_dimensions, helper_ranks = Counter(), Counter() + for role in range(224, 632): + start = frames[canonical['start'][role]] + finish = frames[canonical['final'][role]] + k, l = dimension(start), dimension(finish) + need(start < finish, 'source helper strictly nested and productive') + helper_dimensions[k, l] += 1 + helper_ranks[l-k] += 1 + (nonzero_entrances if k else zero_entrances).append(role) + need(len(nonzero_entrances) == 50 and len(zero_entrances) == 358, + 'complete helper entrance partition') + need(helper_ranks == EXPECTED_HELPERS, 'source helper rank census') + return {'nodes': nodes, 'edges': edges, 'frames': frames, + 'paths': {role: paths[role] for role in nonzero_entrances}, + 'entrances': entrances, 'exits': exits, 'centers': centers, + 'paid': paid, 'helper_dimensions': helper_dimensions, + 'helper_ranks': helper_ranks, 'nonzero_entrances': nonzero_entrances, + 'zero_entrances': zero_entrances, 'adapter_roles': adapter_roles} + + +def check_paths(graph, paths): + """Check every nonzero-entrance helper's complete actual paid wire path.""" + need(sorted(paths) == graph['nonzero_entrances'], + 'every nonzero-entrance helper path covered') + all_ids = [index for ids in paths.values() for index in ids] + need(len(all_ids) == len(set(all_ids)), 'path paid edge occurrences disjoint') + result = [] + for role, ids in paths.items(): + need(ids, 'nonempty helper path') + current = graph['entrances'][role] + ranks, positive = [], [] + for index in ids: + need(type(index) is int and 0 <= index < len(graph['edges']), 'path edge range') + edge = graph['edges'][index] + need(edge['kind'] == 'paid', 'path has no native operation') + need(edge['role'] == role and edge['a'] == current, + 'continuous actual helper-wire path') + current = edge['b'] + ranks.append(edge['rank']) + if edge['rank']: + positive.append({'edge': index, 'event': edge['event'], + 'rank': edge['rank'], 'a': edge['a'], 'b': edge['b']}) + need(current == graph['exits'][role], 'complete helper entry to exit path') + start = graph['frames'][graph['nodes'][graph['entrances'][role]]] + finish = graph['frames'][graph['nodes'][graph['exits'][role]]] + k, l = dimension(start), dimension(finish) + need(0 < k < l <= 9 and start < finish, 'source helper endpoint heights') + need(sum(ranks) == l-k, 'source helper path geodesic') + result.append({'role': role, 'entrance_node': graph['entrances'][role], + 'exit_node': graph['exits'][role], 'entrance_height': k, + 'exit_height': l, 'source_helper_rank': l-k, + 'edge_occurrences': ids, 'positive_source_edges': positive, + 'path_rank_mass': sum(ranks)}) + need(len(all_ids) == 1016, 'complete selected paid path occurrence census') + return result + + +def verify(payload): + need(canonical_hash(payload) == SOURCE_SHA256, 'source payload hash') + directions = {} + for direction in ('forward', 'backward'): + graph = source_graph(payload, direction) + paths = check_paths(graph, graph['paths']) + directions[direction] = { + 'program_sha256': canonical_hash(payload['programs'][direction]), + 'nodes': len(graph['nodes']), + 'paid_edge_occurrences': sum(e['kind'] == 'paid' for e in graph['edges']), + 'native_edge_occurrences': sum(e['kind'] == 'native' for e in graph['edges']), + 'source_native_ranks_all_zero': True, + 'source_main_adapter_occurrences': len(graph['adapter_roles']), + 'source_adapters_touch_no_helper': True, + 'helper_dimension_census': {str(k)+'->'+str(l): v for (k, l), v + in sorted(graph['helper_dimensions'].items())}, + 'zero_entrance_helpers': graph['zero_entrances'], + 'rigid_zero_entrance_helper_count': len(graph['zero_entrances']), + 'paid_only_nonzero_entrance_helper_count': len(paths), + 'selected_paid_edge_occurrences': sum(len(p['edge_occurrences']) for p in paths), + 'paths_edge_occurrence_disjoint': True, + 'source_geodesic_rank_census': dict(sorted(Counter(p['source_helper_rank'] for p in paths).items())), + 'paths': paths, + 'owned_center_profile_fixed': dict(sorted(graph['centers'].items())), + 'baseline_paid_profile': dict(sorted((graph['paid']+graph['centers']).items())), + 'baseline_helper_profile': dict(sorted(graph['helper_ranks'].items()))} + return { + 'status': 'PASS_FIXED_PROJECTION_HEIGHT_CLIFFORD_OBSTRUCTION', + 'source_sha256': SOURCE_SHA256, + 'directions': directions, + 'rank_metric': 'd(L,M)=9-dim(L intersect M), L(F)=F^-1(Z)', + 'fixed_height': 'k(L)=dim(proj_x L)=d(L,Z)', + 'path_debt_inequality': 'sum(H(r_i+delta_i)-H(r_i)) >= H(sum(r_i)+sum(delta_i))-H(sum(r_i))', + 'proof_domain': 'H(x)=x^t, H(0)=0, 0