BesselSeg1.lean

import LeanExe.ProofKit.BesselLarge1
import LeanExe.ProofKit.BesselRatio

/-!
Short polynomials for comparing `P1` and `Q1` with fdlibm's rational approximations.  Each piece of
`BesselLarge1` 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
`BesselLarge1`, `P1` and `Q1` 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.BesselSeg1

open Set PolyBound PolyCalc BesselPQ BesselChain BesselRatio BesselLarge1

/-- Segment `[2, 9 / 2 ^ 2]` of `piece1_0`. -/
def seg1_0_0 : Piece where
  a := 2
  b := 9 / 2 ^ 2
  c := 17 / 2 ^ 3
  H := 1 / 2 ^ 3
  A := [1235266005781853363600467 / 2 ^ 80, -10821448007712330176917 / 2 ^ 79, 13142616984189048259601 / 2 ^ 80, -7050091812828184870269 / 2 ^ 80, 1772047679118013667267 / 2 ^ 79, -1716178352547648966355 / 2 ^ 80, 812570661405124980787 / 2 ^ 80, -189754104438549326271 / 2 ^ 79, 175785759239772907547 / 2 ^ 80, -81024283653720732325 / 2 ^ 80, 4655370309370016411 / 2 ^ 77, -8547337365012568051 / 2 ^ 79, 7842228192210819891 / 2 ^ 80, -224851593938514615 / 2 ^ 76, 1650960263765215067 / 2 ^ 80, -379018021953837067 / 2 ^ 79, 348278328495229489 / 2 ^ 80]
  B := [102082137449563494857403 / 2 ^ 79, -2795000846705649413861 / 2 ^ 75, 4824714336521096278293 / 2 ^ 77, -4139187989390313301389 / 2 ^ 78, 221928927281459128075 / 2 ^ 75, -1528518383789944271257 / 2 ^ 79, 1323192240661696468677 / 2 ^ 80, -576334333859057072021 / 2 ^ 80, 252634779745926887713 / 2 ^ 80, -55707676926708523741 / 2 ^ 79, 24704916631925527253 / 2 ^ 79, -5505447880824727537 / 2 ^ 78, 9858688151745540429 / 2 ^ 80, -4430843008473444595 / 2 ^ 80, 249782179150485575 / 2 ^ 77, -451966594507834835 / 2 ^ 79, 205001337225735071 / 2 ^ 79]

/-- Segment `[9 / 2 ^ 2, 5 / 2 ^ 1]` of `piece1_0`. -/
def seg1_0_1 : Piece where
  a := 9 / 2 ^ 2
  b := 5 / 2 ^ 1
  c := 19 / 2 ^ 3
  H := 1 / 2 ^ 3
  A := [1230578883445226595783995 / 2 ^ 80, -8100652168471928917651 / 2 ^ 79, 4478402872316311065153 / 2 ^ 79, -4368378366474516030367 / 2 ^ 80, 1992826392405652925539 / 2 ^ 80, -873937192719759075675 / 2 ^ 80, 187002981261820803463 / 2 ^ 79, -157604512356513953877 / 2 ^ 80, 16441398033745880849 / 2 ^ 78, -6818435866820011115 / 2 ^ 78, 11267721438983904581 / 2 ^ 80, -2322310642271827895 / 2 ^ 79, 956102822036251171 / 2 ^ 79, -393417708064068143 / 2 ^ 79, 323736560945849653 / 2 ^ 80, -133224415140216933 / 2 ^ 80, 54845405013128059 / 2 ^ 80]
  B := [91991486556727770730499 / 2 ^ 79, -18213633191740347444443 / 2 ^ 78, 14216429668088179603335 / 2 ^ 79, -11019127658170366527833 / 2 ^ 80, 4263263807259461409159 / 2 ^ 80, -1652390890191306335483 / 2 ^ 80, 321459069402138818517 / 2 ^ 79, -251379747122765122903 / 2 ^ 80, 6175656388893945705 / 2 ^ 76, -39044371046048275623 / 2 ^ 80, 15505196847494710939 / 2 ^ 80, -6185717568879518263 / 2 ^ 80, 619511770112332575 / 2 ^ 78, -498218463614077019 / 2 ^ 79, 201004847389400475 / 2 ^ 79, -40667870274507925 / 2 ^ 78, 65998428387568659 / 2 ^ 80]

/-- Segment `[5 / 2 ^ 1, 11 / 2 ^ 2]` of `piece1_0`. -/
def seg1_0_2 : Piece where
  a := 5 / 2 ^ 1
  b := 11 / 2 ^ 2
  c := 21 / 2 ^ 3
  H := 1 / 2 ^ 3
  A := [1227027115431696922906853 / 2 ^ 80, -12432538994419558957573 / 2 ^ 80, 6310357980208906966555 / 2 ^ 80, -2823323868592653835055 / 2 ^ 80, 147496132809135185329 / 2 ^ 77, -236667457112923333529 / 2 ^ 79, 185000202392710185625 / 2 ^ 80, -35546690991110467597 / 2 ^ 79, 13509128082940563831 / 2 ^ 79, -10193227139620183817 / 2 ^ 80, 3827363534463066041 / 2 ^ 80, -716374276363396051 / 2 ^ 79, 535342195662550453 / 2 ^ 80, -3122130954140987 / 2 ^ 74, 74542700050959783 / 2 ^ 80, -27804428736000627 / 2 ^ 80, 5186038694661625 / 2 ^ 79]
  B := [167389402463502285316827 / 2 ^ 80, -15116656973406234794509 / 2 ^ 78, 10771083169686032140469 / 2 ^ 79, -238042554702742258915 / 2 ^ 75, 167871159344466152869 / 2 ^ 76, -473743325381067868975 / 2 ^ 79, 335074908149752224267 / 2 ^ 80, -29735064243334229721 / 2 ^ 78, 42402362640377425001 / 2 ^ 80, -15184501106431832425 / 2 ^ 80, 5461629090779096749 / 2 ^ 80, -246582512902582909 / 2 ^ 77, 178811642016729793 / 2 ^ 78, -260247487738150951 / 2 ^ 80, 94994720630296669 / 2 ^ 80, -34774226169965669 / 2 ^ 80, 12762471347613317 / 2 ^ 80]

