two_pow_neg22_in_interval
plain-language theorem explainer
2 to the power of negative 22 lies inside its precomputed rational interval bound. Numerics routines for power functions cite this membership to anchor exact binary scaling without floating-point error. The tactic proof rewrites the exponentiation via zpow_neg to a reciprocal, then discharges both endpoint inequalities with norm_num.
Claim. $2^{-22}$ belongs to its designated interval bound $I$ on the reals.
background
The module develops interval arithmetic for powers, preferring the exp-log identity for general cases and direct integer computation for special exponents. The Interval type is a closed real interval, and contains checks membership between its lower and upper endpoints. This theorem supplies a concrete verified fact for the integer power 2 to the negative 22, equal to one over 4,194,304. Upstream results include the contains predicate and Interval structure from the Basic interval module.
proof idea
The tactic proof first simplifies the contains statement by unfolding the interval definition. It introduces an auxiliary equality rewriting 2 to the negative 22 as the reciprocal of 2 to the 22, computed as 4,194,304 via norm_num and zpow_neg. The proof then rewrites this equality into the membership claim and splits it into two inequalities, each discharged immediately by norm_num.
why it matters
The membership populates the library of certified power facts required for rigorous numerics in the Recognition framework. It supports interval bounds for phi-ladder calculations and related constants, consistent with the direct-computation strategy for integer exponents. No downstream theorems cite it yet, so it functions as a foundational primitive rather than a link in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.