Result Types

LeanCert returns rich result objects containing both numerical data and verification certificates.

BoundsResult

Returned by find_bounds().

leancert.result.BoundsResult dataclass

Result of finding global bounds.

Contains intervals enclosing the minimum and maximum values, along with a verification certificate.

Access Patterns

Get the interval bounds (Interval objects)

result.min_bound # Interval containing true minimum result.max_bound # Interval containing true maximum

Get exact Fraction endpoints

result.min_bound.lo # Lower bound of min interval (rigorous) result.max_bound.hi # Upper bound of max interval (rigorous)

Get float approximations (for comparisons/display)

result.min_lo # float(min_bound.lo) - guaranteed lower bound result.min_hi # float(min_bound.hi) - upper estimate of minimum result.max_lo # float(max_bound.lo) - lower estimate of maximum result.max_hi # float(max_bound.hi) - guaranteed upper bound

Get midpoint approximations

result.min_value # midpoint of min_bound (approximate) result.max_value # midpoint of max_bound (approximate)

Source code in python/leancert/result.py

@dataclass
class BoundsResult:
    """
    Result of finding global bounds.

    Contains intervals enclosing the minimum and maximum values,
    along with a verification certificate.

    Access Patterns:
        # Get the interval bounds (Interval objects)
        result.min_bound  # Interval containing true minimum
        result.max_bound  # Interval containing true maximum

        # Get exact Fraction endpoints
        result.min_bound.lo  # Lower bound of min interval (rigorous)
        result.max_bound.hi  # Upper bound of max interval (rigorous)

        # Get float approximations (for comparisons/display)
        result.min_lo  # float(min_bound.lo) - guaranteed lower bound
        result.min_hi  # float(min_bound.hi) - upper estimate of minimum
        result.max_lo  # float(max_bound.lo) - lower estimate of maximum
        result.max_hi  # float(max_bound.hi) - guaranteed upper bound

        # Get midpoint approximations
        result.min_value  # midpoint of min_bound (approximate)
        result.max_value  # midpoint of max_bound (approximate)
    """
    min_bound: Interval
    max_bound: Interval
    verified: bool
    certificate: Optional[Certificate] = None

    # --- Convenience float accessors for bounds ---

    @property
    def min_lo(self) -> float:
        """Guaranteed lower bound on minimum value."""
        return float(self.min_bound.lo)

    @property
    def min_hi(self) -> float:
        """Upper estimate of minimum value."""
        return float(self.min_bound.hi)

    @property
    def max_lo(self) -> float:
        """Lower estimate of maximum value."""
        return float(self.max_bound.lo)

    @property
    def max_hi(self) -> float:
        """Guaranteed upper bound on maximum value."""
        return float(self.max_bound.hi)

    @property
    def min_value(self) -> float:
        """Approximate minimum (midpoint of min_bound)."""
        return float(self.min_bound.midpoint())

    @property
    def max_value(self) -> float:
        """Approximate maximum (midpoint of max_bound)."""
        return float(self.max_bound.midpoint())

    def save(self, path: str) -> None:
        """Save the certificate to a file."""
        if self.certificate:
            self.certificate.save(path)
        else:
            raise ValueError("No certificate available to save")

    def __repr__(self) -> str:
        status = "verified" if self.verified else "unverified"
        return (
            f"BoundsResult(\n"
            f"  min_bound={self.min_bound},\n"
            f"  max_bound={self.max_bound},\n"
            f"  verified={self.verified}\n"
            f")"
        )

max_hi property

Guaranteed upper bound on maximum value.

max_lo property

Lower estimate of maximum value.

max_value property

Approximate maximum (midpoint of max_bound).

min_hi property

Upper estimate of minimum value.

min_lo property

Guaranteed lower bound on minimum value.

min_value property

Approximate minimum (midpoint of min_bound).

save(path)

Save the certificate to a file.

Source code in python/leancert/result.py

def save(self, path: str) -> None:
    """Save the certificate to a file."""
    if self.certificate:
        self.certificate.save(path)
    else:
        raise ValueError("No certificate available to save")

RootsResult

Returned by find_roots().

leancert.result.RootsResult dataclass

Result of finding roots.

Contains intervals that may contain roots, with status indicating the certainty level.

Source code in python/leancert/result.py

