Exact A3X qT and d times Jh-minus-one branch certificates

import Definitions.Def_A3X_Step028_second_chain



/-!
# CKLaneA3X.TMFun — functional Taylor-model operations (kernel-evaluable) with soundness

A `TMd` is `(P, r, n)`.  `Good f d` := `Encl f d.P d.r d.n ∧ 0 ≤ d.r`.
All remainders are rounded up to multiples of `2^-40` (`rup`) to keep rationals small.
-/

namespace CKLaneA3X

































/-- exact constant `c` as a TM of order `n` -/
def TMd.const (c : ℚ) (n : ℕ) : TMd := ⟨[[(0, [(0, c)])]], 0, n⟩







/-! ## Horner evaluation of a rational polynomial at a TM -/












/-! ## magnitude of a TM-enclosed function -/



end CKLaneA3X



/-! Generated by num/gen_par.py (Lane A3): TM chain data (definitions only). -/

set_option maxHeartbeats 0
set_option maxRecDepth 100000
set_option linter.unusedVariables false
set_option linter.unnecessarySeqFocus false
set_option linter.unreachableTactic false
set_option linter.unusedTactic false

namespace CKLaneA3X























noncomputable def D_q : TMd := ⟨[[(0, [(0, ((1 : ℚ) / 4))])],
  [],
  [(0, [(0, (-1 : ℚ))])]],
  (0 : ℚ), 24⟩



noncomputable def D_h : TMd := ⟨[[],
  [(0, [(0, (2 : ℚ))])]],
  (0 : ℚ), 24⟩











noncomputable def D_mone : TMd := TMd.const (-1 : ℚ) 24









































































































































































































































end CKLaneA3X



/-! Generated by num/gen_par.py (Lane A3): TM chain data (definitions only). -/

set_option maxHeartbeats 0
set_option maxRecDepth 100000
set_option linter.unusedVariables false
set_option linter.unnecessarySeqFocus false
set_option linter.unreachableTactic false
set_option linter.unusedTactic false

namespace CKLaneA3X





































noncomputable def F_qT : ℝ → ℝ → ℝ := fun t ρ => F_q t ρ * F_JJw2dR t ρ

