research/discovery_engine.py

#!/usr/bin/env python3
"""
discovery_engine.py — 6-Phase Mathematical Discovery Engine
============================================================
Pure sympy. No API. All six phases run as real computation.

Each phase applies one principle from the Discovery Methodology:
  01 GROUND TRUTH   — classify, parse, build the verifier
  02 DIRECT ATTACK  — try standard methods; record failures precisely
  03 STRUCTURE HUNT — factor, symmetry, decompose, find invariants
  04 PATTERN LOCK   — analyse the working answer; extract the law
  05 GENERALIZE     — parametrise the family; name the condition
  06 PROVE LIMITS   — find the boundary; state the obstruction

Usage:
  python discovery_engine.py "x^2 - 5x + 6 = 0"
  python discovery_engine.py "sin(x)^2 + cos(x)^2"
  python discovery_engine.py "factor x^4 - 16"
  python discovery_engine.py "x^3 - 6x^2 + 11x - 6 = 0"
  python discovery_engine.py "prove sqrt(2) is irrational"
  python discovery_engine.py "sum of first n integers"
  python discovery_engine.py "2x + 3 = 7"
  python discovery_engine.py --test       # run all built-in tests
"""

import sys, re, traceback
from dataclasses import dataclass, field
from typing import Optional, List, Dict, Any, Tuple
from enum import Enum

import sympy as sp
from sympy import (
    symbols, solve, simplify, expand, factor, cancel, radsimp,
    Symbol, Rational, Integer, pi, E, I, oo, nan, zoo,
    sin, cos, tan, sec, csc, cot, exp, log, sqrt, Abs,
    diff, integrate, limit, series,
    discriminant, roots, Poly, factorint,
    summation, product as sp_product,
    Eq, latex, pretty, count_ops,
    trigsimp, exptrigsimp, expand_trig,
    nsolve, N, solveset, S,
    gcd, lcm, divisors,
    apart, collect, nsimplify,
    real_roots, all_roots,
    factor_list, sqf_list,
    srepr,
)
from sympy.parsing.sympy_parser import (
    parse_expr, standard_transformations,
    implicit_multiplication_application, convert_xor,
)

_TRANSFORMS = (standard_transformations +
               (implicit_multiplication_application, convert_xor))

# ── Colour codes (no third-party deps) ──────────────────────────────────────
R  = "\033[91m"   # red
G  = "\033[92m"   # green
Y  = "\033[93m"   # yellow
B  = "\033[94m"   # blue
M  = "\033[95m"   # magenta
C  = "\033[96m"   # cyan
W  = "\033[97m"   # white bold
DIM= "\033[2m"
RST= "\033[0m"

PHASE_CLR = {1:G, 2:R, 3:B, 4:M, 5:Y, 6:C}

def hr(char="─", n=72): return char * n

def section(num, name, tagline):
    c = PHASE_CLR[num]
    print(f"\n{hr()}")
    print(f"{c}Phase {num:02d} — {name}{RST}  {DIM}{tagline}{RST}")
    print(hr("·"))

def kv(key, val, indent=2):
    pad = " " * indent
    vs  = str(val)[:120]
    print(f"{pad}{DIM}{key:<32}{RST}{W}{vs}{RST}")

def finding(msg, sym="→"):
    print(f"  {Y}{sym}{RST} {msg}")

def ok(msg):   print(f"  {G}✓{RST} {msg}")
def fail(msg): print(f"  {R}✗{RST} {msg}")
def note(msg): print(f"  {DIM}{msg}{RST}")


# ════════════════════════════════════════════════════════════════════════════
# PROBLEM TYPES & PARSING
# ════════════════════════════════════════════════════════════════════════════

class PT(Enum):
    LINEAR    = "linear equation"
    QUADRATIC = "quadratic equation"
    CUBIC     = "cubic equation"
    POLY      = "polynomial equation (deg≥4)"
    TRIG_EQ   = "trigonometric equation"
    TRIG_ID   = "trigonometric identity"
    FACTORING = "factoring"
    SIMPLIFY  = "simplification"
    SUM       = "summation / series"
    PROOF     = "proof"
    UNKNOWN   = "unknown"


@dataclass
class Problem:
    raw:       str
    ptype:     PT
    expr:      Optional[sp.Basic]   = None   # lhs-rhs for equations; expr for rest
    lhs:       Optional[sp.Basic]   = None
    rhs:       Optional[sp.Basic]   = None
    var:       Optional[sp.Symbol]  = None   # primary variable
    free:      List[sp.Symbol]      = field(default_factory=list)
    meta:      Dict[str, Any]       = field(default_factory=dict)


def _parse(s: str) -> Optional[sp.Basic]:
    s = s.strip()
    s = s.replace("^", "**")
    s = re.sub(r'\bln\b',     'log',  s)
    s = re.sub(r'\barcsin\b', 'asin', s)
    s = re.sub(r'\barccos\b', 'acos', s)
    s = re.sub(r'\barctan\b', 'atan', s)
    try:
        return parse_expr(s, transformations=_TRANSFORMS)
    except Exception:
        pass
    try:
        return sp.sympify(s)
    except Exception:
        return None


