firstreturn.py

Cited on: FLUSH.

To run it: save firstreturn.py, with flush.py, hull.py, induct.py, keyweld.py, ostrowski.py, tie.py beside it; standard library only.

"""
firstreturn.py -- the class step of the integer reader's key window by
the rotation's first return into a gap, against keyweld.py's norm-form
certificate.

QUESTION. At c_inf the real window V(t, f) has forbidden pieces after a
reply (keyweld.py::forbidden), and the hull set holds no key inside
any: the class step. keyweld.py's norm form certifies 7 of the 22
pieces. A key inside a piece (y_a, y_b), L = y_b - y_a, differs from an
end E (a lattice key) by v with y(v) in (0, L) from E_a or in (-L, 0)
from E_b. Let h-(E) < 0 < h+(E) be the nearest G(v) on either side
with y(v) in that one-sided interval: the first returns of the
rotation by r_t into it (Slater's three-gap theorem). Then no key
inside has G strictly between G_E + h- and G_E + h+, since G(v) = 0
forces y(v) an integer, 0 as L < 1. (Q) Does one end's first-return window hold the
hull's whole G-range at the piece, at every one of the 22?

DERIVED BY HAND (before the engine; the numbers read off hull.py's
and keyweld.py's functions at bronze x3, c = c_inf = 2, phase 0).
  alpha = r_0 = [0; 3, 3, ...] = (sqrt 13 - 3)/2, 1/alpha = alpha + 3,
  so y u = H^2 + 3GH - G^2 (den = 1) and kappa sqrt 13 = 1: Z = G +
  kappa y. The zero reply leaves three open pieces on each flag,
  (0.02012, 0.02521), (0.1118, 0.11688), (0.20347, 0.20856), each a
  translate of the first by the key (3, 1) (y = |theta_1| = 1 - 3
  alpha). The first's ends are E_a = (317, 96), Z 317.006, and E_b =
  (99, 30), Z 99.007, E_b being the reduced flag's top hull key (Z =
  Z_hi(0, R)); they differ by 2 (q_4, p_4) = 2 (109, 33), so L = 2
  |theta_4| = 2 alpha^5 = 0.00509 and N(E_a - E_b) = -4, whence |Z_b -
  Z_a| = 4 mu / L exactly: the norm certificate's middle test fails by
  equality, and its low side reads margin 0.70 (full flag) and 0.93
  (reduced). The hull's keys have G -4 .. 29 on the full flag (Z_lo
  -3.94, Z_hi 29.98) and 26 .. 99 on the reduced (Z_lo 26.04, Z_hi
  99.007); the DESIGN's range formula reads -4 .. 30 and 26 .. 100. The nearest keys
  inside the first piece: (208, 63) = E_b + (109, 33), its midpoint,
  Z 208.006, and (-152, -46) = E_b - (251, 76), 251 = 2 q_4 + q_3, Z
  -151.99; so from E_b, h+ = 109 and h- = -251, the window (-152, 208)
  holds both flags' key ranges, by 148 and 109 at the near sides (108
  by the formula's 100). The norm
  form prices the same v at |Z(v)| >= mu / L = 54.5: it charges every
  v the piece's whole length, while Lagrange's bound gives |G(v)| >=
  q_4 = 109 for |y(v)| < L <= |theta_3|, the norm bound being attained
  only at |y(v)| = |theta_4| = L / 2. The other two pieces read the
  same h+ and h-, shifted by (3, 1); their norm margins differ (full
  0.68, 0.67; reduced 0.90, 0.87).

DESIGN (frozen before the engine). Cells, windows, hulls and pieces as
keyweld.py (m = 2 .. 5, --wide to 9), at c_inf. Per piece and each
end that is a lattice key, h+ and h- by exact enumeration of G(v) over
|G(v)| <= B, B = max over the range of |G - G_E| plus a margin
4 (Z_hi - Z_lo) + 4 that only widens what is read, at the piece's flag, a side with no return inside B read as
beyond it (that side then holds the range); the hull's G-range: G
from floor(Z_lo - kappa y_b) to ceil(Z_hi - kappa y_a). A piece is CERTIFIED when for some end both the range's least G
exceeds G_E + h- and its greatest falls below G_E + h+ (a closed end
read directly, as keyweld.py's certify). Beside it, h+ and h- from
r_t's continued fraction by the three-gap theorem, the
enumeration its reference.

THE THREE-GAP SIDES BY HAND (before (P2)'s code). Write r = r_t =
[0; a_1, a_2, ...] with a_k = a_(t+k), q_(-1) = 0, q_0 = 1, theta_(-1)
= -1, theta_0 = r, theta_(k+1) = a_(k+1) theta_k + theta_(k-1), so
theta_k = q_k r - p_k has sign (-1)^k and |theta_k| falls. A key E_a
+ v inside the piece has y(v) = dH - dG r in (0, L), so dH = ceil(dG
r) and the offset is {-dG r} for dG > 0 and {n r} for dG = -n < 0;
from E_b, y(v) in (-L, 0) reads {n r} at dG = n and {-n r} at dG = -n.
So two counts carry both ends: n+(L), the least n >= 1 with {n r} <
L, and n-(L), the least n >= 1 with {-n r} < L; then from E_a, h+ =
n-(L) and h- = -n+(L), and from E_b, h+ = n+(L) and h- = -n-(L). The
records of {n r} are n = q_i + j q_(i+1), i even, j = 0 .. a_(i+2),
at value |theta_i| - j |theta_(i+1)| (falling from |theta_i| to
|theta_(i+2)|); those of {-n r} the same with i odd, from i = -1 (n =
j, value 1 - j r). Each side: take the first i of its parity (from 0,
resp. -1) with |theta_(i+2)| < L; then n = q_i if |theta_i| < L (only
at i = 0), else n = q_i + j q_(i+1) with j = floor((|theta_i| - L) /
|theta_(i+1)|) + 1, at most a_(i+2) since |theta_(i+2)| < L.
Bronze x3: |theta_k| = alpha^(k+1), q = 1, 3, 10, 33, 109, L = 2
alpha^5. n+: i = 2 (alpha^5 < L <= alpha^3), j = floor(1/alpha - 2
alpha) + 1 = floor(2.697) + 1 = 3, n = 10 + 3 * 33 = 109. n-: i = 3
(alpha^6 < L <= alpha^4), j = floor(1/alpha - 2) + 1 = 2, n = 33 + 2
* 109 = 251. From E_b, h+ = 109 and h- = -251: the derivation's.

PREDICTIONS (frozen). (P1) every piece certified, at all 22. (P2) the
three-gap h+, h- equal the enumerated ones per side read, a side
beyond B matching any three-gap |h| > B.
KILL: "uncertified pieces at c_inf: n of 22", n > 0; and for (P2)
"three-gap h != enumerated h at n sides", n > 0. A certified piece
holding a key of the hull is an instrument fault (the window's
exclusion is proved), printed apart.

CONTROLS (read before the verdict). (a) bronze x3's first piece: E_b =
(99, 30), h+ = 109, h- = -251 on the reduced flag (B = 369), and on
the full flag (B = 242.7) h+ = 109 and h- beyond B, as derived. (b) SOUNDNESS, as
keyweld.py's (c): at every c from the first with pinned moves to
c_inf, every stranded (key, reply) pair of H(c) inside a piece lies in
an uncertified one. (c) THE PLANT, in the direction it pushes: h+ and
h- doubled must certify some piece holding a stranded pair below
c_inf, so (b) can fire. (d) the enumeration bound: with B doubled, each
side read inside B unchanged, and each side beyond B still beyond B
or read with |h| > B (it reads nothing and left the script: FINDINGS).

AFTER THE FREEZE, before any engine: the bound was 4 (Z_hi - Z_lo) +
4 alone, 139.7 at bronze x3's full flag, below |h-| = 251, so (a)
could not print and (d) would fire; B gained the range's reach from
G_E and the reading of a side beyond it; (d) and (P2) read per side
(the first repair of (d), "where read", still fired at the full
flag once B doubled).

FINDINGS (the --wide run, copied from its prints; the bare run prints
the same pieces, P1, P2 and (a), with (b) at 159 pairs and (c) at 34,
its cells being m = 2 .. 5).
  CONTROLS. (a) bronze x3's first piece, E_b = (99, 30): full flag B
      242.67, h+ 109, h- beyond B; reduced B 368.89, h+ 109, h- -251;
      as derived. (b) 1165 stranded (key, reply) pairs of H(c), c <=
      c_inf, lie in pieces, 0 in a certified one (keyweld.py's control
      (c) counts the same 1165). (c) h+ and h- doubled certify pieces
      holding 48 stranded pairs: (b) can fire. (d) B doubled: 0 of 88
      sides changed or brought inside at |h| <= B; it reads nothing,
      as enum_side returns the least n, which no larger B can move,
      and it left the script after the run. The fault print (a
      certified piece holding a stranded pair at
      c_inf) prints 0 on an empty population: keyweld.py's (c) finds
      no stranded pair at c_inf.
  P1, KILL MISSED. Uncertified pieces at c_inf: 0 of 22; per cell
      (pieces, certified) golden x2 (2, 2), silver x2 (4, 4), bronze x3
      (6, 6), V1 x2 (6, 6), V1 x3 (2, 2), V2 x4 (2, 2). At bronze x3 only
      E_b's window holds the range (E_a's low margin is -182 to -218);
      at the other 16 pieces both ends' do. The least margin of a
      holding window is 3, at golden x2's full flag, both ends' low side.
  P2, KILL MISSED. Three-gap h != enumerated h at 0 sides: 80 read
      inside B agree, 8 beyond B carry three-gap |h| > B: E_b's h- at
      bronze x3's 3 full-flag pieces, E_b's h+ at silver x2's 4, and
      E_a's h+ at V1 x2's first t = 2 reduced-flag piece.
      (n+, n-) per cell: golden x2 (13, 21), silver x2 (99, 70), bronze
      x3 (109, 251), V1 x2 (19, 31) at t = 1 and (29, 40) at t = 2, V1
      x3 (69, 50), V2 x4 (251, 198): 7 distinct (r_t, L), toy-scale,
      none reaching three_gap's n = q_0 branch.
  So the class step at every piece read is one end's first-return
  window, and the window is r_t's records at the piece's length L.

ARGUED AFTER THE RUN. c_inf is the least c with pinned moves at which
every piece passes, at all 48 (rule). The certificate is a proof
(kappa_t > 0, so Z = G + kappa_t y puts every hull key of the piece in
the G-range; a key strictly inside a window is ruled out by the first
returns, dG = 0 forcing v = 0 as L < len V < 1): a passing piece holds
no hull key. A key of H(c) is stranded
after reply d iff it lies in one of that reply's pieces (forbidden is
built so; keyweld.py's control (e), 0 apart at c <= c_inf). At c <
c_inf with pinned moves H(c) has a stranded key (hull.py's HULL-WI:
the first c whose hull strands nothing is c_inf at all 48), so some
piece fails. At c_inf the 22 pieces all lie at the 6 cells above
(the per-cell table) and all pass; the other 42 have none.

DERIVED AFTER THE RUN (by hand, read off induct.py's Field.valid; its
print was added after the run). The full window is
V(t, F) = [-P_1 - m R_0, P_0 - m R_1],
P_k = |theta_(t+k) / theta_(t-1)|, R the sorted pair (-1)^c P_c,
(-1)^(c+1) P_(c+1), so len V(t, F) = P_0 + P_1 - m (P_c + P_(c+1)).
The zero reply's gap between consecutive translates is r_(t+1) - len
V(t+1, F), and its preimage, scaled by r_t, has length, in units of
|theta_(t-1)|,
    L = m (|theta_(t+c+1)| + |theta_(t+c+2)|) - |theta_(t+2)|,
positive exactly where c_ov's bar fails at phase t + 1. Bronze x3, t = 0, c
= 2: 3 (alpha^4 + alpha^5) - alpha^3 = alpha^3 (3 alpha + 3 alpha^2 -
1) = 2 alpha^5, as 3 alpha = 1 - alpha^2. Golden x2, c = 3: 2 (phi^-5 +
phi^-6) - phi^-3 = phi^-4 (2 - phi) = phi^-6. Both as printed, and
the print of L against l_formula reads 0 of 22 zero-reply pieces
apart, exactly, at the bare and --wide runs (in a scratch copy with
c + 1 put for c, 22 of 22 apart: it can fire, though the script makes
no such print); so none of the 22 is clipped. A piece clipped at an
end of V(t, f) is shorter. So, unclipped,
the window's side is q-scale in alpha's coordinates: n+ and n- are
r_t's records at that L. The ends' G_E should be integer
combinations, with m, of the U of theta_(t+j) = U theta_t + V
theta_(t-1) (induct.py's uv read from phase t - 1; at bronze 99 = 3 *
33 and 317 = 99 + 2 * 109), not derived; the hull's G-range is Z_lo,
Z_hi less kappa_t y, and Z_lo, Z_hi are the Z of integer keys in the
U_k, V_k of q_(n+k) = U_k q_n + V_k q_(n-1), the policy argued and the
starts read, at c_inf at decide.py's 136 cells (hullform.py).

RUN RECORD. Bare 1.3 s, --wide 2.8 s. The engine was written whole
after the hand derivation of the three-gap sides and run once bare,
once --wide, nothing changed between. After the run control (d) left,
the piece-length print was added (every earlier line unchanged), and
the verdicts were made the exit code: 0 iff (a) holds as printed, (b)
finds stranded pairs and none in a certified piece nor a fault, (c)
certifies a piece holding one, P1's 0 of 22 with its per-cell table,
P2's 80 read and 8 beyond B with
0 sides apart, and the length's 0 of 22. --wide 2.8 s, peak commit 8.9
MB.

Usage: python firstreturn.py [--wide]   (--wide adds m = 6 .. 9)
"""

