Explicit rational moment data

Every monomial occurrence uses one base-five exponent key. All degree-four moments are derived from the retained rational certificate. The finite Gram identities and coverage are proved below by kernel reduction.

def PersistentSOS.momentNumerator (k : ℕ) : ℤ

Integer numerator table; unspecified keys have value zero.

Equations

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

def PersistentSOS.blockSize : Fin 8 → ℕ

Dimensions of the eight exact moment-matrix blocks.

Equations

• PersistentSOS.blockSize 0 = 28
• PersistentSOS.blockSize 1 = 11
• PersistentSOS.blockSize 2 = 11
• PersistentSOS.blockSize 3 = 16
• PersistentSOS.blockSize 4 = 11
• PersistentSOS.blockSize 5 = 16
• PersistentSOS.blockSize 6 = 16
• PersistentSOS.blockSize 7 = 11

def PersistentSOS.basisPair (c : Fin 8) : Fin (blockSize c) → Fin 15 × Fin 15

Pairs of padded variable indices forming each quadratic monomial block.

Equations

• One or more equations did not get rendered due to their size.
• PersistentSOS.basisPair 1 = ![(0, 2), (1, 2), (2, 6), (2, 7), (2, 8), (3, 9), (3, 14), (4, 10), (4, 13), (5, 11), (5, 12)]
• PersistentSOS.basisPair 2 = ![(0, 3), (1, 3), (2, 9), (2, 14), (3, 6), (3, 7), (3, 8), (4, 11), (4, 12), (5, 10), (5, 13)]
• PersistentSOS.basisPair 3 = ![(0, 9), (0, 14), (1, 9), (1, 14), (2, 3), (4, 5), (6, 9), (6, 14), (7, 9), (7, 14), (8, 9), (8, 14), (10, 11), (10, 12), (11, 13), (12, 13)]
• PersistentSOS.basisPair 4 = ![(0, 4), (1, 4), (2, 10), (2, 13), (3, 11), (3, 12), (4, 6), (4, 7), (4, 8), (5, 9), (5, 14)]
• PersistentSOS.basisPair 5 = ![(0, 10), (0, 13), (1, 10), (1, 13), (2, 4), (3, 5), (6, 10), (6, 13), (7, 10), (7, 13), (8, 10), (8, 13), (9, 11), (9, 12), (11, 14), (12, 14)]
• PersistentSOS.basisPair 6 = ![(0, 11), (0, 12), (1, 11), (1, 12), (2, 5), (3, 4), (6, 11), (6, 12), (7, 11), (7, 12), (8, 11), (8, 12), (9, 10), (9, 13), (10, 14), (13, 14)]
• PersistentSOS.basisPair 7 = ![(0, 5), (1, 5), (2, 11), (2, 12), (3, 10), (3, 13), (4, 9), (4, 14), (5, 6), (5, 7), (5, 8)]

def PersistentSOS.blockNumerator (c : Fin 8) : Fin (blockSize c) → Fin (blockSize c) → ℤ

Integer moment matrices, with the common denominator kept separate.

Equations

• PersistentSOS.blockNumerator 0 = PersistentSOS.momentBlockFull0Stage0
• PersistentSOS.blockNumerator 1 = PersistentSOS.momentBlock1Stage0
• PersistentSOS.blockNumerator 2 = PersistentSOS.momentBlock2Stage0
• PersistentSOS.blockNumerator 3 = PersistentSOS.momentBlock3Stage0
• PersistentSOS.blockNumerator 4 = PersistentSOS.momentBlock4Stage0
• PersistentSOS.blockNumerator 5 = PersistentSOS.momentBlock5Stage0
• PersistentSOS.blockNumerator 6 = PersistentSOS.momentBlock6Stage0
• PersistentSOS.blockNumerator 7 = PersistentSOS.momentBlock7Stage0

theorem PersistentSOS.blockNumerator_psd (c : Fin 8) : IsPSD fun (i j : Fin (blockSize c)) => ↑(blockNumerator c i j)

noncomputable def PersistentSOS.variableExponent (i : Fin 15) : Exponent

A zero index pads a monomial of degree less than two.

Equations

• PersistentSOS.variableExponent i = if h : i = 0 then 0 else Finsupp.single ⟨↑i - 1, ⋯⟩ 1

def PersistentSOS.variableKey (i : Fin 15) : ℕ

Base-five key of a variable, with zero representing the constant monomial.

Equations

• PersistentSOS.variableKey i = if i = 0 then 0 else 5 ^ (↑i - 1)

noncomputable def PersistentSOS.momentBasis (b : (c : Fin 8) × Fin (blockSize c)) : Exponent

Exponent vector of a quadratic monomial in the complete block basis.

Equations

• PersistentSOS.momentBasis b = PersistentSOS.variableExponent (PersistentSOS.basisPair b.fst b.snd).1 + PersistentSOS.variableExponent (PersistentSOS.basisPair b.fst b.snd).2

