Commit 2026-03-06 17:09 e2c39d6d

refactor: deprecate bespoke Hyperreal machinery (#33650) Currently, these six definitions are in the Hyperreal namespace:

• IsSt x r: a predicate for r being a standard part of x
• st x: the standard part of x
• Infinitesimal x: predicate for infinitesimal elements
• InfinitePos x: predicate for infinite and positive elements
• InfiniteNeg x: predicate for infinite and negative elements
• Infinite x: predicate for infinite (positive or negative) elements. We deprecate all six of these and all of their API, in favor of reasoning with ArchimedeanClass and ArchimedeanClass.stdPart. The replacements are as follows:
• IsSt x r: 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = r
• st x: stdPart x
• Infinitesimal x: 0 < ArchimedeanClass.mk x
• InfinitePos x: 0 < x ∧ ArchimedeanClass.mk x < 0
• InfiniteNeg x: x < 0 ∧ ArchimedeanClass.mk x < 0
• Infinite x: ArchimedeanClass.mk x < 0 All of these equivalences are proved within the PR, though these new theorems have also been insta-deprecated. Most of the existing API on these predicates was largely uninteresting boilerplate, and has been deprecated without replacement. For the few results of mathematical interest (those whose proofs are longer than a few lines), I've golfed their proofs as a stress test to ensure that this new API is capable of easily proving them. I've kept everything in the same file to minimize the diff. A future PR will move the obsolete material to Deprecated.Hyperreal.