"""
Proof: A K=17 binary tree of eml operations evaluates to x * y
Generated: 2026-04-16
"""
import os
import sys

PROOF_ENGINE_ROOT = os.environ.get("PROOF_ENGINE_ROOT")
if not PROOF_ENGINE_ROOT:
    _d = os.path.dirname(os.path.abspath(__file__))
    while _d != os.path.dirname(_d):
        if os.path.isdir(os.path.join(_d, "proof-engine", "skills", "proof-engine", "scripts")):
            PROOF_ENGINE_ROOT = os.path.join(_d, "proof-engine", "skills", "proof-engine")
            break
        _d = os.path.dirname(_d)
    if not PROOF_ENGINE_ROOT:
        raise RuntimeError("PROOF_ENGINE_ROOT not set and skill dir not found via walk-up from proof.py")
sys.path.insert(0, PROOF_ENGINE_ROOT)

from datetime import date
from sympy import Symbol, exp, log, simplify, E, limit, oo

from scripts.computations import compare
from scripts.proof_summary import ProofSummaryBuilder

# ============================================================================
# 1. CLAIM INTERPRETATION (Rule 4)
# ============================================================================

CLAIM_NATURAL = (
    r"The binary operator eml is defined by the expression "
    r"\(\text{eml}(a, b) = \exp(a) - \ln(b)\). "
    r"There exists a finite binary tree consisting solely of eml operations, "
    r"whose 9 leaves are drawn from \(\{1, x, y\}\), such that the tree "
    r"evaluates exactly to \(x \times y\). The tree has K = 17 tokens "
    r"(8 eml operations and 9 leaves), and the identity holds for all "
    r"complex \(x\) and \(y\) (in the algebraic setting where "
    r"\(\ln \circ \exp\) is the identity)."
)

CLAIM_FORMAL = {
    "subject": "Binary operator eml(a, b) = exp(a) - ln(b)",
    "property": (
        "eml(eml(1, eml(eml(eml(1, eml(eml(1, eml(1, x)), 1)), y), 1)), 1) "
        "= x * y for all complex x, y (x != 0, y != 0, x != e^e)"
    ),
    "operator": "==",
    "operator_note": (
        "The claim asserts that a specific K=17 binary tree of eml operations "
        "evaluates to x * y. K denotes the total number of tree nodes "
        "(8 internal eml nodes + 9 leaves = 17). The claim text says 'depth 17'; "
        "following the convention in arXiv:2603.21852, this denotes the RPN code "
        "length (total tree nodes), not the tree height. The actual tree height is 8. "
        "Working inside out through 8 layers: "
        "(1) M1 = eml(1, x) = e - ln(x). "
        "(2) M2 = eml(1, M1) = e - ln(e - ln(x)). "
        "(3) M3 = eml(M2, 1) = exp(e)/(e - ln(x)). "
        "(4) M4 = eml(1, M3) = ln(e - ln(x)). "
        "Steps 1-4 apply the triple-nesting identity to (e - ln(x)), yielding "
        "ln(e - ln(x)). The key observation is that eml(1, x) = e - ln(x) "
        "directly provides the 'e minus logarithm' form, saving one step "
        "compared to the K=19 addition tree where two steps were needed "
        "(eml(x,1) then eml(1,_)) to get e - x. "
        "(5) M5 = eml(M4, y) = exp(ln(e - ln(x))) - ln(y) = (e - ln(x)) - ln(y) "
        "= e - ln(x) - ln(y) = e - ln(xy). "
        "This uses a variant of the subtraction identity: eml(ln(a), y) = a - ln(y) "
        "where y is used as a bare leaf, not wrapped in exp(). This saves another "
        "step compared to the addition tree. "
        "(6) M6 = eml(M5, 1) = exp(e - ln(xy)) = exp(e)/(xy). "
        "(7) M7 = eml(1, M6) = e - ln(exp(e)/(xy)) = e - (e - ln(xy)) = ln(xy). "
        "(8) M8 = eml(M7, 1) = exp(ln(xy)) = xy. "
        "The expression is undefined at x = 0 (ln(0) in M1), y = 0 (ln(0) in M5), "
        "and x = e^e (where e - ln(x) = 0 causes ln(0) in M2). The singularity "
        "at x = e^e is removable: the limit from both sides equals e^e * y, "
        "verified by SymPy. "
        "For complex x, y: the identity holds as a formal algebraic identity "
        "where ln(exp(z)) = z (i.e., on the Riemann surface of log). On the "
        "principal branch, it holds for all x, y with x != 0, y != 0."
    ),
    "threshold": True,
    "is_time_sensitive": False,
}

