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