Auxiliary exchange matrices and low-degree polynomial replacement rows

Given integer parameters Q and r, let AuxLabel Q r = (Fin Q → Fin r) × (Fin Q → Fin r) be the complete auxiliary label array of cardinality D = r ^ (2 * Q), with elements written u = (u.1, u.2).

This module constructs the auxiliary exchange matrix M0, the {0, 1, -1}-valued measurement matrix measurementMatrix (C^B), the mismatch-annihilating polynomials mismatchAnnihilator (φ_{u,y}(T)), and the low-degree auxiliary replacement rows auxReplacementRow (P⃗_u(T)) from Sections 4.1–4.3 (pp. 26–30) and the common-denominator clearing of Section 4.6 (p. 33) of the manuscript The Exponential Time Hypothesis is False (openai/math@7ef5c0cc):

1. Coordinate-pair swap operators and {0, 1, -1}-eigenbasis (Lemma 4.1, pp. 27–28):

   • For s : Fin Q, slotSwap s exchanges u.1 s and u.2 s, with permutation matrix slotSwapMatrix Q r K s (Π_s); fullSwap exchanges u.1 and u.2 across all slots, with permutation matrix fullSwapMatrix Q r K (V_0 = ∏_s Π_s).
   • twoW0 Q r K = ∑ s : Fin Q, (1 - slotSwapMatrix Q r K s) and W0 Q r = (1 / 2 : ℚ) • twoW0 Q r ℚ.
   • For an interval I = Finset.Ico A₀ (A₀ + R), fI A₀ R : ℚ[X] is the degree-(≤ R - 1) polynomial interpolating (-1)^k on k ∈ I, and M0 Q r A₀ R is V_0 f_I(W_0).
   • The tensor-product vectors eigenvec K β (ψ_β, indexed by β : AuxLabel Q r) have entries in {0, 1, -1}, form a pairwise orthogonal basis of AuxLabel Q r → ℚ, and are simultaneous eigenvectors of slotSwapMatrix, fullSwapMatrix, W0, and M0, with M0-eigenvalue 1 whenever antisymCount β ∈ Finset.Ico A₀ (A₀ + R).
   • Consequently, if a vector ξ : AuxLabel Q r → ℚ lies in the kernel of measurementMatrix (the rows eigenvec ℚ β with antisymCount β ∉ Finset.Ico A₀ (A₀ + R)), then (M0 Q r A₀ R).mulVec ξ = ξ.

2. Mismatch support bound (Lemma 4.2, pp. 28–29):

   • Every factor twoW0 Q r ℚ - c • 1 alters the first component z.1 in at most one slot s : Fin Q. Since fI A₀ R is a sum of products of at most R - 1 such factors and fullSwapMatrix swaps u.1 with u.2, any nonzero entry M0 Q r A₀ R u y ≠ 0 satisfies #(mismatchSet u y) ≤ R - 1, where mismatchSet u y = {s : Fin Q | y.1 s ≠ u.2 s}.

3. Auxiliary polynomial replacement rows (Lemma 4.3, pp. 29–30):

   • With nodePoint s = (s.1 : ℚ) + 1 and mismatchAnnihilator u y = ∏ s ∈ mismatchSet u y, (1 - C (nodePoint s)⁻¹ * X), the row auxReplacementRow Q r A₀ R u y has degree at most R - 1, evaluates at T = 0 to δ_u, and at T = nodePoint s depends only on ζ restricted to auxGroup s (u.2 s) = {y | y.1 s = u.2 s} and (measurementMatrix Q r A₀ R ℚ).mulVec ζ.
   • In particular, if g ≠ u.2 s and ξ is supported on auxGroup s g with (measurementMatrix Q r A₀ R ℚ).mulVec ξ = 0, then evalAuxReplacementRow Q r A₀ R u (nodePoint s) ξ = 0.

4. Common denominator clearing (Lemma 4.6, p. 33):

   • With commonDenom Q R = (R - 1).factorial * Q.factorial, scaling auxReplacementRow Q r A₀ R u y by commonDenom Q R yields the explicit integer polynomial auxReplacementRowScaledInt Q r A₀ R u y : ℤ[X].

Main definitions

• Cslib.LinearAlgebra.AuxLabel: auxiliary coordinate space (Fin Q → Fin r) × (Fin Q → Fin r).
• Cslib.LinearAlgebra.subsetSwap, Cslib.LinearAlgebra.slotSwap, Cslib.LinearAlgebra.fullSwap: coordinate-pair swap involutions.
• Cslib.LinearAlgebra.slotSwapMatrix, Cslib.LinearAlgebra.fullSwapMatrix, Cslib.LinearAlgebra.twoW0, Cslib.LinearAlgebra.W0: swap permutation matrices and W₀.
• Cslib.LinearAlgebra.fI, Cslib.LinearAlgebra.M0: parity interpolant on I and matrix M₀.
• Cslib.LinearAlgebra.eigenvecInt, Cslib.LinearAlgebra.eigenvec, Cslib.LinearAlgebra.measurementIndices, Cslib.LinearAlgebra.measurementMatrix: the {0, 1, -1}-valued orthogonal eigenbasis and measurement matrix C^B.
• Cslib.LinearAlgebra.mismatchSet, Cslib.LinearAlgebra.mismatchAnnihilator, Cslib.LinearAlgebra.auxReplacementRow, Cslib.LinearAlgebra.evalAuxReplacementRow: mismatch set E_{u,y}, annihilator polynomial φ_{u,y}(T), and replacement row P⃗_u(T).
• Cslib.LinearAlgebra.commonDenom, Cslib.LinearAlgebra.auxReplacementRowScaledInt: common denominator d_den = (R - 1)! Q! and cleared integer replacement rows.