/-- Segment `[11 / 2 ^ 2, 3]` of `piece1_0`. -/
def seg1_0_3 : Piece where
  a := 11 / 2 ^ 2
  b := 3
  c := 23 / 2 ^ 3
  H := 1 / 2 ^ 3
  A := [1224273451838020246884903 / 2 ^ 80, -608828473293056781649 / 2 ^ 76, 1142735359593112371439 / 2 ^ 78, -1889803016701534228655 / 2 ^ 80, 364581703363980029441 / 2 ^ 79, -269717939498756554619 / 2 ^ 80, 48543065787842837745 / 2 ^ 79, -34318609990282124043 / 2 ^ 80, 11983608744743464191 / 2 ^ 80, -2074968851631497837 / 2 ^ 79, 1429084815688321915 / 2 ^ 80, -15321185798306911 / 2 ^ 75, 167785763485649959 / 2 ^ 80, -57330800293535243 / 2 ^ 80, 19571108336920127 / 2 ^ 80, -6677740030594197 / 2 ^ 80, 1139028270403591 / 2 ^ 79]
  B := [9594359463512763350591 / 2 ^ 76, -6371581952555165441227 / 2 ^ 77, 8352890578394455318057 / 2 ^ 79, -5433109761586291181087 / 2 ^ 80, 880319277888313040681 / 2 ^ 79, -570203257753844366647 / 2 ^ 80, 184932035656195378975 / 2 ^ 80, -60141852111954488313 / 2 ^ 80, 19626331532641658271 / 2 ^ 80, -6428977248603791761 / 2 ^ 80, 264254268935881851 / 2 ^ 77, -174438993821118669 / 2 ^ 78, 231115276496206315 / 2 ^ 80, -76803018055881147 / 2 ^ 80, 25599769931484033 / 2 ^ 80, -1069538769931795 / 2 ^ 77, 1433474338832845 / 2 ^ 79]

/-- Segment `[3, 27 / 2 ^ 3]` of `piece1_1`. -/
def seg1_1_0 : Piece where
  a := 3
  b := 27 / 2 ^ 3
  c := 51 / 2 ^ 4
  H := 3 / 2 ^ 4
  A := [610812124848061456790955 / 2 ^ 79, -460024073661786645013 / 2 ^ 76, 789049638432986323569 / 2 ^ 78, -1192224783385207561231 / 2 ^ 80, 419969441138907997019 / 2 ^ 80, -141673052152574619521 / 2 ^ 80, 46450876650541293243 / 2 ^ 80, -466813700149755659 / 2 ^ 75, 1184983893274938081 / 2 ^ 78, -186249649541129291 / 2 ^ 77, 465319958408452347 / 2 ^ 80, -9040880633140083 / 2 ^ 76, 44826472841883807 / 2 ^ 80, -13861227785322367 / 2 ^ 80, 4280036743000683 / 2 ^ 80, -1320381090155383 / 2 ^ 80, 407118709999195 / 2 ^ 80]
  B := [139061662890978010274613 / 2 ^ 80, -1310393304649305675623 / 2 ^ 75, 3123248893410496155827 / 2 ^ 78, -3693514452534075674355 / 2 ^ 80, 543698704950547873243 / 2 ^ 79, -319644633268535535113 / 2 ^ 80, 23499130525529943531 / 2 ^ 78, -6921968967319349829 / 2 ^ 78, 4088175501666838343 / 2 ^ 79, -605428270276646315 / 2 ^ 78, 359780609993856731 / 2 ^ 79, -214489770007597775 / 2 ^ 80, 32067981925875879 / 2 ^ 79, -19234716097664727 / 2 ^ 80, 5784639874077009 / 2 ^ 80, -1744151635898559 / 2 ^ 80, 131783235650617 / 2 ^ 78]

/-- Segment `[27 / 2 ^ 3, 15 / 2 ^ 2]` of `piece1_1`. -/
def seg1_1_1 : Piece where
  a := 27 / 2 ^ 3
  b := 15 / 2 ^ 2
  c := 57 / 2 ^ 4
  H := 3 / 2 ^ 4
  A := [1219252444147646294271181 / 2 ^ 80, -5419816060223720913173 / 2 ^ 80, 526589309884031842091 / 2 ^ 78, -45073492268281458481 / 2 ^ 76, 115071071391837366883 / 2 ^ 79, -35136315358496190475 / 2 ^ 79, 2604148405865938127 / 2 ^ 77, -756379543799923899 / 2 ^ 77, 1732204512928770419 / 2 ^ 80, -490733653237307029 / 2 ^ 80, 68991948401109723 / 2 ^ 79, -38587935637960353 / 2 ^ 80, 5374563543287277 / 2 ^ 79, -2985902793572263 / 2 ^ 80, 827779063270797 / 2 ^ 80, -229167228034963 / 2 ^ 80, 63384770266189 / 2 ^ 80]
  B := [124918364258623703577161 / 2 ^ 80, -16959784544001410654081 / 2 ^ 79, 142357000944977035195 / 2 ^ 74, -2429037687844341717463 / 2 ^ 80, 644646635170831177007 / 2 ^ 80, -170692743867797308917 / 2 ^ 80, 45172245383053636043 / 2 ^ 80, -11963051298615135923 / 2 ^ 80, 396656548213338087 / 2 ^ 77, -210883344823088143 / 2 ^ 78, 112394263492036557 / 2 ^ 79, -60059799511710261 / 2 ^ 80, 16089487888581381 / 2 ^ 80, -4321400966104911 / 2 ^ 80, 290886858762269 / 2 ^ 78, -157011428133867 / 2 ^ 79, 84935724158375 / 2 ^ 80]

/-- Segment `[15 / 2 ^ 2, 33 / 2 ^ 3]` of `piece1_1`. -/
def seg1_1_2 : Piece where
  a := 15 / 2 ^ 2
  b := 33 / 2 ^ 3
  c := 63 / 2 ^ 4
  H := 3 / 2 ^ 4
  A := [1217482271115109185063391 / 2 ^ 80, -512734357519783941151 / 2 ^ 77, 364378754433951874251 / 2 ^ 78, -456379398648714701871 / 2 ^ 80, 66582986785691802759 / 2 ^ 79, -18579450637001595577 / 2 ^ 79, 10059898923126408257 / 2 ^ 80, -666510656009376329 / 2 ^ 78, 347881217168104025 / 2 ^ 79, -22442691880280395 / 2 ^ 77, 11486788426849067 / 2 ^ 78, -5843126631892323 / 2 ^ 79, 2958727046683205 / 2 ^ 80, -93319475566815 / 2 ^ 77, 93951598478467 / 2 ^ 79, -23603831548915 / 2 ^ 79, 740284063269 / 2 ^ 76]
  B := [113363241668495081466595 / 2 ^ 80, -27990279899636447924031 / 2 ^ 80, 6843842912608643870047 / 2 ^ 80, -1661596428562349000677 / 2 ^ 80, 401520502491294674377 / 2 ^ 80, -96760072577812922539 / 2 ^ 80, 23289844673661090315 / 2 ^ 80, -5605763106339095387 / 2 ^ 80, 1350447457905966605 / 2 ^ 80, -162902385686828985 / 2 ^ 79, 19687211555455361 / 2 ^ 78, -19073813869655891 / 2 ^ 80, 578754701144643 / 2 ^ 77, -1126404906820871 / 2 ^ 80, 68657986260243 / 2 ^ 78, -33549849194797 / 2 ^ 79, 1026689806845 / 2 ^ 76]

