Piecewise polynomial certificates

This module implements a Lean checker for one-dimensional piecewise-polynomial certificates.

Why this exists:

• In TorchLean’s “external producer, Lean checker” workflow, an external tool (Julia, Python, ...) can fit or search for a piecewise-polynomial surrogate and export a compact JSON artifact.
• Lean then checks basic algebraic consistency conditions on that artifact.

Our checker is conservative: it checks exact equalities over Rat with no floating-point tolerance.

Optionally, you can also run an executable float32 cross-check via checkJsonIEEE32ExecExact: if every rational in the certificate is exactly representable as a finite IEEE-754 binary32 (IEEE32Exec), we re-run the endpoint equalities under IEEE32Exec arithmetic. This is useful when the producer is actually operating in float32 and you want to confirm the certificate’s equalities hold under the same semantics.

What is checked in format = "piecewise_poly_v0":

• xs is strictly increasing,
• ys has the same length as xs,
• there is one piece per interval [xs[i], xs[i+1]],
• each piece’s (lo, hi) matches the corresponding interval endpoints,
• the local-coordinate polynomial interpolates the endpoints exactly: p_i(xs[i]) = ys[i] and p_i(xs[i+1]) = ys[i+1].

This certificate format focuses on endpoint and piece consistency. It does not claim global range bounds for higher-degree polynomials; those require additional machinery such as Bernstein bounds or interval arithmetic with derivative-based splitting.

References (background):

• de Boor, A Practical Guide to Splines (1978).
• Certificate checking pattern: export an artifact, then check it in a small Lean checker core.

Utilities: exact rationals in JSON

def NN.Verification.Splines.PiecewisePolyCert.parseRatString (s : String) : Except String ℚ

Parse a rational in the format emitted by TorchLean’s Arb helpers:

• integer: "5", "-3"
• fraction: "5/2", "-7/10"

We avoid JSON numbers here because they are stored as Scientific and are not guaranteed to round-trip exactly for large integers.

def NN.Verification.Splines.PiecewisePolyCert.parseRat (ctx : String) (j : Lean.Json) : IO ℚ

Parse a Rat from a JSON string field with context.

Certificate schema

structure NN.Verification.Splines.PiecewisePolyCert.PolynomialPiece : Type

One polynomial segment on an interval [lo, hi], using local coordinate t = x - lo.

• lo : ℚ
• hi : ℚ
• coeffs : Array ℚ

@[implicit_reducible]

instance NN.Verification.Splines.PiecewisePolyCert.instReprPolynomialPiece : Repr PolynomialPiece

def NN.Verification.Splines.PiecewisePolyCert.instReprPolynomialPiece.repr : PolynomialPiece → ℕ → Std.Format

def NN.Verification.Splines.PiecewisePolyCert.instInhabitedPolynomialPiece.default : PolynomialPiece

@[implicit_reducible]

instance NN.Verification.Splines.PiecewisePolyCert.instInhabitedPolynomialPiece : Inhabited PolynomialPiece

structure NN.Verification.Splines.PiecewisePolyCert.PiecewisePolyCertificate : Type

Parsed certificate payload for piecewise_poly_v0.

degree is redundant (it should equal coeffs.size - 1), but it is useful for fast validation.

• degree : ℕ

  Polynomial degree d (so each piece has d+1 coefficients).

• n : ℕ

  Number of knot points.

• xs : TensorArray.Tensor ℚ [self.n]

  Knot x-coordinates as a length-n vector.

• ys : TensorArray.Tensor ℚ [self.n]

  Knot y-values as a length-n vector.

• pieces : Array PolynomialPiece

  One piece per interval [xs[i], xs[i+1]].

Polynomial evaluation

def NN.Verification.Splines.PiecewisePolyCert.evalPolyHorner {α : Type} [Zero α] [Add α] [Mul α] (coeffs : Array α) (t : α) : α

Evaluate a polynomial in local coordinate t using Horner’s rule.

Given coefficients [a₀, a₁, …, a_d] representing:

a₀ + a₁ t + a₂ t^2 + … + a_d t^d.

This helper is generic so we can reuse it for Rat (exact checking) and for IEEE32Exec (executable float32 semantics).

Parsing

def NN.Verification.Splines.PiecewisePolyCert.Internal.parseRatArray (ctx : String) (j : Lean.Json) : IO (Array ℚ)

Parse an array of rational strings, attaching ctx to any error message.

def NN.Verification.Splines.PiecewisePolyCert.Internal.parsePolynomialPiece (ctx : String) (j : Lean.Json) : IO PolynomialPiece

Parse one polynomial segment from the certificate JSON object.

def NN.Verification.Splines.PiecewisePolyCert.parsePiecewisePolyCertificate (j : Lean.Json) : IO PiecewisePolyCertificate

Parse the piecewise_poly_v0 JSON payload into a structured certificate.

Checking

def NN.Verification.Splines.PiecewisePolyCert.checkCertificateRat (cert : PiecewisePolyCertificate) : IO Unit

Check a piecewise-polynomial certificate exactly over Rat.

This is the smallest checker core for this format: it uses exact rational arithmetic (no tolerances), so a passing check means the certificate’s equalities are literally true as stated.

def NN.Verification.Splines.PiecewisePolyCert.checkJson (j : Lean.Json) : IO Unit

Check a piecewise_poly_v0 certificate payload.

Raises IO.userError on the first mismatch; prints a short success message otherwise.

def NN.Verification.Splines.PiecewisePolyCert.ratToIEEE32ExecExact (ctx : String) (q : ℚ) : IO TorchLean.Floats.IEEE754.IEEE32Exec

Attempt to convert a rational to an exact finite IEEE32Exec value.

This is used for optional “float32 semantics” checking: we only accept values that are exactly representable on the binary32 grid, so equality checks are meaningful at the executable IEEE level.

Implementation note:

• We reuse TorchLean’s existing Rat → IEEE32Exec outward-rounding helpers (roundRatQDown/roundRatQUp), and we accept only when the lower/upper rounding coincide.

def NN.Verification.Splines.PiecewisePolyCert.checkCertificateIEEE32ExecExact (cert : PiecewisePolyCertificate) : IO Unit

Check the same endpoint equalities as checkCertificateRat, but under IEEE32Exec arithmetic.

This is an additional (optional) check that answers: “if we interpret the certificate data as binary32 values and run the polynomial evaluation with executable IEEE-754 ops, do we still hit the claimed endpoints?”

The check is deliberately strict:

• every rational in the cert must be exactly representable as a finite IEEE32Exec,
• comparisons use IEEE-style BEq (so +0 == -0, and NaNs never compare equal).

def NN.Verification.Splines.PiecewisePolyCert.checkJsonIEEE32ExecExact (j : Lean.Json) : IO Unit

Check a piecewise-polynomial certificate stored as JSON, including IEEE32Exec semantics.

def NN.Verification.Splines.PiecewisePolyCert.checkFile (path : String) : IO Unit

Check a piecewise-polynomial certificate stored as a JSON file.