SupportMaskChecker

Abstract

Exact tree evaluation and finite Fourier identities support the exclusion of uniform mixing on the cycle with twenty-one vertices.

Theorem 1.1 (mask_sound).

$\forall (α : Type) (t : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree α) (j : Nat), (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.indexValid t = true) \to ((D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask t) . testBit j = true ⟺ D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.low t + j \in D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.leaves t)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.mask_sound (✓ std3). ∎

Source. Repository-derived.

Commentary.

A valid support tree encodes membership exactly: bit j is set precisely when low(t) + j occurs among its leaves. The induction shifts each child mask to the common lower bound.

Theorem 1.2 (checked_permutation).

$\forall (α : Type) (t : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree α) (n : Nat), (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.indexValid t = true) \to ((D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.low t = 0) \to ((D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask t = 2^{n} - 1) \to ((D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.count t = n) \to ((D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.leaves t) . Perm (List.range n)))))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked_permutation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.3 (list_range_sum).

$\forall (K : Type) [CommRing K] (F : Nat \to K) (n : Nat), ((List.range n) . map F) . sum = \sum i \in Finset.range n, F i$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.list_range_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.4 (source_sum).

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.source_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.5 (rows1).

$rows1 : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.rows1 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.6 (expectedMask1).

$expectedMask1 : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.expectedMask1 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.7 (rowChecked1).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source rows1 = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.rowChecked1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.8 (targetChecked1).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.targetCheck rows1 = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.targetChecked1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.9 (idsValid1).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.indexValid (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids rows1) = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.idsValid1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.10 (maskChecked1).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids rows1) = expectedMask1$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.maskChecked1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.11 (countChecked1).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.count (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids rows1) = 49954$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.countChecked1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.12 (targetSum1).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.targetSum rows1 = 0$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.targetSum1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.13 (g1).

