Julia spline certificate: external producer + Lean checker

This file is the runnable entry point for 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 intentionally small and 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 NN/Examples/Verification/* (bundled certs) and scripts/verification/* (producers).

def NN.Examples.Verification.Splines.PiecewiseLinearVerify.defaultCertPath : String

def NN.Examples.Verification.Splines.PiecewiseLinearVerify.defaultJuliaScript : String

def NN.Examples.Verification.Splines.PiecewiseLinearVerify.usage : String

def NN.Examples.Verification.Splines.PiecewiseLinearVerify.getOptArg? (optPrefix : String) (args : List String) : Option String

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