Piecewise-polynomial spline certificate CLI

The workflow follows the “external producer, Lean checker” pattern:

• Julia acts as an untrusted producer that emits a small JSON certificate describing a piecewise-polynomial interpolant of a small dataset; the bundled example is piecewise linear.
• Lean parses and checks the certificate exactly over Rat using NN.Verification.Splines.PiecewisePolyCert.

This is dependency-free:

• the Julia script uses only Julia Base (no packages),
• the default scripts/lake.sh exe verify -- spline-cert path checks a bundled JSON file, without requiring Julia,
• passing --regen calls Julia to regenerate the JSON and checks the output.

Run via the unified verification CLI:

• Check bundled cert (no Julia required): scripts/lake.sh exe verify -- spline-cert

• Regenerate by calling Julia (requires julia on PATH or TORCHLEAN_JULIA set): scripts/lake.sh exe verify -- spline-cert --regen

References:

• “untrusted producer, trusted checker” workflow: see bundled certificates and scripts/verification/* producers.

inductive NN.Verification.Splines.PiecewisePolyCLI.Arithmetic : Type

Arithmetic used for the optional runtime cross-check.

• exact : Arithmetic
• ieee : Arithmetic

@[instance_reducible]

instance NN.Verification.Splines.PiecewisePolyCLI.instDecidableEqArithmetic : DecidableEq Arithmetic

def NN.Verification.Splines.PiecewisePolyCLI.instReprArithmetic.repr : Arithmetic → ℕ → Std.Format

@[instance_reducible]

instance NN.Verification.Splines.PiecewisePolyCLI.instReprArithmetic : Repr Arithmetic

def NN.Verification.Splines.PiecewisePolyCLI.parseArithmetic (value : String) : Except String Arithmetic

Parse the command-line arithmetic selector.

def NN.Verification.Splines.PiecewisePolyCLI.defaultCertPath : String

Repository-relative path of the bundled piecewise-linear certificate.

def NN.Verification.Splines.PiecewisePolyCLI.defaultJuliaScript : String

Repository-relative path of the Julia certificate producer.

def NN.Verification.Splines.PiecewisePolyCLI.usage : String

Help text for the piecewise-polynomial certificate command.

def NN.Verification.Splines.PiecewisePolyCLI.main (args : List String) : IO Unit

Entry point used by the unified verification CLI.

By default, checks the bundled JSON cert on disk. With --regen, calls Julia and checks its stdout JSON payload instead.