For L_K=2*sum(j<K,1/((2j+1)*3^(2j+1))), every finite extension increment lies in [0,9^-K]; construct a fixed compatible sequence from these bounds.
Method: native-induction. Induction: finite extension length. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.