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 supplies explicit rational bounds packaged as intervals for real powers and targeted powers of the golden ratio. Mass-ladder derivations in the physics necessity files cite these enclosures to close numeric gaps in the phi-ladder formula. The module consists of direct constructors that accept precomputed endpoints and return interval objects together with containment lemmas.

claimLet $I$ be a closed interval with rational endpoints. The constructor rpowIntervalSimple$(I,r)$ for $r>0$ returns an interval $J$ such that $x^r$ lies in $J$ whenever $x$ lies in $I$. The objects phiInterval, phi_pow_neg5_interval, phi_pow_neg3_interval and phi_pow_51_interval each return a concrete interval containing the indicated power of the golden ratio.

background

The module sits inside the verified interval-arithmetic layer whose parent Basic module supplies rational-endpoint enclosures for real numbers. It imports the Exp and Log siblings for related transcendental bounds and the PhiBounds sibling that records the algebraic inequalities $2.236^2<5<2.237^2$ used to certify the golden-ratio interval. In the Recognition Science setting these intervals supply the numeric scaffolding required by the phi-ladder mass formula that appears after T8.

proof idea

This is a definition module, no proofs. Each declaration is a direct constructor that receives explicit rational bounds and returns an interval object; the accompanying containment lemmas are one-line wrappers that apply the interval-membership predicate from Basic.

why it matters in Recognition Science

The module supplies the concrete numeric intervals consumed by the interval_bound tactic and by the necessity proofs in ElectronMass.Necessity and LeptonGenerations.Necessity. Those files in turn close the T9 and T10 steps that derive lepton masses from the T8 ledger quantization. The same intervals appear in QuarkMasses and GalacticBounds, completing the numeric bridge from the algebraic phi bounds to the mass-ladder calculations.

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)