BesselSeg0.lean

import LeanExe.ProofKit.BesselLarge0
import LeanExe.ProofKit.BesselRatio

/-!
Short polynomials for comparing `P0` and `Q0` with fdlibm's rational approximations.  Each piece of
`BesselLarge0` splits into segments of dyadic width, and on each segment `[a, b]` a polynomial of
degree 16 in `x - c`, with `c` the segment's center and dyadic coefficients, lies within `2^-71` of
the piece's polynomials (`segOk`).  On `[30, ∞)`, Hankel's expansion truncated to degree 26 with
dyadic coefficients lies within `2^-72` of the 60-term expansion.  With the bounds of
`BesselLarge0`, `P0` and `Q0` lie within `2^-70` of these polynomials (`near_seg`, `near_asym`),
and the step lemmas combine this with a kernel check of `BesselRatio` on one segment.
-/

namespace LeanExe.ProofKit.BesselSeg0

open Set PolyBound PolyCalc BesselPQ BesselChain BesselRatio BesselLarge0

/-- Segment `[2, 9 / 2 ^ 2]` of `piece0_0`. -/
def seg0_0_0 : Piece where
  a := 2
  b := 9 / 2 ^ 2
  c := 17 / 2 ^ 3
  H := 1 / 2 ^ 3
  A := [1193864631604714226995693 / 2 ^ 80, 5950698104519490576355 / 2 ^ 79, -1726028015540350302877 / 2 ^ 78, 3520621323850848582937 / 2 ^ 80, -1676593236439377265287 / 2 ^ 80, 95929908368170208125 / 2 ^ 77, -343119348639796210399 / 2 ^ 80, 151302973138313226127 / 2 ^ 80, -66206803876290323769 / 2 ^ 80, 28860732047661004973 / 2 ^ 80, -6282317183239397123 / 2 ^ 79, 1367924516671708505 / 2 ^ 78, -149119826486026371 / 2 ^ 76, 1042338468474863183 / 2 ^ 80, -228190830457776609 / 2 ^ 79, 200302039132610041 / 2 ^ 80, -44063000821067559 / 2 ^ 79]
  B := [-64843653975296200190293 / 2 ^ 80, 26144043830010618912941 / 2 ^ 80, -10106416168200332012495 / 2 ^ 80, 1899186764810318559867 / 2 ^ 79, -700704129008475848017 / 2 ^ 79, 510887438123814800709 / 2 ^ 80, -184783711239561536863 / 2 ^ 80, 33228035753614633703 / 2 ^ 79, -23779306854989369949 / 2 ^ 80, 8458447896399621569 / 2 ^ 80, -2983995405589164419 / 2 ^ 80, 519873453257177381 / 2 ^ 79, -88855763431124943 / 2 ^ 78, 29464265430703345 / 2 ^ 78, -37142564536699747 / 2 ^ 80, 1331616626284711 / 2 ^ 77, -2458647954013161 / 2 ^ 80]

/-- Segment `[9 / 2 ^ 2, 5 / 2 ^ 1]` of `piece0_0`. -/
def seg0_0_1 : Piece where
  a := 9 / 2 ^ 2
  b := 5 / 2 ^ 1
  c := 19 / 2 ^ 3
  H := 1 / 2 ^ 3
  A := [1196457608175834793682223 / 2 ^ 80, 4508938982220160275359 / 2 ^ 79, -4789854687117753398181 / 2 ^ 80, 2234029969154526524613 / 2 ^ 80, -60707903737363243407 / 2 ^ 76, 202523284505854420611 / 2 ^ 79, -164606313442519843367 / 2 ^ 80, 16458210307627566567 / 2 ^ 78, -6518761524857223963 / 2 ^ 78, 5135241618981701061 / 2 ^ 79, -4033975947764051767 / 2 ^ 80, 49464626140108255 / 2 ^ 75, -155305530411321481 / 2 ^ 78, 244049467885691229 / 2 ^ 80, -96017470144084255 / 2 ^ 80, 18921761440007659 / 2 ^ 79, -3736039720958723 / 2 ^ 78]
  B := [-58884961169648305079279 / 2 ^ 80, 1357777583683720459265 / 2 ^ 76, -3856474038512145814647 / 2 ^ 79, 2666464328359214166747 / 2 ^ 80, -905286335396487995417 / 2 ^ 80, 303659525241422684345 / 2 ^ 80, -25261428868336378283 / 2 ^ 78, 33441914513778396979 / 2 ^ 80, -11022309639083192259 / 2 ^ 80, 452347862648124079 / 2 ^ 77, -591295891591856921 / 2 ^ 79, 191998593847430263 / 2 ^ 79, -123528428824122423 / 2 ^ 80, 19594794397247531 / 2 ^ 79, -12174246428458357 / 2 ^ 80, 914970291992655 / 2 ^ 78, -1042121016939255 / 2 ^ 80]

/-- Segment `[5 / 2 ^ 1, 11 / 2 ^ 2]` of `piece0_0`. -/
def seg0_0_2 : Piece where
  a := 5 / 2 ^ 1
  b := 11 / 2 ^ 2
  c := 21 / 2 ^ 3
  H := 1 / 2 ^ 3
  A := [1198444183245405752360593 / 2 ^ 80, 6988170958935526472571 / 2 ^ 80, -1711872036565255845175 / 2 ^ 79, 184022168640327763019 / 2 ^ 77, -589379522733297371935 / 2 ^ 80, 28242745691922967953 / 2 ^ 77, -84263492339825752449 / 2 ^ 80, 30872859115087625367 / 2 ^ 80, -11183647564996011039 / 2 ^ 80, 2011368687852007203 / 2 ^ 79, -1440986767495156563 / 2 ^ 80, 257535439642041833 / 2 ^ 79, -183965556809368527 / 2 ^ 80, 8214507184504663 / 2 ^ 77, -11746582325788103 / 2 ^ 79, 8408582946981247 / 2 ^ 80, -1506941162795177 / 2 ^ 79]
  B := [-13474377275124154307917 / 2 ^ 78, 18316739976672767264037 / 2 ^ 80, -3005219183771648794275 / 2 ^ 79, 961712094474656185845 / 2 ^ 79, -604776106241567772641 / 2 ^ 80, 187867062117863295869 / 2 ^ 80, -28941428688801136663 / 2 ^ 79, 17735838611618445173 / 2 ^ 80, -1353340941945463417 / 2 ^ 78, 411788195286855355 / 2 ^ 78, -249824795459085023 / 2 ^ 79, 18875004939561695 / 2 ^ 77, -45402416571222497 / 2 ^ 80, 847053495965147 / 2 ^ 76, -500427203712225 / 2 ^ 77, 1164643664863919 / 2 ^ 80, -20700333490801 / 2 ^ 76]

/-- Segment `[11 / 2 ^ 2, 3]` of `piece0_0`. -/
def seg0_0_3 : Piece where
  a := 11 / 2 ^ 2
  b := 3
  c := 23 / 2 ^ 3
  H := 1 / 2 ^ 3
  A := [37499942009061320776637 / 2 ^ 75, 1379865738908836603443 / 2 ^ 78, -2509697632943633911375 / 2 ^ 80, 125170201051232751809 / 2 ^ 77, -371693273038332688089 / 2 ^ 80, 131957322132380495025 / 2 ^ 80, -45512756639601685763 / 2 ^ 80, 962491715311428967 / 2 ^ 76, -643111764099849775 / 2 ^ 77, 852283470291817473 / 2 ^ 79, -561759974434841409 / 2 ^ 80, 5767163261156353 / 2 ^ 75, -30263468438063113 / 2 ^ 79, 9919416608384465 / 2 ^ 79, -6503272591353885 / 2 ^ 80, 533279118537927 / 2 ^ 78, -700343894287505 / 2 ^ 80]
  B := [-24833057534946503888593 / 2 ^ 79, 15637722318511371984313 / 2 ^ 80, -2384184293924342335225 / 2 ^ 79, 1420135847360291229249 / 2 ^ 80, -415808595154774684781 / 2 ^ 80, 60143596948118497431 / 2 ^ 79, -34507366374277840443 / 2 ^ 80, 4921417566368751215 / 2 ^ 79, -2796528816256227985 / 2 ^ 80, 396133998108033367 / 2 ^ 79, -111956103675710745 / 2 ^ 79, 15781344645027419 / 2 ^ 78, -17742023143147993 / 2 ^ 80, 4966023004240843 / 2 ^ 80, -1381994621944397 / 2 ^ 80, 381475688236773 / 2 ^ 80, -26022983696719 / 2 ^ 78]

/-- Segment `[3, 27 / 2 ^ 3]` of `piece0_1`. -/
def seg0_1_0 : Piece where
  a := 3
  b := 27 / 2 ^ 3
  c := 51 / 2 ^ 4
  H := 3 / 2 ^ 4
  A := [1201505258126322074750149 / 2 ^ 80, 4204464932345317483853 / 2 ^ 80, -219263146633939813973 / 2 ^ 77, 321114293667893429347 / 2 ^ 79, -218619223608809227013 / 2 ^ 80, 71103941407837132961 / 2 ^ 80, -22438638715697198653 / 2 ^ 80, 3468611688845752987 / 2 ^ 79, -2114706707180279017 / 2 ^ 80, 638436339945738393 / 2 ^ 80, -95746026645997943 / 2 ^ 79, 57190701694881943 / 2 ^ 80, -4258777238565635 / 2 ^ 78, 2533302791007821 / 2 ^ 79, -1505941385541109 / 2 ^ 80, 447589998523983 / 2 ^ 80, -133082397870403 / 2 ^ 80]
  B := [-45205285216099742790577 / 2 ^ 80, 13027966437863624276377 / 2 ^ 80, -1824153049233944445637 / 2 ^ 79, 499827564232887341943 / 2 ^ 79, -269502291257579813111 / 2 ^ 80, 35899796629455171061 / 2 ^ 79, -9483298611534425531 / 2 ^ 79, 1245093797158006961 / 2 ^ 78, -1302365501628880063 / 2 ^ 80, 169789137222231169 / 2 ^ 79, -88349959196038795 / 2 ^ 80, 11472076483176821 / 2 ^ 79, -5947238389250863 / 2 ^ 80, 384508245106959 / 2 ^ 78, -24784732937805 / 2 ^ 76, 101824297661893 / 2 ^ 80, -12998843458187 / 2 ^ 79]

/-- Segment `[27 / 2 ^ 3, 15 / 2 ^ 2]` of `piece0_1`. -/
def seg0_1_1 : Piece where
  a := 27 / 2 ^ 3
  b := 15 / 2 ^ 2
  c := 57 / 2 ^ 4
  H := 3 / 2 ^ 4
  A := [601432638530426908662363 / 2 ^ 79, 3119862784884425903145 / 2 ^ 80, -1184281071410742327215 / 2 ^ 80, 394675619756905213583 / 2 ^ 80, -122252562599008162469 / 2 ^ 80, 36153013963027034519 / 2 ^ 80, -10362501580970244671 / 2 ^ 80, 2906296163544556629 / 2 ^ 80, -802666001877689161 / 2 ^ 80, 54817968117811125 / 2 ^ 78, -14859772167229679 / 2 ^ 78, 16025649856306091 / 2 ^ 80, -4304871265631159 / 2 ^ 80, 576804902562935 / 2 ^ 79, -154345018861943 / 2 ^ 79, 41269172771595 / 2 ^ 79, -11031981412343 / 2 ^ 79]
  B := [-40784969736962581723165 / 2 ^ 80, 1332870100990066956497 / 2 ^ 77, -2718164098647798443883 / 2 ^ 80, 169835468669281266433 / 2 ^ 78, -10451479519394565463 / 2 ^ 76, 20346315648070033249 / 2 ^ 79, -9818175187018319093 / 2 ^ 80, 1177122010986808477 / 2 ^ 79, -281006919225545169 / 2 ^ 79, 133746510204670315 / 2 ^ 80, -31757740554946047 / 2 ^ 80, 7528226993412839 / 2 ^ 80, -222761100242751 / 2 ^ 77, 421275138629949 / 2 ^ 80, -99427659419163 / 2 ^ 80, 1463663129537 / 2 ^ 76, -171903427045 / 2 ^ 75]

/-- Segment `[15 / 2 ^ 2, 33 / 2 ^ 3]` of `piece0_1`. -/
def seg0_1_2 : Piece where
  a := 15 / 2 ^ 2
  b := 33 / 2 ^ 3
  c := 63 / 2 ^ 4
  H := 3 / 2 ^ 4
  A := [601943661745418595964385 / 2 ^ 79, 2375532304695161289891 / 2 ^ 80, -827032968479956493973 / 2 ^ 80, 252930671315839865761 / 2 ^ 80, -35948027516456825231 / 2 ^ 79, 19502485352427142991 / 2 ^ 80, -2561954267465946819 / 2 ^ 79, 658049047924489825 / 2 ^ 79, -332566178550083537 / 2 ^ 80, 41520547376752735 / 2 ^ 79, -10277763806123359 / 2 ^ 79, 5056121047650343 / 2 ^ 80, -309509055145961 / 2 ^ 78, 151088192408155 / 2 ^ 79, -36796963095137 / 2 ^ 79, 8949199994995 / 2 ^ 79, -4349434247835 / 2 ^ 80]
  B := [-9283951696887746991157 / 2 ^ 78, 4439644809751806855271 / 2 ^ 79, -2076125447249549897885 / 2 ^ 80, 476799043534007427911 / 2 ^ 80, -107959239562202424689 / 2 ^ 80, 3022088927825868979 / 2 ^ 77, -2684389050560919957 / 2 ^ 79, 1184694232955804049 / 2 ^ 80, -130101335566785063 / 2 ^ 79, 56957269188149957 / 2 ^ 80, -6218759111539597 / 2 ^ 79, 2711182707523185 / 2 ^ 80, -590218750489433 / 2 ^ 80, 128349629969377 / 2 ^ 80, -27881906628917 / 2 ^ 80, 6049836571965 / 2 ^ 80, -327700914899 / 2 ^ 78]

/-- Segment `[33 / 2 ^ 3, 9 / 2 ^ 1]` of `piece0_1`. -/
def seg0_1_3 : Piece where
  a := 33 / 2 ^ 3
  b := 9 / 2 ^ 1
  c := 69 / 2 ^ 4
  H := 3 / 2 ^ 4
  A := [1204673894592598275042823 / 2 ^ 80, 1848520601193533208289 / 2 ^ 80, -74275225086863890901 / 2 ^ 77, 83948883053735148357 / 2 ^ 79, -44101260317721308329 / 2 ^ 80, 5526145099722623901 / 2 ^ 79, -1340770319835134885 / 2 ^ 79, 79457346684662145 / 2 ^ 77, -148134300245260615 / 2 ^ 80, 8521588542255799 / 2 ^ 78, -242795083624203 / 2 ^ 75, 1758424088566245 / 2 ^ 80, -395886639953605 / 2 ^ 80, 22196060216903 / 2 ^ 78, -19855667412083 / 2 ^ 80, 4431766480205 / 2 ^ 80, -493926212261 / 2 ^ 79]
  B := [-8518713514389966498703 / 2 ^ 78, 7502745190895751506981 / 2 ^ 80, -1619494066885212327837 / 2 ^ 80, 21495007668012266335 / 2 ^ 76, -36039741594438950087 / 2 ^ 79, 3737207602847580655 / 2 ^ 78, -3074878768963866031 / 2 ^ 80, 628478541703439023 / 2 ^ 80, -63919057494272801 / 2 ^ 79, 12955072799043037 / 2 ^ 79, -5237618883570891 / 2 ^ 80, 528366783981811 / 2 ^ 79, -106453388345819 / 2 ^ 79, 21425173476597 / 2 ^ 79, -4308362910921 / 2 ^ 79, 1731319171913 / 2 ^ 80, -173780212983 / 2 ^ 79]

