[Tier 1 SSZ] SSZ-2: Prove Uint64 value range

[adust09]

Catalog entry

docs/lean4-proof-propositions.md lines 75-83:

SSZ-2: A Uint64 value lies in [0, 2^64)

• Source: Uint64 (type definition)

theorem uint64_range (v : Uint64) :
    v.toNat < 2 ^ 64 := by sorry

Goal

Commit the theorem:

theorem uint64_range (v : Uint64) : v.toNat < 2 ^ 64

Implementation notes

• The Lean type Uint64 is defined in LeanSpec/Types/Uint.lean:37 as structure Uint64 where val : UInt64. The catalog uses v.toNat, which is not yet defined on the wrapper.
• Add a toNat accessor on Uint8/16/32/64 in LeanSpec/Types/Uint.lean (consistent set across all four widths to avoid one-off divergence later):

  namespace Uint64
  @[inline] def toNat (v : Uint64) : Nat := v.val.toNat
  end Uint64

• Prove uint64_range using UInt64.toNat_lt (the exact lemma name should be confirmed by reading Init.Data.UInt.Basic at implementation time; an equivalent lemma like UInt64.toFin_lt may apply).
• Place the new theorem in LeanSpec/Theorems/Uint.lean, alongside the existing length_law_Uint64 and encode_decode_Uint8.
• Update docs/lean4-proof-propositions.md: replace the sorry stub with a pointer such as ✅ proved in `LeanSpec/Theorems/Uint.lean` as `uint64_range`. Bump the frontmatter last_updated.

Acceptance criteria

• lake build succeeds.
• grep -n "sorry\|axiom" LeanSpec/Theorems/Uint.lean returns nothing.
• docs/lean4-proof-propositions.md SSZ-2 entry updated; frontmatter last_updated bumped.
• No Mathlib dependency introduced.

[adust09]

Status: SSZ-2 was proved and merged in PR #19 — LeanSpec/SSZ/Uint64.lean has Uint64.range, and the catalog entry is checked off with the proved-at pointer. Layout note: the repo settled on one-file-per-concept under LeanSpec/SSZ/ (no LeanSpec/Types/ / LeanSpec/Theorems/ split), and Uint64 is abbrev Uint64 := UInt64, so toNat comes from core and the proof is UInt64.toNat_lt. All acceptance criteria are met under that layout — this issue can be closed as completed.