Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Morphism Iteration Bound Defs

This Blueprint mirror records the machine-checked source module.

Formalization. D5/S1/Words/RankOneMorphismIterationBoundDefs (✓ std3).

Source. Repository-derived.

Commentary.

The module provides the finite-state and word-combinatorial suppliers used by D5/S1/Words/RankOneMorphismIterationBound.effective_iteration_bound. Its declarations are kernel-checked in the actual binary rank-one morphism setting; no proxy fixed word or frequency-only replacement is used.

Declarations

  • Letter

  • Word

  • Morphism

  • parikh

  • subst

  • image

  • Nonerasing

  • Prolongable

  • Primitive

  • RankOne

  • AbelianEq

  • Blocks

  • OriginalCyclicBlockWitness

  • UltimatelyAbelianPeriodic

  • IsFixedWord

  • iterationBound

  • parikh_binary_length

  • abelianEq_length

  • parikh_subst

  • subst_image_commute

  • image_add

  • Parameters

  • d

  • lam

  • mult

  • charge

  • d_pos

  • lam_ge_two

  • image_length

  • charge_eq_iff

  • Truth anchor: D5/S1/Words/RankOneMorphismIterationBoundDefs