/-- Segment `[9 / 2 ^ 1, 41 / 2 ^ 3]` of `piece0_2`. -/
def seg0_2_0 : Piece where
  a := 9 / 2 ^ 1
  b := 41 / 2 ^ 3
  c := 77 / 2 ^ 4
  H := 5 / 2 ^ 4
  A := [150683517908400618834787 / 2 ^ 77, 85075242309059364869 / 2 ^ 76, -396844893864407021917 / 2 ^ 80, 101791827353040728875 / 2 ^ 80, -94846859420629989 / 2 ^ 72, 345362898786441905 / 2 ^ 76, -1217076533087779841 / 2 ^ 80, 130883714675442365 / 2 ^ 79, -55311226830161661 / 2 ^ 80, 11531262209903295 / 2 ^ 80, -1189736142338483 / 2 ^ 79, 243574699279445 / 2 ^ 79, -24783237164123 / 2 ^ 78, 20080159069607 / 2 ^ 80, -4053165467723 / 2 ^ 80, 815983451555 / 2 ^ 80, -163956967605 / 2 ^ 80]
  B := [-30689446368646364616153 / 2 ^ 80, 6109308012958085543727 / 2 ^ 80, -149445848849087618511 / 2 ^ 77, 57656703136424614381 / 2 ^ 78, -43960700265703882723 / 2 ^ 80, 8298132885301736097 / 2 ^ 80, -388521797789399071 / 2 ^ 78, 36154196927255799 / 2 ^ 77, -53565903938242667 / 2 ^ 80, 2470707437352937 / 2 ^ 78, -909060989561217 / 2 ^ 79, 83438866789117 / 2 ^ 78, -15292593331705 / 2 ^ 78, 5599029131727 / 2 ^ 79, -2048143387537 / 2 ^ 80, 23396657413 / 2 ^ 76, -68378737313 / 2 ^ 80]

/-- Segment `[41 / 2 ^ 3, 23 / 2 ^ 2]` of `piece0_2`. -/
def seg0_2_1 : Piece where
  a := 41 / 2 ^ 3
  b := 23 / 2 ^ 2
  c := 87 / 2 ^ 4
  H := 5 / 2 ^ 4
  A := [1206185487769480440918519 / 2 ^ 80, 482168814045408826457 / 2 ^ 79, -125871508566292605489 / 2 ^ 79, 57883553710223823219 / 2 ^ 80, -12384161342977229513 / 2 ^ 80, 1264190286437927293 / 2 ^ 79, -124880618997010259 / 2 ^ 78, 96336290015852257 / 2 ^ 80, -18243140242947645 / 2 ^ 80, 1703222762506153 / 2 ^ 79, -314564847031463 / 2 ^ 79, 115196281827471 / 2 ^ 80, -20950262215221 / 2 ^ 80, 1894903666199 / 2 ^ 79, -682680152253 / 2 ^ 80, 122570720617 / 2 ^ 80, -21950517661 / 2 ^ 80]
  B := [-27287841237170045514049 / 2 ^ 80, 4847733216005659485731 / 2 ^ 80, -848970879565326642681 / 2 ^ 80, 36713098411788510677 / 2 ^ 78, -12568092944040204671 / 2 ^ 79, 1066140795220124127 / 2 ^ 78, -359109573249425843 / 2 ^ 79, 7514486233889283 / 2 ^ 76, -10014475359768349 / 2 ^ 79, 3323522969873537 / 2 ^ 80, -549792894346183 / 2 ^ 80, 45365656643451 / 2 ^ 79, -3736421993715 / 2 ^ 78, 2458495849719 / 2 ^ 80, -50498550033 / 2 ^ 77, 66332602089 / 2 ^ 80, -10884868977 / 2 ^ 80]

/-- Segment `[23 / 2 ^ 2, 51 / 2 ^ 3]` of `piece0_2`. -/
def seg0_2_2 : Piece where
  a := 23 / 2 ^ 2
  b := 51 / 2 ^ 3
  c := 97 / 2 ^ 4
  H := 5 / 2 ^ 4
  A := [1206702318284681653696249 / 2 ^ 80, 707075801122541561601 / 2 ^ 80, -20880095762539439695 / 2 ^ 77, 34792251818732266879 / 2 ^ 80, -421704152535094971 / 2 ^ 76, 624517784668210813 / 2 ^ 79, -111881253857826839 / 2 ^ 79, 19563018295478381 / 2 ^ 79, -419737859056247 / 2 ^ 76, 142024758814219 / 2 ^ 77, -95020080790515 / 2 ^ 79, 15748666480831 / 2 ^ 79, -647785094783 / 2 ^ 77, 211907762525 / 2 ^ 78, -137984132005 / 2 ^ 80, 22376424569 / 2 ^ 80, -3617593883 / 2 ^ 80]
  B := [-12278626060846537334967 / 2 ^ 79, 3936952664137734532209 / 2 ^ 80, -311778305073217938339 / 2 ^ 79, 97713079053158247721 / 2 ^ 80, -15170282170347604673 / 2 ^ 80, 2336490753133459627 / 2 ^ 80, -178711652546724953 / 2 ^ 79, 13591220238275341 / 2 ^ 78, -8229765178361113 / 2 ^ 80, 1240953973796937 / 2 ^ 80, -186526398333933 / 2 ^ 80, 27964878192933 / 2 ^ 80, -261506879971 / 2 ^ 76, 625031678799 / 2 ^ 80, -11656719467 / 2 ^ 77, 13900218547 / 2 ^ 80, -64701737 / 2 ^ 75]

/-- Segment `[51 / 2 ^ 3, 7]` of `piece0_2`. -/
def seg0_2_3 : Piece where
  a := 51 / 2 ^ 3
  b := 7
  c := 107 / 2 ^ 4
  H := 5 / 2 ^ 4
  A := [75442910131766689206807 / 2 ^ 76, 266648661624307027609 / 2 ^ 79, -115013450936359539725 / 2 ^ 80, 21888575370818618113 / 2 ^ 80, -121279155713796953 / 2 ^ 75, 164269528467787537 / 2 ^ 78, -107680537692727389 / 2 ^ 80, 8611849354677349 / 2 ^ 79, -2704057770563671 / 2 ^ 80, 418342688607683 / 2 ^ 80, -63966752354595 / 2 ^ 80, 9688594790139 / 2 ^ 80, -364047500853 / 2 ^ 78, 108744457707 / 2 ^ 79, -16157785923 / 2 ^ 79, 4781292423 / 2 ^ 80, -176241879 / 2 ^ 78]
  B := [-2789811150679448229813 / 2 ^ 77, 3258798234578929557479 / 2 ^ 80, -117729264549293466053 / 2 ^ 78, 67420922598716155145 / 2 ^ 80, -9573507222962535581 / 2 ^ 80, 1349637888567963091 / 2 ^ 80, -47270425887715479 / 2 ^ 78, 13174117532460583 / 2 ^ 79, -3654870178988335 / 2 ^ 80, 252518673538397 / 2 ^ 79, -17390953539885 / 2 ^ 78, 9556408418351 / 2 ^ 80, -654995371687 / 2 ^ 79, 89630264759 / 2 ^ 79, -24496108023 / 2 ^ 80, 3343746027 / 2 ^ 80, -456035081 / 2 ^ 80]