# 2. FACT REGISTRY
FACT_REGISTRY = {
    "A1": {
        "label": "Token count K = 17 (8 eml operations + 9 leaves)",
        "method": None,
        "result": None,
    },
    "A2": {
        "label": "Step-by-step symbolic evaluation: M8 = x * y",
        "method": None,
        "result": None,
    },
    "A3": {
        "label": "Full expression minus x * y = 0",
        "method": None,
        "result": None,
    },
    "A4": {
        "label": "Removable singularity at x = e^e: limit equals e^e * y",
        "method": None,
        "result": None,
    },
    "A5": {
        "label": "Numerical spot-check at 12 real-valued (x, y) pairs",
        "method": None,
        "result": None,
    },
    "A6": {
        "label": "Numerical spot-check at 6 complex-valued (x, y) pairs",
        "method": None,
        "result": None,
    },
    "A7": {
        "label": "Exhaustive search: no K <= 15 eml tree computes x * y",
        "method": None,
        "result": None,
    },
}

# ============================================================================
# 3. COMPUTATION — token count (A1)
# ============================================================================

EXPR_STR = "eml(eml(1, eml(eml(eml(1, eml(eml(1, eml(1, x)), 1)), y), 1)), 1)"


def count_tokens(expr_str):
    """Count eml operations and leaves in a nested eml expression."""
    import re
    s = expr_str.replace(" ", "")
    eml_count = 0
    leaf_count = 0
    i = 0
    while i < len(s):
        if s[i:i + 3] == "eml":
            eml_count += 1
            i += 3
        elif s[i] in "xy" or (s[i] == "1" and (i == 0 or s[i - 1] in "(,")):
            leaf_count += 1
            i += 1
        else:
            i += 1
    return eml_count, leaf_count


eml_ops, leaves = count_tokens(EXPR_STR)
K = eml_ops + leaves
print(f"  Token count: {eml_ops} eml operations + {leaves} leaves = K = {K}")
A1_verified = compare(K, "==", 17, label="A1: K = 17")

# ============================================================================
# 4. COMPUTATION — symbolic step-by-step evaluation (A2, A3)
# ============================================================================

x_sym = Symbol("x", positive=True)
y_sym = Symbol("y", positive=True)


def eml(a, b):
    """eml(a, b) = exp(a) - ln(b)"""
    return exp(a) - log(b)


# Build step-by-step, simplifying at each layer
M1 = simplify(eml(1, x_sym))
M2 = simplify(eml(1, M1))
M3 = simplify(eml(M2, 1))
M4 = simplify(eml(1, M3))
M5 = simplify(eml(M4, y_sym))
M6 = simplify(eml(M5, 1))
M7 = simplify(eml(1, M6))
M8 = simplify(eml(M7, 1))

# Print all 8 steps
print("  Step-by-step evaluation:")
step_labels = [
    "M1=eml(1,x)", "M2=eml(1,M1)", "M3=eml(M2,1)",
    "M4=eml(1,M3)", "M5=eml(M4,y)", "M6=eml(M5,1)",
    "M7=eml(1,M6)", "M8=eml(M7,1)",
]
step_vals = [M1, M2, M3, M4, M5, M6, M7, M8]
for label, val in zip(step_labels, step_vals):
    print(f"    {label} = {val}")

# Verify critical algebraic cancellation points
step_checks = [
    ("A2a: M1 = e - ln(x)", M1, E - log(x_sym)),
    ("A2b: M3 = exp(e)/(e - ln(x))", M3, exp(E) / (E - log(x_sym))),
    ("A2c: M5 = e - ln(xy)", M5, E - log(x_sym * y_sym)),
    ("A2d: M7 = ln(xy)", M7, log(x_sym * y_sym)),
    ("A2e: M8 = x*y", M8, x_sym * y_sym),
]

A2_results = []
for label, actual, expected in step_checks:
    residual = simplify(actual - expected)
    ok = compare(residual, "==", 0, label=label)
    A2_results.append(ok)

A2_verified = all(A2_results)