noncomputable def D_qT : TMd := ⟨[[],
  [(0, [(0, ((5 : ℚ) / 2))]), (1, [(0, (1 : ℚ))])],
  [],
  [(0, [(-1, (1 : ℚ)), (0, ((-25 : ℚ) / 3))]), (1, [(0, (-4 : ℚ))]), (2, [(-1, (-4 : ℚ)), (0, (4 : ℚ))])],
  [],
  [(0, [(-2, ((23 : ℚ) / 32)), (-1, ((-533 : ℚ) / 192)), (0, ((-799 : ℚ) / 240))]), (1, [(-2, ((-53 : ℚ) / 16)), (-1, ((311 : ℚ) / 96)), (0, ((-5 : ℚ) / 8))]), (2, [(-2, ((-21 : ℚ) / 4)), (-1, ((407 : ℚ) / 24)), (0, ((-21 : ℚ) / 2))]), (3, [(-2, ((19 : ℚ) / 2)), (-1, ((-73 : ℚ) / 12)), (0, (-5 : ℚ))]), (4, [(-2, ((3 : ℚ) / 2)), (-1, ((-35 : ℚ) / 4)), (0, (11 : ℚ))]), (5, [(-2, (-1 : ℚ)), (-1, ((11 : ℚ) / 6)), (0, (-2 : ℚ))])],
  [],
  [(0, [(-3, ((5 : ℚ) / 32)), (-2, ((-533 : ℚ) / 768)), (-1, ((-261 : ℚ) / 80)), (0, ((-2311 : ℚ) / 560))]), (1, [(-3, ((-25 : ℚ) / 4)), (-2, ((5017 : ℚ) / 384)), (-1, ((-89 : ℚ) / 12)), (0, ((13 : ℚ) / 8))]), (2, [(-3, ((33 : ℚ) / 8)), (-2, ((1063 : ℚ) / 192)), (-1, ((149 : ℚ) / 30)), (0, ((-61 : ℚ) / 4))]), (3, [(-3, (28 : ℚ)), (-2, ((-5651 : ℚ) / 96)), (-1, ((175 : ℚ) / 6)), (0, ((5 : ℚ) / 2))]), (4, [(-3, ((-41 : ℚ) / 2)), (-2, ((1 : ℚ) / 48)), (-1, ((73 : ℚ) / 3)), (0, (1 : ℚ))]), (5, [(-3, (-12 : ℚ)), (-2, ((1099 : ℚ) / 24)), (-1, ((-344 : ℚ) / 15)), (0, (-34 : ℚ))]), (6, [(-3, (6 : ℚ)), (-2, ((-83 : ℚ) / 12)), (-1, ((-224 : ℚ) / 15)), (0, (36 : ℚ))]), (7, [(-2, ((-17 : ℚ) / 6)), (-1, ((88 : ℚ) / 15)), (0, (-8 : ℚ))])],
  [],
  [(0, [(-4, ((-1165 : ℚ) / 2048)), (-3, ((605 : ℚ) / 384)), (-2, ((-4477 : ℚ) / 1024)), (-1, ((-250771 : ℚ) / 71680)), (0, ((-135325 : ℚ) / 16128))]), (1, [(-4, ((-6405 : ℚ) / 1024)), (-3, ((389 : ℚ) / 32)), (-2, ((57109 : ℚ) / 7680)), (-1, ((-1343617 : ℚ) / 107520)), (0, ((325 : ℚ) / 128))]), (2, [(-4, ((3475 : ℚ) / 128)), (-3, ((-381 : ℚ) / 8)), (-2, ((10201 : ℚ) / 192)), (-1, ((-12317 : ℚ) / 640)), (0, ((-299 : ℚ) / 16))]), (3, [(-4, ((1495 : ℚ) / 64)), (-3, (-86 : ℚ)), (-2, ((16681 : ℚ) / 480)), (-1, ((2293 : ℚ) / 960)), (0, ((273 : ℚ) / 8))]), (4, [(-4, ((-7011 : ℚ) / 64)), (-3, ((765 : ℚ) / 4)), (-2, ((-145783 : ℚ) / 1440)), (-1, ((58687 : ℚ) / 960)), (0, ((-509 : ℚ) / 8))]), (5, [(-4, ((781 : ℚ) / 32)), (-3, (107 : ℚ)), (-2, ((-119447 : ℚ) / 720)), (-1, ((8853 : ℚ) / 160)), (0, ((-189 : ℚ) / 4))]), (6, [(-4, ((519 : ℚ) / 8)), (-3, ((-590 : ℚ) / 3)), (-2, ((15259 : ℚ) / 180)), (-1, ((59 : ℚ) / 8)), (0, ((499 : ℚ) / 3))]), (7, [(-4, ((-93 : ℚ) / 4)), (-2, ((2027 : ℚ) / 18)), (-1, ((-2263 : ℚ) / 60)), (0, (-214 : ℚ))]), (8, [(-4, ((-21 : ℚ) / 8)), (-3, (30 : ℚ)), (-2, ((-1453 : ℚ) / 36)), (-1, ((-8107 : ℚ) / 280)), (0, (133 : ℚ))]), (9, [(-4, ((3 : ℚ) / 4)), (-3, ((-8 : ℚ) / 3)), (-2, ((-23 : ℚ) / 6)), (-1, ((2029 : ℚ) / 140)), (0, ((-82 : ℚ) / 3))])],
  [],
  [(0, [(-5, ((-2497 : ℚ) / 2048)), (-4, ((34405 : ℚ) / 12288)), (-3, ((-33181 : ℚ) / 16384)), (-2, ((-1317941 : ℚ) / 161280)), (-1, ((-6489421 : ℚ) / 1290240)), (0, ((-1057949 : ℚ) / 50688))]), (1, [(-5, ((-139 : ℚ) / 128)), (-4, ((-32785 : ℚ) / 6144)), (-3, ((936947 : ℚ) / 24576)), (-2, ((-2998579 : ℚ) / 322560)), (-1, ((-2278723 : ℚ) / 129024)), (0, ((731 : ℚ) / 256))]), (2, [(-5, ((27285 : ℚ) / 512)), (-4, ((-309509 : ℚ) / 3072)), (-3, ((1004569 : ℚ) / 20480)), (-2, ((29141 : ℚ) / 720)), (-1, ((-11426131 : ℚ) / 322560)), (0, ((-2961 : ℚ) / 128))]), (3, [(-5, ((-1035 : ℚ) / 16)), (-4, ((50083 : ℚ) / 512)), (-3, ((-2132037 : ℚ) / 10240)), (-2, ((4257041 : ℚ) / 26880)), (-1, ((-2386147 : ℚ) / 53760)), (0, ((5389 : ℚ) / 64))]), (4, [(-5, ((-14165 : ℚ) / 64)), (-4, ((211913 : ℚ) / 384)), (-3, ((-958453 : ℚ) / 2560)), (-2, ((98087 : ℚ) / 560)), (-1, ((-119867 : ℚ) / 13440)), (0, ((-3563 : ℚ) / 16))]), (5, [(-5, ((691 : ℚ) / 2)), (-4, ((-87925 : ℚ) / 192)), (-3, ((244153 : ℚ) / 1280)), (-2, ((-311809 : ℚ) / 1440)), (-1, ((23563 : ℚ) / 320)), (0, ((1575 : ℚ) / 8))]), (6, [(-5, ((1541 : ℚ) / 16)), (-4, ((-77573 : ℚ) / 96)), (-3, ((1764667 : ℚ) / 1920)), (-2, ((-1949 : ℚ) / 5)), (-1, ((31603 : ℚ) / 160)), (0, ((1421 : ℚ) / 12))]), (7, [(-5, (-285 : ℚ)), (-4, ((11027 : ℚ) / 16)), (-3, ((-97871 : ℚ) / 960)), (-2, ((-130871 : ℚ) / 840)), (-1, ((14185 : ℚ) / 336)), (0, ((-1827 : ℚ) / 2))]), (8, [(-5, ((475 : ℚ) / 8)), (-4, ((9337 : ℚ) / 48)), (-3, ((-676063 : ℚ) / 960)), (-2, ((30643 : ℚ) / 126)), (-1, ((-43129 : ℚ) / 560)), (0, ((2821 : ℚ) / 2))]), (9, [(-5, (30 : ℚ)), (-4, ((-1575 : ℚ) / 8)), (-3, ((16063 : ℚ) / 96)), (-2, ((99451 : ℚ) / 420)), (-1, ((-1963 : ℚ) / 2520)), (0, ((-3467 : ℚ) / 3))]), (10, [(-5, ((-15 : ℚ) / 2)), (-4, ((53 : ℚ) / 4)), (-3, ((3587 : ℚ) / 48)), (-2, ((-8144 : ℚ) / 63)), (-1, ((-6457 : ℚ) / 84)), (0, (518 : ℚ))]), (11, [(-4, ((7 : ℚ) / 2)), (-3, ((-109 : ℚ) / 8)), (-2, ((-5 : ℚ) / 63)), (-1, ((21739 : ℚ) / 630)), (0, (-92 : ℚ))])],
  [],
  [(0, [(-6, ((-97949 : ℚ) / 65536)), (-5, ((1510249 : ℚ) / 786432)), (-4, ((494667 : ℚ) / 131072)), (-3, ((-408259849 : ℚ) / 41287680)), (-2, ((-187797133 : ℚ) / 12902400)), (-1, ((-361628959 : ℚ) / 37847040)), (0, ((-33639571 : ℚ) / 585728))]), (1, [(-6, ((309295 : ℚ) / 32768)), (-5, ((-12789227 : ℚ) / 393216)), (-4, ((10547653 : ℚ) / 196608)), (-3, ((122573549 : ℚ) / 2949120)), (-2, ((-61917241 : ℚ) / 2150400)), (-1, ((-1732871993 : ℚ) / 56770560)), (0, ((6055 : ℚ) / 2048))]), (2, [(-6, ((450237 : ℚ) / 8192)), (-5, ((-5494657 : ℚ) / 98304)), (-4, ((-6959089 : ℚ) / 49152)), (-3, ((135340471 : ℚ) / 737280)), (-2, ((-691571 : ℚ) / 179200)), (-1, ((-747830203 : ℚ) / 14192640)), (0, ((-14555 : ℚ) / 512))]), (3, [(-6, ((-1108195 : ℚ) / 4096)), (-5, ((9053901 : ℚ) / 16384)), (-4, ((-72274261 : ℚ) / 122880)), (-3, ((128082659 : ℚ) / 860160)), (-2, ((115723711 : ℚ) / 806400)), (-1, ((-54514633 : ℚ) / 645120)), (0, ((38269 : ℚ) / 256))]), (4, [(-6, ((-272015 : ℚ) / 4096)), (-5, ((4570049 : ℚ) / 16384)), (-4, ((41769863 : ℚ) / 122880)), (-3, ((-1502425699 : ℚ) / 2580480)), (-2, ((23372383 : ℚ) / 53760)), (-1, ((-16406233 : ℚ) / 129024)), (0, ((-135615 : ℚ) / 256))]), (5, [(-6, ((2390589 : ℚ) / 2048)), (-5, ((-21255243 : ℚ) / 8192)), (-4, ((134051963 : ℚ) / 61440)), (-3, ((-133577825 : ℚ) / 86016)), (-2, ((37717123 : ℚ) / 80640)), (-1, ((-321503 : ℚ) / 5120)), (0, ((137973 : ℚ) / 128))]), (6, [(-6, ((-201745 : ℚ) / 256)), (-5, ((130087 : ℚ) / 1024)), (-4, ((5705609 : ℚ) / 7680)), (-3, ((4432921 : ℚ) / 53760)), (-2, ((160367 : ℚ) / 5600)), (-1, ((959101 : ℚ) / 4480)), (0, ((-19209 : ℚ) / 16))]), (7, [(-6, ((-125881 : ℚ) / 128)), (-5, ((2172263 : ℚ) / 512)), (-4, ((-15972239 : ℚ) / 3840)), (-3, ((18719523 : ℚ) / 8960)), (-2, ((-10684241 : ℚ) / 8400)), (-1, ((51771 : ℚ) / 320)), (0, ((-6633 : ℚ) / 8))]), (8, [(-6, ((269205 : ℚ) / 256)), (-5, ((-5302561 : ℚ) / 3072)), (-4, ((-3409439 : ℚ) / 2560)), (-3, ((51713293 : ℚ) / 32256)), (-2, ((-35493659 : ℚ) / 50400)), (-1, ((1867527 : ℚ) / 4480)), (0, ((79125 : ℚ) / 16))]), (9, [(-6, ((-1735 : ℚ) / 128)), (-5, ((-2632573 : ℚ) / 1536)), (-4, ((14142143 : ℚ) / 3840)), (-3, ((-5638589 : ℚ) / 5376)), (-2, ((772013 : ℚ) / 1680)), (-1, ((4153 : ℚ) / 64)), (0, ((-71775 : ℚ) / 8))]), (10, [(-6, ((-6635 : ℚ) / 32)), (-5, ((368935 : ℚ) / 384)), (-4, ((-231053 : ℚ) / 960)), (-3, ((-4990433 : ℚ) / 2880)), (-2, ((961901 : ℚ) / 6300)), (-1, ((-270113 : ℚ) / 560)), (0, ((18461 : ℚ) / 2))]), (11, [(-6, ((645 : ℚ) / 16)), (-5, ((2197 : ℚ) / 64)), (-4, ((-350269 : ℚ) / 480)), (-3, ((1528285 : ℚ) / 2016)), (-2, ((1873079 : ℚ) / 3150)), (-1, ((8573797 : ℚ) / 27720)), (0, (-5755 : ℚ))]), (12, [(-6, ((55 : ℚ) / 16)), (-5, ((-3641 : ℚ) / 64)), (-4, ((64721 : ℚ) / 480)), (-3, ((3763681 : ℚ) / 30240)), (-2, ((-1117769 : ℚ) / 3150)), (-1, ((-7079449 : ℚ) / 27720)), (0, (2055 : ℚ))]), (13, [(-6, ((-5 : ℚ) / 8)), (-5, ((99 : ℚ) / 32)), (-4, ((1357 : ℚ) / 240)), (-3, ((-657611 : ℚ) / 15120)), (-2, ((1943 : ℚ) / 105)), (-1, ((26351 : ℚ) / 308)), (0, (-314 : ℚ))])],
  [],
  [(0, [(-7, ((-74891 : ℚ) / 65536)), (-6, ((-3819767 : ℚ) / 3145728)), (-5, ((26078801 : ℚ) / 2621440)), (-4, ((-154937963 : ℚ) / 55050240)), (-3, ((-554543219 : ℚ) / 22937600)), (-2, ((-66930533269 : ℚ) / 2270822400)), (-1, ((-2647658977 : ℚ) / 123002880)), (0, ((-67157189 : ℚ) / 399360))]), (1, [(-7, ((179589 : ℚ) / 8192)), (-6, ((-24718247 : ℚ) / 524288)), (-5, ((7142293 : ℚ) / 786432)), (-4, ((3791266943 : ℚ) / 27525120)), (-3, ((3294917987 : ℚ) / 103219200)), (-2, ((-68085622463 : ℚ) / 1135411200)), (-1, ((-11917289633 : ℚ) / 184504320)), (0, ((3059 : ℚ) / 1024))]), (2, [(-7, ((-49651 : ℚ) / 16384)), (-6, ((43420827 : ℚ) / 262144)), (-5, ((-190301593 : ℚ) / 393216)), (-4, ((112104579 : ℚ) / 917504)), (-3, ((896446367 : ℚ) / 3440640)), (-2, ((-27305923549 : ℚ) / 567705600)), (-1, ((-463015079 : ℚ) / 5125120)), (0, ((-17485 : ℚ) / 512))]), (3, [(-7, ((-64589 : ℚ) / 128)), (-6, ((329179571 : ℚ) / 393216)), (-5, ((-24468827 : ℚ) / 196608)), (-4, ((-400514535 : ℚ) / 458752)), (-3, ((16693008223 : ℚ) / 25804800)), (-2, ((12544590809 : ℚ) / 283852800)), (-1, ((-15410597 : ℚ) / 110880)), (0, ((58773 : ℚ) / 256))]), (4, [(-7, ((3599169 : ℚ) / 4096)), (-6, ((-132326625 : ℚ) / 65536)), (-5, ((999507001 : ℚ) / 294912)), (-4, ((-2653801517 : ℚ) / 1146880)), (-3, ((18568342739 : ℚ) / 38707200)), (-2, ((14329512511 : ℚ) / 38707200)), (-1, ((-92402281 : ℚ) / 354816)), (0, ((-132775 : ℚ) / 128))]), (5, [(-7, ((903077 : ℚ) / 512)), (-6, ((-144163763 : ℚ) / 32768)), (-5, ((1688967559 : ℚ) / 737280)), (-4, ((-1176251 : ℚ) / 114688)), (-3, ((-1303345811 : ℚ) / 774144)), (-2, ((21237133853 : ℚ) / 19353600)), (-1, ((-187289 : ℚ) / 768)), (0, ((996567 : ℚ) / 320))]), (6, [(-7, ((-4792711 : ℚ) / 1024)), (-6, ((456995381 : ℚ) / 49152)), (-5, ((-656225191 : ℚ) / 73728)), (-4, ((4331905735 : ℚ) / 516096)), (-3, ((-37597407961 : ℚ) / 9676800)), (-2, ((469446509 : ℚ) / 276480)), (-1, ((-137783 : ℚ) / 1008)), (0, ((-601535 : ℚ) / 96))]), (7, [(-7, ((5253 : ℚ) / 16)), (-6, ((58806613 : ℚ) / 8192)), (-5, ((-43330365 : ℚ) / 4096)), (-4, ((2329819123 : ℚ) / 430080)), (-3, ((-788798251 : ℚ) / 230400)), (-2, ((-177673507 : ℚ) / 537600)), (-1, ((-582877 : ℚ) / 3360)), (0, ((99957 : ℚ) / 16))]), (8, [(-7, ((1384591 : ℚ) / 256)), (-6, ((-73242967 : ℚ) / 4096)), (-5, ((269883215 : ℚ) / 18432)), (-4, ((-5198486371 : ℚ) / 645120)), (-3, ((647521081 : ℚ) / 115200)), (-2, ((-695920189 : ℚ) / 806400)), (-1, ((217419 : ℚ) / 160)), (0, ((32835 : ℚ) / 8))]), (9, [(-7, ((-99841 : ℚ) / 32)), (-6, ((3648385 : ℚ) / 6144)), (-5, ((133277117 : ℚ) / 9216)), (-4, ((-3793547689 : ℚ) / 322560)), (-3, ((2674095001 : ℚ) / 403200)), (-2, ((-1340158711 : ℚ) / 403200)), (-1, ((-9983 : ℚ) / 336)), (0, ((-116831 : ℚ) / 4))]), (10, [(-7, ((-64617 : ℚ) / 64)), (-6, ((10498577 : ℚ) / 1024)), (-5, ((-366532997 : ℚ) / 23040)), (-4, ((65554513 : ℚ) / 32256)), (-3, ((-55164377 : ℚ) / 40320)), (-2, ((-178343971 : ℚ) / 120960)), (-1, ((8039 : ℚ) / 60)), (0, ((114785 : ℚ) / 2))]), (11, [(-7, (1085 : ℚ)), (-6, ((-1776205 : ℚ) / 512)), (-5, ((-7054867 : ℚ) / 2304)), (-4, ((908887919 : ℚ) / 80640)), (-3, ((-55889713 : ℚ) / 33600)), (-2, ((12489960481 : ℚ) / 3326400)), (-1, ((48203 : ℚ) / 35)), (0, (-68601 : ℚ))]), (12, [(-7, ((-1925 : ℚ) / 16)), (-6, ((-760865 : ℚ) / 768)), (-5, ((1953361 : ℚ) / 384)), (-4, ((-375735317 : ℚ) / 120960)), (-3, ((-1817474909 : ℚ) / 453600)), (-2, ((-286041131 : ℚ) / 151200)), (-1, ((-18617131 : ℚ) / 6930)), (0, ((161890 : ℚ) / 3))]), (13, [(-7, ((-105 : ℚ) / 2)), (-6, ((62575 : ℚ) / 128)), (-5, ((-40415 : ℚ) / 64)), (-4, ((-37291957 : ℚ) / 20160)), (-3, ((175652647 : ℚ) / 75600)), (-2, ((1652671381 : ℚ) / 831600)), (-1, ((1864075 : ℚ) / 1001)), (0, (-27388 : ℚ))]), (14, [(-7, ((35 : ℚ) / 4)), (-6, ((-1235 : ℚ) / 64)), (-5, ((-5925 : ℚ) / 32)), (-4, ((17777987 : ℚ) / 30240)), (-3, ((5135453 : ℚ) / 37800)), (-2, ((-401773073 : ℚ) / 415800)), (-1, ((-2753560 : ℚ) / 3003)), (0, (8200 : ℚ))]), (15, [(-6, ((-395 : ℚ) / 96)), (-5, ((15533 : ℚ) / 720)), (-4, ((-46829 : ℚ) / 5040)), (-3, ((-6475223 : ℚ) / 56700)), (-2, ((788969 : ℚ) / 9900)), (-1, ((10208504 : ℚ) / 45045)), (0, ((-5456 : ℚ) / 5))])],
  [],
  [(0, [(-8, ((-832765 : ℚ) / 8388608)), (-7, ((-66899651 : ℚ) / 12582912)), (-6, ((115638317 : ℚ) / 10485760)), (-5, ((10132849417 : ℚ) / 660602880)), (-4, ((-4025355589 : ℚ) / 188743680)), (-3, ((-39317555351 : ℚ) / 707788800)), (-2, ((-167986207815737 : ℚ) / 2479738060800)), (-1, ((-281745108369 : ℚ) / 5248122880)), (0, ((-8591673337 : ℚ) / 16711680))]), (1, [(-8, ((122539795 : ℚ) / 4194304)), (-7, ((-129462235 : ℚ) / 6291456)), (-6, ((-1743666361 : ℚ) / 15728640)), (-5, ((12347843773 : ℚ) / 66060288)), (-4, ((22519956139 : ℚ) / 94371840)), (-3, ((645175036501 : ℚ) / 27249868800)), (-2, ((-161690721228313 : ℚ) / 1239869030400)), (-1, ((-524485031887 : ℚ) / 3373793280)), (0, ((98185 : ℚ) / 32768))]), (2, [(-8, ((-36125541 : ℚ) / 262144)), (-7, ((192991001 : ℚ) / 393216)), (-6, ((-185332603 : ℚ) / 327680)), (-5, ((-1914255181 : ℚ) / 2949120)), (-4, ((116339610137 : ℚ) / 206438400)), (-3, ((575487343273 : ℚ) / 1703116800)), (-2, ((-6916425451801 : ℚ) / 77491814400)), (-1, ((-276067888969 : ℚ) / 1476034560)), (0, ((-82023 : ℚ) / 2048))]), (3, [(-8, ((-62411209 : ℚ) / 131072)), (-7, ((-11425403 : ℚ) / 196608)), (-6, ((79150821 : ℚ) / 32768)), (-5, ((-26517869087 : ℚ) / 10321920)), (-4, ((-67494001 : ℚ) / 2949120)), (-3, ((122262920387 : ℚ) / 121651200)), (-2, ((-2635150726877 : ℚ) / 38745907200)), (-1, ((-623612215 : ℚ) / 2342912)), (0, ((332701 : ℚ) / 1024))]), (4, [(-8, ((378573769 : ℚ) / 131072)), (-7, ((-1193021329 : ℚ) / 196608)), (-6, ((553874281 : ℚ) / 98304)), (-5, ((551820229 : ℚ) / 1474560)), (-4, ((-369968365229 : ℚ) / 103219200)), (-3, ((8747597571 : ℚ) / 4505600)), (-2, ((49889589227 : ℚ) / 615014400)), (-1, ((-744559309 : ℚ) / 1622016)), (0, ((-1837605 : ℚ) / 1024))]), (5, [(-8, ((-53256847 : ℚ) / 65536)), (-7, ((91763525 : ℚ) / 32768)), (-6, ((-2949260411 : ℚ) / 245760)), (-5, ((665521003 : ℚ) / 49152)), (-4, ((-442439123029 : ℚ) / 51609600)), (-3, ((215500963109 : ℚ) / 141926400)), (-2, ((36396545489 : ℚ) / 30412800)), (-1, ((-1656413161 : ℚ) / 4055040)), (0, ((17863391 : ℚ) / 2560))]), (6, [(-8, ((-197875671 : ℚ) / 16384)), (-7, ((237518681 : ℚ) / 8192)), (-6, ((-538140721 : ℚ) / 20480)), (-5, ((2429307143 : ℚ) / 143360)), (-4, ((-197730803 : ℚ) / 204800)), (-3, ((-330543552293 : ℚ) / 106444800)), (-2, ((148165234103 : ℚ) / 53222400)), (-1, ((-292384003 : ℚ) / 337920)), (0, ((-7468279 : ℚ) / 384))]), (7, [(-8, ((117419221 : ℚ) / 8192)), (-7, ((-261093481 : ℚ) / 12288)), (-6, ((133384613 : ℚ) / 6144)), (-5, ((-19261504357 : ℚ) / 645120)), (-4, ((39857525341 : ℚ) / 2150400)), (-3, ((-9327063853 : ℚ) / 691200)), (-2, ((47646239671 : ℚ) / 16934400)), (-1, ((-272251081 : ℚ) / 322560)), (0, ((2337335 : ℚ) / 64))]), (8, [(-8, ((161139601 : ℚ) / 16384)), (-7, ((-1394186593 : ℚ) / 24576)), (-6, ((870676777 : ℚ) / 12288)), (-5, ((-64049117309 : ℚ) / 1290240)), (-4, ((1306169799649 : ℚ) / 38707200)), (-3, ((-64468780843 : ℚ) / 9676800)), (-2, ((1025964349 : ℚ) / 193536)), (-1, ((34150577 : ℚ) / 18432)), (0, ((-4706845 : ℚ) / 128))]), (9, [(-8, ((-190070543 : ℚ) / 8192)), (-7, ((736840103 : ℚ) / 12288)), (-6, ((-62434317 : ℚ) / 2048)), (-5, ((641323973 : ℚ) / 43008)), (-4, ((-79748911541 : ℚ) / 6451200)), (-3, ((180746483 : ℚ) / 691200)), (-2, ((-19027915451 : ℚ) / 2419200)), (-1, ((-55308899 : ℚ) / 21504)), (0, ((-1576861 : ℚ) / 64))]), (10, [(-8, ((5948341 : ℚ) / 1024)), (-7, ((42802823 : ℚ) / 1536)), (-6, ((-365915087 : ℚ) / 3840)), (-5, ((5473920667 : ℚ) / 80640)), (-4, ((-36380979689 : ℚ) / 806400)), (-3, ((2484304961 : ℚ) / 120960)), (-2, ((-1225413029 : ℚ) / 423360)), (-1, ((73941949 : ℚ) / 13440)), (0, ((1403831 : ℚ) / 8))]), (11, [(-8, ((4123721 : ℚ) / 512)), (-7, ((-12527687 : ℚ) / 256)), (-6, ((33674903 : ℚ) / 640)), (-5, ((602814959 : ℚ) / 40320)), (-4, ((-1898708429 : ℚ) / 403200)), (-3, ((11659751423 : ℚ) / 665280)), (-2, ((-1552994393 : ℚ) / 1663200)), (-1, ((38655223 : ℚ) / 31680)), (0, ((-1491581 : ℚ) / 4))]), (12, [(-8, ((-2314095 : ℚ) / 512)), (-7, ((1752989 : ℚ) / 256)), (-6, ((23612759 : ℚ) / 640)), (-5, ((-7704659231 : ℚ) / 120960)), (-4, ((5314851109 : ℚ) / 518400)), (-3, ((-44830630151 : ℚ) / 1995840)), (-2, ((-2158460977 : ℚ) / 184800)), (-1, ((-81711779 : ℚ) / 10560)), (0, ((5963321 : ℚ) / 12))]), (13, [(-8, ((-29015 : ℚ) / 256)), (-7, ((3446855 : ℚ) / 384)), (-6, ((-1769405 : ℚ) / 64)), (-5, ((299834321 : ℚ) / 60480)), (-4, ((48001681643 : ℚ) / 1814400)), (-3, ((11776406471 : ℚ) / 1663200)), (-2, ((227278782323 : ℚ) / 10810800)), (-1, ((184547293 : ℚ) / 13728)), (0, ((-917413 : ℚ) / 2))]), (14, [(-8, ((29015 : ℚ) / 64)), (-7, ((-273275 : ℚ) / 96)), (-6, ((8903 : ℚ) / 48)), (-5, ((28578107 : ℚ) / 1680)), (-4, ((-5389452811 : ℚ) / 453600)), (-3, ((-517780019 : ℚ) / 46200)), (-2, ((-23680512199 : ℚ) / 1719900)), (-1, ((-1050876041 : ℚ) / 72072)), (0, (294970 : ℚ))]), (15, [(-8, ((-1925 : ℚ) / 32)), (-7, ((-5527 : ℚ) / 48)), (-6, ((95117 : ℚ) / 40)), (-5, ((-32513137 : ℚ) / 7560)), (-4, ((-895557151 : ℚ) / 226800)), (-3, ((551277997 : ℚ) / 89100)), (-2, ((1861656017 : ℚ) / 242550)), (-1, ((35302131 : ℚ) / 4004)), (0, ((-633356 : ℚ) / 5))]), (16, [(-8, ((-525 : ℚ) / 128)), (-7, ((5711 : ℚ) / 64)), (-6, ((-137449 : ℚ) / 480)), (-5, ((-330191 : ℚ) / 1120)), (-4, ((27679831 : ℚ) / 14400)), (-3, ((32244293 : ℚ) / 831600)), (-2, ((-105064094857 : ℚ) / 37837800)), (-1, ((-803438819 : ℚ) / 240240)), (0, (32777 : ℚ))]), (17, [(-8, ((35 : ℚ) / 64)), (-7, ((-331 : ℚ) / 96)), (-6, ((-2057 : ℚ) / 240)), (-5, ((1277251 : ℚ) / 15120)), (-4, ((-8810747 : ℚ) / 90720)), (-3, ((-7694453 : ℚ) / 27720)), (-2, ((713759569 : ℚ) / 2702700)), (-1, ((32986913 : ℚ) / 51480)), (0, (-3854 : ℚ))])],
  [],
  [(0, [(-9, ((11740955 : ℚ) / 8388608)), (-8, ((-97738055 : ℚ) / 12582912)), (-7, ((37592739 : ℚ) / 16777216)), (-6, ((3073591357 : ℚ) / 82575360)), (-5, ((5444007425 : ℚ) / 528482304)), (-4, ((-1914280079359 : ℚ) / 29066526720)), (-3, ((-410457046744309 : ℚ) / 3051985305600)), (-2, ((-451153042084499 : ℚ) / 2645053931520)), (-1, ((-347096244619 : ℚ) / 2422210560)), (0, ((-68723344643 : ℚ) / 42336256))]), (1, [(-9, ((5917385 : ℚ) / 262144)), (-8, ((191009633 : ℚ) / 3145728)), (-7, ((-6075596917 : ℚ) / 25165824)), (-6, ((1245940705 : ℚ) / 66060288)), (-5, ((46838634439 : ℚ) / 88080384)), (-4, ((97328597733 : ℚ) / 230686720)), (-3, ((242528860065859 : ℚ) / 9017229312000)), (-2, ((-1236959055922307 : ℚ) / 3967580897280)), (-1, ((-46536524247121 : ℚ) / 114708971520)), (0, ((196541 : ℚ) / 65536))]), (2, [(-9, ((-658912275 : ℚ) / 2097152)), (-8, ((1888393105 : ℚ) / 3145728)), (-7, ((17574509791 : ℚ) / 62914560)), (-6, ((-87195643351 : ℚ) / 41287680)), (-5, ((-7493297597 : ℚ) / 31457280)), (-4, ((13884669942421 : ℚ) / 12111052800)), (-3, ((2208798802396061 : ℚ) / 3814981632000)), (-2, ((-271647829531187 : ℚ) / 1983790448640)), (-1, ((-178321366796887 : ℚ) / 401481400320)), (0, ((-1507859 : ℚ) / 32768))]), (3, [(-9, ((8030175 : ℚ) / 32768)), (-8, ((-286696969 : ℚ) / 98304)), (-7, ((190373390501 : ℚ) / 31457280)), (-6, ((-61834021457 : ℚ) / 82575360)), (-5, ((-484021517239 : ℚ) / 110100480)), (-4, ((821854322701 : ℚ) / 550502400)), (-3, ((73521433818869 : ℚ) / 54499737600)), (-2, ((-925545193810877 : ℚ) / 4959476121600)), (-1, ((-7127573423293 : ℚ) / 11808276480)), (0, ((7140799 : ℚ) / 16384))]), (4, [(-9, ((650397747 : ℚ) / 131072)), (-8, ((-1252765423 : ℚ) / 196608)), (-7, ((-1150480997 : ℚ) / 262144)), (-6, ((13667356327 : ℚ) / 860160)), (-5, ((-27323728189 : ℚ) / 2752512)), (-4, ((-326396628651 : ℚ) / 252313600)), (-3, ((1374028140438277 : ℚ) / 442810368000)), (-2, ((-29969349460417 : ℚ) / 123986903040)), (-1, ((-1288975920773 : ℚ) / 1476034560)), (0, ((-5834969 : ℚ) / 2048))]), (5, [(-9, ((-93375459 : ℚ) / 8192)), (-8, ((1447937569 : ℚ) / 49152)), (-7, ((-29212941291 : ℚ) / 655360)), (-6, ((129311362633 : ℚ) / 5160960)), (-5, ((41246125393 : ℚ) / 20643840)), (-4, ((-1571137188281 : ℚ) / 126156800)), (-3, ((9621266841407161 : ℚ) / 1549836288000)), (-2, ((2230679999411 : ℚ) / 2108620800)), (-1, ((-490033140319 : ℚ) / 738017280)), (0, ((13822309 : ℚ) / 1024))]), (6, [(-9, ((-424373271 : ℚ) / 32768)), (-8, ((1295760949 : ℚ) / 49152)), (-7, ((2111093863 : ℚ) / 196608)), (-6, ((-737568663 : ℚ) / 17920)), (-5, ((536931920611 : ℚ) / 10321920)), (-4, ((-14799671867021 : ℚ) / 567705600)), (-3, ((532705286508611 : ℚ) / 110702592000)), (-2, ((42327518377051 : ℚ) / 22140518400)), (-1, ((-22923608041 : ℚ) / 10543104)), (0, ((-24325175 : ℚ) / 512))]), (7, [(-9, ((119534019 : ℚ) / 2048)), (-8, ((-417930691 : ℚ) / 3072)), (-7, ((76713713153 : ℚ) / 491520)), (-6, ((-184386285137 : ℚ) / 1290240)), (-5, ((318187176431 : ℚ) / 5160960)), (-4, ((-5222107963271 : ℚ) / 283852800)), (-3, ((-19818973379939 : ℚ) / 1986969600)), (-2, ((3966725392171 : ℚ) / 662323200)), (-1, ((-13870760653 : ℚ) / 14192640)), (0, ((31505539 : ℚ) / 256))]), (8, [(-9, ((-416765403 : ℚ) / 16384)), (-8, ((-142528611 : ℚ) / 8192)), (-7, ((13533681107 : ℚ) / 491520)), (-6, ((558311267 : ℚ) / 16128)), (-5, ((-580772165999 : ℚ) / 15482880)), (-4, ((7585511204039 : ℚ) / 121651200)), (-3, ((-570455326035799 : ℚ) / 29804544000)), (-2, ((92732222426929 : ℚ) / 5960908800)), (-1, ((818814551 : ℚ) / 2027520)), (0, ((-57123391 : ℚ) / 256))]), (9, [(-9, ((-19337885 : ℚ) / 256)), (-8, ((1845946535 : ℚ) / 6144)), (-7, ((-85414607863 : ℚ) / 245760)), (-6, ((62063123953 : ℚ) / 215040)), (-5, ((-1664897971867 : ℚ) / 7741440)), (-4, ((66055829093 : ℚ) / 860160)), (-3, ((-4954402581377 : ℚ) / 90316800)), (-2, ((-459800249651 : ℚ) / 54190080)), (-1, ((-6024211351 : ℚ) / 645120)), (0, ((28075619 : ℚ) / 128))]), (10, [(-9, ((331819259 : ℚ) / 4096)), (-8, ((-815937641 : ℚ) / 6144)), (-7, ((-8459302759 : ℚ) / 122880)), (-6, ((321569161 : ℚ) / 3840)), (-5, ((-234490714837 : ℚ) / 3870720)), (-4, ((892283979073 : ℚ) / 19353600)), (-3, ((14261833075969 : ℚ) / 677376000)), (-2, ((3151931050441 : ℚ) / 135475200)), (-1, ((1349236813 : ℚ) / 64512)), (0, ((9342619 : ℚ) / 64))]), (11, [(-9, ((1094157 : ℚ) / 128)), (-8, ((-44101645 : ℚ) / 192)), (-7, ((10050973857 : ℚ) / 20480)), (-6, ((-10069455379 : ℚ) / 32256)), (-5, ((10189794611 : ℚ) / 43008)), (-4, ((-676592242433 : ℚ) / 7096320)), (-3, ((4749086163649 : ℚ) / 149022720)), (-2, ((-2768930875583 : ℚ) / 82790400)), (-1, ((-4656005489 : ℚ) / 253440)), (0, ((-34946951 : ℚ) / 32))]), (12, [(-9, ((-22322697 : ℚ) / 512)), (-8, ((145818125 : ℚ) / 768)), (-7, ((-88597985 : ℚ) / 1024)), (-6, ((-6535000991 : ℚ) / 30240)), (-5, ((149447130001 : ℚ) / 1451520)), (-4, ((-12181048130879 : ℚ) / 79833600)), (-3, ((9684452273827 : ℚ) / 931392000)), (-2, ((-5168815591109 : ℚ) / 186278400)), (-1, ((512501023 : ℚ) / 88704)), (0, ((19592027 : ℚ) / 8))]), (13, [(-9, ((456603 : ℚ) / 32)), (-8, ((4283125 : ℚ) / 192)), (-7, ((-134903427 : ℚ) / 512)), (-6, ((18455126359 : ℚ) / 60480)), (-5, ((-25100130299 : ℚ) / 725760)), (-4, ((1419649092313 : ℚ) / 13305600)), (-3, ((73814167941907 : ℚ) / 864864000)), (-2, ((1236056130667 : ℚ) / 19219200)), (-1, ((5545428601 : ℚ) / 137280)), (0, ((-14222047 : ℚ) / 4))]), (14, [(-9, ((557613 : ℚ) / 128)), (-8, ((-3652957 : ℚ) / 64)), (-7, ((89346851 : ℚ) / 768)), (-6, ((72735263 : ℚ) / 1260)), (-5, ((-60605428409 : ℚ) / 362880)), (-4, ((-203554864393 : ℚ) / 19958400)), (-3, ((-391932533048503 : ℚ) / 3027024000)), (-2, ((-6916605239351 : ℚ) / 67267200)), (-1, ((-119630847431 : ℚ) / 1441440)), (0, ((7405613 : ℚ) / 2))]), (15, [(-9, ((-22575 : ℚ) / 8)), (-8, ((44835 : ℚ) / 4)), (-7, ((9773057 : ℚ) / 384)), (-6, ((-1806136519 : ℚ) / 15120)), (-5, ((7833525283 : ℚ) / 181440)), (-4, ((39087722827 : ℚ) / 665280)), (-3, ((34778484611473 : ℚ) / 504504000)), (-2, ((2649377439823 : ℚ) / 23284800)), (-1, ((68850309523 : ℚ) / 720720)), (0, (-2817937 : ℚ))]), (16, [(-9, ((26355 : ℚ) / 128)), (-8, ((189707 : ℚ) / 64)), (-7, ((-75738059 : ℚ) / 3840)), (-6, ((71550421 : ℚ) / 3780)), (-5, ((16564508629 : ℚ) / 362880)), (-4, ((-617598424171 : ℚ) / 19958400)), (-3, ((-119044256104349 : ℚ) / 3027024000)), (-2, ((-1714121464589 : ℚ) / 24216192)), (-1, ((-36411585031 : ℚ) / 480480)), (0, ((3080375 : ℚ) / 2))]), (17, [(-9, ((315 : ℚ) / 4)), (-8, ((-45703 : ℚ) / 48)), (-7, ((3015919 : ℚ) / 1920)), (-6, ((35325533 : ℚ) / 5040)), (-5, ((-3175120583 : ℚ) / 181440)), (-4, ((-3543835697 : ℚ) / 399168)), (-3, ((24188834066153 : ℚ) / 1513512000)), (-2, ((9221378282489 : ℚ) / 302702400)), (-1, ((67768228327 : ℚ) / 1750320)), (0, (-574363 : ℚ))]), (18, [(-9, ((-315 : ℚ) / 32)), (-8, ((1225 : ℚ) / 48)), (-7, ((70459 : ℚ) / 192)), (-6, ((-590669 : ℚ) / 378)), (-5, ((22753663 : ℚ) / 90720)), (-4, ((206609993 : ℚ) / 36960)), (-3, ((-145226051471 : ℚ) / 756756000)), (-2, ((-26328249463 : ℚ) / 3088800)), (-1, ((-74892913567 : ℚ) / 6126120)), (0, (131082 : ℚ))]), (19, [(-8, ((14 : ℚ) / 3)), (-7, ((-14723 : ℚ) / 480)), (-6, ((15313 : ℚ) / 756)), (-5, ((316265 : ℚ) / 1296)), (-4, ((-1054795859 : ℚ) / 2494800)), (-3, ((-23111605519 : ℚ) / 34398000)), (-2, ((20557265977 : ℚ) / 25225200)), (-1, ((5855329819 : ℚ) / 3063060)), (0, (-13796 : ℚ))])],
  [],
  [(0, [(-10, ((751324489 : ℚ) / 268435456)), (-9, ((-9076858645 : ℚ) / 1610612736)), (-8, ((-1066482121 : ℚ) / 67108864)), (-7, ((88739820389 : ℚ) / 2013265920)), (-6, ((1064660070239 : ℚ) / 14092861440)), (-5, ((-66570803674499 : ℚ) / 3720515420160)), (-4, ((-229159091912860177 : ℚ) / 1269625887129600)), (-3, ((-220429793609669843 : ℚ) / 634812943564800)), (-2, ((-82363333010094209 : ℚ) / 179863667343360)), (-1, ((-32705650368758167 : ℚ) / 81366897131520)), (0, ((-2199057337423 : ℚ) / 418381824))]), (1, [(-10, ((-501688251 : ℚ) / 134217728)), (-9, ((45630255885 : ℚ) / 268435456)), (-8, ((-23026254523 : ℚ) / 100663296)), (-7, ((-475573163527 : ℚ) / 1006632960)), (-6, ((11643510136009 : ℚ) / 21139292160)), (-5, ((451592193753485 : ℚ) / 372051542016)), (-4, ((185132232908606057 : ℚ) / 211604314521600)), (-3, ((31075771156885943 : ℚ) / 529010786304000)), (-2, ((-1085804620655940011 : ℚ) / 1348977505075200)), (-1, ((-1608218986448069 : ℚ) / 1435886419968)), (0, ((1572715 : ℚ) / 524288))]), (2, [(-10, ((-14190342695 : ℚ) / 33554432)), (-9, ((1149479073 : ℚ) / 67108864)), (-8, ((57247372313 : ℚ) / 25165824)), (-7, ((-222431001713 : ℚ) / 83886080)), (-6, ((-6613816970737 : ℚ) / 1761607680)), (-5, ((217250451760799 : ℚ) / 332188876800)), (-4, ((1760224598478543427 : ℚ) / 793516179456000)), (-3, ((76329011234271487 : ℚ) / 56679727104000)), (-2, ((-21833367903483637 : ℚ) / 112414792089600)), (-1, ((-1674917926234409 : ℚ) / 1452980305920)), (0, ((-6816409 : ℚ) / 131072))]), (3, [(-10, ((32327627745 : ℚ) / 16777216)), (-9, ((-663195089453 : ℚ) / 100663296)), (-8, ((311541731921 : ℚ) / 62914560)), (-7, ((470150844399 : ℚ) / 41943040)), (-6, ((-24363715098539 : ℚ) / 2642411520)), (-5, ((-5143879065511159 : ℚ) / 1162661068800)), (-4, ((46840753843375689 : ℚ) / 14694744064000)), (-3, ((11996446785708019 : ℚ) / 5667972710400)), (-2, ((-60735679854990863 : ℚ) / 168622188134400)), (-1, ((-1225424546594879 : ℚ) / 802962800640)), (0, ((36871191 : ℚ) / 65536))]), (4, [(-10, ((64602211545 : ℚ) / 16777216)), (-9, ((270649465945 : ℚ) / 33554432)), (-8, ((-6997743939677 : ℚ) / 188743680)), (-7, ((4111932866629 : ℚ) / 125829120)), (-6, ((48372252929863 : ℚ) / 7927234560)), (-5, ((-66879469010820749 : ℚ) / 3487983206400)), (-4, ((1295276477041587851 : ℚ) / 396758089728000)), (-3, ((2610607477260620963 : ℚ) / 595137134592000)), (-2, ((-14355535808753459 : ℚ) / 33724437626880)), (-1, ((-503700914289709 : ℚ) / 267654266880)), (0, ((-278426433 : ℚ) / 65536))]), (5, [(-10, ((-265466472963 : ℚ) / 8388608)), (-9, ((1060675823669 : ℚ) / 16777216)), (-8, ((-3975443520373 : ℚ) / 94371840)), (-7, ((-877854304853 : ℚ) / 20971520)), (-6, ((287678761265699 : ℚ) / 3963617280)), (-5, ((-59762647727949049 : ℚ) / 1743991603200)), (-4, ((-1064383943449366049 : ℚ) / 198379044864000)), (-3, ((3272810772971807047 : ℚ) / 297568567296000)), (-2, ((553240034374039 : ℚ) / 450861465600)), (-1, ((-3670340407683 : ℚ) / 2624061440)), (0, ((775334691 : ℚ) / 32768))]), (6, [(-10, ((12599381919 : ℚ) / 524288)), (-9, ((-279447188971 : ℚ) / 3145728)), (-8, ((429946134947 : ℚ) / 1966080)), (-7, ((-2544682287727 : ℚ) / 11796480)), (-6, ((3925417810231 : ℚ) / 35389440)), (-5, ((378277174372879 : ℚ) / 36333158400)), (-4, ((-487620157975492363 : ℚ) / 12398690304000)), (-3, ((271463860047686893 : ℚ) / 18598035456000)), (-2, ((-374947358790233 : ℚ) / 309967257600)), (-1, ((-331640757941 : ℚ) / 70287360)), (0, ((-205021615 : ℚ) / 2048))]), (7, [(-10, ((31710473775 : ℚ) / 262144)), (-9, ((-148582243729 : ℚ) / 524288)), (-8, ((628451576197 : ℚ) / 2949120)), (-7, ((-238879042217 : ℚ) / 4587520)), (-6, ((-19012753951631 : ℚ) / 123863040)), (-5, ((1622077408888577 : ℚ) / 10899947520)), (-4, ((-41960397273952351 : ℚ) / 476872704000)), (-3, ((26986247598823441 : ℚ) / 1859803545600)), (-2, ((16872123232253 : ℚ) / 1703116800)), (-1, ((12913947353 : ℚ) / 18923520)), (0, ((2325947871 : ℚ) / 7168))]), (8, [(-10, ((-114148840935 : ℚ) / 524288)), (-9, ((486929897193 : ℚ) / 1048576)), (-8, ((-1255752733703 : ℚ) / 1966080)), (-7, ((2950402815637 : ℚ) / 3932160)), (-6, ((-40373292160979 : ℚ) / 82575360)), (-5, ((10462039760710369 : ℚ) / 36333158400)), (-4, ((-436750159394669317 : ℚ) / 12398690304000)), (-3, ((1294860751160569 : ℚ) / 1690730496000)), (-2, ((453087454722101 : ℚ) / 23843635200)), (-1, ((-1126600027183 : ℚ) / 164003840)), (0, ((-1631324913 : ℚ) / 2048))]), (9, [(-10, ((-15273204635 : ℚ) / 262144)), (-9, ((289941842189 : ℚ) / 524288)), (-8, ((-2110461724901 : ℚ) / 2949120)), (-7, ((2749644182251 : ℚ) / 5898240)), (-6, ((-10520018361751 : ℚ) / 41287680)), (-5, ((-533170017621683 : ℚ) / 4954521600)), (-4, ((6015617697337217 : ℚ) / 158957568000)), (-3, ((-504249775597297 : ℚ) / 4335206400)), (-2, ((-5995208490889 : ℚ) / 794787840)), (-1, ((-95846396087 : ℚ) / 6307840)), (0, ((1428722347 : ℚ) / 1024))]), (10, [(-10, ((25315409763 : ℚ) / 65536)), (-9, ((-163237400229 : ℚ) / 131072)), (-8, ((315576529471 : ℚ) / 245760)), (-7, ((-39951883279 : ℚ) / 32768)), (-6, ((1133569970951 : ℚ) / 1146880)), (-5, ((-242452182851733 : ℚ) / 504627200)), (-4, ((15142606832350567 : ℚ) / 39739392000)), (-3, ((765968651856781 : ℚ) / 178827264000)), (-2, ((968223475392293 : ℚ) / 8941363200)), (-1, ((687989043143 : ℚ) / 14192640)), (0, ((-347751235 : ℚ) / 256))]), (11, [(-10, ((-6945679637 : ℚ) / 32768)), (-9, ((-5720170949 : ℚ) / 65536)), (-8, ((91665071245 : ℚ) / 73728)), (-7, ((-92838050459 : ℚ) / 81920)), (-6, ((14781939855797 : ℚ) / 15482880)), (-5, ((-3697948719653431 : ℚ) / 6812467200)), (-4, ((5659910949246677 : ℚ) / 59609088000)), (-3, ((-3200972613957511 : ℚ) / 17882726400)), (-2, ((-608895202536443 : ℚ) / 4470681600)), (-1, ((-11528461863 : ℚ) / 112640)), (0, ((-115980579 : ℚ) / 128))]), (12, [(-10, ((-5234903475 : ℚ) / 32768)), (-9, ((250211282503 : ℚ) / 196608)), (-8, ((-251598761179 : ℚ) / 122880)), (-7, ((2326124737937 : ℚ) / 2211840)), (-6, ((-8560337054107 : ℚ) / 9289728)), (-5, ((14805310654754887 : ℚ) / 61312204800)), (-4, ((-32709158820580631 : ℚ) / 178827264000)), (-3, ((11036529461835707 : ℚ) / 89413632000)), (-2, ((60096743306653 : ℚ) / 638668800)), (-1, ((933654778033 : ℚ) / 7096320)), (0, ((2664550369 : ℚ) / 384))]), (13, [(-10, ((3092387985 : ℚ) / 16384)), (-9, ((-18035338999 : ℚ) / 32768)), (-8, ((-85715329273 : ℚ) / 184320)), (-7, ((124021125635 : ℚ) / 73728)), (-6, ((-2316024950011 : ℚ) / 2580480)), (-5, ((10918797457571177 : ℚ) / 10218700800)), (-4, ((-100796715885879919 : ℚ) / 1162377216000)), (-3, ((168927745221912739 : ℚ) / 581188608000)), (-2, ((7679947702979 : ℚ) / 358758400)), (-1, ((-55339356779 : ℚ) / 2196480)), (0, ((-1042869777 : ℚ) / 64))]), (14, [(-10, ((-47780985 : ℚ) / 2048)), (-9, ((-1413923825 : ℚ) / 4096)), (-8, ((2247877055 : ℚ) / 1536)), (-7, ((-1125578956163 : ℚ) / 967680)), (-6, ((-23760552397 : ℚ) / 322560)), (-5, ((-49516592842793 : ℚ) / 141926400)), (-4, ((-29058583455205747 : ℚ) / 48432384000)), (-3, ((-29136138819107707 : ℚ) / 72648576000)), (-2, ((-67212006256519 : ℚ) / 172972800)), (-1, ((-126243336521 : ℚ) / 640640)), (0, ((1417118079 : ℚ) / 56))]), (15, [(-10, ((-36698361 : ℚ) / 1024)), (-9, ((1755856949 : ℚ) / 6144)), (-8, ((-738942407 : ℚ) / 2304)), (-7, ((-52797738749 : ℚ) / 69120)), (-6, ((155781916979 : ℚ) / 161280)), (-5, ((-60804921587449 : ℚ) / 638668800)), (-4, ((2025910170406807 : ℚ) / 2905943040)), (-3, ((22434137418793021 : ℚ) / 36324288000)), (-2, ((402667444594759 : ℚ) / 605404800)), (-1, ((42413303783 : ℚ) / 87360)), (0, ((-115868175 : ℚ) / 4))]), (16, [(-10, ((54969957 : ℚ) / 4096)), (-9, ((-139422059 : ℚ) / 8192)), (-8, ((-854778575 : ℚ) / 3072)), (-7, ((62341228019 : ℚ) / 92160)), (-6, ((-52780501829 : ℚ) / 1935360)), (-5, ((-2447424439670081 : ℚ) / 7664025600)), (-4, ((-72363661107506819 : ℚ) / 290594304000)), (-3, ((-97230351314264297 : ℚ) / 145297152000)), (-2, ((-65909481715929 : ℚ) / 89689600)), (-1, ((-2496376050089 : ℚ) / 3843840)), (0, ((401082819 : ℚ) / 16))]), (17, [(-10, ((951825 : ℚ) / 2048)), (-9, ((-122460807 : ℚ) / 4096)), (-8, ((2760277471 : ℚ) / 23040)), (-7, ((-1910886947 : ℚ) / 138240)), (-6, ((-369586789361 : ℚ) / 967680)), (-5, ((42392610837121 : ℚ) / 348364800)), (-4, ((7135179421771883 : ℚ) / 48432384000)), (-3, ((191192217909053 : ℚ) / 508032000)), (-2, ((12382552566512353 : ℚ) / 20583763200)), (-1, ((182439460475 : ℚ) / 311168)), (0, ((-130546017 : ℚ) / 8))]), (18, [(-10, ((-419895 : ℚ) / 512)), (-9, ((6669649 : ℚ) / 1024)), (-8, ((7575463 : ℚ) / 5760)), (-7, ((-2783231867 : ℚ) / 34560)), (-6, ((11228491987 : ℚ) / 103680)), (-5, ((4551192552299 : ℚ) / 38320128)), (-4, ((-8655900624779 : ℚ) / 148262400)), (-3, ((-2747935997051909 : ℚ) / 18162144000)), (-2, ((-563481833482021 : ℚ) / 1715313600)), (-1, ((-9241862810783 : ℚ) / 24504480)), (0, ((46662437 : ℚ) / 6))]), (19, [(-10, ((21105 : ℚ) / 256)), (-9, ((129857 : ℚ) / 512)), (-8, ((-16620541 : ℚ) / 2880)), (-7, ((5436409 : ℚ) / 384)), (-6, ((322526947 : ℚ) / 24192)), (-5, ((-5555154047801 : ℚ) / 95800320)), (-4, ((-95304093369451 : ℚ) / 3632428800)), (-3, ((383675400935579 : ℚ) / 9081072000)), (-2, ((927017762278787 : ℚ) / 7718911200)), (-1, ((38340868819139 : ℚ) / 232792560)), (0, (-2566201 : ℚ))]), (20, [(-10, ((1197 : ℚ) / 256)), (-9, ((-64659 : ℚ) / 512)), (-8, ((1460767 : ℚ) / 2880)), (-7, ((11166097 : ℚ) / 17280)), (-6, ((-236872367 : ℚ) / 40320)), (-5, ((1794053232199 : ℚ) / 479001600)), (-4, ((96185269396679 : ℚ) / 6054048000)), (-3, ((-3797242909 : ℚ) / 37065600)), (-2, ((-655713679661 : ℚ) / 23750496)), (-1, ((-496388939941 : ℚ) / 11085360)), (0, (524299 : ℚ))]), (21, [(-10, ((-63 : ℚ) / 128)), (-9, ((2891 : ℚ) / 768)), (-8, ((17479 : ℚ) / 1440)), (-7, ((-2911879 : ℚ) / 20160)), (-6, ((42763933 : ℚ) / 181440)), (-5, ((137376010859 : ℚ) / 239500800)), (-4, ((-271599911311 : ℚ) / 185328000)), (-3, ((-171546011969 : ℚ) / 100900800)), (-2, ((118609931779 : ℚ) / 47647600)), (-1, ((46107125621 : ℚ) / 7759752)), (0, ((-349518 : ℚ) / 7))])],
  [],
  [(0, [(-11, ((900666979 : ℚ) / 268435456)), (-10, ((16291896827 : ℚ) / 6442450944)), (-9, ((-18308023799 : ℚ) / 536870912)), (-8, ((2352931174117 : ℚ) / 169114337280)), (-7, ((496772405716721 : ℚ) / 3382286745600)), (-6, ((5837985098488159 : ℚ) / 44646185041920)), (-5, ((-136048527182867483 : ℚ) / 1269625887129600)), (-4, ((-290116599628833371 : ℚ) / 585981178675200)), (-3, ((-23557260276410082961 : ℚ) / 24904200093696000)), (-2, ((-1101426658373854921 : ℚ) / 854352419880960)), (-1, ((-95325835680580223 : ℚ) / 81366897131520)), (0, ((-8796130247605 : ℚ) / 506462208))]), (1, [(-11, ((-1567181035 : ℚ) / 33554432)), (-10, ((738150292729 : ℚ) / 3221225472)), (-9, ((72239837605 : ℚ) / 805306368)), (-8, ((-18405142569221 : ℚ) / 16911433728)), (-7, ((-539733985368041 : ℚ) / 1691143372800)), (-6, ((41863678883090021 : ℚ) / 22323092520960)), (-5, ((447178656509100671 : ℚ) / 158703235891200)), (-4, ((3640411994284729661 : ℚ) / 1731308027904000)), (-3, ((28438153083603582061 : ℚ) / 161877300609024000)), (-2, ((-4025540801413288141 : ℚ) / 1830755185459200)), (-1, ((-393712170686103251 : ℚ) / 122050345697280)), (0, ((1572823 : ℚ) / 524288))]), (2, [(-11, ((-20129000529 : ℚ) / 67108864)), (-10, ((-2456699219857 : ℚ) / 1610612736)), (-9, ((561255982737 : ℚ) / 134217728)), (-8, ((40468775223889 : ℚ) / 42278584320)), (-7, ((-7789082729723539 : ℚ) / 845571686400)), (-6, ((-62462119629720989 : ℚ) / 11161546260480)), (-5, ((162864407373075623 : ℚ) / 79351617945600)), (-4, ((4226312502516177499 : ℚ) / 865654013952000)), (-3, ((295525424460367727999 : ℚ) / 80938650304512000)), (-2, ((-345112026533381039 : ℚ) / 1601910787276800)), (-1, ((-27700525136196019 : ℚ) / 8717881835520)), (0, ((-15204759 : ℚ) / 262144))]), (3, [(-11, ((8728047955 : ℚ) / 2097152)), (-10, ((-5226883037227 : ℚ) / 805306368)), (-9, ((-3286549379421 : ℚ) / 335544320)), (-8, ((94290693928573 : ℚ) / 3019898880)), (-7, ((1757274465378923 : ℚ) / 422785843200)), (-6, ((-111269663722460879 : ℚ) / 5580773130240)), (-5, ((-647925481106090849 : ℚ) / 158703235891200)), (-4, ((28319473008249169 : ℚ) / 5441253801984)), (-3, ((171316425735964271537 : ℚ) / 40469325152256000)), (-2, ((-728912826488581283 : ℚ) / 1067940524851200)), (-1, ((-5993528647583831 : ℚ) / 1452980305920)), (0, ((92446895 : ℚ) / 131072))]), (4, [(-11, ((-91571664195 : ℚ) / 16777216)), (-10, ((5898413113807 : ℚ) / 134217728)), (-9, ((-7192610851339 : ℚ) / 100663296)), (-8, ((-15187040840779 : ℚ) / 1509949440)), (-7, ((3234228422420027 : ℚ) / 42278584320)), (-6, ((-76265202040567511 : ℚ) / 2790386565120)), (-5, ((-1781535223037728303 : ℚ) / 79351617945600)), (-4, ((6726863953996590113 : ℚ) / 793516179456000)), (-3, ((1314723343006813 : ℚ) / 174399160320)), (-2, ((-2139835423857281 : ℚ) / 22884439818240)), (-1, ((-1976083197759601 : ℚ) / 435894091776)), (0, ((-395848825 : ℚ) / 65536))]), (5, [(-11, ((-102803535197 : ℚ) / 2097152)), (-10, ((6918217592191 : ℚ) / 201326592)), (-9, ((31757933147303 : ℚ) / 251658240)), (-8, ((-191502153604393 : ℚ) / 754974720)), (-7, ((13472260590710513 : ℚ) / 105696460800)), (-6, ((66418074558988787 : ℚ) / 1395193282560)), (-5, ((-124006506518250329 : ℚ) / 1803445862400)), (-4, ((11577859368366981913 : ℚ) / 1190274269184000)), (-3, ((1387073462052188695 : ℚ) / 80938650304512)), (-2, ((95911375021722413 : ℚ) / 42155547033600)), (-1, ((-16329924168589 : ℚ) / 4411883520)), (0, ((1265068697 : ℚ) / 32768))]), (6, [(-11, ((604574798025 : ℚ) / 4194304)), (-10, ((-12787327979509 : ℚ) / 33554432)), (-9, ((21467350400051 : ℚ) / 41943040)), (-8, ((-12874726637675 : ℚ) / 75497472)), (-7, ((-10998885926815517 : ℚ) / 52848230400)), (-6, ((203787374920613933 : ℚ) / 697596641280)), (-5, ((-3431282364216283 : ℚ) / 30519853056)), (-4, ((-5369750471770187 : ℚ) / 198180864000)), (-3, ((35752762981423334059 : ℚ) / 1686221881344000)), (-2, ((-5811759016329011 : ℚ) / 878240563200)), (-1, ((-31802701026319 : ℚ) / 3186360320)), (0, ((-3118041265 : ℚ) / 16384))]), (7, [(-11, ((1178092311 : ℚ) / 16384)), (-10, ((-186063146935 : ℚ) / 16777216)), (-9, ((-39707766943889 : ℚ) / 62914560)), (-8, ((455562755653559 : ℚ) / 440401920)), (-7, ((-26030125478253403 : ℚ) / 26424115200)), (-6, ((44873098235886421 : ℚ) / 116266106880)), (-5, ((84786825489438151 : ℚ) / 9918952243200)), (-4, ((-11281512930688262281 : ℚ) / 99189522432000)), (-3, ((2835944796693345653 : ℚ) / 49594761216000)), (-2, ((362514301618981 : ℚ) / 17712414720)), (-1, ((10675139677571 : ℚ) / 1968046080)), (0, ((42165429375 : ℚ) / 57344))]), (8, [(-11, ((-363208409025 : ℚ) / 524288)), (-10, ((7160451555117 : ℚ) / 4194304)), (-9, ((-2094611311971 : ℚ) / 1048576)), (-8, ((177021612111731 : ℚ) / 110100480)), (-7, ((-6234406882053377 : ℚ) / 19818086400)), (-6, ((-2687377121484701 : ℚ) / 9688842240)), (-5, ((355404991514927269 : ℚ) / 676292198400)), (-4, ((-15614435529539402887 : ℚ) / 74392141824000)), (-3, ((1749188197030073599 : ℚ) / 37196070912000)), (-2, ((-11071381743641 : ℚ) / 5960908800)), (-1, ((-14522476951321 : ℚ) / 492011520)), (0, ((-4572496851 : ℚ) / 2048))]), (9, [(-11, ((37399008625 : ℚ) / 65536)), (-10, ((-5147766817603 : ℚ) / 6291456)), (-9, ((3994378626959 : ℚ) / 2621440)), (-8, ((-425346618944477 : ℚ) / 165150720)), (-7, ((1521821433212471 : ℚ) / 660602880)), (-6, ((-17286562095795515 : ℚ) / 8719958016)), (-5, ((8778717867026153 : ℚ) / 12915302400)), (-4, ((-12876978629516648869 : ℚ) / 37196070912000)), (-3, ((-363103124666529827 : ℚ) / 3719607091200)), (-2, ((127484614291583 : ℚ) / 15498362880)), (-1, ((26284051399 : ℚ) / 16400384)), (0, ((5362337795 : ℚ) / 1024))]), (10, [(-11, ((114292976171 : ℚ) / 131072)), (-10, ((-12491332267877 : ℚ) / 3145728)), (-9, ((6800792765641 : ℚ) / 1310720)), (-8, ((-56336488225549 : ℚ) / 11796480)), (-7, ((2452029441343381 : ℚ) / 707788800)), (-6, ((-7597540613164619 : ℚ) / 7266631680)), (-5, ((830947306421591 : ℚ) / 1435033600)), (-4, ((9097301503568539453 : ℚ) / 18598035456000)), (-3, ((1154363001339089371 : ℚ) / 9299017728000)), (-2, ((6912350513840663 : ℚ) / 29059430400)), (-1, ((3260355757771 : ℚ) / 52715520)), (0, ((-4572610547 : ℚ) / 512))]), (11, [(-11, ((-6416568045 : ℚ) / 4096)), (-10, ((6180921688313 : ℚ) / 1572864)), (-9, ((-375362260893 : ℚ) / 131072)), (-8, ((19100584901953 : ℚ) / 5898240)), (-7, ((-2326489695301817 : ℚ) / 825753600)), (-6, ((19968179183294213 : ℚ) / 10899947520)), (-5, ((-133193546030844911 : ℚ) / 71530905600)), (-4, ((34584011054214673 : ℚ) / 238436352000)), (-3, ((-41703817733136817 : ℚ) / 51093504000)), (-2, ((-622403756079251 : ℚ) / 1490227200)), (-1, ((-17884333663 : ℚ) / 61440)), (0, ((2201203979 : ℚ) / 256))]), (12, [(-11, ((7002891229 : ℚ) / 32768)), (-10, ((2486263554749 : ℚ) / 786432)), (-9, ((-2889904393629 : ℚ) / 327680)), (-8, ((13824581416195 : ℚ) / 1769472)), (-7, ((-3808058735002439 : ℚ) / 530841600)), (-6, ((13161063171829871 : ℚ) / 3269984256)), (-5, ((-20501546522341727 : ℚ) / 11921817600)), (-4, ((1363664082701608957 : ℚ) / 1072963584000)), (-3, ((96181081091141801 : ℚ) / 178827264000)), (-2, ((908980190047373 : ℚ) / 1117670400)), (-1, ((202206540191 : ℚ) / 337920)), (0, ((2200826069 : ℚ) / 384))]), (13, [(-11, ((4258684155 : ℚ) / 4096)), (-10, ((-735627230811 : ℚ) / 131072)), (-9, ((1059296681613 : ℚ) / 163840)), (-8, ((-1207658589295 : ℚ) / 884736)), (-7, ((3412977588230921 : ℚ) / 1857945600)), (-6, ((7914724697126761 : ℚ) / 8174960640)), (-5, ((166860228732433603 : ℚ) / 348713164800)), (-4, ((20252057170952881 : ℚ) / 634023936000)), (-3, ((-3978948239296511 : ℚ) / 12773376000)), (-2, ((-10851947074084913 : ℚ) / 14529715200)), (-1, ((-962660511877 : ℚ) / 1317888)), (0, ((-2879003975 : ℚ) / 64))]), (14, [(-11, ((-5393114375 : ℚ) / 8192)), (-10, ((124951901473 : ℚ) / 196608)), (-9, ((1464539519081 : ℚ) / 245760)), (-8, ((-10376280314221 : ℚ) / 1032192)), (-7, ((1045278188794559 : ℚ) / 185794560)), (-6, ((-5059019783368037 : ℚ) / 817496064)), (-5, ((10190174036045057 : ℚ) / 24908083200)), (-4, ((-7719283481746838459 : ℚ) / 3487131648000)), (-3, ((-9157061292172933 : ℚ) / 16605388800)), (-2, ((-824624256611 : ℚ) / 2837835)), (-1, ((5046586579 : ℚ) / 16896)), (0, ((24554548825 : ℚ) / 224))]), (15, [(-11, ((-1565949 : ℚ) / 16)), (-10, ((79140703561 : ℚ) / 32768)), (-9, ((-271643935019 : ℚ) / 40960)), (-8, ((2327816495671 : ℚ) / 860160)), (-7, ((355362836874991 : ℚ) / 154828800)), (-6, ((44957038625663 : ℚ) / 681246720)), (-5, ((21269351261591579 : ℚ) / 5283532800)), (-4, ((245312018822150081 : ℚ) / 116237721600)), (-3, ((93296055856155463 : ℚ) / 32288256000)), (-2, ((795222745445549 : ℚ) / 403603200)), (-1, ((38849193819 : ℚ) / 36608)), (0, ((-2878890279 : ℚ) / 16))]), (16, [(-11, ((849795375 : ℚ) / 4096)), (-10, ((-36918261139 : ℚ) / 32768)), (-9, ((-19666923677 : ℚ) / 122880)), (-8, ((6542826117277 : ℚ) / 1105920)), (-7, ((-325689579508261 : ℚ) / 66355200)), (-6, ((2052831913926449 : ℚ) / 2043740160)), (-5, ((-112622798005925099 : ℚ) / 34871316480)), (-4, ((-73142977157326693 : ℚ) / 21525504000)), (-3, ((-10177562238303101 : ℚ) / 2483712000)), (-2, ((-820013064566659 : ℚ) / 201801600)), (-1, ((-67102215861 : ℚ) / 23296)), (0, ((3556234845 : ℚ) / 16))]), (17, [(-11, ((-23588103 : ℚ) / 512)), (-10, ((-2883198465 : ℚ) / 16384)), (-9, ((40830530783 : ℚ) / 20480)), (-8, ((-1685312646833 : ℚ) / 552960)), (-7, ((-306471144877333 : ℚ) / 232243200)), (-6, ((1889140807800011 : ℚ) / 1021870080)), (-5, ((233979184483439 : ℚ) / 622702080)), (-4, ((76990703245962599 : ℚ) / 22353408000)), (-3, ((213185199488466001 : ℚ) / 50409216000)), (-2, ((52833143131006387 : ℚ) / 10291881600)), (-1, ((19956602672143 : ℚ) / 4667520)), (0, ((-1703411085 : ℚ) / 8))]), (18, [(-11, ((-13202805 : ℚ) / 1024)), (-10, ((1722483385 : ℚ) / 8192)), (-9, ((-16246802341 : ℚ) / 30720)), (-8, ((-36152759371 : ℚ) / 55296)), (-7, ((60144539076949 : ℚ) / 23224320)), (-6, ((-126157424664883 : ℚ) / 510935040)), (-5, ((-1367246331674849 : ℚ) / 3632428800)), (-4, ((-217111634179148083 : ℚ) / 145297152000)), (-3, ((-599530310777760083 : ℚ) / 176432256000)), (-2, ((-151634290984763 : ℚ) / 32986800)), (-1, ((-30896134031749 : ℚ) / 7001280)), (0, ((1902645959 : ℚ) / 12))]), (19, [(-11, ((190575 : ℚ) / 32)), (-10, ((-115580829 : ℚ) / 4096)), (-9, ((-1716391187 : ℚ) / 15360)), (-8, ((89433041491 : ℚ) / 138240)), (-7, ((-4917089923133 : ℚ) / 11612160)), (-6, ((-1192320393911 : ℚ) / 1105920)), (-5, ((395643018539039 : ℚ) / 4358914560)), (-4, ((1443431388970027 : ℚ) / 3459456000)), (-3, ((6557985335353169 : ℚ) / 3742502400)), (-2, ((90262300569511381 : ℚ) / 29331862560)), (-1, ((14687265010057 : ℚ) / 4434144)), (0, ((-180878645 : ℚ) / 2))]), (20, [(-11, ((-81543 : ℚ) / 256)), (-10, ((-13936573 : ℚ) / 2048)), (-9, ((28622363 : ℚ) / 512)), (-8, ((-4874810797 : ℚ) / 69120)), (-7, ((-21850478839 : ℚ) / 92160)), (-6, ((17799216017749 : ℚ) / 42577920)), (-5, ((554421780448603 : ℚ) / 1556755200)), (-4, ((-1533878231414393 : ℚ) / 36324288000)), (-3, ((-180022103848291279 : ℚ) / 308756448000)), (-2, ((-17880652552229743 : ℚ) / 12221609400)), (-1, ((-60266214201233 : ℚ) / 33256080)), (0, (38273211 : ℚ))]), (21, [(-11, ((-3465 : ℚ) / 32)), (-10, ((1650705 : ℚ) / 1024)), (-9, ((-12272677 : ℚ) / 3840)), (-8, ((-4813718521 : ℚ) / 241920)), (-7, ((1001693250661 : ℚ) / 14515200)), (-6, ((658843939909 : ℚ) / 63866880)), (-5, ((-484604359438531 : ℚ) / 2724321600)), (-4, ((-5459163952860721 : ℚ) / 54486432000)), (-3, ((124730354266001 : ℚ) / 1079568000)), (-2, ((127468336159303 : ℚ) / 271591320)), (-1, ((80196609998327 : ℚ) / 116396280)), (0, ((-79341818 : ℚ) / 7))]), (22, [(-11, ((693 : ℚ) / 64)), (-10, ((-16401 : ℚ) / 512)), (-9, ((-1212667 : ℚ) / 1920)), (-8, ((134863027 : ℚ) / 40320)), (-7, ((-3310585291 : ℚ) / 2419200)), (-6, ((-576348914501 : ℚ) / 31933440)), (-5, ((3377815763471 : ℚ) / 194594400)), (-4, ((2421654980357 : ℚ) / 51891840)), (-3, ((255346438741741 : ℚ) / 77189112000)), (-2, ((-25017965070118 : ℚ) / 269594325)), (-1, ((-3193079789357 : ℚ) / 19399380)), (0, (2097164 : ℚ))]), (23, [(-10, ((-1323 : ℚ) / 256)), (-9, ((39203 : ℚ) / 960)), (-8, ((-2098813 : ℚ) / 60480)), (-7, ((-1702620919 : ℚ) / 3628800)), (-6, ((2038648561 : ℚ) / 1774080)), (-5, ((1542779246507 : ℚ) / 1362160800)), (-4, ((-63305097771389 : ℚ) / 13621608000)), (-3, ((-177875361179357 : ℚ) / 38594556000)), (-2, ((6418406826721 : ℚ) / 833291550)), (-1, ((554356066207 : ℚ) / 29099070)), (0, (-182360 : ℚ))])]],
  ((182727474561122132597 : ℚ) / 1099511627776), 24⟩