/-- Segment `[7, 8]` of `piece0_3`. -/
def seg0_3_0 : Piece where
  a := 7
  b := 8
  c := 15 / 2 ^ 1
  H := 1 / 2 ^ 1
  A := [1207454193784131071479311 / 2 ^ 80, 382656811760516768423 / 2 ^ 80, -74102346616508473905 / 2 ^ 80, 12675812471138891429 / 2 ^ 80, -1010779625078565753 / 2 ^ 79, 154008659710766049 / 2 ^ 79, -22719645747611607 / 2 ^ 79, 6543521427539765 / 2 ^ 80, -924879942902579 / 2 ^ 80, 64402096377545 / 2 ^ 79, -1107811244871 / 2 ^ 76, 18870846129 / 2 ^ 73, -326528683321 / 2 ^ 80, 21923591161 / 2 ^ 79, -5855266917 / 2 ^ 80, 194569405 / 2 ^ 78, -103047053 / 2 ^ 80]
  B := [-4987293652895186589591 / 2 ^ 78, 81535287347687656821 / 2 ^ 75, -84581328155917666351 / 2 ^ 78, 10882074604316683173 / 2 ^ 78, -2780425510881961411 / 2 ^ 79, 88243249493759097 / 2 ^ 77, -44560260963260193 / 2 ^ 79, 11195862982538881 / 2 ^ 80, -43766088690327 / 2 ^ 75, 174550913519845 / 2 ^ 80, -10843297364179 / 2 ^ 79, 2687215972803 / 2 ^ 80, -10382216759 / 2 ^ 75, 10249586131 / 2 ^ 78, -2525766335 / 2 ^ 79, 38851987 / 2 ^ 76, -76418995 / 2 ^ 80]

/-- Segment `[8, 9]` of `piece0_3`. -/
def seg0_3_1 : Piece where
  a := 8
  b := 9
  c := 17 / 2 ^ 1
  H := 1 / 2 ^ 1
  A := [301943417703093076025401 / 2 ^ 78, 265700180536884557325 / 2 ^ 80, -22845104992874413909 / 2 ^ 79, 217100712247348357 / 2 ^ 75, -985611424081575443 / 2 ^ 80, 133668879894533555 / 2 ^ 80, -17558870715902377 / 2 ^ 80, 140757642145221 / 2 ^ 76, -70887231858377 / 2 ^ 78, 35174840089765 / 2 ^ 80, -2155627377777 / 2 ^ 79, 523188580859 / 2 ^ 80, -62967180943 / 2 ^ 80, 3762856225 / 2 ^ 79, -447093127 / 2 ^ 79, 105716657 / 2 ^ 80, -12445661 / 2 ^ 80]
  B := [-17639776505604936981731 / 2 ^ 80, 2043883614949151352289 / 2 ^ 80, -117590768031759807225 / 2 ^ 79, 26887810542213876225 / 2 ^ 80, -3055923162054165483 / 2 ^ 80, 43182268811160373 / 2 ^ 77, -38863511525439357 / 2 ^ 80, 4353134306091729 / 2 ^ 80, -121429654243973 / 2 ^ 78, 54011554468211 / 2 ^ 80, -187128765761 / 2 ^ 75, 662162246565 / 2 ^ 80, -73056965457 / 2 ^ 80, 4022451443 / 2 ^ 79, -884435801 / 2 ^ 80, 48548839 / 2 ^ 79, -10647463 / 2 ^ 80]

/-- Segment `[9, 10]` of `piece0_3`. -/
def seg0_3_2 : Piece where
  a := 9
  b := 10
  c := 19 / 2 ^ 1
  H := 1 / 2 ^ 1
  A := [603999880252102165881317 / 2 ^ 79, 191795749431689918821 / 2 ^ 80, -29648451795759312877 / 2 ^ 80, 126742053065186107 / 2 ^ 75, -259000735180543761 / 2 ^ 79, 7909635812577083 / 2 ^ 77, -3744928277989741 / 2 ^ 79, 865863745016839 / 2 ^ 80, -12284341070287 / 2 ^ 77, 10991047722979 / 2 ^ 80, -607263747073 / 2 ^ 79, 16609023185 / 2 ^ 77, -7207494729 / 2 ^ 79, 1552762561 / 2 ^ 80, -166249661 / 2 ^ 80, 17707527 / 2 ^ 80, -938819 / 2 ^ 79]
  B := [-3951733007166176340017 / 2 ^ 78, 1643481410398429512279 / 2 ^ 80, -169902491774259578987 / 2 ^ 80, 17470502224722348397 / 2 ^ 80, -1787490401685577641 / 2 ^ 80, 182046001042515539 / 2 ^ 80, -18462250872001679 / 2 ^ 80, 932585602668161 / 2 ^ 79, -187777195301139 / 2 ^ 80, 2355699502081 / 2 ^ 77, -1886099118297 / 2 ^ 80, 47074153683 / 2 ^ 78, -4689322901 / 2 ^ 78, 1864935655 / 2 ^ 80, -185110207 / 2 ^ 80, 18347069 / 2 ^ 80, -1816187 / 2 ^ 80]

/-- Segment `[10, 45 / 2 ^ 2]` of `piece0_4`. -/
def seg0_4_0 : Piece where
  a := 10
  b := 45 / 2 ^ 2
  c := 85 / 2 ^ 3
  H := 5 / 2 ^ 3
  A := [1208183052441223628042641 / 2 ^ 80, 68986117961145242783 / 2 ^ 79, -19144917583901520799 / 2 ^ 80, 294064727658984873 / 2 ^ 77, -270064902492011737 / 2 ^ 80, 29667205758718971 / 2 ^ 80, -3159156214123815 / 2 ^ 80, 328661246807827 / 2 ^ 80, -33576781954095 / 2 ^ 80, 422579360895 / 2 ^ 77, -336327743677 / 2 ^ 80, 33127909773 / 2 ^ 80, -3235676841 / 2 ^ 80, 39221493 / 2 ^ 77, -1889991 / 2 ^ 76, 90589 / 2 ^ 75, -276603 / 2 ^ 80]
  B := [-7075371029584411794195 / 2 ^ 79, 659317812455785504261 / 2 ^ 79, -122303594195875179171 / 2 ^ 80, 1411681783968625091 / 2 ^ 77, -259621140101011197 / 2 ^ 78, 23780261524278453 / 2 ^ 78, -4340569501286007 / 2 ^ 79, 197406221028955 / 2 ^ 78, -71602460843815 / 2 ^ 80, 1618654151449 / 2 ^ 78, -291985288655 / 2 ^ 79, 52549120003 / 2 ^ 80, -4718876291 / 2 ^ 80, 422965927 / 2 ^ 80, -37849003 / 2 ^ 80, 845489 / 2 ^ 78, -150901 / 2 ^ 79]

/-- Segment `[45 / 2 ^ 2, 25 / 2 ^ 1]` of `piece0_4`. -/
def seg0_4_1 : Piece where
  a := 45 / 2 ^ 2
  b := 25 / 2 ^ 1
  c := 95 / 2 ^ 3
  H := 5 / 2 ^ 3
  A := [1208329619100977642162619 / 2 ^ 80, 12417430558219202671 / 2 ^ 77, -12373109910171051879 / 2 ^ 80, 341400827893109911 / 2 ^ 78, -35221055433872179 / 2 ^ 78, 869671954082557 / 2 ^ 76, -1332733511388331 / 2 ^ 80, 15593420227501 / 2 ^ 77, -11469388976237 / 2 ^ 80, 519718571013 / 2 ^ 79, -93092989549 / 2 ^ 80, 4127678541 / 2 ^ 79, -725951951 / 2 ^ 80, 31690105 / 2 ^ 79, -5499167 / 2 ^ 80, 474557 / 2 ^ 80, -40759 / 2 ^ 80]
  B := [-12673764176511919812719 / 2 ^ 80, 264680599331538154961 / 2 ^ 78, -22026270717211387101 / 2 ^ 78, 7305212375722178931 / 2 ^ 80, -603608170756201179 / 2 ^ 80, 24855354097145881 / 2 ^ 79, -4081339096100071 / 2 ^ 80, 41764782529155 / 2 ^ 77, -27279081858489 / 2 ^ 80, 1110830191989 / 2 ^ 79, -180521363795 / 2 ^ 80, 7318712501 / 2 ^ 79, -148072685 / 2 ^ 77, 95698441 / 2 ^ 80, -3769 / 2 ^ 69, 155427 / 2 ^ 78, -25005 / 2 ^ 79]