@dataclass
class RootsResult:
    """
    Result of finding roots.

    Contains intervals that may contain roots, with status indicating
    the certainty level.
    """
    roots: list[RootInterval]
    iterations: int
    verified: bool
    certificate: Optional[Certificate] = None

    def confirmed_roots(self) -> list[RootInterval]:
        """Return only roots with confirmed sign change."""
        return [r for r in self.roots if r.status == 'confirmed']

    def possible_roots(self) -> list[RootInterval]:
        """Return roots that may exist but aren't confirmed."""
        return [r for r in self.roots if r.status == 'possible']

    def __repr__(self) -> str:
        confirmed = len(self.confirmed_roots())
        total = len(self.roots)
        return f"RootsResult({confirmed}/{total} confirmed, {self.iterations} iterations)"

confirmed_roots()

Return only roots with confirmed sign change.

Source code in python/leancert/result.py

def confirmed_roots(self) -> list[RootInterval]:
    """Return only roots with confirmed sign change."""
    return [r for r in self.roots if r.status == 'confirmed']

possible_roots()

Return roots that may exist but aren't confirmed.

Source code in python/leancert/result.py

def possible_roots(self) -> list[RootInterval]:
    """Return roots that may exist but aren't confirmed."""
    return [r for r in self.roots if r.status == 'possible']

RootInterval

Represents an isolating interval for a root.

leancert.result.RootInterval dataclass

A single root interval with its status.

Access Patterns

root.interval # The Interval object root.status # 'confirmed', 'possible', 'no_root', 'unique' root.lo # float lower bound of interval root.hi # float upper bound of interval root.value # float midpoint (approximate root location) root.width # float interval width (uncertainty)

Source code in python/leancert/result.py

@dataclass
class RootInterval:
    """
    A single root interval with its status.

    Access Patterns:
        root.interval       # The Interval object
        root.status         # 'confirmed', 'possible', 'no_root', 'unique'
        root.lo             # float lower bound of interval
        root.hi             # float upper bound of interval
        root.value          # float midpoint (approximate root location)
        root.width          # float interval width (uncertainty)
    """
    interval: Interval
    status: str  # 'confirmed', 'possible', 'no_root', 'unique'

    @property
    def lo(self) -> float:
        """Lower bound of root interval."""
        return float(self.interval.lo)

    @property
    def hi(self) -> float:
        """Upper bound of root interval."""
        return float(self.interval.hi)

    @property
    def value(self) -> float:
        """Approximate root value (midpoint of interval)."""
        return float(self.interval.midpoint())

    @property
    def width(self) -> float:
        """Width of root interval (uncertainty measure)."""
        return float(self.interval.width())

    def __repr__(self) -> str:
        return f"RootInterval({self.interval}, status='{self.status}')"

hi property

Upper bound of root interval.

lo property

Lower bound of root interval.

value property

Approximate root value (midpoint of interval).

width property

Width of root interval (uncertainty measure).

UniqueRootResult

Returned by find_unique_root().

leancert.result.UniqueRootResult dataclass

Result of unique root finding via Newton contraction.

When Newton iteration contracts, it proves both existence AND uniqueness of a root in the interval. This is a mathematically stronger result than ordinary root finding (which only proves existence via sign change).

Access Patterns

result.unique # bool - True if unique root proven result.interval # Interval object containing the root result.reason # 'newton_contraction', 'no_contraction', 'newton_step_failed' result.lo # float lower bound result.hi # float upper bound result.root_value # float midpoint (approximate root) result.width # float interval width (uncertainty)

Source code in python/leancert/result.py

@dataclass
class UniqueRootResult:
    """
    Result of unique root finding via Newton contraction.

    When Newton iteration contracts, it proves both existence AND uniqueness
    of a root in the interval. This is a mathematically stronger result
    than ordinary root finding (which only proves existence via sign change).

    Access Patterns:
        result.unique       # bool - True if unique root proven
        result.interval     # Interval object containing the root
        result.reason       # 'newton_contraction', 'no_contraction', 'newton_step_failed'
        result.lo           # float lower bound
        result.hi           # float upper bound
        result.root_value   # float midpoint (approximate root)
        result.width        # float interval width (uncertainty)
    """
    unique: bool  # True if unique root proven
    interval: Interval  # Refined interval containing the root
    reason: str  # 'newton_contraction', 'no_contraction', 'newton_step_failed'
    certificate: Optional[Certificate] = None

    @property
    def lo(self) -> float:
        """Lower bound of root interval."""
        return float(self.interval.lo)

    @property
    def hi(self) -> float:
        """Upper bound of root interval."""
        return float(self.interval.hi)

    @property
    def root_value(self) -> float:
        """Approximate root value (midpoint of interval)."""
        return float(self.interval.midpoint())

    @property
    def width(self) -> float:
        """Width of root interval (uncertainty measure)."""
        return float(self.interval.width())

    def __repr__(self) -> str:
        if self.unique:
            return f"UniqueRootResult(UNIQUE root in {self.interval})"
        return f"UniqueRootResult(not proven unique, {self.reason})"

