From 2c0a331c71ce1d25c4e32a47a4339b33630a8941 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sat, 10 Oct 2026 22:25:32 -0500 Subject: [PATCH 1/2] Improve E8 recursive cost with four coupled frame changes --- .github/workflows/e8-coupled-retiming.yml | 29 + research/e8-coupled-retiming/NOTICE.md | 26 + research/e8-coupled-retiming/PROOF.md | 161 ++++ research/e8-coupled-retiming/README.md | 80 ++ .../e8-coupled-retiming/data/original.json.gz | Bin 0 -> 21883 bytes .../e8-coupled-retiming/data/retimed.json.gz | Bin 0 -> 21938 bytes research/e8-coupled-retiming/reconstruct.py | 211 +++++ research/e8-coupled-retiming/retime.py | 102 +++ .../scalar_map_comparison.py | 66 ++ research/e8-coupled-retiming/sources.json | 30 + research/e8-coupled-retiming/vendor/LICENSE | 201 +++++ research/e8-coupled-retiming/vendor/NOTICE | 489 +++++++++++ .../vendor/tools/e8/replay.py | 797 ++++++++++++++++++ .../vendor/tools/gen/foldlib.py | 146 ++++ .../vendor/tools/gen/gen_rates.py | 30 + .../vendor/tools/gen/gen_sharp.py | 33 + .../e8-coupled-retiming/vendor/tools/gx/gx.py | 296 +++++++ .../vendor/tools/gx/gxcore.py | 375 ++++++++ .../vendor/tools/gx/gxdry.py | 58 ++ .../vendor/tools/gx/gxpaths.py | 21 + .../vendor/tools/gx/gxrun.py | 226 +++++ .../vendor/tools/gx/gxunit.py | 47 ++ .../vendor/tools/gx/refcheck.py | 30 + .../e8-coupled-retiming/verification.json | 65 ++ research/e8-coupled-retiming/verify.py | 128 +++ 25 files changed, 3647 insertions(+) create mode 100644 .github/workflows/e8-coupled-retiming.yml create mode 100644 research/e8-coupled-retiming/NOTICE.md create mode 100644 research/e8-coupled-retiming/PROOF.md create mode 100644 research/e8-coupled-retiming/README.md create mode 100644 research/e8-coupled-retiming/data/original.json.gz create mode 100644 research/e8-coupled-retiming/data/retimed.json.gz create mode 100644 research/e8-coupled-retiming/reconstruct.py create mode 100644 research/e8-coupled-retiming/retime.py create mode 100644 research/e8-coupled-retiming/scalar_map_comparison.py create mode 100644 research/e8-coupled-retiming/sources.json create mode 100644 research/e8-coupled-retiming/vendor/LICENSE create mode 100644 research/e8-coupled-retiming/vendor/NOTICE create mode 100644 research/e8-coupled-retiming/vendor/tools/e8/replay.py create mode 100644 research/e8-coupled-retiming/vendor/tools/gen/foldlib.py create mode 100644 research/e8-coupled-retiming/vendor/tools/gen/gen_rates.py create mode 100644 research/e8-coupled-retiming/vendor/tools/gen/gen_sharp.py create mode 100644 research/e8-coupled-retiming/vendor/tools/gx/gx.py create mode 100644 research/e8-coupled-retiming/vendor/tools/gx/gxcore.py create mode 100644 research/e8-coupled-retiming/vendor/tools/gx/gxdry.py create mode 100644 research/e8-coupled-retiming/vendor/tools/gx/gxpaths.py create mode 100644 research/e8-coupled-retiming/vendor/tools/gx/gxrun.py create mode 100644 research/e8-coupled-retiming/vendor/tools/gx/gxunit.py create mode 100644 research/e8-coupled-retiming/vendor/tools/gx/refcheck.py create mode 100644 research/e8-coupled-retiming/verification.json create mode 100644 research/e8-coupled-retiming/verify.py diff --git a/.github/workflows/e8-coupled-retiming.yml b/.github/workflows/e8-coupled-retiming.yml new file mode 100644 index 0000000000..92f866dbb6 --- /dev/null +++ b/.github/workflows/e8-coupled-retiming.yml @@ -0,0 +1,29 @@ +name: E8 coupled retiming + +on: + pull_request: + paths: + - 'research/e8-coupled-retiming/**' + - '.github/workflows/e8-coupled-retiming.yml' + push: + paths: + - 'research/e8-coupled-retiming/**' + - '.github/workflows/e8-coupled-retiming.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-24.04 + timeout-minutes: 5 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 + with: + python-version: '3.14' + - run: python3 -B research/e8-coupled-retiming/verify.py + - run: git diff --exit-code diff --git a/research/e8-coupled-retiming/NOTICE.md b/research/e8-coupled-retiming/NOTICE.md new file mode 100644 index 0000000000..1b4ec86218 --- /dev/null +++ b/research/e8-coupled-retiming/NOTICE.md @@ -0,0 +1,26 @@ +# Attribution and scope of new work + +Jacob Sussman supplied the E8 label family, circuit, scatter, frame scheduler, +checkers, price routines, and general proof framework in +`jacobalansussman/wht-power-saving-lean`, commit +`9c94857bbaee886f8649edee0bc2d3c738f9555e`. + +The files in `vendor/` are unchanged copies from that commit. Its Apache-2.0 +license and notices are included. `data/original.json.gz` is also unchanged. +The new certificate derives from that file. Sussman's upstream notice retains +the attribution for earlier contributions to the construction. + +DaysSky's CrocSwap PR352 supplies the connection to the complex branch and the +exact coarse-moment convention used here. Its commit +`04b4c3c478b5bd8797d2663d89d8db4dfd0ad9f2`, source paths, and hashes are +recorded in `sources.json`. Prior frame-retiming contributions +include CrocSwap PR328 and PR350. No claim of priority for the general method is +made. + +The new work consists of four explicit frame changes, a deterministic +generator, independent scalar and frame checks, exact rational cost bounds, +and the short cost proof. OpenAI Codex and its research agents supplied +substantial assistance. New contributions are +offered under the repository's Apache-2.0 license. + +Attribution does not imply review or endorsement by the credited authors. diff --git a/research/e8-coupled-retiming/PROOF.md b/research/e8-coupled-retiming/PROOF.md new file mode 100644 index 0000000000..e82e7287eb --- /dev/null +++ b/research/e8-coupled-retiming/PROOF.md @@ -0,0 +1,161 @@ +# Four E8 frame changes + +All gate and register indices below are zero-based indices in the original +certificate. Binary frames are given by integer bit masks. The new certificate +has uncompressed SHA-256 +`3191011e0cb189665c8e0a9b97137dbed50241a0704c8be01c11b1b5a9518fc2`. + +## Circuit changes + +1. Remove `helper388 -= source64` and `helper771 += source64` from A65. + Insert those two additions just before A187, at frame 285 with basis + `[196,56]`. No gate A66 through A186 touches any of these three registers. + Source 64 has label 56. +2. Remove `helper693 += source98` and `helper839 -= source98` from A100. + Insert those two additions just before A198, at frame 296 with basis + `[257,243,14]`. No gate A101 through A197 touches any of these three + registers. Source 98 has label 253, and `253 = 243 XOR 14`. +3. In B193, B916, and B917, replace frame 599, with basis + `F=[276,148,84,51,15]`, by `G=[256,128,64,39,20,15]`. + These gates add helper807 to helper766, distribute plus or minus half of + helper807 to targets149 and155, and add helper766 to helper807. +4. In B873 and B874, replace frame 585, with basis `[161,81,9,5,3]`, + by `[305,161,81,9,5,3]`. The first gate adds half of helper550 to target198 + and subtracts half of helper550 from target202. The second gate adds + helper521 to helper550. + +The first two changes move additions only across gates that touch disjoint +registers. Such scalar operations commute, for all initial register values. +Neither change crosses the scatter. The last two changes keep all scalar +operations and their order. Thus the complete scalar operator and the retained +totals at scatter stay the same. The verifier also compares the complete +1023-by-1023 rational scalar matrices. + +All paths remain nested. The verifier checks actual binary subspace inclusion, +not only dimensions. For the third change, `G=F+span(256)` has dimension six. +The identities + +``` +276 = 256 XOR 20 +148 = 128 XOR 20 +84 = 64 XOR 20 +51 = 39 XOR 20 +``` + +show that F is contained in G. The preceding helper frames are contained in F. +The next helper frames are + +``` +helper766: [256,128,64,37,20,13,2] +helper807: [256,128,64,38,20,14,1] +``` + +They contain G because `39=37 XOR 2=38 XOR 1` and +`15=13 XOR 2=14 XOR 1`. The final target frames also contain G: + +``` +target149: [256,128,64,32,18,8,6,1] +target155: [256,128,64,34,16,10,4,1] +``` + +For target149, use `39=32 XOR 6 XOR 1`, `20=18 XOR 6`, and +`15=8 XOR 6 XOR 1`. For target155, use `39=34 XOR 4 XOR 1`, +`20=16 XOR 4`, and `15=10 XOR 4 XOR 1`. + +For the fourth change, let `F=span(161,81,9,5,3)` and +`G=F+span(305)`. These frames have dimensions five and six. All preceding +frames are contained in F. The next frame of helper521 is +`span(257,145,81,48,9,5,3)`. The next frame of helper550 and both targets is +`span(304,160,80,8,4,2,1)`. Both contain F. They contain the added vector +because `305=257 XOR 48=304 XOR 1`. Thus both contain G, and the paths +remain nested. + +## Child ranks + +Each climb contributes a child whose rank is the increase in frame dimension. +The four changes affect disjoint sets of registers. Thus their histogram +differences add. + +| Change | Register | Old child ranks | New child ranks | +| --- | --- | --- | --- | +| 1 | source64 | 5,3 | 1,4,3 | +| 1 | helper388 | 1,1,2,2,3 | 2,2,2,3 | +| 1 | helper771 | 1,1,1,3,1,2 | 2,1,3,1,2 | +| 2 | source98 | 5,3 | 2,3,3 | +| 2 | helper693 | 1,2,1,5 | 3,1,5 | +| 2 | helper839 | 1,2,1,2,1,1,1 | 3,1,2,1,1,1 | +| 3 | helper766 and helper807, each | 3,2,2,1,1 | 3,3,1,1,1 | +| 3 | target149 and target155, each | 5,3 | 6,2 | +| 4 | target198 and target202, each | 5,2,1 | 6,1,1 | +| 4 | helper521 | 2,1,2,2,1,1 | 2,1,2,1,1,1,1 | +| 4 | helper550 | 2,1,2,2,2 | 2,1,3,1,2 | + +The combined invocation histogram difference is + +``` +rank: 1 2 3 4 5 6 +change: +2 -6 +4 +1 -6 +4 +``` + +Its rank mass is zero and its child count is minus one. Copy cost remains 72. +The five-stage histogram is five times the invocation histogram, plus 240 +children at each rank 4, 8, 16, and 20. Therefore its rank mass remains 56,715, +with dimension m=45, stock W=1263, and deficit mW-56715=120. + +## Strict cost inequality + +Let a be a saving, with 0 1 +M_candidate(876412559609473 / 10^18) < 1 +M_candidate(876412559609474 / 10^18) > 1. +``` + +The logarithm uses the atanh series with a positive geometric tail bound. +Arguments are reduced to [1,2]. The exponential uses a Taylor polynomial of degree 20 with +a geometric tail bound. All arithmetic in these enclosures is rational. +Decimals in the saved result are only displays of the proved margins. + +## Limits + +This proves the finite circuit and recursive-cost improvement under the +stated convention. The general frame-transfer and recursion theorems remain +dependencies. A complete scalar identity is not a proof of the tape compiler +or the integer-multiplication assembly. No global optimum or larger final +integer-multiplication saving is claimed. diff --git a/research/e8-coupled-retiming/README.md b/research/e8-coupled-retiming/README.md new file mode 100644 index 0000000000..8cf566b7f1 --- /dev/null +++ b/research/e8-coupled-retiming/README.md @@ -0,0 +1,80 @@ +# E8 complex cost from four coupled frame changes + +This package changes Jacob Sussman's E8 circuit at commit +`9c94857bbaee886f8649edee0bc2d3c738f9555e`. It gives a smaller recursive moment with +the same 783 helpers, copy cost 72, rank mass 56,715, and deficit 120. + +| Quantity | Original | Candidate | +| --- | ---: | ---: | +| Conditional complex saving under PR352's fallback convention | 876248285600677 / 10^18 | 876412559609473 / 10^18 | +| Published checker's conservative figure, denominator 10^10 | 8762479 | 8764122 | +| Children in one invocation | 3974 | 3973 | +| Children in five stages | 20830 | 20825 | +| Scalar additions, including scatter | 3876 | 3876 | + +The first saving increases by about 0.01875%. The checker figure uses a different +reserve convention; the two rows must not be treated as the same bound. + +Four phase-A additions move to two later frames. Two sets of phase-B gates use +larger frames. The original frame table gains two entries. All scalar coefficients, +retained totals, and scatter coefficients stay the same. The complete rational +scalar operator also stays the same, including its dependence on every initial +helper value. + +[PROOF.md](PROOF.md) gives the exact edits and a strict cost inequality for every +saving between zero and one. It does not rely on the approximate moment root. + +## Reproduce + +From the repository root, run: + +```sh +python3 -B research/e8-coupled-retiming/verify.py +``` + +The script uses Python and its standard library. It checks source hashes, +rebuilds the candidate, checks every frame path, reconstructs the scalar source +map and histogram, compares all 1,046,529 entries of the complete scalar maps, +and runs three unchanged upstream checkers. A coefficient identity checks the +strict-concavity proof for the full saving interval. Exact rational bounds prove both +reported savings. In each case the next 10^-18 grid point fails. Three damaged +inputs must fail for their stated reasons. + +To write the candidate to another file, run: + +```sh +python3 -B research/e8-coupled-retiming/retime.py /tmp/e8-retimed.json.gz +``` + +The saved verification result is `verification.json`. Run the script to obtain +a fresh result; the script does not use that saved result as an input. + +## Scope + +This is a finite complex-circuit improvement. It does not change the selected +integer-multiplication result, the bit circuit, or its saving. + +The new certificate has not been compiled in Lean. The original certificate's +Lean data and theorem do not certify this changed file. A formal extension must +generate and compile new data. The general frame-transfer, helper cleanup, +recursive construction, and multiplication assembly remain inherited +dependencies. The complete scalar-map comparison does not prove those steps. + +## Source and search + +The baseline is Sussman's `tools/certificate/gcert1-e8-r783.json.gz`. The exact +commit and hashes of all imported files are in `sources.json`. The E8 complex +connection and fallback convention follow CrocSwap PR352 at +`04b4c3c478b5bd8797d2663d89d8db4dfd0ad9f2`. The exact reference paths and +hashes are recorded as mathematical provenance in `sources.json`; those files +are not imported or run. Earlier retiming +work includes Sussman's `tools/e8/sched.py` and CrocSwap PR328 and PR350. +This package supplies a new E8 witness; it does not claim to invent retiming. + +The candidate came from bounded searches over pairs of moves and common +intermediate frames. Frames came from existing stops and their joins or +intersections. A later search moved two more complete gates to one common +intermediate frame. These searches do not establish +global optimality. The search is not needed to reproduce or verify the witness. + +See [NOTICE.md](NOTICE.md) for attribution and AI assistance. diff --git a/research/e8-coupled-retiming/data/original.json.gz b/research/e8-coupled-retiming/data/original.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..0bd0bacf744f1c31419e05b834e34a92be77ae57 GIT binary patch literal 21883 zcmYIvW3Vthtmd(8+qP}nwr%^o$F^}b~C|6`2*=Xq@J`{X1n&HwWzj{oPRuRZPR#GU{5`OE+7!Ts+E-~V$7 zpL_qUj{omO-v9R_%>VsjY%S0KYmWc-R{!t*=j`rPwL_&?yb(s>*vGo z=PJ(s=c(@ZZO;EQP5)=?!KG{TFO!>Oor_0m&`bPNqI`|06#7 zLfugn`cwD}`&I95D7`C41GE>gK+)oKU2Tw5MUd;3{az13^@OYr^ML;X=T`cwGA z|B!l9^`+1BmVU5mXg?qCoS&OOt+wqoS z{|!TYv-fpqFi`2y!|#)C@R$GbuN@K!OM#Qd{Wo&u-?sX`|Edo8V^^|$+1+oN;w zxA#Wsk{|YX1L3Re^M|KvUzYaLyXLHM*!$S~{ps~Fmgo00hTo86-`BhAlUH-4 zJgL#jw@?*#d&$pLp62WPexUUyFY&{l(F-b$iv2Sx|BVYU`5nV&Mz`{ZT+t$sFGTPe z*_g5!_r9eZA;#;lBUQud1Gg8qUeo~cl&B%k1Qh{VpCY^f3BWs`wbQcArt4E}ji zo)BxNlC)Xa%DeKgtd`FRVmGzmUr{D-!VPukp5LMDImfFwg^OwVy?izEck)6&A=^ew zmQuiG8N=nJlp*rxs=}l&Aw-Ita%@|ASM#5!Nda$cvuBAS=BHkTUBO-;LX?yn%4nL* z4MGs85SzRy7t@kXIla6sml)h2zW!|bwtPS2Jp34>0>qoU07lp$pv07AM!+kN7!1X$ zPY-jYU;JEAV*mr$`CO3};7td~FHfaA*O(SAH+w*H^=-owB!wG4obSCK&gc4n?BFoI zS=o!#TUpxxql5!RW6^)&G0X--Nd7`#?)o22XiDCw(Ba#wVB?z;KoD=6UjWOv*t-|q z@YK29ZSg#1NOM2*@m8h&*JX>5xSbmSO=+kKZz;{PBMsEv%Gmk0)_p7EQ(*j7IDm7q z5n(NN)tYDQ-GL@rw7?a{xcKqEwzc&_k3BU%9eI2~Ue{*e7WCBn3lrS3rn$YgmyjBn zTx;c>iP|y52D-^s=5Vu&RMIQ}IgFz`Yy$XkG7f;x^i$JuvZD6|Wu!vh4EU4yea>HVcNS&#%2V>Y%j$gcV|N*` zOGn=QfL6Qr?U6vL4n70FmExRs&Gx}O=jR|in*k_2iGxp{ zy8!ZX`7>YjxB!EYB+e0_(B;-=6FSKU>nd7w-wt>wpcMW{vqhU2^(FutwJQxz6B2eg z*aA9gZ|fgPbVvaNS4k?z68QZ_ zn(Lx;>S>*!MG;cK9g)!vx( z*wiyt5x+%~xewx_ycTxtxSG*Xtl%eD+(Gns_nZ=)V$s5B<4fOvzM_zZKKi>4+|-Ah9}5ZM4duj; zM_|wH8ju4x{^)wS4UGLns}B3(I{cHl25FkALEhJ?|K636bx2TfAf&$rvvwzjaL3Gl zMK?RW^Og6+#2~*H;L!=?LJk?nVWn#tdZDQAT$O^=KKOJCbownm;dJq6p^`IoAjN}F zaens6%UB30VI_osxA(d8Tbv8248Bx^5FuLPz6Kw2JAErTP)|P71iQ{TntT{2SyF7Ff@RDN|Fw65oCgqLD%Ws=g%U|AYPS~zsX!EkExni6sN%-)5$=_X`wF_hMA3=xH zrQT!{g->b=5RaYVYg`n#7-NS7)OGM&5t@2u=JC;$t|8Iha`y2X77v?x9e`91#>hb} zXq%hIErEbQ2jV;x?{CC7cqnieR=o|}kNCGA#S!r^wX8-B2xfR+LCV0rEB)I8&qXjp z1LWm|Vz*T9$miz7v*s2!DE)pBfs&vGRNB4;S(GVF@z9NXz<%drp+^-IOX``5yDy#1`B`H?hc}qD6&QHl}(6FR+CNNYpmU%AQ$8f|FN=lJ@8goKCdtltm2xxaW zp!wpyz{`0OG!(Pj%QwcIba@fFtAE0Gxh%wKqXlD5!fow3by^K|3Z6t%IxLaTK?$)R zG@Otixat5J`#g9BAG2&(96OjFYiKrmP_WP;8eAWH@_HTHn5~&x1L117;ZmUF!Uc^T2)fA+w9>sP3Aex{muR`(6$cz5nhnw0!rTVG> zh+dA_F?Bixj^omsTM7(9VUCEsbT)IfmwV@24USCq+gn*SPH06^uBBV&s>f z9(x~PnMmH9z#|m4tlQ*&lvoB*us2laC{Gh~<$B-4I!QBMF_71PBj$}P3i+Uuk<4<& zfg&iSl7TV(=u%SG+Y-(MhP;QK>0=H3|NKjq(4U9uAVi`N{ka3Y6`S{IHZ9>d;?M zo~fnKgD;U*b2gJ0wCx=0otHj6w%uz1Z>ZJGwDUsTi82M!roPIMBs)5b@VW@2V2B58 zt!0VsD+|qMiPK@*>3=2tn)}}vRan$FyciuwIH3D8^Tg01dGw}jxui**-u#QfZ$h;C zYadE~%TrGXN0!(0_~o=%Ew=OFNV`H}5vlkt*7ZsnC&yS<)n}KOAeatfwQ;`##=)4& zlaR;=8`qtj=cx-lp{voUV<+uFB-~ewz3p!@uzzkWMV=|v52Fn|Wt9(oC&Gq3fZl5; zVx~a#Ms^*cnX^UzL5WOr{+!p1EN{b;?l~C!7;JMyt+|YGth&6gijEcDW9)4ZBkg!W zX=Gw*9q>{JmQ8sYwybQs zY{OC`bs$@!3m1He@l-w+Y}NG3UYHB_er`2i)ooNV54dPh=R%#i&}G@`SQVNe zv1@lq(S5N=lD3t39AqX~{$`%E{bBRiFe1a8F~~&SlunH%C<(<}d)f0n^jk9Xsn0}JULu)UOjTVQ?Ngg9*8$aW_5rVZWz9yoJw&9Kv zU5LeQUM{=H5;vc`I6kNh|AjkdD4F#l!K!9V7^Pn&uR|NvoqSRMOzpW2pVngIca`gk z@U-RRcM8g2NlZM3V_vM>adT5l>3qBENy!Ey{6q5jJTHO_*SKvq%U8OTYt2Fu->9cc zLiI>66r_o(7zty=^u9bd8Ouv6Z~4V#s`e}OY$Hx`KVnnZJpj^b-^ zb^_&u9M^{2zKdzwVu^k=qPR8}XWXp^a3#ow4$R)<3mymrZEcysN&mQ!-R7MgVo{N1 zDZ7*gse09>ZUcL6^*07zfHVo9=Mnv`?P7QA# z<+QH&*=+~9gweZ@`_F?hac!qo_oipGWX61#Fn#}Sr}laR^!b|l0B;#^Z|m9CLx<(z zUU!r7%l!lbUygeciLbOm=3ohrZ+)<=3nFiy5svl9$mc~s`#4BNKZbaqn>?ulGjhpo zhbH=N`IMLD-V6BhH0|b#BkyGS>?u)6(fEnoA#RIB_SEks-Fj4-B4Yk4xxAaP1dR*% zpnht%MjV2?>LyAL<7B%MKk;;JU^jWy%Q42*-PZe%3Pq6huR z7*Y}^ItYo2?_JBBXb?WhW-HED$K45;&oj~UbE!J%_<%Q(ewO7Lxp$wbN@N7|#N!Pc z&wM;B%0FCZ8h(#dvx%eaC)Nt%Jgv2IPQxF0>#2T>kUYe^0oPq!*0Eks;^dh(TS9Jg zGvbJk9F^}%N%W);Oxv6!sr)Sdd-15}Yq4DB)gZso2?5;s&(P`N=g~7`yAZQtbi@LQ z-Euf;Mw>6`i$D1h zx&SJw*aPK{P0*2i`{Lt;GN__!&De7#PeF>Sj#ndjvTf=^&eTl1nVv(Cl|;R=@;{XJIC8jZrm zs0Au##Lcp=7UucUSCDN_qUgCe!K7#%v-TGiPZpIoYEbjTV)e3|HQZ89 zi$YshGxjsz!?s?XIuL>G?IY(#3VSAdw&Jv_y%YtIveHcIZfMFYZFl6%V~xM%XLNRMZc&?3Z0A^V zr@0DZs%y{^3LaCObO~7$7ij_S$S6b2lote(ZpHh$h&Cq^U5$R443AzA(2P?3-C?bD%l-*x#l zpX9sWPH~Ku!SCCFvz`>c5HMMw9x!An4!!Jhjj*1>3E`3^W1#lo+S=5d|Hq8Hzvst6 zOndL@t7YtSUd|y+slzetK2(ad_$3beU2Z&WBPRn!_iC9QvdLqrnv__f_z@R zIRb%%|0-kGQaRs)-%N@}N=Wdoq~-;AE?titY~`5h)(3EUGP6y!uj3c!`sXai_Vf>v zmC4Fo6|A+pe)MSJR}3{=twSJi?OiV!y9Xfw(mik*ZK|vXO*Kv`oV7TY@p(!Ag#o$1 z+P3T8<6WA6-}l$a9{r!+#~c0+{-WRaufE??*lf%*_A~z~eL*MT$#Uz zrMUM8FlG$uEF4mOVo>A~3*sc(Kh<;f;$_?SP!QV~KS6YVXQ$?0=o{ggCvB3;ueY?m z?^FMu1M%niu6PKV4}bbU{91MK%{mUh;s@e5{80aA{V=m)nRxiUooKi)!vDo6A9rRh z9J;TanR5q)i@W)0Lk^%U?ca_XrWqf*s$Kh2VeJ>#8J{UN-{K5v+T5UUDG3DYG+qGlk78>z}2&5WG{j;zg$z#9h$yy zNqtFyU(pu7|94UJWPQ@f{A}5EORsm>GvMr3SMI}S|DGmhK4-g5foV?mDl*{ZuDIjQ z!Bar}SdQ@Xx_?lv%PjawzbLolP5(mlXJ2n@_WnP}eZ964+jBquKd8e6-Lk5$0sCLD zW!)qzv?clv*b;0$Os2?b^Jp2U>+kFI|8BfK>KHD%|GR8@bn<-Q-AA`;6mO4Z{y$Sw zp_b32LHZEdN&C1$tp#nG5P{SbC@l(&p-T2wF~o?(!|6Sa-NP=sY$fp!r!kE}u}WbN150nEMx9n4 z^;X9)G9xbUADlkdc-u-$|4zSK{T+x(UFU3<>A60guy{G&`y8j|SQo!Hj2vDIj5_;8 z#WmodVc^X+6AFPV-U=|XgA}T{Xise!-vyV{RB%msqZ5r(D$-*cPlXwwK>Ui1o9s?E z&5JB;yuwqlo=MiXuz9COST_wBCt$-PDd|{n9k^jJdIeMj(VKA5mXtZjBPn}ZfqT8A z)|M<6c*QX7%KGG{B2}7I2rU}Q`{2$Y^GbzK8_~F<(e30@A}<~Pu<;J{;ZHH91Usd0k{84wfvS;9II(zbRHP!L_FtnFIJFa)#XK&>~W$gM&Qn%7Koaa6~!^-i-x=0 zRAj_6j_b&HZLkLK-G>4Njpbo zC>zUw3rQx~gRwkU=U1k~KFBAD{#`Ly#Z;ds!Gp6Z8rb6ds0}8Rj}A!#HwuYZ?l zr@?E7IpA+{^_&ZF!uI4R=~bV5Oj&lL#77x%?Jm)-r%^7fUhJUDx$El>iD;{%)I6iX zlxf$~n-vPHqB>s!Iy0FPcpte`D_t{4f$%OUR&q^xVVQ~qQI8> zORp$**XPM$A!)W(p|NiG&*4&aN51L81qjl~)?U5v-B3o$^%;tHpqh-Eqz3QIUlRGVuivCu-%W}4{|7yGBb+-a}%N{%do9gExs z06|`ITVdm_bXFKm%d1DRsLfeum&%CylJ1+}Fm9FW93i;rdBfV@N{xYF>Vg>JY(l|>7C2By!q4XY;-9nYF%>ByT{p>M+WdAr5T+Hdo;;ror0b?@&ZN9o$ipu()@pA z(HpXxq5l&oy4RQ|h*ag}2H&onwW- zzmG?MprB7!CuF0U@v_3Yxh$4PryFZpOf}i*@WHVtR`V7_lS3&2n zLIrhQE!)Zs4z@I}obAjtla&JA#O!%Ex)?oUFy6#WaX03*B^)7Inl10g-g0Eh&=M8Q zk>QprRj8sUPqG}FQ28GXOg9`EVl{>Na;GGy$_T8M@QIDk7sGS}i<=3*1e8PZaxlOZ zW8oKemfH^#ThuToJc^NoWPF(j6MxjQE}E&c;q;{u5|U0IwBbBI zcF0N$4X;r2C(%Iz_@7eG0_?>KOX^6NUq58U`Bud)$a3stlc3tSFADWAs>ygSOC=Fb z1F7CEN!8EuUt3%Ah%~azgdL&!kK)emR4_(&?BzO75jZdEQ<&7XKr@gk#X<6rA(!wd$#~UCGSNax0P^X087mdko zbmB$6soXUB=-U_f$=-PkiAY6NMrakffgYhaY!bZ}q@U!>(+DJ$_uzUdgs#SHn2T)@ zx4uJSLjE$wQ&jQC-cSlM1OXIZzDlGE*4hjBs*Ybfr`V&CM#_x zNxd=9sq|>Yv-gA06K1!&@+^~7Fom0`jFMKAgjPOd%dKn3XaGiwou}qOeZp zITp_lDsQBN*o7bRR49o z#R!r~_BP(;_z=Wl(`w9o-QSDAL;5Qt)ADB;w%vb&73_TlC8CiC;(+R#OE#^-PP`Js zdh&zi;GUQQn|H@yUWCsZHT{r^9VP4~*rU z@)`zPs+^cPt(t)v7m+*1#*MJF4K{PC`gXcl)FS@z^1`p4s-?4~*%C`o2wp!iIMl7q zp_axZ3lqyht^W8qsq4lOUB&C$0_WBSSf=ZVHw?OymZ z`lD$Sa|3l6sb)v1&rm6lGY*q0^Dn$ip5DbgcZis{av;2uQy|{O0>z8))gG}!H%DblOQcZWiZRRj z2@pFy{>QNJC)`wV7q)bT0ima5*bc#x+;jY3gd-N0-#--(& zucYZXbRWmhCUrVA;m`2jHGo-R*!2E?(I(WD-6w&Z^mv9O8Mp!aLzCQ@eJPCna^NzJn(h!TnKb!f$Qw)khJO1 z!<;piuNCr@I^O0)k{0Ca)1u2(->$jpG_*#y{Nv~l=ovtC)j>^Iz%efEfU|k0GuhmW zm5*j+Ut1F$y}&h8eO=?g%fQc}stJA4HkINPpjbwa7j!KLa8|4`IeVh z`*{V%Db(`ogJH?g75i5MUV$W{GV?3MYT;%1^(q2s7CA9PJLVnL$f__!6^{Y;ArL;8 znbL7&2D2dL8Z=(?yGw|=JxV|d<~_Q{uE+x*^!BnO&EDN&R{DJ6o>p61+b}q~idwW6 zUIJKOwUAGL`Jhfn9pVmW|ECuAxmjB$duX+wmI1divlOm2K2Rq6I?=41$%{E_mGRa` zZ`K6QXpgz+m)ap(D5d5N6894@qAG3^Ik}PJ($)lsuJ!sOX}U(JF8y;P?*>vzRR`pa z%-Wtwq9y0CoR_02ku@*5nxP?42I0*+N5Ds@5Hadt1~g__@tPMG?+M^zyPBE{@r~q>w