/-- Segment `[25 / 2 ^ 1, 55 / 2 ^ 2]` of `piece0_4`. -/
def seg0_4_2 : Piece where
  a := 25 / 2 ^ 1
  b := 55 / 2 ^ 2
  c := 105 / 2 ^ 3
  H := 5 / 2 ^ 3
  A := [1208436821574592521346637 / 2 ^ 80, 18463918781353785047 / 2 ^ 78, -2085748670933906861 / 2 ^ 78, 835526633251786211 / 2 ^ 80, -9781145646275547 / 2 ^ 77, 3509218875791559 / 2 ^ 79, -610659771217007 / 2 ^ 80, 51939725310547 / 2 ^ 80, -4340313175303 / 2 ^ 80, 357578879727 / 2 ^ 80, -14558454015 / 2 ^ 79, 586953281 / 2 ^ 78, -187743151 / 2 ^ 80, 7452871 / 2 ^ 79, -1176097 / 2 ^ 80, 46147 / 2 ^ 79, -901 / 2 ^ 77]
  B := [-11475093450076908536587 / 2 ^ 80, 868527261334109286005 / 2 ^ 80, -65529076703590626057 / 2 ^ 80, 4928983502253439973 / 2 ^ 80, -369664819261927469 / 2 ^ 80, 27646820404940695 / 2 ^ 80, -1031099254267323 / 2 ^ 79, 38359049593943 / 2 ^ 78, -2847358932553 / 2 ^ 78, 210891358719 / 2 ^ 78, -3896926857 / 2 ^ 76, 4599771157 / 2 ^ 80, -338737133 / 2 ^ 80, 3113093 / 2 ^ 77, -914159 / 2 ^ 79, 67019 / 2 ^ 79, -4907 / 2 ^ 79]

/-- Segment `[55 / 2 ^ 2, 15]` of `piece0_4`. -/
def seg0_4_3 : Piece where
  a := 55 / 2 ^ 2
  b := 15
  c := 115 / 2 ^ 3
  H := 5 / 2 ^ 3
  A := [1208517565402566172353743 / 2 ^ 80, 56379129281126050605 / 2 ^ 80, -2912860203055579015 / 2 ^ 79, 533886412521027533 / 2 ^ 80, -45770071342509049 / 2 ^ 80, 3759173007960043 / 2 ^ 80, -299586346794857 / 2 ^ 80, 11672622369217 / 2 ^ 79, -893832103413 / 2 ^ 79, 67491369711 / 2 ^ 79, -10075223021 / 2 ^ 80, 744773957 / 2 ^ 80, -54602559 / 2 ^ 80, 993701 / 2 ^ 78, -287563 / 2 ^ 80, 5173 / 2 ^ 78, -741 / 2 ^ 79]
  B := [-10483021962610914990263 / 2 ^ 80, 181306150677688266803 / 2 ^ 78, -25018896372098476345 / 2 ^ 79, 215218098128551615 / 2 ^ 76, -236381826659184261 / 2 ^ 80, 2023472061617121 / 2 ^ 77, -553011197716871 / 2 ^ 79, 18850897610199 / 2 ^ 78, -2565019148589 / 2 ^ 79, 174168448661 / 2 ^ 79, -23609057293 / 2 ^ 80, 798689253 / 2 ^ 79, -107903641 / 2 ^ 80, 3638995 / 2 ^ 79, -15319 / 2 ^ 75, 32975 / 2 ^ 80, -277 / 2 ^ 77]

/-- Segment `[15, 67 / 2 ^ 2]` of `piece0_5`. -/
def seg0_5_0 : Piece where
  a := 15
  b := 67 / 2 ^ 2
  c := 127 / 2 ^ 3
  H := 7 / 2 ^ 3
  A := [302147655468175061630713 / 2 ^ 78, 41970954298804368167 / 2 ^ 80, -1966889890117494249 / 2 ^ 79, 163556410576645693 / 2 ^ 79, -25454505140655815 / 2 ^ 80, 1898204618110007 / 2 ^ 80, -137391723946617 / 2 ^ 80, 2431486848951 / 2 ^ 78, -676719166625 / 2 ^ 80, 46437761567 / 2 ^ 80, -3150557845 / 2 ^ 80, 211716445 / 2 ^ 80, -3527987 / 2 ^ 78, 934049 / 2 ^ 80, -30723 / 2 ^ 79, 4021 / 2 ^ 80, -131 / 2 ^ 79]
  B := [-4748616750628655819271 / 2 ^ 79, 595528367592919080085 / 2 ^ 80, -18630158530453132899 / 2 ^ 79, 1163118465111165833 / 2 ^ 79, -72464017316856177 / 2 ^ 79, 9010987165874633 / 2 ^ 80, -559173434764793 / 2 ^ 80, 4329316499327 / 2 ^ 77, -2141393680169 / 2 ^ 80, 8260851455 / 2 ^ 76, -2036251415 / 2 ^ 78, 7830577 / 2 ^ 74, -15395691 / 2 ^ 79, 1889273 / 2 ^ 80, -115773 / 2 ^ 80, 3543 / 2 ^ 79, -433 / 2 ^ 80]

/-- Segment `[67 / 2 ^ 2, 37 / 2 ^ 1]` of `piece0_5`. -/
def seg0_5_1 : Piece where
  a := 67 / 2 ^ 2
  b := 37 / 2 ^ 1
  c := 141 / 2 ^ 3
  H := 7 / 2 ^ 3
  A := [1208653565871849187791937 / 2 ^ 80, 30739594290529216971 / 2 ^ 80, -162429980212089203 / 2 ^ 76, 195003483214555089 / 2 ^ 80, -13696536214605213 / 2 ^ 80, 922174887868923 / 2 ^ 80, -15069811821105 / 2 ^ 78, 3854594458889 / 2 ^ 80, -121159377939 / 2 ^ 79, 7513350505 / 2 ^ 79, -921437037 / 2 ^ 80, 6996663 / 2 ^ 77, -3372985 / 2 ^ 80, 1577 / 2 ^ 73, -12007 / 2 ^ 80, 355 / 2 ^ 79, -21 / 2 ^ 79]
  B := [-4278963630719590019731 / 2 ^ 79, 241878180171753150627 / 2 ^ 79, -13647966802436947897 / 2 ^ 79, 1537442861383615835 / 2 ^ 80, -86446755853845605 / 2 ^ 80, 4852527971276323 / 2 ^ 80, -271944145809211 / 2 ^ 80, 3804064299333 / 2 ^ 78, -425057563731 / 2 ^ 79, 2964119269 / 2 ^ 76, -2642095285 / 2 ^ 80, 1148401 / 2 ^ 73, -4083931 / 2 ^ 79, 453305 / 2 ^ 80, -25129 / 2 ^ 80, 87 / 2 ^ 76, -77 / 2 ^ 80]

/-- Segment `[37 / 2 ^ 1, 81 / 2 ^ 2]` of `piece0_5`. -/
def seg0_5_2 : Piece where
  a := 37 / 2 ^ 1
  b := 81 / 2 ^ 2
  c := 155 / 2 ^ 3
  H := 7 / 2 ^ 3
  A := [604350165654978412963337 / 2 ^ 79, 5794871836253146967 / 2 ^ 78, -1784685076727030805 / 2 ^ 80, 121982155759126947 / 2 ^ 80, -487894701252939 / 2 ^ 76, 478990151327241 / 2 ^ 80, -28539673706537 / 2 ^ 80, 1663837332293 / 2 ^ 80, -95377588587 / 2 ^ 80, 5394103177 / 2 ^ 80, -4714111 / 2 ^ 74, 16718947 / 2 ^ 80, -919189 / 2 ^ 80, 3137 / 2 ^ 76, -681 / 2 ^ 78, 147 / 2 ^ 80, -1 / 2 ^ 77]
  B := [-3893722970016814467911 / 2 ^ 79, 50087021808071215881 / 2 ^ 77, -10293186596121922831 / 2 ^ 79, 1056089149388148341 / 2 ^ 80, -54099184789872177 / 2 ^ 80, 345919554326401 / 2 ^ 77, -70682175500241 / 2 ^ 79, 3605807117845 / 2 ^ 79, -183709324109 / 2 ^ 79, 18695848799 / 2 ^ 80, -475088237 / 2 ^ 79, 3014663 / 2 ^ 76, -2445847 / 2 ^ 80, 61945 / 2 ^ 79, -6269 / 2 ^ 80, 317 / 2 ^ 80, -1 / 2 ^ 76]

