Exact moment block certificate

Generated by scripts/generate_moments.py; all identities below are checked by the Lean kernel with integer arithmetic. No external verifier is trusted.

def PersistentSOS.momentBlock2Stage0 : Fin 11 → Fin 11 → ℤ

Exact integer matrix after 0 fraction-free Schur steps in moment block 2.

Equations

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

def PersistentSOS.momentBlock2Stage1 : Fin 10 → Fin 10 → ℤ

Exact integer matrix after 1 fraction-free Schur steps in moment block 2.

Equations

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

def PersistentSOS.momentBlock2Stage2 : Fin 9 → Fin 9 → ℤ

Exact integer matrix after 2 fraction-free Schur steps in moment block 2.

Equations

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

def PersistentSOS.momentBlock2Stage3 : Fin 8 → Fin 8 → ℤ

Exact integer matrix after 3 fraction-free Schur steps in moment block 2.

Equations

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

def PersistentSOS.momentBlock2Stage4 : Fin 7 → Fin 7 → ℤ

Exact integer matrix after 4 fraction-free Schur steps in moment block 2.

Equations

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

def PersistentSOS.momentBlock2Stage5 : Fin 6 → Fin 6 → ℤ

Exact integer matrix after 5 fraction-free Schur steps in moment block 2.

Equations

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

def PersistentSOS.momentBlock2Stage6 : Fin 5 → Fin 5 → ℤ

Exact integer matrix after 6 fraction-free Schur steps in moment block 2.

Equations

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

def PersistentSOS.momentBlock2Stage7 : Fin 4 → Fin 4 → ℤ

Exact integer matrix after 7 fraction-free Schur steps in moment block 2.

Equations

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

def PersistentSOS.momentBlock2Stage8 : Fin 3 → Fin 3 → ℤ

Exact integer matrix after 8 fraction-free Schur steps in moment block 2.

Equations

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

def PersistentSOS.momentBlock2Stage9 : Fin 2 → Fin 2 → ℤ

Exact integer matrix after 9 fraction-free Schur steps in moment block 2.

Equations

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

def PersistentSOS.momentBlock2Stage10 : Fin 1 → Fin 1 → ℤ

Exact integer matrix after 10 fraction-free Schur steps in moment block 2.

Equations

• PersistentSOS.momentBlock2Stage10 = ![![4230655176739430507011639448708130569138958702359]]

def PersistentSOS.momentBlock2Stage11 : Fin 0 → Fin 0 → ℤ

Exact integer matrix after 11 fraction-free Schur steps in moment block 2.

Equations

• PersistentSOS.momentBlock2Stage11 i = i.elim0

theorem PersistentSOS.momentBlock2Stage10_psd : IsPSD fun (i j : Fin 1) => ↑(momentBlock2Stage10 i j)

theorem PersistentSOS.momentBlock2Stage9_psd : IsPSD fun (i j : Fin 2) => ↑(momentBlock2Stage9 i j)

theorem PersistentSOS.momentBlock2Stage8_psd : IsPSD fun (i j : Fin 3) => ↑(momentBlock2Stage8 i j)

theorem PersistentSOS.momentBlock2Stage7_psd : IsPSD fun (i j : Fin 4) => ↑(momentBlock2Stage7 i j)

theorem PersistentSOS.momentBlock2Stage6_psd : IsPSD fun (i j : Fin 5) => ↑(momentBlock2Stage6 i j)

theorem PersistentSOS.momentBlock2Stage5_psd : IsPSD fun (i j : Fin 6) => ↑(momentBlock2Stage5 i j)

theorem PersistentSOS.momentBlock2Stage4_psd : IsPSD fun (i j : Fin 7) => ↑(momentBlock2Stage4 i j)

theorem PersistentSOS.momentBlock2Stage3_psd : IsPSD fun (i j : Fin 8) => ↑(momentBlock2Stage3 i j)

theorem PersistentSOS.momentBlock2Stage2_psd : IsPSD fun (i j : Fin 9) => ↑(momentBlock2Stage2 i j)

theorem PersistentSOS.momentBlock2Stage1_psd : IsPSD fun (i j : Fin 10) => ↑(momentBlock2Stage1 i j)

theorem PersistentSOS.momentBlock2Stage0_psd : IsPSD fun (i j : Fin 11) => ↑(momentBlock2Stage0 i j)