# A3: Full expression residual
residual = simplify(M8 - (x_sym * y_sym))
A3_verified = compare(residual, "==", 0, label="A3: M8 - x*y = 0")

# ============================================================================
# 5. COMPUTATION — removable singularity at x = e^e (A4)
# ============================================================================

# At x = e^e, M1 = e - ln(e^e) = e - e = 0, and M2 = eml(1, 0) involves
# log(0) → undefined. Verify the limit from both sides equals e^e * y.

# Use general real x for limit computation
x_real = Symbol("x", real=True)
y_real = Symbol("y", real=True)
M1r = simplify(eml(1, x_real))
M2r = simplify(eml(1, M1r))
M3r = simplify(eml(M2r, 1))
M4r = simplify(eml(1, M3r))
M5r = simplify(eml(M4r, y_real))
M6r = simplify(eml(M5r, 1))
M7r = simplify(eml(1, M6r))
M8r = simplify(eml(M7r, 1))

lim_left = limit(M8r, x_real, exp(E), "-")
lim_right = limit(M8r, x_real, exp(E), "+")
lim_both = limit(M8r, x_real, exp(E))

print(f"  Limit as x -> e^e-: {lim_left}")
print(f"  Limit as x -> e^e+: {lim_right}")
print(f"  Limit as x -> e^e:  {lim_both}")

lim_left_ok = simplify(lim_left - exp(E) * y_real) == 0
lim_right_ok = simplify(lim_right - exp(E) * y_real) == 0
lim_agree = simplify(lim_left - lim_right) == 0

A4_verified = compare(
    lim_left_ok and lim_right_ok and lim_agree, "==", True,
    label="A4: limit(M8, x->e^e) = e^e * y from both sides",
)

# ============================================================================
# 6. CROSS-CHECKS — numerical evaluation (A5, A6)
# ============================================================================

import cmath
import math


def eml_num(a, b):
    """Numerical eml evaluation using cmath."""
    return cmath.exp(a) - cmath.log(b)


def eval_mult_chain(xv, yv):
    """Evaluate the full K=17 chain numerically."""
    m1 = eml_num(1, xv)
    m2 = eml_num(1, m1)
    m3 = eml_num(m2, 1)
    m4 = eml_num(1, m3)
    m5 = eml_num(m4, yv)
    m6 = eml_num(m5, 1)
    m7 = eml_num(1, m6)
    m8 = eml_num(m7, 1)
    return m8


# A5: Real-valued spot-checks (12 points)
ee = math.e ** math.e  # e^e ≈ 15.1543
real_tests = [
    (2.0, 3.0),
    (0.5, 4.0),
    (-2.0, 3.0),
    (-3.0, -5.0),
    (100.0, 0.01),
    (-100.0, 0.5),
    (1.0, 1.0),
    (math.e, math.pi),
    (ee - 1e-6, 2.0),       # just left of singularity
    (ee + 1e-6, 2.0),       # just right of singularity
    (ee - 1e-12, 1.0),      # extremely close to singularity
    (0.001, 1000.0),
]

print("  Numerical (real):")
real_diffs = []
for xv, yv in real_tests:
    result = eval_mult_chain(xv, yv)
    expected = xv * yv
    diff = abs(result - expected)
    real_diffs.append(diff)
    print(f"    x={xv:>20.14g}, y={yv:>12.6g}  "
          f"|diff|={diff:.2e}")

max_real_diff = max(real_diffs)
A5_verified = compare(
    max_real_diff < 1e-6, "==", True,
    label="A5: all real spot-checks agree within 1e-6",
)

# A6: Complex-valued spot-checks (6 points)
complex_tests = [
    (1 + 0.5j, 2 - 0.3j),
    (0.5 + 1j, -1.5 + 2j),
    (-3 + 0.7j, 4 - 0.7j),
    (1j, -1j),
    (2 + 3j, -1 - 0.1j),
    (-1 + 0j, -1 + 0j),     # (-1)*(-1) = 1
]

print("  Numerical (complex):")
complex_diffs = []
for xv, yv in complex_tests:
    result = eval_mult_chain(xv, yv)
    expected = xv * yv
    diff = abs(result - expected)
    complex_diffs.append(diff)
    print(f"    x={str(xv):>12s}, y={str(yv):>12s}  "
          f"|diff|={diff:.2e}")