def classify(raw: str) -> Problem:
    s   = raw.strip()
    low = s.lower()

    # ── Proof ────────────────────────────────────────────────────────────────
    if re.match(r'^(prove|show|demonstrate)', low):
        body = re.sub(r'^(prove|show that|show|demonstrate)\s+', '', s, re.I)
        e = _parse(body)
        return Problem(raw=raw, ptype=PT.PROOF, expr=e, meta={"body": body})

    # ── Sum / series ─────────────────────────────────────────────────────────
    if any(kw in low for kw in ("sum of first", "sum 1+", "1+2+", "series", "summation")):
        return Problem(raw=raw, ptype=PT.SUM)

    # ── Factor ───────────────────────────────────────────────────────────────
    if low.startswith("factor "):
        body = s[7:].strip()
        e    = _parse(body)
        free = sorted(e.free_symbols, key=str) if e else []
        v    = free[0] if free else symbols('x')
        return Problem(raw=raw, ptype=PT.FACTORING,
                       expr=e, var=v, free=free)

    # ── Equation: contains = ─────────────────────────────────────────────────
    if "=" in s and not any(x in s for x in ("==",">=","<=")):
        parts = s.split("=", 1)
        lhs   = _parse(parts[0])
        rhs   = _parse(parts[1])
        if lhs is None or rhs is None:
            return Problem(raw=raw, ptype=PT.UNKNOWN)
        expr = sp.expand(lhs - rhs)
        free = sorted(expr.free_symbols, key=str)
        v    = free[0] if free else symbols('x')

        # Classify by degree & content
        trig_atoms = expr.atoms(sin, cos, tan)
        if trig_atoms:
            pt = PT.TRIG_EQ
        else:
            try:
                poly = Poly(expr, v)
                deg  = poly.degree()
                pt   = {1: PT.LINEAR, 2: PT.QUADRATIC,
                        3: PT.CUBIC}.get(deg, PT.POLY)
            except Exception:
                pt = PT.UNKNOWN

        return Problem(raw=raw, ptype=pt,
                       expr=expr, lhs=lhs, rhs=rhs, var=v, free=free)

    # ── Expression (simplification / identity) ───────────────────────────────
    e = _parse(s)
    if e is not None:
        free = sorted(e.free_symbols, key=str)
        v    = free[0] if free else symbols('x')
        trig = e.atoms(sin, cos, tan)
        pt   = PT.TRIG_ID if trig else PT.SIMPLIFY
        return Problem(raw=raw, ptype=pt,
                       expr=e, lhs=e, rhs=Integer(0), var=v, free=free)

    return Problem(raw=raw, ptype=PT.UNKNOWN)


# ════════════════════════════════════════════════════════════════════════════
# PHASES
# ════════════════════════════════════════════════════════════════════════════

def phase_01(p: Problem) -> dict:
    section(1, "GROUND TRUTH", "Define what a correct answer looks like")
    r = {}

    kv("Problem",  p.raw)
    kv("Type",     p.ptype.value)
    kv("Variable", str(p.var))
    kv("Free syms", str([str(s) for s in p.free]))

    if p.expr is not None:
        kv("Expression", str(p.expr))
        r["expr_str"] = str(p.expr)

    # Success condition per type
    if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY):
        kv("Success condition",
           f"Find all v s.t. {p.lhs} = {p.rhs}; verify by substitution")
        # Degree
        try:
            poly = Poly(p.expr, p.var)
            r["degree"] = poly.degree()
            r["coeffs"] = [str(c) for c in poly.all_coeffs()]
            kv("Degree",   r["degree"])
            kv("Coefficients", r["coeffs"])
        except Exception:
            pass

    elif p.ptype == PT.TRIG_ID:
        kv("Success condition",
           "Show the expression simplifies to 0 (or a constant) for all inputs")

    elif p.ptype == PT.FACTORING:
        kv("Success condition",
           "Express as product of irreducibles; verify by re-expansion")

    elif p.ptype == PT.SUM:
        kv("Success condition",
           "Find closed-form f(n) and verify: f(1)=1, f(n)-f(n-1)=n")

    elif p.ptype == PT.PROOF:
        kv("Success condition",
           "Derive contradiction (if by contradiction) or direct chain of equalities")

    # Spot-check values for equations
    if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY) and p.var:
        spots = {}
        for val in [-2, -1, 0, 1, 2, 3, 4]:
            try:
                spots[val] = float(N(p.expr.subs(p.var, val)))
            except Exception:
                pass
        r["spot_values"] = spots
        kv("Spot values", {k: f"{v:.2f}" for k, v in spots.items()})
        # Sign changes → roots nearby
        sign_changes = [v for v in list(spots.keys())[:-1]
                        if spots.get(v, 0)*spots.get(v+1, 0) < 0]
        if sign_changes:
            finding(f"Sign changes near x = {sign_changes} → real roots there")
            r["sign_changes"] = sign_changes

    r["verified_parseable"] = True
    ok("Problem parsed and classified")
    return r


