mulPos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply when either lower endpoint is non-positive.
- Does not produce the tightest possible enclosing interval.
- Assumes exact rational arithmetic and does not address floating-point rounding.
- Does not define division, subtraction or other interval operations.
Lean usage
def phi_pow_102_interval : Interval := mulPos phi_pow_51_interval phi_pow_51_interval phi_pow_51_lo_pos phi_pow_51_lo_posformal statement (Lean)
105def mulPos (I J : Interval) (hI : 0 < I.lo) (hJ : 0 < J.lo) : Interval where
106 lo := I.lo * J.lo
proof body
Definition body.
107 hi := I.hi * J.hi
108 valid := by
109 apply mul_le_mul I.valid J.valid
110 · exact le_of_lt hJ
111 · linarith [I.valid]
112
used by (17)
-
mulPos_contains_mul -
phi_pow_102_interval -
phi_pow_102_lo_pos -
phi_pow_140_interval -
phi_pow_140_lo_pos -
phi_pow_140_lt_ratio -
phi_pow_142_interval -
phi_pow_142_lt_ratio_1_3 -
phi_pow_145_interval -
phi_pow_32_interval -
phi_pow_32_lo_pos -
phi_pow_37_interval -
phi_pow_37_lo_pos -
phi_pow_38_interval -
phi_pow_38_lo_pos -
ratio_0_7_lt_phi_pow_142 -
ratio_lt_phi_pow_145