Numerical checks for the Jacobi example

These checks run the actual sweep, stopRelative, and stopAbsolute terms through the Float evaluator in the native binary. Matrix composition reaches the C dot-product implementation, so these are run-time checks, not #guard assertions. The endomorphism inverse check inverseIsIdentity runs here for the same reason; the typing and parametricity checks remain in Examples.

The sweep checks cover 125 finite symmetric matrices with positive, negative, and zero off-diagonals, and equal or unequal diagonals. They check the result, not the formula used to construct the rotation: both off-diagonals must vanish, symmetry must hold, trace and determinant must be preserved, and an already diagonal input must come back unchanged. The tolerance is 1e-12 * max(1, |expected|) for these small test matrices. This is not an error bound for arbitrary floating-point inputs.

structure LambdaS.JacobiChecks.SymmetricInput : Type

The three independent entries of a symmetric two-by-two input.

• a : Float
• b : Float
• d : Float

structure LambdaS.JacobiChecks.MatrixResult : Type

A result with exactly two rows and two columns.

• a : Float
• b : Float
• c : Float
• d : Float

structure LambdaS.JacobiChecks.StopCase : Type

Expected branch decisions are supplied independently of the stopping code.

• name : String
• input : SymmetricInput
• relativeStops : Bool
• absoluteStops : Bool

def LambdaS.JacobiChecks.allChecks : Bool

All numerical Jacobi regressions, plus the endomorphism inverse check from Examples, which composes matrices and so also needs the binary; main exits nonzero on a failure.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.JacobiChecks.report : String

Report failed inputs individually, so a failure can be reproduced.

Equations

• One or more equations did not get rendered due to their size.