Shape-checked decoding of exact rational parameters

def NN.Verification.Cert.RationalJson.decodeVector (n : ℕ) (j : Lean.Json) : Except String (TorchLean.Tensor ℚ [n])

Decode integer or fraction strings without floating-point conversion.

def NN.Verification.Cert.RationalJson.decodeLinear (n : ℕ) (j : Lean.Json) : Except String ((m : ℕ) × Spec.LinearSpec ℚ n m)

Decode a row-major matrix and bias, checking both dimensions.