Thanks for this very interesting implementation.

Just one remark on how to implement the less-than type LT without a circular reference to Subtract. A simple recycling of your Subtract idea does the job (I restrict myself to the core idea, so I leave out typechecking for natural numbers which can be added trivially with the help of your AreValid type):

type LT<Small extends number, Big extends number> =

BuildTuple<Big> extends [...BuildTuple<Small>, ...any[]]

? true

: false

Compare this to your own implementation of Subtract (parameters renamed)

type Subtract<Big extends number, Small extends number> =

BuildTuple<Big> extends [...(infer Difference), ...BuildTuple<Small>]

? Length<Difference>

: never;

Just, rather than to infer the difference as in your Subtract, simply check whether there is ANY (natural number) difference.