From bd9f7961105d8aa67ce4e83e1db09df7052aebba Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 2 Jul 2024 11:36:36 -0400 Subject: [PATCH] chore: bump to v4.9 --- .lake/lakefile.olean | Bin 81016 -> 0 bytes .lake/lakefile.olean.lock | 0 .lake/lakefile.olean.trace | 4 ---- HepLean/AnomalyCancellation/MSSMNu/Basic.lean | 1 - .../MSSMNu/OrthogY3B3/PlaneWithY3B3.lean | 3 --- .../SM/NoGrav/One/LinearParameterization.lean | 3 --- HepLean/SpaceTime/MinkowskiMetric.lean | 1 - README.md | 2 +- lake-manifest.json | 18 +++++++++--------- lakefile.toml | 3 ++- lean-toolchain | 2 +- 11 files changed, 13 insertions(+), 24 deletions(-) delete mode 100644 .lake/lakefile.olean delete mode 100644 .lake/lakefile.olean.lock delete mode 100644 .lake/lakefile.olean.trace diff --git a/.lake/lakefile.olean b/.lake/lakefile.olean deleted file mode 100644 index ceaa1e7bf690817dc9918c589fa305d43cb8c4c5..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 81016 zcmbq+30zcF8~3mbj+#2|V{W6p7N*&_q+@ALsX1CEYAR{vAfkgJOe}`Bky_DaWNNe- z?WkF#mAt(zq%ByPWE)l{rX`sfl^V8w_qpf)AI@Ar{l4$|`}uIsvp?rK%RT4ZI~i#y zN$F9ularI@%o;K*~Az zX>POmhh1YrDT%V#j@#uA<06bzx3;nAsoD6`=C(yg8MNl*gPg)Sr)?_#y4&ee=rSY) zQLd=e|0j}vS(PRG{&Hvb*pSRoL3&A>oNxigc~GO|);&m0200FjpnIk|v2 z$6`~?{BB(n!Jo*!naNq%Npn*M2punxR}4AjfbK4nPCNMIzm-CBLV2O2xx$XKDKpCZ+p|#hXpV4jMOnNLi$aA`+GoO0Fmd1oFL%Q-_O~9p5qVs3xIi$2;*NV`Ls85whCnq;ON>aoSDI6Qv-9rw*$ zxaC*sA)fh}Km5F^nQ#3%mv}$;7{4B841e__=LPo=&-|tz`7LL6=yQ10>%`|<`B&Wf z?CLKTh4Y{BBDBVBs0hNP*LOMOwi+WFaMo;ABmkw?1;DL33cl&E_0@*!_c&deWHRZg5neWfU8 zyq~@NXi`q#x_yEdeYBU5^}Zk}JD8R_E3C($HLqI8o0jrf$qm;mTPua)mpe}R!*h)-AqWpfq)%^Q$#nIcT z&x3O6o40Lc>oupbX08*#4Z%BKbwkw0YR|NY6pnICpOAox?sAFa8X`AB<9AUEa8FIJ5D zY4#1&S7p%`+WGuViT@n76VLjlKM8~X82m!hl^4(+_8Ww3N8$cM8wqs(ea%&z{{7|W zKCTs=hErb%<VJn2sX*~S{P4%IsUA2{ZN!KH11pSvwvnhKgepe zG4S}ly~GDB@)y2dxa{p;Dqk18#Dn8AA;)PoKU3MR=T#Bpb^Pdwr0r`Td7OG^C+%3i zC_j7r{7?TTzS?5P@B21XJv!y+e&QKt@^2q}`;7@hBDDC&twTzyd%U z#wXUl8}|i(6@WE>9`xTKz$!pD`YRt`9-tfcm*d`n_Ui}C2W0)0Qee4v%@p~CNw8T#{JBUS@VQOE@^)Tt$BsosyrKX;fD2< z-JUl4GXo!6h;q_BG`;3Guo(O?Hs%ZQrJxrYqpWc|a_gqVx*fIPZ+h#lsQJ~~&DEL{ z$q6rd82WTMzIMu=OWvA%(+?vno~At<*9hYTVO*0gzC2@giuzmR1i_yVc-zfy?MOOz z{e?ntB72PG&N)hovZn<66@U|;|K_QZsqyT;V{1`v$TY7BeRIsQNNz+ApOXkVKF>@~ z$;r-4N>g0wf8Bp?d*%Q74-z&#^6Yw3yn&AmqMZ5;y??NrG7P-k1$;i>W0x=cA87?& zY{8!!bHE)90b(!bQ-qvXjYI}2GyCkAyC6P1?~Q?MLh4#D zpH{0lyE-U;y?}v{?>+VLiwpY*mG~V%IemHH@H@LH!Nj8-6TkWHL7g?cJrDdvfY*+G zdmd?pKOg-d%g(-Ve0QC{41869>+a3pLSJOvn0$YHa-^NjsW>IxwvNg#H(g0I9 zp8(kPpR4T6$A86nb8IfkY46(1+wWG~rX8_dpCf+y&z0uf1a{gB!CwmaQQy=6X-{P5 zp1YHZn-4JW&@D}l z#AKZ<6eqGPJ1KK+N_L%`5cmrKmyPIgc~$!nzX*loeJRRm|D>P)?y9&=yuA|sRD!Nz z>J7HKypN8u=8N!39#$i-YAy0zrz^jxL!jiLM=O^+TXS7f&d8Lq337FC4wf$vjQ@Q~k>*%cfquss- z-wBTg5^p|t6Ce9j<sk0De?o|_7kreThOBsK^%oDlPhhBfkHEdL>Ueucn;ZQ?w&v&gDsHrlKc`dc0j#oGJ$YGWp4`T3=2( z0w|}RE{|RMNu3?hu{D@a6JJoZ=zxZ|=YhWnaD3{@k4P)yiPaC`m3nZ2zRaS(3is3@ zQ0k#pD>vjH=eSSEx*vUQ9jEwDTfE(r|M&Jvscm}f%{@Y8jIUw*ORZm+E(y%?JkY<< z>i%cgF^NBgD5qSZm--B#yae#yW7*G{!i@h6Ju#H`Os9l{EI0V<<)E(yoVYyiGs-q# zqw}Wm8MAZJQbr|ZCsCSdM-=Bx?(WLpn>XD2*I#cfzFMfn&IFWGN2~a$_fmrBO+ zcC7R%N{K7=6hPhs!Amd9O6>lGP>39J!O-}d@HEA0%NU&-%E-*VBq^DriL$#Caw-95 zH+yTz=|3*uzJ)QNQU1{Gcm7I#5F%|7#}N49LDyl&*Skn7cpLD3;0N5db|iB~>}5Yq z$o~4`oYb`0<1%JZmq6YBe8`*kck7$-e|pq>E|EN;ZbI2E}`RExD{sT|{`@a9fgb4rt z6Y2lnVawY@_zyh&|G4_Hqq_gYU<{%80BMxf`ENKale@YOb^Lr|igrP zrQ*;htzCe9vg9q--6&t_jj@%X{kXyB0~EY5o<=8X_tK8JZbv!#yx5>O{?%Q^c-FKS z{Fg5twu~6Dm-B&A;BR^4>0abDV59S=i!w8l7D139C)|J5K+eQ|Z$&=~+p0EbZTQriz~z@a4@{M4$Hfgh`@O@R$N?-wN{)MGBx8#ja; zXJy^%vea24Gt%dz;<4GZ+jSQF2ON3(ra@^zPo2R{}W|fM2b@@WR}AIpODd@)L4iGBYcb zlB}H%vc)U^+<=EFZ0$RbD&xLztRLlujpntc#jVTnr`Qq8b4tX&bnrZL&LlJj-W~*h zK48Jbl`}~z_+pfEJ!VSO?xWF8r9tH9Vttl8+a^Btm8Rcb4*qJubs3x9YiK=(&jA%^ z7mnV_@9FRMTF2a_T0QZz3Q0CvcTDkNW#j#2+`Skw6C~I^c zIU$stnvt%g8*vG@^Ge8{dGN*8V!oYW?sJG7<{=?{G`i<-3l}-Ivr+$mt1^4;zjW)p zOGT5!-;Z+IyRu;PN@WG=7kI93y4DuYAg$QJydz{gnVgZ6nG8$B4$g~ioxN zHI&cHn|%0L2|jz9W8rZeE|~K)Yu*V?^0^fGQwx6D?dhxHL>U4lpZ!|7mhgKVk@fZAt$WssY`G+!<>0FZ-0|w2aL8S;pDl6wM+-U%0(F`zg5-c7HHC z=k3@Bg-z`7q1^D*ytaL}C=-7QK8kqm4?Owjs8^q{{kTqOgg?*1pYv|FdE_@_Hu^k* z;SOQU8kHK>YRV1UT?YAX$C^iWwodLvy|os-lja`e^hoTo7Xj}&SNT1-=-aV|J?15L zvA-l_e={?8=0K2%oN)h}2sw|8p4)%w^Jk408u6d=CO#MK^*r|!`9%*K0U_sMG7r)F zddREu8~S>5ed~b#%A03VUk%C)+2-~B_D#RxPqD{d1iaIu{C?og(I1jl?BP6tkp1<7 z`J)$vvQ-GhZ~B!0Ilt~&d|UD22Tk+E?_8AA@5C7kpU~|n1fF&roLwF;UcUY+UQ>VQ zcpqsEemngj{*wbYzNh2!z(+s6oIcfiihk(NIblD_AaB$glQzcgJ8v`n;P}mWKd|we z9hx7pTrZ|=tzADb)okL2V}SB69&rDgn>?hIIC1=^{LSCIc(x|r9<=Z;>(G58`3-oY z`Wm9i3Hw$yNyzq@nPTjaV~0TGRDiz*@Zx_e?#aI=>IVAl8WidGU*EXQ zwL;+SdEoPcuH|nJJz?lKFWFaRyUYCbz6Xqf)VvJ6_C(O<0zPv|o1AFig^%;KIm7zj zVmKV;D*$~7;K){g6~<_C%Psgn2K9U-R>N0Y@J)svZerK)j`NhiwCn!ATOEqi@bSP? z|Gd}kncqai`z`n{a(}zsq2YrT{7rA{|FE`!Oo9P>}!Vm zL~``UL$m(DUjw*&!N3l~E_~s03Allebq$WJ|0z$-531TQ@%DW1c|rHo2M6ag)BH_D zIp?PjzH{h-=9<6E4??Yf_G)^ERpB>em$de}Y**-n$VjzyylsO$4X?!!;UtZen<73Kgb z`f@G$VteG6dsiaHz}w@2F9e*K^SINn!@R^E>L+A-52l1>8Z8}9fQnw`rInB)C9=Nc z@G5^Ft&E900!j4IUm;YNdueZ%ye(;~`!si`* zh!e+|qqBW49_e3E0zYEQ!AILhy!}!c#M>lZw26>({YYd$$rH!<${#6~Jn`VZ^t)R> zCaJ`w8v1;|Z`pp%8p;%X^p{Zgn-gT+?_9`<>hR&+uWgzh5M82&dBXWq@ya&}s7LV3 z6XN}CllKyTGCMed((SNap!{$D(cCu{r@nKm*dgN*+gbM>Z>_Q=NU5?fyzdXbC0Qdo zMrrr}%3auBo;rEmdC|b1%sx(hbo+`RZ{^hKi+kklG{P#_NPC{B5~#Owj21Llg13C4#9g-&i;M%png|zJ?>H zY>BX=qp~yc-lDgnoXS$s!+a*BjpxuA1B%~OkT1n%|2JI8Taj@ISxtRqpmPEL-Iqs3 zpQ>N%0Cm3-AgA?D9|b+Trp^)l;urPse9lex^j&j`dIoqzh;iw9N}*>^i#LyYI@}h{ z3yuqfoDcRh4jlEHyV#T?@v&W~;voeRpLpE2Xuql4Br^Wf?e+qn6#GVd+Aa2QeS-be zM+2{lp7+2CzsNA~u_5q9LFlpTyQkn!vz_q})8XnL^ofAYtA2hlR^#J(OWuM39c_7ad?C;m03IE?^?!Eoi66x%XFoFh?Xxb4 z)8ux7J*!@yvdvaeC$}7Y)qra@U;k4RO|H$S{3QN|^G5A=XmYt;_502R?QEesxo+_J z055&2)wHJIGwSxZ6ZR0&Z_Go@#~Uu%NZxSWD;M&b%_v;5u=$)eB1ZD280E|x&*+{^ z6~WsRfiDO2H@l;ydV5>V6HP&eEJD^F?2*SqV_Sz7DdTm!92coLP5FGnxEpM@)zU5> z%4yfQo$bxJ1@QK2*b@L)TG-(iV6* zw_JsBg7c*W^ouprJ1(n9yDH@m{};Yo3tu7bougEIK3@LFl=cz6$VNmA`pq*M$0f6<8PZVZA38avYZ^{}S&Rwy&G7 zK3_G~A^qUbryTH=UEO(GcTasjH~0d8MS!{B>%T8)sM}qiFAwY19mkP+^K5NGIbNr+gd=2n?UY)b+*3&rw7Qd|e#a{8N z1bj|^q+cG~TmABD<>FT$E|Smc7vIySt$EFFoI#mlH{Sy(hTJ}(S?`k8z{e)Gij;q( z_u=1k{&MhD1LoxRxs`s4e8*VD&wlmD`1gK|LB5>meUEtXjX(3RPF#bcUWupGZ^4=S zim<~Ee)^J!d&&?f^YcQjT;f@Df_Mr&zds}VGM}#ne}3ERUX(Jq#6GJWDHr=HLGKtB z8CN&%g^ri#^J?W%AFd9Od__$=KR|l1zszEPuEsC&;-eJ5@QD4Tz)yU0d`6v|Xgk-d z%7Nc_Lv|0=s}a)^?JEq>CWY?s3BMUQQCoN>!Cp*fM9tc=L_7P!yihny={#t+&3 z>w%FXN8%DfIrm8xE*WgDK>}|t0G{LCqXj>%U~Zhqjs;1n;Wa;rUj^idT(kahpYi#P z*GidOlJ_MjcU-3YUeNE}9j6$-K}w1#CmcT?xKPgZ{;QL2dpz2$BnaLMJo}5k-k<$MOdUR!?;rBq z=F>A*nP*Exg7D{ppW|`o!i0`Qjr&i}mqW!J?GGxv5+WY5gt zqPe0=F0rQ){I!7VyM5Gcn4{KIYv7~Z6I47d?WuUKjf$D^^c@fXE_WVVOq>sR)+5_( z&DhUxHSCDE40-lK#5n-I155lbvyKgX_`Ou-&Bht6Gbu#)ODy^lmmc_odIVnqJmm+E zFTINLB`#bCB5VTT<`G>)*pL%`|H_%5{GZ~yVb7}X{N`hi*y%+%b&qM19MP{N0?&Aq zF6{RtX-{OwQ-}qh# z<$y1?3VgPS%D(}tyju|pk!yFMya4fhCUgFb7!Vk;8eMk`cjmBYaJfqjb}A1~-_lT{qXEEyYQUnKfGD5t)U#x8L+fj+~BM%!0fa)NwuFB}*88-lzk zLq<%yZEAOuz|a$0h;q`!2U>(vOZU45`C0YpL;cz33ceKlm4IJAdF~wgEBFMI*8;}h zd%<}Q_#t@Cx4Dk-=H18lMFmu(1n<2<#fSUl>r2jgJ6gjh0?#-t$t`~~26&lI^SLq? z?a)PefHV3fj%=Es^znb;<8vkJll~Wi?}FWHu59Kbhl0Wv#5^D$FcJN51^Bv5`fM}z zr^zjRe6F-UZ#$+a|F3Ot8-JRc9CiBQF|Xo!f*X2$;G6aH)$>~*-sBd2d>&={tirrD z7ks~E{d+Ul4R;eEjK9K`H-$qSlk_yF*1 z2fM}%TiG0Vqb?dfS1?oNx0$K@G=@zsBOXyar%(jBwY`73JCJt?P;SUJujW_n zdkTNrL?8PyLiPzWQx}AIfLZk94pDJ&CMx)Co0(7DH%Y6O=eVf%kaOqy+5nj(I2Y%!ogDNOT z{H1?{>?1=tSwU(Le|cWfcBS&y|6py8j~4oS2#xp~k8(q%d9B=i>ErlQ@OD4&Tz7FT zIr|OL3O)!t^Wesv*$LXdnLQtP=3$out!`pFG2}GrM^@cy(PBr~k8;TC`&6%zKW^Ug zo!BaV)S#TU{hjz$#QKqQy7HfXJYBHoZ_uV&|_(yGz+G8Tn-6 zytm(k5mH_PfDa6l;Pfyk$X33#b36k3gFxCYIZK$f#8{c++X~1$%JLm zc}jxd9akxTS#JlL9oZHGyx7h9BGl_`5DYQogzL=@dD~K_ZFu&BVdk^1fsb`IReD&z zA64d{r6D?N`c7dKB4z4CFk9B(|u>}T7CfhQ5E3l^T1$lb&EYc zzc=@GM1KwN)ct-e0jIXUDZg$N4V5hB2-H2VztCc?k89i9piwP zeD7>i*To~tuCrCCzs0X=@Hwtgat}J3ottQQH_DmMA03UUacFoS@N9?8b3U2ZRKo{= zXI{ofS37B2=&2vMG5Znz}NNgFRPnZ*di|BD?%K}7Z1K7@ICz1vg4VK1`#iN>lzhIAmIuE3uRi#pGmjh!3Lp1*$QPo1@C{!2z>Lz-FshqPklblY2fg&iZ_u z$CHoyCO+`J@W!1Fxgyz&{@qxIv&^@JMCS26%wu!G&;F|f_qr$uT&F>qMPxo8sYq5_f{4&0}la(JMRwYL4GjM$M z0KewS_rmYv8M2K@gt`bhCZ2Hp`W$09dqIxzOB##L#dp~U_0wKd6#IhENBhcfUw&0; z52&Z{iny(!VM9zl5Lb0UTeBUvcTs zD4()G@P6=f9Pqo>Bu8ubphf;YfBkSM26*YWtnIqIy|O1Ce0RP6)XO~2ue8dyGwYtu zS+DV+F9!TzZo#j1H#rm(zQ)>h75IL->a9_6r_iqbh^s3_**kIl;MPqd)tT+unukIn z`E3J#0{B^H`MB3bNj?;5<>vEw6Q!4YjDzr*{fPxH<)XI=avWHfAir&nk|%V$M6XLL zH~SOEiS_b3qG7p)FwvU`IXquUe6A*6*IS^Ki(Y=0lzh6sMjnRu*NFdQ*ezoyPx7<| z^7wo+f69Z4NGtsOo<7UYT34N_^E>A%zde9)1zXJTXL z&ezJ#cw6Spy5EMZM%Samofza+YjUN(a|V?^UlpVdqzz_&Y|$q;@uM94Zt&3$FYYNr zp!kuXm5U$zjx70fKSZw;FLFe00p#%chWsU(e4&*~^p4(`9+u5l?OdVfRtaR>DTS5 z)XL3#Y8L5_ZkJjA7CiO3<|#gogVgIqIduv&>t8E3>)#?**K4-lrjd4?^XIQWQKrO; z<8TS&_CL0HryehUhnRK=ubDrfuK*;z2KUqxpo!vpmJ>&Alf9iHy<%?di+YkDDK=RnK#O^Y!T;j>+Ve&PNKC($sE5G=i zX5wvWb$%OV$9Z0skc)4|`&Bu~*<+2b9F3~?;Sob`cpbn8d4ES0lwEpF2lI%$F|3C1 zVvCV)wp`E^YWgJ)i*X;e&!9KtH!DNAcaXAo-BlajCym6L?w=f1X6gGZVLM$5l%Aun?cMvd{m*4$x5(lC7a_;~?2NiE?npd*;12-q9sIiQc>i}z zT?RfjALTq3(k*s&_$fyGDF&YJLw|bZ4_DJ)v4i##8X0R|>8V`RHRBexqZ;z2ufFZt z`_A0(rx1%B&UED`?MUu&%hgJfiMM-zryW1F>2^Ks5If5uHvx3{rI}AN&kcOI-a^2C z|Iw<`XshtoqP_}%@Al%Z>*$l<83*nww_g_>@f|waNBnb#%5K)}tAN}Zzz;t=Yj8vM zIWtro4j#UKp>AIZ_&mTzJJ&wR91{ByP)__cGrsS{H8a77Ech+?KTlxJ2)+RL0_aI@ z*7qjnmf%Y){B5sacPsZ|1z%yokGyZg_uNw!e2oRa>4>8h_nr-WxPG{wF{aObpXl*( zhE!ZUfE`Q!_?I1>&d>9n8~)n1Sc|Vc0em6A|9%knZVM!s*vECY0^rx}?mCP6U4|Wv zekW#ud{nHz5@g5;?>kpO&bVL4-v4ODAG?LZz{l32oW4~#Zt4Rw1aEg;tNi5t#D6m5 zDo88%67YLL_vtOo?r#MF20k1|o(Ik!vGzhe4vFB)1)Tl-&vW>=A@Z5$+y~tMQp_oR zPc}ItJ-mi&$O*UiO6Zxj?t(oNmfdw7<6z5-Z14HoAB`Aq-N4h1gZFL=pHmV$eZVsg z?H)hBrS7K(c})J@6@RzZ;}`&c9$?D#dyDk;Rtmd|fFC;f%RO3u5RP*h@VzpB{Z?;} zh2XCO{)2ulTjE_4@#fRr9g72qCJWu$5r+@EX?`li` z4A|&6GsgJtmzHngb?rRJ`({io+E@ZTfBhnBVUb0+GW$nUH-r_p$U3(26`S*p;>7I_9fHXr5m z#WQlk3xbnN{PH25#h{y-n;!nYtl-O0&baTWN_ba~E9<2ibRU)u%GT;N99PG6%HKJ$ zuTR(V(q4mj#sgn4f6|~1$~-e3^q-JpVpcFCCvCR+C@;vxpYXgg2zf5Q`E{x|<54{5o_Ci->+yA?euxj;dgqnIi$9DtA#thMDKtau2*)KKdRj$4aBO(j zvVVj~{3t;=&+YB}-$?TeD)9CS;AzLj^ZQ*-UBb`rNRxm6icjyS0TKu2BISSl00lQW zyPj{@Z(f4;0MB*OJ2THIGHMudTkBjPzn6D)yv!QT%6d+K828dn0&W&R7!H{?4(&~ zDWk8|KTj`qh3m()SjDINs$RugC;O+-?gW(6?jz5wq-f!{hk$4Nntnf{NfahNf-eA` zeyy$qQk#O8e3zr@A9Ol8CKIi=k>}j zwu3ukrmfWaZ@UM0elPfo)UrK#e#OTse)_*@%Z*2=Kpv)$d&w8hoe0@48Ru;V3=$&al6(ovxk>ryexqCO@Av%uk>F1xXUf?0Y_AX* zmoCQ-IR*dt{7sVIG5cr(9~(kB^*z!i%baTqzY+H)jC%p-xXw0iN!&B!5n8!~KHfrC zg8TISJ-4vkDr&JW#>U?xqpT{>3yo3M==>irgebDQ74 zDB7bm2)@!HfA_bW-i`rY_P?zA)1{!V1^lmn$5*j#T3jc$5O`Of@_Y9A*L-6Koy3px zNkZnG`FuVgEGPVY9)g^j;>tze&27C|C?tM`C^ux9*E;v$GW==AuM~L3r{m+xpCYXR z8?__F{CNZ=N!m*-x;$5BA$aQLFWO!=uOXWtdEBF6aAoLJTExwP;Nu< zOn}@V=!^e3urtoB?9=-pwud6neSh9Lf3Uw))Mk5#v$lsa(69J-+E<+OlV18AYkLr! z^gB+}a}D?zTlW$bAIcCYarA2C<~o0KMMpliW1%XG`Y*2=~1niJPo zc;Ch4Rras{Pu>CACH2MUZuV#2MUVSM@6UqE6d#{k@9{*vtk3KCeHVUjwZ{kRAE6H- zzZm>Hce(GGrOxP(@<{OI!1H~Dk(b@>jnVMc!1Mg$)lYx(d~9AFzvEVAAJ5;N_40~i z_JTTmJn*#tx>4!9<21bA!hiI&GuAiJ@Iedyu@+H_92!0!c%Bb@Vny=lO*MQm@ch2X zl!YIsH`DOt!1FsJi;DkT-CV<01JCb$TzQkT;xrBKxJ~)b?{7G21An*B@bSRAMk=~H zVmgg(sp0*=Gro^?{p)<5Ym@p3TJW6`Lrt6-f4&8u@zEo5TWk1Y;F(_?US2t(jfO7= zp7k@}NWq}Cz)Szk^K@*F{O(0H_#VCLj#cfD531JH`4XO|BOkwe;kaGJ;q0*)o!W=U zp`hrqo~Pq?FMQzJ^ZKsx4uSf7*7J1y?nN&626fz%*fF6#pY=RlKJvW;d|#g1`UaP; zKA-j6jURl~;CsB|wX-^T>hm>rp3a@G;xgx#?l+w7uFu!lxtm1r_3kh@qqDO% z^K=E^n~;}yQ!PH;bZO<%U-EZr$;bQzB`Yo&Blw^H%x7D|RP>z7R01ANSNDQ0%VI%EfN}&Tg2m zZJobjH-9Ib__q_&%sms4Cw8-+_uQ%Yz8v&c#Qs|X%GnOP4cr}`Cy8HH{UX<#Z-6fZ zNc{!47dl?zSFu(ue(`sM$*0$c=(XZSmgud99QM29cidGM7hSJgD;K@|onrD?^;+@N z8-N^+r{vGm-GzFNrtaoPg+;|J~eLSoo- zqUXnf4L$ey?pAR-!+Bo!ZExIu$*IUO4+R*6x;^=j^J){ zJ$cZx*U@)h^DT!~o{GH#g~+&czsn&fx=ov^NA6F#26($~sPcpFOEsIcC;C+FZD_r~ zvs}p=`oeoJwYg*QKIjR*FU4~N-S4>Zpy1?^xaES6`(}$?`1BzoUgjnELf|>x`xo5S zT%RwN0?+5);INWBKHnO0PL#KU&a2Z?m;aFW#8WNrTfH~wu#kux#)gnKCP9V(J?_4H zRXl!ANM1Cq#|P$`n&5*d=l2x`w0h#=_3al?PYues&v--0tE25-RhxQ*-&vsS=l2l&u|vX z;E(nI&wY-kUYT{-Lw62I5xlI&BmmEP<$mPE4d3P(eneb`K6?W8(^$_xt$cJ@6vlsf z{2gp-_nv<3gzQdxIMK-fIoy&7FAH)E?grcZ)2M!?j96K0DU^`e$Ul zd+$?mdwBPr;Q1{+TqAM}|6&6ur|*N#>Z-qQ7k(d)?PNjz*x|w}m&B(C{EX+O9z!Nm zmf*{P=eg@<1E0Pl+HJC%elQM%dOR8$2W%^pAHVuHp4s-AMI%I#q3?uoZD<_uLr#lj zFI9j1{LAJV_{ronG!7I%&VyN(o>?^FyQyN28JBaFoy@N#i|=g5xX5_VzqxM@zF7V) zSS{opYyC71Db?|J1~$`ZXE;Hh`oeZQ_|9vXCwes5*$Y_ULHhMcf{A;|mf zhll>TeRYv}*4V(u7NVSa@x$9o-_!W*3BZ>Erv2I>jX5fI@XQY(&j`u>&iIV8d{SfoC4K{Uk0s&S#=Uzr7fE_7n5o|9fi_4POpC-;Z-9>{{zcQ2Y`P=0Bm< z4$f<6-r!iJ{QY|N_jhgIJ#&so5<58m5#`+ zw}N*SD!qL-5A!N@H2y?eKh=`7!d0xL0)f z<>2Fd_~sSYT^5UuP2^VtPygTDQ}&V_cv-KiM%*aB81#;Zl)rz^Sb7=jA7N4NUxAO~ zWfA3oujey`QPzD5vBwL#0O*397EN@xmE@Dvdqea0QpoxAk$X%1!B@=b>B;0YG#|7* zto;2sz3aaG`H6eQBC(hCSJXq{*KDty)lmKU!9U=#9Z9S|bAJfsjBgP4jPJ597Orh5 zzE$vx@#Vf!KKK{h**>kI_!g26bQ@A$xVtIhEB550-Lroy$9*m6-&k-UkNe@OR?PW* z{eAIAR6Ii0uez;)eev*lUVgW|`ljWFqH2^xiEAGC`TqIfPrWhG8omg4exLls_piAp zM#Gm8f1$GD$6ehP#%lN~;JGjGW82gJv1@qSql%C7hF%vB|0_L&sI6oGHz z_N>mQRk4N?6uuzG)1k_)V%(R3@1v%t7q+OV&u1fDPsQiPeJ%Kw_IG~WvaCK|Ddrc} z?-_g6C^=Up{P}XLlKOle@bSEU2=_toZQA{P7iUp@zEaHJD*>x9|0@EYBe3-__YcS| zaS4IG7WKvV>MOx_*6xkN+T@W#LE($H@bSHR=VQvhd(tPZZ5yi3=fd+@9$*!qAAHj% z-ttJhKz%+pp3_5oo(9YV-*c6ZKHNT`K3^i&O;GQZxGx3Y%;AUob@0{atHF8^>(2?k z8t~n8L0@}EPkp{(@CDE>^1OR|k&4U4_d3{I?)rQ_@UdSDP!9NB+LgGnle0cwE!Oj_ z-=i)BU(^5H`P}IZ*jWNT{{UrIK41m;M(r5axdA(a;0yFud_{nc$JPCz8(&$`r2#wL z;In>@+6TTRuU~bnYovSTenq`?U4ur}sVlKQn+twpY%{MC+~d{+vOZp}mCJf@UJGR} z`Sf*aqaTVbZW)O`IB9W9%9MVJ`xWs|D7wzhpKj)Jf;?|qM+NFOdSnP6LtMGgu@%TeWBGwW4-g*_}uDW$qf7&hl)yay#>U;&aM_&=~ zo`(BLRbJ{jHU@ zcj)8MAAj0)^4k)h6Uj@FU*Bv%UJ2w>0LGk`Z=bRMksTt>&=+faO8Ld-`m0C2dy(Me zlK8lR=Xd&=&CZ<4_=!F36luNRuaI?yhJ1wFC~tz&8-VI( zGk)Er58`0&n};emb9jjOH9|E{H<6u;N0sVlqU+5*j11Oh!$#3g9${^<53U54joT23Mx#YXYwx{cUltCV! zJ8pdP-FKOPQh&DpMDo90ow!`*w>_iqeeRpdr8uQ)U-v$ z`=92=V>4#wq@~E`e#gtJSQqhk@yuU(8J98ZlGL=6grw}?Os*E1`4v95?t>k>{NH^r z#5?zOQ6u?TgmT8wA2sC?m>_t&8~8H7-*$Arh4m=-D#WJ>_)j-)Tf?;ssaI?Km0sif z>a3?{Reaolf;Z|h+N<45JvuD?r?r30i&JvwM@3P{)%CCWko(II!!BYw6FaT) zg-`M?2>N0`$}iXK6I!_>|EjcdvD<$VyG!knc0cud^l>Fk^$&@I6y8^?;8zb8_NCnt z{{YH~kFL7lIX(aKEciV?zB`WjC;UYg{M19fxAgigv*5Q5yXJbVe6w9$mNbC_ zg14=WwEy;lel3V6`O@>OYxh#8#3Nyy!iNC!^A9y)zKCB|{q)NN`T{`eEWtf>2o%4{ zwQ}(*F)Gro#^w>_;}qTTD+c$X4zZi_i1_si?-_DIChZoyYrHDwcV2It@V99vX7!J8bAYcLkmFM|?&%}rW_wQg zA@>ru@)P8P=(Xah*9SR_C-nq0`9dp~)K{)nE_%JKlpW-=_NVa{yQcX@gokXYkK$#D zzY=l>T=3F#y}oKu?(eMVei-!F%X+`$+MvqWZe8sTrSbh4k?#fGhxWGN;!<8?a=l0RUC%4|JWqK0k280%-x9nRc%CPGc68IE)6lO8J`s4H zC;Z5NZZCfCSn#>P^E_eqn(T!wHU2{28UH!u)26r5@TC@f%%_1zoEpB;f`7H==A71b z_*hSq$oTa=c;_OOjcQ!0rF}0by8fd}UTIUuZ}*~{^*ix!+t1npf1-Xp5q$e%uKtO0 zXX=&qWX*fQNxxo-e9Z+v+eHcPDMO&y|7qpYo^o47`fF`ZUS}kJ!@(QJP^MYmeH1>v zM8Vj{r$l@=-j8zD*P>^xxL!Z65wzg_>xP}f_4gCSD<6CnZ^jh&ENA!AMRPo{W45>E}f zRPx!cu33M4mEN!M`&9g{*9E?!i1%bUj&Z%S|G2BYQ3=W-k?-872t6R^Z*0A2dH(}{05Bpto155 z$(IuFCxD;%l8<}J5GeUlq?Jp)xSUEa`51Sh7rj=zl#AXf$l>p}lHc}{k|%V$M6XLL z7rlum(QCzvEYX_?Is8r`_2z2wb-e{zx#%rCfnLd9zW2fNsoS=0Kf-Zc;$h{dT@}z% z14z4^FE<>Ic&*%QwsYalm`MI_KFwIk zI0=6-_{srS{-^jW_6uhIS?r_VLC{wN(r?Er4g2lZ%Ej+mi(Koxn)|z4pWArnFN0{8 z*v<7f_BYFZYI=XPTX`n#Yp;)GbijZ>3f)_2z9InNQY!!-^L$} zZ@YFa+rQvzP|oiQy;SaYGwy=tda}!_^b8B^pP=h^{#TWI0Jlx{l=8vD;1Ao+eEN3z z{?2;7Cx9;m_))$p5ONvpB=YU|Ncn@@SY51=k90D z9oJTqUt_^<2+di;d8p`jzN+|guT}8HfzNbnU&kNzkIxOwwrt7LGqWu>pQQcT9Zbx;;973HT}ilP+j>ldA!KK9_{H`?l)* zHQ;mpPx=4#l~GGOHNem3mPcA1PSyE6;7b7XJoMyOr#HaQe&gj&3L?HQ5CUHT;L^;coR?-<~&JxAL5BTU1@b5{1aTVRX@1KPoe_bno%Q>zB;5oiV zHy>D~_jgq&XTF_#$D~?5M~UBDVvPc#|Dpfg z98(}VgufDa*3;)t{&q=^JOBAF@wLFSp4QDxeEae*o7{8zuY`0%~Uugnr6LvL&W${Dk3FP(8V1sHgH z3Gg2DvR2x;{_L?!$FOLtnVRcbBPntcW?D zz=kgN)S$od0pC6T=IU-xAou{vIbJY`wL zHwANhDOlVa_k9%%VO~@;2IYPQ%f~7h#5%QSs=BXDQm|&0f)yzW`sXNE23R^*-RA`r ztOX3Es(Z&g-~qk!)qM@&jp{zQM8UvP1zlKg_1~fHZFeeI37Bw~x-SQ;eO%p_VE?oL z`)!HXpK@Yd)xA#9)dG634pt0U`+~y9<2kwrumaDwemu{W0Vd)(Cjs+k2lEWD8ucHD ztk*{0znM8JBbUF?Xykj8v#GMjzg59YcD~TXo|V~Kaz^r_50Zy4*iz9IM=4kXem*aT za36v^ANCPlSSP9_j8*)h<_Z>~oZltpJ|5SNiyVs14?h0>b_w_s(SCCAe3uA${O$su zM~h)U*W>9we@`MG^11)%g*@kJNlX14Vwq`lK_bNY4p99q@3JIDamzp zE%bVQ*SxFjO#SJZ-7DwyH;))gdlfqCCHmd(DS98E&=~Z``7B7t`EPoLys4Lym70+r zHbU1Qf}FEs-}>eBdy761d7`JN5j~tw6LODuc1m*Eq@?t@DPb*x0{WVTDAxx$q))`X zPAB{>l!pK*m;G9yrJQFj!uG-r=D%Jq;$J!VNneF~olfkaT-r-JSgzNL$aR09;zW8c z?sYnmTMK;&z*8>Ai(IYTu<;n5y9jHLzZIyb638pi_(YEbbj4b^A@4ZjLdgChl$nuj z963xeK1s@9&!+c7wUE=c-xEDrj$XB$cE^9H{65wGE-5WFNru*xbm{U$N@PD2fV_V% z&t2T^uk^nJFa8uXqKA1*$ThE|?Ci|cSvlF#-|4!n`pO~qt4@F1S5dkymHKSk8}^I! zPslx;kr@j@#!0qJ;pe5t&kK2@w)&ed$iH`?&`5nS{)Bv2A~iiNH9h4b!;376Q}qEk z`GBu?nOOMHC))-Hk;IApfFV14NjdXNFE{=^#%DyrO31AN6d}T2ihIXLDlSrP@HaZH zC8s52ov5DukW*NFV8eetf6IJ67d^Qsx8@Vu6(QF~GgD^gB&W_wO*4KhYh*@dirB?V z;!l4|Aa~}rvn$T)dvvYPh`wr+Tm51l5mK+N&q%GzBq}qYuFt(g#VK?6pbd{6-0>Fm zC8GRP{Y%ft3K^eWHJZ(0GaEE@roJHRr2ukW=U30){MfQ;>ML(VALk*2oR2i5&CFxw zLxu8dRP6JPH{N$#Mm-*sTm7P3LiRhN$J#V?JweD@)Nga9CwZ({uTozPJ?Bd~^Scy$ zw5y@>wnESGq}oE?(DyTip6$x@ab5mPc|+%=q@42&zeXR`K!09A{h;#z1~fjAR|vXX zt=y2;=z5dUpU+cA$S+ABn?5JQh;=x1%sAtDrX2E|&&@yUu6a|&FmAS;%1>*3vVS7v znZ^{Oo6Ss@{wl0S!T^Z(Z5oOdr>w%EgC2dm(5;hu8aru#*@-S6&L@f5$z_fFi+hlYULu2 zYltG&xNlyl;bophJo~LY;EOGEw2O2e;7cuZj6dmIz*lK>9>YsM|I&ZbJ3do>7`}%u zp|5QhSx&qa3X|kX0CFfF<#ButwwCkxS1%X6few*+8Lx))8fC}mKOyUhacBL}&Pv$n z_+06ca;Z1Yhj8CKLBmVE5zn}Jfe%>dXfNr?pf6;hv(|4h=n5@#^o#NeKv$;GN!+-O zz<83r8gz^w;ttT$L5T`$cs0=J3xNILePgNHYQ!H z;eonncOK}9HThBxltVfn@D&=J#DnWN^pEtlpwr_a?bJCe(huF=hV&*>D*6DRSTA}@ znyPZE-Vo@ldilHO!rzdd@<#M<9m=YwvH?BDcv&xQqK}v0t??&LU_*J~*`@qU02DeS zj?E~iF+RqX?NjKae|92n#hSc^+Fb?kk?k&~3H35RszIm6Tja5QlCBVR&M)igU+R(T z(jnlPKVH!3a>ahGQ?fqjS9rZrTTj#Npxk1}Jy}0d0J<{G-iGpq{Y14!Cw_6=ly*|T z^DE`Q?w8Q}&yFl7-U{KbEeJW3&p6cfQ*x~3TvxW1bA8!b&h==$T-tAOue$n^`rx{< zPABEXzJ~4aUDR-SWh3RmiyNk|ZKRy*-MT$yo?WQqFrH^fz>JIc%xfu=afo5#shi* z{eX#plxKxO;Kf9ver@H@m#dXa+_)YpbdoQgZ=U8+1$dybL$B;!Rp`P^h} z57zis!LC|B(Ia_Id5lvz@a}Jwe$r7N=}JK7*XShv-0!5Hqz{448W-+AlAiu^KUyz0 zcX^ z`bGKz&{^Y?>rwRjb4Ek;RtV{IFI)$xk4v)S?hsz#e>djm-Tt8F@1U959@_K zuCH0+P}qPz8L!;Qb@qz?)_B)6qKEtFRz0@wlsw(9hUA9(OUP%utn)C&E3pB&=6HMl ziR~`|pEXX_c^vhWHK0fO6P~M}zqB`WsnXB55z>D`p*Q|M#(P4xFTu+^!}Gn87XXy< zhVn8G_><+Oi*%Yi$xEIapg&>%K}Y*wR~*kRkY38gANotkeu92+{zf_ec;%nxKxDmH z$G-sZkc-puC(tNol8(vMtCj%;=UeEk z^Uz}0Rc4{H>SKOXTj*#f^>Uu)JXq(a*k_%G7C^7pLPt4-xu6SJ=vaTGV|&QA&@sPB z$9Zjug^u-3x&ZW6TIj6fJm;adA0z!`JES~6==Nq%#`iFr@@T+lJk zC69#Oo2cwzd1FxMB|j@5hw@P#XC3cYUNKF{kDO1|@25P66y3?@K`zkw0Yy(k2{g(l3VKd8}dIN zeAaQ@x*tP5g$?Lw$WP|`sm?=dEPh(ozp3AKSox#-DdU0Hsmk^EOT1itR5{xP+Z*`_ zr5=sHPdW~BJVw3S@?lRYpp;8IsE2k}1Anr-4N=a|C$2X>U&d>6;%{Oj&wUA?)BTmW zS=Xs)zqP+92LGw%ZJEU`>+@1LE{)h_T?eIItViibGugiUB4(hb^E2AmySDezJ$PMjT6tqTJ_{L zphxTq42;yz@tXE9Z^U1ttkHQ8=R^Ou(AxegVW;EQI{zgeoL`9@G7sXoO?z2S9H)7o zr^#uE&*~@n3N$`x|J2943j$vrK^GHe?I&!%A-+^(*e~*|cJg^89`xd8L;VitPYD(} z))Vb#KIdBKh^HUycZxJR$qVZ~0qM&@r@3R(_p>Np?B`|B*4yXgewO=4T|JB5TC`ir zZw!iT>F;>%ocS*0qK|f1A@hxSN;zD&DbeiF>xuqX0e`aRuR_q(YVu?r6~w*!Xr$kT zi_|^sJ(=Iu^985sx89B#KAhBt^|FJ#wT>vc2Yq6u{wVx4gr+M zYvodJ+y^K0gDyd%GxRj$@8(+bKB&=2K5?JZhq$vI3qZ#>GY_omi7YSer0m!8O#G#O z%C-Hj=uWntSq=Rz(2E|im+x&*59RtmXSJ8_H;|t8TGug99-iOm=P|?&_D9rL4t*!f z^AgZiX?`>mmqOqjwRL$Qbj)|^Wq;(+=p-)I^DCrJ1f3oibG#UPVm&3`vyPv6agp^* zJ!OsPDLctJq3gJkXVqh!-%?LJ=yiV@il^&SCHGY4Z+Vc*JhS$j)L-0ye(5KydC5Gp z?n_8{gZBQR>^)h#uz}74NPDgOxwJPCbb7qR-jb$~^+->=Vto>Ly_)j&zsz5LDq`g|t zq0uhKUk&?Td+AC12cOk{>-sbGgc{M~@Sa#tc_VtP>jBhL*?=C2v#XWTqxZ`V^>?1X z6`j>Do=+w}_4z@s=a1;CvE+f&gOmrlLcX@nt+!8(*QJnqvh!a>psN66eOuSTDYq7M zy1fm>f$Iy_=O*hqFXNE#kMc{GEA7ZJT$PJm4e2QcpEcgreNpNuZA4GaWhd6-{1?ZFd7%3=QHJ} z^9u#t@Vk)y??ODjRM7jCf-daq<^dLBAF~wuiwW2VD+7$jK2#oHH6ilbg>}>-tXGy{ zeJ&B}QDuNWtjpwLy~2s-^*lfyo;k@z&wl#9`uie zfFAT4g@87+lMtXAd6x@V1?We8RB82R|fcFo=Ypz#^?)aZHdl-y88rsagX ze$Kx%O36u0IsC;L7e6vf>RR+vqn!Pcl#3p|k3`7!KPBCGv3*iXR!&;v`vg2!?v7S^ zaz7h$`h`1x%Aq`-ODE*~G)LrF4%Um^36K*4{Acc{`)>HQ>@krib{C=CYIi#!FfKx_ zCrnAtOi4-(Ce2Dqxi~W^Jvo??r3j7xMIY_2gxt*MN`LGYtpmU_nx5s{Y!zDc2dJ;^6^Yo!@KbeEY)}id@m_7=n6ERPgi7KOGq6nJ`uG<~$jE zoIkLiFl;g}?z6~^QC9DHi+qGaXT&eM7;-BCQ64_$Zi|h`yL$V%R(agd^=N#er=jzV zVkh~nFai8QiyW@w=2^-cIyc{teEL%Y{&I^Po@=j)EDxUxciQXXA^FGgnf5b&oTpmL zLm1EX@`mgrp8gZE-WZ2`&7Owj(BD$fHRf-HCP)0@x~?s*&R>zw_DV=Q|6ifiFRl}M zEP9#Wgw$6+I@A~C5&!=SDbETim-WH(lEt*gKu8=pU-UPri=&kD`N|?EeD29w&i!v| zc_HSb)^eVUvF0oH^{n(fhhi<~xe;qQ*CE(WnfE+5pwl;$H`aP1{r@dw{JGB_bVSCP z`={lWa_$?leb9dH+gZ!G&qn)5&;2iJc_QkC?T+-^U$M&PK8W7lBv1HUYn9LEJ!?7F zcf;{D6pI{Z1O1Ma^ZDN@hwC!zCuu+DtyX%jdsxf49%1#D&;3?(TE;?(~Xex%aN0fH*JO4xJ*B`tNE#;rSfC+imp$$xc$AJ zf|t1P`xJ!CcjLWaAu%tJ;{ksHU@P0pzsj5EDgp7;vb3)0+rx$Xv zWo94owkzyzr|kYem0fvsRMi>NoF9k zI145Q^g&8kb1+%lMC? zhrfddLYKa`)jWcTE!_W=%sc+Z_8H%;tC!Pa(yNc6hxZGCh+p2vGIHQ5*|2gqwpac; zlvGr{dHur7y%x0m$;`8M%&v|@#}{k| zzcmWKkuDI2QT}T%V4ozHE5~DV6ofvbCUy@~Rom$ft)gh_bvg5&INiO|-Dipi5gp~L zE{ZPN3n12gT&{`E6lYW4Mm$=b_>Rg?<93c-@IlAN9;r6Mt;owwbMD7fA7h{uhY- zO!6!)x5aD{+fg)`On!;GNBJX>G3QF>WowqKT1R>^{yAOm7qr_z_$SY47GKX3C9mn@ zwEhn;-!8Pr@%k|o%OTFIEkP9kM=v7th*e0juaB&` zaZ4Q&y>AsaV-LB1dChMdPI55^dt$!+= zC;dPaeXR2W(NE?(-J(ktWk%Ig<72&Eka_oa9r@(g_r`t&y_hbM^9%n1;b(1r)1qi= z^O?;2pMG1i&2aQmJ#=%QZ)qJK;+G|4r6bzqOou{}&{Q)B0 z?IyF^sq+=tTgN`ml!eO$m!AneVyxb1W=9a?@X^ISi9^+)%j z#qt`m7v%}W_(znio${_TImBDWe3gtR&c1m5<%1u}#ea&Y`Y3jz-36k5O0ftrr<=lA zYQTQfSL40PKa&<*ExFL`&dYTER{qW-KArL8k4)xqF&?qC9^CSgz2}He)_+dd`y1^H z5bcdg3>+NdA(6?E*Q_pR^=g^-kxgk^dUwb;3%$5*k?R54bs*Yz(T|6ED&j}~oz6Tb zC#~+j=A)W$}r{~J?0r?;8I1uG3$4@4QH_cg? zM|q`#>lEiJaWS*MHS*Rc4z-FUcR^?q2TZLen1yc zdAe}^6E$C@bg~2a!hUG2=Z`wDVe)Hza9>4)`^Y}TD-d>Og?5u826bq4>X0pUN|$8EHDu+~)C%I>%xD!+-0{mz{J{>`7?$|gR_Z!V{6<5z13p2O{4 zxHxrHZ0;hukIo0c%j+|Tj{n$hSK#mr@K#0OCHv9N0ny&M#5RQ!Ob+oW2ioO}Si=3@ zz?V-_`D`|)7^?6 z{Xx7@`C;wpQ#o79wpP-4vb!VwM;t)(%U;P7xy7dPO=iAa#(6WU7u>dcqwHqM?f|E2 zeDOV% zKaO`iy!-WeE9G-svOAO0^>%|F2tS#99IYj-uC%E)WM0`(98tG|lFMB2lNsgeJS#6~5&p=^|bmnZK&q_QFqxbH))T z=_cJ5xn7_h0-}D%?$1N{BnEY8bzICh^U=E(KDBcA*K`Hxlt393^L`o!nL$ApBK>GniJ7RV^3aACqE;4D$DT(r^ui>~zsEjTCsK-5Fl%SxSRqKs+XEb9aG z0?a#bZ|v?%pS}4F^ny|J;5Q)pH`0rwgL)V9fXdhM&4bp=SvJNGog_}z=L_{3i1yrL z5gE#gASMX4ao}R!O>Nrb-1o+yP`gqQMGyTm5cO_?%|q))DNeJ8OqK`fV7;P_`MTs} zC+z5WvxF|VRlM1o_`>2XuD9|}BBQ0`eDT!9H%1VjEPqbd`w4ylBJM=}^|?K2kxMs? z3-eQec~fJ3D?VTQ+IZ*%qv*Aw3&a5wHD4an()d3D$Uo>eV*03j#dqnq_v3TBj?z`+ zANUs-YTur2w*9K)OJtr*#>qEtX06^4mr8u(pHfcO`v>(Mh`1H~oOlRg$xE|Y3iG&V zwRTrA-=k*=mb4!HmR!yyyWwXb{4M&sCO#TukYRifZ$0zHBq)E}nDx~^o)~E^q)W*D zWKP%H5B~t+C$YFCpHG-1gA&r(U&MT||5@3x$AF8nzoGLLoDM%eQ#<*U3*(=j06S`; z*n$2JhYLz6PS=0rkbuSLOeoYybBB5Bp=Yp_|O< z`ut;F21GkY{w}o80C7~I__SDt%_I6@Z<8O;?i4Za2*2;bwe^!WL$5N59{NEb`ok=X zTWoCG#Ey`K;tK*Y)Dke;%g{v{pQU(S3R|MX$m!m;b5xwndQtFzG3#2IqA zBq!b=^EEJz+S`5K*4+Fq~70;1nE+w-Ey$$UUBmwDS?>i>4$=UMsC z3q;XF{RKi-M6-K}%Pb1VEOttFYunb+81>7@I!k1c~a0d?>PCus#7qzoLyS;>SE^ zI`a%n`}XHEM?QL(_{lFAhXB!!TZ*V%2pj&$xG80xa>ii%ko?y=x0Cgk{1S{}FUk#w zb(TqXOM!`u5r@{^n1@xqrwo05So+C*p?NCW10d!zv*$^sh$9^0O=P}I#xCwlE#92^ zq--9^Za=5%>lfzLK+O9liZ$2KCJ#qoll^EvtC=tN`XAO?;(s5CL--encE{!OScy+x zehthMH$eGgc-v$319}WzOp0W8GNUBr1QbKhtX4xYymG z`jW}%dViq(03r@OPy0+BYjgYk%=67z`?;aczz({C?5~W%54(Y|Kdabo*V>QxsAryQ z886?p^4N|QbPf3#@dbpv9>Ie$BR|ItRQXS2+;{M!lo{5_(0F7zr|bOyyMQRqDfxvk zQ`SS+S;jo=pZjyaszbxZ|B{_Rnw89VrS`i&R(0F=6fTzdlFjNvAA|4&nr;iOByC z^jbXLDL#ioJzOKJ!}FEIe5EC^j<^G@)95_uSUFu^P8g>Gp{K^hY2pKwO-|JMubla+ zHVuD2aJJ1V=mewaz+XVcu1}KlM0Tykf(NJ=f?w01&_!sqxm^Wojjs0dx?J($7M%KGxqYK0Vtlh1iuTAIYY}Jf)dsTY+K82NxMt;vM zalc9rFvc8Ezl#{_88d@?|3QVuLkj(jjf__Q`@ZrP%6~B}6;?AE?^eJ4j17!|SiZh3 zU(c8jr+z22Qy5^3X|H~lGA49Tzx|Acj_S9SG00eYk4mp+%dR-s~HpdxoR1ZpF7qtmhyAAT0GC==T!!N&Qitb;^z=`jMI5Nznam= z>)L+CI9>-XWo%%a&g-5vjHSF@*uYrM>s`6Lo>b46%j+dUMnBJ|(|JB!#hAeJ$Xd)# zc|O*_Sb=#7kHh159O_~WG8XZ8&B)`E0Hcxn?MlXY?(a$&8yJhY9j{|d=k~9X(a7zD jpRs{4m+M!Mk?IuveWIa-itj)>g|3|n%XTTO=j;Cmy}tfg diff --git a/.lake/lakefile.olean.lock b/.lake/lakefile.olean.lock deleted file mode 100644 index e69de29..0000000 diff --git a/.lake/lakefile.olean.trace b/.lake/lakefile.olean.trace deleted file mode 100644 index bfb3860..0000000 --- a/.lake/lakefile.olean.trace +++ /dev/null @@ -1,4 +0,0 @@ -{"platform": "aarch64-apple-darwin", - "options": {"env": "dev"}, - "leanHash": "dcccfb73cb247e9478220375ab7de03f7c67e505", - "configHash": "17439028364340488343"} diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean index 8b5d687..cbf418d 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean @@ -538,7 +538,6 @@ def dot : BiLinearSymm MSSMCharges.Charges := BiLinearSymm.mk₂ intro S1 S2 T simp only [MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue, ACCSystemCharges.chargesAddCommMonoid_add, map_add, Hd_apply, Fin.reduceFinMk, Hu_apply] - repeat erw [AddHom.map_add] rw [Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three] simp only [Fin.isValue] ring) diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean index 4ac3197..a871c11 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean @@ -152,7 +152,6 @@ lemma lineQuad_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) : change _ = (d • planeY₃B₃ R _ _ _).val rw [← planeY₃B₃_smul] rw [lineQuad_val] - congr 2 ring_nf /-- A helper function to simplify following expressions. -/ @@ -193,7 +192,6 @@ lemma lineCube_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) : change _ = (d • planeY₃B₃ R _ _ _).val rw [← planeY₃B₃_smul] change (planeY₃B₃ R _ _ _).val = (planeY₃B₃ R _ _ _).val - congr 2 ring_nf lemma lineCube_cube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) : @@ -210,7 +208,6 @@ lemma lineCube_quad (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) : rw [α₁, α₂, α₃] ring - section proj lemma α₃_proj (T : MSSMACC.Sols) : α₃ (proj T.1.1) = diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean index f708255..43ddbd0 100644 --- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean +++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean @@ -121,13 +121,11 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where left_inv S := by apply linearParameters.ext rfl - repeat erw [speciesVal] simp only [Fin.isValue] repeat erw [speciesVal] simp only [asCharges, neg_add_rev] ring simp only [toSpecies_apply] - repeat erw [speciesVal] rfl right_inv S := by simp only [Fin.isValue, toSpecies_apply] @@ -257,7 +255,6 @@ def bijectionLinearParameters : field_simp ring_nf field_simp [hQ, hE] - ring_nf field_simp ring_nf field_simp [hQ, hE] diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean index aba0497..884945e 100644 --- a/HepLean/SpaceTime/MinkowskiMetric.lean +++ b/HepLean/SpaceTime/MinkowskiMetric.lean @@ -63,7 +63,6 @@ lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by lemma as_block : @minkowskiMatrix d = ( Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin d) (Fin d) ℝ)) := by rw [minkowskiMatrix] - congr simp [LieAlgebra.Orthogonal.indefiniteDiagonal] rw [← fromBlocks_diagonal] refine fromBlocks_inj.mpr ?_ diff --git a/README.md b/README.md index e0fbd2c..f2e2ca1 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ [![](https://img.shields.io/badge/Read_The-Docs-green)](https://heplean.github.io/HepLean/) [![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls) [![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com) -[![](https://img.shields.io/badge/Lean-v4.9.0--rc3-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0-rc3) +[![](https://img.shields.io/badge/Lean-v4.9.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0) A project to digitalize high energy physics. diff --git a/lake-manifest.json b/lake-manifest.json index 2e0a53e..b6dca83 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589", + "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c", + "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,10 +31,10 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", + "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.36", + "inputRev": "v0.0.38", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96", + "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,10 +58,10 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "cd7c51790cac1a32c321373d45700290b3e8496c", + "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "v4.9.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/acmepjz/md4lean", @@ -85,10 +85,10 @@ {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "rev": "1f51169609a3a7c448558c3d3eb353fb355c7025", + "rev": "1daa0de7eea6bf8d3e1b0814156ede21a8a9e9e9", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.9.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "hep_lean", diff --git a/lakefile.toml b/lakefile.toml index b29acd2..f873798 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,11 +6,12 @@ defaultTargets = ["HepLean"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" +rev = "v4.9.0" [[require]] name = "«doc-gen4»" git = "https://github.com/leanprover/doc-gen4" -rev = "main" +rev = "v4.9.0" [[lean_lib]] name = "HepLean" diff --git a/lean-toolchain b/lean-toolchain index e5ea660..4ef27c4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.9.0-rc3 +leanprover/lean4:v4.9.0