hi property

Upper bound of root interval.

lo property

Lower bound of root interval.

root_value property

Approximate root value (midpoint of interval).

width property

Width of root interval (uncertainty measure).

IntegralResult

Returned by integrate().

leancert.result.IntegralResult dataclass

Result of numerical integration.

Contains an interval enclosing the true integral value.

Access Patterns

result.bounds # Interval object enclosing true integral result.verified # bool verification status result.lo # float guaranteed lower bound result.hi # float guaranteed upper bound result.value # float midpoint (approximate integral) result.error # float maximum error (interval width)

Source code in python/leancert/result.py

@dataclass
class IntegralResult:
    """
    Result of numerical integration.

    Contains an interval enclosing the true integral value.

    Access Patterns:
        result.bounds       # Interval object enclosing true integral
        result.verified     # bool verification status
        result.lo           # float guaranteed lower bound
        result.hi           # float guaranteed upper bound
        result.value        # float midpoint (approximate integral)
        result.error        # float maximum error (interval width)
    """
    bounds: Interval
    verified: bool
    certificate: Optional[Certificate] = None

    @property
    def lo(self) -> float:
        """Guaranteed lower bound on integral."""
        return float(self.bounds.lo)

    @property
    def hi(self) -> float:
        """Guaranteed upper bound on integral."""
        return float(self.bounds.hi)

    @property
    def value(self) -> float:
        """Approximate integral value (midpoint)."""
        return float(self.bounds.midpoint())

    @property
    def error(self) -> float:
        """Maximum error (width of bounds interval)."""
        return float(self.bounds.width())

    def error_bound(self) -> Fraction:
        """Maximum error (width of the bounds interval). Returns exact Fraction."""
        return self.bounds.width()

    def __repr__(self) -> str:
        return f"IntegralResult(bounds={self.bounds}, error<={self.error:.2e})"

error property

Maximum error (width of bounds interval).

hi property

Guaranteed upper bound on integral.

lo property

Guaranteed lower bound on integral.

value property

Approximate integral value (midpoint).

error_bound()

Maximum error (width of the bounds interval). Returns exact Fraction.

Source code in python/leancert/result.py

def error_bound(self) -> Fraction:
    """Maximum error (width of the bounds interval). Returns exact Fraction."""
    return self.bounds.width()

Certificate

Contains the verification certificate that can be exported to Lean.

leancert.result.Certificate dataclass

A verification certificate that can be saved and reloaded.

Certificates contain all the information needed to reproduce and verify a computation.

Source code in python/leancert/result.py