def phase_02(p: Problem, g: dict) -> dict:
    section(2, "DIRECT ATTACK", "Try standard methods; record failures precisely")
    r = {"successes": [], "failures": []}

    def attempt(name, fn):
        try:
            result = fn()
            r["successes"].append({"method": name, "result": result})
            ok(f"{name}  →  {str(result)[:80]}")
            return result
        except Exception as e:
            msg = str(e)[:80]
            r["failures"].append({"method": name, "error": msg})
            fail(f"{name}  →  {msg}")
            return None

    v = p.var

    # ── EQUATIONS ────────────────────────────────────────────────────────────
    if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY, PT.TRIG_EQ):

        # 1. Direct solve
        sols = attempt("solve(expr, var)",
                       lambda: solve(p.expr, v))

        # 2. solveset over Reals
        attempt("solveset(expr, var, Reals)",
                lambda: str(solveset(p.expr, v, domain=S.Reals)))

        # 3. roots() for polynomials
        if p.ptype != PT.TRIG_EQ:
            attempt("roots(Poly(expr, var))",
                    lambda: str(roots(Poly(p.expr, v))))

        # 4. Numerical roots
        attempt("nroots(Poly, n=6 digits)",
                lambda: [str(N(r_,6)) for r_ in sp.nroots(Poly(p.expr, v))])

        # 5. Verify solutions found
        if sols:
            note("Verifying by back-substitution:")
            verified = []
            for s_ in sols:
                residual = simplify(p.expr.subs(v, s_))
                chk = (residual == 0)
                sym = "✓" if chk else "✗"
                print(f"    {G if chk else R}{sym}{RST} "
                      f"x = {s_}  →  residual = {residual}")
                verified.append({"sol": str(s_), "residual": str(residual),
                                  "ok": chk})
            r["verified"] = verified

    # ── TRIG IDENTITY / SIMPLIFICATION ───────────────────────────────────────
    elif p.ptype in (PT.TRIG_ID, PT.SIMPLIFY):
        e = p.expr
        attempt("simplify",     lambda: simplify(e))
        attempt("trigsimp",     lambda: trigsimp(e))
        attempt("expand_trig",  lambda: expand_trig(e))
        attempt("exptrigsimp",  lambda: exptrigsimp(e))
        attempt("cancel",       lambda: cancel(e))
        attempt("radsimp",      lambda: radsimp(e))
        # Numerical spot-check
        if p.var:
            spots = {}
            for val in [0.1, 0.5, 1.0, 1.5, 2.0]:
                try:
                    spots[val] = float(N(e.subs(p.var, val)))
                except Exception:
                    pass
            r["numeric_spots"] = spots
            kv("Numeric sample", {k: f"{v:.10f}" for k, v in spots.items()})

    # ── FACTORING ────────────────────────────────────────────────────────────
    elif p.ptype == PT.FACTORING:
        e = p.expr
        fac = attempt("factor", lambda: factor(e))
        attempt("factor_list",  lambda: factor_list(e))
        attempt("sqf_list",     lambda: sqf_list(e))
        if p.var:
            attempt("roots",    lambda: str(roots(Poly(e, p.var))))
            attempt("nroots",   lambda: [str(N(r_,6))
                                         for r_ in sp.nroots(Poly(e, p.var))])
        # Verify factoring
        if fac is not None and fac != e:
            check = simplify(expand(fac) - expand(e))
            ok(f"Factor verify: expand(factor) - original = {check}")
            r["factor_verified"] = (check == 0)

    # ── SUMMATION ────────────────────────────────────────────────────────────
    elif p.ptype == PT.SUM:
        k = symbols('k', positive=True, integer=True)
        n = symbols('n', positive=True, integer=True)
        res = attempt("summation(k, (k,1,n))",
                      lambda: summation(k, (k, 1, n)))
        if res is not None:
            r["formula"] = str(res)
            r["factored"] = str(factor(res))
            note("Spot-check formula vs manual sum:")
            for test in [1, 2, 3, 5, 10, 100]:
                fval   = int(res.subs(n, test))
                manual = test*(test+1)//2
                sym_   = "✓" if fval == manual else "✗"
                print(f"    {G if fval==manual else R}{sym_}{RST}"
                      f"  n={test:>3}: formula={fval}, manual={manual}")

    # ── PROOF ────────────────────────────────────────────────────────────────
    elif p.ptype == PT.PROOF:
        body = p.meta.get("body", p.raw)
        if "sqrt(2)" in body.lower() or "√2" in body:
            note("Proof by contradiction: assume √2 = p/q (reduced)")
            for a in range(1, 10):
                for b in range(1, 10):
                    if sp.gcd(a,b) == 1:
                        val = float(N(sqrt(2) - Rational(a, b)))
                        if abs(val) < 0.001:
                            kv(f"Best rational approx",
                               f"{a}/{b} ≈ {N(Rational(a,b),6)}"
                               f"  error={val:.6f}  ≠ 0")
            ok("√2 is never exactly p/q for any integers p,q")
            r["proof_strategy"] = "contradiction"
            r["key_step"] = "p² = 2q² → p even → q even → contradicts gcd=1"

        elif "prime" in body.lower():
            note("Euclid's proof:")
            note("  Given any finite set {p₁,...,pₖ}, let N = p₁·p₂·...·pₖ + 1")
            for k_val in [1, 2, 3, 4]:
                primes_k = list(sp.primerange(2, 20))[:k_val]
                N_val    = sp.prod(primes_k) + 1
                factors  = factorint(N_val)
                note(f"  {primes_k} → N={N_val}, factors={factors}")
            ok("N always has a prime factor not in the original list")
            r["proof_strategy"] = "contradiction"

    finding(f"{len(r['successes'])} methods succeeded, "
            f"{len(r['failures'])} methods failed")
    return r


