Piecewise-linear 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 (piecewise-linear) interpolant of a small dataset.
• 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 lake exe verify -- spline-cert path checks a bundled JSON file and does not require 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): lake exe verify -- spline-cert

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

References:

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

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

Arithmetic used for the optional runtime cross-check.

• exact : Arithmetic
• ieee : Arithmetic

@[instance_reducible]

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

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

@[instance_reducible]

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

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

Parse the command-line arithmetic selector.

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

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

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

Repository-relative path of the Julia certificate producer.

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

Help text for the piecewise-linear certificate command.

def NN.Verification.Splines.PiecewiseLinearCLI.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.