Main results

• Cslib.LinearAlgebra.M0_mulVec_eq_self_of_measurementMatrix_mulVec_eq_zero: Lemma 4.1 kernel invariance.
• Cslib.LinearAlgebra.card_mismatchSet_le_of_M0_ne_zero: Lemma 4.2 mismatch support bound.
• Cslib.LinearAlgebra.natDegree_auxReplacementRow_le, Cslib.LinearAlgebra.evalAuxReplacementRow_zero, Cslib.LinearAlgebra.evalAuxReplacementRow_nodePoint_eq_zero_of_kernel, Cslib.LinearAlgebra.evalAuxReplacementRow_nodePoint_eq_of_eq_on_auxGroup: Lemma 4.3 replacement row properties.
• Cslib.LinearAlgebra.map_auxReplacementRowScaledInt: Lemma 4.6 common-denominator clearing.

References

• [OAI26c]

1. Auxiliary coordinate space and coordinate-pair swap operators

@[reducible, inline]

abbrev Cslib.LinearAlgebra.AuxLabel (Q r : ℕ) : Type

The auxiliary coordinate space B = ([r]^Q)² of pairs of length-Q sequences in Fin r.

theorem Cslib.LinearAlgebra.card_auxLabel (Q r : ℕ) : Fintype.card (AuxLabel Q r) = r ^ (2 * Q)

The cardinality of AuxLabel Q r is D = r ^ (2 * Q).

def Cslib.LinearAlgebra.subsetSwap {Q r : ℕ} (J : Finset (Fin Q)) (u : AuxLabel Q r) : AuxLabel Q r

Swap u.1 s and u.2 s at all coordinates s ∈ J, leaving s ∉ J unchanged.

def Cslib.LinearAlgebra.slotSwap {Q r : ℕ} (s : Fin Q) (u : AuxLabel Q r) : AuxLabel Q r

Swap u.1 s and u.2 s at a single slot s : Fin Q (ϑ_s in Section 4.2).

def Cslib.LinearAlgebra.fullSwap {Q r : ℕ} (u : AuxLabel Q r) : AuxLabel Q r

Swap the complete sequences u.1 and u.2 (u ↦ ū).

@[simp]

theorem Cslib.LinearAlgebra.subsetSwap_empty {Q r : ℕ} (u : AuxLabel Q r) : subsetSwap ∅ u = u

theorem Cslib.LinearAlgebra.subsetSwap_subsetSwap {Q r : ℕ} (J₁ J₂ : Finset (Fin Q)) (u : AuxLabel Q r) : subsetSwap J₁ (subsetSwap J₂ u) = subsetSwap (symmDiff J₁ J₂) u

@[simp]

theorem Cslib.LinearAlgebra.subsetSwap_self {Q r : ℕ} (J : Finset (Fin Q)) (u : AuxLabel Q r) : subsetSwap J (subsetSwap J u) = u

@[simp]

theorem Cslib.LinearAlgebra.slotSwap_self {Q r : ℕ} (s : Fin Q) (u : AuxLabel Q r) : slotSwap s (slotSwap s u) = u

@[simp]

theorem Cslib.LinearAlgebra.fullSwap_fst {Q r : ℕ} (u : AuxLabel Q r) : (fullSwap u).1 = u.2

@[simp]

theorem Cslib.LinearAlgebra.fullSwap_snd {Q r : ℕ} (u : AuxLabel Q r) : (fullSwap u).2 = u.1

@[simp]

theorem Cslib.LinearAlgebra.fullSwap_self {Q r : ℕ} (u : AuxLabel Q r) : fullSwap (fullSwap u) = u

def Cslib.LinearAlgebra.subsetSwapMatrix (Q r : ℕ) (K : Type u_1) [CommRing K] (J : Finset (Fin Q)) : Matrix (AuxLabel Q r) (AuxLabel Q r) K

Permutation matrix on AuxLabel Q r associated to subsetSwap J.

def Cslib.LinearAlgebra.slotSwapMatrix (Q r : ℕ) (K : Type u_1) [CommRing K] (s : Fin Q) : Matrix (AuxLabel Q r) (AuxLabel Q r) K

The single-slot exchange matrix Π_s on AuxLabel Q r.

def Cslib.LinearAlgebra.fullSwapMatrix (Q r : ℕ) (K : Type u_1) [CommRing K] : Matrix (AuxLabel Q r) (AuxLabel Q r) K

The full-swap permutation matrix V_0 on AuxLabel Q r.

@[simp]

theorem Cslib.LinearAlgebra.subsetSwapMatrix_empty (Q r : ℕ) (K : Type u_1) [CommRing K] : subsetSwapMatrix Q r K ∅ = 1

@[simp]

theorem Cslib.LinearAlgebra.subsetSwapMatrix_mulVec (Q r : ℕ) (K : Type u_1) [CommRing K] (J : Finset (Fin Q)) (ζ : AuxLabel Q r → K) (u : AuxLabel Q r) : (subsetSwapMatrix Q r K J).mulVec ζ u = ζ (subsetSwap J u)