def PersistentSOS.basisKey (c : Fin 8) (i : Fin (blockSize c)) : ℕ

Moment-table key of a quadratic basis monomial.

Equations

• PersistentSOS.basisKey c i = PersistentSOS.variableKey (PersistentSOS.basisPair c i).1 + PersistentSOS.variableKey (PersistentSOS.basisPair c i).2

@[simp]

theorem PersistentSOS.exponentKey_variableExponent (i : Fin 15) : exponentKey (variableExponent i) = variableKey i

@[simp]

theorem PersistentSOS.exponentKey_momentBasis (b : (c : Fin 8) × Fin (blockSize c)) : exponentKey (momentBasis b) = basisKey b.fst b.snd

theorem PersistentSOS.moment_block_0 (i j : Fin (blockSize 0)) : momentNumerator (basisKey 0 i + basisKey 0 j) = blockNumerator 0 i j

theorem PersistentSOS.moment_block_1 (i j : Fin (blockSize 1)) : momentNumerator (basisKey 1 i + basisKey 1 j) = blockNumerator 1 i j

theorem PersistentSOS.moment_block_2 (i j : Fin (blockSize 2)) : momentNumerator (basisKey 2 i + basisKey 2 j) = blockNumerator 2 i j

theorem PersistentSOS.moment_block_3 (i j : Fin (blockSize 3)) : momentNumerator (basisKey 3 i + basisKey 3 j) = blockNumerator 3 i j

theorem PersistentSOS.moment_block_4 (i j : Fin (blockSize 4)) : momentNumerator (basisKey 4 i + basisKey 4 j) = blockNumerator 4 i j

theorem PersistentSOS.moment_block_5 (i j : Fin (blockSize 5)) : momentNumerator (basisKey 5 i + basisKey 5 j) = blockNumerator 5 i j

theorem PersistentSOS.moment_block_6 (i j : Fin (blockSize 6)) : momentNumerator (basisKey 6 i + basisKey 6 j) = blockNumerator 6 i j

theorem PersistentSOS.moment_block_7 (i j : Fin (blockSize 7)) : momentNumerator (basisKey 7 i + basisKey 7 j) = blockNumerator 7 i j

theorem PersistentSOS.moment_block (c : Fin 8) (i j : Fin (blockSize c)) : momentNumerator (basisKey c i + basisKey c j) = blockNumerator c i j

theorem PersistentSOS.moment_cross_0 (d : Fin 8) : 0 ≠ d → ∀ (i : Fin (blockSize 0)) (j : Fin (blockSize d)), momentNumerator (basisKey 0 i + basisKey d j) = 0

theorem PersistentSOS.moment_cross_1 (d : Fin 8) : 1 ≠ d → ∀ (i : Fin (blockSize 1)) (j : Fin (blockSize d)), momentNumerator (basisKey 1 i + basisKey d j) = 0

theorem PersistentSOS.moment_cross_2 (d : Fin 8) : 2 ≠ d → ∀ (i : Fin (blockSize 2)) (j : Fin (blockSize d)), momentNumerator (basisKey 2 i + basisKey d j) = 0

theorem PersistentSOS.moment_cross_3 (d : Fin 8) : 3 ≠ d → ∀ (i : Fin (blockSize 3)) (j : Fin (blockSize d)), momentNumerator (basisKey 3 i + basisKey d j) = 0

theorem PersistentSOS.moment_cross_4 (d : Fin 8) : 4 ≠ d → ∀ (i : Fin (blockSize 4)) (j : Fin (blockSize d)), momentNumerator (basisKey 4 i + basisKey d j) = 0

theorem PersistentSOS.moment_cross_5 (d : Fin 8) : 5 ≠ d → ∀ (i : Fin (blockSize 5)) (j : Fin (blockSize d)), momentNumerator (basisKey 5 i + basisKey d j) = 0

theorem PersistentSOS.moment_cross_6 (d : Fin 8) : 6 ≠ d → ∀ (i : Fin (blockSize 6)) (j : Fin (blockSize d)), momentNumerator (basisKey 6 i + basisKey d j) = 0

theorem PersistentSOS.moment_cross_7 (d : Fin 8) : 7 ≠ d → ∀ (i : Fin (blockSize 7)) (j : Fin (blockSize d)), momentNumerator (basisKey 7 i + basisKey d j) = 0

theorem PersistentSOS.moment_cross (c d : Fin 8) : c ≠ d → ∀ (i : Fin (blockSize c)) (j : Fin (blockSize d)), momentNumerator (basisKey c i + basisKey d j) = 0

theorem PersistentSOS.moment_quadratic_numerator_sum : ∑ i : Fin 14, momentNumerator (2 * 5 ^ ↑i) = 1000000000

theorem PersistentSOS.moment_quartic_numerator_sum : ∑ i : Fin 14, ∑ j : Fin 14, momentNumerator (2 * 5 ^ ↑i + 2 * 5 ^ ↑j) = 1000000000