@SamHopkins thanks for doing that calculation! Indeed, the constant maps are maximal. More generally, if $f_1, f_2$ are such that the partition into $f_1$-fibers refines the partition into $f_2$-fibers, then there are at least as many factorizations of $f_2$ as of $f_1$. (Any $h$ that works for $f_2$ will work for $f_1$, and once you've picked $h$, say $|h(S)| = m$, you have $n^{n-m}$ choices for $g$, whether factoring $f_1$ or $f_2$.)

Certainly! But I think that it's not just the change in level of formality that matters -- the content of the informal description and of the formal definition matter as well. If the informal description was "if you use enough decimal places for $x$, your calculator will give pretty much the correct value of $f(x)$", then I would see the change to the $\varepsilon$-$\delta$ formulation as entirely an issue of precision and rigour. (I don't think you were saying that the only meaningful change was in the level of rigour, I'm just enjoying the conversation and thought I'd add this thought.)

You're right, it's not equivalent! However ... a high school student who was prepared to grapple with the base 13 function would already be way beyond the level of an intro lesson on the IVT! This is what I meant by "not quite what is being asked" -- mathematically, it's not equivalent, but pedagogically and historically, the shift in perspective feels similar to me. (The historical narrative is complicated by the work Bolzano, and the pedagogical one by [insert your favourite pedagogical complication].)

@BenjaminSteinberg Thanks for these comments! You're right about the transitivity. I have removed the other condition that I stated to prevent confusion. I've been reading your book, but my knowledge of modules is remedial at best, so I thought that while I work on that remediation, I'd see if phrasing the question in a slightly different way could dredge up any ideas that might be latent in the community. What I'm ultimately interested in is a potentially different proof of road colouring that might generalize to other, related problems more readily.

Update: I have it now, so if you send me an email, I am happy to send it you.

My university library has a copy. I'll be able to get a scan of it later this week; you can find my contact information on the homepage linked in my profile.

When $G$ is nilpotent and torsion-free, Breuillard-Le Donne characterize the limit as the volume of the unit ball of some space that would make sense if one knew some things that I don't. See the paragraph after Corollary 8.1 on page 15 in "On the rate of convergence to the asymptotic cone for nilpotent groups and subFinsler geometry", PNAS 110 (48) 2013 pp. 19220-19226, arxiv:1204.1613.

@BenjaminSteinberg ah, ok! Thank you, that's exactly the kind of thing that I needed to know.

@LSpice well, perhaps, but I wasn't deliberately obfuscating things. I am looking to re-prove an existing result (the Road Colouring Theorem) by new methods, and I have an idea of how to do it but don't know how to make a key step work. So I'm describing what I'm trying to do in that step, and what I don't about it, in the hope that someone more familiar with the relevant objects can offer ideas. If this makes sense and you have suggestions about a way to go about things, I would be glad to edit the question further to make it more appropriate.