max_complex_diff = max(complex_diffs)
A6_verified = compare(
    max_complex_diff < 1e-10, "==", True,
    label="A6: all complex spot-checks agree within 1e-10",
)

# ============================================================================
# 7. CROSS-CHECK — exhaustive search through K=15 (A7)
# ============================================================================

import time as _time


def exhaustive_search(max_k=15):
    """
    Enumerate all distinct eml binary trees with leaves {1, x, y} up to K=max_k.
    Return (found_at_k, level_sizes) where found_at_k is None if x*y not found.
    Uses a fixed complex test point for numerical fingerprinting.
    """
    x_test = 2.17 + 0.83j
    y_test = 0.31 + 1.47j
    target = x_test * y_test  # multiplication target

    def _eml(a, b):
        try:
            r = cmath.exp(a) - cmath.log(b)
            if not cmath.isfinite(r) or abs(r) > 1e150:
                return None
            return r
        except:
            return None

    def _fp(z):
        return (round(z.real, 8), round(z.imag, 8)) if z else None

    levels = {1: {}}
    for name, val in [("1", 1 + 0j), ("x", x_test), ("y", y_test)]:
        levels[1][_fp(val)] = val

    target_fp = _fp(target)
    level_sizes = {1: 3}
    found_at_k = None

    for k in range(3, max_k + 1, 2):
        new = {}
        for kl in range(1, k - 1, 2):
            kr = k - 1 - kl
            if kr < 1 or kr % 2 == 0:
                continue
            if kl not in levels or kr not in levels:
                continue
            for lv in levels[kl].values():
                for rv in levels[kr].values():
                    r = _eml(lv, rv)
                    if r is None:
                        continue
                    f = _fp(r)
                    if f and f not in new:
                        new[f] = r
        levels[k] = new
        level_sizes[k] = len(new)

        if target_fp in new and abs(new[target_fp] - target) < 1e-10:
            found_at_k = k
            break

        # Also scan for close matches
        for v in new.values():
            if abs(v - target) < 1e-10:
                found_at_k = k
                break
        if found_at_k:
            break

    return found_at_k, level_sizes


print("  Exhaustive search K=1..15:")
t_search = _time.time()
found_k, level_sizes = exhaustive_search(max_k=15)
search_time = _time.time() - t_search

for k in sorted(level_sizes):
    print(f"    K={k:2d}: {level_sizes[k]:>10,} distinct values")
print(f"    Search time: {search_time:.2f}s")
print(f"    x*y found at K <= 15: {found_k}")

A7_verified = compare(
    found_k is None, "==", True,
    label="A7: no K <= 15 tree computes x*y",
)

# ============================================================================
# 8. ADVERSARIAL CHECKS (Rule 5)
# ============================================================================

