Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Record Bounds and the Inverse Bijection

Abstract

Record maxima control prefixes and the inverse fundamental bijection is injective on distinct letters.

Theorem 1.1 (Bounds from the last record).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverse.last_record_bounds_prefix

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverse.last_record_bounds_prefix (✓ 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 every position i of a word, all entries through i are at most the value of the last left-to-right maximum through i.

Theorem 1.2 (Distinct cyclic successors).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverse.hat_inj_on

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverse.hat_inj_on (✓ 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 word with distinct letters, two letters in the word have the same cyclic successor only when they are equal.

References