import math
import os
import sys
import time

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
from flush import PERIODIC  # noqa: E402
from induct import Field, Window, least, QF, le  # noqa: E402
from hull import Coords, hull, hull_set, eq  # noqa: E402
from keyweld import forbidden, lattice_key, lt, stranded  # noqa: E402

WIDE = "--wide" in sys.argv


def abs_q(x):
    return x if x.sign() >= 0 else QF(0) - x


def frac_up(n, r):
    """{-n r} = ceil(n r) - n r, exact, n > 0."""
    y = QF(math.ceil(n * r.f)) - r * n
    if y.sign() <= 0:
        y = y + QF(1)
    elif not lt(y, QF(1)):
        y = y - QF(1)
    assert y.sign() > 0 and lt(y, QF(1))
    return y


def enum_side(r, L, B, up):
    """The least n in 1 .. floor(B) with {-n r} < L (up) or {n r} < L,
    else None (beyond B)."""
    for n in range(1, math.floor(B) + 1):
        y = frac_up(n, r)
        if not up:
            y = QF(1) - y
        if lt(y, L):
            return n
    return None


def three_gap(F, t, L):
    """(n+, n-) from r_t's records, as derived by hand."""
    r = F.r[t]
    assert math.floor(1 / r.f) == F.a(t + 1)
    th = {-1: QF(-1), 0: r}
    q = {-1: 0, 0: 1}
    k = 0
    while not (lt(abs_q(th[k]), L) and lt(abs_q(th[k - 1]), L)):
        a = F.a(t + k + 1)
        th[k + 1] = th[k] * a + th[k - 1]
        q[k + 1] = q[k] * a + q[k - 1]
        assert lt(abs_q(th[k + 1]), abs_q(th[k]))
        assert th[k + 1].sign() == (-1) ** (k + 1)
        k += 1
    th[k + 1] = th[k] * F.a(t + k + 1) + th[k - 1]
    out = []
    for i0 in (0, -1):
        i = i0
        while not lt(abs_q(th[i + 2]), L):
            i += 2
        if lt(abs_q(th[i]), L):
            out.append(q[i])
            continue
        num, den = abs_q(th[i]) - L, abs_q(th[i + 1])
        j = math.floor(num.f / den.f) + 1          # exact floor + 1:
        while j > 1 and lt(num, den * (j - 1)):
            j -= 1
        while le(den * j, num):
            j += 1
        assert 1 <= j <= F.a(t + i + 2)
        out.append(q[i] + j * q[i + 1])
    return out[0], out[1]


