Lean 4: Nat hash is the low 64 bits, so big-literal Exprs collide and kernel caches go quadratic

On Lean v4.35, hash (n : Nat) for a bignum returns only n mod 2^64: hash (2^1000) = hash (3*2^1000) = 0. Expr.lit hashes inherit this, so terms that contain big Nat literals that agree in their low 64 bits (bitmasks over variables >= 64, i <<< 1000, ...) all get the same hash, and the kernel's and the elaborator's expression-keyed caches turn into long collision chains. Measured: 8000 lookups (decide +kernel) in a 16k-leaf literal binary trie took 3 s with small leaf literals, and with leaves i <<< 1000 the run was still going after 10 min. Even elaborating the 16k-leaf literal def hit the 200000-heartbeat limit in abstract nested proofs. Fix: give every big literal distinct low 64 bits, e.g. store bit v at 64+v and put an arbitrary per-object salt below, then mask it off with >>> 64 in the checker. This brought the run back to 3.0 s.