From 469a9628250252d5e07a1d31eb7894e909f7f466 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 17 Aug 2026 13:40:39 +0200 Subject: [PATCH] paper v0.15: the dichotomy named, the question aligned MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two edits. (1) The alternatives paragraph of section 1 now states the frame the site opens with, in paper register: each alternative fails on one of two sides — checking cost stays with the consumer, or it disappears because belief in a label is demanded — and the primitive studied occupies the point between. (2) The introduction's italic question said 'opaque provider verdict' where the abstract says 'label'; aligned to label, consistent with the v0.13 verdict/label separation. Gate green, 25pp, page 2 eye-checked. --- paper/README.md | 6 ++++-- paper/ltl.pdf | Bin 223811 -> 224022 bytes paper/ltl.tex | 9 ++++++--- provider/src/pacta_provider/webdocs.py | 2 +- 4 files changed, 11 insertions(+), 6 deletions(-) diff --git a/paper/README.md b/paper/README.md index 80c49fa..6585783 100644 --- a/paper/README.md +++ b/paper/README.md @@ -1,6 +1,6 @@ # Which file is current? -**`ltl.pdf` / `ltl.tex` — the current paper (v0.14, revised August 2026).** +**`ltl.pdf` / `ltl.tex` — the current paper (v0.15, revised August 2026).** The review process concluded in August 2026. v0.10 folded in the corrections queued during the freeze (the closed consistency-verifier divergence with its `sn = 0` root cause, replay-harness-integrity @@ -12,7 +12,9 @@ revision from an external-persona referee pass (house terms defined at first use, theorem statements carry their own scoping, notation collisions resolved, FIPS 205 reference added); v0.14 completes that pass after a full-document eye inspection of the published PDF (notation-table rows -for C and b, HIST chain length renamed to avoid the split-point k). The +for C and b, HIST chain length renamed to avoid the split-point k); v0.15 names the +two-sided dilemma explicitly in the introduction and aligns the +introduction's question with the abstract (label, not verdict). The version submitted for review (July 17, 2026, sha256 `7f140356…`) is preserved unchanged in this repository's git history. The live copy at serves the current revision. diff --git a/paper/ltl.pdf b/paper/ltl.pdf index 211ad89dbf8162c1f0084e9e02447befffdc44bf..c1411b0577fe2d9b2c314fbe689684a03694e89e 100644 GIT binary patch delta 17279 zcmaf)Q;eWpu&&#f_OxyHv~63{wrxxsU)#3LX?xnXZQHiazms#Z?{@OuRAr?uR#hb{ zd7st4fRM6;5XTA1lFtPO%%wE2V_Tf++D#Z~mHD>*+624*{G8+pB|#`E%UsW{<|zZE z7!4A|{sq6}fPTi|r=JVnDaZ4+&A;?UCoRM{hT(FQRnF15!B(}Vy3BJ*n4hTF4dN8r zjAb&p`s*c5dA0X#@_@vxF%aQ;RIfemUp76Wj(8kY@BnC&uu0S(z()fDy3^tevJ$g; zDnvWyBqg-OS(2w0s-u{go-WzUBc(cUFKAnJ3+W6mPr91WMeh|tMd+3TQeUEy5wDU@ zkjl+}ajO01Q$)Cv$R;A|gro1&`%-!$v5b3um`2kwMKPUo z&fP|F;+1p4K4Xy!fW9dEPzd-=c9^2h|JO-M(BixmtA*j;e@Q}Ijq85}=9kwb$FWko zNI#o;$211w+nlUPLTw9+5)wwsfT4-907f<=nlkpw<>2RiPhCBQm1<`)8I}atF*UUJxulemqQWNT?6N0(yQ)C9+D0Ph`mREZRM! zv3PTtJ8mfP97wTRO@E(bUKWDN3`ecNRR)7N!nk2eJ6Sm5+98EgnV2YbGii98PA^DU zEaeuKeWNH~pk@n8?fx{hVVAQ^kQx08ad|lKXTQx*O$n#_+xthh7`0zL|Js6XR4Vno zix1e(gc(Ma{XiO)_4; zxZ1%?AlJ*RaLv4!VAkTu_Zs*M>tAb9W3Zs=>}C(K5XCyAe`%({J|_1I8J~Njuz=u~ zyudH7L^+e0O?sK`!iIBpbDs$4CDG_DP&=CJM|WdzIeN%%Kq;oAcy81~X%y-6h9t|0FqhD3G4)w@ykRIwINZr+D0P{2WHM{FAcyq=_qW z5jV|624IgG z?#`N9%j!AXt=y{pxmU-(iGRgdYA1^AOoV23Xq+XH?x!CPX8q#Z-OftXQNXsxvAEO0 zzn?Bl9$4Kx1D_!aC%FC<+g|PH_J;8iNo)jSuK?}E`RIK-pqo@CsjZOSQeDm?8}RND0P7VID})`FlG z=^@p(th*7_7g+~6;vw5bDdLHVl#?{nVGS5G(w^^@N@8(kGllCDP3U4t?;+-NVfwQUFR9 zd|R?%!ax7OU3d77LylWxhds(&=x*9F<(%^OFL2I!y%r5>uFFDfcWhV%%F~ZCq!GGG zbUj?E@K`Y^!wiIm1JC;i)JQCu@kT+sr~F`_({fp3JsT%ul>2Jc6R%m@{v{yFyI2f= zT%z%_pBdEqs!%IU1#->C&Hdyl)(0M|7VuE^*EIX3D6J9>t|U*1V^QM`VC-+=UAIy< z@iL5KJi5fe7Fpz&sbM+PeP}L?AjUbn(Xf7aRm+?Fy&biv<~~G3TPG~$!Sf(`T+lk% z6(QMdqa;8*sI3w>VDTOoa&z--h0E+l80&%dZ;<}?$h^)t3w11mJAOXRDbG_M>pEe zaLtQ*St^~WgjcwnajPYwih(Dz)`I$Q>+8a7E?wz_qe79LAHrtfT65~Vk)bGpJmVR` zrRXi*t28)@o2qfhz-@z@RRGYvstRCeIo#>=CmW}0i64;x)@gmP=MPezU~}tsQL`St z>cNG~rvy^TtcWBgw-L$YJT@?~iyAClcL5HLW7*UW&bf4<`$Y`90;xmzUVN@fHL^TY zdcV#+)J6^(PFlF1tmXy=UNI2=JrF$z?PeI8<%&J5GWY$pzDX&zY6rRvL}BeZ`4>lT zYP-84*81gw#7(9&zhkN$%n1jUa?WXg;fz=(&wy7Y`}F>9?#*t4#y{OyfV!g!ZJaPB zF+z87WoRdJE4Xzuku#B`*|CaVlU8Q-e{}klg)8|wh$mGWrDAJ)?F8p@>` z7{){Rda7xFM+NdYHX#plb*~zD(W=TgCf`GM3##6$Xga&DnqD^FR-tfiN{k|kEqIq5 zPV#ny9A`5LTLF}q{ZN`=DR1KtIb&;LW}i4-xTs9Xj$awWmv`bd)jW}sjxh_Na(23n zv0S2pWtJ+~MB3yJL*C#MtrC%De$0p=?>18t(JPbF0b~bVF@KIyk$vzobRk}ew+tQ8 z(f4N!=739-E*vMoH127F=9i}4MvmaSdjLM9OSVu|qaqJqS zXqkUhFb6eCj-}Y|=)4^0q)bLh4{JKX%ogiaF^>G!tz%Mfmuod9wMbSn$`dg1T$rf8 zYa?NM`03<=o8R-2l5^V}vbgs+uy}YMw-orMIN@Ms>ViIJRQje8GNWu|h&QI09g&p7 z3aBosOn_83nMkshlua^YbVqb-u%6kxRm!Vh8FT=n<`o&D?;7Q{oJC+@%AijZ?Bu#w z;yNntk~jA+$TYm8IWt6o%}Vaz@YP(#=gREugBL67iuwvaX6ShT>lu@6Fz24p05R?N zzg0aAJ|#x?N$R0`>uP4)k0VvKT!&%^%^W~BJAe@dS#3Iw&z~Yh!C@aQ6}9F5#6oRl zb>c}9JnvJ&@93L6WV-~J4c;hVJ4Ic=U@x?2So{yW+f3w#Z-mw0-6wWQl4|UH!?>DH zuVM8Tw`Q&oQlbZ#PqAE)UdRaMS(}g9Ba8{R%Q0F(V*gBdV@H+E0=YT2lGB! z+{32&-vU-*L&M@7*2-V(*9_kug}}GI7qQul2*vs2K#}urpDlZ-)1-_u+IOGK?P^WX zx-lDWvBVg`iA!1y&14SLfJo~~8(&!3LU#O4q;7axR2lc{0-j!)&Y)zuOvL8qY~YKe zGHW}kLAs{y?ufkd47X^D&LB;;i}6U5_ZbPkMWpTQw?LJ&p<0D|m-YfT!IqlWDWo4= zq<%qqe9lN}zy+FZS|w)t2scNc-+;_gU;AFIoyG3hSuj7JIvfkMQ(Y&YjZ7O zf>S^Gr$V{nefGBvdQ;l5U^Gah5og0Oi^dj@?bUa%#Yj|qwgzDl018#lO+w4Uj{YjgJ= zFB)G!(9+h1P{_2|=BbEA7+Q2NevRq#`&GaP)&Z6upQ&VrUch(Uw)-eIcYV6%<2sQS zi3qeUQ5OjZm?QnpSc>E0ZT4mXeaDIWl(tS^70+t*cDcPgE2OpFD%aO6 ze+YcX4Px#d?w;(7qVCL7tagA>csS4u>_chNMG4ljQN<6&|uiS%d7o z?Xjt8&G3-))W@TJT*TEgvCu8lfx_VAMF1L1SyJ@^T-yWV!+WtN9dfT6&YYQf*$St+ zuO{)nrH)I&shupL=RXcVdS1kRcna6r74^#~_)#c-#P&c4>2ej$RXor)ND}ymM@zhD zAIfC2wTSY2zR5x#T*-yywMfl{_w=DTT!}+GK>iMU(>G=3juY1TY_V?r*q>C|Zn-<~LB7w-w4R9H~-hnR>EfFqGs+)+t-8bHR=2bDKUW%E@Y}T zFc%7*E3Ccr5uhB>mm5U$aFkRlx1yy$jD71v^fY^^mmCYxK94n&cmRKSs-!OC*iu8g@Liy|eDt-VZ1*%ifLeXi|>HYdyJz~LGcEqo!Tw#NU4qpLKF zf28cVG&!vQT-k)Tow|0ENLb!`7(m>2x3Tovt1Z93>p!WQf_Mg zLq!{X`KZEM1jUx8uMK7wHy6Aa&lje@dB{K{RDnsQU4ai$iLfn*_~C;l875W&?9$$` zF3P+(oM%-IozKdd@gXlJ<$E#>)$vb_DRr9%*H|->6tF$Cr_WMUV-twVT^U=N!D>ys z|L`da$B**bM8d^>=wLK*R?|C3I1LE>%=E|Tf-So@P_1n^-Am+nN6T=nU+5{Aiu0v= zqxjU4u!pJJHfk!5U2U$DsnYca0z{qR+#~C@A<32ol72T591P#%0>Eq*^-cD*RCPlIaTpEW|6OkG=rBFvn zU{vISgQgq`HII_?vjN)f7t`A4ogPlLUG|{`K_hu92 zC~sz*nhr68>~Es2d}#oKk8;Z8@0>1AlxWVm+c2w6vVs7yzV1A&{eZ@?N_+!_vW69?T0{{Z(wFk@y!Q*olO#IIF|qYe}ORKwxV#xu##le!}L zm5oG;;3UABk1AO zd9VB-g$pZ_Oi+67{Lp ztr{*+XSDc8g48t4A7dVuL@+?4^ zJ!&*!1ohMi;L4*zN9o_hP0Fpnvq>-&CJ%4bWTTamE)Nt2^pjiL@W&Bo1I+fWY*JF; zk$fB$@?g+-y)!hY)RTP}DnuNx`Q{bWb%tQR$bwB{-9d7n3069FITP%|ICte(GdV>n5N{B_fhAS%)s}oeQBw4ao zhLYVT@T&9We}I`u=vAr7ROT5YX7-cGF6mfmHz~)19RF0YPVTC;gssh#xDAtwO21Zc z6HT;|yk!6qCohApY9<>gT7O6^z560vyt;)_;qi$(C%*}WlHW9Xy653IDE0GNVY^ld zgQDF_BlGtQ`MZEmk&Oc??3f$>&%)rLJy$MTfXJr_`K9^9=qQmN1dojU9$X{hZ8SPm zlNRb(U4q%5!p}%@QIzKF(Oxy%>-xG+%5yiOuyO!5u1e{>tNy6rjQh!*AcHxxW@4$; zU8K=~+Fj5mnRy6s4uS7x?7>fHQl`;2BIA$a)}fKly(wJSROA-vySB~`^Ac*2zYQD! z?D?oj8RU^^@aB?`;^B;4v(@RKMcvi%auyIDc3u1&TD6Li@S|PPXwUVSn22o1>bS@K zW;v)s^}#&ROCMVG#uXTpJPtF#^=`nDXGWAvS&vJ`GmlHoJ<)bhQYI9=t?BpVmcV!) zJmIYu0(G$CNr*&_dkWICet(0#&Pm$<%*5sHv(zThI}6f7;OnV%fuMDnd7qZ{3l<^3q^;JB5hZ z$;UON#7d_|XU?Pl)ulG4eG;kz+Oe$>zv_qvxcb=?H=gqcbvMWriD@emdC^R@S}$fiYjbg5mqR z8%wr5U9iebJLPDc<8+TFc%sv~8_#K9D{z*$X>+TsaqZH{VdvnvUaPN|;fQ0{=b;^~ z!s^+pn-@mbNB`Jc(QMfR`?6{q?_s=9)u5nO@<=%*NrP-EpI79y1T|T6-lex`>4qS4 zOVQA#IHvTqvnQ@ezv{A??tKNnUox)N`%g_GuFUNd)yL$!@;@H_Zh4_gyYnj$HH2s* zn@tSOg>y2FvcwH~-?5_EM-gX-d1&4@ArY!ZFNtbE!=+Jr`l93k*zntS1dG=1B36sM z&W?1BD+pI!pV#FGcXwnmDK)y*yPwEC)q|iqr}rGo7AoCpomz=%lWt$-#zlI2utWT* zDl5wgB{!WL&1G%RG7X)Gmke7ABV9Qx_Mc~?ByJx^W|<5-VLpr`ufs{4V&NkJA~m~) zKfg=|21hp`Wn=t-M$MsW4imjesald7a8e&sSR&i67Z-$rmkH~xv~g!_lwF4a(!wsDwvhgDmwxlCBIu5wBbSpLN?E&{)3dAx;+E^kb z-1|AFg55kI7rs3D>^(>1KH@r3I-;O*o!bI)kN5T!`lDRPhk~3#>-6s?dfkW)nP zJ4uONlh!&ZmY?4DOI;VHB~vq<_EO5Kwy`^}mvz*onacW+_YF%Xc@7cTXpL5HWP73y zBD;~!lf8BZgR5lW!NL(6G_G{%K&MP)eC@1djgB55TqbWsKcq<_w{qOrlEZUo%^Zch z0bPT)rgVSlWqHSaDv~}@j_oiPUBakmiggvp_F z?h@lfuWydeK|Vs*EqCjR^sAq%$Acy9OFqZV>-HNYrWC^Ge$El~;__K|=QFSB`5@L5 zVodUN4tiQ4MZLN&u?6X!6{+g$S8?*YsxAVnjfq(bj|$im*zRJ^OqvC4iJV@4X_a`c zD#}s!e~bnFAPEp?e9q!3H=G&APQp`IF`xRM5_FK2 zI$7{kFgb`%ePE{jJBk{zKi>?N1uGdDzaAtK={rpiy&a(pqZ1;9dD^RCh&w&G#H>(sY}BC3_LIqi{CxI(0B5J|BLn)13W6kF^m@ zuk{hGdp9R_=9DzGHg$5r6PY@&!*HUJ$_=eWe=yZL^->A&VD|K_BF4)8C;^8|EWGMC z7u|0~%D(ZL2DRXwHjo+GLF>2z%b~n%L*^MJ(Ur_zq<1AUM8GK=R1~B$f}ua6&*!sP zCx>Us2b{7ePjZEi;VBZ0jv)dSu>L;&J604TGae(jAGL@j%9+i%nX!oaZ5@>p$kGSb zOD8yI0lyAF!3auBfRm7b6EayD)0rjQj2N7R)Zk9R7O+zM=~d#5^KbxlI%ou=uo*DQ z3CDD&wbpZ=Ks#ep3CMTI525nMgiTcF7)j#`v1AN@A^2CTE4%cYRCfZ6Yaxl1)!ODH zVbsQ7mJZ6)CLpeiUr~X8h8fWa78cw&PQQ;1AtV!EhDLHRn`2A^FsLR4>sG}(Vl2&} zZ?SL2{qF;`oYE1KvRFJkq~+FSZ4?X01Y@*7AVp9tN^gVgtrZNRCxlU9N-+N%pue0$ zn4*9{ncM(*VF=XV-cWmBRT^mVg1IciARgokAf;f%xTw@w8cDreqE>Vw&mnF~bl`ab zAqD_;NYa23ELsd_4BksX0w;!*Hi*trIv`ddb zx5zp08>%U^3WQEn2Uu=oiLtC;_cNt=NOwSstye|m8j_JA;VBKd8q5We7xuroY9vnT zK3I@2+)W^n}SI*&@QPqY`p;sNdr-$L%{(f zvmq8D0-b9J;T+vDGxQe(JF=feBquo}LWs#dF-SmfegRss zuo|^Vs&g6Y3$^mzIAMqiZjygs@CdShI)G`V)Jw;7C6_5IG?4ct#&*zz`NN-hfQl&A zic0j2|06ks$46IIc%V+HAH!j;OH!pMpp)ZPp8qdIyl+WDm;EW9RzH^06SW^yu@F zSdgA2vV|={!DeuW?7lx1(Es|_wexvhyu37Xd!2t*=h^zae0ypcui;op5_nr*#+$ByFd5NJX_SdtE=tkyFTvjh94KN$ny%w<~l8tgBcxv zFd9lK!Z>z&zaHjJ4Z3~C0*_Bt@4I#!%nIV@?OQC<1@KHBzDM@e>g|2rEKbv!;m_c1 z25QM+4!&0vkC&b<0uHVeG+MVknh8b*nNDA3&JC+ye_GnK`gPB*hR3ftT6h|PSk}C5 z38E{8IL!ylD2-2aZ~sGd_b;FJ);G&eFOSz}`|j=!kI(7NL!@gpzvU7*GbaFgl$d4 z6}{?d7<0jQD%#s0FVD|`zt`fy+ND?uDB!B$3G!$xsUUfS22+zS75+^1V++_oI zg78oQL`7VF9~O0lZ3r-FnnImHw^xH*&wTI>UXa9nqsNMafZgL+$s^0iwdyENqS{m{ zjuPa-RYK?35U&n%WubGQ1tAGO1sW7qN`Woq`=)aBNsknwBm@z zo1kk6zdTi^zyJy=RzC+_2NpEhy50620sA#i*31YRAkX)ixO~70<;{riDzPkUj>Ri_ zCz*mdUd9oDxbL}u{sBrgF;-!ue2ufKtZ}vx_mjCiF_d*wtl!7_jB$rrrSi(?LxjsX z4NToP9$$k(0r8aUM*TyOJDoL}Su4&V@_GnE{%v#`wMwsMTW4Dj6Lgg+TpBs$%2;KO zhG`!XNYHGf;Y#(|_-xy13uw7qp#L>xq%EP&o8tMYG|sSMRRjm(^ijrZKe9 znXf}^;!-z_7kNvYX5Frsbai%aSo5{0S1skc(14oK0m5{QvmAU$5HXE!P~Hi>-@x1j zJf!vgXG^k#f=!T#6C&uJt{B`vPa}CUeV=TAPh#yI;u6+c1jU#%mIed_ZK2)?IXsm= zJHtVlnW(*{3-?ZDUAJ*H?htM9Rbr0$(@iQ)4ZhEIiz8U!VSC&y3b5%Kt5Uz2B=Tlx z{_~K!*bVFw=0CweN#ahOnxITJTa|=*bDoLETv|hZp|NoBGnXEkg*HR~cK!2V8;9o% zWD!UBTJ3u}e?EP>ZWa{=v<;XCz95zk54yri^TayDG%^lS{>u|bubL2-np-^UpD0A1 zHi}spYg?Svkkq=$ITBFBvCM?j=cK*z?GKaL4AmG$S5%qh%3b_d#6(|OWMkqW76VFO zxBw$IobaL9D(}2hf0#)3kJ#6lFHYtI;G#|JYY+?n$=lj_vfKR2EiH+fr>YO<8ZAy@ zUl-yoY?2gG-uP&I@H&kHY4zq$h@mLS0!#`}$8y^1%jBf&y3GI{$}XZ>40cr7W+-cRqC_wh{O2YAMbF z_jHHK??oO~RE+2d5(GOa?qou&!1IEU)Nmrt`O(FBOLvTR!w}~{6}_N+c^3bC#IY;b z1NHG{g-*AxPdAQjl0OZRm_gP;{P4I6J?&8K>dth;Du=q%x|tla=^!e$*V2Z5E$=T! z-=%w>8#+_yF4-Jf?UDCZaC=mBiz%zJ?#;@r?Z}iF8;suPd&bzn)E!uQ08LOm&Calxs}y6#~#j~=cDT$rO9JYlS@6}2hz2F!tLt{ z&O!;(Lo!62wV!6@OjdpAOkIF?WK0H1u!KL?(04F^^6q0~gm8)izR zpKQa_L)@Nm%GM&#lptS3k*`oJhw*}T6E~vfMi4?d168Q_)6rx0KnAHChEQU~LD>9Y z?%hd&3oN#e=L2Z9M0KIx%I5yV@^&?-KBM z$-FEMdAhvmQCFvvv~fCr^D&gZ@!pXUU8tNRb{$NgEs@~_0GZZ91DNK0|AHBMO=rO8 zhDyD-=*hNbIqWYrPkTH2>fc?E`*snQ8s>8G^)PgIz3-^DQ9F${eog4R#}lJ+)Ea9+ zrIMVwQ1I3LHg=hRK~2H?fRVhF`DOguapg`bMi~9>VO|073-kj!&T_dTArW~Ufe7~6 zS=LN5j<~x8G)MZ@{v>Abx}6z5v3%7K0z2IdzMGdE+^#5$er9r`}*Eua5^otZKOoIu@rwcYi#+WO<= zVkjm@rdbeg&?FnAyBiZ#3-|_?i2G{gizw;FW`_o#tJ?`Yf0+fx-GhDIyiK|^PzajW z-*-+fFa&ee=1)4{Qm$@(zat0XtHuu) zw_F4mIT15&p({A2sg_bSl|A?#9o{$BIo#G;YGyo|)~i}tQn#zW9etXMedMQz&VEl$McR7q+d8M1YP107plQ&6v zExO3M{lV+@vue5DWh zN_5ozv)DyU@hi@5fG7WpaQVNR{?8<)Jv?9js;L3)!OAJ1S}L;oB{Ppn%(y%3XUOJD z>=}ymowjTp< zw(iPrs2q_xiWAfKbJ(O0JHz+jgGz{zF2>_8e>DJMA?Oaz;K*}yy7F)9;xB|@@h$s> ziSh8$m3RI*p6JuR-7De_`|o=XOd)csGiVCRA##MLpYwm}(sD5oqYr%?udw>HU|P0k zU&BL#nmf^BX4$snen)&$acLy13tW(9aNc*4`N+RD`y3F~4OX5v66*=yz@01~8c^B}EK+t> z7<(=96+i3z>(g|vc*z^|Wxs$l9Kn_C8`|+vDTI`KCb5?w`korv`sP^uPN_4BTM89; zsxX7ZaHD(&+4kIy3j*y?=Lu@D^YrxDu73XOYOT?5P0lFUYW|1jP@}!A<;}@G$#z}h z1XerjeseCF^9Z=Jg3}5-3P9!+(Ue=8vYNH-O9h4G(W6?-XitGIbu091%Ht_63|+ch zm{e7==;4M}P-HrMY)@8N;mdP$H;w7U24ju*k&g0}P5pL(|ER$9OCS15oKoSoPJ{1+5Aw zwtk?&e&2;kzIA`0sWLhLeHtm6nLqo-=s9I2v_fR!!auq_`5J2cu^G$;w}T%0L~aP( zxSsg2p9TC^R8OM;L=V(`A|Mci*m{rp%Q>_D2*yito=$KXjHlk^$ez61f=%FT}V-avTj#xRWCB3Iex%tKn7g~Sc3O9ah8i#O~(HI zVhkdXQtC{o(krj&8$-h4Ll!6%eHoYOlz~GJY5u7R=J8z(Y@u529ejmX70Uy$>5suv zHvukRRGWqlzVev0Ri<(P5<00yoo{&k_2udFi`UMpIVQMM+8X0|<} zMqdI?4!>$@2jFT?H?`)WE*2I#eOAq!wSFtxb?#ZG8~!Kd=)K6(FG-^2g}b>G|LKgq zSX&UwoN+`+UD?Y}f~vDYy4rvTYi0pim`TwgD1OB43&Tu;0hx03rXic=@TSvZ+i8NG9cfv zVJ#aiExq+)-_Mk31!~ko!z@lfAP}cxj}ejX6B^A=`M|azm!-pU>2k6pI(9i6fnsw! zEmccLD`d;!VUVAifc@$?J^*zaB(wN<15W)Q1&L6N3qMQ(s3H{h_EnTL&@S7$GN=U_ zR=!;x?L7@@4U3Wxq2Y>G!_^BhE>wgS1AKaDg-9=ZSu}t0B&n%?QS#*@oFiote-A=_ zNKx|aT2bnhe(FpnQ*MrO6S4(W*i1J*1Xy|QJa3b!YZ{STucWcv0Baj*pSxyGnJu)Ai`3diO!mQ5t3imLc!3btt z@MJjEE5QCo>Z_YZ7y|jkEI@{xBlpE|01qCA8TN-Ei#fJ@ojBe$KxYx-5G=NM0er7J zRhNA4XWG?)tq7z>9?6XOkG?D{Dj94Cz%E)Dcu)SqfY=X>nVc@gbLfG8Q{4La7gS;S z`C?gCLH#K?GWY?r*c9bOw!l2F$UHEZ5k}@iqJf`qmTEa>|MFz;7m%lE60DNBR!W60 zGNXO8$GLf~C!9G1zNf!kQ3x78{xT_mZFP0Gz8)$t%zrpWePEoP82gUGGA#|4d^w4F zCZ{ z4*jsHM%W(TgY?y4kkCDzvU;(TnZip=-FVSV5!U&cy7wU~Q?8+HQ|_*ITg=^e)3Ff2 zNydP{A5u5zCv`SQ!$?$uR`>4*A^eHcfC#AfAb1XP=C1$FPMVSwR$|YO9qc}-s7+)E z5_j+sGN5V?G>|JaDFE7CayK(1Pf(DV2rVuPMoREE^G@oIE__f)^4%~&KYkDL&NMDk zsA6i|fMV)?RZE&Y+4ukz_*sI91XJbY!FwwOSlLnK)hpjS;GZ@B$TYT$N;mJE?5cs5HYFjHL>6Y-=w* zOcBW6gqghsiq)Dw=m`YVXH_pH5c;%GloRtmll_<~tR%rq3x7~m*!+`)kR>mH5o4K` zUInPYRK~;`YUOXV)O(E>O$w8uX^LT1ElR|3ooTYNE&pbLEiic`MKkq^_o41fK!jL{ ze(c26JAB2SbLDAi?cM?DX>pOFRA?ZY<7gmce<2%BGo1E>PA&7Zi&E8IGSWC_s5sR? z35jS6)ln%@k*3CC1`rIyH}Ybd5K)L)>3}LpHq(GeSrqMnIzcSlNCKHOK^I}@SvGa| zkp;wUkXSzl~jnkYAP*6&*HFfH))`;$WX6BR8)_DuEY#tz*phVtjzgnRYyI| z(6F-L4oCU1TA5{o8-8pfbN*eX2}1hgo=1zKb`;4-b3fP;4W3VEEgx+Bq_)bm zlR@mnNBm^IvFc zYEo)#{uj@!QqvF$`(qn4zCdq-_?Prdc7l-26&14BZ!a@{kZSW3xRo0n%~eM9D+o~y zjj$c)f=IfzL0VjXup4PL+HJJ@U<^PX_tpC3)&{aCiy8#{Xd=Z%gY#JQs}@N`3GSw~ z?zyjltl7?wK_!5=*=PZgggQ7t6s?%6JX$82=wlh8<=@BUDdG1ACVPaS;Q`j&-R*iP z()ZV74RuqdCiqPOEOgS)V3%79PS4d0AsI9y^V2dOQBj>PUDE2ClyLeap)nxXjlb5k zZJA5Jg%qiZ@WYt5R*s~P=-pZ7L8aO|2)#eF@up#1vg@AE9 z$x#|ncaCVi*OyYI-wyeTSxDBlBEHJ(hFSnG!v4s>y@v)Kl4ndN@Y% zxS~#CZw_>1|DMz%j0BhXQmnrDJH5Kjak$a8*p6S(?3W1PDuOH0K-2l~h=inqJ{j(PpGPa|*^GcU<^1-pG53-pz5Vt<7$FJr7ReQqB! z6j$(WWto4qD|1#iWqUrGyR)O?yP}JTB%izL&CNpQ<1JpgiVsWCB22~%Y)$3!Gz{Ss z5U3o=@a-DVBENp6)UjD#+R1ZYb221#Op-%`nIG}Sc1%1f&Lg?P^;2lX*ilfc;^1+d zQT0a??Rqb^0@pFXm2S-`sla)-xiM~r2mW%Mn^if_%k=;ar)Nps27Kz@x+DbEG!r@w z`72bdR?s0@_S1j_dkFbG}VxjqSN2}nm*4&y?+bg8OFsXzZlDGA$30qOmVy~md%Ay{^POUS)hKrVcIJxJ&SC3KGy@wwxR+Q$->v#F?Zc}nzJz96Y9eyq& zm8wsd9v@@oypytFje_xHJ-R zP~>g%d|5%D`_=pHB^dzGMEQJt=&m`BeF+`sF0EQm@cjxMer!0fm0GtcWl1_ubK^)m zclQZ;ycEDRx$~=XUD3ibpv7%=)w`CKTPq{^b^Gxd0ra~+t`4RCnnEw#IMUv>y&nbG zm#yZ1J=IUPPX7LAUgF+rd*zxo?Tn`M$#Eos&ieRxeb|1yX2KV;%uA=eeKuh5KWM?N zg*%}~j?qW`FxvYA)y}&rdb=*kAbIE zw%_huO*7YPW=+;?nbj?7%5Q4>fojez&x?)~b>0|+b+nAsdnz5u9#pF?+XT+GNL9t! zxj>SD-nZlTJzuxmad6e4!>WN=sG;$b!XIBwaudcC4-f}-nS&wMP#(xCTr zC7Ybt3r_{@ z*Pqwd5IoxEQ#09>>IwtZD+rGkNa9^Yl!giyq{| zD9JBtZ2>>MVWa^elFzP|!ay!=KVArBM)c4=0TL7F6RKudfgb~;T0&vb@OMm|YVvXa%+Xq! zUKlFRhlc~ z>sRVP`^oDh_FunFj}wuMNGk=qK``gChIHLSd{I0&ng@~}B1e%NS~3? zbi|dxrwh7r$465gaP3Os?zs1?8wWj`KvHV0)}W z`@AjMP*cTj{q@m9Mu_qG^Xx3YCZ+^m$}{KKK5mUvy{|MP)5Euzg6j|i!sbzxCtdn=yvhYJFiC_x~c1Ief1{|g`k-~2p6lZjcF zO@EX;6?HBzqCZB~H(cLmeS43S^&QqXb_M+jJW107lTddE-;(v7f<=tkgAX zHqN2fcV1T^U0W8?>nzYG(jE0FTqWzX&^xdDnQN$XMDOqk)E!O%S?^&o>i0-z&|qAR zYv^@O=^WP?olCE?Oy}1=%tPIq6_WK{>7CI#psVghjK**1bsesU4N!L-x*NGq6N^o; ze;K{5)y+{?s%Q8RpQC=$_3QHpU*lVTCFs*U#v*)zPetB!3a$)+F}kbKx%?QPVG%yT zr}!G5;|natm-veF=yi4Fc}wGo-~A!iDq)=|VHGL~{%rwucU=~BCme#hm#%=iTMkFv z8|zNE3hM4x_qw{Xt&X~<)qQLP*23DTfBV(Zs5?E~qt?f|7=sN^_lJ$J33fu=8S3sX z4&$*6cEonr9(5n3`#0U2C1N*B!hYBb``{={#uOZgy1yERBQZ_nhrPl7*L-*s^ru-t zKgI?9c~H<_j|KhIJ?L+L*mD^t^7$9bfj!l~|5%<7c%0iTr;7{C3H-`M4Yg*Xf4Dlu zmNUe~*0Y=`F8-|LN#fdcw45a_p`7K(;u1@*m@O`8VDQYnYgjWyT;FMyr-~cc!16S4 zgG>AA;!>h5=ZH)FXnBUXv}DUO#f`pbd6u|w@xiO4zYm%bYyE6-nHj-ma(`=9ipzd) zd5*YMT`aE&+zPi1aj$&SRn56cb2z{ z`_k6(LUDgyvAj#%Um=zkiTkg;<-LKNXL+&s;SDVx59D0SOT>@Jw|q_fTAt;l;>VY< z{49{OEH4wk-6zYh#7{`Hyj=XQw=BOAzgwu~{rFb=^wMW{5D()~46MoSIc{(rnE1}d zoEASb&GK2y#|wA~uiy>5g@t$*@8d(xEaFevY-f9nPq0}0te3&-W(WQU{XZk2!uyvR RY6Bk%GBGg9-F@1&dD=K_+qP}v{;%o{?(9~r(M~c+RZ>azT4^ir zgG=y=#+#mpzKl4^WX*6;7mOuM_gIj&R-LeZTa+vlAjI7Z2GQmOL; zM(~=20ibWs+;d$wNx<{}{A-@IQ-h6C=`W_ZRULggY;{_y>pT|(MJNjcfR705na8r4 zb?=DFn?jzm$Hi}~AaQq6dOV1odG+zyV~OBlqCjoJ#;^eA9}Q3lKJ!bkT8w(R@NIna z^oa7Oi5|i5Ub3QkS~SxSbo!9P(EqBt375Eq{^$u_bU#2>1RprU^u}u$b7}boD&2ro z=X&mcMud9VI~r|fdmPVf;!SXND zcy!L#Wvd3bBCILD=Y##y?&qkAIQvTSIh=MAw$On@Y>JEMae{1v0}0z^J2V(q>lZN| zo2CMP+0izOscfK-z#(fI&^3`%fJ+rb(f!fA7$ZLkGBuZ9s`8 za)L)$#2+WAz*h6msS^Q5^3O$ng|a|HJIn4!sEY-lb^}q%XO`eyNfVV>wgyTPaF=lQ z-;$6x5)ic5sNdq>S3)ZfCND!&L_<3wxuYofS~?JU!iF-KnkaN~sCykPtczPLWL4CE zW62}I6-g>?pINxGs#s=74>`eKo{fXrAFx-`p=zszoM*^ThS!Vi&TA#7FueNv{)})U zrv?GeY4XTT(vl}kw+;&W))&S55{?KJQKOV=B64_)lZOavsm~NC`8GGHMqAgn`x(h( zyE!zkIo31H|2l}gMyjKN7>^tDS5%+e>_AmuTgU#}m~OC3&DJ5}ach?p=hw*z(0QTA z9xLe5PYaN=T(zJ1KtrsF!s!9sQscS2AAta5@iphgVA&lZxa1y$i{Xh0PVvhS6c(H z?^0j^uXno#aFlvuYQ(HOaGoE9>n2!hqjM}AAav?FQLN)(OShrjpKgw?#PA3B8Xhj{ zm2P$m>W-E^9;#8Q$5~Ns^>+m$dke+4L$U%IJY_{`Lp?z{mB$!d5iRr9$UI&_YAh#upsn^reOq5eHjmg z4Js-Ab(_byoU#Xl%U^)idZO)MU|hLOdaSa@5D=quF|bBmzhcefClEiN9B~5%+=T!P z7ixTxNm@hRY}Px9}*;i&3c)3y0uikc9JmMucaK-%0>$ z$}ggJBD8bf%M!F}Qwb*tgnhu@nBmrhb}E+e2d+oCr7NArw9owvtW~-JTiAE(@+39#S5Mdsd&LN zC&;Tl-x>H>SHgrxl}oKXch2l1k3uau&z;8Lgs5i`l)&$R1+4$w5#`P4t)^5(^_&FDI@$Z||es)X! zX5SSmB{`6;MZ~4#9x{M`7rK?)BqJ@&;VBABWaHaO3!(&+B>hM`d!*Ohj9uJpqj-;g zabQ)JS!OCI4s{=D8^cg(&H>a+XfJxXV`_&f^Lp+R_*AWeGM-!yLKl@SbAu6Lo$iW! z6l2D^fHBLrw2+${5LZJQDUI#!GVrDcnF5x72|C5zV#a976C(iRn@cp8$p^8_YjZpT z41{>Hg9nPKjmjS}aje%6WM0 zVeCYWLmEaer8N zZaMGhezjZ@74=Au=X5T77Bav-IwcTu)@&ZCzPd**yA1FE^hcs>`S@3*>>C68(OV+2 zq2k7Jnt$;1_h$qmYx!3-b=VSDX$m2AXg`CC?Lv6n5qTCmD&dcm5v(&u#fE4ut_(b+ zZ^RA{$Fjx})%uokTK<%ofm|NzaB(Jn@Gmi(z`}JueUORnN0fK32qEQ!LMFK8Olj?n z)jrZ2lmd7sCAp+v$z!knyh4-2IZRstDOoI^n(ftaEwGDWP%K#kD(*ibR)W2Vy-=;- zy07p*IYdI9+7m^dr>4FbGh|Yrne-##nHc^upY0v(Eo%`40X`kQ3;)2mzF=v_2WJT+(c>3fj*CNurd^$V4fn zn%6<7P^e{n=9p7&B3g@eNYZv@8dPz~i~2Q@4_}5goA+cQ9$ee~7%Qw29n44u_+Vf` z!U*-SG@}N8`YjXrI-tikp)$$(^{F$dX+L?WQ(XMLxmfhkmI70TNc6KTitObEBhz&q zr~*`G2BSU6RozS{`pDPD!as7e^H!T#lC`=-q~IxPWB4Q|7iSVr8*Jmy#V%ngt5~?s)Q5D<*EVv;Ofp$Ep7zaC zKX;IU)Ou<3m1~=I>NX)%+meJOkg|NTU;-o**#yghr_iRz!nsT7O5inEhAHru#hKI2 zy_4hkCJFFlQM4bV-fimxwOj1|gmLe^WECHeu+wQYr$Mz^RF!~R>B~(BUYUS2Aj+y1 zUJFo}AD1)WmB+uqk02=ays9R!&VYcp(HRS}{b^`EqA=Z5fqHG0+ZseGqJr_IT?ZU* zFOZDansbh8iR+1n139r-y+rxOP)riarSV3E%((uGMZoMwV}PU%dcGH zJ6!F?4|07-RiFP>P;OM@oX!0WHf;=Wh~3XN&%lxAE@j0 zj?0+rWDXUoYcz=DmpzcmGcF8#;o~7k zJ6ySDu5DKQ$bZ-~((7|TksbS%7)XZe!7E-CmZ;p_Po`iSN#t;@&A{C}{&JF!z*wWy z7i$R{4+MSRUmnvik?IzU)LCv| zCJu)E6II=rNP2pv?tZma&_fmSlDC75gA+q2J6&fA4Kj?z=8I(^wE+9_e^9iioQE|F zwl&?}(A6Ihm7K6x6e*0c+{m-vpo782;+#N!Jqta`_Jco_9=LY^P!}=?gx#uFd$JS_UyAI}^6;)ko*(3_& z!Ieoy`kSp&WX|q#6al8B6*RG(@~C#o^`n|Hn?2b+Fcce;4)+7;^q_(fN^zm zF*mk{@!BZG?TRPspnuhTLUhwE+7U7Z0X+rH$?eJ9H}d^FK{0ev`1(u}ODZB*USu6H zX<$`H5x@Vgnk2;Z|8JD<1#1V(kH=DVN+2hc?F zo0rd>`wK{2ehF9Po7;Jq0n@V;s-sneHN!=A@xDCRT$a?F>0az~QPGBc<%9z79sM`m zb46WUU{r?`OzFq6RNy4(Uk63XQ(Z&#JJ_>3BmlD&;5blNH%uBJ(l85Ox@hHNp zYm5TN#QNfh z;fqRgHcNI9YD5gfDz+M>HuA7S}=*ilB)qVo_V(Vv~qF%4b2jzB9Pk= z?3=MLG%Q&jD7cRhRm(p21Zdezlt8vZ;|L8iCoU_W;g~;=RRfRc>Xu@~uyg7{hV$yD zVt_({KvurFq@}r^meMgJtn?ud(3cf6OG#KI*ek3QE^Q!kmAs=$H0Iy{CTUFJ zI(%w)mhE&z4kZ5@h2N1wJP3ok#|C)1NiZ-d_@z97AlIM z`?$)iQTXX}B*uCP5`CU|)K5qT<8y|8lW~W1F8hPaG^hhz%Cx#wLYw2LClQhM@OlVO zV_B{K!98CVWwD!775>JPMdYVeEF%2!7m0lO;&y%BX8=pisJ6HgEnlE^U7@lX| z^x}$vAmsj$tCV%O0OAxO_@{;9;ti7&^)_!ea-D(<@SHj*>#C9wb9W9i9nvC;ZhuyS z)Y**w_O;8iH1H!sHEM}_^9PF{AigG5;CM8yn=~dSrQDEhK}VDM1!!uy3-xyAbCZ|A zc>nHPONqmxyF#nhpWji?_>L#_?WdZf*UT3tkdTdu z*h?#RVh^mG~+epg7lU;zF+s$*H@A{xc6u#)zv_3O$ za(UFcQzKcX0`{1@xRHBW&~4NW+656syNJc2HT-QQ>RhvT=nSlxp2V!=5lpsR)87&H zYaMg>^fBJ1uUN25Oow+oaZdQbW&e=P@yj8iuHMN4kmh65r?2)5Q<=uG3P*S=Y&s`H znn@+F!Y{OmYj+Y8P;p37{V{ZN44fLtJ!56f5hCs@0VsQMPX6kNrTjoT@VBV_iJNCP zL^zHbq@8WF3nF87cndY}@2mPh$tC#o*oKI7)(K?XC1g_ZF4C7|@Xp&6H8v0TL?{Jh z$})J~f3H{S);mig554euJ&gzS`jNLrRfg##%F-~SfxvWsbOt~}q40HBA!B^c=eSn5gGT;a(*i}wQm^G& zU?n5POHR>BCYwMq`3A%C<9bmB9E8?(@_cuS%Du)3XcCN@=J1z9Qi%GB!WLfJCe>qr zZL-HFsG>B?`F!CpK4DZsq`2u4M@_1K8EO!w0MMfDT|(ZDo^4O5-7s6`Yun%la`dBPx&+79l{Nr(@hWRftQ&)u|~6JHCr)vm}N z0oT~N9Nk4E3s>VDPRy!gnYA+7o*3~EamHrsCINMl$Vl3!Lw`I%bmpb~R8=J$9Y|7? zT#Z;+2sBf?lzJll7O$oQQHnY!3iq7Gak9@B2Co&%mNZjRky2ikl-0UW1Gf5CIL@gb zO={6b^nBE-q7G-utvys!HEfxiyMq-X0IW0&I{YX5pK>g>;JSP)^R-;XRw-0X*b0F< z9CVkSxpe&Sk!|DVe-tQc~XQNr0aSK+Z&g6RZm8Ha4q2&U6%S89wUTInB53h&u>V!*AO0BcS} zSss)zL-!#h8Tc=;?ed2NwY^fK~}7KN_;!_tjZw#?RgSUSni_Igi(|sOae~xQB2nSC*VDz#?17Wd9m*jY#!U;y`Kw(i>M47CAf9n z5+49SbGf7bhasl~vyN+mA{Y2w&1P3~#&5-I5Ph~-o#OG&I1eWaH0Biw0NKAC(!70; zjdJ=8VyC?9)L(Twg&Bpl#34O;5jY@q8d2R{?5lSr-W%QR5>2oITwMZtUA45rsX~uW z%xCI|$I$`~d0+e1Mum4SVij0qrE4!fBZmV`;L<>hoyd+XiDxo!o|8Jl5a!7yXTi8f zqe-XaVM1P<(JDyB$_$efkmb5~Jng#Z&M&ivoMy({%Z_xJDjls+9&i1Y)}(SBL4fku zk{T9=#;g3=hc4=T@k^Aie-srt9u~}xoXzp0ECWBU|D$VB1*8%U&_3kc25mve-U*2X#kVs-Ns zlC_KD{bHMWXLUndXk{k<0Ap22%FV66|0^Qr1+Swxo+p1Lp|TumPBe^#b^MK26u7Wp zvr$+?@4C3rxC$}xWKARfHjP4xT3~Xbi&LeJdr5Pdq*f-TtyaYllbX0Lj!aXbo~a^K ztom(dlMiFvno{mBF0FIV^~FRLO5I*2EB6|@Fpi#){Bk}94E$R#FpI=OXKg?bb-xq09Ajoqh?*j*`M6SDmQIv7=#H`WylsaG z#HR@%>scciu*ChSz z6Njf)q8weB-!{#v?R;x`#H<8QRdDi9pq=x}S6H^&16MO@%@*vLm5|8|C$!ahUm#Ol z1I~fBjnGWq#%j@vct&Wr=wgLfOsgDns2ZS@XaR$?Ey(tAGAlZm>OA#;$xB~ z82cgc#+l$8NmV%Nu6f^xNTB##5z#`#Xi#|S=3IjdcN~OrFY=_S&9Y>OCr3!{_pkr$ z`73OYXEy#IR)(>I2)fq79Z2aPkP+tb95uO|^%o-lQ4ycC7G-h$Q%8l^kTz@Jbs?~} z^VPN)(1UQz$l=&re>$OiE5Yb8dib{K18jK}f;=u*c0?^>hLPg~ze~4gC^4mSZPCO9 zxnQy0#W8JIE8ReH*9Q4P0VA~W^^31J@HS=Jt2OD0wBaXOf6RUrp|kT&A3?JNsWEZt zHdNwLBQGhX-#$YeTKb;Cnzw+ECv=v@9a_%>pcWIB0tF?8K2yqvajs#*_BXH|7?7)H zn|8BS7=g+M ztndVs1R3FIv)|f{D(8xaXxHu61-KC+kWRRIoykW1K$v>7On2YT31T;7!qlhSzSjs# zahuO(`VV{9RD*vK=DXY{cq;+Q#I5u3Fw8=m&cG8BK6c z?LJ;>ve(X^+QC^oT-P;q;FN5EKMA1(+@<>klSu#U!FOYoUofpjI&c2dw$`Icymf0})x6ObzjB8b48!}|}y26`CGpjrPV~)bb z27zl++^Q~R(T*E&;Al|MwUhCntgk^uVN&aN2#W7j)}GGuiTB5>b)(@OzV#CyKwCA& zo@J^t>4-}|H8r%!Pb&yF0%N5lt+1ko$@J<%6hP5(?PM+?jG25Glp3W;!HN{iZ(;8+ z^U1*2Wx4R~DdpCRtPXw-YQ@ts12dJW`^gd6qnT((6USQjH?4dK)xU^00rc+FT^crl z{M!Y8_)FPheA*50KD_lNj<#A35VM7LPVC3^zkCw0Z1P9q@MCJUx;Z!6tmJ1pF|DwL z>3Nc_?(N-h_Pgq=YPP22&i}|~$z;8YJ~3$&bEkBELC>eUZm&;Mh^1AgNF^HJ<@)Op z|L>;Sdv20E)d(TmE{e=Ts5XlU82K7gro1~s)OyuNfQFI^JkpD z-5Jj^tE1ks4V;t~9$Z^BmDXpH9be`pSPKavcxV>*v!xSE-i% zLc#(HtO>G`p+S_WV_k$S9wCV9D0clwkW3s>+jc@8AxT>*j;B3EF(@Nmg3Zw3%l*eP zN;16@=9g6-BoHr>){H|!tv z3M#8|@MnYoPIhBKy)t5!YU;b;cqs6w-WIW&OgtWc`uX55*CL5QGw&n48o!j7GX48Pn z8y&%cBcXs}f1@xyV=#8GLL|zXBS3|yRy#y1Dfr`%!_kd21wsaBafxHaN*sC1;mlzE z=m=D{jmspzBa)r9sAcv@3WeP*U>pk5_KkVBMwVMtP0VnN?C#T*z8^3yYhP3gZY_Xg z2fOc%%G1-{ZiNwWo zN$*uhevxXlEEcHj2jeF!_#Um3*heeCE<~iIA|9=|RD23j65S_@_KXFjOdKmWR3oMu z1g(NBuTM3oE{2XmAkwYXPbXHvTazvks}!R*9Ucvy?2KNaq=Y0Z{*lT0R^+)M9`UNZ%bZx!~3A(Rp9|RhZq!HE>E%O+i0fgjy9EC78G{+z& zR9xr`tU$yrsx1zi7haLD)J!~34BHJO2KQ5byqt707#fRjHKC-zJkOx2k;Fkx%2OFy z&P*C(kx@pYj1t}?gYm(hs$N9gma6^`eUd4Wr_+$CG*DoT=^UnsQ^#+F?9#MUqw+Vp z?++EAXa&ZegWV{ImI$4+L1aotpfoRa@S^!Y(+riVFnH`1h-SlUVqJ?^Q!syXyi^%_ z%M(PFRm&4-E@>fTU?#A+Vh-;Exk`Z%-?RaZiMZ|ET(1FNv*7tu zkTKxht4+tx)wgS%J|MuW>u`H_rR^Vm@3!4;ZL1@iUfqZL{pxT+%&k+g_anT)r}usO zG-LMgWj(`cm-?r%x3~ZO^J+}KMtT=#piK63n1=m8su8+QUnoOiSj^}1W&N)kLoc8j zP}7>enc&$KSkv;vuj_+xtV{PmQI^tyZrU{&Dga|^b-*Zw9}XC;AVimva4Y9qRt2w zuD9_#_x@bCDXf$%0xj_S;6^>J-&gZ*ac84yHA*l*#!Eva4`Gq6d5W!4?P zRxM|n{q$;Ed^}@Eng!A~ln$LxmsRPB82q;Qcvw&5U0D+eILtV&%V zS9Qa)4YB(2x!@R!i66|=NNzAgq#CQDdTwAZ7sMTLpWn%r>2$0}Z^1ZS)@PeB=>B+n z`{HH$Bmep}WG2pjKLI=L=xm7bzD zpDsQiIl}47#Ol*S>nJ)tq)`?Z%fDjHXEKANKjb`}oeANR+r!vsQqK#KD^#C}Nzw3h zIjauigYE!Hj+-5L11caS83~e?Rb~HFV->j(TiFQ$uSrNRve}qv59~h%2l+eZ3v@r| z*Op5^iIH8-UL?{x5kRDSU%+2EM@_3VOxSoUP>HcNxp?Qog)*diq0*dZ6ug8))E<^L z?ip3r(ohJy_s@jt8wXL8Wbl?tGqAKiZiW^q-h+wZjQILhr28zELPwm(z$>bd5^aZw z@G%;V(Avl*G|b4FQyjq4ki&%^M+qEErPW!WmD!0D5f0XF!%i z-G$+?{j*`iPLtCfuZBexUC4e`qmN#_ z;?2#v>olf`hqv9gLe!yjB4<~x$;mk>GXf>1lJ?Qvh*gm8mrYz#NcB>acQCKEonq*6U1Ns>Nq9jh_Ty|$P* ziH(mz9#Fuvpyu1lq_Gt;L^9(|=!efKoFrcEwlYkf zr#9&)@Q#0QB7pPb;w$4Ds__>3Y`GsOjl<0}Qrj+#P%r>p)@)pAi2dg~s8tIAWGV7) zE8{bb*>TT1-N2#O$uf;| z8sf-_Gj7v*6ILHjPm5s?{@)>!R;x#^Gz1J5n85^RIK|2gjUo&acDn{L`cc|Ng(5N%E@AcP`Ki}W;*_bQ$cwBpLTz=|v14(Xj0Uyy{hQ*Q}8Sr`& zz+I!vLqnjtpxD$JiYwJt~`>*K8qRKo^Hg?52Kijxc_+6 z(Hz#EA8|+F5^+)k``mVUJlI2Zzifd`+@bVCCK#YK1EopP#1{m(%YTQ=UGG>s!z2-IVV~F_)oJxA;8)`0NC{b0f z?49bH>FsYM(xx>`)CNf8DQ6C^lTOl1UA%H?8L*qOUrrSvJX;)eF}ir%2lzuCX#j5E z9nfNicsHADrUpn@EFOb&7e9{Uk-Ua(aWE6Jn=|4&U^%Ib_!C)r@pR+1*xndYh&PiIU6fjcq(p-2nw5CB{&%!+Z%V76DaU#^Gf;TO z;i&+63$Z(~ok~>?;>$2rwk&}Z&H)S+qoU8mP25&hQGk|@>$|+2+bM>r7jcjjB`DVI z`!sQ19{+|ZC_ZcLF&r-`SuKQ2j!tUqDHMBGif-0u(SmM9;!&)|aEBH0h}InrC)eg$(6L`X>r8aL3CP%#M4gc~045 z%r?2SJFQ5_>`{ZlcCx>U8vMk8Ug5LEjkF1iyh{fWb$&E0@5$AOh5l65D+P3c|QYhyeKnVN+M~nuX)C z5d=Phhrb`^l0TmpgASgazqc{N&o`al|8})%<{VlzLoDl`p%Clfd~cM0ou8MR!0Y})j9c6RC8sy8PS>gza{p;9hh(2Taj@}Ipj zTs!alwC*z{+PeZ;x&hsO?cVJM1IOLL{CfWkHGM(YUcO-FkNANC5{T@L;z)9XTJy~l zJvXOMzW;0giTl+vM!g&M9IKa`)tW#{_U8RH<6+lOO}g-s*4FcSW4uxVABu)EvkVG6 z!-sZH2ZNEK^!*!UIdu$0U z*`?qWZZN~Hdk?daKR0x z>GtzZs+!O`|01S3w2hL;!9!bPxyU`qfxfCLrX9gpU6IWrd;M_ry%{FrO2WKPG)ZgL z_9;gYNw~8V7kj-kNbV%f!W$0aQ=~L6;8)5I5>QeHDLs0Tm%1qZ4Y$Or-qkeYuYJ1X z2?+7o(v&-Qqda;~hv%t4<3%|k+vwSvU50nv7Tj0ZVPdDts0;1|2oK~S)!%xq0wEk6 zyr35ZZEi+nw^h^MTr?PO$%`b}EW>Drw>#EaH#~W#-Ofo<#9l`_Zz~oF90heqa@&PN z0gAYXH{!G=&1T#M$wDIdjH-(AIZ~pB?kX_K`FN#5K}xj>kYUM8{QL;M9=v7LEG(0K zWmH&AM+#E%tRt3Ea*hB@)Sj_|OMkB52+wFcGCd*%-c!E5QvrM@t-YujU#gaQr>fK;{W zWvwI-Ka&{^qWKTDcF2EUv*81B^u5rdZ=k#^A^$Ht=Wh_O>w=OTu|M2=Mr9Bi3d7!ZqY+nH%tC@`~H* zTth85)bfT~YTfQ)oNDKszqDDWZ$;yz@dxIV9mWE`e3-*^{fnZUG;b$D`|~pW5L>oQ z>@e>ev1yEpUL!vF4m$%uu?Xyve#ZFTnWGHP!nUbfFAB(aOnR}KeW5Qv2!rSTPu;nI zA33PX^Jv9Q)CaWkLd}z0vUPjdiv?=Lm(xF!#ZWReJQ{S-!9o!_G|VgM%rXP!-Wm+U zG!rUWXAa}`O@|wf*Uy~0>gx-Oj_+Cy>O+LG5*T+{H+7Y;AA8npveZ!~9CO#VU8tHo z)!(($8l$r?icB`(`sQ;$-<;^GAC1)#zuY)TI7icK3df!q#}A>;T2^}gA^4h`MXe2} zhs>G5Kf7ds+6v}2g?sX8rvK3Bb-(TeAVRXSv39uXvxL5n;0R=sH-{{l34ifV(0MMh z)Dr$6&mhbyIA=@3+i7VQ{+cr#nwV)snae1E@fb;~=m}V#kpNtYB5K}ef#UFJu>+%v zXy}Su71HZzv1bZMrsmZME`}7AK(_t|S;Pm$TYi%xOQ?>6SXmZZnIGep06Vqk;0#?v zq^dk99FYaoRAGq?{*ki0PdqnbC4OX=?gk%{!_YEGGrih2A59xC8*{S;Drs6$t9^dj zgbZ2;;lWi!03;m{2sS;(grY=b(Hj|`Jb9-0O5Jr+=9g^DwxRCNh$O@%q|CijgHjf@ zHoHxKEIAl?hGY#2n+j&$c+Ohk-=;^w3ut>R&o#LBS%Q z2J9Nk;$7u(YFp09tZ%#ZX+m~T1oE+5rN)&!rK40^Km@F+hWGmPUvtr|neYj8_-ssB ze@6?;fq>Sb*0k{~itgfYPj~K>5A}=+30w0lXGxEPy^wU6lQy z*IBXiHj-hkbeRg1;o<7n*F%lo<{CfVQ$Z0jgij}`3DXj{j%J4OHjr_4msW z)kyde5w{uT?q&buV^y#xYH^hKPPe2u;hmgvNQ>a|VG{Y>+fF+puVLlmRA0`ZXU0%i zyvF0}*-Dp_Zx!;^ckx5g0CAyn-y8F0DTTFF{&W6YQ0nn26UN-Z?EkZ+%u~JzAk(?W zfh7Rk|C>YgM_WGzuM63Kw*GANh*+mmrWBD0mN@;0JXF?&Fj?U^KcF|V|cz%&(SxJ zXRtcTK{Cp&tZY^H3AwDE+E;SiYQs@5`+bd(Ke{f=NQR0r^C>KNR@|)(&0*2o{(!7@QTC0CtGDAF`B6oJ&^OWQ}Sf zPz^aak@Sl`gWIw@_F2T34XH&5jZt$=kHw%awsdq7{Q})!p-gE%XyHVMu@RI5WDiMA zVhKy$Mm-!}%{a%176Qf?-7!#~8LXvIsLk3qpquOCwwXm9+qpAg4@Jlotpp@C*RsW9Eh8!V4|#V}gDJ zW3-_#c1|DDvQeS~%gKWRrqq_^KZd6?-KYS$!#d*tri7Nt#?tr=GA?iqidnGFz{vzl zd(UWQ{oX^s7@4~C$+TeVbJ9c=%Y2!ekkh4_`6H*a5$b)WOB_cExu;p8few)lDl|D2 zzAfi0fwM9!6#xjVM%IaByEFX(li-@CsE{d>jRI9kv?~IYqaA_?5kt9`HV+b7VfH1j ztud*PrYJ*K8XSn^rie=_EW;jxtRq^6MnQoeQ=U0G)z^E}9+Np??J01~6pwR9Dm*G- zCe@(*$RsG}EfCYtX&V~&V{NP*Hz04^&1Ebu98HI`JO*&uS{hK3qVlcD%~;}thCQ1a zBuMmOPQ`t|2c>|Lg5I=dj4ts)Km*+X#lZ~{gD40<;Q=zX9DvYJ6VlYyfyPJKB`Fj= zz`eu+2FKDuGh>~K1U_M=fI49jRiJvaiK+yWAl?UI#SIxii=cwEAj>neAS(kpr%4F_ z?)1WLYy*g>!R9mNWh}wi0ZUcf(}6c|CjqgM6Vo7}r~2L?S3FlDnNpQxy$_|~VJTwe zkB3GcjUMDkrsZJMdL_{&FYk%pYrU@mvH$zJ-Y5M1!sLLFG$FfPczFLTSN#2%t|wm7 zuR$}37ItQ5Cf!JUP3y1bNqWnV8)q98bC;DACo-= zMAgL)R}jwB-Go4S?$}~aG>EqQi4&+lXv99b-1E3@VIq(qjAy90NQD;qKr!eK(+zd~ zL|0JQ2i`uxJ5T!R^+@My=#5=RqqL=+Yi@ zwE@Uq9zzo=qILiWG9^itOd;g%Knj4oLu?orR&AEwcFQg+vcmY*z&h6`dgpXNI*H<6 z7K6K`9G6z1;zRzVtwKUWKE_A26=JIBI!&ECdb(WII3NmC{pNO-gs=4Eco&*FHF$Qp zOx4=^I2)@th}6(~nnWsHDlBTn2Xs}^_3%-x^&H0JmMhML_w?vFzRizM2T!`wK_1Zk zWOr{-Li$*x*Pozg7q4O-t7R`|<5#Oicz|8o$o9^(Yn6~2GE%;wp3W6_@yw5|4*|q; z$Ix{boFoS`drAY6K+inA)7LTln)P2VxcEDCMto5;9A5`}agjv)khlx6Bv&CeXjGlM zHVG#NX+P|B2*%tET%P}|A8vJICj+Pe;{W6~NWCR}a~L;EZd=*#GB*vX(wkSat|}^5 zC}NaS}i0Q9*Qr{Bmoo7>R#CbDCKPQUx@Yf%gd&3yJd_W<9zq7A8!6! z@qG&BTLZ;ZVb0kE$|}d5g{Mw#0%MZiUGC>+Edxq+P**!q9wy@aFFuKX>X$=9riG5K z$xUfjHt=%X44e(5-?_^1fO4W1w;uUUMWF??=t&ep-_Pt&L<;+y3SL;Ypa38|H4;6x zK+{<|i#`D-s9lF#Xpd}lrq@cMiyxk5=xq7Ma&3{O%NY~M+E`|CoC*%8S{=Y2OgC`n zI=N?*1%!`Ct5z-Ry}XTO*`msAox!-x+u7yo(x#?et?ETA1TiKKp*#(G6;{2v+NgC@!gjGC#IVT5s9Whjfd@# zaL|M)+|(&4JP8{t0x>v>qQ)*b(kTwl%OOl{%i60TtM)E)@pG@JGv+<#G9RG_lo>2T z3N7yrYxrU{e+h{@L!<_nmlI~GbyPQ%p9s;ltshHB`>2-`aaxZWzW`#pRcxCNLEUd< zN(5ub8{-e*X(AMafp9tLnJ?88y|o-YTj^;l{+ce6Q@yu)#DWROL8lG>b?fg| zIe}!T%zQ-LPEK=$mubml&s%~39)I8W5rE=d�up$MNB0`C`}U;$!pcm`lFG&S_-6 zQLJT@>7e@Ttm<}NK7fGm2k85s;Me;kqai`S$93D{;^Zh}zW&?x;o;!y?Y}&Me|Nux z)#3pD?_2Zla6o&F^F|ZB^(kTaC40I3c>B15rE1-+-`cd^?y7Hd@9(Ke=GM9f&Sn+i zS{mo(g?A4vn{h~V!`tKc^3U{0^~_7a&X?YGs(y?SyA=IuR=$Fl&o7EAM z6a1QH;sr*7EYc-*4f-6egCp>rJi*v{I(r`>#Fk;>*WzgXu0h?|_wjcdtq&sL>j59( z%i#9Wbda~r3ozMNAH%Q6d!t#SXeqe*88dy$navoW=(Ms4wmz|Lp_oHCMqYNg;clWy z%bR=MeTGl2DZ}eo2aRDVFcyS}tNGV`3?dXkcit9rg@2Gy+uzW8VR4EI9~WJ>c%hGK zJF|mjjRQ1GrO9H)HN|~VYP3;!1t%2}!k%raHKI+l0>JD8fB1+ofCx{|(DG$11l?1j zCmJJLb)it{0ccOdkZ7C{YG8&c7IIS-EPD@|Sbs@&r59Z>dNke?%zH)oD6`kdR%yQX zp=Ix&XXl_|=kztiPS5&J_*Z-llZ_TYlUKP_de!Ne&=~JoTB@D@n<8lN8}Qpqu$vuV zO#6DCjMmT7EQxTnZepl=$nd%I3+zYq8L+S4M{AKmrqQdfDjf8@J;v^*V`bVQ3E;+c62?xA}ynHtg43!Zewt{Xsa$Ix_z zP&|?eJxv0~{}_6t(KZaee|7?`D+Vw|l{T=Y?Vnj}MZUL(6`K!NdkxQM$M*tv@Ok6j z6hM>Q4uITWw6qzj7g)>HQ5j^+e#kt@I}_fNB2wH^YGTyu#>V|8kj>FUub#(4bKIlF zRn0A9Cm1PyVsD^WL1FYRjjNx|P~uZS6%mmB3HHO8J=DH0^K<-HD~c*nM+-1;K)ig; z^CVi8>@kIJO!9iawKp@B@EC&ig0A0V@9rO?SVPM$+=;-5?I7Q|C-<01W6K?@9rL`) z^YVnXkKM_4IO4#Hwr7^>zKzcJ;+2rtC-oEBC3xP&ipOULdA`VPjPW8|xVF>h7Da3_ z;72KL;Juj7i}jPc2{SZtOaid5UfIpZ&I>?%8W|=fvT&3Unih>WlGuOf5K7h`ewubi z{uU76_s##O6T}OJ=E6dChC&!N=E6&H0*fC~=E50`gsZn(l{wM5KSE1__N^h5t=Ci> zX2Xj(Cvgq7H-jKW6-&c!u;80EN|Kjekt@KCp1q^?FO%vQ$7M|l$N-F;2dv0FaNfQx z^VV~wmFLSL48Ukb1;BK$XbfLGsgD1bMT64(@I~voefMr@!4N-K!~>m=%p;d}^r7!y$1`pVZ0CTqs?|4_m^o(!eQJBMGs(xlFD#NrQKQaBh_|< z)kVt`P9t%+vRPuye!y{iZ~!wyf9VsgGkRU&EP2}qN5!KLHaFa6;miS_3nZMRzij#; zOxB_o#O%VQ`|Q4Vw@^J`T)aCp{rs80pr4sdQR&yhze)Tphxr5IqQ^xGj8rD4@1AQI!eZ{l%W#60irB6UoY*m9Xi=`%NS# zq|fh>_+N@IE(#rQo#aIHMLm)v5A5({|KY+~EimDaF5VJb7R?-YJo%1)gkOHvI64w* z?;87?HlM%l2V~`~!MaB{1=hTh!9MF2xN?B-76u@@A$auHRqTS~Ch*vjFvC1|6|gF3 z=27^E^yf4%NH+s>#Gy%=v~j;G0srWgFet^ zlApEDa#z2nxRO-zL0-;Z@@xU&7T)l^meSCn=@DV=7C-@YLIFDXe zSDqI%p7^@|#cfY#V)tzls z)IF{4V{2edtc8ENUmbzE)6+d_L#&JSu@UP2un9K9E~q<0-QBgpw%8s!V>m{j?xS@7 zrhBtU?2f&#FZRY5Ou|?kg#A(XSBW?rhlsp-82Eq9x4#E`T^R7qn1DZI2mJA?fIm$O z_)CaAm(e0`gDm^^RDUrvYaU{F46Ktaq-3dByj`dEoX^KC~JAL zxWomPr-(~>ZF#D=Q7M6|B!3DxHp%*F;!-yUn)LbB$e9GsT@RKJ!X{erb7@xT5uz*Z6bsjF>I%*MBXq7x#9YfpSuXPD z$(9$1FY;&0&&3xNWqCWk5MOffv)hTgaS!^}WOq3|unwgBV`C19FE!8d5j=(`@D!fG zi+CBY;&r@h(jFYUUW?JnNOC*m9TA#mM{4xaZv@v_Mrm+fi;9||xqG72RnMNdWw DZip`@ diff --git a/paper/ltl.tex b/paper/ltl.tex index 93aca56..3ba108f 100755 --- a/paper/ltl.tex +++ b/paper/ltl.tex @@ -48,7 +48,7 @@ showstringspaces=false,breaklines=true,xleftmargin=.5em,xrightmargin=.5em} \large A Transparency Model and the Lean Transparency Log} \author{Olaf Horvath\\ \small Olaf.Horvath@zkdefi.org \quad ORCID 0009-0004-8008-5805} -\date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.14}} +\date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.15}} \begin{document} \maketitle @@ -112,7 +112,7 @@ This creates a problem that is logically downstream of proof construction: \begin{quote} \emph{How can a consumer that cannot execute the prover obtain precise, accountable evidence about a proof replay, without collapsing the result into -an opaque provider verdict?} +an opaque provider label?} \end{quote} A detached signature on the word ``verified'' authenticates an issuer but does @@ -123,7 +123,10 @@ portability objective. Committees distribute trust but do not themselves fix the semantics of the attested result. Succinct proofs of verifier execution would provide validity rather than mere accountability, but require a circuit or verified-VM representation of the prover and are not yet the deployment -assumption of the artifacts studied here. +assumption of the artifacts studied here. Each alternative thus fails on +one of two sides: the cost of checking stays with the consumer, or it +disappears because belief in a label is demanded. The primitive studied +here occupies the point between. We therefore study a narrower primitive: \emph{accountable delegation of deterministic proof replay}. The operator still observes the replay. The diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index f308402..306578f 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -397,7 +397,7 @@ our roadmap. (The full walk-through is lecture 11 of the Jupyter c

The paper

Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log -(PDF, 25 pages, v0.14 — revised August 2026; the version is printed on the +(PDF, 25 pages, v0.15 — revised August 2026; the version is printed on the title page) — the trust decomposition (expensive verification produces an observation; transparency makes the observation accountable; consumer-local policy decides acceptance), collision-extracting soundness for inclusion and consistency, scheme-level