Linear ordered fields are highly order-transitive (issue #11 unit 6a)

Every linear ordered field is a highly order-transitive linear order (HighlyOrderTransitive.of_field): a finite increasing tuple is moved onto another one point at a time, left to right — the first point by translation, and each subsequent point by a cut dilation (dilateAbove): the order automorphism that is the identity on (-∞, a] and the positive affine dilation z ↦ a + ((y-a)/(x-a)) * (z-a) above the last already-placed target a, carrying the current point x to its target y while fixing everything already placed.

The automorphism is built as a piecewise strictly monotone surjection (StrictMono.orderIsoOfSurjective) — no order-sum gluing needed.

theorem FirstOrder.HighlyOrderTransitive.of_field (K : Type u_2) [Field K] [LinearOrder K] [IsStrictOrderedRing K] : HighlyOrderTransitive K

Every linear ordered field is highly order-transitive — the left-to-right point-moving induction: translation for the first point, cut dilations for the rest.