mulPos
plain-language theorem explainer
The mulPos definition constructs the product interval for two positive intervals by multiplying their rational lower and upper endpoints. Code that bounds high powers of the golden ratio cites this to chain multiplications while keeping endpoints ordered. The construction is a direct record update whose validity proof applies mul_le_mul to the endpoint inequalities together with the positivity hypotheses.
Claim. For closed intervals $I=[I_0,I_1]$ and $J=[J_0,J_1]$ with rational endpoints satisfying $I_0<I_1$, $J_0<J_1$, $0<I_0$ and $0<J_0$, the product interval is defined by lower endpoint $I_0 J_0$ and upper endpoint $I_1 J_1$.
background
The Numerics.Interval.Basic module supplies verified interval arithmetic over the rationals to bound real expressions that arise in Recognition Science calculations. An Interval is the structure with fields lo, hi : ℚ and valid : lo ≤ hi. The mulPos operation is restricted to intervals whose lower endpoints are strictly positive so that multiplication preserves the endpoint order.
proof idea
The definition directly sets the new lo field to the product of the input lower bounds and the new hi field to the product of the input upper bounds. The single-line validity proof applies mul_le_mul to the two valid inequalities, using le_of_lt on the second positivity hypothesis and linarith on the first valid inequality.
why it matters
mulPos is called by mulPos_contains_mul to prove that the constructed interval contains the product of any two contained reals, and by the GalacticBounds module to build intervals for phi^102 = (phi^51)^2, phi^140 = phi^102 * phi^38 and higher powers used in galactic-ratio bounds. These constructions support the phi-ladder mass formula and the eight-tick octave computations in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.