pxfm 0.1.28

/*
 * // Copyright (c) Radzivon Bartoshyk 7/2025. All rights reserved.
 * //
 * // Redistribution and use in source and binary forms, with or without modification,
 * // are permitted provided that the following conditions are met:
 * //
 * // 1.  Redistributions of source code must retain the above copyright notice, this
 * // list of conditions and the following disclaimer.
 * //
 * // 2.  Redistributions in binary form must reproduce the above copyright notice,
 * // this list of conditions and the following disclaimer in the documentation
 * // and/or other materials provided with the distribution.
 * //
 * // 3.  Neither the name of the copyright holder nor the names of its
 * // contributors may be used to endorse or promote products derived from
 * // this software without specific prior written permission.
 * //
 * // THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * // AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * // IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * // DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * // FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * // DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * // SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * // CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * // OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * // OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */

/**
Generating Taylor expansions for zero and extremums see [crate::bessel::j1_coeffs::J1_ZEROS]
to start of explanation.

Generated by SageMath and Sollya:
```python
def compute_intervals(zeros):
    intervals = []
    for i in range(0, len(zeros)):
        if i == 0:
            a = (zeros[i]) / 2 - 0.05 - zeros[i]
            b = (zeros[i] + zeros[i + 1]) / 2 + 0.05 - zeros[i]
            intervals.append((RealField(18)(a), RealField(18)(b), RealField(110)(zeros[i])))
        elif i + 1 > len(zeros) - 1:
            a = (zeros[i - 1] + zeros[i]) / 2 - 0.05 - zeros[i]
            b = (zeros[i]) + 0.83 + 0.05 - zeros[i]
            intervals.append((RealField(18)(a), RealField(18)(b), RealField(110)(zeros[i])))
        else:
            a = (zeros[i - 1] + zeros[i]) / 2 - zeros[i] - 0.05
            b = (zeros[i] + zeros[i + 1]) / 2 + 0.05  - zeros[i]
            intervals.append((RealField(18)(a), RealField(18)(b), RealField(110)(zeros[i])))
    return intervals

intervals = compute_intervals(j1_zeros)
# print(intervals)

def build_sollya_script(a, b, zero, deg):
    return f"""
prec = 500;
bessel_j1 = library("./pxfm/notes/bessel_sollya/cmake-build-release/libbessel_sollya.dylib");
f = bessel_j1(x + {zero});
d = [{a}, {b}];
pf = remez(f, {deg}, d, 1, 1e-25);
for i from 0 to degree(pf) do {{
    write(coeff(pf, i)) >> "coefficients.txt";
    write("\\n") >> "coefficients.txt";
}};
"""

def load_coefficients(filename):
    with open(filename, "r") as f:
        return [RR(line.strip()) for line in f if line.strip()]

def call_sollya_on_interval(a, b, zero, degree=12):
    sollya_script = build_sollya_script(a, b, zero, degree)
    with open("tmp_interval.sollya", "w") as f:
        f.write(sollya_script)
    import subprocess
    if os.path.exists("coefficients.txt"):
        os.remove("coefficients.txt")
    try:
        result = subprocess.run(
            ["sollya", "tmp_interval.sollya"],
            check=True,
            capture_output=True,
            text=True
        )
    except subprocess.CalledProcessError as e:
        return

degree = 13

print(f"pub(crate) static J1F_COEFFS: [[u64;{degree + 1}]; {len(intervals)}] = [")
for i in range(0, len(intervals)):
    interval = intervals[i]
    call_sollya_on_interval(interval[0], interval[1], interval[2], degree)
    coeffs = load_coefficients(f"coefficients.txt")
    print("[")
    for c in coeffs:
        print(double_to_hex(c) + ",")
    print("],")
print("];")
```
**/
pub(crate) static J1F_COEFFS: [[u64; 14]; 47] = [
    [
        0x3fe29ea3d19f035d,
        0xbce22d3695a081b6,
        0xbfca41115c5deeab,
        0x3f78d1448e710c46,
        0x3f8c441a2f9a4f69,
        0xbf386671c22a634e,
        0xbf39e2504b2e7b5b,
        0x3ee34ccc14eef789,
        0x3eda49718b72405e,
        0xbe810474efe3c9c6,
        0xbe70fa29fb791201,
        0x3e1362d76c062ab0,
        0x3dfdd76f07295520,
        0xbda1a753bf39cb58,
    ],
    [
        0xbc600f4743bf63e1,
        0xbfd9c6cf582cbf8a,
        0x3faae8a39f51ad73,
        0x3fab589d1da1462b,
        0xbf7537544c334c23,
        0xbf624b34099ee01c,
        0x3f26e4c2d53c4f46,
        0x3f083a06ee794927,
        0xbec9799d241e5d2b,
        0xbea3382caabc394d,
        0x3e617039a48bb9f6,
        0x3e345a8c920dcd07,
        0xbdf014c3bf3000a5,
        0xbdc034aa4e0a0169,
    ],
    [
        0xbfd626ee83500bf2,
        0x3cb26dfd317b25ec,
        0x3fc55f6bec9ef90d,
        0xbf83d23336fd2aca,
        0xbf88c77a98398e83,
        0x3f45cdc98dc64f81,
        0x3f373576fec2e394,
        0xbef24614559dc202,
        0xbed7b852bb05a2ff,
        0x3e90ac054c63ba46,
        0x3e6ea70b302a9ba3,
        0xbe23616f333984e9,
        0xbdfb0a064790ebe6,
        0x3db0d9e08e0394a8,
    ],
    [
        0xbc69b70cbe5811c2,
        0x3fd33518b3874e8d,
        0xbf95e70dc6036109,
        0xbfa80c83bdeee89d,
        0x3f69a4b292e2ab0d,
        0x3f613fbc7d6bc462,
        0xbf207358bb38afba,
        0xbf0796a754e5c2d1,
        0x3ec4255a5a67b552,
        0x3ea3026fd5c83da8,
        0xbe5d482c06555943,
        0xbe34473271553ffa,
        0x3dec0515656e1a0c,
        0x3dbf11e1948b68d2,
    ],
    [
        0x3fd17dbf09d40d24,
        0xbca5b86542306439,
        0xbfc1404bf647c233,
        0x3f74f4df276a170d,
        0x3f85c628542932bb,
        0xbf3d68ab724123eb,
        0xbf356acb63c4c7d5,
        0x3eec10b48d91d910,
        0x3ed67eaa56c73092,
        0xbe8bb65dbfeed0f6,
        0xbe6d8683c673b075,
        0x3e20f7b6316797c6,
        0x3dfa451f70b9922a,
        0xbdadce2c76e4d044,
    ],
    [
        0x3c65df812ede650d,
        0xbfcff654544ebcd3,
        0x3f89223ff2c07565,
        0x3fa4b0c5d5da68d8,
        0xbf5f91a9ee0b0e8a,
        0xbf5f51c2489da5c1,
        0x3f16b4c9c8efdfe6,
        0x3f063c54768ebb67,
        0xbebe3724b50493f9,
        0xbea25c12f8827c9d,
        0x3e5747d49182153b,
        0x3e33e41718262cb9,
        0xbde738f2d8f2cac8,
        0xbdbe80a4948dbf09,
    ],
    [
        0xbfcddceb4ce1bf49,
        0x3c9e79566c79eb3d,
        0x3fbda52116c0a587,
        0xbf6a9da4603b9358,
        0xbf8331e74ea51630,
        0x3f33e5cb6ecbca42,
        0x3f33885fe920e6b8,
        0xbee494c100626ece,
        0xbed512b940a2ae49,
        0x3e85a8688c9ba4ce,
        0x3e6c31a31b773184,
        0xbe1bd11439ffd259,
        0xbdf96a9daeb33936,
        0x3da9176221cc5aa0,
    ],
    [
        0xbc62383f10698557,
        0x3fcbf3337873a7d9,
        0xbf80c83a2d7adab7,
        0xbfa251858011820e,
        0x3f559eb160bdad7b,
        0x3f5c5bce33b024a1,
        0xbf10413e2f7af958,
        0xbf04a6704d9a9d07,
        0x3eb6c43df550ea17,
        0x3ea16abdc27eeb92,
        0xbe52576e7fc9d1e6,
        0xbe332dc1c1ed3ee2,
        0x3de2f6391206ebbc,
        0x3dbda410af6fe5f4,
    ],
    [
        0x3fca7f63fea81f25,
        0xbc9710bf367611f2,
        0xbfba60afb0664019,
        0x3f62c1e930937e24,
        0x3f814506466cfd08,
        0xbf2cca8c0c28fab3,
        0xbf31df821c353039,
        0x3edee8816088c0d5,
        0x3ed3a365144be247,
        0xbe80ed354ac60d34,
        0xbe6ab31b90ea8e41,
        0x3e168836e968cdd7,
        0x3df8613c2e496c6b,
        0xbda4daa0300cec8d,
    ],
    [
        0x3c5e59bc05abf185,
        0xbfc925c6fca08f55,
        0x3f786dd32e0596e8,
        0x3fa09463bbd036c8,
        0xbf4fda0298c57ed5,
        0xbf59f4be6075f749,
        0x3f0877991961e89e,
        0x3f032cb00f1d1bde,
        0xbeb19d8c17e4c965,
        0xbea06a043bd432bf,
        0x3e4d398ca8f49a5e,
        0x3e3250f2ec743ceb,
        0xbddf086f08c63838,
        0xbdbc8e4fa8a9f9e9,
    ],
    [
        0xbfc810f50225b04a,
        0x3c923e2f625151bc,
        0x3fb7fdf97ac36a6f,
        0xbf5c3c256a8cde19,
        0xbf7f98feb7276ef1,
        0x3f25f6559e6b5a2c,
        0x3f3080f57a3a527d,
        0xbed80c5147824d09,
        0xbed256dac8ee5bae,
        0x3e7af7628377d0c7,
        0x3e6938ef2e239da2,
        0xbe12633fe4f5465f,
        0xbdf745af34a2de92,
        0x3da15e1c189cc1e4,
    ],
    [
        0xbc59737d6e4fe431,
        0x3fc70c511227d5aa,
        0xbf72ccb0e975555d,
        0xbf9e7dc08e70e9c5,
        0x3f48acdc5b030cb1,
        0x3f580503724ae80a,
        0xbf032ee4c8c82218,
        0xbf01e5d2836968fa,
        0x3eac129da754f086,
        0x3e9ef1612a209ee4,
        0xbe47b90193cc5cb3,
        0xbe316f0e2a3b6246,
        0x3dd9aabe334f3655,
        0x3dbb62c2bd937db8,
    ],
    [
        0x3fc633e7f7f05300,
        0xbc8dba9947515d38,
        0xbfb6273784c1bfc4,
        0x3f563ae94ade4347,
        0x3f7d4666536b9564,
        0xbf216d528356c33f,
        0xbf2ec0dcdab1fcc9,
        0x3ed34e967676159e,
        0x3ed135c5c78436c9,
        0xbe75f7c3c6380689,
        0xbe67dba82b616a97,
        0x3e0e71b8431ababd,
        0x3df62fc761d5cf41,
        0xbd9d2fe54f4a496b,
    ],
    [
        0x3c558a68c87f4030,
        0xbfc5664e13b70622,
        0x3f6e16555e1087dd,
        0x3f9c5e1ad9fb2f2d,
        0xbf43d369f956c6bd,
        0xbf566f4ec27a7a37,
        0x3eff0de050de72b9,
        0x3f00cf26431ce3a2,
        0xbea6f46c2694b0df,
        0xbe9d407f232dd5f2,
        0x3e43a29f2e4c9c8a,
        0x3e3098ca879e4471,
        0xbdd585d6255bc3df,
        0xbdba39fcc1ea78bf,
    ],
    [
        0xbfc4b71d4ca2cc69,
        0x3c88c930c0b4c560,
        0x3fb4ae245697fb03,
        0xbf5215e4e1a6153c,
        0xbf7b633ed6d8e543,
        0x3f1c7f17b4d42a82,
        0x3f2ce01b8a6eca10,
        0xbecfced72e1b750f,
        0xbed03c9cd706bc3a,
        0x3e72450e1e5d9dd3,
        0x3e66a249f63c5bc1,
        0xbe0999366388212b,
        0xbdf52ba007be60f3,
        0x3d98ced5beb32a74,
    ],
    [
        0xbc526f6d035edf6d,
        0x3fc40f90793605bb,
        0xbf68c833077fb99d,
        0xbf9aa0ce0421d16e,
        0x3f405fa598ed8bab,
        0x3f551d30d78a7993,
        0xbef9c5807480a6e1,
        0xbeffc1bbf50ca15b,
        0x3ea32dfda14ee884,
        0x3e9bc2119616c18d,
        0xbe408b0d01f43d88,
        0xbe2fa87db40715d8,
        0x3dd24d20c9bf3988,
        0x3db920af9a64d8b9,
    ],
    [
        0x3fc37dfa8f5a550a,
        0xbc850d0284917193,
        0xbfb3775c1a04efff,
        0x3f4e2b4810a4a882,
        0x3f79d151a72aa26d,
        0xbf17d8e5a0a8f01d,
        0xbf2b49a641814268,
        0x3ecac10968085b43,
        0x3ececa610eed952d,
        0xbe6eefd23aebb19b,
        0xbe658bda5ec8aafe,
        0x3e05d77b1c39da47,
        0x3df43d63ca6b9538,
        0xbd9555dba21d3a76,
    ],
    [
        0x3c4fe3057c054c4c,
        0xbfc2f2072e638cf3,
        0x3f64df208bbd408f,
        0x3f992bb5e1e159a9,
        0xbf3ba181c0657121,
        0xbf53fe9d5ba9fb4a,
        0x3ef5d17600fd9483,
        0x3efe26d373f4ffea,
        0xbea0509689b62f58,
        0xbe9a70f1b160bc28,
        0x3e3c4fa74da61f57,
        0x3e2e44cc2feeed24,
        0xbdcf87b5a4255e18,
        0xbdb81bebaaec3c7c,
    ],
    [
        0xbfc2768d29c69936,
        0x3c822565e3c86e7f,
        0x3fb271811730b057,
        0xbf49a8df96a15635,
        0xbf787c81cf1b96e9,
        0x3f14549cdbcc339c,
        0x3f29ed2567282f3d,
        0xbec6e4137cf2411c,
        0xbecd53321406f402,
        0x3e6a98443cd6fc90,
        0x3e6494adc7c6521b,
        0xbe02e1d787962f20,
        0xbdf3653d7772f823,
        0x3d928dbabedf1d31,
    ],
    [
        0xbc4bd8c1a48b98b5,
        0x3fc1ff5eec6a01cd,
        0xbf61e438b722bfe0,
        0xbf97ed5fffc1c711,
        0x3f37b7997ba917ee,
        0x3f53081def95b78f,
        0xbef2c5f5ec3350b1,
        0xbefcc11a59469f36,
        0x3e9c2c3894e80d05,
        0x3e9946d150444e47,
        0xbe388ce82c32666d,
        0xbe2d044ba8d28f8d,
        0x3dcb7a77f047774e,
        0x3db72cad88060e0b,
    ],
    [
        0x3fc194eba75b32f9,
        0xbc7faef3b1a5e821,
        0xbfb190f7dc273599,
        0x3f462bb47a5c8cc1,
        0x3f7756ef20f501d3,
        0xbf1198b0baaa058c,
        0xbf28be8cf854b2d7,
        0x3ec3dd6f88b69c69,
        0x3ecc09c72877c12b,
        0xbe6728ec2da828ad,
        0xbe63b897c2c7b139,
        0x3e008344f3db34b5,
        0x3df2a1a5ef6e57ff,
        0xbd904c70dc90d3bc,
    ],
    [
        0x3c4888e51c985983,
        0xbfc12dd57bf18ad9,
        0x3f5f1e1e7f3937bf,
        0x3f96d9afe883018e,
        0xbf34a538a4802887,
        0xbf52316250b44b33,
        0x3ef05f11562b37ff,
        0x3efb86bad38b7b43,
        0xbe98a1b250bb7d2f,
        0xbe983dca646511fe,
        0x3e3588f1be962e6d,
        0x3e2be36513882145,
        0xbdc831edc515fa05,
        0xbdb6520b1c14e6f6,
    ],
    [
        0xbfc0d0d36473e98c,
        0x3c7bf69dcc64d467,
        0x3fb0cda9974abd9e,
        0xbf4367f38f204418,
        0xbf7656b75e3b5a4f,
        0x3f0ed82abf947b58,
        0x3f27b4e5b765cd39,
        0xbec171fd1a726d85,
        0xbecae62a6c526e99,
        0x3e64648b6f18fd5e,
        0x3e62f3b53a117819,
        0xbdfd2c72ca1c90f8,
        0xbdf1f085bd0fab41,
        0x3d8ce566a6478844,
    ],
    [
        0xbc45ca84b624bf30,
        0x3fc076826cc2c191,
        0xbf5b62885e006ac2,
        0xbf95e7f53001e43e,
        0x3f322ebeb8d9f78a,
        0x3f517444a79fe500,
        0xbeece06f1cc95449,
        0xbefa7006e603acdb,
        0x3e95c42dcf4cb755,
        0x3e9750c9cbea6158,
        0xbe3313f5f0d7c83f,
        0xbe2ade4e1f9c8db0,
        0x3dc57f801723eb46,
        0x3db58a5b7895974e,
    ],
    [
        0x3fc02455675ab6d2,
        0xbc78e3f9125495c0,
        0xbfb021c155a72057,
        0x3f412be56fc16829,
        0x3f75749d556a12df,
        0xbf0b51f1f9db1832,
        0xbf26c96a07103bad,
        0x3ebef3a7bef163ee,
        0x3ec9e206eb2ce693,
        0xbe6220bf8745e1a3,
        0xbe6242a68bb3eb7f,
        0x3df9ffc1c0ac86f0,
        0x3df14fb8a5e39fac,
        0xbd89d286115bf7a6,
    ],
    [
        0x3c4380441b0b0c6a,
        0xbfbfa8b41711c839,
        0x3f5857d39699926e,
        0x3f9511c6dadaa99b,
        0xbf302c289dbbcc5a,
        0xbf50cc2238d1bf52,
        0x3ee9b64d5a4aa86c,
        0x3ef976fb01920f8b,
        0xbe93693a8cc790fd,
        0xbe967b9496685d1b,
        0x3e310c25f77e4f25,
        0x3e29f17f3e13ecd9,
        0xbdc3414987038eec,
        0xbdb4d3b9dc98b4b1,
    ],
    [
        0xbfbf161d0c28b48b,
        0x3c765dc0b792167d,
        0x3faf11d837aa6e5c,
        0xbf3eab76da4d4788,
        0xbf74ab329f05bdc5,
        0x3f086ada57d5a903,
        0x3f25f6e78e464093,
        0xbebbb2720677d252,
        0xbec8f8525854df7e,
        0x3e603f882886871e,
        0x3e61a293516bd71e,
        0xbdf75995de0fcb8d,
        0xbdf0bd411cec4c70,
        0x3d873e4d136b8f8b,
    ],
    [
        0xbc418c91b7939a2c,
        0x3fbe8727daa3daec,
        0xbf55d353e285455c,
        0xbf94524d4813cbac,
        0x3f2d037574df02eb,
        0x3f50356bb7473b5d,
        0xbee7156bfaea76f5,
        0xbef896d7dbd3810e,
        0x3e9172c5e1abd5c6,
        0x3e95baadfc18282d,
        0xbe2eb240c0cc9c75,
        0xbe2919d9b9e0a0b9,
        0x3dc15e50952db326,
        0x3db42c51c147e65d,
    ],
    [
        0x3fbe0357c158b118,
        0xbc74361048923786,
        0xbfadffc2fc1a90f5,
        0x3f3b9b82ae081404,
        0x3f73f64e05315346,
        0xbf05fe4b66e63077,
        0xbf2539518d55a85c,
        0x3eb8f8d02bcc2897,
        0x3ec825039164993f,
        0xbe5d566920c2c9ab,
        0xbe61111befe6e2b8,
        0x3df51d4c70439a2f,
        0x3df0375b8b7f66b3,
        0xbd850e412a9bff06,
    ],
    [
        0x3c3fc518d24f616f,
        0xbfbd8293aa55d18f,
        0x3f53b6beb83f212f,
        0x3f93a5ccbc12a602,
        0xbf2a3765d26776da,
        0xbf4f5ab33747e91e,
        0x3ee4df6f1a6da3df,
        0x3ef7cbd49b834b1a,
        0xbe8f9607c8362a02,
        0xbe950b374b4c0d92,
        0x3e2bd1f7180ef6ba,
        0x3e2854abbc0c7de8,
        0xbdbf87db79765a71,
        0xbdb3926b2e69585a,
    ],
    [
        0xbfbd0b36e5737457,
        0x3c726585805a22d8,
        0x3fad082ce3c6b4a2,
        0xbf3905d00c5e9c91,
        0xbf7352b073fcfa33,
        0x3f03f1ccfed800a0,
        0x3f248d74577878fa,
        0xbeb6a9ef1ba885bb,
        0xbec764d8b51b8b1c,
        0x3e5aa78ed7e846ea,
        0x3e608c46d6182272,
        0xbdf33581106d6379,
        0xbdef78fcff7e62ac,
        0x3d832f39fadd44c1,
    ],
    [
        0xbc3cea65a1050db5,
        0x3fbc96700bf039e1,
        0xbf51ec0b5de4bafb,
        0xbf93095734a2441c,
        0x3f27d74e122576e6,
        0x3f4e636fe2585c98,
        0xbee2fe11959a4f56,
        0xbef712e4d39f1e3a,
        0x3e8cc3ac0e3e5a57,
        0x3e946ad2493deefc,
        0xbe295ca72f5034a9,
        0xbe279fa7ce9e0732,
        0x3dbcc7fe67868a0c,
        0x3db30482af82a3e3,
    ],
    [
        0x3fbc29ae8400a31f,
        0xbc70d624180ba1cb,
        0xbfac27138da31b39,
        0x3f36d141fcbed86f,
        0x3f72bdc71061ff60,
        0xbf0231cf645337e2,
        0xbf23f0bf3a855d26,
        0x3eb4b05ea24a407d,
        0x3ec6b52ac7705590,
        0xbe585a82e1962dc0,
        0xbe60126ea6b0d3d5,
        0x3df191f5eda7279d,
        0x3dee96ae83ca14cd,
        0xbd8191df21c5049c,
    ],
    [
        0x3c3a725871d54f1e,
        0xbfbbbf246914235e,
        0x3f5062daee353d6e,
        0x3f927a96f174b658,
        0xbf25cdb5dea7195a,
        0xbf4d818348f8b2ae,
        0x3ee160aab6b91ebc,
        0x3ef6698d6e3dde27,
        0xbe8a56325d99553d,
        0xbe93d7884737e010,
        0x3e273dfa1c71021f,
        0x3e26f8d7f1f40cd1,
        0xbdba675a7a73a904,
        0xbdb28141631b6b6a,
    ],
    [
        0xbfbb5b8273b75054,
        0x3c6ef081b4f49e8c,
        0x3fab59418c36a598,
        0xbf34eafeaa92d6ad,
        0xbf7235801af9154a,
        0x3f00af9747e26a9d,
        0x3f23611db02b9d63,
        0xbeb2fbe420b9b6ee,
        0xbec613cc016f8c79,
        0x3e565cfa070daeea,
        0x3e5f4465aa2f3924,
        0xbdf0262c878a66b9,
        0xbdedc58772bf3be9,
        0x3d802a5900529d85,
    ],
    [
        0xbc384aa4fbafc099,
        0x3fbaf9cb49c4f934,
        0xbf4e1d930b512b68,
        0xbf91f7a8fec6eb30,
        0x3f240a553105f569,
        0x3f4cb20c812efe23,
        0xbedff5195120ac4b,
        0xbef5cdc48eb38532,
        0x3e883b07bbc753fc,
        0x3e934fb5f8f40030,
        0xbe2566435ca657bc,
        0xbe265e90a4422b0e,
        0x3db85513c8865e5e,
        0x3db2077cf853887e,
    ],
    [
        0x3fba9e13a0db6429,
        0xbc6c8fc49071e774,
        0xbfaa9c1ca2161ab5,
        0x3f3344a09efdef03,
        0x3f71b82c43097eb4,
        0xbefebfb97beaa2a2,
        0xbf22dcdb1b1095b7,
        0x3eb180048a016cca,
        0x3ec57eee38f33b34,
        0xbe54a0cd96cea7fb,
        0xbe5e74d5d6cab4bf,
        0x3dedd0d2df39d680,
        0x3ded0395b2b002c8,
        0xbd7ddf4961633a0a,
    ],
    [
        0x3c366129d7cdda38,
        0xbfba4407e04298d1,
        0x3f4bcc9df0cefa78,
        0x3f917f0266db20d1,
        0xbf2280a052210834,
        0xbf4bf2ada1f36d37,
        0x3edd83d57dbfecdc,
        0x3ef53dd97231158c,
        0xbe8663c0bacd7255,
        0xbe92d1fb6736ed8c,
        0x3e23c94599131ea8,
        0x3e25cf6504993c56,
        0xbdb683e80faa06e8,
        0xbdb19631ce482d25,
    ],
    [
        0xbfb9ef3bb2213b0a,
        0x3c6a7968b4e09650,
        0x3fa9ed82007a9965,
        0xbf31d2fdeeb2c55d,
        0xbf71446866fe7a9f,
        0x3efc73b6851770db,
        0x3f22628de4e7b12f,
        0xbeb03303cb6b68e6,
        0xbec4f50f5682c560,
        0x3e531ae61db4a107,
        0x3e5db4387e5cde8e,
        0xbdeba1fde369500d,
        0xbdec4f2d9a6ca338,
        0x3d7bb4d1335b858d,
    ],
    [
        0xbc34b2fde0d60fa7,
        0x3fb99be744018c90,
        0xbf49c3f52a2af15f,
        0xbf910f5ca51f983b,
        0x3f2126c8e8c80fca,
        0x3f4b416f7d4ef26a,
        0xbedb5e2e533b6e90,
        0xbef4b86226f8434d,
        0x3e84c505ef1872eb,
        0x3e925d2f3adca31c,
        0xbe225d5434e81821,
        0xbe254a1c99a03af6,
        0x3db4e94bd07d8a6f,
        0x3db12c7cbd69804c,
    ],
    [
        0x3fb94d3276914e50,
        0xbc68a054fb407a48,
        0xbfa94bac1950e23d,
        0x3f308d4ff8f228ce,
        0x3f70d90d29bf518f,
        0xbefa6d56164ba1ad,
        0xbf21f107d97a6716,
        0x3eae1a62755de03b,
        0x3ec474ea4fd020bb,
        0xbe51c2774b54b19c,
        0xbe5d00e34f95d0da,
        0x3de9b39b1acf50d9,
        0x3deba6dd96aebb23,
        0xbd79c96d87e11eb2,
    ],
    [
        0x3c3336a57f397478,
        0xbfb8ffc9bd24fe07,
        0x3f47f7d46ab331c5,
        0x3f90a7a725d3fb50,
        0xbf1fea1728ee3283,
        0xbf4a9cac69f01f7f,
        0x3ed977f48dd3df20,
        0x3ef43c2d8dc63c79,
        0xbe8355d08ef44310,
        0xbe91f054ae49cd66,
        0x3e211ab3e0c31baf,
        0x3e24cdaac969d4dd,
        0xbdb37cc6ee5acaa3,
        0xbdb0c99a10f9a149,
    ],
    [
        0xbfb8b67a2481077c,
        0x3c66ff282f533f22,
        0x3fa8b51f21068dcb,
        0xbf2ed935c7af3be8,
        0xbf707522a502e55b,
        0x3ef8a1960639d120,
        0x3f21874a473e56eb,
        0xbeac10cf4666ac95,
        0xbec3fd6b83d91ed3,
        0x3e509072f594172b,
        0x3e5c5969c0715bb8,
        0xbde7fbce7fa1d168,
        0xbdeb09679444c7c3,
        0x3d7813cf0f88ee50,
    ],
    [
        0xbc31df60e9bfe4d4,
        0x3fb86e51be0a9153,
        0xbf465ed1b387e0dc,
        0xbf9046fc5a218a13,
        0x3f1dca617fec07ec,
        0x3f4a030022145da6,
        0xbed7c761870dcbbb,
        0xbef3c83888dc1ceb,
        0x3e820edd9a880dbb,
        0x3e918a9391ba3964,
        0xbe1ff64d38db85c5,
        0xbe245927a9c55d79,
        0x3db2377b4d9f1923,
        0x3db06cdd9727d79f,
    ],
    [
        0x3fb829d06fee9265,
        0xbc6580de45a47453,
        0xbfa8289a526d76b3,
        0x3f2cd680355cdc28,
        0x3f7017d70f5091c7,
        0xbef707978e429e47,
        0xbf21247ce0bc7ead,
        0x3eaa3f6135c91ad4,
        0x3ec38da7a255e74a,
        0xbe4efe445dfcd93f,
        0xbe5bbc925c9c4b66,
        0x3de6729121dc2aec,
        0x3dea75b6fa634294,
        0xbd768bad7f03cc70,
    ],
    [
        0x3c30ac9cf88bc679,
        0xbfb7e656efb009ad,
        0x3f44f15066f3d3cc,
        0x3f8fd932c26aacb2,
        0xbf1be460dd833bb1,
        0xbf49733b5917b1ec,
        0x3ed64488c387546b,
        0x3ef35ba58b547387,
        0xbe80ea46c863072a,
        0xbe912b31edd1db5a,
        0x3e1df32c5fd2f995,
        0x3e23ebca247be24d,
        0xbdb113cb7b7c70db,
        0xbdb015b1107de244,
    ],
    [
        0xbfb7a62320798174,
        0x3c9957b1463c023c,
        0x3fa7a50ca4504ab9,
        0xbf2b095ccb52d0c4,
        0xbf6f80ef11d944d8,
        0x3ef59822dd4acc8e,
        0x3f20c7e6a7116068,
        0xbea89e01408239eb,
        0xbec324d470ec229a,
        0x3e4d13ff680fb32a,
        0x3e5b2943a9554368,
        0xbde5283c9b463c57,
        0xbde9e8488fabd47c,
        0x3d7a620fb02a1ce9,
    ],
];