adversarial_checks = [
    {
        "question": (
            "Does the identity hold for negative real x and y?"
        ),
        "verification_performed": (
            "For negative real x (e.g., x = -2), ln(x) = ln|x| + pi*i. "
            "Then M1 = e - ln|x| - pi*i (complex intermediate). "
            "Tracing through the chain: the imaginary components from "
            "ln(negative) at steps M1 and M5 interact through exp and log "
            "operations. The +-pi*i terms cancel exactly across the chain, "
            "returning a real result. Numerical tests confirm: "
            "(-2)*3 gives |diff| < 5e-15, (-3)*(-5) gives |diff| < 8e-15."
        ),
        "finding": (
            "The identity holds for all real nonzero x and y, including "
            "negatives. Intermediate complex values with +-pi*i cancel exactly."
        ),
        "breaks_proof": False,
    },
    {
        "question": (
            "What singularities does the expression have, and are they "
            "removable?"
        ),
        "verification_performed": (
            "Three singularity classes: "
            "(1) x = 0: M1 = eml(1, 0) = e - ln(0) is undefined. The limit "
            "as x -> 0 diverges (M1 -> +infinity), so this is NOT removable. "
            "However, x*y = 0 at x = 0, and multiplication by zero is well-defined, "
            "so this is a genuine limitation of the eml expression. "
            "(2) y = 0: M5 = eml(M4, 0) = exp(M4) - ln(0) is undefined. "
            "Same analysis: not removable. "
            "(3) x = e^e (approx 15.154): M1 = e - ln(e^e) = 0, and "
            "M2 = eml(1, 0) involves ln(0). SymPy limit confirms: "
            "lim_{x->e^e} M8 = e^e * y from both sides. This IS a removable "
            "singularity, analogous to x = e in the K=19 addition tree. "
            "Numerical tests within 1e-12 of e^e confirm convergence."
        ),
        "finding": (
            "x = 0 and y = 0 are genuine singularities (not removable). "
            "x = e^e is a removable singularity. The identity holds for all "
            "real x not in {0, e^e} and y != 0."
        ),
        "breaks_proof": False,
    },
    {
        "question": (
            "Does the identity hold for arbitrary complex x, y on the "
            "principal branch of log?"
        ),
        "verification_performed": (
            "The critical cancellation is M7 = e - ln(exp(e - ln(xy))). "
            "On the principal branch, ln(exp(z)) = z when |Im(z)| < pi. "
            "Here z = e - ln(xy) = (e - ln|xy|) - i*arg(xy). Since "
            "arg(xy) is in (-pi, pi], we have |Im(z)| <= pi, and the "
            "cancellation holds for all nonzero x, y. The earlier "
            "cancellation exp(ln(e-ln(x))) at M5 requires e-ln(x) != 0, "
            "which fails only at x = e^e. "
            "Numerical tests at 6 complex points (including (-1)*(-1)=1, "
            "purely imaginary inputs) all agree within 1e-15. "
            "In the formal algebraic framework, ln(exp(z)) = z is an axiom "
            "and the identity holds for all nonzero complex x, y."
        ),
        "finding": (
            "On the principal branch: holds for all nonzero x, y "
            "(except x = e^e). As a formal algebraic identity: holds for "
            "all nonzero complex x, y."
        ),
        "breaks_proof": False,
    },
    {
        "question": "Is K = 17 the minimum code length for multiplication?",
        "verification_performed": (
            "An embedded exhaustive search (A7) enumerated all distinct "
            "eml trees through K=15 and found no expression evaluating to "
            "x*y. The search space at K=15 contains approximately 2 million "
            "distinct values. No expression at K <= 15 computes x*y. "
            "Note: the search covers K=1 through K=15 (all odd K); K=17 "
            "is the next possible level. Whether K=17 is strictly minimal "
            "(i.e., no other K=17 tree also computes x*y) is not determined, "
            "but the search confirms no shorter tree exists."
        ),
        "finding": (
            "Exhaustive search through K=15 found no eml tree computing x*y. "
            "K=17 is the shortest known code length for multiplication."
        ),
        "breaks_proof": False,
    },
    {
        "question": "Could numerical overflow cause false agreement?",
        "verification_performed": (
            "The largest intermediate value is M6 = exp(e - ln(xy)). "
            "For |xy| << 1 (e.g., x=0.001, y=0.001), M6 = exp(e+6.9) "
            "which is large but finite (~15000). For |xy| >> 1, "
            "M6 = exp(e - ln(xy)) becomes small. The symbolic proof does "
            "not depend on floating-point. The log-exp cancellation at M7 "
            "(= ln(xy)) bounds intermediate values. Numerical tests at "
            "extremes (x=100/y=0.01, x=-100/y=0.5) confirm |diff| < 1e-14."
        ),
        "finding": (
            "No overflow risk for representable floats. The proof rests "
            "on exact symbolic algebra."
        ),
        "breaks_proof": False,
    },
]

# ============================================================================
# 9. VERDICT AND STRUCTURED OUTPUT
# ============================================================================