@[simp]

theorem Cslib.LinearAlgebra.slotSwapMatrix_mulVec (Q r : ℕ) (K : Type u_1) [CommRing K] (s : Fin Q) (ζ : AuxLabel Q r → K) (u : AuxLabel Q r) : (slotSwapMatrix Q r K s).mulVec ζ u = ζ (slotSwap s u)

@[simp]

theorem Cslib.LinearAlgebra.fullSwapMatrix_mulVec (Q r : ℕ) (K : Type u_1) [CommRing K] (ζ : AuxLabel Q r → K) (u : AuxLabel Q r) : (fullSwapMatrix Q r K).mulVec ζ u = ζ (fullSwap u)

theorem Cslib.LinearAlgebra.subsetSwapMatrix_mul (Q r : ℕ) (K : Type u_1) [CommRing K] (J₁ J₂ : Finset (Fin Q)) : subsetSwapMatrix Q r K J₁ * subsetSwapMatrix Q r K J₂ = subsetSwapMatrix Q r K (symmDiff J₁ J₂)

@[simp]

theorem Cslib.LinearAlgebra.subsetSwapMatrix_mul_self (Q r : ℕ) (K : Type u_1) [CommRing K] (J : Finset (Fin Q)) : subsetSwapMatrix Q r K J * subsetSwapMatrix Q r K J = 1

@[simp]

theorem Cslib.LinearAlgebra.slotSwapMatrix_mul_self (Q r : ℕ) (K : Type u_1) [CommRing K] (s : Fin Q) : slotSwapMatrix Q r K s * slotSwapMatrix Q r K s = 1

theorem Cslib.LinearAlgebra.slotSwapMatrix_comm (Q r : ℕ) (K : Type u_1) [CommRing K] (s t : Fin Q) : slotSwapMatrix Q r K s * slotSwapMatrix Q r K t = slotSwapMatrix Q r K t * slotSwapMatrix Q r K s

theorem Cslib.LinearAlgebra.fullSwapMatrix_mul_subsetSwapMatrix (Q r : ℕ) (K : Type u_1) [CommRing K] (J : Finset (Fin Q)) : fullSwapMatrix Q r K * subsetSwapMatrix Q r K J = subsetSwapMatrix Q r K Jᶜ

@[simp]

theorem Cslib.LinearAlgebra.fullSwapMatrix_mul_apply (Q r : ℕ) (K : Type u_1) [CommRing K] (A : Matrix (AuxLabel Q r) (AuxLabel Q r) K) (u y : AuxLabel Q r) : (fullSwapMatrix Q r K * A) u y = A (fullSwap u) y

def Cslib.LinearAlgebra.twoW0 (Q r : ℕ) (K : Type u_1) [CommRing K] : Matrix (AuxLabel Q r) (AuxLabel Q r) K

The integer-valued operator 2 W_0 = ∑ s : Fin Q, (I - Π_s) (eq. 4.6).

def Cslib.LinearAlgebra.W0 (Q r : ℕ) : Matrix (AuxLabel Q r) (AuxLabel Q r) ℚ

The operator W_0 = (1/2) ∑ s : Fin Q, (I - Π_s) over ℚ (eq. 4.6).

theorem Cslib.LinearAlgebra.two_smul_W0 (Q r : ℕ) : 2 • W0 Q r = twoW0 Q r ℚ

2. Parity interpolation polynomial f_I and exchange matrix M_0

noncomputable def Cslib.LinearAlgebra.fallingTermPoly (A₀ j : ℕ) : Polynomial ℚ

The j-th polynomial factor (-1)^(A₀ + j) ∏_{a < j} (2 X - 2 (A₀ + a)) appearing in the numerator of f_I(X) (eq. 4.7 and Lemma 4.6).

noncomputable def Cslib.LinearAlgebra.fI (A₀ R : ℕ) : Polynomial ℚ

The parity interpolation polynomial f_I(z) = (-1)^{A₀} ∑_{j=0}^{R-1} (-2)^j choose(z - A₀, j) over ℚ (eq. 4.7).

theorem Cslib.LinearAlgebra.natDegree_fallingTermPoly_le (A₀ j : ℕ) : (fallingTermPoly A₀ j).natDegree ≤ j

theorem Cslib.LinearAlgebra.natDegree_fI_le (A₀ R : ℕ) : (fI A₀ R).natDegree ≤ R - 1

The parity interpolation polynomial fI A₀ R has degree at most R - 1 (eq. 4.7, p. 28).

def Cslib.LinearAlgebra.fallingProdMatrixInt (Q r A₀ j : ℕ) : Matrix (AuxLabel Q r) (AuxLabel Q r) ℤ

Product of the j integer matrix factors ∏_{a < j} (2 W_0 - 2 (A₀ + a) I).

def Cslib.LinearAlgebra.fallingTermMatrixInt (Q r A₀ j : ℕ) : Matrix (AuxLabel Q r) (AuxLabel Q r) ℤ

The j-th integer matrix term (-1)^(A₀ + j) ∏_{a < j} (2 W_0 - 2 (A₀ + a) I) from the proof of Lemma 4.6 (p. 33).

