smulPos
plain-language theorem explainer
Scalar multiplication by a positive rational scales both endpoints of a closed rational interval while preserving the order relation. Code that builds rigorous bounds for transcendental functions cites this definition to construct scaled intervals such as multiples of piInterval. The definition is a direct structure constructor that applies the nonnegativity multiplication lemma to the original validity proof.
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 is defined by lower endpoint $qa$, upper endpoint $qb$, and validity proof obtained by multiplying the original inequality by the positive scalar $q$.
background
The module supplies verified interval arithmetic over rational endpoints to bound real-valued transcendental functions. An Interval is a structure with rational fields lo and hi together with a proof that lo ≤ hi; the structure derives decidable equality. The same Interval concept appears in the Recognition.Certification module, where endpoints are real numbers and the ordering hypothesis is named lo_le_hi.
proof idea
The definition is a direct structure constructor. Lower and upper bounds are set to the rational products q * I.lo and q * I.hi. Validity is obtained by a single application of mul_le_mul_of_nonneg_left to the original I.valid proof and the hypothesis le_of_lt hq.
why it matters
This definition is used by smulPos_contains_smul to relate the scaled interval to the scaled real value and by arctanTwoInterval to form pi/4 + arctan(1/3) bounds. It supplies the scaling step required for interval expressions that certify constants appearing in the phi-ladder and alpha-band calculations of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.