Morphism Iteration Bound Source Residues

This Blueprint mirror records the machine-checked source module.

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

• startState

• expandedPosition

• expandedPosition_succ

• indexedFixedWord_start

• fixedWord_zero

• source_transitions

• length_sum_mem

• equal_parameters_of_no_double

• d_mem_return

• Truth anchor: D5/S1/Words/RankOneMorphismIterationBoundSourceResidues