/-- Segment `[33 / 2 ^ 3, 9 / 2 ^ 1]` of `piece1_1`. -/
def seg1_1_3 : Piece where
  a := 33 / 2 ^ 3
  b := 9 / 2 ^ 1
  c := 69 / 2 ^ 4
  H := 3 / 2 ^ 4
  A := [152015918437539070217201 / 2 ^ 77, -794114292550971322211 / 2 ^ 78, 259867130020367240617 / 2 ^ 78, -74967071462351742591 / 2 ^ 78, 40305545672027281831 / 2 ^ 79, -20717009037067089301 / 2 ^ 80, 5163018661172313289 / 2 ^ 80, -1258802385218367227 / 2 ^ 80, 302025194782516345 / 2 ^ 80, -71605372624725207 / 2 ^ 80, 8412455013328609 / 2 ^ 79, -3926579026287305 / 2 ^ 80, 113959757222123 / 2 ^ 77, -210849424595413 / 2 ^ 80, 48620292194127 / 2 ^ 80, -11186436650997 / 2 ^ 80, 1284717185955 / 2 ^ 79]
  B := [51874480473092765618323 / 2 ^ 79, -11741158972476594433575 / 2 ^ 79, 1317108424604836634053 / 2 ^ 78, -587103757797066163483 / 2 ^ 79, 260480990311137175013 / 2 ^ 80, -28805111211238225355 / 2 ^ 79, 12720733318620446789 / 2 ^ 80, -701823017137923035 / 2 ^ 78, 619709998845511903 / 2 ^ 80, -68462307939432849 / 2 ^ 79, 15146897711530287 / 2 ^ 79, -6713175677016843 / 2 ^ 80, 1490313884364635 / 2 ^ 80, -82866413371947 / 2 ^ 78, 36930781007835 / 2 ^ 79, -16489454059213 / 2 ^ 80, 3687885212407 / 2 ^ 80]

/-- Segment `[9 / 2 ^ 1, 41 / 2 ^ 3]` of `piece1_2`. -/
def seg1_2_0 : Piece where
  a := 9 / 2 ^ 1
  b := 41 / 2 ^ 3
  c := 77 / 2 ^ 4
  H := 5 / 2 ^ 4
  A := [1214765965188593827350975 / 2 ^ 80, -581802837324260230195 / 2 ^ 78, 344407646177558651853 / 2 ^ 79, -5619892635282918289 / 2 ^ 75, 43758635324361018803 / 2 ^ 80, -1272185916631274015 / 2 ^ 77, 1147240459083322639 / 2 ^ 79, -505780936916017351 / 2 ^ 80, 109645479715600087 / 2 ^ 80, -2933911026905699 / 2 ^ 77, 4976075074508761 / 2 ^ 80, -1047126760125091 / 2 ^ 80, 219079079506191 / 2 ^ 80, -22814981307251 / 2 ^ 79, 2367660594853 / 2 ^ 78, -1960317036815 / 2 ^ 80, 25306688739 / 2 ^ 76]
  B := [46596396605370833717299 / 2 ^ 79, -18980190047180218743805 / 2 ^ 80, 3836151836433353970825 / 2 ^ 80, -192670199325071081999 / 2 ^ 78, 19266618437023043809 / 2 ^ 77, -15364356059333797661 / 2 ^ 79, 6113959699168469421 / 2 ^ 80, -303798252802402297 / 2 ^ 78, 120730086304897533 / 2 ^ 79, -47993471888434849 / 2 ^ 80, 1193327403416619 / 2 ^ 77, -1901025230279639 / 2 ^ 80, 23690418617637 / 2 ^ 76, -75687559646369 / 2 ^ 80, 15136177924559 / 2 ^ 80, -3031657606711 / 2 ^ 80, 304076825673 / 2 ^ 79]

/-- Segment `[41 / 2 ^ 3, 23 / 2 ^ 2]` of `piece1_2`. -/
def seg1_2_1 : Piece where
  a := 41 / 2 ^ 3
  b := 23 / 2 ^ 2
  c := 87 / 2 ^ 4
  H := 5 / 2 ^ 4
  A := [606771223882957764938403 / 2 ^ 79, -1640839696728526982411 / 2 ^ 80, 433728371711654787729 / 2 ^ 80, -25301637907713184201 / 2 ^ 78, 22016991064008264951 / 2 ^ 80, -2289144678853870079 / 2 ^ 79, 461299611778713625 / 2 ^ 79, -45427398186649773 / 2 ^ 78, 35177302553210945 / 2 ^ 80, -840067554943743 / 2 ^ 77, 79424453250335 / 2 ^ 76, -238357427950079 / 2 ^ 80, 22211142312495 / 2 ^ 79, -2059213256043 / 2 ^ 78, 1521102801467 / 2 ^ 80, -279993660887 / 2 ^ 80, 51405992315 / 2 ^ 80]
  B := [2583169662671748718327 / 2 ^ 75, -14958010957860004727157 / 2 ^ 80, 336157564874254075713 / 2 ^ 77, -240466655923564501821 / 2 ^ 79, 85648167835071968237 / 2 ^ 80, -15204888869139528209 / 2 ^ 80, 168329988737222619 / 2 ^ 76, -238192914802837983 / 2 ^ 79, 84198770345239785 / 2 ^ 80, -7439257449565253 / 2 ^ 79, 2629718343501397 / 2 ^ 80, -465051231539373 / 2 ^ 80, 20577074764559 / 2 ^ 78, -3645493375399 / 2 ^ 78, 323282530575 / 2 ^ 77, -28702822223 / 2 ^ 76, 40824487253 / 2 ^ 79]