@dataclass
class Certificate:
    """
    A verification certificate that can be saved and reloaded.

    Certificates contain all the information needed to reproduce
    and verify a computation.
    """
    operation: str
    expr_json: dict[str, Any]
    domain_json: list[dict[str, Any]]
    result_json: dict[str, Any]
    verified: bool
    lean_version: str
    leancert_version: str
    computation_time_ms: Optional[float] = None
    metadata: dict[str, Any] = field(default_factory=dict)

    def to_dict(self) -> dict[str, Any]:
        """Convert to JSON-serializable dictionary."""
        return {
            'operation': self.operation,
            'expr': self.expr_json,
            'domain': self.domain_json,
            'result': self.result_json,
            'verified': self.verified,
            'lean_version': self.lean_version,
            'leancert_version': self.leancert_version,
            'computation_time_ms': self.computation_time_ms,
            'metadata': self.metadata,
        }

    def save(self, path: str) -> None:
        """Save certificate to a JSON file."""
        with open(path, 'w') as f:
            json.dump(self.to_dict(), f, indent=2)

    @classmethod
    def load(cls, path: str) -> Certificate:
        """Load certificate from a JSON file."""
        with open(path) as f:
            data = json.load(f)

        return cls(
            operation=data['operation'],
            expr_json=data['expr'],
            domain_json=data['domain'],
            result_json=data['result'],
            verified=data['verified'],
            lean_version=data['lean_version'],
            leancert_version=data['leancert_version'],
            computation_time_ms=data.get('computation_time_ms'),
            metadata=data.get('metadata', {}),
        )

    def hash(self) -> str:
        """Compute SHA256 hash of the certificate content."""
        # Create deterministic JSON string
        content = json.dumps(self.to_dict(), sort_keys=True)
        return hashlib.sha256(content.encode()).hexdigest()

    def to_lean_tactic(self) -> str:
        """
        Generate Lean tactic code that reproduces the verified proof.

        Returns a string of Lean code that can be pasted into a Lean file.
        This provides the "round trip" - Python finds the certificate,
        then generates Lean code that verifies it.

        Example output for find_bounds:
            theorem bound_check : ∀ x ∈ Set.Icc 0 1, x^2 ≤ 1 := by
              interval_bound 10

        Example output for verify_bound:
            theorem upper_bound_check : ∀ x ∈ I, f x ≤ 1.5 := by
              interval_bound 10
        """
        lines = []
        lines.append(f"-- Certificate hash: {self.hash()[:16]}...")
        lines.append(f"-- Generated from: {self.operation}")
        lines.append("")

        if self.operation == 'find_bounds':
            lines.extend(self._to_lean_find_bounds())
        elif self.operation == 'verify_bound':
            lines.extend(self._to_lean_verify_bound())
        elif self.operation == 'find_roots':
            lines.extend(self._to_lean_find_roots())
        elif self.operation == 'integrate':
            lines.extend(self._to_lean_integrate())
        else:
            lines.append(f"-- Unknown operation: {self.operation}")
            lines.append(f"-- Raw result: {self.result_json}")

        return '\n'.join(lines)

    def _to_lean_find_bounds(self) -> list[str]:
        """Generate Lean code for find_bounds operation."""
        lines = []
        expr_lean = self._expr_to_lean(self.expr_json)
        domain_lean = self._domain_to_lean(self.domain_json)
        min_lo = self.result_json.get('min', {}).get('lo', {})
        max_hi = self.result_json.get('max', {}).get('hi', {})
        taylor_depth = self.metadata.get('taylor_depth', 10)

        lines.append(f"-- Expression: {expr_lean}")
        lines.append(f"-- Domain: {domain_lean}")
        lines.append("")
        lines.append(f"-- Verified min ≥ {self._rat_to_float(min_lo):.6f}")
        lines.append(f"-- Verified max ≤ {self._rat_to_float(max_hi):.6f}")
        lines.append("")
        lines.append("theorem bounds_check :")
        lines.append(f"    ∀ x ∈ {domain_lean}, {self._rat_to_float(min_lo):.6f} ≤ {expr_lean} ∧ {expr_lean} ≤ {self._rat_to_float(max_hi):.6f} := by")
        lines.append(f"  interval_bound {taylor_depth}")

        return lines

    def _to_lean_verify_bound(self) -> list[str]:
        """Generate Lean code for verify_bound operation."""
        lines = []
        expr_lean = self._expr_to_lean(self.expr_json)
        domain_lean = self._domain_to_lean(self.domain_json)
        taylor_depth = self.metadata.get('taylor_depth', 10)

        bound_type = self.result_json.get('bound_type', 'unknown')
        bound_value = self.result_json.get('bound_value', 0)

        lines.append(f"-- Expression: {expr_lean}")
        lines.append(f"-- Domain: {domain_lean}")
        lines.append("")

        if bound_type == 'upper':
            lines.append(f"theorem upper_bound_check : ∀ x ∈ {domain_lean}, {expr_lean} ≤ {bound_value} := by")
        elif bound_type == 'lower':
            lines.append(f"theorem lower_bound_check : ∀ x ∈ {domain_lean}, {bound_value} ≤ {expr_lean} := by")
        else:
            lines.append(f"theorem bound_check : ∀ x ∈ {domain_lean}, ... := by")

        lines.append(f"  interval_bound {taylor_depth}")

        return lines

    def _to_lean_find_roots(self) -> list[str]:
        """Generate Lean code for find_roots operation."""
        lines = []
        expr_lean = self._expr_to_lean(self.expr_json)

        lines.append(f"-- Expression: {expr_lean}")
        lines.append("-- Root existence verified via IVT (sign change)")
        lines.append("")
        lines.append("-- Roots found:")

        roots = self.result_json.get('roots', [])
        for i, root in enumerate(roots):
            lo = self._rat_to_float(root.get('lo', {}))
            hi = self._rat_to_float(root.get('hi', {}))
            status = root.get('status', 'unknown')
            lines.append(f"-- Root {i+1}: [{lo:.6f}, {hi:.6f}] (status: {status})")

        lines.append("")
        lines.append("-- To verify existence, use:")
        lines.append("-- theorem root_exists : ∃ x ∈ I, f x = 0 := by")
        lines.append("--   interval_root <root_interval>")

        return lines

    def _to_lean_integrate(self) -> list[str]:
        """Generate Lean code for integrate operation."""
        lines = []
        expr_lean = self._expr_to_lean(self.expr_json)
        lo = self.result_json.get('lo', {})
        hi = self.result_json.get('hi', {})
        taylor_depth = self.metadata.get('taylor_depth', 10)

        lines.append(f"-- Expression: {expr_lean}")
        lines.append(f"-- Integral bounds: [{self._rat_to_float(lo):.6f}, {self._rat_to_float(hi):.6f}]")
        lines.append("")
        lines.append(f"-- theorem integral_bound : ∫ x in I, {expr_lean} ∈ bounds := by")
        lines.append(f"--   interval_integrate {taylor_depth}")

        return lines

    def _expr_to_lean(self, expr: dict) -> str:
        """Convert expression JSON to Lean syntax (approximate)."""
        kind = expr.get('kind', '')

        if kind == 'const':
            val = expr.get('val', {})
            n, d = val.get('n', 0), val.get('d', 1)
            if d == 1:
                return str(n)
            return f"({n}/{d})"
        elif kind == 'var':
            idx = expr.get('idx', 0)
            return f"x{idx}" if idx > 0 else "x"
        elif kind == 'add':
            e1 = self._expr_to_lean(expr.get('e1', {}))
            e2 = self._expr_to_lean(expr.get('e2', {}))
            return f"({e1} + {e2})"
        elif kind == 'mul':
            e1 = self._expr_to_lean(expr.get('e1', {}))
            e2 = self._expr_to_lean(expr.get('e2', {}))
            return f"({e1} * {e2})"
        elif kind == 'neg':
            e = self._expr_to_lean(expr.get('e', {}))
            return f"(-{e})"
        elif kind == 'div':
            e1 = self._expr_to_lean(expr.get('e1', {}))
            e2 = self._expr_to_lean(expr.get('e2', {}))
            return f"({e1} / {e2})"
        elif kind == 'pow':
            base = self._expr_to_lean(expr.get('base', {}))
            exp = expr.get('exp', 0)
            return f"({base}^{exp})"
        elif kind in ('sin', 'cos', 'exp', 'log', 'sqrt', 'tan', 'atan', 'inv', 'arsinh', 'atanh', 'sinc', 'erf'):
            e = self._expr_to_lean(expr.get('e', {}))
            return f"Real.{kind} {e}"
        else:
            return f"<{kind}?>"

    def _domain_to_lean(self, domain: list) -> str:
        """Convert domain JSON to Lean syntax."""
        if len(domain) == 1:
            lo = self._rat_to_float(domain[0].get('lo', {}))
            hi = self._rat_to_float(domain[0].get('hi', {}))
            return f"Set.Icc {lo} {hi}"
        else:
            intervals = []
            for i, d in enumerate(domain):
                lo = self._rat_to_float(d.get('lo', {}))
                hi = self._rat_to_float(d.get('hi', {}))
                intervals.append(f"x{i} ∈ [{lo}, {hi}]")
            return " × ".join(intervals)

    def _rat_to_float(self, rat: dict) -> float:
        """Convert rational JSON to float."""
        n = rat.get('n', 0)
        d = rat.get('d', 1)
        return n / d if d != 0 else 0.0

    def __repr__(self) -> str:
        status = "verified" if self.verified else "unverified"
        return f"Certificate({self.operation}, {status}, hash={self.hash()[:8]}...)"

