The source computes every letter of the child configuration graph by a rational function: each of its finitely many components — the fixed pebbles, the first child in the column, and the outgoing and incoming edges of every state — is a regular property of the input marked at the gap, decided by the regular languages of Claim D.2.3 ($PartD/CGLang.lean$, $PartD/CGAtom.lean$, $PartD/CGSem.lean$), and a rational function is a for-transducer by Theorem D.1.1. The concept's letters form a distinct structure from the source's; the source's for-transducer is post-composed with the letter-to-letter bijection $cgLetterOfSrc$, itself a for-transducer ($isForTransducer_map$), and the two representations agree under the bijection ($cgOfChildren_toSrc$).

Claim D.2.6 of Transducers, Part D; formalised by Aristotle (Harmonic), $PartD/CGFor.lean$.