Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Morphism Iteration Bound Fixed Word

This Blueprint mirror records the machine-checked source module.

Formalization. D5/S1/Words/RankOneMorphismIterationBoundFixedWord (✓ 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

  • factor_append

  • factor_take

  • image_prefix_succ

  • image_prefix

  • image_growth

  • fixedWord

  • fixedWord_eq_image

  • fixedWord_prefix

  • fixedWord_semantics

  • fixedWord_unique

  • height

  • height_add

  • fixedWord_height_range

  • fixedWord_height_finite

  • uap_of_height_ray

  • height_ray_of_uap

  • Truth anchor: D5/S1/Words/RankOneMorphismIterationBoundFixedWord