[abdoo8080]

Summary

The hep : 2 < ein hypothesis on add_eq_add, sub_eq_sub, mul_eq_mul, div_eq_div, fma_eq_fma, sqrt_eq_sqrt and the rounding lemmas under them is not needed. This PR changes every 2 < e exponent hypothesis to 1 < e. Where a theorem then has both he : 1 < e and hep : 1 < e, it deletes hep.

The main theorems now also hold for e = 2. SMT-LIB allows (_ FloatingPoint eb sb) for any eb, sb > 1, which is exactly 1 < e ∧ 0 < s, so they now cover every SMT-LIB format.

Where hep came from

• PackedFloat.toRatSig_maxNormalNumber and PackedFloat.toRatExp_maxNormalNumber (Fp/PackedFloat/Lemmas/SpecialValues.lean) were added in feat: Show that lower/upper is computable for PackedFloat ~ ExtRat #70 with (he : 2 < e). Both statements are true for 1 < e, and their proofs compile unchanged. At e = 2, maxNormalNumber has biased exponent 0b10 = 2 and bias 2 = 1, so toRatExp = 1 = maxNormalExp 2. The significand is 2 - 2^-s for any e.
• feat: prove theorem about toRat_maxNormal #88 built the maxNormal value lemmas on top of these: toRat_maxNormalNumber_lt_two_pow, toRat_maxNormalNumber_lt_toRat_maxNormalNumber_succ and toRat'_maxNormal_eq_toRat_maxNormalNumber. It then added hep : 2 < ep next to he : 1 < ep up through blast{Lower,Upper}_Rel_smtLib* to mul_eq_mul.
• Later files copied the pattern (RNA/RTN/RTP/RTZ, the IsLowerHalf/TieBreak/IsEven files, Packable/PackUnpackRoundTrip, add/sub/div/fma/sqrt). That made 144 declarations in total.

Commits

1. Weaken 2 < e to 1 < e. This edits 144 binders with no proof changes. On its own it shows that no proof actually used 2 < e.
2. Drop the redundant hep. This removes the binder from the 36 declarations that also take he : 1 < e. At call sites, he hep becomes he. After apply/rw of these lemmas there is one side goal fewer, so the six bullets that discharged it are deleted: · simp [hep] ×2, · exact hep ×2, and · grind only ×2 in mul_eq_mul. One stale comment and one stale docstring note are fixed.

The other 108 declarations had 2 < e as their only exponent hypothesis. They keep their argument and its name and now take 1 < e. Their callers are unchanged.

Breaking change: the 36 declarations listed in commit 2, including the six *_eq_* theorems, each lose one explicit argument (e.g. mul_eq_mul hsin he rm a b). The only caller in this repo, FpAgainstFloatModel/Mul.lean, is updated.

Testing

• lake build Fp FpAgainstFloatModel FpExecutableTests Examples FpSymbolicRewritingTests passes after each commit. The #guard_msgs in #print axioms checks are unchanged, so no new sorry.
• As a sanity check on the newly covered e = 2 case, I ran a one-off exhaustive check outside the repo against computableSmtLibRoundMethod (the round method the test suite uses), comparing up to NaN with equal_denotation, under all 5 rounding modes. Every case matched:
  • add, sub, mul and div for PackedFloat 2 s with s ∈ {1, 2, 3}, and fma with s ∈ {1, 2}: 291,840 cases;
  • test_roundCircuitAgainstSmtlib rounding into (e, s) = (2, 1), (2, 2), (2, 3): 7,070 cases.

Not done here

• About 15 lemmas whose only hypothesis was hep : 2 < ep still contain have he : 1 < ep := by grind, which is now redundant. I left them so the diff stays mechanical.
• CI never tests an e = 2 output format: roundCircuitAgainstSmtLib uses eout ∈ {3, 4}, and the golden tests use FP8 formats. An e = 2 case could be added.

🤖 Generated with Claude Code