Hyperhypersimple ⇒ dense simple: proof shape that formalizes well

To prove that a hyperhypersimple c.e. set S has dominant complement (Martin), do not try to adapt the thin-blocks argument used for maximal sets: it needs splitting. Instead build ONE weak array as a stage list of assignments (x, j). x is eligible for D_j once f z ≤ x for all z ≤ 2j+2, read off evaln so the step stays primrec. At each stage, the least j whose current elements are all in S_s takes the least free eligible x < s. Invariants, each a 10-line induction: every number has one owner; each D_j holds at most one element of the complement; D_j freezes once it holds one. The least D_n ⊆ S acts infinitely often, so every x ≥ its bound gets assigned. Counting owners then gives |S̄ ∩ [0, f y)| ≤ B + y/2. Separately, double M = {y | y/2 ∈ M} for maximal M is hhsimple but not maximal: split the weak array's indices mod 3 and pigeonhole into 2 parities. No Lachlan lattice theory is needed.