rays.py

Checks: COLLIDE: Signed pentanomials theorem.

Cited on: COLLIDE.

To run it: save rays.py; needs flint, numpy.

"""rays.py -- whether a signed pentanomial's survivors can fill a plane:
the shared factor of a 5-term Laurent polynomial in two variables and
its reversal.

QUESTION. A SURVIVOR is a signed f = 1 + s1 x^q + s2 x^p + s3 x^m +
s4 x^n, e = (q, p, m, n) ADMISSIBLE (0 < q < p < m < n), not
+-reciprocal, with a non-cyclotomic factor in gcd(f, f~). With
G(x1..x4) = 1 + sum s_i x_i and H = x1 x2 x3 x4 G(1/x),
f = G(x^e) and H(x^e) = x^(q + p + m) f~ (x^n f(1/x) = f~), so a survivor
is exactly an e at which G(x^e) and H(x^e) share a non-cyclotomic factor.

THEOREM 3 OF FILASETA AND KALOGIROU (arXiv:2508.12242, Bombieri and
Zannier, 1998), as printed: for k >= 2, n1 < ... < nk positive and G, H
in Z[x1..xk] relatively prime in Q[x1..xk], if G(x^n1, ..., x^nk) and
H(x^n1, ..., x^nk) share a non-cyclotomic irreducible factor then j . n
= 0 for some j in Z^k, not all 0, with sum |j_i| <= C(G, H), a computable
constant depending only on G and H (also E. Bombieri, D. Masser and U.
Zannier, IMRN 2007, Theorem 1.6, not read here; their structure
theorem may hold the reduction). Its proof is not printed there. The
condition it reaches is exactly the survivor condition, and its constant
is effective.

THE REDUCTION (by hand). Restrict to a hyperplane j . e = 0, e = M t,
t in Z^3, M's columns a basis of its lattice: G_M(y) = G(y^M) = 1 + sum
s_i y^(r_i), r_i the rows of M, H_M ~ G_M(1/y), and f_e = G_M(x^t). A
sublattice on which two of 0, r_1..r_4 coincide lies in e_i = e_j or
e_i = 0 and holds no admissible e, so G_M has 5 terms. THE CHAMBERS:
Theorem 3 wants 0 < t_1 < t_2 < t_3. The planes t_i = 0 and t_i = +-t_j
cut Z^3 into finitely many open chambers, each fixing the signs of the
t_i and the order of the |t_i|; in each, a permutation and an inversion
of the y_i, times a monomial, gives a polynomial pair whose exponents
are positive and increasing, the specialization changing by a
power of x, which no survivor's factor is (f(0) = 1). The walls are
rank-2 sublattices, recursed on in turn. Either G_M and G_M(1/y) share a
factor of measure > 1 (CASE A), or their gcd E has measure 1, so is a
product of monomials and extended cyclotomic polynomials Phi_m(y^v)
(D. W. Boyd, Kronecker's theorem and Lehmer's problem for polynomials in
several variables, J. Number Theory 13 (1981) 116-121), every
irreducible factor of E(x^t) is cyclotomic or x, and a survivor's shared
factor divides both coprime cofactors at x^t: Theorem 3 again, a
hyperplane in t. The recursion ends at rank 1, where the admissible
half of a line Z v holds survivors at every point or at none (f_(tv)(x)
= f_v(x^t), and gcd(a(x^t), b(x^t)) = gcd(a, b)(x^t)): a ray. At rank
k the rows r_i span R^k, so G_M's support has affine rank k. A CASE A
sublattice of rank 3 restricts to rank 2:
Lawton's theorem (W. M. Lawton, J. Number Theory 16 (1983) 356-362:
M(Q(x^r)) -> M(Q) as q(r) -> oo, q(r) the least height, max |s_i|, of
a nonzero s with s . r = 0), applied to D and to D(y^N) with q(N s) >=
min(q(N), q(s)/|N|), gives M(D(y^N)) -> M(D) as q(N) -> oo, q(N) the least
height
of a nonzero s with N^T s = 0, |N| the largest column sum of |N|'s
entries. The kernel of N^T is Z s0, s0 primitive, q(N) = |s0|, and s0
of any height occurs (N a basis of the integer vectors orthogonal to
s0); once q(N) passes Lawton's threshold and exceeds every |r_i - r_j|
and |r_i + r_j - r_k - r_l| (i = j and k = l allowed), N^T is injective
on the points and on their pairwise sums, so G_M(y^N) has 5 terms,
support of affine rank 2 (N^T is onto), and a shared factor of measure
> 1, and a central symmetry of it, r_i + r_pi(i) mapped to one point,
lifts to G_M. Then (R2) makes every CASE A G_M +-reciprocal,
and every f on its sublattice with it: no survivor.
Here (R2) is the bivariate statement:

  (R2) every 5-term +-1 Laurent polynomial G in two variables, its
  support affinely of rank 2, that shares a factor of measure > 1 with
  G(1/y) is +-reciprocal (G(1/y) = +-monomial G).

So Theorem 3 and (R2) put the survivors on finitely many rays, and make
"three rays" a finite computation with the constants C. (R2) is proved
below.

THE PROOF OF (R2) (by hand). G as in (R2), D irreducible of measure > 1
dividing G and G* (G(1/y) times a monomial; D* likewise), P its Newton
polygon.
  SEGMENT. D's Newton polytope is not a segment: else D = mono phi(y^w),
  w primitive,
  phi not cyclotomic, and each coset of Z w meeting the support carries
  a component of G divisible by phi, so of 3 terms at least (a binomial's
  roots are roots of unity); rank 2 puts the support in at least two
  cosets, 6 terms.
  TWO LAYERS. The support does not lie on two parallel lines: write G =
  g0(z) + t^h g1(z) along them. D involves t (else D divides g0 and g1,
  each then of measure > 1 and 3 terms) and z (else D is a segment), so
  its zero curve dominates z,
  where G = G(1/y) = 0 gives g0(z) g0(1/z) = g1(z) g1(1/z) identically,
  so |g0| = |g1| on the circle and, by Jensen's formula in t, M(G) =
  M(g0) = M(g1) >= M(D) > 1: each layer has 3 terms at least, 6 in all.
  PARALLELOGRAM. N(G) has at most 5 edges. If D ~ D*, P is centrally
  symmetric; if not, D* divides G too and D D* does, so P + (-P) is a
  Minkowski summand of N(G). Either way each edge normal of P and of -P
  is one of N(G)'s; that set is closed under negation, so of even size
  at most 5: four, +-n1 and +-n2, and no three of them span the plane
  positively, so P uses all four: a parallelogram, its sides along
  primitive u and v.
  2-1-2. Cut the plane into lines along u. G's face at either normal to
  u is D's face there, an edge of P and so not a monomial, times a
  nonzero face: each outer line holds 2 terms at least, and by TWO
  LAYERS a third line holds one, so the lines carry 2, 1 and 2. Likewise
  along v. With a and b the linear forms constant along u and along v
  (together injective on Z^2), the support sits in a 3 x 3 grid of
  a-values 0 < alpha < A and b-values 0 < beta < B, 2, 1, 2 points to a
  row and to a column: the X (the four corners and the center cell), or
  a SKEW pattern, the middle row's point in an outer column, such as
  (0, 0), (0, B), (alpha, 0), (A, beta), (A, B).
  MIDLINE. With z along u and t across, G = g0(z) + c z^r t^alpha +
  g2(z) t^A, g0 and g2 binomials. D's top face in t divides g2, so has
  measure 1, and Jensen's formula in t makes the integral of the sum of
  log+ |t_i(z)| over D(z, .)'s roots log M(D) > 0: the z with a root off
  the circle have positive measure and, the roots moving continuously,
  hold an arc, shrunk off the zeros of g0 and g2. There a root t0 = rho
  w, |w| = 1, rho != 1, has G(z, t0) = 0, and G*(z, t0) = 0 conjugated
  is G(z, 1/conj(t0)) = 0. With a
  = g0(z), X = c z^r w^alpha, Y = g2(z) w^A: a + X rho^alpha + Y rho^A =
  0 = a + X rho^-alpha + Y rho^-A, a real system of determinant
  rho^(alpha - A) - rho^(A - alpha) != 0, so X/a and Y/a are real and R
  = X^A Y^-alpha a^(alpha - A) = c^A z^(rA) g2^-alpha g0^(alpha - A), w
  cancelled, is real on the arc: R(z) = R(1/z) identically. A +-1
  binomial with exponents i, j has g(1/z) = +-z^-(i + j) g(z), so this
  is a monomial identity, 2 r A = (A - alpha)(i0 + j0) + alpha (i2 +
  j2): the middle term lies on the segment joining the midpoints of the
  two outer pairs. Each outer pair holds two b-values, so that point's
  b lies strictly inside (0, B), and a SKEW pattern's middle point does
  not: the support is the X, its corners p1, p2, p3, p4 with p1 + p4 =
  p2 + p3, and MIDLINE along u and along v puts its fifth point m at
  the center (p1 + p4)/2.
  THE X. Align G* = y^(p1 + p4) G(1/y), c_i the coefficient at p_i, c0
  at m, and e = c1 c4: D divides H = G - e G*, which vanishes at p1 and
  p4. If c3 = e c2, H = (1 - e) c0 y^m, a monomial unless e = 1, G = G*.
  If c3 = -e c2, H = 2 c2 (y^p2 - e y^p3) + (1 - e) c0 y^m is not 0 and
  lies on the diagonal p2 p3, a segment, of which P is no summand. So G
  is +-reciprocal: (R2) holds.

DESIGN. Every 5-point set S in the box [0, B]^2 touching both axes (one
per translate), affinely of rank 2, with the 16 sign vectors fixing the
first point's coefficient at +1; G* = y^(B, B) G(1/y). The gcd of G and
G* over Z[y, z] (flint), factored; a factor is FLAGGED when its Newton
polytope has dimension 2, or dimension 1 with a non-cyclotomic phi. G is
+-RECIPROCAL when G* is +-G after translation.
  C1 detector plants, off the 5-term family: (1 + y + z)(y z + y + z)(1
     + 2y), not +-reciprocal, a 2-dimensional shared factor; and (1 + y -
     y^3)(y^3 + y^2 - 1)(1 + z), a 1-dimensional non-cyclotomic one; each
     flagged twice (D and its reversal both divide), and 1 + 2y + z,
     sharing nothing, not.
  C2 the +-reciprocal family is seen: the set {(1,0), (2,0), (1,1),
     (0,2), (1,2)} (the hyperplane n = 2p = m + q, t = (a, b) -> (a, b,
     2b - a, 2b), shifted) with coefficients (1, s1, s2, s1, 1), so
     G = G* at every sign, is counted +-reciprocal, and its gcd is G.
  C3 the lemmas as a check, over every flagged G, +-reciprocal or not:
     with a segment factor (SEGMENT says 0), on two parallel lines (TWO
     LAYERS says 0).
  C4 the proof's later steps as a check, over every G with a flagged
     2-dimensional factor: its P not a parallelogram; the support not
     the X with m at its center. And MIDLINE's algebra, at 8 points z =
     exp(2 pi i (k + sqrt 2 - 1)/8) of the circle, never a root of
     unity, so g0(z) and g2(z) are not 0: each root t0 of G(z, .) in
     t (z along a side of P) with |t0| > 1 + 1e-6 whose 1/conj(t0) is
     also a root, R(z) computed, the pairs counted and the largest
     |Im R|/|R| printed. A pair count of 0 reads nothing. Every G it
     reads is +-reciprocal (the box holds no other flagged G), so C4
     checks the steps' algebra, never a contrary case.

PREDICTIONS, frozen before the engine. P1 B = 4: no flagged G that is not
+-reciprocal. P2 the +-reciprocal G are flagged unless G is a product of
cyclotomic polynomials in monomials. P3 C3 prints 0 and 0. P4 C4 prints
0 and 0, pairs > 0, and the largest |Im R|/|R| below 1e-9 (the third
count, not on three lines along P's side, was added with the code).

KILL. "flagged, not +-reciprocal: h" over the box B = 4: h >= 1 kills
(R2) as a theorem to seek; the example then names a candidate plane of
survivors, to be read at its generic member.

FINDINGS. C1 ['2d', '2d'], ['1d', '1d'], [] (D and its reversal both
  divide each plant); C2 each of the four sign choices +-reciprocal, gcd
  G. B = 4: "26486 sets of rank 2 (4 collinear skipped), 423776 signed
  G"; "+-reciprocal G: 248, with a flagged factor 248"; "flagged with a
  segment factor: 0; flagged on two parallel lines: 0"; "flagged, not
  +-reciprocal: 0": P1, P2, P3 held, the kill misses. --box 6: "582480
  sets of rank 2 (60 collinear skipped), 9319680 signed G"; "+-reciprocal
  G: 1056, with a flagged factor 1056"; the lemma prints 0 and 0;
  "flagged, not +-reciprocal: 0". So (R2) holds for every support in
  [0, 6]^2 (a rule over that box), and every +-reciprocal G there
  carries a factor of measure > 1. C4 at --box 6: "P not a
  parallelogram: 0; the support not the centered X: 0; not on three
  lines along P's side: 0"; "MIDLINE: 6956 root pairs, largest |Im
  R|/|R| 3.99e-14" (B = 4: 920 pairs, 4.13e-15): P4 held.

RUN RECORD. --rehearse first failed C1: the wanted set held one flag per
plant, forgetting that D and D* both divide it; the detector was right.
Then 3 of 3, B = 2, 0.0 s. B = 4: 3 of 3, 8.8 s, peak commit 12.4 MB;
the lemma prints were then widened to every flagged G. --box 6: 3 of 3,
197.4 s, 12.6 MB. With recip() returning False in a scratch copy, C2
stops the run; with the controls also skipped, the kill fires,
"flagged, not +-reciprocal: 248". C4 first sampled z = exp(2 pi i (k +
1/3)/8), each a root of unity, and failed at --box 6, "largest |Im
R|/|R| 9.85e-01" (and at B = 4, 5.80e-01): at k = 1 the g0 and g2 of
y^6 z^4 + y^6 z^3 + y^3 z^2 + z + 1 both vanish, outside MIDLINE's arc,
and the roots were noise; moved to k + sqrt 2 - 1. Then 4 of 4: B = 4,
9.1 s; --box 6, 205.0 s, peak commit 21.2 MB. With R's exponent of Y
as 1 - alpha in a scratch
copy, --rehearse prints "MIDLINE: 40 root pairs, largest |Im R|/|R|
9.87e-01" and C4 fails. C3 then made a check: B = 4, 5 of 5, 13.1 s;
with layers() returning True in a scratch copy, "flagged on two
parallel lines: 248" and C3 fails. --box 6 at 4 of 4 before it: 208.0
s, peak commit 21.3 MB.

RESOURCE. 26,490 of the C(25, 5) five-sets (those touching both axes)
times 16 signs, a bivariate gcd each, at B = 4 (8.8 s); --box 6 about
20 times that; --rehearse B = 2.
"""
import os
import sys
import time
from itertools import combinations, product
from math import gcd

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")

import flint  # noqa: E402
import numpy as np  # noqa: E402

CHECKS = []
TWO_D = []      # (G, its 2-dimensional flagged factors), filled by the box
SQ2 = 2 ** 0.5
REHEARSE = "--rehearse" in sys.argv
B = 2 if REHEARSE else (int(sys.argv[sys.argv.index("--box") + 1])
                        if "--box" in sys.argv else 4)
CTX = flint.fmpz_mpoly_ctx.get(("y", "z"), "lex")


def check(name, ok, detail=""):
    CHECKS.append(bool(ok))
    tag = "ok  " if ok else "FAIL"
    print(f"  [{tag}] {name}" + (f"  ({detail})" if detail else ""))


def control(name, ok, detail=""):
    check(name, ok, detail)
    if not ok:
        print("  control failed: run stopped")
        raise SystemExit(1)


def poly(terms):
    """terms {(a, b): c} -> fmpz_mpoly, shifted so both minima are 0."""
    a0 = min(a for a, _ in terms)
    b0 = min(b for _, b in terms)
    return CTX.from_dict({(a - a0, b - b0): c for (a, b), c in terms.items()})


def terms_of(P):
    return {tuple(int(x) for x in e): int(c) for e, c in P.to_dict().items()}


def star(P):
    """y^(top) P(1/y), shifted: the reversal."""
    t = terms_of(P)
    return poly({(-a, -b): c for (a, b), c in t.items()})


