Marked prime words and divisor snapshots
Abstract
Prime words over a strict divisor snapshot.
Theorem 1.1 (Splitting into successive quotient words).
Lean statement: D5/S3/Factorization/Combinatorics/MarkedPrimeWordSnapshotFiber.snapshot_fiber_equiv_and_forced_marks
Proof. Machine-checked in Lean as D5/S3/Factorization/Combinatorics/MarkedPrimeWordSnapshotFiber.snapshot_fiber_equiv_and_forced_marks (✓ std3). ∎
Source. Repository-derived.
Commentary.
Fix a strict divisor chain from one to an integer greater than one. A prime word together with marks realizing its prefix products is equivalent to a family of prime words, one for each successive quotient of the chain. Splitting at the marks gives the family; concatenation reconstructs the word. Each mark is forced to equal the total prime multiplicity of its observed divisor.