smulPos
plain-language theorem explainer
smulPos constructs the scaled interval by multiplying both rational endpoints by a positive rational q. It is cited in downstream interval bounds for arctan and related transcendentals. The definition is a direct record construction whose validity field is discharged by monotonicity of multiplication.
Claim. Let $I = [a, b]$ be a closed interval with rational endpoints $a, b$ satisfying $a ≤ b$. For positive rational $q > 0$ the scaled interval $q · I$ is the closed interval with endpoints $q a$ and $q b$.
background
The module supplies verified interval arithmetic whose endpoints are rational numbers, allowing exact Lean computation while still bounding real values. The central structure Interval is a record with fields lo : ℚ, hi : ℚ and valid : lo ≤ hi. A parallel but distinct Interval structure appears in Recognition.Certification whose endpoints are real numbers.
proof idea
Direct record construction that sets the new lo and hi to the componentwise products and supplies the validity proof via mul_le_mul_of_nonneg_left applied to the original valid field and the hypothesis 0 < q.
why it matters
The definition is invoked inside arctanTwoInterval to scale the pi/4 interval and inside the containment theorem smulPos_contains_smul. It therefore supplies the elementary scaling step required for rigorous interval bounds on transcendental functions inside the numerics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.