def rank(points):
    p0 = points[0]
    vs = [(a - p0[0], b - p0[1]) for a, b in points[1:]]
    return 2 if any(u[0] * v[1] - u[1] * v[0] for u in vs for v in vs) else (
        1 if any(v != (0, 0) for v in vs) else 0)


def flagged(D):
    """D irreducible: dimension 2, or 1 with a non-cyclotomic phi."""
    t = terms_of(D)
    pts = sorted(t)
    r = rank(pts)
    if r == 2:
        return "2d"
    if r == 0:
        return None
    lo, hi = pts[0], pts[-1]
    dx, dy = hi[0] - lo[0], hi[1] - lo[1]
    g = gcd(dx, dy)
    w = (dx // g, dy // g)
    k = {((a - lo[0]) // w[0] if w[0] else (b - lo[1]) // w[1]): c
         for (a, b), c in t.items()}
    phi = flint.fmpz_poly([k.get(i, 0) for i in range(max(k) + 1)])
    return None if phi.is_cyclotomic() else "1d"


def recip(P):
    S = star(P)
    return S == P or S == -P


def shared(P):
    """The flagged irreducible factors of gcd(P, P*)."""
    g = P.gcd(star(P))
    if g.total_degree() <= 0:
        return g, []
    _, fl = g.factor()
    return g, [(D, flagged(D)) for D, _ in fl if flagged(D)]


def layers(points):
    """The support lies on two parallel lines."""
    for i, j in combinations(range(5), 2):
        u = (points[j][0] - points[i][0], points[j][1] - points[i][1])
        vals = {u[0] * p[1] - u[1] * p[0] for p in points}
        if len(vals) == 2:
            return True
    return False


def section_controls():
    print("CONTROLS")
    y, z = CTX.gens()
    p1 = (1 + y + z) * (y * z + y + z) * (1 + 2 * y)
    p2 = (1 + y - y ** 3) * (y ** 3 + y ** 2 - 1) * (1 + z)
    p3 = 1 + 2 * y + z
    f1 = [k for _, k in shared(p1)[1]]
    f2 = [k for _, k in shared(p2)[1]]
    f3 = [k for _, k in shared(p3)[1]]
    control("C1 the detector: a 2-dimensional plant, a 1-dimensional "
            "non-cyclotomic plant, and a coprime pair",
            f1 == ["2d", "2d"] and f2 == ["1d", "1d"] and not f3
            and not recip(p1),
            f"{f1}, {f2}, {f3}")
    found = []
    for s1, s2 in product((1, -1), repeat=2):
        P = poly({(1, 0): 1, (2, 0): s1, (1, 1): s2, (0, 2): s1, (1, 2): 1})
        g, fl = shared(P)
        found.append((recip(P), g == P or g == -P, [k for _, k in fl]))
    control("C2 the +-reciprocal plane n = 2p = m + q: each sign choice "
            "+-reciprocal, the gcd G itself", all(a and b for a, b, _ in found),
            f"{found}")


def section_box():
    print(f"BOX -- every signed 5-set in [0, {B}]^2 touching both axes")
    t0 = time.time()
    cells = [(a, b) for a in range(B + 1) for b in range(B + 1)]
    sets = rk1 = 0
    rec, recflag, bad, seg, two = 0, 0, [], 0, 0
    for S in combinations(cells, 5):
        if min(a for a, _ in S) or min(b for _, b in S):
            continue
        if rank(list(S)) < 2:
            rk1 += 1
            continue
        sets += 1
        lay = layers(list(S))
        for sg in product((1, -1), repeat=4):
            P = poly(dict(zip(S, (1,) + sg)))
            g, fl = shared(P)
            if fl:
                seg += any(k == "1d" for _, k in fl)
                two += lay
                if any(k == "2d" for _, k in fl):
                    TWO_D.append((P, [D for D, k in fl if k == "2d"]))
            if recip(P):
                rec += 1
                recflag += bool(fl)
            elif fl:
                bad.append((S, (1,) + sg, [str(D) for D, _ in fl]))
    print(f"    {sets} sets of rank 2 ({rk1} collinear skipped), "
          f"{16 * sets} signed G, {time.time() - t0:.1f} s")
    print(f"    +-reciprocal G: {rec}, with a flagged factor {recflag}")
    print(f"    flagged with a segment factor: {seg}; flagged on two "
          f"parallel lines: {two}")
    check("C3 SEGMENT and TWO LAYERS: no flagged G breaks either",
          seg == two == 0)
    for x in bad[:6]:
        print(f"      {x}")
    print(f"    flagged, not +-reciprocal: {len(bad)}")
    check("KILL no flagged G that is not +-reciprocal", not bad)


def cross(u, v):
    return u[0] * v[1] - u[1] * v[0]


def hull(points):
    """The convex hull's vertices, counterclockwise (monotone chain)."""
    pts = sorted(set(points))
    out = []
    for seq in (pts, pts[::-1]):
        part = []
        for p in seq:
            while len(part) >= 2 and cross(
                    (part[-1][0] - part[-2][0], part[-1][1] - part[-2][1]),
                    (p[0] - part[-1][0], p[1] - part[-1][1])) <= 0:
                part.pop()
            part.append(p)
        out += part[:-1]
    return out


def parallelogram(points):
    """The hull's 4 vertices v0..v3 with v0 + v2 = v1 + v3, or None."""
    v = hull(points)
    if len(v) == 4 and all(v[0][i] + v[2][i] == v[1][i] + v[3][i]
                           for i in (0, 1)):
        return v
    return None


def midline_pairs(G, u):
    """Root pairs t0, 1/conj(t0) of G(z, .) at 8 points z, z along u:
    their count and the largest |Im R|/|R|, or None when G does not sit
    on three lines along u."""
    g = gcd(abs(u[0]), abs(u[1]))
    u = (u[0] // g, u[1] // g)
    _, s, r = ext_gcd(u[0], u[1])       # s u0 + r u1 = 1
    w = (-r, s)                          # det(u, w) = 1
    terms = {(cross(x, w), cross(u, x)): c for x, c in terms_of(G).items()}
    js = sorted({j for _, j in terms})
    if len(js) != 3:
        return None
    j0, alpha, A = js[0], js[1] - js[0], js[2] - js[0]
    pairs, worst = 0, 0.0
    for k in range(8):
        z = np.exp(2j * np.pi * (k + SQ2 - 1) / 8)
        co = [sum(c * z ** i for (i, j), c in terms.items() if j - j0 == d)
              for d in range(A + 1)]
        roots = np.roots(co[::-1])
        for t0 in roots:
            if abs(t0) <= 1 + 1e-6:
                continue
            if min(abs(roots - 1 / np.conj(t0))) > 1e-7:
                continue
            pairs += 1
            wv = t0 / abs(t0)
            a, X, Y = co[0], co[alpha] * wv ** alpha, co[A] * wv ** A
            R = X ** A * Y ** (-alpha) * a ** (alpha - A)
            worst = max(worst, abs(R.imag) / abs(R))
    return pairs, worst


def ext_gcd(a, b):
    if b == 0:
        return (abs(a), 1 if a >= 0 else -1, 0)
    g, x, y = ext_gcd(b, a % b)
    return g, y, x - (a // b) * y


def section_proof():
    print(f"PROOF -- the later steps over the {len(TWO_D)} G with a "
          f"2-dimensional flagged factor")
    notpar = notx = unlayered = pairs = 0
    worst = 0.0
    for G, Ds in TWO_D:
        pts = list(terms_of(G))
        for D in Ds:
            v = parallelogram(list(terms_of(D)))
            if v is None:
                notpar += 1
                continue
            u = (v[1][0] - v[0][0], v[1][1] - v[0][1])
            res = midline_pairs(G, u)
            if res is None:
                unlayered += 1
            else:
                pairs += res[0]
                worst = max(worst, res[1])
        c = parallelogram(pts)
        inner = [p for p in pts if c is None or p not in c]
        if c is None or len(inner) != 1 or any(
                2 * inner[0][i] != c[0][i] + c[2][i] for i in (0, 1)):
            notx += 1
    print(f"    P not a parallelogram: {notpar}; the support not the "
          f"centered X: {notx}; not on three lines along P's side: "
          f"{unlayered}")
    print(f"    MIDLINE: {pairs} root pairs, largest |Im R|/|R| "
          f"{worst:.2e}")
    check("C4 the proof's steps hold and MIDLINE's R is real",
          notpar == notx == unlayered == 0 and pairs > 0 and worst < 1e-9)


def main():
    t0 = time.time()
    section_controls()
    print()
    section_box()
    print()
    section_proof()
    print()
    print(f"{sum(CHECKS)} of {len(CHECKS)} checks, {time.time() - t0:.1f} s")
    return 0 if all(CHECKS) else 1


if __name__ == "__main__":
    sys.exit(main())