to_lean_tactic()

Generate Lean tactic code that reproduces the verified proof.

Returns a string of Lean code that can be pasted into a Lean file. This provides the "round trip" - Python finds the certificate, then generates Lean code that verifies it.

Example output for find_bounds

theorem bound_check : ∀ x ∈ Set.Icc 0 1, x^2 ≤ 1 := by interval_bound 10

Example output for verify_bound

theorem upper_bound_check : ∀ x ∈ I, f x ≤ 1.5 := by interval_bound 10

Source code in python/leancert/result.py

def to_lean_tactic(self) -> str:
    """
    Generate Lean tactic code that reproduces the verified proof.

    Returns a string of Lean code that can be pasted into a Lean file.
    This provides the "round trip" - Python finds the certificate,
    then generates Lean code that verifies it.

    Example output for find_bounds:
        theorem bound_check : ∀ x ∈ Set.Icc 0 1, x^2 ≤ 1 := by
          interval_bound 10

    Example output for verify_bound:
        theorem upper_bound_check : ∀ x ∈ I, f x ≤ 1.5 := by
          interval_bound 10
    """
    lines = []
    lines.append(f"-- Certificate hash: {self.hash()[:16]}...")
    lines.append(f"-- Generated from: {self.operation}")
    lines.append("")

    if self.operation == 'find_bounds':
        lines.extend(self._to_lean_find_bounds())
    elif self.operation == 'verify_bound':
        lines.extend(self._to_lean_verify_bound())
    elif self.operation == 'find_roots':
        lines.extend(self._to_lean_find_roots())
    elif self.operation == 'integrate':
        lines.extend(self._to_lean_integrate())
    else:
        lines.append(f"-- Unknown operation: {self.operation}")
        lines.append(f"-- Raw result: {self.result_json}")

    return '\n'.join(lines)