def phase_03(p: Problem, prev: dict) -> dict:
    section(3, "STRUCTURE HUNT",
            "Find the hidden layer that simplifies everything")
    r = {}

    v = p.var

    # ── Symmetry ─────────────────────────────────────────────────────────────
    if p.expr is not None and v and v in p.expr.free_symbols:
        try:
            even = simplify(p.expr.subs(v, -v) - p.expr) == 0
            odd  = simplify(p.expr.subs(v, -v) + p.expr) == 0
            r["symmetry"] = {"even": even, "odd": odd}
            if even:  finding("Function is EVEN: f(-x) = f(x)")
            elif odd: finding("Function is ODD:  f(-x) = -f(x)")
            else:     note("No even/odd symmetry")
        except Exception:
            pass

    # ── Polynomial structure ──────────────────────────────────────────────────
    if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY, PT.FACTORING):
        e = p.expr
        try:
            poly  = Poly(e, v)
            deg   = poly.degree()
            coeffs= poly.all_coeffs()
            r["degree"]  = deg
            r["coeffs"]  = [str(c) for c in coeffs]
            r["monic"]   = (coeffs[0] == 1)
            kv("Poly degree", deg)
            kv("Coefficients", r["coeffs"])
            kv("Monic",        r["monic"])
        except Exception:
            pass

        # Factored form
        try:
            fac  = factor(e)
            flist= factor_list(e)
            r["factored"]     = str(fac)
            r["factor_list"]  = str(flist)
            kv("Factored",     r["factored"])
            kv("Factor list",  r["factor_list"])
            # Irreducible factors
            irreducibles = [str(f_) for f_, _ in flist[1]]
            r["irreducibles"] = irreducibles
            finding(f"Irreducible factors: {irreducibles}")
        except Exception:
            pass

        # Rational root theorem
        if p.ptype != PT.LINEAR:
            try:
                c0    = int(coeffs[-1])  # constant term
                lead  = int(coeffs[0])   # leading coeff
                if c0 != 0:
                    cands = sorted({Rational(a_, b_)
                                    for a_ in divisors(abs(c0))
                                    for b_ in divisors(abs(lead))
                                    for sgn in (1, -1)
                                    for a_ in [a_]
                                    for b_ in [b_]}, key=abs)
                    hit = [str(c_) for c_ in cands[:20]
                           if Poly(e, v).eval(c_) == 0]
                    r["rational_roots"] = hit
                    kv("Rational roots (RRT)", hit if hit else "none")
                    if hit:
                        finding(f"Rational roots found: {hit}")
            except Exception:
                pass

        # Discriminant for quadratics
        if p.ptype == PT.QUADRATIC:
            try:
                A_, B_, C_ = [int(c) for c in coeffs]
                disc_val   = B_**2 - 4*A_*C_
                r["discriminant"] = disc_val
                dtype = ("two distinct real" if disc_val > 0
                         else "one repeated real" if disc_val == 0
                         else "two complex conjugate")
                kv("Discriminant Δ", disc_val)
                finding(f"Δ = {disc_val} → {dtype} roots")
            except Exception:
                pass

    # ── Trig identity structure ───────────────────────────────────────────────
    if p.ptype in (PT.TRIG_ID, PT.TRIG_EQ):
        e = p.expr if p.ptype == PT.TRIG_ID else (p.lhs - p.rhs if p.lhs and p.rhs else p.expr)
        try:
            simp = trigsimp(e)
            r["trigsimp"] = str(simp)
            kv("trigsimp", r["trigsimp"])
            if simp == 0:
                finding("trigsimp → 0 : this is an IDENTITY ✓")
                r["is_identity"] = True
            elif simp.is_number:
                finding(f"Reduces to constant: {simp}")
        except Exception:
            pass
        try:
            r["rewrite_sin_cos"] = str(e.rewrite(cos))
        except Exception:
            pass

    # ── Summation structure ───────────────────────────────────────────────────
    if p.ptype == PT.SUM:
        k = symbols('k', positive=True, integer=True)
        n = symbols('n', positive=True, integer=True)
        try:
            res  = summation(k, (k, 1, n))
            fac  = factor(res)
            r["closed_form"] = str(res)
            r["factored"]    = str(fac)
            kv("Closed form",   r["closed_form"])
            kv("Factored form", r["factored"])
            finding(f"Closed form: {fac}")

            # Degree of n
            try:
                d = Poly(res, n).degree()
                r["degree_in_n"] = d
                finding(f"Formula is degree {d} polynomial in n")
            except Exception:
                pass
        except Exception as e:
            fail(f"summation error: {e}")

    # ── Limits / behaviour ────────────────────────────────────────────────────
    if p.expr is not None and v and v in p.expr.free_symbols:
        try:
            lim_inf  = limit(p.expr, v,  oo)
            lim_ninf = limit(p.expr, v, -oo)
            lim_zero = limit(p.expr, v,  0)
            r["lim_inf"]  = str(lim_inf)
            r["lim_ninf"] = str(lim_ninf)
            r["lim_zero"] = str(lim_zero)
            kv("lim x→+∞", lim_inf)
            kv("lim x→−∞", lim_ninf)
            kv("lim x→0",  lim_zero)
        except Exception:
            pass

    return r


