npow
This definition raises a positive rational interval to a natural power by exponentiating its endpoints. Numerics code for mass bounds and containment checks cites it when computing phi-powered terms. The implementation is a direct record construction whose validity obligation is met by monotonicity of exponentiation on positive bases.
claimLet $I = [q_l, q_h]$ be a closed interval with rational endpoints $q_l, q_h$ satisfying $q_l < q_h$ and $q_l > 0$. For $n$ a natural number the powered interval is the structure whose lower bound is $q_l^n$, upper bound is $q_h^n$, and whose validity follows from the monotonicity of the power map on positive rationals.
background
The Numerics.Interval.Basic module supplies verified interval arithmetic that uses exact rational endpoints to bound real computations. Its core Interval structure is a record carrying rational lo and hi fields together with a proof that lo ≤ hi. The module imports Mathlib interval and ordering tactics and sits alongside a real-endpoint Interval variant defined in Recognition.Certification.
proof idea
The definition is a direct record construction that sets the new lo and hi fields to the n-th powers of the input endpoints. The single validity obligation is discharged by applying the lemma pow_le_pow_left₀ to the positivity hypothesis on the lower endpoint and the original interval validity proof.
why it matters in Recognition Science
The definition is invoked by rs_mass_MeV to evaluate the phi-ladder mass formula in MeV units and by npow_contains_pow to establish that the powered interval contains the real power. It therefore supplies the numerical engine required for the Recognition Science mass formula and for the phi-based constants appearing in the eight-tick octave and D = 3 derivations.
scope and limits
- Does not accept intervals whose lower endpoint is non-positive.
- Does not define powers for real or negative exponents.
- Does not itself prove containment of real numbers inside the result interval.
- Does not operate on the real-endpoint Interval structure from Certification.
Lean usage
example (I : Interval) (h : 0 < I.lo) : Interval := npow I 2 hformal statement (Lean)
143def npow (I : Interval) (n : ℕ) (hI : 0 < I.lo) : Interval where
144 lo := I.lo ^ n
proof body
Definition body.
145 hi := I.hi ^ n
146 valid := by
147 apply pow_le_pow_left₀ (le_of_lt hI) I.valid
148