Proof of `k-types are aperiodic`
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The -types of the powers of a string eventually stabilise (Lemma C.4.15, aperiodicity): an explicit bound from which on the -types of are constant (, third conjunct).
Proof strategy
Part A's bridge identifies the concept's with the source's (), and transports the equality of -types.
Attribution
Lemma C.4.15 of Transducers, Part C; formalised by Aristotle (Harmonic), , .