noncomputable def F_Jh : ℝ → ℝ → ℝ := fun t ρ => F_J t ρ * F_h t ρ

noncomputable def D_Jh : TMd := ⟨[[],
  [],
  [(0, [(0, (8 : ℚ))])],
  [],
  [(0, [(0, ((32 : ℚ) / 3))])],
  [],
  [(0, [(0, ((128 : ℚ) / 5))])],
  [],
  [(0, [(0, ((512 : ℚ) / 7))])],
  [],
  [(0, [(0, ((2048 : ℚ) / 9))])],
  [],
  [(0, [(0, ((8192 : ℚ) / 11))])],
  [],
  [(0, [(0, ((32768 : ℚ) / 13))])],
  [],
  [(0, [(0, ((131072 : ℚ) / 15))])],
  [],
  [(0, [(0, ((524288 : ℚ) / 17))])],
  [],
  [(0, [(0, ((2097152 : ℚ) / 19))])],
  [],
  [(0, [(0, ((8388608 : ℚ) / 21))])],
  []],
  ((17404102049040161909 : ℚ) / 549755813888), 24⟩

noncomputable def F_Jhm1 : ℝ → ℝ → ℝ := fun t ρ => F_Jh t ρ + F_mone t ρ

noncomputable def D_Jhm1 : TMd := ⟨[[(0, [(0, (-1 : ℚ))])],
  [],
  [(0, [(0, (8 : ℚ))])],
  [],
  [(0, [(0, ((32 : ℚ) / 3))])],
  [],
  [(0, [(0, ((128 : ℚ) / 5))])],
  [],
  [(0, [(0, ((512 : ℚ) / 7))])],
  [],
  [(0, [(0, ((2048 : ℚ) / 9))])],
  [],
  [(0, [(0, ((8192 : ℚ) / 11))])],
  [],
  [(0, [(0, ((32768 : ℚ) / 13))])],
  [],
  [(0, [(0, ((131072 : ℚ) / 15))])],
  [],
  [(0, [(0, ((524288 : ℚ) / 17))])],
  [],
  [(0, [(0, ((2097152 : ℚ) / 19))])],
  [],
  [(0, [(0, ((8388608 : ℚ) / 21))])],
  []],
  ((17404102065248995039 : ℚ) / 549755813888), 24⟩