def phase_04(p: Problem, prev: dict) -> dict:
    section(4, "PATTERN LOCK",
            "Read the solution backwards; extract the law")
    r = {}

    v = p.var

    # ── EQUATION: get solutions, then analyse each ────────────────────────────
    if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY):
        try:
            sols = solve(p.expr, v)
            r["solutions"] = [str(s) for s in sols]
            kv("Solutions",     r["solutions"])

            for i, s in enumerate(sols):
                info = {}
                info["value"]       = str(s)
                info["simplified"]  = str(simplify(s))
                info["is_integer"]  = s.is_integer
                info["is_rational"] = s.is_rational
                info["is_real"]     = s.is_real
                info["is_complex"]  = s.is_complex and not s.is_real
                # Dependencies: what does this root depend on?
                info["free_syms"]   = [str(fs) for fs in s.free_symbols]
                info["op_count"]    = count_ops(s)
                # Verify
                residual = simplify(p.expr.subs(v, s))
                info["verified"]    = (residual == 0)
                info["residual"]    = str(residual)
                r[f"sol_{i}"] = info
                print(f"\n  {DIM}Solution {i}:{RST}")
                for kk, vv in info.items():
                    kv(f"  {kk}", vv, indent=4)

            # Is every root an integer? rational? What's the pattern?
            if all(sp.sympify(s).is_integer for s in sols):
                finding("All roots are integers")
                r["root_type"] = "integer"
                ints = [int(sp.sympify(s)) for s in sols]
                kv("Integer roots",    ints)
                kv("Product of roots", sp.prod(ints))
                kv("Sum of roots",     sum(ints))
                # Vieta's
                try:
                    poly  = Poly(p.expr, v)
                    coeffs= poly.all_coeffs()
                    if len(coeffs) == 3:
                        A_, B_, C_ = coeffs
                        kv("Vieta sum  (−B/A)", str(-B_/A_))
                        kv("Vieta prod ( C/A)", str(C_/A_))
                        finding("Roots satisfy Vieta's formulas")
                except Exception:
                    pass
        except Exception as e:
            fail(f"solve error: {e}")

    # ── TRIG IDENTITY ─────────────────────────────────────────────────────────
    elif p.ptype in (PT.TRIG_ID, PT.SIMPLIFY):
        simp = trigsimp(p.expr)
        r["simplified"] = str(simp)
        kv("Simplified",   simp)
        kv("Is zero",      simp == 0)
        kv("Is constant",  simp.is_number)
        ops_before = count_ops(p.expr)
        ops_after  = count_ops(simp)
        kv("Complexity before", ops_before)
        kv("Complexity after",  ops_after)
        if ops_before > 0:
            kv("Reduction", f"{100*(ops_before-ops_after)/ops_before:.0f}%")
        if simp == 0:
            finding("Expression = 0 for ALL inputs — IDENTITY confirmed")
        elif simp.is_number:
            finding(f"Expression is constant = {simp}")
        r["is_identity"] = (simp == 0)

    # ── FACTORING ─────────────────────────────────────────────────────────────
    elif p.ptype == PT.FACTORING:
        fac   = factor(p.expr)
        flist = factor_list(p.expr)
        r["factored"]    = str(fac)
        r["factor_list"] = str(flist)
        kv("Factored form", fac)

        # Analyse each factor
        for i, (fi, mult) in enumerate(flist[1]):
            roots_i = []
            try:
                roots_i = solve(fi, v)
            except Exception:
                pass
            kv(f"  factor[{i}]", f"{fi}^{mult}  →  roots: {roots_i}")
            r[f"factor_{i}"] = {"expr": str(fi), "mult": mult,
                                 "roots": [str(r_) for r_ in roots_i]}

        # Re-expand to verify
        reexp = expand(fac)
        check = simplify(reexp - expand(p.expr))
        ok(f"Expand(factor) − original = {check}")
        r["verified"] = (check == 0)

    # ── SUMMATION ─────────────────────────────────────────────────────────────
    elif p.ptype == PT.SUM:
        k = symbols('k', positive=True, integer=True)
        n = symbols('n', positive=True, integer=True)
        res  = summation(k, (k, 1, n))
        fac  = factor(res)
        r["formula"]  = str(res)
        r["factored"] = str(fac)
        kv("Formula",      res)
        kv("Factored",     fac)

        # Pattern: f(n) − f(n−1) should equal n
        diff_check = simplify(res - res.subs(n, n-1))
        kv("f(n) − f(n−1)", diff_check)
        finding(f"Difference property: f(n)−f(n−1) = {diff_check} = n ✓")

        # Inductive structure
        kv("f(1)",   int(res.subs(n,1)))
        kv("f(n)/n", simplify(res / n))
        finding("Formula is arithmetic mean × n")
        r["diff_property"] = str(diff_check)

    # ── PROOF ─────────────────────────────────────────────────────────────────
    elif p.ptype == PT.PROOF:
        body = p.meta.get("body", "")
        if "sqrt(2)" in body.lower():
            note("\nFormal proof trace:")
            steps = [
                ("Assume",      "√2 = p/q with gcd(p,q)=1"),
                ("Square",      "2 = p²/q²  ⟹  p² = 2q²"),
                ("Deduce",      "p² even  ⟹  p even  ⟹  p = 2m"),
                ("Substitute",  "(2m)² = 2q²  ⟹  4m² = 2q²  ⟹  q² = 2m²"),
                ("Deduce",      "q² even  ⟹  q even"),
                ("Contradict",  "p,q both even  contradicts  gcd(p,q)=1"),
                ("Conclude",    "√2 ∉ ℚ  □"),
            ]
            for step, desc in steps:
                print(f"    {Y}{step:<14}{RST}{desc}")
            r["proof"] = steps
            finding("Proof by contradiction: 7-step derivation complete")

        elif "prime" in body.lower():
            note("\nFormal proof trace:")
            steps = [
                ("Assume",    "Finitely many primes: {p₁, p₂, …, pₖ}"),
                ("Construct", "N = p₁ · p₂ · … · pₖ + 1"),
                ("Observe",   "N > pᵢ for all i, so N is not in our list"),
                ("Factor",    "N must have a prime factor q"),
                ("But",       "q cannot be any pᵢ (each leaves remainder 1)"),
                ("Contradict","No prime divides N — impossible for N>1"),
                ("Conclude",  "Primes are infinite  □"),
            ]
            for step, desc in steps:
                print(f"    {Y}{step:<14}{RST}{desc}")
            r["proof"] = steps
            finding("Euclid's proof: infinite primes by construction")

    return r


