Background
The current certificate format and verifier use rational coefficients throughout (CMvPolynomial n ℚ). This is sound and easy to check, but it means goals whose only SOS witnesses use algebraic coefficients, such as coefficients involving √2, are out of scope.
Desired outcome
Investigate and implement a certificate path for algebraic-extension coefficients, or document a principled alternative if this should remain out of scope.
Notes
This likely touches certificate representation, verifier soundness lemmas, search/rounding, and user-facing witness printing. It should remain kernel-checkable and should not make successful proofs depend on trusting CSDP.
Background
The current certificate format and verifier use rational coefficients throughout (
CMvPolynomial n ℚ). This is sound and easy to check, but it means goals whose only SOS witnesses use algebraic coefficients, such as coefficients involving√2, are out of scope.Desired outcome
Investigate and implement a certificate path for algebraic-extension coefficients, or document a principled alternative if this should remain out of scope.
Notes
This likely touches certificate representation, verifier soundness lemmas, search/rounding, and user-facing witness printing. It should remain kernel-checkable and should not make successful proofs depend on trusting CSDP.