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.momentBlock7Stage0 : Fin 11 → Fin 11 → ℤ

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• PersistentSOS.momentBlock7Stage10 = ![![18923129851434570969679744770567303891184915294505751]]

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

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

Equations

• PersistentSOS.momentBlock7Stage11 i = i.elim0

theorem PersistentSOS.momentBlock7Stage10_psd : IsPSD fun (i j : Fin 1) => ↑(momentBlock7Stage10 i j)

theorem PersistentSOS.momentBlock7Stage9_psd : IsPSD fun (i j : Fin 2) => ↑(momentBlock7Stage9 i j)

theorem PersistentSOS.momentBlock7Stage8_psd : IsPSD fun (i j : Fin 3) => ↑(momentBlock7Stage8 i j)

theorem PersistentSOS.momentBlock7Stage7_psd : IsPSD fun (i j : Fin 4) => ↑(momentBlock7Stage7 i j)

theorem PersistentSOS.momentBlock7Stage6_psd : IsPSD fun (i j : Fin 5) => ↑(momentBlock7Stage6 i j)

theorem PersistentSOS.momentBlock7Stage5_psd : IsPSD fun (i j : Fin 6) => ↑(momentBlock7Stage5 i j)

theorem PersistentSOS.momentBlock7Stage4_psd : IsPSD fun (i j : Fin 7) => ↑(momentBlock7Stage4 i j)

theorem PersistentSOS.momentBlock7Stage3_psd : IsPSD fun (i j : Fin 8) => ↑(momentBlock7Stage3 i j)

theorem PersistentSOS.momentBlock7Stage2_psd : IsPSD fun (i j : Fin 9) => ↑(momentBlock7Stage2 i j)

theorem PersistentSOS.momentBlock7Stage1_psd : IsPSD fun (i j : Fin 10) => ↑(momentBlock7Stage1 i j)

theorem PersistentSOS.momentBlock7Stage0_psd : IsPSD fun (i j : Fin 11) => ↑(momentBlock7Stage0 i j)