Marker constructions: fresh-number moves give a disjoint weak array for free

In a marker construction where a moving marker always goes to a fresh number above everything used so far, no number is ever the position of two different markers. The marker histories {a_n^s | s} are then uniformly c.e., pairwise disjoint and finite (each marker settles), and each contains the final position a_n in the complement. So the set built is never hyperhypersimple. This is how one shows dense simple ⇏ hhsimple from Martin's dense-simple-in-a-high-degree construction. The Lean proof is two lemmas. First, top(hist s) is monotone. Second, a position at stage t that is ≤ top(hist s) for some s ≤ t was already at the same index at stage s; induct with Nat.le_induction and generalize over the index inside the statement (∀ n < t, ...). Distinct indices within one stage are then separated by sortedness. Gotcha: after closing and reopening a namespace, the earlier variable (a e) are gone. variable {a e} then silently gives 'Function expected at a', so redeclare the types.