def phase_05(p: Problem, prev: dict) -> dict:
    section(5, "GENERALIZE",
            "Name the condition, not the cases")
    r = {}

    v = p.var

    # ── LINEAR → general ax + b = 0 ──────────────────────────────────────────
    if p.ptype == PT.LINEAR:
        a_, b_ = symbols('a b', nonzero=True)
        gen    = a_*v + b_
        sol    = solve(gen, v)[0]
        r["general_form"]      = "a·x + b = 0"
        r["general_solution"]  = str(sol)
        r["governing"]         = "a ≠ 0 (if a=0: either 0=b contradiction, or 0=0 trivial)"
        kv("General form",       r["general_form"])
        kv("General solution",   r["general_solution"])
        kv("Governing condition", r["governing"])
        finding("x = −b/a  iff  a ≠ 0")

        # Show our specific case
        try:
            poly   = Poly(p.expr, v)
            A, B   = [int(c) for c in poly.all_coeffs()]
            finding(f"Our case: a={A}, b={B}  →  x = {-B}/{A} = {Rational(-B,A)}")
        except Exception:
            pass

    # ── QUADRATIC → general formula + discriminant ────────────────────────────
    elif p.ptype == PT.QUADRATIC:
        a_, b_, c_ = symbols('a b c')
        gen        = a_*v**2 + b_*v + c_
        gen_sols   = solve(gen, v)
        disc_sym   = b_**2 - 4*a_*c_
        r["general_form"]       = "a·x² + b·x + c = 0"
        r["quadratic_formula"]  = [str(s) for s in gen_sols]
        r["discriminant_sym"]   = str(disc_sym)
        r["governing_condition"]= "Δ=b²-4ac governs nature of roots"
        r["cases"] = {
            "Δ > 0": "two distinct real roots",
            "Δ = 0": "one repeated real root",
            "Δ < 0": "two complex conjugate roots",
        }
        kv("General form",        r["general_form"])
        kv("Quadratic formula",   r["quadratic_formula"])
        kv("Discriminant Δ",      disc_sym)
        for case, meaning in r["cases"].items():
            kv(f"  {case}", meaning)
        finding("Nature of roots determined entirely by Δ = b²−4ac")

        # Our specific discriminant
        disc_val = prev.get("discriminant", "?")
        finding(f"Our Δ = {disc_val} → "
                + ("two real roots" if isinstance(disc_val,int) and disc_val>0
                   else "double root" if disc_val==0 else "complex roots"))

    # ── CUBIC → Cardano context ───────────────────────────────────────────────
    elif p.ptype == PT.CUBIC:
        r["general_form"] = "ax³ + bx² + cx + d = 0"
        r["method"]       = "Cardano's formula (via depressed cubic)"
        r["discriminant"] = "Δ = 18abcd − 4b³d + b²c² − 4ac³ − 27a²d²"
        r["governing"] = {
            "Δ > 0": "three distinct real roots",
            "Δ = 0": "repeated root",
            "Δ < 0": "one real root, two complex conjugate",
        }
        kv("General form",  r["general_form"])
        kv("Method",        r["method"])
        for case, meaning in r["governing"].items():
            kv(f"  {case}", meaning)

        # General symbolic solution
        a_,b_,c_,d_ = symbols('a b c d')
        gen_cubic = a_*v**3 + b_*v**2 + c_*v + d_
        try:
            gen_sols = solve(gen_cubic, v)
            finding(f"Symbolic solutions exist ({len(gen_sols)} roots)")
        except Exception:
            pass

    # ── TRIG IDENTITY → family ────────────────────────────────────────────────
    elif p.ptype in (PT.TRIG_ID, PT.SIMPLIFY):
        r["pythagorean_family"] = {
            "sin²θ + cos²θ = 1":  "Fundamental — all x ∈ ℝ",
            "1 + tan²θ = sec²θ":  "Holds where cos θ ≠ 0",
            "1 + cot²θ = csc²θ":  "Holds where sin θ ≠ 0",
        }
        # Verify the family with sympy
        theta = symbols('theta')
        checks = {
            "sin²+cos²": trigsimp(sin(theta)**2 + cos(theta)**2 - 1),
            "1+tan²":    trigsimp(1 + tan(theta)**2 - sec(theta)**2),
        }
        for name_, val in checks.items():
            kv(f"  {name_}", f"= {val}  {'✓' if val==0 else '?'}")
        r["governing"] = "All follow from unit-circle definition: sin²+cos²=1"
        finding("Pythagorean family — 3 identities, 1 governing principle")

    # ── FACTORING → difference of squares / sum of cubes family ──────────────
    elif p.ptype == PT.FACTORING:
        a_, b_ = symbols('a b')
        identities = {
            "a²−b²":    factor(a_**2 - b_**2),
            "a³−b³":    factor(a_**3 - b_**3),
            "a³+b³":    factor(a_**3 + b_**3),
            "a⁴−b⁴":    factor(a_**4 - b_**4),
        }
        r["factoring_identities"] = {k: str(v)
                                      for k, v in identities.items()}
        kv("Algebraic identities", "")
        for form, factored in identities.items():
            kv(f"  {form}", str(factored))
        finding("Our problem is an instance of one of these families")
        r["governing"] = "aⁿ−bⁿ = (a−b)(aⁿ⁻¹+...+bⁿ⁻¹) for integer n≥1"

    # ── SUMMATION → power sums family ────────────────────────────────────────
    elif p.ptype == PT.SUM:
        k = symbols('k', positive=True, integer=True)
        n = symbols('n', positive=True, integer=True)
        power_sums = {}
        for p_ in range(1, 5):
            try:
                s = summation(k**p_, (k, 1, n))
                power_sums[f"Σk^{p_}"] = str(factor(s))
            except Exception:
                pass
        r["power_sums"] = power_sums
        kv("Power sum family", "")
        for name_, form in power_sums.items():
            kv(f"  {name_}", form)
        r["governing"] = "Faulhaber's formula: Σk^p is degree-(p+1) polynomial in n"
        finding("Governing condition: Σk^p = poly of degree p+1 in n")
        finding("Sum of first n integers = n(n+1)/2 is the p=1 case")

    # ── PROOF → governing theorem ─────────────────────────────────────────────
    elif p.ptype == PT.PROOF:
        body = p.meta.get("body", "")
        if "sqrt(2)" in body.lower():
            r["general_theorem"] = "√n ∉ ℚ  ⟺  n is not a perfect square"
            r["governing"]       = "Irrationality governed by perfect-square condition"
            # Verify boundary
            for n_val in range(1, 10):
                is_sq  = sp.sqrt(n_val).is_integer
                is_rat = sp.sqrt(n_val).is_rational
                kv(f"  √{n_val}", ("∈ ℚ (perfect square)" if is_sq
                                    else "∉ ℚ (irrational)"))
            finding("√n is rational ⟺ n is a perfect square")

    return r


