OrbitIncidenceChecker

Abstract

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

Theorem 1.1 (checked_inc).

$$\forall (K:\mathrm{Type})[\mathrm{CommRing}K](F:D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Exp\to K)(\mathrm{src}:\mathrm{Nat}\to (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Exp\times \mathrm{Int}))(\mathrm{rep}:D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Exp)(t:(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Index.Tree\mathrm{Nat})),(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.checkInc\mathrm{src}\mathrm{rep}t=\mathrm{true})\to (D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.evalIncF\mathrm{src}t=(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.coefficientSum\mathrm{src}t:K)\cdot D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.normF\mathrm{rep})$$

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

Source. Repository-derived.

Commentary.

Every accepted incidence tree evaluates to its total coefficient times the orbit sum of its representative. Node composition preserves this equality.

Definition 1.2 (certificateScalar).

$$\mathrm{certificateScalar}:\mathrm{Nat}$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIncidenceChecker.certificateScalar (✓ std3).

Source. Repository-derived.

Commentary.

The fixed natural scalar in the integer Laurent certificate has the displayed type. Its value is specified by the Lean definition.

Theorem 1.3 (identity).

$$\forall (K:\mathrm{Type})[\mathrm{CommRing}K](F:D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Exp\to K),((List.range149736).\mathrm{map}(\mathrm{fun}i\mapsto ((D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.sourcei).2:K)\cdot D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.normF(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Data.sourcei).1)).\mathrm{sum}=(\mathrm{certificateScalar}:K)\cdot D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.normFD5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.zeroExp$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIncidenceChecker.identity (✓ 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/OrbitIncidenceChecker.certificateScalar
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIncidenceChecker.checked_inc
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIncidenceChecker.identity
• Dependency: D5/S3/Quantum/Dynamics/CycleUniformMixing/SupportMaskChecker