def Cslib.LinearAlgebra.M0 (Q r A₀ R : ℕ) : Matrix (AuxLabel Q r) (AuxLabel Q r) ℚ

The auxiliary exchange matrix M_0 = V_0 f_I(W_0) over ℚ (eq. 4.7).

def Cslib.LinearAlgebra.M0ScaledInt (Q r A₀ R : ℕ) : Matrix (AuxLabel Q r) (AuxLabel Q r) ℤ

The scaled integer exchange matrix (R - 1)! M_0 over ℤ (Lemma 4.6, p. 33).

theorem Cslib.LinearAlgebra.eval_fallingTermPoly_add (A₀ q j : ℕ) : Polynomial.eval (↑(A₀ + q)) (fallingTermPoly A₀ j) = (-1) ^ A₀ * (-2) ^ j * ↑j.factorial * ↑(q.choose j)

theorem Cslib.LinearAlgebra.eval_fI_of_mem_Ico {A₀ R k : ℕ} (hk : k ∈ Finset.Ico A₀ (A₀ + R)) : Polynomial.eval (↑k) (fI A₀ R) = (-1) ^ k

On the interval I = Finset.Ico A₀ (A₀ + R), the polynomial fI A₀ R evaluates to (-1)^k.

3. Explicit {0, 1, -1}-eigenbasis and Lemma 4.1

def Cslib.LinearAlgebra.pairInd {r : ℕ} (a b x y : Fin r) : ℤ

Indicator of the ordered pair (a, b) ∈ Fin r × Fin r.

def Cslib.LinearAlgebra.pairBasis {r : ℕ} (α δ x y : Fin r) : ℤ

1-slot orthogonal basis function on Fin r × Fin r with values in {0, 1, -1} (Proof of Lemma 4.1, p. 28).

def Cslib.LinearAlgebra.pairSign {r : ℕ} (α δ : Fin r) : ℤ

Swap eigenvalue of pairBasis α δ: -1 when δ < α and +1 otherwise.

def Cslib.LinearAlgebra.pairNormSq {r : ℕ} (α δ : Fin r) : ℤ

Squared ℓ₂-norm of pairBasis α δ: 1 on the diagonal α = δ and 2 off the diagonal.

theorem Cslib.LinearAlgebra.pairNormSq_pos {r : ℕ} (α δ : Fin r) : 0 < pairNormSq α δ

theorem Cslib.LinearAlgebra.pairInd_swap {r : ℕ} (a b x y : Fin r) : pairInd a b y x = pairInd b a x y

theorem Cslib.LinearAlgebra.pairBasis_swap {r : ℕ} (α δ x y : Fin r) : pairBasis α δ y x = pairSign α δ * pairBasis α δ x y

theorem Cslib.LinearAlgebra.pairBasis_mem {r : ℕ} (α δ x y : Fin r) : pairBasis α δ x y = 0 ∨ pairBasis α δ x y = 1 ∨ pairBasis α δ x y = -1

theorem Cslib.LinearAlgebra.sum_pairBasis_mul_pairBasis {r : ℕ} (α δ α' δ' : Fin r) : ∑ x : Fin r, ∑ y : Fin r, pairBasis α δ x y * pairBasis α' δ' x y = if α = α' ∧ δ = δ' then pairNormSq α δ else 0

def Cslib.LinearAlgebra.eigenvecInt {Q r : ℕ} (β u : AuxLabel Q r) : ℤ

The integer-valued simultaneous eigenvector ψ_β on AuxLabel Q r (Proof of Lemma 4.1).

def Cslib.LinearAlgebra.eigenvec {Q r : ℕ} (K : Type u_1) [CommRing K] (β : AuxLabel Q r) : AuxLabel Q r → K

The simultaneous eigenvector ψ_β over any commutative ring K.

def Cslib.LinearAlgebra.antisymCount {Q r : ℕ} (β : AuxLabel Q r) : ℕ

The number of antisymmetric factors (j(β)) in eigenvec K β, i.e., slots s with β.2 s < β.1 s.

def Cslib.LinearAlgebra.eigenNormSq {Q r : ℕ} (β : AuxLabel Q r) : ℤ

Squared ℓ₂-norm of eigenvecInt β.

theorem Cslib.LinearAlgebra.eigenNormSq_pos {Q r : ℕ} (β : AuxLabel Q r) : 0 < eigenNormSq β

theorem Cslib.LinearAlgebra.eigenvecInt_mem {Q r : ℕ} (β u : AuxLabel Q r) : eigenvecInt β u = 0 ∨ eigenvecInt β u = 1 ∨ eigenvecInt β u = -1

Every entry of eigenvecInt β belongs to {0, 1, -1}.

theorem Cslib.LinearAlgebra.abs_eigenvecInt_le_one {Q r : ℕ} (β u : AuxLabel Q r) : |eigenvecInt β u| ≤ 1

theorem Cslib.LinearAlgebra.eigenvecInt_slotSwap {Q r : ℕ} (s : Fin Q) (β u : AuxLabel Q r) : eigenvecInt β (slotSwap s u) = pairSign (β.1 s) (β.2 s) * eigenvecInt β u