if __name__ == "__main__":
    all_verified = (
        A1_verified and A2_verified and A3_verified and A4_verified
        and A5_verified and A6_verified and A7_verified
    )
    claim_holds = compare(
        all_verified, "==", CLAIM_FORMAL["threshold"],
        label="All facts verified (symbolic + numerical + search)",
    )

    any_breaks = any(ac.get("breaks_proof") for ac in adversarial_checks)
    if any_breaks:
        verdict = "UNDETERMINED"
    else:
        verdict = "PROVED" if claim_holds else "DISPROVED"

    print(f"\nVERDICT: {verdict}")

    builder = ProofSummaryBuilder(CLAIM_NATURAL, CLAIM_FORMAL)

    builder.add_computed_fact(
        "A1",
        label=FACT_REGISTRY["A1"]["label"],
        method=(
            "Programmatic parsing of the expression string to count eml "
            "operation nodes and leaf nodes (1, x, y)"
        ),
        result=f"Confirmed: {eml_ops} eml + {leaves} leaves = K = {K}",
    )
    builder.add_computed_fact(
        "A2",
        label=FACT_REGISTRY["A2"]["label"],
        method=(
            "SymPy symbolic evaluation through 8 layers: build each "
            "sub-expression M1..M8 with simplification at each step, "
            "verify residuals at 5 critical algebraic cancellation points "
            "(M1=e-ln(x), M3=exp(e)/(e-ln(x)), M5=e-ln(xy), M7=ln(xy), "
            "M8=x*y) all equal zero"
        ),
        result="Confirmed: all 5 critical residuals = 0, M8 = x * y",
        depends_on=["A1"],
    )
    builder.add_computed_fact(
        "A3",
        label=FACT_REGISTRY["A3"]["label"],
        method=(
            "SymPy simplify(M8 - x*y) for positive real symbols x, y; "
            "verify residual equals 0"
        ),
        result=f"Confirmed: residual = {residual}",
        depends_on=["A2"],
    )
    builder.add_computed_fact(
        "A4",
        label=FACT_REGISTRY["A4"]["label"],
        method=(
            "SymPy limit(M8, x, exp(e)) from left, right, and both sides; "
            "verify all three equal exp(e) * y"
        ),
        result=(
            f"Confirmed: limit from left = {lim_left}, "
            f"from right = {lim_right}, both = e^e * y"
        ),
        depends_on=["A2"],
    )
    builder.add_computed_fact(
        "A5",
        label=FACT_REGISTRY["A5"]["label"],
        method=(
            "Numerical evaluation of the full 8-layer chain at 12 "
            "real-valued (x, y) pairs including positive, negative, "
            "near-zero, near-singularity (x near e^e within 1e-12); "
            "verify |result - x*y| < 1e-6"
        ),
        result=f"Confirmed: max |diff| = {max_real_diff:.2e}",
    )
    builder.add_computed_fact(
        "A6",
        label=FACT_REGISTRY["A6"]["label"],
        method=(
            "Numerical evaluation of the full 8-layer chain at 6 "
            "complex-valued (x, y) pairs including purely imaginary "
            "and negative real inputs; verify |result - x*y| < 1e-10"
        ),
        result=f"Confirmed: max |diff| = {max_complex_diff:.2e}",
    )
    builder.add_computed_fact(
        "A7",
        label=FACT_REGISTRY["A7"]["label"],
        method=(
            "Embedded exhaustive bottom-up search: enumerate all distinct "
            "eml binary trees with leaves {1, x, y} at each odd K from 1 "
            "to 15 using numerical fingerprinting at a generic complex "
            "test point; check if x*y appears"
        ),
        result=(
            f"Confirmed: {level_sizes.get(15, 0):,} distinct values at K=15, "
            "x*y not found at any K <= 15"
        ),
    )

    builder.add_cross_check(
        description=(
            "Symbolic (A2, A3) vs numerical (A5, A6): symbolic algebra "
            "proves identity exactly for positive real x, y; numerical "
            "evaluation independently confirms at 18 test points "
            "(12 real including negatives + 6 complex)"
        ),
        fact_ids=["A3", "A5", "A6"],
        agreement=A3_verified and A5_verified and A6_verified,
    )
    builder.add_cross_check(
        description=(
            "Exhaustive search (A7) as independent method: bottom-up "
            "enumeration of all eml trees through K=15 finds no tree "
            "computing x*y, confirming K=17 is not achievable at lower K"
        ),
        fact_ids=["A3", "A7"],
        agreement=A3_verified and A7_verified,
    )

    for ac in adversarial_checks:
        builder.add_adversarial_check(
            question=ac["question"],
            verification_performed=ac["verification_performed"],
            finding=ac["finding"],
            breaks_proof=ac["breaks_proof"],
        )

    builder.set_verdict(verdict)
    builder.set_key_results(
        token_count_K=K,
        symbolic_steps_verified=A2_verified,
        full_residual_zero=A3_verified,
        singularity_limit_verified=A4_verified,
        real_numerical_max_diff=max_real_diff,
        complex_numerical_max_diff=max_complex_diff,
        exhaustive_search_max_k=15,
        exhaustive_search_found=found_k,
        claim_holds=claim_holds,
    )

    builder.emit()
