Rational labels for a finite alphabet

The reduction in Section 1.1, used in Section 6 to prove Theorem 1.1 (thm:main). exists_rational_model preserves all pattern counts and all individual periods.

noncomputable def Nivat.rationalLabel (A : Type u_1) [Finite A] : A ↪ ℚ

An injective rational labeling of a finite alphabet (Section 1.1).

Equations

• Nivat.rationalLabel A = { toFun := fun (a : A) => ↑↑((Fintype.equivFin A) a), inj' := ⋯ }

theorem Nivat.exists_rational_model {A : Type u_1} [Finite A] (c : Configuration A) : ∃ (d : Configuration ℚ), FiniteRange d ∧ (∀ (D : Finset Lattice), complexity d D = complexity c D) ∧ ∀ (h : Lattice), IsPeriod d h ↔ IsPeriod c h

The rational alphabet reduction in Section 1.1 and the proof of Theorem 1.1 in Section 6: the labeling preserves every pattern count and every period vector.