def l_formula(F, t, m, c):
    """m (|theta_(c+1)| + |theta_(c+2)|) - |theta_2|, r_t's own theta's
    (theta_(-1) = -1, theta_0 = r_t): the unclipped zero-reply piece's
    length, derived after the run."""
    th = {-1: QF(-1), 0: F.r[t]}
    for k in range(c + 2):
        th[k + 1] = th[k] * F.a(t + k + 1) + th[k - 1]
    return (abs_q(th[c + 1]) + abs_q(th[c + 2])) * m - abs_q(th[2])


def g_range(co, t, ya, yb, zlo, zhi):
    k = co.kap[t]
    return (math.floor(zlo.f - k.f * yb.f),
            math.ceil(zhi.f - k.f * ya.f))


def read_piece(F, co, t, pc, zlo, zhi, bmul=1):
    """Per end that is a lattice key: (side, E, G_E, B, h+, h-) by
    enumeration, None for a side beyond B; and the G-range."""
    ya, yb, ca, cb = pc
    L = yb - ya
    glo, ghi = g_range(co, t, ya, yb, zlo, zhi)
    span = 4 * (zhi.f - zlo.f) + 4
    r = F.r[t]
    ends = []
    for side, y in (("a", ya), ("b", yb)):
        E = lattice_key(F, t, y)
        if E is None:
            continue
        GE = E[0]
        B = bmul * (max(abs(glo - GE), abs(ghi - GE)) + span)
        hp = hm = None
        if L.sign() > 0:
            # from E_a: h+ reads {-n r}, h- reads {n r}; E_b the mirror
            hp = enum_side(r, L, B, up=(side == "a"))
            hm = enum_side(r, L, B, up=(side == "b"))
        ends.append((side, E, GE, B, hp, None if hm is None else -hm))
    return ends, (glo, ghi)