save(path)

Save certificate to a JSON file.

Source code in python/leancert/result.py

def save(self, path: str) -> None:
    """Save certificate to a JSON file."""
    with open(path, 'w') as f:
        json.dump(self.to_dict(), f, indent=2)

load(path) classmethod

Load certificate from a JSON file.

Source code in python/leancert/result.py

@classmethod
def load(cls, path: str) -> Certificate:
    """Load certificate from a JSON file."""
    with open(path) as f:
        data = json.load(f)

    return cls(
        operation=data['operation'],
        expr_json=data['expr'],
        domain_json=data['domain'],
        result_json=data['result'],
        verified=data['verified'],
        lean_version=data['lean_version'],
        leancert_version=data['leancert_version'],
        computation_time_ms=data.get('computation_time_ms'),
        metadata=data.get('metadata', {}),
    )

VerifyResult

Returned by verify_bound().

leancert.result.VerifyResult dataclass

Result of bound verification.

Indicates whether a claimed bound was verified.

Access Patterns

result.verified # bool - True if bound verified result.computed_bound # Interval object with actual computed bound result.lo # float lower bound of computed interval result.hi # float upper bound of computed interval result.value # float midpoint of computed interval

Source code in python/leancert/result.py

@dataclass
class VerifyResult:
    """
    Result of bound verification.

    Indicates whether a claimed bound was verified.

    Access Patterns:
        result.verified         # bool - True if bound verified
        result.computed_bound   # Interval object with actual computed bound
        result.lo               # float lower bound of computed interval
        result.hi               # float upper bound of computed interval
        result.value            # float midpoint of computed interval
    """
    verified: bool
    computed_bound: Interval
    certificate: Optional[Certificate] = None

    @property
    def lo(self) -> float:
        """Lower bound of computed interval."""
        return float(self.computed_bound.lo)

    @property
    def hi(self) -> float:
        """Upper bound of computed interval."""
        return float(self.computed_bound.hi)

    @property
    def value(self) -> float:
        """Midpoint of computed interval."""
        return float(self.computed_bound.midpoint())

    def __repr__(self) -> str:
        status = "VERIFIED" if self.verified else "FAILED"
        return f"VerifyResult({status}, computed={self.computed_bound})"

hi property

Upper bound of computed interval.

lo property

Lower bound of computed interval.

value property

Midpoint of computed interval.

Discovery Results (Lean)

The Lean side provides structured result types for discovery operations.

VerifiedGlobalMin

Contains the lower bound, the box where it was found, and the formal proof.

structure VerifiedGlobalMin where
  lowerBound : ℚ
  achievingBox : Box
  proof : ∀ x ∈ domain, f x ≥ lowerBound

VerifiedRoot

Contains an isolating interval for a root and the proof of existence (via sign change/IVT).

structure VerifiedRoot where
  interval : IntervalRat
  proof : ∃ x ∈ interval, f x = 0

VerifiedEquivalence

Contains the certificate that two neural networks produce outputs within a specific tolerance ε.

structure VerifiedEquivalence where
  tolerance : ℚ
  proof : ∀ x ∈ domain, |teacher x - student x| ≤ tolerance