/-- Segment `[81 / 2 ^ 2, 22]` of `piece0_5`. -/
def seg0_5_3 : Piece where
  a := 81 / 2 ^ 2
  b := 22
  c := 169 / 2 ^ 3
  H := 7 / 2 ^ 3
  A := [302184004366536059894579 / 2 ^ 78, 4476601063252896533 / 2 ^ 78, -316389629225661623 / 2 ^ 78, 79417845402816783 / 2 ^ 80, -2333566581661327 / 2 ^ 79, 263020697341731 / 2 ^ 80, -1799509025945 / 2 ^ 77, 385545219673 / 2 ^ 79, -40616565965 / 2 ^ 80, 1055520371 / 2 ^ 79, -108525259 / 2 ^ 80, 5528177 / 2 ^ 80, -279411 / 2 ^ 80, 14027 / 2 ^ 80, -175 / 2 ^ 78, 35 / 2 ^ 80, -1 / 2 ^ 79]
  B := [-7144079122738751887977 / 2 ^ 80, 337304104300546109385 / 2 ^ 80, -7952665853582750891 / 2 ^ 79, 187265562025549969 / 2 ^ 78, -35233580372547115 / 2 ^ 80, 413818710575861 / 2 ^ 78, -38836470404369 / 2 ^ 79, 1820281030127 / 2 ^ 79, -170443230839 / 2 ^ 80, 3985547407 / 2 ^ 79, -186194971 / 2 ^ 79, 1086213 / 2 ^ 76, -405149 / 2 ^ 79, 2359 / 2 ^ 76, -439 / 2 ^ 78, 41 / 2 ^ 79, -1 / 2 ^ 78]

/-- Segment `[22, 24]` of `piece0_6`. -/
def seg0_6_0 : Piece where
  a := 22
  b := 24
  c := 23
  H := 1
  A := [1208765614094225423377787 / 2 ^ 80, 3472393469670648419 / 2 ^ 78, -902280269556243743 / 2 ^ 80, 52050869121029783 / 2 ^ 80, -2812417946453973 / 2 ^ 80, 145748945231279 / 2 ^ 80, -7336823858653 / 2 ^ 80, 180737085541 / 2 ^ 79, -17516153315 / 2 ^ 80, 837621399 / 2 ^ 80, -19811433 / 2 ^ 79, 232175 / 2 ^ 77, -675 / 2 ^ 73, 499 / 2 ^ 77, -183 / 2 ^ 80, 1 / 2 ^ 77, 0]
  B := [-3281506829477721672979 / 2 ^ 79, 284722864837774905449 / 2 ^ 80, -6169383624247317237 / 2 ^ 79, 534143076305694955 / 2 ^ 80, -11549330458445475 / 2 ^ 79, 249463623568695 / 2 ^ 78, -21531659395257 / 2 ^ 79, 928297169903 / 2 ^ 79, -79966083731 / 2 ^ 80, 3440998809 / 2 ^ 80, -147932711 / 2 ^ 80, 6354135 / 2 ^ 80, -68173 / 2 ^ 78, 11693 / 2 ^ 80, -501 / 2 ^ 80, 21 / 2 ^ 80, -1 / 2 ^ 80]

/-- Segment `[24, 26]` of `piece0_6`. -/
def seg0_6_1 : Piece where
  a := 24
  b := 26
  c := 25
  H := 1
  A := [1208790159765756236014979 / 2 ^ 80, 5412731425475588463 / 2 ^ 79, -161839758902822249 / 2 ^ 78, 17191296173368059 / 2 ^ 79, -427657422239359 / 2 ^ 78, 10205011172567 / 2 ^ 77, -3785140792617 / 2 ^ 80, 171782354535 / 2 ^ 80, -3834300409 / 2 ^ 79, 337868183 / 2 ^ 80, -14726881 / 2 ^ 80, 318087 / 2 ^ 79, -27273 / 2 ^ 80, 581 / 2 ^ 79, -49 / 2 ^ 80, 1 / 2 ^ 79, 0]
  B := [-6038990038151631665641 / 2 ^ 80, 241110672917539958207 / 2 ^ 80, -9617664843320850593 / 2 ^ 80, 383290698676214631 / 2 ^ 80, -7630753572353165 / 2 ^ 79, 607131544264717 / 2 ^ 80, -12065928503143 / 2 ^ 79, 479179438173 / 2 ^ 79, -19013956947 / 2 ^ 79, 753861621 / 2 ^ 79, -59730185 / 2 ^ 80, 1182219 / 2 ^ 79, -46763 / 2 ^ 79, 3697 / 2 ^ 80, -73 / 2 ^ 79, 3 / 2 ^ 79, 0]

/-- Segment `[26, 28]` of `piece0_6`. -/
def seg0_6_2 : Piece where
  a := 26
  b := 28
  c := 27
  H := 1
  A := [1208809471336397380934705 / 2 ^ 80, 537484496386563765 / 2 ^ 76, -476392721612832591 / 2 ^ 80, 23441606150809827 / 2 ^ 80, -540319432562601 / 2 ^ 79, 11947838179307 / 2 ^ 78, -1026745815923 / 2 ^ 79, 86376677003 / 2 ^ 80, -3574219647 / 2 ^ 80, 145981473 / 2 ^ 80, -5899059 / 2 ^ 80, 236267 / 2 ^ 80, -587 / 2 ^ 76, 371 / 2 ^ 80, -15 / 2 ^ 80, 1 / 2 ^ 80, 0]
  B := [-5592399212794104509039 / 2 ^ 80, 51698866125855252969 / 2 ^ 78, -7640835753434316449 / 2 ^ 80, 70524654876091025 / 2 ^ 78, -2601747073440419 / 2 ^ 78, 95908580203265 / 2 ^ 78, -7065662285297 / 2 ^ 79, 520147496799 / 2 ^ 80, -19131718345 / 2 ^ 80, 703187667 / 2 ^ 80, -12913817 / 2 ^ 79, 947983 / 2 ^ 80, -8693 / 2 ^ 78, 1275 / 2 ^ 80, -47 / 2 ^ 80, 1 / 2 ^ 79, 0]

/-- Segment `[28, 30]` of `piece0_6`. -/
def seg0_6_3 : Piece where
  a := 28
  b := 30
  c := 29
  H := 1
  A := [1208824936920132851162349 / 2 ^ 80, 3472182134510345167 / 2 ^ 79, -358295696321604649 / 2 ^ 80, 16422259822556803 / 2 ^ 80, -705234266251885 / 2 ^ 80, 908022341985 / 2 ^ 75, -1163242886843 / 2 ^ 80, 45592024907 / 2 ^ 80, -1758012047 / 2 ^ 80, 66914227 / 2 ^ 80, -1260039 / 2 ^ 79, 94075 / 2 ^ 80, -1743 / 2 ^ 79, 1 / 2 ^ 73, -5 / 2 ^ 80, 0, 0]
  B := [-1301817478936904617403 / 2 ^ 78, 89656236881337774605 / 2 ^ 79, -6170394305324552035 / 2 ^ 80, 106093746353196305 / 2 ^ 79, -455736662275163 / 2 ^ 76, 31301754994505 / 2 ^ 77, -8594044098793 / 2 ^ 80, 294750554883 / 2 ^ 80, -5051311355 / 2 ^ 79, 173025731 / 2 ^ 79, -11846203 / 2 ^ 80, 12665 / 2 ^ 75, -13857 / 2 ^ 80, 237 / 2 ^ 79, -1 / 2 ^ 76, 1 / 2 ^ 80, 0]

theorem segs_0_ok :
    segOk (piece0_0, seg0_0_0) = true ∧ segOk (piece0_0, seg0_0_1) = true ∧ segOk (piece0_0, seg0_0_2) = true ∧ segOk (piece0_0, seg0_0_3) = true := by
  decide +kernel