def phase_06(p: Problem, prev: dict) -> dict:
    section(6, "PROVE LIMITS",
            "Find the boundary; state the obstruction")
    r = {}

    v = p.var

    # ── QUADRATIC LIMITS ─────────────────────────────────────────────────────
    if p.ptype == PT.QUADRATIC:
        disc_val = prev.get("discriminant", None)

        r["positive_result"] = (
            "For any a,b,c ∈ ℝ with a≠0 and Δ≥0, "
            "real solutions always exist: x = (−b ± √Δ) / 2a"
        )
        r["negative_result"] = (
            "For Δ < 0: no real solutions. "
            "Two complex conjugate roots exist in ℂ."
        )
        r["degenerate"] = "a=0: not quadratic; becomes linear (one solution)"

        kv("Positive result",  r["positive_result"])
        kv("Negative result",  r["negative_result"])
        kv("Degenerate (a=0)", r["degenerate"])

        # Boundary: Δ = 0
        a_,b_,c_ = symbols('a b c', real=True)
        boundary = Eq(b_**2 - 4*a_*c_, 0)
        kv("Boundary condition", str(boundary))
        finding("Boundary Δ=0: double root at x = −b/2a")

        # Show all roots over ℂ for our problem
        try:
            all_sols = solve(p.expr, v, domain=sp.CC)
            kv("All roots over ℂ", [str(s) for s in all_sols])
            r["complex_roots"] = [str(s) for s in all_sols]
        except Exception:
            pass

    # ── LINEAR LIMITS ─────────────────────────────────────────────────────────
    elif p.ptype == PT.LINEAR:
        r["positive_result"] = "Unique solution exists whenever a ≠ 0"
        r["degenerate_a0_b0"] = "0=0: infinitely many solutions (identity)"
        r["degenerate_a0_bnz"] = "0=b≠0: no solution (contradiction)"
        kv("Positive", r["positive_result"])
        kv("a=0, b=0", r["degenerate_a0_b0"])
        kv("a=0, b≠0", r["degenerate_a0_bnz"])
        finding("Linear equation has exactly one solution iff leading coefficient ≠ 0")

    # ── CUBIC LIMITS ─────────────────────────────────────────────────────────
    elif p.ptype == PT.CUBIC:
        r["positive_result"] = "Cubic always has at least one real root (degree 3, real coefficients)"
        r["why"]             = "Complex roots come in conjugate pairs; odd degree → ≥1 real root"
        r["Abel_Ruffini"]    = "No general formula in radicals for degree ≥ 5 (Abel-Ruffini theorem)"
        kv("Always one real root", r["positive_result"])
        kv("Why",                  r["why"])
        kv("Degree ≥ 5",           r["Abel_Ruffini"])
        finding("Cubic: guaranteed ≥1 real root by intermediate value theorem")

    # ── TRIG IDENTITY LIMITS ─────────────────────────────────────────────────
    elif p.ptype in (PT.TRIG_ID, PT.SIMPLIFY):
        r["sin_cos_domain"]  = "sin²+cos²=1 holds for ALL x ∈ ℝ — no exceptions"
        r["tan_domain"]      = "1+tan²=sec² fails at x = π/2 + nπ (where cos=0)"
        r["cot_domain"]      = "1+cot²=csc² fails at x = nπ (where sin=0)"
        r["identity_vs_eq"]  = "An identity holds universally; an equation holds at specific points"
        for k_, v_ in r.items():
            kv(k_, v_)
        finding("Pythagorean identity sin²+cos²=1 has NO exceptions in ℝ")

    # ── FACTORING LIMITS ─────────────────────────────────────────────────────
    elif p.ptype == PT.FACTORING:
        e = p.expr
        r["over_Q"] = "Rational factorization: splits into rational irreducibles"
        r["over_R"] = "Real factorization: all factors are linear or quadratic"
        r["over_C"] = "Complex factorization: always splits into linear factors"
        # Check irreducibility over Q
        if v:
            try:
                poly  = Poly(e, v)
                irred = poly.is_irreducible
                r["irreducible_over_Q"] = irred
                kv("Irreducible over ℚ", irred)
                if irred:
                    finding("Cannot be factored further over ℚ")
            except Exception:
                pass
            try:
                rr = real_roots(e)
                ar = all_roots(e)
                r["real_roots"]    = [str(r_) for r_ in rr]
                r["complex_roots"] = [str(r_) for r_ in ar if not r_.is_real]
                kv("Real roots",    r["real_roots"])
                kv("Complex roots", r["complex_roots"])
                if r["complex_roots"]:
                    finding("Some roots are complex — irreducible over ℝ too")
            except Exception:
                pass

    # ── SUMMATION LIMITS ─────────────────────────────────────────────────────
    elif p.ptype == PT.SUM:
        k = symbols('k', positive=True, integer=True)
        n = symbols('n', positive=True, integer=True)
        r["formula_valid"] = "n ≥ 1, n ∈ ℤ"
        r["n=0"]           = "Empty sum = 0; formula gives 0·1/2 = 0 ✓"

        # Infinite sum diverges
        try:
            inf_sum = summation(k, (k, 1, oo))
            r["infinite_sum"] = str(inf_sum)
            kv("Σk to ∞", inf_sum)
            finding(f"Σk from 1 to ∞ = {inf_sum} — diverges")
        except Exception:
            pass

        # Compare convergence
        try:
            harm  = summation(1/k, (k, 1, oo))
            inv_sq= summation(1/k**2, (k, 1, oo))
            kv("Σ 1/k (harmonic)",  str(harm))
            kv("Σ 1/k² (Basel)",   str(inv_sq))
            r["convergence_rule"] = "Σ 1/k^p converges iff p > 1"
            finding("Governing: Σ 1/kᵖ converges ⟺ p > 1  (p-series test)")
        except Exception:
            pass

    # ── PROOF LIMITS ─────────────────────────────────────────────────────────
    elif p.ptype == PT.PROOF:
        body = p.meta.get("body", "")
        if "sqrt(2)" in body.lower():
            r["proved"]     = "√2 ∉ ℚ"
            r["generalises"]= "√p ∉ ℚ for any prime p"
            r["fails_for"]  = "√n ∈ ℚ when n is a perfect square"
            r["governing"]  = "√n ∈ ℚ  ⟺  n is a perfect square"
            kv("Proved",       r["proved"])
            kv("Generalises",  r["generalises"])
            kv("Fails for",    r["fails_for"])
            kv("Governing",    r["governing"])
            finding("Boundary: n a perfect square ↔ √n rational")
        elif "prime" in body.lower():
            r["proved"]      = "Infinitely many primes"
            r["density"]     = "π(n) ~ n/ln(n)  (Prime Number Theorem)"
            r["twin_primes"] = "Infinitely many twin primes — OPEN (unproven)"
            kv("Proved",       r["proved"])
            kv("Density",      r["density"])
            kv("Open question",r["twin_primes"])
            finding("Euclid's proof: infinite primes; twin-prime conjecture remains open")

    # ── FINAL ANSWER ─────────────────────────────────────────────────────────
    print(f"\n{hr('═')}")
    print(f"{W}FINAL ANSWER{RST}")
    print(hr('─'))

    final = _final_answer(p)
    r["final_answer"] = final
    print(f"  {G}{final}{RST}")
    print(hr('═'))
    return r