def certified(F, co, t, pc, zlo, zhi, ends, grange, scale=1):
    """No key of the hull in the piece: no closed end in the hull, and
    some end's first-return window holds the G-range."""
    ya, yb, ca, cb = pc
    for closed, y in ((ca, ya), (cb, yb)):
        if closed:
            E = lattice_key(F, t, y)
            if E is None:
                return False
            z = co.Z(*E, t)
            if le(zlo, z) and le(z, zhi):
                return False
    if not lt(ya, yb):
        return True
    glo, ghi = grange
    for side, E, GE, B, hp, hm in ends:
        lo_ok = hm is None or glo > GE + scale * hm
        hi_ok = hp is None or ghi < GE + scale * hp
        if lo_ok and hi_ok:
            return True
    return False


def inside(y, pc):
    ya, yb, ca, cb = pc
    return ((le(ya, y) if ca else lt(ya, y)) and
            (le(y, yb) if cb else lt(y, yb)))


def main():
    t0 = time.time()
    maps = (2, 3, 4, 5) + ((6, 7, 8, 9) if WIDE else ())
    pieces = cert_n = 0
    unc, rows, per_cell = [], [], {}
    p2_read = p2_bad = p2_beyond = p2_beyond_bad = 0
    lf_n = lf_bad = 0
    sound_n = sound_bad = plant_hit = fault = 0
    ctl_a = []
    for name, per in PERIODIC:
        F = Field(per)
        p = F.p
        cname = name.split()[0]
        for m in maps:
            cinf = least(F, m, "pin")
            for c in range(cinf + 1):
                win = Window(F, m, c)
                st, miss = win.pin_starts()
                if miss:
                    continue
                co = Coords(F, m, c)
                zhi, _ = hull(win, co, st)
                zlo, _ = hull(win, co, st, low=True)
                Hs = hull_set(win, co, zlo, zhi)
                strand = stranded(win, Hs)
                cert = {}
                for t in range(p):
                    for f in (True, False):
                        for d in win.replies(f, t):
                            for pc in forbidden(win, t, f, d):
                                zl, zh = zlo[(t, f)], zhi[(t, f)]
                                ends, gr = read_piece(F, co, t, pc, zl, zh)
                                ok = certified(F, co, t, pc, zl, zh, ends,
                                               gr)
                                okp = certified(F, co, t, pc, zl, zh, ends,
                                                gr, scale=2)
                                cert[(t, f, d, pc)] = (ok, okp)
                                if c != cinf:
                                    continue
                                pieces += 1
                                cert_n += ok
                                key = f"{cname} x{m}"
                                a0, b0 = per_cell.get(key, (0, 0))
                                per_cell[key] = (a0 + 1, b0 + ok)
                                if not ok:
                                    unc.append((key, t, int(f), d))
                                L = pc[1] - pc[0]
                                if d == 0:
                                    lf_n += 1
                                    lf_bad += not eq(L, l_formula(F, t, m,
                                                                  c))
                                tg = (three_gap(F, t, L) if L.sign() > 0
                                      else None)
                                for side, E, GE, B, hp, hm in ends:
                                    if tg is not None:
                                        npl, nmi = tg
                                        w_p = nmi if side == "a" else npl
                                        w_m = -(npl if side == "a" else nmi)
                                        for h, w in ((hp, w_p), (hm, w_m)):
                                            if h is not None:
                                                p2_read += 1
                                                p2_bad += h != w
                                            else:
                                                p2_beyond += 1
                                                p2_beyond_bad += abs(w) <= B
                                    mhi = None if hp is None else GE + hp - gr[1]
                                    mlo = None if hm is None else gr[0] - GE - hm
                                    rows.append((key, t, int(f), d,
                                                 round(pc[0].f, 5),
                                                 round(L.f, 6), side, E,
                                                 gr, round(B, 1), hm, hp,
                                                 mlo, mhi, ok, tg))
                                if (key == "bronze x3" and t == 0 and d == 0
                                        and abs(pc[0].f - 0.02012) < 1e-4):
                                    for side, E, GE, B, hp, hm in ends:
                                        if side == "b":
                                            ctl_a.append((int(f), E,
                                                          round(B, 2),
                                                          hp, hm))
                for (G, H, f, t), d in strand:
                    y = QF(H) - F.r[t] * G
                    for (t2, f2, d2, pc), (ok, okp) in cert.items():
                        if (t2, f2, d2) != (t, f, d) or not inside(y, pc):
                            continue
                        sound_n += 1
                        sound_bad += ok
                        plant_hit += okp
                        fault += ok and c == cinf
            print(f"    {name:20s} x{m} c_inf {cinf}", flush=True)
    print("== PIECES at c_inf: (cell, t, f, d, y_a, L, end, E, G-range, B, "
          "h-, h+, margin lo, margin hi, certified, three-gap (n+, n-))")
    for row in rows:
        print("  ", row)
    print("== CONTROLS")
    print(f"  (a) bronze x3, first piece, end E_b (flag, E, B, h+, h-): "
          f"{ctl_a}")
    print(f"  (b) SOUNDNESS: stranded (key, reply) pairs of H(c), c <= "
          f"c_inf, inside a piece: {sound_n}; in a certified one: "
          f"{sound_bad}")
    print(f"  (c) THE PLANT (h+, h- doubled): stranded pairs in a piece "
          f"it certifies: {plant_hit}")
    print(f"  instrument fault (a certified piece holding a key of "
          f"H(c_inf)): {fault}")
    print("== P1")
    print(f"  per cell (pieces, certified): {per_cell}")
    print(f"  uncertified: {unc}")
    print(f"  KILL: uncertified pieces at c_inf: {pieces - cert_n} of "
          f"{pieces}")
    print("== P2")
    print(f"  sides read inside B: {p2_read}; beyond B: {p2_beyond}, "
          f"three-gap |h| <= B there: {p2_beyond_bad}")
    print(f"  KILL: three-gap h != enumerated h at "
          f"{p2_bad + p2_beyond_bad} sides")
    print("== THE PIECE LENGTH (derived after the run)")
    print(f"  zero-reply pieces at c_inf whose L != m(|theta_(c+1)| + "
          f"|theta_(c+2)|) - |theta_2|, r_t's own theta's: {lf_bad} of "
          f"{lf_n}")
    checks = [
        ctl_a == [(1, (99, 30), 242.67, 109, None),
                  (0, (99, 30), 368.89, 109, -251)],
        sound_n > 0 and sound_bad == 0 and fault == 0, plant_hit > 0,
        pieces == 22 and cert_n == 22 and not unc,
        per_cell == {"golden x2": (2, 2), "silver x2": (4, 4),
                     "bronze x3": (6, 6), "V1 x2": (6, 6),
                     "V1 x3": (2, 2), "V2 x4": (2, 2)},
        (p2_read, p2_beyond, p2_bad, p2_beyond_bad) == (80, 8, 0, 0),
        (lf_n, lf_bad) == (22, 0),
    ]
    print(f"  {sum(checks)}/{len(checks)} checks as recorded, "
          f"{time.time() - t0:.1f} s")
    sys.exit(0 if all(checks) else 1)


if __name__ == "__main__":
    main()