fix: align Lean justifiability overflow semantics

[ss1738]

Context

While extending the existing justifiability formalization, I found a
fixed-width arithmetic boundary outside the current proof domain.

For delta = 2^62 + 2, the previous Lean implementation returned true
because UInt64 wrapping reduced 4 * delta + 1 to 9, satisfying the
odd-square check. The corresponding mathematical delta is neither square nor
pronic.

Change

The Lean implementation now evaluates the pronic branch only when
4 * delta + 1 fits in UInt64, matching the checked-arithmetic structure in
the native Rust source.

Regression proofs cover values around the overflow boundary.

Proof contract

justifiable_equiv remains explicitly bounded by d.toNat < 2^62.
This PR does not strengthen that theorem to a total equivalence result.

The Rust-side documentation has also been updated to state the actual proof
domain rather than claiming correctness for all natural numbers.

Testing

• cd formal && lake build EthLambdaProofs
• regression cases for 2^62 - 1, 2^62, 2^62 + 2, and UInt64::MAX

[MegaRedHand]

We should make this work correctly with all values if possible, otherwise just leaving it at < 2**62 like before is enough. Making this return a fixed wrong result, true or false, isn't really a fix here.

[MegaRedHand]

We're not currently accepting PRs to the lean-formalization branch. As I mentioned in Telegram, the Lean4 formalization is expected to land on the leanSpec repo, so the PR should go there. Feel free to use the code in lean-formalization as the base, however, or ask us for feedback.