two_pow_neg22_interval
plain-language theorem explainer
This definition supplies the closed rational interval [2.38e-7, 2.39e-7] that contains 2^{-22}. Interval-arithmetic code in power-function proofs cites it to obtain rigorous bounds without floating-point error. The construction is a direct record definition whose only obligation is the lo ≤ hi check, discharged by norm_num.
Claim. Define the closed interval $I = [238/10^9, 239/10^9]$ whose rational endpoints satisfy the ordering condition. The interval is guaranteed to contain the real number $2^{-22}$.
background
The module supplies interval arithmetic for the power function, using the identity $x^y = exp(y log x)$ for $x > 0$ and direct computation for natural-number exponents to obtain tighter bounds. An Interval is the structure with rational fields lo and hi together with the proof obligation lo ≤ hi; it derives decidable equality. The basic Interval definition appears in Numerics.Interval.Basic and is re-exported by Recognition.Certification.
proof idea
One-line definition that records the lower endpoint 238/1000000000, the upper endpoint 239/1000000000, and discharges the validity predicate by the norm_num tactic.
why it matters
The definition is the target of the downstream theorem two_pow_neg22_in_interval that proves exact containment of 2^{-22}. It supports the module's strategy of direct integer-power bounds, which feeds higher-level numerics used for phi-ladder constants and Recognition Science mass formulas. No open scaffolding remains at this site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.