/-- Segment `[23 / 2 ^ 2, 51 / 2 ^ 3]` of `piece1_2`. -/
def seg1_2_2 : Piece where
  a := 23 / 2 ^ 2
  b := 51 / 2 ^ 3
  c := 97 / 2 ^ 4
  H := 5 / 2 ^ 4
  A := [1212664611329989951087835 / 2 ^ 80, -1198811310013947532041 / 2 ^ 80, 143094777460864996605 / 2 ^ 79, -60354464225816896799 / 2 ^ 80, 11871389955758569911 / 2 ^ 80, -279040053420447533 / 2 ^ 77, 50846953631074559 / 2 ^ 77, -36215127825726179 / 2 ^ 79, 1584083139619385 / 2 ^ 77, -1093634984007103 / 2 ^ 79, 373485622971019 / 2 ^ 80, -15807669720925 / 2 ^ 78, 10631501528919 / 2 ^ 80, -1777655353243 / 2 ^ 80, 147949115443 / 2 ^ 79, -49073206049 / 2 ^ 80, 4057129609 / 2 ^ 79]
  B := [18564378190114274368843 / 2 ^ 78, -12086623994624346667905 / 2 ^ 80, 61139390613126772527 / 2 ^ 75, -315215008061020130175 / 2 ^ 80, 25295859241476376281 / 2 ^ 79, -4047696850002948703 / 2 ^ 79, 646209342731355433 / 2 ^ 79, -205997123132627635 / 2 ^ 80, 16399487715980025 / 2 ^ 79, -5219291702712439 / 2 ^ 80, 830405365731775 / 2 ^ 80, -33035289111537 / 2 ^ 78, 21036234864483 / 2 ^ 80, -418867532239 / 2 ^ 77, 534193932429 / 2 ^ 80, -85233676337 / 2 ^ 80, 13612402123 / 2 ^ 80]

/-- Segment `[51 / 2 ^ 3, 7]` of `piece1_2`. -/
def seg1_2_3 : Piece where
  a := 51 / 2 ^ 3
  b := 7
  c := 107 / 2 ^ 4
  H := 5 / 2 ^ 4
  A := [303003508108242995493953 / 2 ^ 78, -225426579872059208513 / 2 ^ 78, 196203044776213612507 / 2 ^ 80, -37738416394419601125 / 2 ^ 80, 6773008457735785063 / 2 ^ 80, -1162357295026014419 / 2 ^ 80, 48328941963511465 / 2 ^ 78, -7853639143246805 / 2 ^ 78, 5015368661901963 / 2 ^ 80, -789685581184035 / 2 ^ 80, 30743464417931 / 2 ^ 78, -18980575869961 / 2 ^ 80, 2908481308187 / 2 ^ 80, -443051317287 / 2 ^ 80, 33581451297 / 2 ^ 79, -5070281683 / 2 ^ 79, 381498875 / 2 ^ 78]
  B := [16849419014712445864119 / 2 ^ 78, -9966548908544190813179 / 2 ^ 80, 1466836627956188551391 / 2 ^ 80, -214995551014651885097 / 2 ^ 80, 31402745430607066795 / 2 ^ 80, -4573715022246106673 / 2 ^ 80, 20770222335495395 / 2 ^ 75, -48210239041174085 / 2 ^ 79, 13970572191990647 / 2 ^ 80, -31603134116483 / 2 ^ 74, 146347425529631 / 2 ^ 79, -42350830870097 / 2 ^ 80, 3064292982987 / 2 ^ 79, -887153337863 / 2 ^ 80, 64241717259 / 2 ^ 79, -9309566921 / 2 ^ 79, 1350037451 / 2 ^ 79]

/-- Segment `[7, 8]` of `piece1_3`. -/
def seg1_3_0 : Piece where
  a := 7
  b := 8
  c := 15 / 2 ^ 1
  H := 1 / 2 ^ 1
  A := [1211393267953362459588141 / 2 ^ 80, -645261756375942642345 / 2 ^ 80, 62936647597709422929 / 2 ^ 79, -2715197214802274783 / 2 ^ 77, 3499425611377680351 / 2 ^ 80, -33704345589928425 / 2 ^ 76, 80548279817818925 / 2 ^ 80, -734741179211825 / 2 ^ 76, 842740406671377 / 2 ^ 79, -59571371676343 / 2 ^ 78, 16654999860853 / 2 ^ 79, -4613864520967 / 2 ^ 80, 634273403251 / 2 ^ 80, -86650645731 / 2 ^ 80, 368005049 / 2 ^ 75, -796730985 / 2 ^ 79, 214827345 / 2 ^ 80]
  B := [60165114828934141638501 / 2 ^ 80, -7950081824493664218063 / 2 ^ 80, 261590630475542563317 / 2 ^ 78, -137235780009263160917 / 2 ^ 80, 8972166910702865269 / 2 ^ 79, -1170126646243730489 / 2 ^ 79, 304556880302202783 / 2 ^ 80, -2472904354704461 / 2 ^ 76, 2566719195528837 / 2 ^ 79, -41585696019353 / 2 ^ 76, 86184501795331 / 2 ^ 80, -11158908323489 / 2 ^ 80, 1444582914129 / 2 ^ 80, -187015069235 / 2 ^ 80, 12107785993 / 2 ^ 79, -3136566039 / 2 ^ 80, 203222467 / 2 ^ 79]

/-- Segment `[8, 9]` of `piece1_3`. -/
def seg1_3_1 : Piece where
  a := 8
  b := 9
  c := 17 / 2 ^ 1
  H := 1 / 2 ^ 1
  A := [1210855188339415863511641 / 2 ^ 80, -446965917421799816739 / 2 ^ 80, 77313667977763971727 / 2 ^ 80, -11839334751357762623 / 2 ^ 80, 1693541266727584285 / 2 ^ 80, -231817014388383325 / 2 ^ 80, 30764431884739775 / 2 ^ 80, -3989853674547829 / 2 ^ 80, 508329924139475 / 2 ^ 80, -63857028317663 / 2 ^ 80, 3965366367511 / 2 ^ 79, -487881849467 / 2 ^ 79, 119122106813 / 2 ^ 80, -14447918371 / 2 ^ 80, 435679951 / 2 ^ 78, -13076861 / 2 ^ 76, 25020441 / 2 ^ 80]
  B := [53140033361644784584567 / 2 ^ 80, -6207401842434429091483 / 2 ^ 80, 361389619684026511963 / 2 ^ 79, -41957156140221705527 / 2 ^ 79, 4858558149056748155 / 2 ^ 79, -1122665027532133671 / 2 ^ 80, 129453628667105273 / 2 ^ 80, -14902701918634045 / 2 ^ 80, 1713290549331173 / 2 ^ 80, -98378849404013 / 2 ^ 79, 22577531394899 / 2 ^ 80, -647297071949 / 2 ^ 78, 296811492131 / 2 ^ 80, -34017649935 / 2 ^ 80, 3898528137 / 2 ^ 80, -223406779 / 2 ^ 79, 51218741 / 2 ^ 80]