theorem Cslib.LinearAlgebra.slotSwapMatrix_mulVec_eigenvec (Q r : ℕ) (K : Type u_1) [CommRing K] (s : Fin Q) (β : AuxLabel Q r) : (slotSwapMatrix Q r K s).mulVec (eigenvec K β) = ↑(pairSign (β.1 s) (β.2 s)) • eigenvec K β

theorem Cslib.LinearAlgebra.prod_pairSign_eq_neg_one_pow_antisymCount {Q r : ℕ} (β : AuxLabel Q r) : ∏ s : Fin Q, pairSign (β.1 s) (β.2 s) = (-1) ^ antisymCount β

theorem Cslib.LinearAlgebra.eigenvecInt_fullSwap {Q r : ℕ} (β u : AuxLabel Q r) : eigenvecInt β (fullSwap u) = (-1) ^ antisymCount β * eigenvecInt β u

theorem Cslib.LinearAlgebra.fullSwapMatrix_mulVec_eigenvec (Q r : ℕ) (K : Type u_1) [CommRing K] (β : AuxLabel Q r) : (fullSwapMatrix Q r K).mulVec (eigenvec K β) = (-1) ^ antisymCount β • eigenvec K β

theorem Cslib.LinearAlgebra.sum_one_sub_pairSign {Q r : ℕ} (β : AuxLabel Q r) : ∑ s : Fin Q, (1 - pairSign (β.1 s) (β.2 s)) = 2 * ↑(antisymCount β)

theorem Cslib.LinearAlgebra.twoW0_mulVec_eigenvec (Q r : ℕ) (K : Type u_1) [CommRing K] (β : AuxLabel Q r) : (twoW0 Q r K).mulVec (eigenvec K β) = (2 * ↑(antisymCount β)) • eigenvec K β

theorem Cslib.LinearAlgebra.W0_mulVec_eigenvec {Q r : ℕ} (β : AuxLabel Q r) : (W0 Q r).mulVec (eigenvec ℚ β) = ↑(antisymCount β) • eigenvec ℚ β

theorem Cslib.LinearAlgebra.fallingTermMatrixInt_mulVec_eigenvec (Q r A₀ j : ℕ) (β : AuxLabel Q r) : (fallingTermMatrixInt Q r A₀ j).mulVec (eigenvec ℤ β) = ((-1) ^ (A₀ + j) * ∏ a ∈ Finset.range j, (2 * ↑(antisymCount β) - 2 * (↑A₀ + ↑a))) • eigenvec ℤ β

theorem Cslib.LinearAlgebra.fallingTermMatrix_map_mulVec_eigenvec (Q r A₀ j : ℕ) (β : AuxLabel Q r) : ((fallingTermMatrixInt Q r A₀ j).map Int.cast).mulVec (eigenvec ℚ β) = Polynomial.eval (↑(antisymCount β)) (fallingTermPoly A₀ j) • eigenvec ℚ β

theorem Cslib.LinearAlgebra.M0_mulVec_eigenvec {Q r A₀ R : ℕ} (β : AuxLabel Q r) : (M0 Q r A₀ R).mulVec (eigenvec ℚ β) = ((-1) ^ antisymCount β * Polynomial.eval (↑(antisymCount β)) (fI A₀ R)) • eigenvec ℚ β

theorem Cslib.LinearAlgebra.M0_mulVec_eigenvec_of_mem_Ico {Q r A₀ R : ℕ} {β : AuxLabel Q r} (hβ : antisymCount β ∈ Finset.Ico A₀ (A₀ + R)) : (M0 Q r A₀ R).mulVec (eigenvec ℚ β) = eigenvec ℚ β

When antisymCount β ∈ Finset.Ico A₀ (A₀ + R), M0 Q r A₀ R fixes eigenvec ℚ β.

