OrbitIndexedSums

Abstract

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

Definition 1.1 (Exp).

$$\mathrm{Exp}:\mathrm{Type}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.Exp (✓ std3).

Source. Repository-derived.

Commentary.

The constructor fields are a : Int b : Int c : Int d : Int e : Int f : Int deriving DecidableEq.

Definition 1.2 (plus).

$$\forall (v:\mathrm{Exp})(w:\mathrm{Exp}),\mathrm{plus}vw=⟨v.a+w.a,v.b+w.b,v.c+w.c,v.d+w.d,v.e+w.e,v.f+w.f⟩$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.plus (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.3 (neg).

$$\forall (v:\mathrm{Exp}),\mathrm{neg}v=⟨-v.a,-v.b,-v.c,-v.d,-v.e,-v.f⟩$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.neg (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.4 (act0).

$$(\forall (v:\mathrm{Exp}),act00v=⟨(1)\cdot v.a,(1)\cdot v.b,(1)\cdot v.c,(1)\cdot v.d,(1)\cdot v.e,(1)\cdot v.f⟩)\wedge (\forall (v:\mathrm{Exp}),act01v=⟨(1)\cdot v.a+(-1)\cdot v.d+(1)\cdot v.e,(-1)\cdot v.e,(1)\cdot v.b+(1)\cdot v.d+(-1)\cdot v.e,(-1)\cdot v.d+(1)\cdot v.e+(-1)\cdot v.f,(1)\cdot v.c+(-1)\cdot v.f,(1)\cdot v.d+(-1)\cdot v.e⟩)\wedge (\forall (v:\mathrm{Exp}),act02v=⟨(1)\cdot v.a+(1)\cdot v.c,(-1)\cdot v.c+(1)\cdot v.f,(-1)\cdot v.c+(-1)\cdot v.d,(1)\cdot v.c,(1)\cdot v.b,(-1)\cdot v.c+(-1)\cdot v.d+(1)\cdot v.e⟩)\wedge (\forall (v:\mathrm{Exp}),act03v=⟨(1)\cdot v.a+(1)\cdot v.b,(-1)\cdot v.b,(-1)\cdot v.b+(1)\cdot v.f,(1)\cdot v.b+(1)\cdot v.d+(-1)\cdot v.e,(-1)\cdot v.e,(-1)\cdot v.b+(1)\cdot v.c⟩)\wedge (\forall (v:\mathrm{Exp}),act04v=⟨(1)\cdot v.a+(-1)\cdot v.d,(1)\cdot v.e,(1)\cdot v.d,(-1)\cdot v.c+(-1)\cdot v.d,(-1)\cdot v.c+(1)\cdot v.f,(1)\cdot v.b+(1)\cdot v.d⟩)\wedge (\forall (v:\mathrm{Exp}),act05v=⟨(1)\cdot v.a+(1)\cdot v.f,(1)\cdot v.c+(-1)\cdot v.f,(-1)\cdot v.d+(1)\cdot v.e+(-1)\cdot v.f,(-1)\cdot v.b+(1)\cdot v.f,(-1)\cdot v.b,(-1)\cdot v.d+(-1)\cdot v.f⟩)\wedge (\forall (i:\mathrm{Nat})(v:\mathrm{Exp}),6\le i\to act0iv=v)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.act0 (✓ std3).

Source. Repository-derived.

Commentary.

These six coordinate formulas and the default clause define the action.

Definition 1.5 (act).

$$\forall (g:(\mathrm{ZMod}6\times \mathrm{ZMod}2))(v:\mathrm{Exp}),\mathrm{act}gv=\mathrm{if}Fin.val(\mathrm{show}\mathrm{Fin}2\mathrm{from}g.2)=0\mathrm{then}act0(Fin.val(\mathrm{show}\mathrm{Fin}6\mathrm{from}g.1))v\mathrm{else}\mathrm{neg}(act0(Fin.val(\mathrm{show}\mathrm{Fin}6\mathrm{from}g.1))v)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.act (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.6 (norm).

$$\forall (K:\mathrm{Type})[\mathrm{AddCommMonoid}K](F:\mathrm{Exp}\to K)(v:\mathrm{Exp}),\mathrm{norm}Fv=\sum g:(\mathrm{ZMod}6\times \mathrm{ZMod}2),F(\mathrm{act}gv)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.norm (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Theorem 1.7 (norm_act).

$$\forall (K:\mathrm{Type})[\mathrm{AddCommMonoid}K](F:\mathrm{Exp}\to K)(v:\mathrm{Exp})(h:(\mathrm{ZMod}6\times \mathrm{ZMod}2)),\mathrm{norm}F(\mathrm{act}hv)=\mathrm{norm}Fv$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.8 (Poly).

$$\mathrm{Poly}:\mathrm{Type}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.Poly (✓ std3).

Source. Repository-derived.

Commentary.

The constructor fields are | tip : (Exp × Int) → Poly | node : Nat → Poly → Poly → Poly.

Definition 1.9 (size).

$$(\forall (field0:\mathrm{Exp}\times \mathrm{Int}),\mathrm{size}(Poly.tipfield0)=1)\wedge (\forall (n:\mathrm{Nat})(field1:\mathrm{Poly})(r:\mathrm{Poly}),\mathrm{size}(Poly.nodenfield1r)=n+\mathrm{size}r)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.size (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.10 (valid).

$$(\forall (field0:\mathrm{Exp}\times \mathrm{Int}),\mathrm{valid}(Poly.tipfield0)=\mathrm{true})\wedge (\forall (n:\mathrm{Nat})(l:\mathrm{Poly})(r:\mathrm{Poly}),\mathrm{valid}(Poly.nodenlr)=Bool.and(Bool.and(\mathrm{decide}(n=\mathrm{size}l))(\mathrm{valid}l))(\mathrm{valid}r))$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.valid (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.11 (lookup).

$$(\forall (t:\mathrm{Exp}\times \mathrm{Int})(i:\mathrm{Nat}),\mathrm{lookup}(Poly.tipt)i=t)\wedge (\forall (n:\mathrm{Nat})(l:\mathrm{Poly})(r:\mathrm{Poly})(i:\mathrm{Nat}),\mathrm{lookup}(Poly.nodenlr)i=\mathrm{if}i<n\mathrm{then}\mathrm{lookup}li\mathrm{else}\mathrm{lookup}r(i-n))$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.lookup (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.12 (sumValues).

$$(\forall (K:\mathrm{Type})[\mathrm{AddCommMonoid}K],\forall (F:(\mathrm{Exp}\times \mathrm{Int})\to K)(t:\mathrm{Exp}\times \mathrm{Int}),\mathrm{sumValues}F(Poly.tipt)=Ft)\wedge (\forall (K:\mathrm{Type})[\mathrm{AddCommMonoid}K],\forall (F:(\mathrm{Exp}\times \mathrm{Int})\to K)(field0:\mathrm{Nat})(l:\mathrm{Poly})(r:\mathrm{Poly}),\mathrm{sumValues}F(Poly.nodefield0lr)=\mathrm{sumValues}Fl+\mathrm{sumValues}Fr)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.sumValues (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Theorem 1.13 (indexed_sum).

$$\forall (K:\mathrm{Type})[\mathrm{AddCommMonoid}K](F:(\mathrm{Exp}\times \mathrm{Int})\to K)(p:\mathrm{Poly}),(\mathrm{valid}p=\mathrm{true})\to ((\sum i\in Finset.range(\mathrm{size}p),F(\mathrm{lookup}pi))=\mathrm{sumValues}Fp)$$

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

Source. Repository-derived.

Commentary.

For a valid polynomial tree, indexed lookup visits every leaf exactly once, so its indexed sum equals recursive evaluation. The proof follows the tree decomposition.

Definition 1.14 (mulTerm).

$$\forall (t:(\mathrm{Exp}\times \mathrm{Int}))(u:(\mathrm{Exp}\times \mathrm{Int})),\mathrm{mulTerm}tu=(\mathrm{plus}t.1u.1,t.2\cdot u.2)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.mulTerm (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.15 (evalPoly).

$$\forall (K:\mathrm{Type})[\mathrm{CommRing}K](F:\mathrm{Exp}\to K)(p:\mathrm{Poly}),\mathrm{evalPoly}Fp=\mathrm{sumValues}(\mathrm{fun}t\mapsto (t.2:K)\cdot Ft.1)p$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.evalPoly (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.16 (Tree).

$$\mathrm{Tree}:\mathrm{Type}\to \mathrm{Type}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.Tree (✓ std3).

Source. Repository-derived.

Commentary.

The constructor fields are | tip : Nat → α → Tree α | node : Nat → Tree α → Tree α → Tree α.

Definition 1.17 (low).

$$(\forall (\alpha :\mathrm{Type}),\forall (i:\mathrm{Nat})(field1:\alpha ),\mathrm{low}(Tree.tipifield1)=i)\wedge (\forall (\alpha :\mathrm{Type}),\forall (\mathrm{lo}:\mathrm{Nat})(field1:\mathrm{Tree}\alpha )(field2:\mathrm{Tree}\alpha ),\mathrm{low}(Tree.node\mathrm{lo}field1field2)=\mathrm{lo})$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.low (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.18 (indexValid).

$$(\forall (\alpha :\mathrm{Type}),\forall (field0:\mathrm{Nat})(field1:\alpha ),\mathrm{indexValid}(Tree.tipfield0field1)=\mathrm{true})\wedge (\forall (\alpha :\mathrm{Type}),\forall (\mathrm{lo}:\mathrm{Nat})(l:\mathrm{Tree}\alpha )(r:\mathrm{Tree}\alpha ),\mathrm{indexValid}(Tree.node\mathrm{lo}lr)=Bool.and(Bool.and(\mathrm{decide}(\mathrm{lo}\le \mathrm{low}l\wedge \mathrm{lo}\le \mathrm{low}r))(\mathrm{indexValid}l))(\mathrm{indexValid}r))$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.indexValid (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.19 (mask).

$$(\forall (\alpha :\mathrm{Type}),\forall (field0:\mathrm{Nat})(field1:\alpha ),\mathrm{mask}(Tree.tipfield0field1)=1)\wedge (\forall (\alpha :\mathrm{Type}),\forall (\mathrm{lo}:\mathrm{Nat})(l:\mathrm{Tree}\alpha )(r:\mathrm{Tree}\alpha ),\mathrm{mask}(Tree.node\mathrm{lo}lr)=Nat.lor((Nat.shiftLeft(\mathrm{mask}l)((\mathrm{low}l-\mathrm{lo}))))((Nat.shiftLeft(\mathrm{mask}r)((\mathrm{low}r-\mathrm{lo})))))$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.mask (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.20 (leaves).

$$(\forall (\alpha :\mathrm{Type}),\forall (i:\mathrm{Nat})(field1:\alpha ),\mathrm{leaves}(Tree.tipifield1)=[i])\wedge (\forall (\alpha :\mathrm{Type}),\forall (field0:\mathrm{Nat})(l:\mathrm{Tree}\alpha )(r:\mathrm{Tree}\alpha ),\mathrm{leaves}(Tree.nodefield0lr)=List.append(\mathrm{leaves}l)(\mathrm{leaves}r))$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.leaves (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.21 (count).

$$(\forall (\alpha :\mathrm{Type}),\forall (field0:\mathrm{Nat})(field1:\alpha ),\mathrm{count}(Tree.tipfield0field1)=1)\wedge (\forall (\alpha :\mathrm{Type}),\forall (field0:\mathrm{Nat})(l:\mathrm{Tree}\alpha )(r:\mathrm{Tree}\alpha ),\mathrm{count}(Tree.nodefield0lr)=\mathrm{count}l+\mathrm{count}r)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.count (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.22 (groupOfNat).

$$\forall (n:\mathrm{Nat}),\mathrm{groupOfNat}n=((Nat.cast(Nat.modn6):\mathrm{ZMod}6),(Nat.cast(Nat.div(n)6):\mathrm{ZMod}2))$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.groupOfNat (✓ std3).

Source. Repository-derived.

Commentary.

Division n/6 is the natural-number quotient, and n%6 is the natural-number remainder. The remainder is cast to ZMod 6, and the quotient is cast to ZMod 2; these are the two finite group coordinates.

Definition 1.23 (zeroExp).

$$\mathrm{zeroExp}=⟨0,0,0,0,0,0⟩$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.zeroExp (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.24 (checkInc).

$$(\forall (\mathrm{src}:\mathrm{Nat}\to (\mathrm{Exp}\times \mathrm{Int}))(\mathrm{rep}:\mathrm{Exp})(i:\mathrm{Nat})(g:\mathrm{Nat}),\mathrm{checkInc}\mathrm{src}\mathrm{rep}(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree.tipig)=\mathrm{decide}(\mathrm{act}(\mathrm{groupOfNat}g)(\mathrm{src}i).1=\mathrm{rep}))\wedge (\forall (\mathrm{src}:\mathrm{Nat}\to (\mathrm{Exp}\times \mathrm{Int}))(\mathrm{rep}:\mathrm{Exp})(field0:\mathrm{Nat})(l:(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat}))(r:(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat})),\mathrm{checkInc}\mathrm{src}\mathrm{rep}(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree.nodefield0lr)=Bool.and(\mathrm{checkInc}\mathrm{src}\mathrm{rep}l)(\mathrm{checkInc}\mathrm{src}\mathrm{rep}r))$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.checkInc (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.25 (coefficientSum).

$$(\forall (\mathrm{src}:\mathrm{Nat}\to (\mathrm{Exp}\times \mathrm{Int}))(i:\mathrm{Nat})(field1:\mathrm{Nat}),\mathrm{coefficientSum}\mathrm{src}(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree.tipifield1)=(\mathrm{src}i).2)\wedge (\forall (\mathrm{src}:\mathrm{Nat}\to (\mathrm{Exp}\times \mathrm{Int}))(field0:\mathrm{Nat})(l:(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat}))(r:(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat})),\mathrm{coefficientSum}\mathrm{src}(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree.nodefield0lr)=\mathrm{coefficientSum}\mathrm{src}l+\mathrm{coefficientSum}\mathrm{src}r)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.coefficientSum (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.26 (evalInc).

$$(\forall (K:\mathrm{Type})[\mathrm{CommRing}K],\forall (F:\mathrm{Exp}\to K)(\mathrm{src}:\mathrm{Nat}\to (\mathrm{Exp}\times \mathrm{Int}))(i:\mathrm{Nat})(field1:\mathrm{Nat}),\mathrm{evalInc}F\mathrm{src}(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree.tipifield1)=((\mathrm{src}i).2:K)\cdot \mathrm{norm}F(\mathrm{src}i).1)\wedge (\forall (K:\mathrm{Type})[\mathrm{CommRing}K],\forall (F:\mathrm{Exp}\to K)(\mathrm{src}:\mathrm{Nat}\to (\mathrm{Exp}\times \mathrm{Int}))(field0:\mathrm{Nat})(l:(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat}))(r:(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat})),\mathrm{evalInc}F\mathrm{src}(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree.nodefield0lr)=\mathrm{evalInc}F\mathrm{src}l+\mathrm{evalInc}F\mathrm{src}r)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.evalInc (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.27 (Rows).

$$\mathrm{Rows}:\mathrm{Type}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.Rows (✓ std3).

Source. Repository-derived.

Commentary.

The constructor fields are | row : Exp → Int → (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree Nat) → Rows | node : Nat → Rows → Rows → Rows.

Definition 1.28 (ids).

$$(\forall (field0:\mathrm{Exp})(field1:\mathrm{Int})(t:D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat}),\mathrm{ids}(Rows.rowfield0field1t)=t)\wedge (\forall (\mathrm{lo}:\mathrm{Nat})(l:\mathrm{Rows})(r:\mathrm{Rows}),\mathrm{ids}(Rows.node\mathrm{lo}lr)=D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree.node\mathrm{lo}(\mathrm{ids}l)(\mathrm{ids}r))$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.ids (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.29 (rowCheck).

$$(\forall (\mathrm{src}:\mathrm{Nat}\to (\mathrm{Exp}\times \mathrm{Int}))(\mathrm{rep}:\mathrm{Exp})(\mathrm{expected}:\mathrm{Int})(t:D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat}),\mathrm{rowCheck}\mathrm{src}(Rows.row\mathrm{rep}\mathrm{expected}t)=Bool.and(\mathrm{checkInc}\mathrm{src}\mathrm{rep}t)(\mathrm{decide}(\mathrm{coefficientSum}\mathrm{src}t=\mathrm{expected})))\wedge (\forall (\mathrm{src}:\mathrm{Nat}\to (\mathrm{Exp}\times \mathrm{Int}))(field0:\mathrm{Nat})(l:\mathrm{Rows})(r:\mathrm{Rows}),\mathrm{rowCheck}\mathrm{src}(Rows.nodefield0lr)=Bool.and(\mathrm{rowCheck}\mathrm{src}l)(\mathrm{rowCheck}\mathrm{src}r))$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.rowCheck (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Theorem 1.30 (combine_checked).

$$\forall (\mathrm{src}:\mathrm{Nat}\to (\mathrm{Exp}\times \mathrm{Int}))(\mathrm{lo}:\mathrm{Nat})(l:\mathrm{Rows})(r:\mathrm{Rows}),(\mathrm{rowCheck}\mathrm{src}l=\mathrm{true})\to ((\mathrm{rowCheck}\mathrm{src}r=\mathrm{true})\to (\mathrm{rowCheck}\mathrm{src}(Rows.node\mathrm{lo}lr)=\mathrm{true}))$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.31 (targetCheck).

$$(\forall (\mathrm{rep}:\mathrm{Exp})(\mathrm{expected}:\mathrm{Int})(field2:D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat}),\mathrm{targetCheck}(Rows.row\mathrm{rep}\mathrm{expected}field2)=\mathrm{decide}(\mathrm{expected}=0\vee \mathrm{rep}=\mathrm{zeroExp}))\wedge (\forall (field0:\mathrm{Nat})(l:\mathrm{Rows})(r:\mathrm{Rows}),\mathrm{targetCheck}(Rows.nodefield0lr)=Bool.and(\mathrm{targetCheck}l)(\mathrm{targetCheck}r))$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.targetCheck (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.32 (targetSum).

$$(\forall (field0:\mathrm{Exp})(\mathrm{expected}:\mathrm{Int})(field2:D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat}),\mathrm{targetSum}(Rows.rowfield0\mathrm{expected}field2)=\mathrm{expected})\wedge (\forall (field0:\mathrm{Nat})(l:\mathrm{Rows})(r:\mathrm{Rows}),\mathrm{targetSum}(Rows.nodefield0lr)=\mathrm{targetSum}l+\mathrm{targetSum}r)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.targetSum (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.33 (targetValue).

$$(\forall (K:\mathrm{Type})[\mathrm{CommRing}K],\forall (F:\mathrm{Exp}\to K)(\mathrm{rep}:\mathrm{Exp})(\mathrm{expected}:\mathrm{Int})(field2:D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat}),\mathrm{targetValue}F(Rows.row\mathrm{rep}\mathrm{expected}field2)=(\mathrm{expected}:K)\cdot \mathrm{norm}F\mathrm{rep})\wedge (\forall (K:\mathrm{Type})[\mathrm{CommRing}K],\forall (F:\mathrm{Exp}\to K)(field0:\mathrm{Nat})(l:\mathrm{Rows})(r:\mathrm{Rows}),\mathrm{targetValue}F(Rows.nodefield0lr)=\mathrm{targetValue}Fl+\mathrm{targetValue}Fr)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.targetValue (✓ std3).

Source. Repository-derived.

Commentary.

The operation is determined by these constructor equations. Type denotes an arbitrary universe. Division of natural numbers is integer quotient; Nat.mod is the remainder. Bool.and, Nat.lor, Nat.shiftLeft and Nat.shiftRight retain their Lean meanings.

Definition 1.34 (h0).

$$h0:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h0 (✓ 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.35 (p0).

$$p0:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p0 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are specified by the Lean definition.

Theorem 1.36 (hv0).

$$\mathrm{valid}h0=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.37 (pv0).

$$\mathrm{valid}p0=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.38 (h1).

$$h1:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h1 (✓ 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.39 (p1).

$$p1:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p1 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are specified by the Lean definition.

Theorem 1.40 (hv1).

$$\mathrm{valid}h1=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.41 (pv1).

$$\mathrm{valid}p1=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.42 (h2).

$$h2:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h2 (✓ 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 (p2).

$$p2:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p2 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are specified by the Lean definition.

Theorem 1.44 (hv2).

$$\mathrm{valid}h2=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.45 (pv2).

$$\mathrm{valid}p2=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.46 (h3).

$$h3:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h3 (✓ 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 (p3).

$$p3:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p3 (✓ 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.48 (hv3).

$$\mathrm{valid}h3=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.49 (pv3).

$$\mathrm{valid}p3=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.50 (h4).

$$h4:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h4 (✓ 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 (p4).

$$p4:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p4 (✓ std3).

Source. Repository-derived.

Commentary.

The fixed balanced certificate tree has the displayed type. Its leaf sequence and node boundaries are specified by the Lean definition.

Theorem 1.52 (hv4).

$$\mathrm{valid}h4=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.53 (pv4).

$$\mathrm{valid}p4=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.54 (h5).

$$h5:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h5 (✓ 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 (p5).

$$p5:\mathrm{Poly}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p5 (✓ 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.56 (hv5).

$$\mathrm{valid}h5=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.57 (pv5).

$$\mathrm{valid}p5=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.58 (source).

$$\forall (i:\mathrm{Nat}),\mathrm{source}i=\mathrm{if}i<29421\mathrm{then}\mathrm{mulTerm}(\mathrm{lookup}h0(Nat.div(i-0)21))(\mathrm{lookup}p0(Nat.mod((i-0))(21)))\mathrm{else}\mathrm{if}i<49308\mathrm{then}\mathrm{mulTerm}(\mathrm{lookup}h1(Nat.div(i-29421)21))(\mathrm{lookup}p1(Nat.mod((i-29421))(21)))\mathrm{else}\mathrm{if}i<59388\mathrm{then}\mathrm{mulTerm}(\mathrm{lookup}h2(Nat.div(i-49308)21))(\mathrm{lookup}p2(Nat.mod((i-49308))(21)))\mathrm{else}\mathrm{if}i<118080\mathrm{then}\mathrm{mulTerm}(\mathrm{lookup}h3(Nat.div(i-59388)67))(\mathrm{lookup}p3(Nat.mod((i-59388))(67)))\mathrm{else}\mathrm{if}i<142740\mathrm{then}\mathrm{mulTerm}(\mathrm{lookup}h4(Nat.div(i-118080)36))(\mathrm{lookup}p4(Nat.mod((i-118080))(36)))\mathrm{else}\mathrm{if}i<149736\mathrm{then}\mathrm{mulTerm}(\mathrm{lookup}h5(Nat.div(i-142740)66))(\mathrm{lookup}p5(Nat.mod((i-142740))(66)))\mathrm{else}(⟨0,0,0,0,0,0⟩,0)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.source (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation. Nat.div is the natural-number integer quotient; Nat.mod is the remainder.

Definition 1.59 (rows0).

$$rows0:\mathrm{Rows}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.rows0 (✓ 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.60 (expectedMask0).

$$expectedMask0:\mathrm{Nat}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.expectedMask0 (✓ 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.61 (rowChecked0).

$$\mathrm{rowCheck}\mathrm{source}rows0=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.62 (targetChecked0).

$$\mathrm{targetCheck}rows0=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.63 (idsValid0).

$$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.indexValid(\mathrm{ids}rows0)=\mathrm{true}$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.64 (maskChecked0).

$$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.mask(\mathrm{ids}rows0)=expectedMask0$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.65 (countChecked0).

$$D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.count(\mathrm{ids}rows0)=49940$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.66 (targetSum0).

$$\mathrm{targetSum}rows0=0$$

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

Source. Repository-derived.

Commentary.

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

Theorem 1.67 (char_star).

$$\forall (N:\mathbb{N})[\mathrm{NeZero}N](x:\mathrm{ZMod}N),\overline{ZMod.stdAddCharx}=ZMod.stdAddChar(-x)$$

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

Source. Repository-derived.

Commentary.

Complex conjugation negates the argument of the standard additive character.

Definition 1.68 (amplitude).

$$\forall (N:\mathbb{N})[\mathrm{NeZero}N](z:\mathrm{ZMod}N\to \mathbb{C})(a:\mathrm{ZMod}N)(b:\mathrm{ZMod}N),\mathrm{amplitude}zab=(N:\mathbb{C}{)}^{-1}\cdot ZMod.dftz(b-a)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.amplitude (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Theorem 1.69 (uniform_amplitude_iff_ratio).

$$\forall (N:\mathbb{N})[\mathrm{NeZero}N](z:\mathrm{ZMod}N\to \mathbb{C}),(\forall (j:\mathrm{ZMod}N),Complex.normSq(zj)=1)\to ((\forall (ab:\mathrm{ZMod}N),Complex.normSq(\mathrm{amplitude}zab)=1/(N:\mathbb{R}))⟺(\forall (l:\mathrm{ZMod}N),l\ne 0\to \sum j:\mathrm{ZMod}N,z(j+l)/zj=0))$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.70 (cycleA).

$$\forall (N:\mathbb{N})[\mathrm{NeZero}N],\mathrm{cycleA}=(D5.S3.Combinatorics.NarayanaStrip.CiglerCycleWalkFolding.cycleAdjN).\mathrm{map}(Int.castRingHom\mathbb{C})$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.cycleA (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Definition 1.71 (eigenvalue).

$$\forall (N:\mathbb{N})[\mathrm{NeZero}N](j:\mathrm{ZMod}N),\mathrm{eigenvalue}j=ZMod.stdAddCharj+ZMod.stdAddChar(-j)$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.eigenvalue (✓ std3).

Source. Repository-derived.

Commentary.

The displayed identity defines this operation.

Theorem 1.72 (exp_cycle_entry).

$$\forall (N:\mathbb{N})[\mathrm{NeZero}N](c:\mathbb{C})(a:\mathrm{ZMod}N)(b:\mathrm{ZMod}N),NormedSpace.exp(SMul.smul(c)(\mathrm{cycleA}))ab=(N:\mathbb{C}{)}^{-1}\cdot ZMod.dft(\mathrm{fun}j\mapsto Complex.exp(c\cdot \mathrm{eigenvalue}j))(b-a)$$

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

Source. Repository-derived.

Commentary.

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

Definition 1.73 (instDecidableEqExp).

$$\mathrm{instDecidableEqExp}:\mathrm{DecidableEq}\mathrm{Exp}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.instDecidableEqExp (✓ 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/OrbitIndexedSums.Exp
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.Poly
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.Rows
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.Tree
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.act
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.act0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.amplitude
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.char_star
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.checkInc
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.coefficientSum
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.combine_checked
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.count
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.countChecked0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.cycleA
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.eigenvalue
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.evalInc
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.evalPoly
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.exp_cycle_entry
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.expectedMask0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.groupOfNat
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h1
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h2
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h3
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h4
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.h5
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.hv0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.hv1
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.hv2
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.hv3
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.hv4
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.hv5
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.ids
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.idsValid0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.indexValid
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.indexed_sum
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.instDecidableEqExp
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.leaves
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.lookup
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.low
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.mask
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.maskChecked0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.mulTerm
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.neg
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.norm
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.norm_act
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p1
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p2
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p3
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p4
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.p5
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.plus
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.pv0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.pv1
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.pv2
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.pv3
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.pv4
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.pv5
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.rowCheck
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.rowChecked0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.rows0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.size
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.source
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.sumValues
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.targetCheck
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.targetChecked0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.targetSum
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.targetSum0
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.targetValue
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.uniform_amplitude_iff_ratio
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.valid
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIndexedSums.zeroExp
• Dependency: D5/S3/Combinatorics/NarayanaStrip/CiglerCycleWalkFolding
• Dependency: D5/S3/Quantum/QuantumChannels/TomiyamaDiagonalKPositivity