/-- Segment `[9, 10]` of `piece1_3`. -/
def seg1_3_2 : Piece where
  a := 9
  b := 10
  c := 19 / 2 ^ 1
  H := 1 / 2 ^ 1
  A := [1210475185705585114188601 / 2 ^ 80, -40260160793308492655 / 2 ^ 77, 50028665206488626163 / 2 ^ 80, -3441890135404075889 / 2 ^ 79, 885208488850920223 / 2 ^ 80, -54485206972048697 / 2 ^ 79, 13008986160185809 / 2 ^ 80, -758978481405567 / 2 ^ 79, 87009488481635 / 2 ^ 79, -19670589710939 / 2 ^ 80, 2198176932131 / 2 ^ 80, -121665023807 / 2 ^ 79, 26723214019 / 2 ^ 80, -364406855 / 2 ^ 77, 4940979 / 2 ^ 74, -34134601 / 2 ^ 80, 229329 / 2 ^ 76]
  B := [47580206985282780077039 / 2 ^ 80, -4979646621658823482653 / 2 ^ 80, 259891488710525064963 / 2 ^ 79, -27061631917470576941 / 2 ^ 79, 5623152713803687315 / 2 ^ 80, -583055912752348617 / 2 ^ 80, 7543747401646257 / 2 ^ 77, -3118544137176403 / 2 ^ 79, 643758106129559 / 2 ^ 80, -518541063301 / 2 ^ 73, 6837239821797 / 2 ^ 80, -703828447317 / 2 ^ 80, 36207210229 / 2 ^ 79, -3723850023 / 2 ^ 79, 765803853 / 2 ^ 80, -39367107 / 2 ^ 79, 8094791 / 2 ^ 80]

/-- Segment `[10, 45 / 2 ^ 2]` of `piece1_4`. -/
def seg1_4_0 : Piece where
  a := 10
  b := 45 / 2 ^ 2
  c := 85 / 2 ^ 3
  H := 5 / 2 ^ 3
  A := [1210167605339507849572969 / 2 ^ 80, -14460185034214395143 / 2 ^ 76, 8057503782563618325 / 2 ^ 78, -3979424847147452381 / 2 ^ 80, 459398841594044345 / 2 ^ 80, -50788478764858425 / 2 ^ 80, 5446751622633399 / 2 ^ 80, -571061601354867 / 2 ^ 80, 14707912858849 / 2 ^ 78, -747080240039 / 2 ^ 77, 300129526907 / 2 ^ 79, -29858528149 / 2 ^ 79, 2946870165 / 2 ^ 79, -288873195 / 2 ^ 79, 1759581 / 2 ^ 75, -2730075 / 2 ^ 79, 527185 / 2 ^ 80]
  B := [5320869845120808552771 / 2 ^ 77, -996925974700072658137 / 2 ^ 78, 372761854701505788327 / 2 ^ 80, -4346776864203729805 / 2 ^ 77, 809480649032375507 / 2 ^ 78, -18810895641267969 / 2 ^ 76, 6983281256504059 / 2 ^ 78, -2588872590400989 / 2 ^ 80, 119824657958699 / 2 ^ 79, -2770112342351 / 2 ^ 77, 2047446312551 / 2 ^ 80, -94511846835 / 2 ^ 79, 8720248801 / 2 ^ 79, -402101921 / 2 ^ 78, 74139391 / 2 ^ 79, -854149 / 2 ^ 76, 1259393 / 2 ^ 80]

/-- Segment `[45 / 2 ^ 2, 25 / 2 ^ 1]` of `piece1_4`. -/
def seg1_4_1 : Piece where
  a := 45 / 2 ^ 2
  b := 25 / 2 ^ 1
  c := 95 / 2 ^ 3
  H := 5 / 2 ^ 3
  A := [604960986837078464124131 / 2 ^ 79, -10399122050634038403 / 2 ^ 76, 5197584919462132559 / 2 ^ 78, -1151800734093093475 / 2 ^ 79, 238749418782237247 / 2 ^ 80, -5926172483470679 / 2 ^ 78, 570935707469577 / 2 ^ 78, -215144884605851 / 2 ^ 80, 19919165636383 / 2 ^ 80, -454695520799 / 2 ^ 78, 164193739723 / 2 ^ 80, -7341653149 / 2 ^ 79, 325657765 / 2 ^ 78, -57388699 / 2 ^ 79, 1256751 / 2 ^ 77, -876209 / 2 ^ 80, 76023 / 2 ^ 80]
  B := [4762991621593462621595 / 2 ^ 77, -399591337293451292141 / 2 ^ 77, 33464371405228531423 / 2 ^ 77, -22382540201723647165 / 2 ^ 80, 1868363113213618395 / 2 ^ 80, -155731851972221507 / 2 ^ 80, 6481560768912529 / 2 ^ 79, -1077732395178353 / 2 ^ 80, 22375623812837 / 2 ^ 78, -7425665957759 / 2 ^ 80, 615550528721 / 2 ^ 80, -50988258269 / 2 ^ 80, 2110438135 / 2 ^ 79, -349225673 / 2 ^ 80, 28881715 / 2 ^ 80, -298471 / 2 ^ 77, 49339 / 2 ^ 78]

/-- Segment `[25 / 2 ^ 1, 55 / 2 ^ 2]` of `piece1_4`. -/
def seg1_4_2 : Piece where
  a := 25 / 2 ^ 1
  b := 55 / 2 ^ 2
  c := 105 / 2 ^ 3
  H := 5 / 2 ^ 3
  A := [18902226488329256525383 / 2 ^ 74, -123595624781792141249 / 2 ^ 80, 13998827049830128083 / 2 ^ 80, -703256340104901093 / 2 ^ 79, 132229694648391845 / 2 ^ 80, -2978082001027391 / 2 ^ 78, 1041578299984989 / 2 ^ 80, -22268278832967 / 2 ^ 78, 7487362227403 / 2 ^ 80, -620776595013 / 2 ^ 80, 50891819839 / 2 ^ 80, -4133118627 / 2 ^ 80, 333005541 / 2 ^ 80, -13324001 / 2 ^ 79, 2119913 / 2 ^ 80, -41945 / 2 ^ 78, 13219 / 2 ^ 80]
  B := [4310842414466816784911 / 2 ^ 77, -2619454223841211869467 / 2 ^ 80, 198668798802438746483 / 2 ^ 80, -15046529710525463519 / 2 ^ 80, 284513324964079593 / 2 ^ 78, -42984651969607007 / 2 ^ 79, 405411597135355 / 2 ^ 76, -488899755438481 / 2 ^ 80, 4601551938117 / 2 ^ 77, -692340594307 / 2 ^ 78, 104084505855 / 2 ^ 79, -15636597067 / 2 ^ 80, 1173805509 / 2 ^ 80, -44033593 / 2 ^ 79, 825545 / 2 ^ 77, -123771 / 2 ^ 78, 37101 / 2 ^ 80]