$\forall (K : Type) [CommRing K] (x0 : K) (x1 : K) (x2 : K) (x3 : K) (x4 : K) (x5 : K), g1 x0 x1 x2 x3 x4 x5 = ((((((1) : K) \cdot x1^{(2 : N)} \cdot x2 \cdot x3 \cdot x4 \cdot x5 + ((1) : K) \cdot x1^{(2 : N)} \cdot x2^{(2 : N)} \cdot x4 \cdot x5^{(2 : N)}) + (((1) : K) \cdot x0 \cdot x1 \cdot x2^{(2 : N)} \cdot x4 \cdot x5 + (((1) : K) \cdot x0 \cdot x1^{(2 : N)} \cdot x2 \cdot x4 \cdot x5 + ((1) : K) \cdot x0^{(2 : N)} \cdot x2^{(2 : N)} \cdot x3 \cdot x4 \cdot x5))) + ((((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x3^{(2 : N)} \cdot x4 + ((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x3^{(2 : N)} \cdot x4 \cdot x5) + (((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x3^{(2 : N)} \cdot x4^{(2 : N)} + (((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2 \cdot x4^{(2 : N)} \cdot x5 + ((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2 \cdot x3 \cdot x5^{(2 : N)})))) + (((((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2 \cdot x3 \cdot x4 \cdot x5 + ((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2 \cdot x3 \cdot x4^{(2 : N)}) + (((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2 \cdot x3^{(2 : N)} \cdot x5 + (((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x5^{(2 : N)} + ((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x4 \cdot x5))) + ((((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x4 \cdot x5^{(2 : N)} + (((1) : K) \cdot x0^{(2 : N)} \cdot x1^{(2 : N)} \cdot x3 \cdot x4 \cdot x5 + ((1) : K) \cdot x0^{(3 : N)} \cdot x2 \cdot x3^{(2 : N)} \cdot x4 \cdot x5)) + (((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x3^{(2 : N)} \cdot x4 \cdot x5 + (((1) : K) \cdot x0^{(4 : N)} \cdot x3^{(2 : N)} \cdot x4 + ((1) : K) \cdot x0^{(4 : N)} \cdot x2 \cdot x3 \cdot x4 \cdot x5)))))$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g1 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.14 (g2).

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g2 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.15 (g3).

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g3 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.16 (g4).

$\forall (K : Type) [CommRing K] (x0 : K) (x1 : K) (x2 : K) (x3 : K) (x4 : K) (x5 : K), g4 x0 x1 x2 x3 x4 x5 = ((((((1) : K) \cdot x1 \cdot x2 \cdot x3 \cdot x4^{(2 : N)} \cdot x5^{(2 : N)} + ((1) : K) \cdot x0 \cdot x1 \cdot x2 \cdot x4 \cdot x5^{(2 : N)}) + (((1) : K) \cdot x0 \cdot x1 \cdot x2 \cdot x4 \cdot x5^{(3 : N)} + (((1) : K) \cdot x0 \cdot x1 \cdot x2 \cdot x3^{(2 : N)} \cdot x4^{(2 : N)} \cdot x5^{(2 : N)} + ((1) : K) \cdot x0 \cdot x1 \cdot x2^{(2 : N)} \cdot x3 \cdot x4^{(2 : N)} \cdot x5^{(3 : N)}))) + ((((1) : K) \cdot x0 \cdot x1^{(2 : N)} \cdot x2 \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0 \cdot x1^{(2 : N)} \cdot x2^{(2 : N)} \cdot x4^{(2 : N)} \cdot x5^{(3 : N)}) + (((1) : K) \cdot x0^{(2 : N)} \cdot x2 \cdot x3 \cdot x4 \cdot x5^{(3 : N)} + (((1) : K) \cdot x0^{(2 : N)} \cdot x2 \cdot x3^{(2 : N)} \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x3 \cdot x4)))) + (((((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2 \cdot x3 \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x3 \cdot x4 \cdot x5^{(4 : N)}) + (((1) : K) \cdot x0^{(2 : N)} \cdot x1^{(2 : N)} \cdot x2 \cdot x4 \cdot x5^{(2 : N)} + (((1) : K) \cdot x0^{(2 : N)} \cdot x1^{(2 : N)} \cdot x2 \cdot x3 \cdot x4 \cdot x5 + ((1) : K) \cdot x0^{(3 : N)} \cdot x3^{(2 : N)} \cdot x5))) + ((((1) : K) \cdot x0^{(3 : N)} \cdot x2 \cdot x3^{(2 : N)} \cdot x4 \cdot x5^{(2 : N)} + (((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x3 \cdot x5 + ((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x2 \cdot x5^{(2 : N)})) + (((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x2 \cdot x3^{(2 : N)} \cdot x4 \cdot x5 + (((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x2 \cdot x3^{(2 : N)} \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0^{(4 : N)} \cdot x1 \cdot x2 \cdot x3 \cdot x5^{(2 : N)})))))$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g4 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.17 (g5).

$\forall (K : Type) [CommRing K] (x0 : K) (x1 : K) (x2 : K) (x3 : K) (x4 : K) (x5 : K), g5 x0 x1 x2 x3 x4 x5 = ((((((1) : K) \cdot x1 \cdot x2 \cdot x3 \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0 \cdot x2^{(2 : N)} \cdot x4 \cdot x5^{(2 : N)}) + (((1) : K) \cdot x0 \cdot x1 \cdot x3 \cdot x4 \cdot x5 + (((1) : K) \cdot x0 \cdot x1 \cdot x2^{(2 : N)} \cdot x3 \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0 \cdot x1 \cdot x2^{(2 : N)} \cdot x3 \cdot x4^{(2 : N)} \cdot x5^{(2 : N)}))) + ((((1) : K) \cdot x0 \cdot x1^{(2 : N)} \cdot x2^{(2 : N)} \cdot x3 \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0^{(2 : N)} \cdot x2 \cdot x3 \cdot x4^{(2 : N)} \cdot x5) + (((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x3 + (((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x3^{(2 : N)} \cdot x4 \cdot x5 + ((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2)))) + (((((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2 \cdot x3 \cdot x4 \cdot x5 + ((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2 \cdot x3^{(2 : N)} \cdot x4^{(2 : N)} \cdot x5^{(2 : N)}) + (((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x4 \cdot x5 + (((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x3 \cdot x4^{(2 : N)} \cdot x5^{(2 : N)} + ((1) : K) \cdot x0^{(2 : N)} \cdot x1^{(2 : N)} \cdot x2 \cdot x3 \cdot x5))) + ((((1) : K) \cdot x0^{(3 : N)} \cdot x3 \cdot x4 + (((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x3 + ((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x3 \cdot x4)) + (((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x3 \cdot x4 \cdot x5 + (((1) : K) \cdot x0^{(3 : N)} \cdot x1^{(2 : N)} \cdot x3^{(2 : N)} \cdot x4 + ((1) : K) \cdot x0^{(4 : N)} \cdot x1 \cdot x2 \cdot x3 \cdot x4)))))$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g5 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.18 (g6).

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g6 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.19 (g7).

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g7 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.20 (g8).

$\forall (K : Type) [CommRing K] (x0 : K) (x1 : K) (x2 : K) (x3 : K) (x4 : K) (x5 : K), g8 x0 x1 x2 x3 x4 x5 = ((((((1) : K) \cdot x3^{(3 : N)} \cdot x4 \cdot x5 + ((1) : K) \cdot x2 \cdot x3^{(2 : N)} \cdot x4 \cdot x5^{(2 : N)}) + (((1) : K) \cdot x1 \cdot x2 \cdot x3 \cdot x4 \cdot x5^{(3 : N)} + (((1) : K) \cdot x1^{(2 : N)} \cdot x2^{(2 : N)} \cdot x3 \cdot x4 \cdot x5^{(4 : N)} + ((1) : K) \cdot x0 \cdot x3^{(2 : N)} \cdot x4 \cdot x5))) + ((((1) : K) \cdot x0 \cdot x1 \cdot x3 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0 \cdot x1 \cdot x3^{(2 : N)} \cdot x5) + (((1) : K) \cdot x0 \cdot x1 \cdot x3^{(3 : N)} \cdot x4 \cdot x5 + (((1) : K) \cdot x0 \cdot x1 \cdot x2 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0 \cdot x1 \cdot x2 \cdot x3 \cdot x4 \cdot x5^{(3 : N)})))) + (((((1) : K) \cdot x0 \cdot x1 \cdot x2 \cdot x3^{(2 : N)} \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0 \cdot x1 \cdot x2 \cdot x3^{(3 : N)} \cdot x4 \cdot x5) + (((1) : K) \cdot x0 \cdot x1 \cdot x2 \cdot x3^{(4 : N)} \cdot x4^{(2 : N)} \cdot x5^{(2 : N)} + (((1) : K) \cdot x0 \cdot x1 \cdot x2^{(2 : N)} \cdot x3 \cdot x4 \cdot x5^{(3 : N)} + ((1) : K) \cdot x0 \cdot x1 \cdot x2^{(2 : N)} \cdot x3^{(2 : N)} \cdot x4^{(2 : N)} \cdot x5^{(3 : N)}))) + ((((1) : K) \cdot x0 \cdot x1 \cdot x2^{(2 : N)} \cdot x3^{(3 : N)} \cdot x4^{(2 : N)} \cdot x5^{(2 : N)} + (((1) : K) \cdot x0 \cdot x1^{(2 : N)} \cdot x2^{(2 : N)} \cdot x3^{(2 : N)} \cdot x4 \cdot x5^{(3 : N)} + ((1) : K) \cdot x0^{(2 : N)} \cdot x3^{(3 : N)} \cdot x4)) + (((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2 \cdot x3^{(3 : N)} \cdot x4 \cdot x5 + (((1) : K) \cdot x0^{(2 : N)} \cdot x1^{(2 : N)} \cdot x2 \cdot x3^{(2 : N)} \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0^{(2 : N)} \cdot x1^{(2 : N)} \cdot x2^{(2 : N)} \cdot x3 \cdot x4 \cdot x5^{(3 : N)})))))$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g8 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.21 (g9).

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g9 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.22 (g12).

$\forall (K : Type) [CommRing K] (x0 x1 x2 x3 x4 x5 : K), g12 x0 x1 x2 x3 x4 x5 : K$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g12 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed cleared certificate polynomial has the displayed type. Its coefficients and monomials are specified by the Lean definition.

Definition 1.23 (g14).

$\forall (K : Type) [CommRing K] (x0 x1 x2 x3 x4 x5 : K), g14 x0 x1 x2 x3 x4 x5 : K$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g14 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed cleared certificate polynomial has the displayed type. Its coefficients and monomials are specified by the Lean definition.

Definition 1.24 (g19).

$\forall (K : Type) [CommRing K] (x0 x1 x2 x3 x4 x5 : K), g19 x0 x1 x2 x3 x4 x5 : K$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g19 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed cleared certificate polynomial has the displayed type. Its coefficients and monomials are specified by the Lean definition.

Definition 1.25 (g10).

$\forall (K : Type) [CommRing K] (x0 : K) (x1 : K) (x2 : K) (x3 : K) (x4 : K) (x5 : K), g10 x0 x1 x2 x3 x4 x5 = ((((((1) : K) \cdot x1 \cdot x2^{(2 : N)} \cdot x5 + ((1) : K) \cdot x0 \cdot x1 \cdot x2^{(2 : N)} \cdot x4 \cdot x5) + (((1) : K) \cdot x0 \cdot x1 \cdot x2^{(2 : N)} \cdot x3 \cdot x5 + (((1) : K) \cdot x0 \cdot x1 \cdot x2^{(3 : N)} \cdot x5^{(2 : N)} + ((1) : K) \cdot x0 \cdot x1 \cdot x2^{(3 : N)} \cdot x4 \cdot x5))) + ((((1) : K) \cdot x0 \cdot x1^{(2 : N)} \cdot x2^{(3 : N)} \cdot x3 \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0 \cdot x1^{(2 : N)} \cdot x2^{(4 : N)} \cdot x4 \cdot x5^{(2 : N)}) + (((1) : K) \cdot x0^{(2 : N)} \cdot x2 \cdot x3 \cdot x4 + (((1) : K) \cdot x0^{(2 : N)} \cdot x2^{(2 : N)} \cdot x5 + ((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x3 \cdot x4)))) + (((((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x3 \cdot x4 \cdot x5 + ((1) : K) \cdot x0^{(2 : N)} \cdot x1 \cdot x2^{(4 : N)} \cdot x3 \cdot x4 \cdot x5^{(2 : N)}) + (((1) : K) \cdot x0^{(2 : N)} \cdot x1^{(2 : N)} \cdot x2^{(2 : N)} \cdot x3^{(2 : N)} \cdot x4^{(2 : N)} \cdot x5 + (((1) : K) \cdot x0^{(2 : N)} \cdot x1^{(2 : N)} \cdot x2^{(3 : N)} \cdot x3 \cdot x4 \cdot x5^{(2 : N)} + ((1) : K) \cdot x0^{(3 : N)} \cdot x3^{(2 : N)} \cdot x4))) + ((((1) : K) \cdot x0^{(3 : N)} \cdot x2 \cdot x3 \cdot x4 + (((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x2 \cdot x3^{(2 : N)} \cdot x4 \cdot x5 + ((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x2 \cdot x3^{(2 : N)} \cdot x4^{(2 : N)})) + (((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x3 \cdot x4^{(2 : N)} \cdot x5 + (((1) : K) \cdot x0^{(3 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x3^{(2 : N)} \cdot x4 \cdot x5 + ((1) : K) \cdot x0^{(4 : N)} \cdot x1 \cdot x2^{(2 : N)} \cdot x3^{(2 : N)} \cdot x4^{(2 : N)} \cdot x5)))))$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g10 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.26 (basisPhase).

$\forall (c : C) (r : Fin 6), basisPhase c r = if r.val = 0 then Complex.exp c else Complex.exp (c \cdot D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Fourier.eigenvalue (r.val : ZMod 21))$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.basisPhase (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.27 (phase21).

$\forall (c : C) (j : ZMod 21), phase21 c j = Complex.exp (c \cdot D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Fourier.eigenvalue j)$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.phase21 (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Theorem 1.28 (basisPhase_ne_zero).

$\forall (c : C) (r : Fin 6), basisPhase c r \neq = 0$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.basisPhase_ne_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.29 (correlation_polynomial_1).

$\forall (c : C), D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g1 (basisPhase c 0) (basisPhase c 1) (basisPhase c 2) (basisPhase c 3) (basisPhase c 4) (basisPhase c 5) = ((basisPhase c 0)^{(2 : N)} \cdot (basisPhase c 1) \cdot (basisPhase c 2) \cdot (basisPhase c 3) \cdot (basisPhase c 4) \cdot (basisPhase c 5)) \cdot \sum j : ZMod 21, phase21 c (j + 1) / phase21 c j$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.30 (correlation_polynomial_2).

$\forall (c : C), D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g2 (basisPhase c 0) (basisPhase c 1) (basisPhase c 2) (basisPhase c 3) (basisPhase c 4) (basisPhase c 5) = ((basisPhase c 0)^{(2 : N)} \cdot (basisPhase c 1) \cdot (basisPhase c 2)^{(2 : N)} \cdot (basisPhase c 3)^{(2 : N)} \cdot (basisPhase c 4) \cdot (basisPhase c 5)^{(2 : N)}) \cdot \sum j : ZMod 21, phase21 c (j + 2) / phase21 c j$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_2 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.31 (correlation_polynomial_3).

$\forall (c : C), D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g3 (basisPhase c 0) (basisPhase c 1) (basisPhase c 2) (basisPhase c 3) (basisPhase c 4) (basisPhase c 5) = ((basisPhase c 0)^{(2 : N)} \cdot (basisPhase c 1) \cdot (basisPhase c 2)^{(2 : N)} \cdot (basisPhase c 3)^{(2 : N)} \cdot (basisPhase c 4) \cdot (basisPhase c 5)^{(2 : N)}) \cdot \sum j : ZMod 21, phase21 c (j + 3) / phase21 c j$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_3 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.32 (correlation_polynomial_4).

$\forall (c : C), D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g4 (basisPhase c 0) (basisPhase c 1) (basisPhase c 2) (basisPhase c 3) (basisPhase c 4) (basisPhase c 5) = ((basisPhase c 0)^{(2 : N)} \cdot (basisPhase c 1) \cdot (basisPhase c 2) \cdot (basisPhase c 3) \cdot (basisPhase c 4) \cdot (basisPhase c 5)^{(2 : N)}) \cdot \sum j : ZMod 21, phase21 c (j + 4) / phase21 c j$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_4 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.33 (correlation_polynomial_5).

$\forall (c : C), D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g5 (basisPhase c 0) (basisPhase c 1) (basisPhase c 2) (basisPhase c 3) (basisPhase c 4) (basisPhase c 5) = ((basisPhase c 0)^{(2 : N)} \cdot (basisPhase c 1) \cdot (basisPhase c 2) \cdot (basisPhase c 3) \cdot (basisPhase c 4) \cdot (basisPhase c 5)) \cdot \sum j : ZMod 21, phase21 c (j + 5) / phase21 c j$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_5 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.34 (correlation_polynomial_6).

$\forall (c : C), D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g6 (basisPhase c 0) (basisPhase c 1) (basisPhase c 2) (basisPhase c 3) (basisPhase c 4) (basisPhase c 5) = ((basisPhase c 0)^{(3 : N)} \cdot (basisPhase c 1) \cdot (basisPhase c 2)^{(2 : N)} \cdot (basisPhase c 3) \cdot (basisPhase c 4)^{(2 : N)} \cdot (basisPhase c 5)^{(2 : N)}) \cdot \sum j : ZMod 21, phase21 c (j + 6) / phase21 c j$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_6 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.35 (correlation_polynomial_7).

$\forall (c : C), D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g7 (basisPhase c 0) (basisPhase c 1) (basisPhase c 2) (basisPhase c 3) (basisPhase c 4) (basisPhase c 5) = ((basisPhase c 0)^{(3 : N)} \cdot (basisPhase c 1)^{(2 : N)} \cdot (basisPhase c 2)^{(2 : N)} \cdot (basisPhase c 3)^{(2 : N)} \cdot (basisPhase c 4)^{(2 : N)} \cdot (basisPhase c 5)^{(2 : N)}) \cdot \sum j : ZMod 21, phase21 c (j + 7) / phase21 c j$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_7 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.36 (correlation_polynomial_8).

$\forall (c : C), D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g8 (basisPhase c 0) (basisPhase c 1) (basisPhase c 2) (basisPhase c 3) (basisPhase c 4) (basisPhase c 5) = ((basisPhase c 0) \cdot (basisPhase c 1) \cdot (basisPhase c 2) \cdot (basisPhase c 3)^{(2 : N)} \cdot (basisPhase c 4) \cdot (basisPhase c 5)^{(2 : N)}) \cdot \sum j : ZMod 21, phase21 c (j + 8) / phase21 c j$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_8 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.37 (correlation_polynomial_9).

$\forall (c : C), D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g9 (basisPhase c 0) (basisPhase c 1) (basisPhase c 2) (basisPhase c 3) (basisPhase c 4) (basisPhase c 5) = ((basisPhase c 0)^{(2 : N)} \cdot (basisPhase c 1)^{(2 : N)} \cdot (basisPhase c 2) \cdot (basisPhase c 3)^{(2 : N)} \cdot (basisPhase c 4) \cdot (basisPhase c 5)) \cdot \sum j : ZMod 21, phase21 c (j + 9) / phase21 c j$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_9 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.38 (correlation_polynomial_10).

$\forall (c : C), D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g10 (basisPhase c 0) (basisPhase c 1) (basisPhase c 2) (basisPhase c 3) (basisPhase c 4) (basisPhase c 5) = ((basisPhase c 0)^{(2 : N)} \cdot (basisPhase c 1) \cdot (basisPhase c 2)^{(2 : N)} \cdot (basisPhase c 3) \cdot (basisPhase c 4) \cdot (basisPhase c 5)) \cdot \sum j : ZMod 21, phase21 c (j + 10) / phase21 c j$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_10 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.39 (group2_0).

$group 2_{0} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_0 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.40 (group2_1).

$group 2_{1} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_1 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.41 (group2_2).

$group 2_{2} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_2 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.42 (group2_3).

$group 2_{3} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_3 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.43 (group2_4).

$group 2_{4} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_4 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.44 (group2_5).

$group 2_{5} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_5 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.45 (group2_6).

$group 2_{6} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_6 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.46 (group2_7).

$group 2_{7} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_7 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.47 (group2_8).

$group 2_{8} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_8 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.48 (group2_9).

$group 2_{9} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_9 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.49 (group2_10).

$group 2_{10} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_10 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.50 (group2_11).

$group 2_{11} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_11 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.51 (group2_12).

$group 2_{12} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_12 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.52 (group2_13).

$group 2_{13} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_13 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.53 (group2_14).

$group 2_{14} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_14 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.54 (group2_15).

$group 2_{15} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_15 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.55 (group2_16).

$group 2_{16} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_16 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.56 (group2_17).

$group 2_{17} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_17 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.57 (group2_18).

$group 2_{18} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_18 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.58 (group2_19).

$group 2_{19} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_19 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Definition 1.59 (group2_20).

$group 2_{20} : D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Rows$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_20 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.60 (checked2_0).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{0} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_0 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.61 (checked2_1).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{1} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.62 (checked2_2).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{2} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_2 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.63 (checked2_3).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{3} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_3 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.64 (checked2_4).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{4} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_4 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.65 (checked2_5).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{5} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_5 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.66 (checked2_6).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{6} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_6 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.67 (checked2_7).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{7} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_7 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.68 (checked2_8).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{8} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_8 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.69 (checked2_9).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{9} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_9 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.70 (checked2_10).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{10} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_10 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.71 (checked2_11).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{11} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_11 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.72 (checked2_12).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{12} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_12 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.73 (checked2_13).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{13} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_13 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.74 (checked2_14).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{14} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_14 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.75 (checked2_15).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{15} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_15 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.76 (checked2_16).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{16} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_16 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.77 (checked2_17).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{17} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_17 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.78 (checked2_18).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{18} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_18 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.79 (checked2_19).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{19} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_19 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Theorem 1.80 (checked2_20).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.rowCheck D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.source group 2_{20} = true$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_20 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.81 (groupMask2_0).

$groupMask 2_{0} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_0 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.82 (groupMaskChecked2_0).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{0}) = groupMask 2_{0}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_0 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.83 (groupMask2_1).

$groupMask 2_{1} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_1 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.84 (groupMaskChecked2_1).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{1}) = groupMask 2_{1}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.85 (groupMask2_2).

$groupMask 2_{2} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_2 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.86 (groupMaskChecked2_2).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{2}) = groupMask 2_{2}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_2 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.87 (groupMask2_3).

$groupMask 2_{3} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_3 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.88 (groupMaskChecked2_3).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{3}) = groupMask 2_{3}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_3 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.89 (groupMask2_4).

$groupMask 2_{4} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_4 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.90 (groupMaskChecked2_4).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{4}) = groupMask 2_{4}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_4 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.91 (groupMask2_5).

$groupMask 2_{5} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_5 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.92 (groupMaskChecked2_5).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{5}) = groupMask 2_{5}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_5 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.93 (groupMask2_6).

$groupMask 2_{6} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_6 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.94 (groupMaskChecked2_6).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{6}) = groupMask 2_{6}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_6 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.95 (groupMask2_7).

$groupMask 2_{7} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_7 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.96 (groupMaskChecked2_7).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{7}) = groupMask 2_{7}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_7 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.97 (groupMask2_8).

$groupMask 2_{8} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_8 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.98 (groupMaskChecked2_8).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{8}) = groupMask 2_{8}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_8 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.99 (groupMask2_9).

$groupMask 2_{9} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_9 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.100 (groupMaskChecked2_9).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{9}) = groupMask 2_{9}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_9 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.101 (groupMask2_10).

$groupMask 2_{10} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_10 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.102 (groupMaskChecked2_10).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{10}) = groupMask 2_{10}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_10 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.103 (groupMask2_11).

$groupMask 2_{11} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_11 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.104 (groupMaskChecked2_11).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{11}) = groupMask 2_{11}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_11 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.105 (groupMask2_12).

$groupMask 2_{12} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_12 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.106 (groupMaskChecked2_12).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{12}) = groupMask 2_{12}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_12 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.107 (groupMask2_13).

$groupMask 2_{13} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_13 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.108 (groupMaskChecked2_13).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{13}) = groupMask 2_{13}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_13 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.109 (groupMask2_14).

$groupMask 2_{14} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_14 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.110 (groupMaskChecked2_14).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{14}) = groupMask 2_{14}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_14 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.111 (groupMask2_15).

$groupMask 2_{15} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_15 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.112 (groupMaskChecked2_15).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{15}) = groupMask 2_{15}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_15 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.113 (groupMask2_16).

$groupMask 2_{16} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_16 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.114 (groupMaskChecked2_16).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{16}) = groupMask 2_{16}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_16 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.115 (groupMask2_17).

$groupMask 2_{17} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_17 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.116 (groupMaskChecked2_17).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{17}) = groupMask 2_{17}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_17 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.117 (groupMask2_18).

$groupMask 2_{18} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_18 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.118 (groupMaskChecked2_18).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{18}) = groupMask 2_{18}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_18 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.119 (groupMask2_19).

$groupMask 2_{19} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_19 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.120 (groupMaskChecked2_19).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{19}) = groupMask 2_{19}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_19 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

Definition 1.121 (groupMask2_20).

$groupMask 2_{20} : Nat$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_20 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed integer support mask has the displayed type. Its leaf sequence and node boundaries are the explicit values in this definition.

Theorem 1.122 (groupMaskChecked2_20).

$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.ids group 2_{20}) = groupMask 2_{20}$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_20 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is used in the orbit-sum and spectral calculation.

References

Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.basisPhase
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.basisPhase_ne_zero
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_0
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_10
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_11
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_12
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_13
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_14
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_15
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_16
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_17
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_18
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_19
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_2
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_20
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_3
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_4
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_5
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_6
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_7
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_8
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked2_9
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.checked_permutation
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_10
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_2
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_3
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_4
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_5
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_6
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_7
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_8
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.correlation_polynomial_9
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.countChecked1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.expectedMask1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g10
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g12
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g14
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g19
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g2
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g3
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g4
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g5
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g6
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g7
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g8
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.g9
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_0
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_10
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_11
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_12
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_13
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_14
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_15
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_16
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_17
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_18
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_19
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_2
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_20
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_3
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_4
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_5
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_6
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_7
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_8
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.group2_9
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_0
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_10
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_11
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_12
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_13
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_14
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_15
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_16
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_17
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_18
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_19
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_2
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_20
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_3
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_4
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_5
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_6
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_7
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_8
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMask2_9
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_0
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_10
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_11
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_12
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_13
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_14
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_15
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_16
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_17
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_18
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_19
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_2
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_20
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_3
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_4
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_5
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_6
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_7
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_8
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.groupMaskChecked2_9
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.idsValid1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.list_range_sum
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.maskChecked1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.mask_sound
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.phase21
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.rowChecked1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.rows1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.source_sum
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.targetChecked1
Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker.targetSum1
Dependency: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums

Keyboard shortcuts

trureturing — Discovering truth

SupportMaskChecker

Abstract

References