The strict coefficient deficit outside cyclic arcs

Abstract

The strict coefficient deficit outside cyclic arcs

Theorem 1.1 (strict_coefficient_non_arc).

$$\forall m\in \mathbb{N},(1\le m)\Rightarrow (\forall x\in \mathrm{Stationing}\left(2\cdot m\right),(\neg (\mathrm{isArc}\left(m,x\right)))\Rightarrow (|\mathrm{psi}\left(m,x\right)|<(K\left(m\right):\mathbb{Z})))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/SpinChains/HKNNBlockBlochLargestWeight/ArcCoefficients.strict_coefficient_non_arc (✓ std3). ∎

Source. Repository-derived.

Commentary.

A balanced cyclic binary word outside the block orbit contains alternating down-up-down-up sites or the complementary pattern. The prescribed partner swap supplies opposite signs. Unbalanced configurations have zero coefficient, and K is positive.

References

• Truth anchor: D5/S3/Quantum/SpinChains/HKNNBlockBlochLargestWeight/ArcCoefficients.strict_coefficient_non_arc
• Dependency: D5/S1/Phase/SeatTowerCombinatorics
• Dependency: D5/S3/Quantum/SpinChains/HKNNBlockBlochLargestWeight/PairingCoefficients
• Dependency: D5/S3/Zeros/Convolution/PerfectMatchingCount