/-- Segment `[55 / 2 ^ 2, 15]` of `piece1_4`. -/
def seg1_4_3 : Piece where
  a := 55 / 2 ^ 2
  b := 15
  c := 115 / 2 ^ 3
  H := 5 / 2 ^ 3
  A := [1209607416856150348551051 / 2 ^ 80, -94287005927532179207 / 2 ^ 80, 9764535858310644761 / 2 ^ 80, -897312709022126081 / 2 ^ 80, 38588326543209937 / 2 ^ 79, -6362299118431107 / 2 ^ 80, 509167409004143 / 2 ^ 80, -19930327965019 / 2 ^ 79, 3067758369221 / 2 ^ 80, -232903238647 / 2 ^ 80, 17485501157 / 2 ^ 80, -650278341 / 2 ^ 79, 95972271 / 2 ^ 80, -1758549 / 2 ^ 78, 128135 / 2 ^ 78, -18577 / 2 ^ 79, 2681 / 2 ^ 80]
  B := [15747996243663825955283 / 2 ^ 79, -2185364235752094524633 / 2 ^ 80, 151444194562380091937 / 2 ^ 80, -163787784419693991 / 2 ^ 74, 90590640908201053 / 2 ^ 77, -50051104206162609 / 2 ^ 80, 3453107368369139 / 2 ^ 80, -238008059703045 / 2 ^ 80, 16390360992027 / 2 ^ 80, -1127798008073 / 2 ^ 80, 77544483029 / 2 ^ 80, -5328167613 / 2 ^ 80, 45735385 / 2 ^ 77, -25111551 / 2 ^ 80, 1722661 / 2 ^ 80, -118127 / 2 ^ 80, 8097 / 2 ^ 80]

/-- Segment `[15, 67 / 2 ^ 2]` of `piece1_5`. -/
def seg1_5_0 : Piece where
  a := 15
  b := 67 / 2 ^ 2
  c := 127 / 2 ^ 3
  H := 7 / 2 ^ 3
  A := [302371318926224923775841 / 2 ^ 78, -17537256938476277715 / 2 ^ 78, 6586947165477680851 / 2 ^ 80, -548985750147343237 / 2 ^ 80, 1338597022177223 / 2 ^ 75, -3204248123007327 / 2 ^ 80, 116367483469609 / 2 ^ 79, -8269600484847 / 2 ^ 79, 1155658924105 / 2 ^ 80, -79667557579 / 2 ^ 80, 5431633899 / 2 ^ 80, -11466149 / 2 ^ 75, 1537023 / 2 ^ 76, -1637221 / 2 ^ 80, 108361 / 2 ^ 80, -7135 / 2 ^ 80, 117 / 2 ^ 78]
  B := [28526641902639167348341 / 2 ^ 80, -1793130742518792434003 / 2 ^ 80, 112596755800488285041 / 2 ^ 80, -7063274492634117785 / 2 ^ 80, 442658245636288465 / 2 ^ 80, -27716045233846977 / 2 ^ 80, 108366191732985 / 2 ^ 76, -108376984629253 / 2 ^ 80, 6768975780597 / 2 ^ 80, -422468227191 / 2 ^ 80, 13174777981 / 2 ^ 79, -410604599 / 2 ^ 78, 12789647 / 2 ^ 77, -6370745 / 2 ^ 80, 396489 / 2 ^ 80, -12333 / 2 ^ 79, 767 / 2 ^ 79]

/-- Segment `[67 / 2 ^ 2, 37 / 2 ^ 1]` of `piece1_5`. -/
def seg1_5_1 : Piece where
  a := 67 / 2 ^ 2
  b := 37 / 2 ^ 1
  c := 141 / 2 ^ 3
  H := 7 / 2 ^ 3
  A := [604690050155265697118077 / 2 ^ 79, -12837625088108945691 / 2 ^ 78, 4347984743915102869 / 2 ^ 80, -163427437443661623 / 2 ^ 79, 23008356839700867 / 2 ^ 80, -776546899409841 / 2 ^ 79, 101813326699059 / 2 ^ 80, -6531399026099 / 2 ^ 80, 103009881723 / 2 ^ 78, -12824446831 / 2 ^ 79, 197404829 / 2 ^ 77, -24087915 / 2 ^ 78, 5833147 / 2 ^ 80, -43849 / 2 ^ 77, 10487 / 2 ^ 79, -39 / 2 ^ 75, 37 / 2 ^ 79]
  B := [803105548942710050091 / 2 ^ 75, -727797397584602819313 / 2 ^ 79, 82374345309329365505 / 2 ^ 80, -2328929117368049715 / 2 ^ 79, 263168694408701043 / 2 ^ 80, -14857583056106905 / 2 ^ 80, 419094204998433 / 2 ^ 79, -47252989623099 / 2 ^ 80, 1331056678591 / 2 ^ 79, -37470503995 / 2 ^ 78, 1054204415 / 2 ^ 77, -474284899 / 2 ^ 80, 13329381 / 2 ^ 79, -1497731 / 2 ^ 80, 21027 / 2 ^ 78, -4721 / 2 ^ 80, 265 / 2 ^ 80]

/-- Segment `[37 / 2 ^ 1, 81 / 2 ^ 2]` of `piece1_5`. -/
def seg1_5_2 : Piece where
  a := 37 / 2 ^ 1
  b := 81 / 2 ^ 2
  c := 155 / 2 ^ 3
  H := 7 / 2 ^ 3
  A := [1209301993831260973174647 / 2 ^ 80, -38706262088345420073 / 2 ^ 80, 1491950918492700385 / 2 ^ 79, -204265630638661669 / 2 ^ 80, 6548153208975115 / 2 ^ 79, -805300093114197 / 2 ^ 80, 24049169460389 / 2 ^ 79, -1405820961443 / 2 ^ 79, 20206369349 / 2 ^ 77, -4585800553 / 2 ^ 79, 257381445 / 2 ^ 79, -14315675 / 2 ^ 79, 790157 / 2 ^ 79, -21663 / 2 ^ 78, 1181 / 2 ^ 78, -1 / 2 ^ 72, 7 / 2 ^ 79]
  B := [11690820593535928604951 / 2 ^ 79, -150632464153572784093 / 2 ^ 77, 62063572743484840387 / 2 ^ 80, -1597114441965870579 / 2 ^ 79, 164287290858139573 / 2 ^ 80, -8444214882064891 / 2 ^ 80, 433752117844409 / 2 ^ 80, -22266986294573 / 2 ^ 80, 1142430936459 / 2 ^ 80, -29290642961 / 2 ^ 79, 93823257 / 2 ^ 75, -38449195 / 2 ^ 78, 3937331 / 2 ^ 79, -403021 / 2 ^ 80, 10309 / 2 ^ 79, -527 / 2 ^ 79, 27 / 2 ^ 79]

