Incompatible Middle Cycle Data

Abstract

The prescribed cycle edges cannot satisfy the terminal return condition.

Theorem 1.1 (A middle-cycle contradiction).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Middle.middle_cycle_conflict

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Middle.middle_cycle_conflict (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kassie Archer, Robert P. Laudone (2024). Pattern avoidance and the fundamental bijection. DOI: 10.48550/arXiv.2407.06338. URL: https://arxiv.org/abs/2407.06338v1.

Commentary.

For a permutation q of size n at least four and an integer c from two through n minus two, q cannot have n and one at consecutive positions c minus one and c, end with n minus one, and have its second inverse image end with c.

References

• Truth anchor: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Middle.middle_cycle_conflict
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverse