smulPos
smulPos constructs the scaled interval obtained by multiplying both rational endpoints of a closed interval by a positive rational q. Numerics code for verified bounds on functions such as arctan cites this definition to scale reference intervals while keeping exact rational arithmetic. The definition is a direct structure constructor that multiplies the endpoints and invokes mul_le_mul_of_nonneg_left on the existing validity proof.
claimFor $q > 0$ rational and closed interval $I = [a, b]$ with $a, b$ rational and $a ≤ b$, define $q · I := [q a, q b]$.
background
The Numerics.Interval.Basic module supplies verified interval arithmetic over rational endpoints to bound real-valued transcendental functions. An Interval is the structure with rational fields lo and hi together with the proof lo ≤ hi. Positive scalar multiplication is defined directly on this structure and is referenced by both the local Interval type and the real-endpoint Interval appearing in Recognition.Certification.
proof idea
Direct structure constructor. It sets the new lo and hi fields to the products q * I.lo and q * I.hi, then discharges the validity obligation by applying mul_le_mul_of_nonneg_left to I.valid and the hypothesis 0 < q.
why it matters in Recognition Science
The definition is invoked inside arctanTwoInterval to form scaled copies of piInterval and is the target of the containment theorem smulPos_contains_smul. It therefore supplies the exact rational scaling step required by the numerics layer that produces certified bounds for Recognition Science constants and trigonometric identities.
scope and limits
- Does not accept negative or zero scalars.
- Does not accept real-valued multipliers.
- Does not guarantee the resulting interval is the tightest possible bound.
- Does not alter the real-number containment semantics of the original interval.
Lean usage
let pi4 := smulPos (1 / 4) piInterval (by norm_num)formal statement (Lean)
128def smulPos (q : ℚ) (I : Interval) (hq : 0 < q) : Interval where
129 lo := q * I.lo
proof body
Definition body.
130 hi := q * I.hi
131 valid := mul_le_mul_of_nonneg_left I.valid (le_of_lt hq)
132