"""cert_C3s_v7.py: driver for cert_C3s.lhs_split, the interval certificate of the paper's Lemma 6 (cert_C3s.py imports cert_C2.py and
cert_C3.py).

This driver adds no mathematics: it calls lhs_split(LX, K, delta) for the rows the paper states and prints them in cert_C3s.py's own format.
The interval it prints encloses the left side of the condition of Lemma 6 itself (every truncation is carried as an enclosure), so its
upper end proves the condition and its lower end disproves it, at the stated delta only.
  (e^1800, 18) and (e^1800, 17): Lemma 7, for Theorem 1, and the remark on K = 17;
  (e^350, 14): Lemma 7, for Theorem 2;
  (e^62, 9): Lemma 7, the unconditional first piece of Theorem 3;
  (X_2' = exp(2736.86), 18): the remark after the proof of Theorem 1 (left side > 0.628287);
  (e^73, 8): Remark 26 (the left side at e^73 with K = 8 is about 1.004).
"""
import hashlib, math, os, sys
from fractions import Fraction
from mpmath import iv, mpf
import cert_C3s as C3s

HERE = os.path.dirname(os.path.abspath(__file__))
SHA = hashlib.sha256(open(os.path.join(HERE, 'cert_C3s.py'), 'rb').read()).hexdigest()[:8]

if __name__ == '__main__':
    print(f"# python3 {sys.version.split()[0]} + mpmath iv ({iv.prec} bits); cert_C3s.lhs_split (sha {SHA}), v7 paper rows")
    for (LX, K, delta) in [('1800', 18, Fraction(1, 5)), ('1800', 17, Fraction(1, 5)), ('350', 14, Fraction(1, 5)), ('62', 9, Fraction(1, 5)),
                           ('2736.86', 18, Fraction(1, 5)), ('73', 8, Fraction(1, 5))]:
        tot, rhs = C3s.lhs_split(LX, K, delta)
        up = math.ceil(float(mpf(tot.b)) * 1e6) / 1e6; lo = math.floor(float(mpf(tot.a)) * 1e6) / 1e6
        rl = math.floor(float(mpf(rhs.a)) * 1e7) / 1e7
        verdict = 'HOLDS' if tot.b < rhs.a else ('FAILS' if tot.a > rhs.b else 'UNDECIDED')
        print(f"Lemma C'''_delta, delta = {delta}, all even N in [4e18, exp({LX})], K = {K}: left side in [{lo:.6f}, {up:.6f}] vs G0' > {rl:.7f}: {verdict}")
        sys.stdout.flush()