theorem segs_1_ok :
    segOk (piece0_1, seg0_1_0) = true ∧ segOk (piece0_1, seg0_1_1) = true ∧ segOk (piece0_1, seg0_1_2) = true ∧ segOk (piece0_1, seg0_1_3) = true := by
  decide +kernel

theorem segs_2_ok :
    segOk (piece0_2, seg0_2_0) = true ∧ segOk (piece0_2, seg0_2_1) = true ∧ segOk (piece0_2, seg0_2_2) = true ∧ segOk (piece0_2, seg0_2_3) = true := by
  decide +kernel

theorem segs_3_ok :
    segOk (piece0_3, seg0_3_0) = true ∧ segOk (piece0_3, seg0_3_1) = true ∧ segOk (piece0_3, seg0_3_2) = true := by
  decide +kernel

theorem segs_4_ok :
    segOk (piece0_4, seg0_4_0) = true ∧ segOk (piece0_4, seg0_4_1) = true ∧ segOk (piece0_4, seg0_4_2) = true ∧ segOk (piece0_4, seg0_4_3) = true := by
  decide +kernel

theorem segs_5_ok :
    segOk (piece0_5, seg0_5_0) = true ∧ segOk (piece0_5, seg0_5_1) = true ∧ segOk (piece0_5, seg0_5_2) = true ∧ segOk (piece0_5, seg0_5_3) = true := by
  decide +kernel

theorem segs_6_ok :
    segOk (piece0_6, seg0_6_0) = true ∧ segOk (piece0_6, seg0_6_1) = true ∧ segOk (piece0_6, seg0_6_2) = true ∧ segOk (piece0_6, seg0_6_3) = true := by
  decide +kernel

/-- Hankel's expansion truncated to degree 26 with dyadic coefficients. -/
def casym : AsymPiece where
  X := asym.X
  A := [1, 0, -9 / 2 ^ 7, 0, 3675 / 2 ^ 15, 0, -2401245 / 2 ^ 22, 0, 13043905875 / 2 ^ 31, 0, -3780160155647 / 2 ^ 35, 0, 815531211669 / 2 ^ 28, 0, -124611121651 / 2 ^ 20, 0, 25612089317 / 2 ^ 12, 0, -851878433 / 2 ^ 1, 0, 36468400800, 0, -3833534660608, 0, 485401468862464, 0, -72868573520855040]
  B := [0, -1 / 2 ^ 3, 0, 75 / 2 ^ 10, 0, -59535 / 2 ^ 18, 0, 57972915 / 2 ^ 25, 0, -418854310875 / 2 ^ 34, 0, 2367969642955 / 2 ^ 32, 0, -306314307267 / 2 ^ 24, 0, 13645566837 / 2 ^ 14, 0, -1602226865 / 2 ^ 5, 0, 3836255180, 0, -364901081856, 0, 42189715734528, 0, -5827244626804736, 0]
  m := asym.m

theorem asym_close : absSum (1 / asym.X) (subP asym.A casym.A) ≤ 1 / 2 ^ 72 ∧
    absSum (1 / asym.X) (subP asym.B casym.B) ≤ 1 / 2 ^ 72 := by
  decide +kernel

theorem near_seg (q : Piece × Piece) (hq : segOk q = true) (hpc : q.1 ∈ pieces ++ [last]) (x : ℝ)
    (hx : x ∈ Icc (q.2.a : ℝ) q.2.b) :
    |P0 x - q.2.fA x| ≤ 1 / 2 ^ 70 ∧ |Q0 x - q.2.fB x| ≤ 1 / 2 ^ 70 := by
  simp only [segOk, Bool.and_eq_true, decide_eq_true_eq] at hq
  obtain ⟨⟨⟨hok, hab⟩, hA⟩, hB⟩ := hq
  obtain ⟨-, -, hca, hbc⟩ := ok_facts hok
  have ha : (q.1.a : ℝ) ≤ q.2.a := by exact_mod_cast hab.1
  have hb' : (q.2.b : ℝ) ≤ q.1.b := by exact_mod_cast hab.2
  have hb := pieces_bound q.1 hpc x ⟨ha.trans hx.1, hx.2.trans hb'⟩
  have hH : (0 : ℚ) ≤ q.2.H := by
    exact_mod_cast (by linarith [hx.1, hx.2] : (0 : ℝ) ≤ q.2.H)
  have hxc : |x - q.2.c| ≤ ((q.2.H : ℚ) : ℝ) := by
    rw [abs_le]; constructor <;> linarith [hx.1, hx.2]
  have eA := abs_eval_le q.2.H hH (subP (shift (q.2.c - q.1.c) q.1.A) q.2.A) (x - q.2.c) hxc
  have eB := abs_eval_le q.2.H hH (subP (shift (q.2.c - q.1.c) q.1.B) q.2.B) (x - q.2.c) hxc
  have hd : (((q.2.c - q.1.c : ℚ)) : ℝ) + (x - q.2.c) = x - q.1.c := by push_cast; ring
  rw [eval_subP, eval_shift, hd] at eA eB
  have cA : ((absSum q.2.H (subP (shift (q.2.c - q.1.c) q.1.A) q.2.A) : ℚ) : ℝ) ≤ 1 / 2 ^ 71 :=
    le_trans (Rat.cast_le.mpr hA) (by norm_num)
  have cB : ((absSum q.2.H (subP (shift (q.2.c - q.1.c) q.1.B) q.2.B) : ℚ) : ℝ) ≤ 1 / 2 ^ 71 :=
    le_trans (Rat.cast_le.mpr hB) (by norm_num)
  have f1 : q.1.fA x = eval q.1.A (x - q.1.c) := rfl
  have f2 : q.1.fB x = eval q.1.B (x - q.1.c) := rfl
  have g1 : q.2.fA x = eval q.2.A (x - q.2.c) := rfl
  have g2 : q.2.fB x = eval q.2.B (x - q.2.c) := rfl
  constructor
  · calc |P0 x - q.2.fA x| ≤ |P0 x - q.1.fA x| + |q.1.fA x - q.2.fA x| := abs_sub_le _ _ _
      _ ≤ 1 / 2 ^ 80 + 1 / 2 ^ 71 := by
          have hb1 : |P0 x - eval q.1.A (x - q.1.c)| ≤ 1 / 2 ^ 80 := hb.1
          rw [f1, g1]; linarith
      _ ≤ 1 / 2 ^ 70 := by norm_num
  · calc |Q0 x - q.2.fB x| ≤ |Q0 x - q.1.fB x| + |q.1.fB x - q.2.fB x| := abs_sub_le _ _ _
      _ ≤ 1 / 2 ^ 80 + 1 / 2 ^ 71 := by
          have hb2 : |Q0 x - eval q.1.B (x - q.1.c)| ≤ 1 / 2 ^ 80 := hb.2
          rw [f2, g2]; linarith
      _ ≤ 1 / 2 ^ 70 := by norm_num