/-- Segment `[81 / 2 ^ 2, 22]` of `piece1_5`. -/
def seg1_5_3 : Piece where
  a := 81 / 2 ^ 2
  b := 22
  c := 169 / 2 ^ 3
  H := 7 / 2 ^ 3
  A := [1209242412200568779815227 / 2 ^ 80, -14946039220287334331 / 2 ^ 79, 2114905630141846727 / 2 ^ 80, -132892027651347703 / 2 ^ 80, 1955474069743903 / 2 ^ 78, -441610682513433 / 2 ^ 80, 24220653002717 / 2 ^ 80, -1300293126589 / 2 ^ 80, 68664557643 / 2 ^ 80, -223664075 / 2 ^ 76, 23064529 / 2 ^ 77, -2357225 / 2 ^ 78, 239087 / 2 ^ 79, -6023 / 2 ^ 78, 1207 / 2 ^ 80, -15 / 2 ^ 78, 3 / 2 ^ 80]
  B := [83777933519854126553 / 2 ^ 72, -1014019609716437429753 / 2 ^ 80, 2994641460136280385 / 2 ^ 76, -282839212659131913 / 2 ^ 77, 106793844682608581 / 2 ^ 80, -2518784260289349 / 2 ^ 79, 59374625878353 / 2 ^ 78, -11191122319859 / 2 ^ 80, 527069053367 / 2 ^ 80, -1550712401 / 2 ^ 76, 291859591 / 2 ^ 78, -27453337 / 2 ^ 79, 645319 / 2 ^ 78, -121303 / 2 ^ 80, 2849 / 2 ^ 79, -67 / 2 ^ 78, 13 / 2 ^ 80]

/-- Segment `[22, 24]` of `piece1_6`. -/
def seg1_6_0 : Piece where
  a := 22
  b := 24
  c := 23
  H := 1
  A := [1209193011169040490529887 / 2 ^ 80, -2897601829441484949 / 2 ^ 77, 1507202769859646407 / 2 ^ 80, -87044876661823267 / 2 ^ 80, 4709482028125787 / 2 ^ 80, -244437695787601 / 2 ^ 80, 1540777867559 / 2 ^ 77, -608479872265 / 2 ^ 80, 14774427011 / 2 ^ 79, -1416336903 / 2 ^ 80, 67168165 / 2 ^ 80, -3157197 / 2 ^ 80, 18411 / 2 ^ 77, -6827 / 2 ^ 80, 315 / 2 ^ 80, -7 / 2 ^ 79, 1 / 2 ^ 80]
  B := [9850305058520169892985 / 2 ^ 79, -427835603897102486767 / 2 ^ 79, 18573137746773621667 / 2 ^ 79, -1611788552553900123 / 2 ^ 80, 8737743271098343 / 2 ^ 77, -3030145316452363 / 2 ^ 80, 131291246444511 / 2 ^ 80, -710758181095 / 2 ^ 77, 246148842737 / 2 ^ 80, -5325619055 / 2 ^ 79, 460707807 / 2 ^ 80, -9959817 / 2 ^ 79, 53809 / 2 ^ 76, -37197 / 2 ^ 80, 1607 / 2 ^ 80, -69 / 2 ^ 80, 3 / 2 ^ 80]

/-- Segment `[24, 26]` of `piece1_6`. -/
def seg1_6_1 : Piece where
  a := 24
  b := 26
  c := 25
  H := 1
  A := [1209152050239436808606499 / 2 ^ 80, -18063272324562628757 / 2 ^ 80, 1081002576838656089 / 2 ^ 80, -57468830862465541 / 2 ^ 80, 2862473960475327 / 2 ^ 80, -17098940083355 / 2 ^ 77, 6351627202319 / 2 ^ 80, -288738368567 / 2 ^ 80, 12913363117 / 2 ^ 80, -285043159 / 2 ^ 79, 12451321 / 2 ^ 79, -67391 / 2 ^ 76, 11585 / 2 ^ 78, -1979 / 2 ^ 80, 21 / 2 ^ 78, -1 / 2 ^ 78, 0]
  B := [4531496923578135469433 / 2 ^ 78, -724410227566823429075 / 2 ^ 80, 7234716235287538471 / 2 ^ 78, -1155566233181469415 / 2 ^ 80, 46124057839152393 / 2 ^ 80, -920137713211213 / 2 ^ 79, 73394676313833 / 2 ^ 80, -2926017062091 / 2 ^ 80, 116606890241 / 2 ^ 80, -4645275299 / 2 ^ 80, 23123507 / 2 ^ 77, -7364211 / 2 ^ 80, 146533 / 2 ^ 79, -11659 / 2 ^ 80, 29 / 2 ^ 76, -9 / 2 ^ 79, 1 / 2 ^ 80]

/-- Segment `[26, 28]` of `piece1_6`. -/
def seg1_6_2 : Piece where
  a := 26
  b := 28
  c := 27
  H := 1
  A := [151139978718660734744501 / 2 ^ 77, -7173564979319334391 / 2 ^ 79, 397648388277393083 / 2 ^ 79, -9791428880195409 / 2 ^ 78, 1807268392400305 / 2 ^ 80, -10002133661749 / 2 ^ 77, 3442582952151 / 2 ^ 80, -145014694007 / 2 ^ 80, 6010153927 / 2 ^ 80, -122948887 / 2 ^ 79, 1244413 / 2 ^ 77, -99883 / 2 ^ 78, 3979 / 2 ^ 78, -315 / 2 ^ 79, 25 / 2 ^ 80, -1 / 2 ^ 80, 0]
  B := [16784361615567365673215 / 2 ^ 80, -310589962143946340959 / 2 ^ 79, 2872632603855512975 / 2 ^ 77, -424946831029705413 / 2 ^ 79, 31419777816419339 / 2 ^ 80, -580574720205497 / 2 ^ 79, 42896555919987 / 2 ^ 80, -99012303319 / 2 ^ 76, 58485966813 / 2 ^ 80, -539626989 / 2 ^ 78, 79637747 / 2 ^ 80, -2937323 / 2 ^ 80, 108307 / 2 ^ 80, -499 / 2 ^ 77, 147 / 2 ^ 80, -5 / 2 ^ 80, 0]

