Clean up section on translated cyclers

[int-y1]

Big changes:

• Algorithm 3: Change "abs(offset) $<$ distanceL" to "abs(offset) $\leq$ distanceL". The old version looks incorrect.
• Algorithm 3: Change a condition to "(...).value != (...).value". Also add \newline to make the line look nicer.

Smaller changes:

• Section 3 intro: Remove the link to #59,090,563 because Figure 3 already has a link to #59,090,563.
• Lemma 3.3: The "Furthermore" sentence seems out of place in the lemma statement. I moved this sentence to the proof.
• Improve spelling / grammar / clarity.

[UncombedCoconut]

Thumbs up from me.

[tcosmo]

Looks great, thank you for your work!