Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Marked cuts and parity profiles

Abstract

Marked cycle partitions yield exact parity-profile cardinalities.

The first count agrees with the denominator-cleared form of source Lemma 3.5 on its stated range. The formal proof also covers m equals zero and all vanishing support cases. The other statements justify the actual block and parity bookkeeping.

Theorem 1.1 (The marked parity-profile count).

Lean statement: D5/S3/Combinatorics/Geometry/CrownOrderPolytopeMarkedCuts.card_prescribedOddConnectedCyclePartition_identity

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/CrownOrderPolytopeMarkedCuts.card_prescribedOddConnectedCyclePartition_identity (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Teemu Lundström and Leonardo Saud Maia Leite (2025). Order polytopes of crown posets. DOI: 10.48550/arXiv.2504.05123. URL: https://arxiv.org/abs/2504.05123v3.

Commentary.

For n at least two and i at least two, multiplying the number of connected partitions of the 2n-cycle into i blocks with 2m odd blocks by i gives 2n times choose(i,2m) times choose(n+m-1,i-1). The factor i counts markings; all natural support cases are included.

In the profile construction, the sum of the actual fiber cardinalities is the even cycle size. The library parity-of-sum equivalence therefore makes the number of odd blocks even and allows profiles to be indexed by 2m.

Theorem 1.2 (Cuts count the actual quotient blocks).

Lean statement: D5/S3/Combinatorics/Geometry/CrownOrderPolytopeMarkedCuts.quotient_card_eq_boundaryCuts_card

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/CrownOrderPolytopeMarkedCuts.quotient_card_eq_boundaryCuts_card (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Teemu Lundström and Leonardo Saud Maia Leite (2025). Order polytopes of crown posets. DOI: 10.48550/arXiv.2504.05123. URL: https://arxiv.org/abs/2504.05123v3.

Commentary.

For a cycle of size at least three with at least two boundary cuts, the actual quotient cardinality equals the cardinality of the boundary-cut set.

References