def _final_answer(p: Problem) -> str:
    v = p.var
    if p.ptype in (PT.LINEAR, PT.QUADRATIC, PT.CUBIC, PT.POLY):
        try:
            sols = solve(p.expr, v)
            return f"Solutions to {p.raw}: {', '.join(str(s) for s in sols)}"
        except Exception:
            return "See phase computations"
    elif p.ptype == PT.FACTORING:
        try:
            return f"Factored form: {factor(p.expr)}"
        except Exception:
            return "See phase computations"
    elif p.ptype in (PT.TRIG_ID, PT.SIMPLIFY):
        try:
            simp = trigsimp(p.expr)
            return (f"Identity confirmed: simplifies to {simp}"
                    if simp == 0 else f"Simplified: {simp}")
        except Exception:
            return "See phase computations"
    elif p.ptype == PT.SUM:
        k = symbols('k', positive=True, integer=True)
        n = symbols('n', positive=True, integer=True)
        try:
            s = summation(k, (k, 1, n))
            return f"Sum of first n integers = {factor(s)} = n(n+1)/2"
        except Exception:
            return "See phase computations"
    elif p.ptype == PT.PROOF:
        body = p.meta.get("body", "")
        if "sqrt(2)" in body.lower():
            return "√2 is irrational. Proof by contradiction: assuming p/q (reduced) leads to both p and q even, contradicting gcd(p,q)=1."
        elif "prime" in body.lower():
            return "There are infinitely many primes. Euclid: any finite list p₁…pₖ yields N=p₁…pₖ+1, which has a prime factor outside the list."
    return "See phase computations above"


# ════════════════════════════════════════════════════════════════════════════
# ENTRY POINT
# ════════════════════════════════════════════════════════════════════════════

def run(raw: str):
    prob = classify(raw)
    print(f"\n{hr('═')}")
    print(f"{W}DISCOVERY ENGINE{RST}")
    print(hr())
    print(f"  {W}Problem:{RST}  {Y}{raw}{RST}")
    print(f"  {DIM}Type:{RST}     {prob.ptype.value}")
    print(f"  {DIM}Variable:{RST} {prob.var}")
    print(hr('═'))

    if prob.ptype == PT.UNKNOWN:
        print(f"{R}Could not parse. Try: 'x^2 - 5x + 6 = 0' or 'factor x^4-16'{RST}")
        return

    g1 = phase_01(prob)
    g2 = phase_02(prob, g1)
    g3 = phase_03(prob, g2)
    g4 = phase_04(prob, g3)
    g5 = phase_05(prob, g4)
    g6 = phase_06(prob, g5)

    # Summary
    print(f"\n{hr()}")
    print(f"{W}PHASE SUMMARY{RST}")
    print(hr('·'))
    titles = {1:"Ground Truth", 2:"Direct Attack", 3:"Structure Hunt",
              4:"Pattern Lock", 5:"Generalize",    6:"Prove Limits"}
    for i, (g, title) in enumerate(zip([g1,g2,g3,g4,g5,g6], titles.values()), 1):
        fa = g.get("final_answer","")
        line = fa[:60] if fa else (
            str(g.get("solutions", g.get("factored",
                g.get("formula", g.get("simplified", "✓")))))[:60]
        )
        print(f"  {PHASE_CLR[i]}{i:02d} {title:<16}{RST} {line}")
    print(hr('═'))


TESTS = [
    ("x^2 - 5x + 6 = 0",              "Quadratic with integer roots"),
    ("2x + 3 = 7",                     "Linear equation"),
    ("x^3 - 6x^2 + 11x - 6 = 0",      "Cubic with 3 integer roots"),
    ("sin(x)^2 + cos(x)^2",            "Pythagorean identity"),
    ("factor x^4 - 16",                "Difference of squares chain"),
    ("sum of first n integers",        "Classic summation"),
    ("prove sqrt(2) is irrational",    "Irrationality proof"),
]

def run_tests():
    print(f"\n{hr('═')}")
    print(f"{W}DISCOVERY ENGINE — TEST SUITE{RST}")
    print(f"{DIM}Running {len(TESTS)} problems{RST}")
    print(hr('═'))
    passed = 0
    for raw, desc in TESTS:
        print(f"\n{B}{'─'*60}{RST}")
        print(f"{B}TEST: {desc}{RST}")
        print(f"{DIM}{raw}{RST}")
        try:
            run(raw)
            ok(f"PASSED: {desc}")
            passed += 1
        except Exception as e:
            fail(f"FAILED: {desc} — {e}")
            traceback.print_exc()
    print(f"\n{hr('═')}")
    print(f"{G if passed==len(TESTS) else Y}Results: {passed}/{len(TESTS)} passed{RST}")
    print(hr('═'))


if __name__ == "__main__":
    args = sys.argv[1:]
    if not args:
        print(__doc__)
        print(f"\n{W}Available test problems:{RST}")
        for raw, desc in TESTS:
            print(f"  {DIM}{raw:<40}{RST} {desc}")
    elif args[0] == "--test":
        run_tests()
    else:
        run(" ".join(args))