Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Refinement and recognizability of factorial tilings

Abstract

Refinement and recognizability of factorial tilings.

Definition 1.1 (Construction).

Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialRefinement.factorialSubshift

Formalization. D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialRefinement.factorialSubshift (✓ std3).

Source. Repository-derived.

Commentary.

Each upper block is refined into its actual repeated lower blocks. On the lower block types, the marker 10 occurs exactly at the upper boundaries. Induction from the one-letter level gives unique marked decoding at every level. The descending compact tiling subshifts have a nonempty intersection; this actual closed shift-invariant intersection defines the base.

Theorem 1.2 (Result).

Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialRefinement.readTiling_injective

Proof. Machine-checked in Lean as D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialRefinement.readTiling_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each upper block is refined into its actual repeated lower blocks. On the lower block types, the marker 10 occurs exactly at the upper boundaries. Induction from the one-letter level gives unique marked decoding at every level. The descending compact tiling subshifts have a nonempty intersection; this actual closed shift-invariant intersection defines the base.

References