noncomputable def F_dJh : ℝ → ℝ → ℝ := fun t ρ => F_d t ρ * F_Jhm1 t ρ

noncomputable def D_dJh : TMd := ⟨[[],
  [(0, [(0, ((-1 : ℚ) / 2))]), (1, [(0, (-1 : ℚ))])],
  [],
  [(0, [(0, (4 : ℚ))]), (1, [(0, (8 : ℚ))])],
  [],
  [(0, [(0, ((16 : ℚ) / 3))]), (1, [(0, ((32 : ℚ) / 3))])],
  [],
  [(0, [(0, ((64 : ℚ) / 5))]), (1, [(0, ((128 : ℚ) / 5))])],
  [],
  [(0, [(0, ((256 : ℚ) / 7))]), (1, [(0, ((512 : ℚ) / 7))])],
  [],
  [(0, [(0, ((1024 : ℚ) / 9))]), (1, [(0, ((2048 : ℚ) / 9))])],
  [],
  [(0, [(0, ((4096 : ℚ) / 11))]), (1, [(0, ((8192 : ℚ) / 11))])],
  [],
  [(0, [(0, ((16384 : ℚ) / 13))]), (1, [(0, ((32768 : ℚ) / 13))])],
  [],
  [(0, [(0, ((65536 : ℚ) / 15))]), (1, [(0, ((131072 : ℚ) / 15))])],
  [],
  [(0, [(0, ((262144 : ℚ) / 17))]), (1, [(0, ((524288 : ℚ) / 17))])],
  [],
  [(0, [(0, ((1048576 : ℚ) / 19))]), (1, [(0, ((2097152 : ℚ) / 19))])],
  [],
  [(0, [(0, ((4194304 : ℚ) / 21))]), (1, [(0, ((8388608 : ℚ) / 21))])]],
  ((652653828054668557 : ℚ) / 68719476736), 24⟩

























end CKLaneA3X