"""Exact rational nearest images for the zero-tolerance CCM interface.

Finite binary inputs are treated as their exact rational values. A left inverse
bounds a complete integer box; exhaustive minimization includes every exact tie.
The certificate fields match the Lean specification in formal/rhf/VibeQCStage2.lean.
The Python program is tested correspondence code; kernel replay is optional and
is not a production runtime dependency. See docs/formal_exact_images.md.
"""
from dataclasses import dataclass
from fractions import Fraction as Q
from itertools import product
import math

def rational(value):
    if isinstance(value, (float, int)) and not math.isfinite(value):
        raise ValueError('finite represented inputs required')
    try:
        return Q(value)
    except (TypeError, ValueError, OverflowError) as exc:
        raise ValueError('finite real or rational input required') from exc


class SearchBudgetExceeded(ValueError):
    pass


def matrix3(A):
    if len(A) != 3 or any(len(row) != 3 for row in A):
        raise ValueError('3 by 3 column-basis matrix required')
    return tuple(tuple(rational(x) for x in row) for row in A)


def inverse3(A):
    a = [list(row)+[Q(i == j) for j in range(3)] for i, row in enumerate(A)]
    for j in range(3):
        pivot = next((i for i in range(j, 3) if a[i][j]), None)
        if pivot is None:
            raise ValueError('singular lattice')
        a[j], a[pivot] = a[pivot], a[j]
        divisor = a[j][j]; a[j] = [v/divisor for v in a[j]]
        for i in range(3):
            if i != j:
                factor = a[i][j]; a[i] = [v-factor*w for v, w in zip(a[i], a[j])]
    return tuple(tuple(row[3:]) for row in a)


def matvec(A, x):
    return tuple(sum((a*b for a, b in zip(row, x)), Q(0)) for row in A)


def cost(A, x, n):
    v = matvec(A, n)
    return sum(((a-b)**2 for a, b in zip(x, v)), Q(0))


def ceil_sqrt(q):
    if q < 0:
        raise ValueError('negative square')
    r = math.isqrt(q.numerator//q.denominator)
    return r if Q(r*r) == q else r+1


def box_points(lo, hi, budget):
    if type(budget) is not int or budget < 1:
        raise ValueError('positive integer work budget required')
    size = math.prod(max(0, h-l+1) for l, h in zip(lo, hi))
    if size > budget:
        raise SearchBudgetExceeded(f'complete box needs {size} candidates, budget {budget}')
    return product(*(range(l, h+1) for l, h in zip(lo, hi)))


@dataclass(frozen=True)
class ImageCertificate:
    A: tuple
    H: tuple
    x: tuple
    R: Q
    lo: tuple
    hi: tuple
    best: tuple
    ties: tuple


def certify_image(A, x, max_candidates=100000, candidate=None):
    """Exact complete 3D triclinic search; no Minkowski or shell hypothesis."""
    A = matrix3(A)
    if len(x) != 3:
        raise ValueError('three displacement coordinates required')
    x = tuple(map(rational, x)); H = inverse3(A); f = matvec(H, x)
    incumbent = tuple(round(v) for v in f) if candidate is None else tuple(candidate)
    if len(incumbent) != 3 or any(type(v) is not int for v in incumbent):
        raise ValueError('integer candidate required')
    R = Q(ceil_sqrt(cost(A, x, incumbent)))
    radii = tuple(sum(map(abs, row))*R for row in H)
    lo = tuple(math.floor(v-r) for v, r in zip(f, radii))
    hi = tuple(math.ceil(v+r) for v, r in zip(f, radii))
    best_cost, ties = None, []
    for n in box_points(lo, hi, max_candidates):
        value = cost(A, x, n)
        if best_cost is None or value < best_cost:
            best_cost, ties = value, [n]
        elif value == best_cost:
            ties.append(n)
    if not ties:
        raise AssertionError('complete box unexpectedly empty')
    certificate = ImageCertificate(A, H, x, R, lo, hi, ties[0], tuple(ties))
    verify_image(certificate, max_candidates)
    return certificate


def verify_image(c, max_candidates=100000):
    """Recheck all ValidImageCert premises and equality of the complete tie set."""
    A, H = matrix3(c.A), matrix3(c.H)
    if len(c.x) != 3 or any(len(v) != 3 for v in (c.lo, c.hi, c.best)):
        raise ValueError('certificate shape mismatch')
    if any(type(v) is not int for row in (c.lo, c.hi, c.best, *c.ties) for v in row):
        raise ValueError('integer images required')
    x, R = tuple(map(rational, c.x)), rational(c.R)
    if any(sum(H[i][a]*A[a][j] for a in range(3)) != Q(i == j)
           for i in range(3) for j in range(3)):
        raise ValueError('inverse witness invalid')
    best = cost(A, x, c.best)
    if R < 0 or best > R*R:
        raise ValueError('incumbent radius invalid')
    f = matvec(H, x); radii = tuple(sum(map(abs, row))*R for row in H)
    if any(l > v-r or v+r > h for l, h, v, r in zip(c.lo, c.hi, f, radii)):
        raise ValueError('box completeness inequalities invalid')
    ties = []
    for n in box_points(c.lo, c.hi, max_candidates):
        value = cost(A, x, n)
        if value < best:
            raise ValueError('selected image is not nearest')
        if value == best:
            ties.append(n)
    if tuple(ties) != c.ties or c.best not in ties:
        raise ValueError('tie set incomplete, duplicated or misordered')
    return True