pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Numerics.Interval.Pow

show as:
view Lean formalization →

The Numerics.Interval.Pow module packages explicit rational bounds into interval arithmetic for real exponentiation, with emphasis on powers of the golden ratio. Mass necessity proofs and galactic scale calculations cite these enclosures to keep phi-ladder numerics rigorous. The structure consists of direct wrapper definitions that apply Basic interval constructors to pre-verified bounds from PhiBounds.

claimDefines interval enclosures $I^r$ for real exponent $r$ given interval $I$ on the base, together with explicit rational bounds on the specific powers $phi^{-5}$, $phi^{-3}$, $phi^{51}$, and $phi^8$ where $phi = (1 + sqrt(5))/2$.

background

The module sits inside the verified interval arithmetic framework of Numerics.Interval.Basic, which bounds real values using exact rational endpoints. It imports Exp and Log for related transcendental control and PhiBounds, whose strategy rests on the algebraic inequalities 2.236² < 5 < 2.237² to pin down phi. In the Recognition Science setting these power intervals supply the numeric enclosures needed for phi-ladder expressions that appear in mass formulas and constants.

proof idea

This is a definition module with no proofs. The central definition rpowIntervalSimple is a one-line wrapper that packages supplied rational endpoints into an interval structure. The remaining definitions create named intervals for the listed phi powers by applying the same packaging pattern to bounds already established in PhiBounds and Mathlib.

why it matters in Recognition Science

The module supplies the concrete numeric intervals required by downstream physics modules that prove T9 electron-mass necessity, T10 lepton-ladder necessity, and quark-mass relations, as well as by GalacticBounds for the ratio tau-star over tau-zero. It also feeds the interval tactic module. These enclosures close the numeric verification step for the phi-power evaluations that appear throughout the forcing chain and mass formulas.

scope and limits

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (26)