Eig3x3.Certificates — runtime instance checking

Runtime error validation of decomposition processes. Since this package intentionally proves no theorems about Float, these certificates are the trust mechanism for downstream computation assurances.

Given any claimed decomposition of A, certify computes per-instance evidence:

• residual — how badly each claimed eigenpair violates Av = λv
• orthonormality — how far the eigenvectors stray from perpendicular unit vectors
• reconstruction — how closely QΛQᵀ reproduces the original A

Deliberately uses only mulVec, dot, and subtraction — no eigenvalue machinery — so it is trustworthy independently of the solver's complexity.

Visibility

Exposes Certificates and certify. The component metrics are package-private.

structure Eig3x3.Certificates : Type

All three certificates for a decomposition of A, bundled.

• maxResidual : Float

  max ‖Avᵢ − λᵢvᵢ‖∞ over the three eigenpairs.

• orthogonality : Float

  max |cᵢ·cⱼ − δᵢⱼ| over all column pairs of Q.

• reconstruction : Float

  max |entry| of QΛQᵀ − A.

def Eig3x3.instReprCertificates.repr : Certificates → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Eig3x3.instReprCertificates : Repr Certificates

Equations

• Eig3x3.instReprCertificates = { reprPrec := Eig3x3.instReprCertificates.repr }

def Eig3x3.certify (A : SymmMat3) (d : Decomposition) : Certificates

Compute all three certificates for a claimed decomposition of A. Expect ≈ 1e-16 · ‖A‖ or smaller on outputs of eigendecomp.

Equations

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