/-- Segment `[28, 30]` of `piece1_6`. -/
def seg1_6_3 : Piece where
  a := 28
  b := 30
  c := 29
  H := 1
  A := [1209094029909684278754139 / 2 ^ 80, -5791949285815755441 / 2 ^ 79, 598014070854999841 / 2 ^ 80, -27429060197902695 / 2 ^ 80, 73681700442611 / 2 ^ 76, -48620594253771 / 2 ^ 80, 974316992703 / 2 ^ 79, -38235138137 / 2 ^ 79, 369093591 / 2 ^ 77, -56279477 / 2 ^ 79, 4246075 / 2 ^ 80, -158787 / 2 ^ 80, 2947 / 2 ^ 79, -217 / 2 ^ 80, 1 / 2 ^ 77, 0, 0]
  B := [15627594977227030687681 / 2 ^ 80, -538534282262238465715 / 2 ^ 80, 9276103932938309845 / 2 ^ 79, -638910805427136531 / 2 ^ 80, 5499065371576937 / 2 ^ 78, -378523997912419 / 2 ^ 79, 13023748478231 / 2 ^ 79, -895940149335 / 2 ^ 80, 30808107681 / 2 ^ 80, -1059075389 / 2 ^ 80, 9099291 / 2 ^ 78, -1250519 / 2 ^ 80, 42953 / 2 ^ 80, -1475 / 2 ^ 80, 51 / 2 ^ 80, -1 / 2 ^ 79, 0]

theorem segs_0_ok :
    segOk (piece1_0, seg1_0_0) = true ∧ segOk (piece1_0, seg1_0_1) = true ∧ segOk (piece1_0, seg1_0_2) = true ∧ segOk (piece1_0, seg1_0_3) = true := by
  decide +kernel

theorem segs_1_ok :
    segOk (piece1_1, seg1_1_0) = true ∧ segOk (piece1_1, seg1_1_1) = true ∧ segOk (piece1_1, seg1_1_2) = true ∧ segOk (piece1_1, seg1_1_3) = true := by
  decide +kernel

theorem segs_2_ok :
    segOk (piece1_2, seg1_2_0) = true ∧ segOk (piece1_2, seg1_2_1) = true ∧ segOk (piece1_2, seg1_2_2) = true ∧ segOk (piece1_2, seg1_2_3) = true := by
  decide +kernel

theorem segs_3_ok :
    segOk (piece1_3, seg1_3_0) = true ∧ segOk (piece1_3, seg1_3_1) = true ∧ segOk (piece1_3, seg1_3_2) = true := by
  decide +kernel

theorem segs_4_ok :
    segOk (piece1_4, seg1_4_0) = true ∧ segOk (piece1_4, seg1_4_1) = true ∧ segOk (piece1_4, seg1_4_2) = true ∧ segOk (piece1_4, seg1_4_3) = true := by
  decide +kernel

theorem segs_5_ok :
    segOk (piece1_5, seg1_5_0) = true ∧ segOk (piece1_5, seg1_5_1) = true ∧ segOk (piece1_5, seg1_5_2) = true ∧ segOk (piece1_5, seg1_5_3) = true := by
  decide +kernel

theorem segs_6_ok :
    segOk (piece1_6, seg1_6_0) = true ∧ segOk (piece1_6, seg1_6_1) = true ∧ segOk (piece1_6, seg1_6_2) = true ∧ segOk (piece1_6, seg1_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, 15 / 2 ^ 7, 0, -4725 / 2 ^ 15, 0, 2837835 / 2 ^ 22, 0, -14783093325 / 2 ^ 31, 0, 2089035875489 / 2 ^ 34, 0, -886446969205 / 2 ^ 28, 0, 66920787553 / 2 ^ 19, 0, -213003767 / 2 ^ 5, 0, 7204457605 / 2 ^ 4, 0, -38338575200, 0, 4011838599168, 0, -506056850538496, 0, 75726164512997376]
  B := [0, 3 / 2 ^ 3, 0, -105 / 2 ^ 10, 0, 72765 / 2 ^ 18, 0, -66891825 / 2 ^ 25, 0, 468131288625 / 2 ^ 34, 0, -648372640333 / 2 ^ 30, 0, 330819451849 / 2 ^ 24, 0, -3646660103 / 2 ^ 12, 0, 3398663047 / 2 ^ 6, 0, -4043620325, 0, 382701134592, 0, -44064814202880, 0, 6065091359277056, 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) :
    |P1 x - q.2.fA x| ≤ 1 / 2 ^ 70 ∧ |Q1 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 |P1 x - q.2.fA x| ≤ |P1 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 : |P1 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 |Q1 x - q.2.fB x| ≤ |Q1 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 : |Q1 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) :
    |P1 x - casym.fA x| ≤ 1 / 2 ^ 70 ∧ |Q1 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 |P1 x - casym.fA x| ≤ |P1 x - asym.fA x| + |asym.fA x - casym.fA x| := abs_sub_le _ _ _
      _ ≤ 1 / 2 ^ 80 + 1 / 2 ^ 72 := by
          have hb1 : |P1 x - eval asym.A (1 / x)| ≤ 1 / 2 ^ 80 := hb.1
          simp only [AsymPiece.fA]; linarith
      _ ≤ 1 / 2 ^ 70 := by norm_num
  · calc |Q1 x - casym.fB x| ≤ |Q1 x - asym.fB x| + |asym.fB x - casym.fB x| := abs_sub_le _ _ _
      _ ≤ 1 / 2 ^ 80 + 1 / 2 ^ 72 := by
          have hb2 : |Q1 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) :
    |P1 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 |P1 x - pFd R S x| ≤ |P1 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 (3 / 8) q.2 R S) = true ∧ isScaled sW (qW q.2 S) = true)
    (hc : ratioCheckI (toInt sE (qE (3 / 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) :
    |Q1 x - qFd (3 / 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 (3 / 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 |Q1 x - qFd (3 / 8) R S x| ≤ |Q1 x - q.2.fB x| + |q.2.fB x - qFd (3 / 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) : |P1 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 |P1 x - pFd R S x| ≤ |P1 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 (3 / 8) casym R S) = true ∧ isScaled sW (sAsym S) = true)
    (hc : ratioCheckI (toInt sE (qEa (3 / 8) casym R S)) (toInt sW (sAsym S)) sE sW 68 e 0 35 10 12 = true)
    (x : ℝ) (hx : 30 ≤ x) : |Q1 x - qFd (3 / 8) R S x| ≤ (e : ℝ) / 2 ^ 68 + 1 / 2 ^ 70 := by
  have h1 := (near_asym x hx).2
  have h2 := q_asym (3 / 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 |Q1 x - qFd (3 / 8) R S x| ≤ |Q1 x - casym.fB x| + |casym.fB x - qFd (3 / 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.BesselSeg1