theorem near_asym (x : ℝ) (hx : 30 ≤ x) :
    |P0 x - casym.fA x| ≤ 1 / 2 ^ 70 ∧ |Q0 x - casym.fB x| ≤ 1 / 2 ^ 70 := by
  obtain ⟨hA, hB⟩ := asym_close
  have hb := asym_bound x hx
  have hX : ((asym.X : ℚ) : ℝ) = 30 := by norm_num [asym]
  have ht : |1 / x| ≤ ((1 / asym.X : ℚ) : ℝ) := by
    rw [abs_of_pos (by positivity)]; push_cast; rw [hX]
    exact one_div_le_one_div_of_le (by norm_num) hx
  have h0 : (0 : ℚ) ≤ 1 / asym.X := by norm_num [asym]
  have eA := abs_eval_le _ h0 (subP asym.A casym.A) (1 / x) ht
  have eB := abs_eval_le _ h0 (subP asym.B casym.B) (1 / x) ht
  rw [eval_subP] at eA eB
  have cA : ((absSum (1 / asym.X) (subP asym.A casym.A) : ℚ) : ℝ) ≤ 1 / 2 ^ 72 :=
    le_trans (Rat.cast_le.mpr hA) (by norm_num)
  have cB : ((absSum (1 / asym.X) (subP asym.B casym.B) : ℚ) : ℝ) ≤ 1 / 2 ^ 72 :=
    le_trans (Rat.cast_le.mpr hB) (by norm_num)
  constructor
  · calc |P0 x - casym.fA x| ≤ |P0 x - asym.fA x| + |asym.fA x - casym.fA x| := abs_sub_le _ _ _
      _ ≤ 1 / 2 ^ 80 + 1 / 2 ^ 72 := by
          have hb1 : |P0 x - eval asym.A (1 / x)| ≤ 1 / 2 ^ 80 := hb.1
          simp only [AsymPiece.fA]; linarith
      _ ≤ 1 / 2 ^ 70 := by norm_num
  · calc |Q0 x - casym.fB x| ≤ |Q0 x - asym.fB x| + |asym.fB x - casym.fB x| := abs_sub_le _ _ _
      _ ≤ 1 / 2 ^ 80 + 1 / 2 ^ 72 := by
          have hb2 : |Q0 x - eval asym.B (1 / x)| ≤ 1 / 2 ^ 80 := hb.2
          simp only [AsymPiece.fB]; linarith
      _ ≤ 1 / 2 ^ 70 := by norm_num

/-- One segment of a comparison with `pFd R S`. -/
theorem p_step (q : Piece × Piece) (hq : segOk q = true) (hpc : q.1 ∈ pieces ++ [last])
    (R S : List ℚ) (hR : R.length ≤ S.length + 1) (lo hi : ℚ) (sE sW e : ℕ) (L H : ℤ) (t : ℕ)
    (hs : isScaled sE (pE q.2 R S) = true ∧ isScaled sW (sTilde q.2.c S) = true)
    (hc : ratioCheckI (toInt sE (pE q.2 R S)) (toInt sW (sTilde q.2.c S)) sE sW 68 e L H t 12 = true)
    (hend : (L : ℚ) / 2 ^ t = lo - q.2.c ∧ (H : ℚ) / 2 ^ t = hi - q.2.c)
    (hsub : 0 < lo ∧ q.2.a ≤ lo ∧ hi ≤ q.2.b) (x : ℝ) (hx : x ∈ Icc (lo : ℝ) hi) :
    |P0 x - pFd R S x| ≤ (e : ℝ) / 2 ^ 68 + 1 / 2 ^ 70 := by
  have hs' : (0 : ℝ) < lo ∧ (q.2.a : ℝ) ≤ lo ∧ (hi : ℝ) ≤ q.2.b := by
    obtain ⟨h1, h2, h3⟩ := hsub
    exact ⟨by exact_mod_cast h1, by exact_mod_cast h2, by exact_mod_cast h3⟩
  have h1 := (near_seg q hq hpc x ⟨hs'.2.1.trans hx.1, hx.2.trans hs'.2.2⟩).1
  have h2 := p_piece q.2 R S hR sE sW 68 e L H t 12 hs.1 hs.2 hc x
    (ends lo q.2.c L t hend.1 x hx.1) (ends' hi q.2.c H t hend.2 x hx.2) (lt_of_lt_of_le hs'.1 hx.1)
  calc |P0 x - pFd R S x| ≤ |P0 x - q.2.fA x| + |q.2.fA x - pFd R S x| := abs_sub_le _ _ _
    _ ≤ (e : ℝ) / 2 ^ 68 + 1 / 2 ^ 70 := by linarith

/-- One segment of a comparison with `qFd q₀ R S`. -/
theorem q_step (q : Piece × Piece) (hq : segOk q = true) (hpc : q.1 ∈ pieces ++ [last])
    (R S : List ℚ) (hR : R.length ≤ S.length + 1) (lo hi : ℚ) (sE sW e : ℕ) (L H : ℤ) (t : ℕ)
    (hs : isScaled sE (qE (-1 / 8) q.2 R S) = true ∧ isScaled sW (qW q.2 S) = true)
    (hc : ratioCheckI (toInt sE (qE (-1 / 8) q.2 R S)) (toInt sW (qW q.2 S)) sE sW 68 e L H t 12 = true)
    (hend : (L : ℚ) / 2 ^ t = lo - q.2.c ∧ (H : ℚ) / 2 ^ t = hi - q.2.c)
    (hsub : 0 < lo ∧ q.2.a ≤ lo ∧ hi ≤ q.2.b) (x : ℝ) (hx : x ∈ Icc (lo : ℝ) hi) :
    |Q0 x - qFd (-1 / 8) R S x| ≤ (e : ℝ) / 2 ^ 68 + 1 / 2 ^ 70 := by
  have hs' : (0 : ℝ) < lo ∧ (q.2.a : ℝ) ≤ lo ∧ (hi : ℝ) ≤ q.2.b := by
    obtain ⟨h1, h2, h3⟩ := hsub
    exact ⟨by exact_mod_cast h1, by exact_mod_cast h2, by exact_mod_cast h3⟩
  have h1 := (near_seg q hq hpc x ⟨hs'.2.1.trans hx.1, hx.2.trans hs'.2.2⟩).2
  have h2 := q_piece (-1 / 8) q.2 R S hR sE sW 68 e L H t 12 hs.1 hs.2 hc x
    (ends lo q.2.c L t hend.1 x hx.1) (ends' hi q.2.c H t hend.2 x hx.2) (lt_of_lt_of_le hs'.1 hx.1)
  calc |Q0 x - qFd (-1 / 8) R S x| ≤ |Q0 x - q.2.fB x| + |q.2.fB x - qFd (-1 / 8) R S x| := abs_sub_le _ _ _
    _ ≤ (e : ℝ) / 2 ^ 68 + 1 / 2 ^ 70 := by linarith

theorem p_asym_step (R S : List ℚ) (sE sW e : ℕ)
    (hs : isScaled sE (pEa casym R S) = true ∧ isScaled sW (sAsym S) = true)
    (hc : ratioCheckI (toInt sE (pEa casym R S)) (toInt sW (sAsym S)) sE sW 68 e 0 35 10 12 = true)
    (x : ℝ) (hx : 30 ≤ x) : |P0 x - pFd R S x| ≤ (e : ℝ) / 2 ^ 68 + 1 / 2 ^ 70 := by
  have h1 := (near_asym x hx).1
  have h2 := p_asym casym R S sE sW 68 e 35 10 12 hs.1 hs.2 hc x (by linarith) (one_div_le x hx)
  calc |P0 x - pFd R S x| ≤ |P0 x - casym.fA x| + |casym.fA x - pFd R S x| := abs_sub_le _ _ _
    _ ≤ (e : ℝ) / 2 ^ 68 + 1 / 2 ^ 70 := by linarith

theorem q_asym_step (R S : List ℚ) (sE sW e : ℕ)
    (hs : isScaled sE (qEa (-1 / 8) casym R S) = true ∧ isScaled sW (sAsym S) = true)
    (hc : ratioCheckI (toInt sE (qEa (-1 / 8) casym R S)) (toInt sW (sAsym S)) sE sW 68 e 0 35 10 12 = true)
    (x : ℝ) (hx : 30 ≤ x) : |Q0 x - qFd (-1 / 8) R S x| ≤ (e : ℝ) / 2 ^ 68 + 1 / 2 ^ 70 := by
  have h1 := (near_asym x hx).2
  have h2 := q_asym (-1 / 8) casym R S sE sW 68 e 35 10 12 hs.1 hs.2 hc x (by linarith) (one_div_le x hx)
  calc |Q0 x - qFd (-1 / 8) R S x| ≤ |Q0 x - casym.fB x| + |casym.fB x - qFd (-1 / 8) R S x| := abs_sub_le _ _ _
    _ ≤ (e : ℝ) / 2 ^ 68 + 1 / 2 ^ 70 := by linarith

#print axioms near_seg
#print axioms near_asym
#print axioms p_step
#print axioms q_step
#print axioms p_asym_step
#print axioms q_asym_step

end LeanExe.ProofKit.BesselSeg0