theorem Cslib.LinearAlgebra.sum_eigenvecInt_mul_eigenvecInt {Q r : ℕ} (β β' : AuxLabel Q r) : ∑ u : AuxLabel Q r, eigenvecInt β u * eigenvecInt β' u = if β = β' then eigenNormSq β else 0

Orthogonality of the {0, 1, -1}-eigenbasis eigenvecInt on AuxLabel Q r.

def Cslib.LinearAlgebra.eigenMatrix (Q r : ℕ) : Matrix (AuxLabel Q r) (AuxLabel Q r) ℚ

The square matrix whose β-th row is eigenvec ℚ β.

def Cslib.LinearAlgebra.invNormDiag (Q r : ℕ) : Matrix (AuxLabel Q r) (AuxLabel Q r) ℚ

The inverse diagonal norm matrix matching eigenMatrix Q r.

theorem Cslib.LinearAlgebra.invNormDiag_mul_eigenMatrix_mul_transpose (Q r : ℕ) : invNormDiag Q r * eigenMatrix Q r * (eigenMatrix Q r).transpose = 1

theorem Cslib.LinearAlgebra.transpose_eigenMatrix_mul_invNormDiag_mul_eigenMatrix (Q r : ℕ) : (eigenMatrix Q r).transpose * (invNormDiag Q r * eigenMatrix Q r) = 1

theorem Cslib.LinearAlgebra.eq_sum_eigenvec (Q r : ℕ) (ξ : AuxLabel Q r → ℚ) : ξ = ∑ β : AuxLabel Q r, ((↑(eigenNormSq β))⁻¹ * eigenvec ℚ β ⬝ᵥ ξ) • eigenvec ℚ β

Orthogonal basis expansion of any vector ξ : AuxLabel Q r → ℚ in terms of eigenvec ℚ β.

def Cslib.LinearAlgebra.measurementIndices (Q r A₀ R : ℕ) : Finset (AuxLabel Q r)

The set of basis indices β : AuxLabel Q r whose antisymmetric count j(β) lies outside the interval I = Finset.Ico A₀ (A₀ + R).

theorem Cslib.LinearAlgebra.card_measurementIndices_add_card_mem_Ico (Q r A₀ R : ℕ) : (measurementIndices Q r A₀ R).card + {β : AuxLabel Q r | antisymCount β ∈ Finset.Ico A₀ (A₀ + R)}.card = r ^ (2 * Q)

The number of measurement rows #(measurementIndices Q r A₀ R) plus the number of fixed basis indices in I = Finset.Ico A₀ (A₀ + R) equals D = r ^ (2 * Q).

theorem Cslib.LinearAlgebra.two_mul_card_antisymPair_add_eq_sq (r : ℕ) : 2 * {p : Fin r × Fin r | p.2 < p.1}.card + r = r ^ 2

At each slot, the number of antisymmetric pairs (α, δ) ∈ Fin r × Fin r with δ < α satisfies 2 * #{p : Fin r × Fin r | p.2 < p.1} + r = r ^ 2 (i.e., r * (r - 1) / 2 pairs with eigenvalue -1 and r * (r + 1) / 2 pairs with eigenvalue +1, Proof of Lemma 4.1, p. 28).

def Cslib.LinearAlgebra.measurementMatrix (Q r A₀ R : ℕ) (K : Type u_1) [CommRing K] : Matrix (↥(measurementIndices Q r A₀ R)) (AuxLabel Q r) K

The {0, 1, -1}-valued measurement matrix C^B of Lemma 4.1 (p. 28), whose rows are the transposes of eigenvec K β for β ∈ measurementIndices Q r A₀ R.

theorem Cslib.LinearAlgebra.measurementMatrix_entry_mem (Q r A₀ R : ℕ) (β : ↥(measurementIndices Q r A₀ R)) (u : AuxLabel Q r) : measurementMatrix Q r A₀ R ℤ β u = 0 ∨ measurementMatrix Q r A₀ R ℤ β u = 1 ∨ measurementMatrix Q r A₀ R ℤ β u = -1

theorem Cslib.LinearAlgebra.measurementMatrix_mulVec_eq_zero_iff (Q r A₀ R : ℕ) (K : Type u_1) [CommRing K] (ξ : AuxLabel Q r → K) : (measurementMatrix Q r A₀ R K).mulVec ξ = 0 ↔ ∀ (β : AuxLabel Q r), antisymCount β ∉ Finset.Ico A₀ (A₀ + R) → eigenvec K β ⬝ᵥ ξ = 0

theorem Cslib.LinearAlgebra.M0_mulVec_eq_self_of_measurementMatrix_mulVec_eq_zero {Q r A₀ R : ℕ} {ξ : AuxLabel Q r → ℚ} (hker : (measurementMatrix Q r A₀ R ℚ).mulVec ξ = 0) : (M0 Q r A₀ R).mulVec ξ = ξ

Lemma 4.1 (Kernel invariance, p. 28): if (measurementMatrix Q r A₀ R ℚ).mulVec ξ = 0, then M0 Q r A₀ R fixes ξ.

4. Mismatch support bound (Lemma 4.2, pp. 28–29)

def Cslib.LinearAlgebra.mismatchSet {Q r : ℕ} (u y : AuxLabel Q r) : Finset (Fin Q)

The mismatch set E_{u,y} = {s : Fin Q | y.1 s ≠ u.2 s} (eq. 4.9).

theorem Cslib.LinearAlgebra.card_mismatchSet_le_of_M0_ne_zero {Q r A₀ R : ℕ} {u y : AuxLabel Q r} (hne : M0 Q r A₀ R u y ≠ 0) : (mismatchSet u y).card ≤ R - 1

Lemma 4.2 (Mismatch support bound, pp. 28–29): if M0 Q r A₀ R u y ≠ 0, then #{s : Fin Q | y.1 s ≠ u.2 s} ≤ R - 1.

theorem Cslib.LinearAlgebra.card_mismatchSet_le_of_M0ScaledInt_ne_zero {Q r A₀ R : ℕ} {u y : AuxLabel Q r} (hne : M0ScaledInt Q r A₀ R u y ≠ 0) : (mismatchSet u y).card ≤ R - 1

Integer counterpart of Lemma 4.2 for M0ScaledInt Q r A₀ R.

5. Auxiliary polynomial replacement rows (Lemma 4.3, pp. 29–30)

def Cslib.LinearAlgebra.nodePoint {Q : ℕ} (s : Fin Q) : ℚ

The 1-based evaluation node t = s.1 + 1 ∈ {1, ..., Q} associated to s : Fin Q.

theorem Cslib.LinearAlgebra.nodePoint_pos {Q : ℕ} (s : Fin Q) : 0 < nodePoint s

theorem Cslib.LinearAlgebra.nodePoint_ne_zero {Q : ℕ} (s : Fin Q) : nodePoint s ≠ 0

noncomputable def Cslib.LinearAlgebra.mismatchAnnihilator {Q r : ℕ} (u y : AuxLabel Q r) : Polynomial ℚ

The Lagrange mismatch annihilator polynomial φ_{u,y}(T) = ∏_{s ∈ E_{u,y}} (1 - T / (s.1 + 1)) ∈ ℚ[X] (eq. 4.9).

@[simp]

theorem Cslib.LinearAlgebra.eval_mismatchAnnihilator_zero {Q r : ℕ} (u y : AuxLabel Q r) : Polynomial.eval 0 (mismatchAnnihilator u y) = 1

theorem Cslib.LinearAlgebra.eval_mismatchAnnihilator_nodePoint_of_ne {Q r : ℕ} {u y : AuxLabel Q r} {s : Fin Q} (hne : y.1 s ≠ u.2 s) : Polynomial.eval (nodePoint s) (mismatchAnnihilator u y) = 0

theorem Cslib.LinearAlgebra.natDegree_mismatchAnnihilator_le {Q r : ℕ} (u y : AuxLabel Q r) : (mismatchAnnihilator u y).natDegree ≤ (mismatchSet u y).card

noncomputable def Cslib.LinearAlgebra.auxReplacementRow (Q r A₀ R : ℕ) (u y : AuxLabel Q r) : Polynomial ℚ

The auxiliary replacement polynomial row P⃗_u(T) ∈ (AuxLabel Q r → ℚ[X]) (eq. 4.10): P⃗_u(T)_y = (I - M_0)[u, y] + M_0[u, y] φ_{u,y}(T).

noncomputable def Cslib.LinearAlgebra.evalAuxReplacementRow (Q r A₀ R : ℕ) (u : AuxLabel Q r) (t : ℚ) (ζ : AuxLabel Q r → ℚ) : ℚ

Pairing ⟨P⃗_u(t), ζ⟩ of auxReplacementRow Q r A₀ R u with ζ : AuxLabel Q r → ℚ at T = t (eq. 4.11).

def Cslib.LinearAlgebra.auxGroup {Q r : ℕ} (s : Fin Q) (g : Fin r) : Finset (AuxLabel Q r)

The auxiliary coordinate group S^B_{s, g} = {y : AuxLabel Q r | y.1 s = g} (eq. 4.3).

@[simp]

theorem Cslib.LinearAlgebra.mem_auxGroup {Q r : ℕ} {s : Fin Q} {g : Fin r} {y : AuxLabel Q r} : y ∈ auxGroup s g ↔ y.1 s = g

theorem Cslib.LinearAlgebra.disjoint_auxGroup {Q r : ℕ} (s : Fin Q) {g₁ g₂ : Fin r} (hne : g₁ ≠ g₂) : Disjoint (auxGroup s g₁) (auxGroup s g₂)

theorem Cslib.LinearAlgebra.biUnion_auxGroup {Q r : ℕ} (s : Fin Q) : Finset.univ.biUnion (auxGroup s) = Finset.univ

def Cslib.LinearAlgebra.auxGroupRestrict {Q r : ℕ} {K : Type u_1} [Zero K] (s : Fin Q) (g : Fin r) (ζ : AuxLabel Q r → K) : AuxLabel Q r → K

Restriction of a vector ζ : AuxLabel Q r → K to auxGroup s g, extended by zero outside auxGroup s g (Section 4.3, p. 29).

theorem Cslib.LinearAlgebra.sum_auxGroupRestrict {Q r : ℕ} {K : Type u_1} [AddCommMonoid K] (s : Fin Q) (ζ : AuxLabel Q r → K) : ∑ g : Fin r, auxGroupRestrict s g ζ = ζ

theorem Cslib.LinearAlgebra.sum_measurementMatrix_mulVec_auxGroupRestrict (Q r A₀ R : ℕ) (K : Type u_1) [CommRing K] (s : Fin Q) (ζ : AuxLabel Q r → K) : ∑ g : Fin r, (measurementMatrix Q r A₀ R K).mulVec (auxGroupRestrict s g ζ) = (measurementMatrix Q r A₀ R K).mulVec ζ

Equation (4.12) (p. 29): the measurement vector C^B ζ is the sum over g : Fin r of the restricted measurement vectors C^B (ζ|_{S^B_{s, g}}).

theorem Cslib.LinearAlgebra.natDegree_auxReplacementRow_le (Q r A₀ R : ℕ) (u y : AuxLabel Q r) : (auxReplacementRow Q r A₀ R u y).natDegree ≤ R - 1

Lemma 4.3 (Degree bound, p. 29): every entry of auxReplacementRow Q r A₀ R u has degree at most R - 1.

@[simp]

theorem Cslib.LinearAlgebra.eval_auxReplacementRow_zero (Q r A₀ R : ℕ) (u y : AuxLabel Q r) : Polynomial.eval 0 (auxReplacementRow Q r A₀ R u y) = if u = y then 1 else 0

Lemma 4.3 (Value at zero, p. 29): P⃗_u(0) = δ_u.

@[simp]

theorem Cslib.LinearAlgebra.evalAuxReplacementRow_zero (Q r A₀ R : ℕ) (u : AuxLabel Q r) (ζ : AuxLabel Q r → ℚ) : evalAuxReplacementRow Q r A₀ R u 0 ζ = ζ u

Lemma 4.3 (Linear form at zero, p. 29): ⟨P⃗_u(0), ζ⟩ = ζ u.

theorem Cslib.LinearAlgebra.evalAuxReplacementRow_eq (Q r A₀ R : ℕ) (u : AuxLabel Q r) (t : ℚ) (ζ : AuxLabel Q r → ℚ) : evalAuxReplacementRow Q r A₀ R u t ζ = (1 - M0 Q r A₀ R).mulVec ζ u + ∑ y : AuxLabel Q r, M0 Q r A₀ R u y * Polynomial.eval t (mismatchAnnihilator u y) * ζ y

Equation (4.11) decomposition of ⟨P⃗_u(t), ζ⟩.

theorem Cslib.LinearAlgebra.evalAuxReplacementRow_nodePoint (Q r A₀ R : ℕ) (u : AuxLabel Q r) (s : Fin Q) (ζ : AuxLabel Q r → ℚ) : evalAuxReplacementRow Q r A₀ R u (nodePoint s) ζ = (1 - M0 Q r A₀ R).mulVec ζ u + ∑ y ∈ auxGroup s (u.2 s), M0 Q r A₀ R u y * Polynomial.eval (nodePoint s) (mismatchAnnihilator u y) * ζ y

At t = nodePoint s, the sum in (4.11) ranges only over y ∈ auxGroup s (u.2 s).

theorem Cslib.LinearAlgebra.evalAuxReplacementRow_nodePoint_eq_zero_of_kernel (Q r A₀ R : ℕ) (u : AuxLabel Q r) (s : Fin Q) (g : Fin r) (hg : g ≠ u.2 s) (ξ : AuxLabel Q r → ℚ) (hsupp : ∀ y ∉ auxGroup s g, ξ y = 0) (hker : (measurementMatrix Q r A₀ R ℚ).mulVec ξ = 0) : evalAuxReplacementRow Q r A₀ R u (nodePoint s) ξ = 0

Lemma 4.3 (Restricted kernel vanishing, p. 29): for g ≠ u.2 s, if ξ is supported on auxGroup s g and (measurementMatrix Q r A₀ R ℚ).mulVec ξ = 0, then ⟨P⃗_u(nodePoint s), ξ⟩ = 0.

theorem Cslib.LinearAlgebra.evalAuxReplacementRow_nodePoint_eq_of_eq_on_auxGroup (Q r A₀ R : ℕ) (u : AuxLabel Q r) (s : Fin Q) (ζ₁ ζ₂ : AuxLabel Q r → ℚ) (hgroup : ∀ y ∈ auxGroup s (u.2 s), ζ₁ y = ζ₂ y) (hmeas : (measurementMatrix Q r A₀ R ℚ).mulVec ζ₁ = (measurementMatrix Q r A₀ R ℚ).mulVec ζ₂) : evalAuxReplacementRow Q r A₀ R u (nodePoint s) ζ₁ = evalAuxReplacementRow Q r A₀ R u (nodePoint s) ζ₂

Lemma 4.3 (Determination by assigned group and measurements, p. 29): at t = nodePoint s, ⟨P⃗_u(nodePoint s), ζ⟩ is uniquely determined by ζ on auxGroup s (u.2 s) and (measurementMatrix Q r A₀ R ℚ).mulVec ζ.

6. Common-denominator clearing (Lemma 4.6, p. 33)

def Cslib.LinearAlgebra.commonDenom (Q R : ℕ) : ℕ

The common denominator d_den = (R - 1)! Q! of Lemma 4.6 (p. 33).

theorem Cslib.LinearAlgebra.commonDenom_pos (Q R : ℕ) : 0 < commonDenom Q R

noncomputable def Cslib.LinearAlgebra.mismatchAnnihilatorScaledInt {Q r : ℕ} (u y : AuxLabel Q r) : Polynomial ℤ

The scaled integer polynomial Q! φ_{u,y}(T) ∈ ℤ[X] (Lemma 4.6, p. 33).

noncomputable def Cslib.LinearAlgebra.auxReplacementRowScaledInt (Q r A₀ R : ℕ) (u y : AuxLabel Q r) : Polynomial ℤ

The scaled integer replacement row d_den P⃗_u(T) (Lemma 4.6, p. 33).

theorem Cslib.LinearAlgebra.map_mismatchAnnihilatorScaledInt {Q r : ℕ} (u y : AuxLabel Q r) : Polynomial.map (Int.castRingHom ℚ) (mismatchAnnihilatorScaledInt u y) = ↑Q.factorial • mismatchAnnihilator u y

theorem Cslib.LinearAlgebra.map_M0ScaledInt (Q r A₀ R : ℕ) : (M0ScaledInt Q r A₀ R).map Int.cast = ↑(R - 1).factorial • M0 Q r A₀ R

theorem Cslib.LinearAlgebra.map_auxReplacementRowScaledInt (Q r A₀ R : ℕ) (u y : AuxLabel Q r) : Polynomial.map (Int.castRingHom ℚ) (auxReplacementRowScaledInt Q r A₀ R u y) = ↑(commonDenom Q R) • auxReplacementRow Q r A₀ R u y

Lemma 4.6 (Common-denominator clearing, p. 33): multiplying auxReplacementRow Q r A₀ R u y by commonDenom Q R = (R - 1)! Q! gives the integer polynomial auxReplacementRowScaledInt Q r A₀ R u y.