`BookProof.SmHamiltonian.smHamiltonian_quadForm_nonneg` (P : SmParams) (x : polyGaussCore (d := 163)) : 0 ≤ quadForm (smHamiltonian P) x

Initializing...

`BookProof.SmHamiltonian.smHamiltonian_quadForm_nonneg` (P : SmParams) (x : polyGaussCore (d := 163)) : 0 ≤ quadForm (smHamiltonian P) x · Prove2Me