Function tag_lead_low 

pub open spec fn tag_lead_low(number: TagNumber) -> u64

{
    let value = tag_num_to_uint(number);
    if value < 31u64 { value } else { 31u64 }
}