Std.Natural

"value < 256^byteCount" WITHOUT ever building 256^byteCount: divide by 256 byteCount times and ask whether anything is left. A runtime natural costs about 164 bytes and 300 ns PER UNIT of its magnitude (measured 2026-09-16: 2^20 takes 0.8 s and 195 MB, 2^24 takes 5 s and 2.75 GB, and 2^32 cannot be built at all -- the image exits 125). So a bound such as 2^32 must never be materialised, and `naturalLess x (naturalPowerOfTwo 32)` is not a comparison but an out-of-memory. This is how "fits in a 32-bit field" is asked instead; it costs about value/256 steps.

224def naturalBelowBytePower =
225  (lambda unrestricted byteCount : Nat .
226    (lambda unrestricted value : Nat .
227      (naturalIsZero
228        (nat-eliminate
229          (lambda unrestricted current : Nat . Nat)
230          value
231          (lambda unrestricted predecessor : Nat .
232            (lambda unrestricted quotient : Nat .
233              (naturalDivideUnchecked quotient naturalTwoHundredFiftySix)))
234          byteCount))))