Lax314295.KTypesAperiodicity

k-types are aperiodic

concepts/Lax314295/KTypesAperiodicity.lean · lax-314295

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax314295.KTypesAperiodicity

⊢Lax314295Proofs.Results.exists_tp_npow_eq

In the paper

page 133 of the paper of lax-157538, Transducers

Theorem

For every string $w$ and every $k$ , the $k$ -types of the powers $w, w^2, w^3, \ldots$ eventually stabilise (Lemma C.4.15 of Transducers, aperiodicity): all sufficiently large powers of a string have the same $k$ -type. This is what makes the automaton of $k$ -types aperiodic.

Lean source view on GitHub

1	import Lax765601.Aperiodicity
2	import Lax314295.KTypes
3
4	/-!
5	---
6	title: k-types are aperiodic
7	type: theorem
8	---
9	For every string $w$ and every $k$ , the $k$ -types of the powers
10	$w, w^2, w^3, \ldots$ eventually stabilise (Lemma C.4.15 of Transducers,
11	aperiodicity): all sufficiently large powers of a string have the same
12	$k$ -type. This is what makes the automaton of $k$ -types aperiodic.
13
14	# Formalization notes
15
16	`npow w n` is `wⁿ`, from `Lax765601.Aperiodicity`. Stated over any alphabet.
17	-/
18
19	namespace Lax314295.KTypesAperiodicity
20
21	open Lax765601.Aperiodicity Lax314295.KTypes
22
23	/-- The `k`-types of the powers of a string eventually stabilise. -/
24	axiom exists_tp_npow_eq {A : Type} (k : ℕ) (w : List A) :
25	∃ N : ℕ, ∀ n ≥ N, tp k (npow w n) = tp k (npow w N)
26
27	end Lax314295.KTypesAperiodicity
28

Show Proof

Formalization notes

$npow w n$ is $wⁿ$ , from $Lax765601.Aperiodicity$ . Stated over any alphabet.

Builds on

Used by

none

From Mathlib

none

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive