(* May 2012, definitions no longer needed in primary verifications of flyspeck. *) (* deprecated May 2012: arclength_x_345 taum_hexall_x dih_hexall_x dih1_hexall_x upper_dih_hexall_x delta_hexall_x delta4_hexall_x eulerA_hexall_x factor345_hexall_x law_cosines_234_x law_cosines_126_x delta_template_B_x dih_template_B_x taum_template_B_x delta_top_x tau_lowform_x tau_m_diff_quotient tau_m_diff_quotient2 *) (* 7/29/2009: * normball deprecated. Replace normball x r with ball(x,r) * rect deprecated. Use interval instead. * wedge is now defined by Harrison using azim. He has proved a lemma giving the equivalence with the previous definition. * azim in defined by Harrison. * directed_angle is now defined through complex Arg. * definition of polar cycle has been changed (again). * a lemma is needed relating atn2 to Arg. * cone -> cone0 * deprecated: volume_props. *) (* deleted obsolete definitions 2/7/2010 svn 1471: obsolete definitions: obsolete: rad2_y, d3, mk_vec3, real3_of_triple, triple_of_real3, obsolete: conv, radius -> norm(vector[x;y]), obsolete: polar_angle -> Arg(vector[x;y]), obsolete: polar_c, less_polar, min_polar, obsolete: iter_SPEC, iter -> ITER, obsolete: azim_cycle_hyp_def, azim_cycle_spec, azim_cycle_def, obsolete: rogers, rogers0, azim_hyp_def, azim_spec, azim_def, 2011-08-01. obsolete: polar_cycle *) (* terms moved to Harrison's flyspeck.ml NULLSET_RULES, solid_triangle, ellipsoid, conic_cap, frustum, frustt, primitive, MEASURABLE_RULES, solid, coplanar, cross, wedge, azim, *) (* (now voronoi_open) let voronoi = new_definition `voronoi v S = { x | !w. ((S w) /\ ~(w=v)) ==> (dist( x, v) < dist( x, w)) }`;; *) (* DEPRECATED, 2011-08-01, not used let directed_angle = new_definition `directed_angle (x,y) (x',y') = Arg (complex(x',y') / complex(x,y))`;; let cyclic_order = new_definition `cyclic_order v u w = ((directed_angle v u < directed_angle v w) \/ ((directed_angle v u = directed_angle v w) /\ (radius u <= radius w)))`;; let polar_cycle = new_definition `polar_cycle V v = if (V SUBSET {v}) then v else (@ u. ~(u=v) /\ V u /\ (!w. ~(w = v) /\ V w ==> cyclic_order v u w))`;; *) (* let sol_euler_y = `sol_euler_y y1 y2 y3 y4 y5 y6 = (let a = y1*y2*y3 + y1*(y2*y2 + y3*y3 - y4*y4)/ &2 + y2*(y1*y1 + y3*y3 - y5*y5)/ &2 + y3*(y1*y1 + y2*y2 - y6*y6)/ &2 in &2 * atn2( &2 * a, sqrt (delta_y y1 y2 y3 y4 y5 y6)))`;; let sol_euler_y = `sol_euler_y = y_of_x sol_euler_x`;; *) (* let acs_sqrt_x1 = new_definition `acs_sqrt_x1 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = acs (sqrt(x1))`;; let acs_sqrt_x2 = new_definition `acs_sqrt_x2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = acs (sqrt(x2))`;; *) (* deprecated let solRy = new_definition `solRy y1 y2 y6 c = solR (y1/ &2) (eta_y y1 y2 y6) c`;; let dihRy = new_definition `dihRy y1 y2 y6 c = dihR (y1/ &2) (eta_y y1 y2 y6) c`;; *) (* deprecated *) let arclength_x_345 = new_definition `arclength_x_345 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = arclength (sqrt x3) (sqrt x4) (sqrt x5)`;; (* let tauq_x = new_definition `tauq_x x1 x2 x3 x4 x5 x6 x7 x8 x9 = tauq (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) (sqrt x7) (sqrt x8) (sqrt x9)`;; *) let taum_hexall_x = new_definition `taum_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) = taum_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12) + flat_term_x x2`;; (* deprecated *) let dih_hexall_x = new_definition `dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) = dih_x x1 x2 x4 ((&2 * h0) pow 2) x14 x12 - dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;; let dih1_hexall_x = new_definition `dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) = dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;; let upper_dih_hexall_x = new_definition `upper_dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) = dih_x x1 x2 x4 ((&2 * h0) pow 2) x14 x12 - upper_dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;; let delta_hexall_x = new_definition `delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) = delta_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;; let delta4_hexall_x = new_definition `delta4_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) = delta_x4 x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;; (* let euler_ap = new_definition `euler_ap y1 y2 y3 y4 y5 y6 = y1*y2*y3 + y1*(y2*y2 + y3*y3 - y4*y4)/ &2 + y2*(y1*y1 + y3*y3 - y5*y5)/ &2 + y3*(y1*y1 + y2*y2 - y6*y6)/ &2`;; *) let eulerA_hexall_x = new_definition `eulerA_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) = eulerA_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;; let factor345_hexall_x = new_definition `factor345_hexall_x c (x1:real) (x2:real) x3 x4 x5 (x6:real) = x5 -x3 -x4 + &2 * c * sqrt(x3) * sqrt(x4)`;; let law_cosines_234_x = new_definition `law_cosines_234_x c (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = x4 -x2 -x3 + &2 * c * sqrt(x2) * sqrt(x3)`;; let law_cosines_126_x = new_definition `law_cosines_126_x c (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = x6 -x1 -x2 + &2 * c * sqrt(x1) * sqrt(x2)`;; (* -- not used let taum_sub156_x = new_definition `taum_sub156_x x1s x5s x6s (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = taum_x x1s x2 x3 x4 x5s x6s`;; *) (* DEPRECATED. let tau_nullform_x = new_definition `tau_nullform_x x1 x2 x3 x4 x5 x6 = rho (sqrt x1) * pi - (pi + sol0) + sqp(delta_x x1 x2 x3 x4 x5 x6) * tau_residual_x x1 x2 x3 x4 x5 x6`;; *) (* deprecated *) let delta_template_B_x = new_definition `delta_template_B_x x15 x45 x34 x12 x1 x2 x3 x4 x5 (x6:real) = (let x23 = x12 in let x13 = edge_flat2_x x2 x1 x3 (&0) x23 x12 in let x14 = edge_flat2_x x5 x1 x4 (&0) x45 x15 in (delta_x x1 x3 x4 x34 x14 x13))`;; let dih_template_B_x = new_definition `dih_template_B_x x15 x45 x34 x12 x25 x1 x2 x3 x4 x5 (x6:real) = (let x23 = x12 in let x13 = edge_flat2_x x2 x1 x3 (&0) x23 x12 in let x14 = edge_flat2_x x5 x1 x4 (&0) x45 x15 in (dih_x x1 x2 x5 x25 x15 x12 - dih_x x1 x3 x4 x34 x14 x13))`;; let taum_template_B_x = new_definition `taum_template_B_x x15 x45 x34 x12 x1 x2 x3 x4 x5 (x6:real) = (let x23 = x12 in let x13 = edge_flat2_x x2 x1 x3 (&0) x23 x12 in let x14 = edge_flat2_x x5 x1 x4 (&0) x45 x15 in (taum_x x1 x3 x4 x34 x14 x13 +flat_term_x x2 + flat_term_x x5))`;; (* No longer needed.... deprecated. *) let delta_top_x = new_definition `delta_top_x (a:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) (x7:real) (x8:real) (x9:real) = delta_y (sqrt x4) (sqrt x9) (sqrt x6) a (sqrt x5) (sqrt x8)`;; (* tau_lowform_x intended for use when dih1 > pi/2, dih2, dih3 < pi/2, tau_residual <0, Then tau_lowform_x is a lower bound on tau (that is graceful when delta->0). *) let tau_lowform_x = new_definition `tau_lowform_x x1 x2 x3 x4 x5 x6 = (let d = delta_x x1 x2 x3 x4 x5 x6 in (rho (sqrt x1) * pi - (pi + sol0) + sqp d * rhazim_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 + sqn d * rhazim2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 + sqn d * rhazim3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6))`;; let tau_m_diff_quotient = new_definition `tau_m_diff_quotient (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) = (let eps = #0.000001 in (taum (y1 + eps) y2 y3 y4 y5 y6 - taum y1 y2 y3 y4 y5 y6)/eps)`;; let tau_m_diff_quotient2 = new_definition `tau_m_diff_quotient2 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) = (let eps = #0.000001 in (taum (y1 + eps) y2 y3 y4 y5 y6 - taum y1 y2 y3 y4 y5 y6 + taum (y1 - eps) y2 y3 y4 y5 y6)/(eps pow 2))`;; (* deleted 2013-08-18 *) let delta_y_LC = new_definition `delta_y_LC (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) = delta_y y1 y2 y3 y4 y5 y6`;; let mardih_x = new_definition `mardih_x x1 x2 x3 x4 x5 x6 = marchal_quartic (sqrt x1 / #2.0) * dih_x x1 x2 x3 x4 x5 x6`;; let mardih2_x = new_definition `mardih2_x x1 x2 x3 x4 x5 x6 = marchal_quartic (sqrt x2 / #2.0) * dih2_x x1 x2 x3 x4 x5 x6`;; let mardih3_x = new_definition `mardih3_x x1 x2 x3 x4 x5 x6 = marchal_quartic (sqrt x3 / #2.0) * dih3_x x1 x2 x3 x4 x5 x6`;; let mardih4_x = new_definition `mardih4_x x1 x2 x3 x4 x5 x6 = marchal_quartic (sqrt x4 / #2.0) * dih4_x x1 x2 x3 x4 x5 x6`;; let mardih5_x = new_definition `mardih5_x x1 x2 x3 x4 x5 x6 = marchal_quartic (sqrt x5 / #2.0) * dih5_x x1 x2 x3 x4 x5 x6`;; let mardih6_x = new_definition `mardih6_x x1 x2 x3 x4 x5 x6 = marchal_quartic (sqrt x6 / #2.0) * dih6_x x1 x2 x3 x4 x5 x6`;; (* c++ associations: ("mardih_x","marchalDih"); ("mardih2_x","marchalDih2"); ("mardih3_x","marchalDih3"); ("mardih4_x","marchalDih4"); ("mardih5_x","marchalDih5"); ("mardih6_x","marchalDih6"); *) (* (* num1 is based on the following Mathematica calculation. It is the numerator of the a-partial derivative of taumarE. num2 is the numerator of second a-partial formal proof: derived_form_sum_dih444 *) taumarE = e1 Dihedral[2, 2, 2, a, b, c] + e2 Dihedral[2, 2, 2, b, c, a] + e3 Dihedral[2, 2, 2, c, a, b]; afac = a (16 - a^2); sd = Sqrt[Delta[2, 2, 2, a, b, c]]; abcsub = {a -> 2.1, b -> 2.2, c -> 2.3, e1 -> 5.5, e2 -> 5.6, e3 -> 5.7, ssd -> sd, aafac -> afac}; abcsq = {a -> Sqrt[a2], b -> Sqrt[b2], c -> Sqrt[c2]}; taumarE1 = 4 a afac e1/(aafac ssd); taumarE2 = 4 (-8 b^2 + a^2 (-8 + b^2) + 8 c^2) e2/(aafac ssd) ; taumarE3 = 4 (-8 c^2 + a^2 (-8 + c^2) + 8 b^2) e3/(aafac ssd); (D[taumarE, a] - taumarE1 - taumarE2 - taumarE3 //. abcsub) // Chop (*0*) num1e = aafac ssd (taumarE1 + taumarE2 + taumarE3) // Together // Simplify; num1sqI = -4*(a2^2*e1 + 8*( b2 - c2)*(e2 - e3) - a2*(16*e1 + (-8 + b2)*e2 + (-8 + c2)*e3)); (* num1 in sphere.hl *) (num1e /. abcsq) - num1sqI (*0*) (* second derivatives *) taumarE1D2calc = D[Dihedral[2, 2, 2, a, b, c], {a, 2}] // Together // Simplify; taumarE1D2 = -(16*(-a^4 + (b^2 - c^2)^2)) afac^2 /(aafac^2 ssd^3); (taumarE1D2calc - taumarE1D2 //. abcsub) // Chop taumarE2D2calc = D[Dihedral[2, 2, 2, b, c, a], {a, 2}] // Together // Simplify; taumarE2D2 = -(8*(6*a^8*(-8 + b^2) + 256*( b^2 - c^2)^3 + a^6*(b^4*(-8 + c^2) - 16*b^2*(3 + c^2) + 16*( 16 + 9*c^2)) - 16*a^2*(b^6 + b^4*( 80 - 13*c^2) - 3*c^4*(16 + c^2) + b^2* c^2*(-32 + 15*c^2)) + 2*a^4*(b^6 + b^4*(56 - 10*c^2) - 24*c^2*(16 + 3*c^2) + b^2*( 384 + 16*c^2 + 9*c^4))))/(aafac^2 ssd^3); (taumarE2D2calc - taumarE2D2 //. abcsub) // Chop taumarE3D2calc = D[Dihedral[2, 2, 2, c, a, b], {a, 2}] // Together // Simplify; taumarE3D2 = -(8*(-256*(b^2 - c^2)^3 + 6*a^8*(-8 + c^2) + 16*a^2* (3*b^6 + b^4*(48 - 15*c^2) - c^4*(80 + c^2) + b^2* c^2*(32 + 13*c^2)) + a^6*(b^2*(144 - 16*c^2 + c^4) - 8*(-32 + 6*c^2 + c^4)) + 2* a^4*(9*b^4*(-8 + c^2) + c^2*(384 + 56*c^2 + c^4) - 2*b^2*(192 - 8* c^2 + 5*c^4))))/(aafac^2 ssd^3); (taumarE3D2calc - taumarE3D2 //. abcsub) // Chop taumarD2num = (e1 taumarE1D2 + e2 taumarE2D2 + e3 taumarE3D2) (aafac^2 ssd^3) // Simplify taumarD2numDef = (taumarD2num /. abcsq) // HolForm; (* num2 in sphere.hl *) (((D[taumarE, {a, 2}]) aafac^2 ssd^3 - taumarD2num) //. abcsub) // Chop (* analysis near a2 -> 16 *) {"near a2->16", DeltaX[4, 4, 4, 16, b2, c2] // Factor, (num1sqI /. a2 -> 16) // Factor, ((taumarD2num /. abcsq) /. a2 -> 16) // Factor} *) let num2 = new_definition `num2 e1 e2 e3 a2 b2 c2 = (&8 * ((&2 * ((a2 pow 5) * e1)) + (((-- &256) * (((b2 + ((-- &1) * c2)) pow 3) * (e2 + ((-- &1) * e3)))) + (((-- &1) * ((a2 pow 3) * ((&2 * (((-- &256) + ((b2 pow 2) + (((-- &2) * (b2 * c2)) + (c2 pow 2)))) * e1)) + (((((b2 pow 2) * ((-- &8) + c2)) + (((-- &16) * (b2 * (&3 + c2))) + (&16 * (&16 + (&9 * c2))))) * e2) + (((b2 * (&144 + (((-- &16) * c2) + (c2 pow 2)))) + ((-- &8) * ((-- &32) + ((&6 * c2) + (c2 pow 2))))) * e3))))) + (((a2 pow 4) * (((-- &64) * e1) + ((-- &6) * ((((-- &8) + b2) * e2) + (((-- &8) + c2) * e3))))) + (((-- &2) * ((a2 pow 2) * ((b2 + ((-- &1) * c2)) * (((b2 pow 2) * e2) + ((&8 * (c2 * ((&4 * e1) + ((&9 * e2) + ((-- &7) * e3))))) + ((&384 * (e2 + ((-- &1) * e3))) + (((-- &1) * ((c2 pow 2) * e3)) + (b2 * (((-- &32) * e1) + (((&56 + ((-- &9) * c2)) * e2) + (&9 * (((-- &8) + c2) * e3)))))))))))) + (&16 * (a2 * ((b2 + ((-- &1) * c2)) * (((b2 pow 2) * (e2 + ((-- &3) * e3))) + (((-- &4) * (b2 * ((&8 * e1) + ((((-- &20) + (&3 * c2)) * e2) + ((-- &3) * (((-- &4) + c2) * e3)))))) + (c2 * ((&32 * e1) + ((&3 * ((&16 + c2) * e2)) + ((-- &1) * ((&80 + c2) * e3))))))))))))))))`;; let rat1 = new_definition `rat1 e1 e2 e3 a2 b2 c2 = num1 e1 e2 e3 a2 b2 c2 / (sqrt(delta_x (&4) (&4) (&4) a2 b2 c2) * sqrt(a2) * (&16 - a2))`;; let rat2 = new_definition `rat2 e1 e2 e3 a2 b2 c2 = num2 e1 e2 e3 a2 b2 c2 / (((sqrt(delta_x (&4) (&4) (&4) a2 b2 c2)) pow 3) * a2 * ((&16 - a2) pow 2))`;; (* num1^2 - #0.01 * num2 *) let num_combo1 = new_definition `num_combo1 e1 e2 e3 a2 b2 c2 = ((&2 / &25) * (((-- &2) * ((a2 pow 5) * e1)) + ((&256 * (((b2 + ((-- &1) * c2)) pow 3) * (e2 + ((-- &1) * e3)))) + (((a2 pow 3) * ((&2 * (((-- &256) + ((b2 pow 2) + (((-- &2) * (b2 * c2)) + (c2 pow 2)))) * e1)) + (((((b2 pow 2) * ((-- &8) + c2)) + (((-- &16) * (b2 * (&3 + c2))) + (&16 * (&16 + (&9 * c2))))) * e2) + (((b2 * (&144 + (((-- &16) * c2) + (c2 pow 2)))) + ((-- &8) * ((-- &32) + ((&6 * c2) + (c2 pow 2))))) * e3)))) + ((&2 * ((a2 pow 4) * ((&32 * e1) + (&3 * ((((-- &8) + b2) * e2) + (((-- &8) + c2) * e3)))))) + ((&200 * ((((a2 pow 2) * e1) + ((&8 * ((b2 + ((-- &1) * c2)) * (e2 + ((-- &1) * e3)))) + ((-- &1) * (a2 * ((&16 * e1) + ((((-- &8) + b2) * e2) + (((-- &8) + c2) * e3))))))) pow 2)) + ((&2 * ((a2 pow 2) * ((b2 + ((-- &1) * c2)) * (((b2 pow 2) * e2) + ((&8 * (c2 * ((&4 * e1) + ((&9 * e2) + ((-- &7) * e3))))) + ((&384 * (e2 + ((-- &1) * e3))) + (((-- &1) * ((c2 pow 2) * e3)) + (b2 * (((-- &32) * e1) + (((&56 + ((-- &9) * c2)) * e2) + (&9 * (((-- &8) + c2) * e3)))))))))))) + ((-- &16) * (a2 * ((b2 + ((-- &1) * c2)) * (((b2 pow 2) * (e2 + ((-- &3) * e3))) + (((-- &4) * (b2 * ((&8 * e1) + ((((-- &20) + (&3 * c2)) * e2) + ((-- &3) * (((-- &4) + c2) * e3)))))) + (c2 * ((&32 * e1) + ((&3 * ((&16 + c2) * e2)) + ((-- &1) * ((&80 + c2) * e3)))))))))))))))))`;; (* x_A is a special case of x_C: *) (* let truncate_gamma23_x_A = new_definition `truncate_gamma23_x_A iw1 m1 m2 m6 = scalar6 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6) dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) iw1 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (#0.08))) * uni((truncate_gamma2_x m1), proj_x1)`;; *) let truncate_gamma23_x_C = new_definition `truncate_gamma23_x_C d iw1 m1 m2 m6 = scalar6 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6) dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) iw1 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (d))) * uni((truncate_gamma2_x m1), proj_x1)`;; let truncate_gamma23_x_B = new_definition `truncate_gamma23_x_B m1 = (dih_x - constant6 (&2 * #0.08)) * uni((truncate_gamma2_x m1),proj_x1)`;; (* function truncate_gamma2_x deprecated. It is incorrect. See gamma2_x_div_azim_v2 *) let truncate_gamma2_x = new_definition `truncate_gamma2_x m x = (&8 - x)* sqrt x / (&24) - ( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) - (&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;; let truncate_gamma3f_x = new_definition `truncate_gamma3f_x d m4 m5 m6 = truncate_vol3r_456 d - truncate_vol3f d m4 m5 m6`;; let truncate_gamma23_x = new_definition `truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 = scalar6 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6) dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) iw1 + scalar6 (compose6 (truncate_gamma3f_x (#0.14) m1 m3 m5) dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) iw2 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + mk_135 (truncate_dih_x (#0.14)))) * uni((truncate_gamma2_x m1),proj_x1)`;; (* version for large azimuth angles *) let truncate_gamma23a_x = new_definition ` truncate_gamma23a_x iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 az4 x5 x6 = truncate_gamma3f_x (&0) m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 + truncate_gamma3f_x (&0) m1 m3 m5 (&0) (&0) (&0) x1 x3 x5 * iw2 + (az4 - (dih_x x1 x2 (&2) (&2) (&2) x6 + dih_x x1 (&2) x3 (&2) x5 (&2))) * truncate_gamma2_x m1 x1`;; let truncate_gamma2_x = new_definition `truncate_gamma2_x m x = (&8 - x)* sqrt x / (&24) - ( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) - (&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;; let truncate_gamma3f_x = new_definition `truncate_gamma3f_x d m4 m5 m6 = truncate_vol3r_456 d - truncate_vol3f d m4 m5 m6`;; let truncate_gamma23_x = new_definition `truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 = scalar6 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6) dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) iw1 + scalar6 (compose6 (truncate_gamma3f_x (#0.14) m1 m3 m5) dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) iw2 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + mk_135 (truncate_dih_x (#0.14)))) * uni((truncate_gamma2_x m1),proj_x1)`;; (* version for large azimuth angles *) let truncate_gamma23a_x = new_definition ` truncate_gamma23a_x iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 az4 x5 x6 = truncate_gamma3f_x (&0) m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 + truncate_gamma3f_x (&0) m1 m3 m5 (&0) (&0) (&0) x1 x3 x5 * iw2 + (az4 - (dih_x x1 x2 (&2) (&2) (&2) x6 + dih_x x1 (&2) x3 (&2) x5 (&2))) * truncate_gamma2_x m1 x1`;; let truncate_sqrt = new_definition ` truncate_sqrt c x = if (x <= c) then sqrt(c) else sqrt(x)`;; let truncate_dih_x = new_definition(`truncate_dih_x c x1 x2 x3 x4 x5 x6 = let d_x4 = delta_x4 x1 x2 x3 x4 x5 x6 in let d = delta_x x1 x2 x3 x4 x5 x6 in pi/ (&2) + atn2( (sqrt ((&4) * x1) * truncate_sqrt c d),-- d_x4)`);; let truncate_sol_x = new_definition `truncate_sol_x c = truncate_dih_x c + (rotate2 (truncate_dih_x c)) + (rotate3 (truncate_dih_x c)) - constant6 (pi)`;; let truncate_vol_x =new_definition `truncate_vol_x c = scalar6 (uni((truncate_sqrt c),delta_x)) (&1 / &12)`;; let truncate_vol3r_456 = new_definition `truncate_vol3r_456 c = mk_456 (truncate_vol_x c)`;; (* new 6/18 *) let truncate_vol3f = new_definition `truncate_vol3f c m4 m5 m6 = scalar6 ( mk_456 (rotate5 (truncate_sol_x c)) + mk_456 (rotate6 (truncate_sol_x c)) + mk_456 (rotate4 (truncate_sol_x c)) ) (&2 * mm1/ pi) - scalar6 ( (scalar6 (uni(lfun,(scalar6 proj_y4 #0.5))) m4) * mk_456 (rotate4 (truncate_dih_x c)) + (scalar6 (uni(lfun,(scalar6 proj_y5 #0.5))) m5) * mk_456 (rotate5 (truncate_dih_x c)) + (scalar6 (uni(lfun,(scalar6 proj_y6 #0.5))) m6) * mk_456 (rotate6 (truncate_dih_x c)) ) (&8 * mm2 / pi)`;; let truncate_sqrt = new_definition ` truncate_sqrt c x = if (x <= c) then sqrt(c) else sqrt(x)`;; let truncate_dih_x = new_definition(`truncate_dih_x c x1 x2 x3 x4 x5 x6 = let d_x4 = delta_x4 x1 x2 x3 x4 x5 x6 in let d = delta_x x1 x2 x3 x4 x5 x6 in pi/ (&2) + atn2( (sqrt ((&4) * x1) * truncate_sqrt c d),-- d_x4)`);; let truncate_sol_x = new_definition `truncate_sol_x c = truncate_dih_x c + (rotate2 (truncate_dih_x c)) + (rotate3 (truncate_dih_x c)) - constant6 (pi)`;; let truncate_vol_x =new_definition `truncate_vol_x c = scalar6 (uni((truncate_sqrt c),delta_x)) (&1 / &12)`;; let truncate_vol3r_456 = new_definition `truncate_vol3r_456 c = mk_456 (truncate_vol_x c)`;; (* new 6/18 *) let truncate_vol3f = new_definition `truncate_vol3f c m4 m5 m6 = scalar6 ( mk_456 (rotate5 (truncate_sol_x c)) + mk_456 (rotate6 (truncate_sol_x c)) + mk_456 (rotate4 (truncate_sol_x c)) ) (&2 * mm1/ pi) - scalar6 ( (scalar6 (uni(lfun,(scalar6 proj_y4 #0.5))) m4) * mk_456 (rotate4 (truncate_dih_x c)) + (scalar6 (uni(lfun,(scalar6 proj_y5 #0.5))) m5) * mk_456 (rotate5 (truncate_dih_x c)) + (scalar6 (uni(lfun,(scalar6 proj_y6 #0.5))) m6) * mk_456 (rotate6 (truncate_dih_x c)) ) (&8 * mm2 / pi)`;; (* in delta_pent_x: nonstandard ordering of variables, x6 swapped with x3 *) let delta_pent_x = new_definition `delta_pent_x (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = delta_x x1 x2 x6 (&4) (&4) (#3.24 pow 2)`;; (* Upper approximation to Sqrt on [0,1]: sqp = 3/8 + (3*x)/4 - x^2/8 + (1 - x)^3 (0.7 x - 0.25); Sqp[x_]:= If[x<1,3/8 + (3*x)/4 - x^2/8 + (1 - x)^3 (0.7 x - 0.25),Sqrt[x]]; DeltaX4[x1_, x2_, x3_, x4_, x5_, x6_] := -(x2*x3) - x1*x4 + x2*x5 + x3*x6 - x5*x6 + x1*(-x1 + x2 + x3 - x4 + x5 + x6); Matan[x_] := ArcTan[Sqrt[x]]/Sqrt[x]; UpperDihX[x1_, x2_, x3_, x4_, x5_, x6_] := Module[{d, d4}, d = DeltaX[x1, x2, x3, x4, x5, x6]; d4 = DeltaX4[x1, x2, x3, x4, x5, x6]; 2 Sqrt[x1] Sqp[d]/d4 * Matan[4 x1 d/d4^2]]; UpperDihY[y1_, y2_, y3_, y4_, y5_, y6_] := UpperDihX @@ ({y1, y2, y3, y4, y5, y6}^2); Lower approx to sqrt on [0,1]: sqn = 3/8 + (3*x)/4 - x^2/8 + (1 - x)^3 (1.3 x (1 - x) - 3/8) - 0.3 x^2(1 - x)^3; Thm: if y1,y2,y3 >= 2, then Dihedral[sqrt2,y1,y2,y3,sqrt2,sqrt2] >= pi/2, (and delta_x4 <= 0). Proof: Imagine the cube of side sqrt2. qed. The case of equality delta_x4=0 occurs when y3=2, and y1 or y2=2. Thm: if y1,y2,y3 in [2,sqrt8], then Dihedral[y1,y2,sqrt2,sqrt2,sqrt2,y6] <= pi/2 (and delta_x4 >= 0). Proof. The triangle y1,y2,y3 is acute, so the circumcenter lands inside. *) let sqp = new_definition `sqp x = if (x < &1) then &3 / &8 + (&1 - x) pow 3 * (-- #0.25 + #0.7 * x) + &3 * x / &4 - x * x/ &8 else sqrt x`;; let sqn = new_definition `sqn x = if (x < &1) then #0.375 + (&3*x)/ &4 - (x pow 2)/ &8 - #0.3*((&1 - x) pow 3)*(x pow 2) + ((&1 - x) pow 3)*(-- #0.375 + #1.3*(&1 - x)*x) else sqrt x`;; (* upper bound on dih (when delta_x4 > 0), useful when delta is near 0 and angle is near 0. Also pi + upper_dih_x is a lower bound on dih when (delta_x4 < 0), useful when delta is near 0 and angle is near pi. *) let upper_dih_x = new_definition `upper_dih_x x1 x2 x3 x4 x5 x6 = (let d = delta_x x1 x2 x3 x4 x5 x6 in let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in ( &2 * sqrt x1 * sqp d * matan (&4 * x1 * d / (d4 pow 2) ) / d4))`;; let upper_dih_y = new_definition `upper_dih_y = y_of_x upper_dih_x`;; let gamma3f_135_n = new_definition `gamma3f_135_n y1 y2 y3 y4 y5 y6 = sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 - ( (&2 * mm1 / pi) * (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) - (&8 * mm2 / pi) * (y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 + y_of_x lmdih3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 + y_of_x lmdih5_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6) ))`;; let gamma3f_126_n = new_definition `gamma3f_126_n y1 y2 y3 y4 y5 y6 = sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 - ( (&2 * mm1 / pi) * (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler246_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) - (&8 * mm2 / pi) * (y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 + y_of_x lmdih2_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 + y_of_x lmdih6_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6) ))`;; let gamma23f_n = new_definition `gamma23f_n y1 y2 y3 y4 y5 y6 w1 w2 r f = gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 + gamma3f_135_n y1 sqrt2 y3 sqrt2 y5 sqrt2 / &w2 + (dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 r r r y6 - upper_dih_y y1 y3 r r r y5) * (vol2r y1 r - vol2f y1 r f) / (&2 * pi)`;; let gamma23f_126_03_n = new_definition `gamma23f_126_03_n y1 y2 y3 y4 y5 y6 w1 r f = gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 + (dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 r r r y6 - #0.03) * (vol2r y1 r - vol2f y1 r f) / (&2 * pi)`;; let euler_3flat_x = new_definition `euler_3flat_x x1 x2 x3 x23 x13 x12 = let x5 = edge_flat2_x x13 x1 x3 (&0) (&4) (&4) in let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in let x4 = edge_flat2_x x23 x2 x3 (&0) (&4) (&4) in (eulerA_x x1 x2 x3 x4 x5 x6)`;; let euler_2flat_x = new_definition `euler_2flat_x x1 x2 x3 x4 x13 x12 = let x5 = edge_flat2_x x13 x1 x3 (&0) (&4) (&4) in let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in (eulerA_x x1 x2 x3 x4 x5 x6)`;; let euler_1flat_x = new_definition `euler_1flat_x x1 x2 x3 x4 x5 x12 = let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in (eulerA_x x1 x2 x3 x4 x5 x6)`;; let taum_3flat_x = new_definition `taum_3flat_x x1 x2 x3 x23 x13 x12 = let x5 = edge_flat2_x x13 x1 x3 (&0) (&4) (&4) in let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in let x4 = edge_flat2_x x23 x2 x3 (&0) (&4) (&4) in (taum_x x1 x2 x3 x4 x5 x6 + flat_term_x x12 + flat_term_x x23 + flat_term_x x13)`;; let taum_2flat_x = new_definition `taum_2flat_x x1 x2 x3 x4 x13 x12 = let x5 = edge_flat2_x x13 x1 x3 (&0) (&4) (&4) in let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in (taum_x x1 x2 x3 x4 x5 x6 + flat_term_x x12 + flat_term_x x13)`;; let taum_1flat_x = new_definition `taum_1flat_x x1 x2 x3 x4 x5 x12 = let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in (taum_x x1 x2 x3 x4 x5 x6 + flat_term_x x12)`;; (* DEPRECATED 2013-05-25. let sphere= new_definition`sphere x=(?(v:real^3)(r:real). (r> &0)/\ (x={w:real^3 | norm (w-v)= r}))`;; *) (* deprecated 2013-2-13. let beta = new_definition(`beta psi theta = let arg = ((cos psi)*(cos psi) - (cos theta)*(cos theta))/ ((&1) - (cos theta)*(cos theta)) in (acs (sqrt arg))`);; *) (* deprecated 2013-2-13. let radius = new_definition `radius (x,y) = sqrt((x pow 2) + (y pow 2))`;; *) (* DEPRECATED added May 11, 2013. x4 st. delta_x = 50, removed May 24, 2013. let edge_flat50 = new_definition`edge_flat50 y1 y2 y3 y5 y6 = sqrt(quadratic_root_plus (abc_of_quadratic ( \x4. &50 - delta_x (y1*y1) (y2*y2) (y3*y3) x4 (y5*y5) (y6*y6))))`;; let edge_flat250_x = new_definition `edge_flat250_x x1 x2 x3 x4 x5 x6 = (edge_flat (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x5) (sqrt x6)) pow 2`;; (* x4 dummy *) let edge_flat50_x = new_definition`edge_flat50_x x1 x2 x3 (x4:real) x5 x6 = edge_flat (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x5) (sqrt x6)`;; *) (* deprecated, Dec 1, 2012 , replaced with beta_bumpA_y *) (* let beta_bump_y = new_definition `beta_bump_y y1 y2 y3 y4 y5 y6 = (if critical_edge_y y1 then &1 else &0) * (if critical_edge_y y2 then &0 else &1) * (if critical_edge_y y3 then &0 else &1) * (if critical_edge_y y4 then &1 else &0) * (if critical_edge_y y5 then &0 else &1) * (if critical_edge_y y6 then &0 else &1) * (bump (y1/ &2) - bump (y4 / &2))`;; *) (* let delta_x6 = new_definition `delta_x6 x1 x2 x3 x4 x5 x6 = -- x1 *x2 + x1 *x4 + x2* x5 - x4* x5 + x3* (x1 + x2 - x3 + x4 + x5 - x6) - x3 * x6`;; *) let gamma3f_135_s_n = new_definition `gamma3f_135_s_n y1 y2 y3 y4 y5 y6 = sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 - (&2 * mm1 / pi) * (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;; let gamma3f_126_s_n = new_definition `gamma3f_126_s_n y1 y2 y3 y4 y5 y6 = sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 - (&2 * mm1 / pi) * (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler246_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;; let lmdih_x_n = new_definition `lmdih_x_n x1 x2 x3 x4 x5 x6 = sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let lmdih2_x_n = new_definition `lmdih2_x_n x1 x2 x3 x4 x5 x6 = sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let lmdih3_x_n = new_definition `lmdih3_x_n x1 x2 x3 x4 x5 x6 = sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let lmdih5_x_n = new_definition `lmdih5_x_n x1 x2 x3 x4 x5 x6 = sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let lmdih6_x_n = new_definition `lmdih6_x_n x1 x2 x3 x4 x5 x6 = sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let gamma3f_vLR_n = new_definition `gamma3f_vLR_n y1 y2 y3 y4 y5 y6 f = (dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - upper_dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;; let gamma3f_vL_n = new_definition `gamma3f_vL_n y1 y2 y3 y4 y5 y6 f = (dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;; let gamma3f_vLR_n0 = new_definition `gamma3f_vLR_n0 y1 y2 y3 y4 y5 y6 = gamma3f_vLR_n y1 y2 y3 y4 y5 y6 (\x. &0)`;; let gamma3f_vLR_nlfun = new_definition `gamma3f_vLR_nlfun y1 y2 y3 y4 y5 y6 = gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lfun`;; let gamma3f_vL_n0 = new_definition `gamma3f_vL_n0 y1 y2 y3 y4 y5 y6 = gamma3f_vL_n y1 y2 y3 y4 y5 y6 (\x. &0)`;; let gamma3f_vL_nlfun = new_definition `gamma3f_vL_nlfun y1 y2 y3 y4 y5 y6 = gamma3f_vL_n y1 y2 y3 y4 y5 y6 lfun`;; let ldih_x_n = new_definition `ldih_x_n x1 x2 x3 x4 x5 x6 = sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let ldih2_x_n = new_definition `ldih2_x_n x1 x2 x3 x4 x5 x6 = sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let ldih3_x_n = new_definition `ldih3_x_n x1 x2 x3 x4 x5 x6 = sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let ldih5_x_n = new_definition `ldih5_x_n x1 x2 x3 x4 x5 x6 = sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let ldih6_x_n = new_definition `ldih6_x_n x1 x2 x3 x4 x5 x6 = sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let gamma3f_vLR_x_nlfun = new_definition `gamma3f_vLR_x_nlfun x1 x2 x3 x4 x5 x6= gamma3f_vLR_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_vL_x_nlfun = new_definition `gamma3f_vL_x_nlfun x1 x2 x3 x4 x5 x6= gamma3f_vL_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_vLR_x_n0 = new_definition `gamma3f_vLR_x_n0 x1 x2 x3 x4 x5 x6= gamma3f_vLR_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_vL_x_n0 = new_definition `gamma3f_vL_x_n0 x1 x2 x3 x4 x5 x6= gamma3f_vL_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_135_x_s_n = new_definition `gamma3f_135_x_s_n x1 (x2:real) x3 (x4:real) x5 (x6:real) = gamma3f_135_s_n (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let gamma3f_126_x_s_n = new_definition `gamma3f_126_x_s_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_126_s_n (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let rr22 = REWRITE_RULE[GSYM sqrt2_sqrt2];; let ldih_x_126_n = rr22 (new_definition `ldih_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 = ldih_x_n x1 x2 (&2) (&2) (&2) x6`);; (* let ldih2_x_126_n = rr22 (new_definition `ldih2_x_126_n_ x1 x2 (x3:real) (x4:real) (x5:real) x6 = ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);; *) let ldih2_x_126_n = rr22 (new_definition `ldih2_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 = ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);; let ldih6_x_126_n = rr22 (new_definition `ldih6_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 = ldih6_x_n x1 x2 (&2) (&2) (&2) x6`);; let ldih_x_135_n = rr22 (new_definition `ldih_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = ldih_x_n x1 (&2) x3 (&2) x5 (&2)`);; let ldih3_x_135_n = rr22 (new_definition `ldih3_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = ldih3_x_n x1 (&2) x3 (&2) x5 (&2)`);; let ldih5_x_135_n = rr22 (new_definition `ldih5_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = ldih5_x_n x1 (&2) x3 (&2) x5 (&2)`);; (* let vol3f_sqrt2_lfun = new_definition `vol3f_sqrt2_lfun y1 y2 (y3:real) (y4:real) (y5:real) y6 = vol3f y1 y2 y6 sqrt2 lfun`;; *) (* remaining splits *) let gamma3f_126 = new_definition `gamma3f_126 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f = gamma3f y1 y2 y6 sqrt2 f`;; let gamma3f_135 = new_definition `gamma3f_135 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f = gamma3f y1 y3 y5 sqrt2 f`;; let gamma3f_vLR = new_definition `gamma3f_vLR (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;; let gamma3f_vL = new_definition `gamma3f_vL (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;; let gamma3f_v = new_definition `gamma3f_v (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;; let gamma23f_126_03 = new_definition `gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 r f = (gamma3f y1 y2 y6 r f / &w1 + (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 r r r y6 - #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)) `;; let gamma23f_red_03 = new_definition `gamma23f_red_03 y1 y2 y3 y4 y5 y6 r f = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)`;; let gamma3f_vLR0 = new_definition `gamma3f_vLR0 y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) * (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) / (&2 * pi)`;; let gamma3f_vLR_lfun = new_definition `gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) * (vol2r y1 sqrt2 - ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) - (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) / (&2 * pi) `;; let gamma3f_vL0 = new_definition `gamma3f_vL0 y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) / (&2 * pi) `;; let gamma3f_vL_lfun = new_definition `gamma3f_vL_lfun y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) - (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) / (&2 * pi)`;; let gamma3f_v0 = new_definition `gamma3f_v0 y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) / (&2 * pi)`;; let gamma3f_v_lfun = new_definition `gamma3f_v_lfun y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) - (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) / (&2 * pi)`;; let dih_x_126_s2 = new_definition `dih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih2_x_126_s2 = new_definition `dih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih2_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih3_x_126_s2 = new_definition `dih3_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih3_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih4_x_126_s2 = new_definition `dih4_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih4_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih5_x_126_s2 = new_definition `dih5_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih5_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih6_x_126_s2 = new_definition `dih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih6_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let ldih_x_126_s2 = new_definition `ldih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = lfun (sqrt x1 / #2.0) * dih_x_126_s2 x1 x2 x3 x4 x5 x6`;; let ldih2_x_126_s2 = new_definition `ldih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = lfun (sqrt x2 / #2.0) * dih2_x_126_s2 x1 x2 x3 x4 x5 x6`;; let ldih6_x_126_s2 = new_definition `ldih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = lfun (sqrt x6 / #2.0) * dih6_x_126_s2 x1 x2 x3 x4 x5 x6`;; let dih_x_135_s2 = new_definition `dih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih2_x_135_s2 = new_definition `dih2_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih2_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih3_x_135_s2 = new_definition `dih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih3_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih4_x_135_s2 = new_definition `dih4_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih4_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih5_x_135_s2 = new_definition `dih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih5_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih6_x_135_s2 = new_definition `dih6_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih6_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let ldih_x_135_s2' = new_definition `ldih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = lfun (sqrt x1/ #2.0) * dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let ldih3_x_135_s2 = new_definition `ldih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = lfun (sqrt x3/ #2.0) * dih3_x_135_s2 x1 x2 x3 x4 x5 x6 `;; let ldih5_x_135_s2 = new_definition `ldih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = lfun (sqrt x5/ #2.0) * dih5_x_135_s2 x1 x2 x3 x4 x5 x6 `;; let delta_x_126_s2 = new_definition `delta_x_126_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = delta_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let delta_x_135_s2 = new_definition `delta_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = delta_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let gamma3f_x_vLR_lfun = new_definition `gamma3f_x_vLR_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vLR_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_vLR0 = new_definition `gamma3f_x_vLR0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vLR0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_vL_lfun = new_definition `gamma3f_x_vL_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vL_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_vL0 = new_definition `gamma3f_x_vL0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vL0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_v_lfun = new_definition `gamma3f_x_v_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_v_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_v0 = new_definition `gamma3f_x_v0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_v0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let vol3_x_135_s2 = new_definition `vol3_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = vol3r (sqrt x1) (sqrt x3) (sqrt x5) sqrt2`;; let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;; let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;; let gamma23f_126_03 = new_definition `gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 r f = (gamma3f y1 y2 y6 r f / &w1 + (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 r r r y6 - #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)) `;; let gamma23f_red_03 = new_definition `gamma23f_red_03 y1 y2 y3 y4 y5 y6 r f = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)`;; let gamma3f_vLR0 = new_definition `gamma3f_vLR0 y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) * (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) / (&2 * pi)`;; let gamma3f_vLR_lfun = new_definition `gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) * (vol2r y1 sqrt2 - ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) - (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) / (&2 * pi) `;; let gamma3f_vL0 = new_definition `gamma3f_vL0 y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) / (&2 * pi) `;; let gamma3f_vL_lfun = new_definition `gamma3f_vL_lfun y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) - (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) / (&2 * pi)`;; let gamma3f_v0 = new_definition `gamma3f_v0 y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) / (&2 * pi)`;; let gamma3f_v_lfun = new_definition `gamma3f_v_lfun y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) - (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) / (&2 * pi)`;; let dih_x_126_s2 = new_definition `dih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih2_x_126_s2 = new_definition `dih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih2_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih3_x_126_s2 = new_definition `dih3_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih3_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih4_x_126_s2 = new_definition `dih4_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih4_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih5_x_126_s2 = new_definition `dih5_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih5_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih6_x_126_s2 = new_definition `dih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih6_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let ldih_x_126_s2 = new_definition `ldih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = lfun (sqrt x1 / #2.0) * dih_x_126_s2 x1 x2 x3 x4 x5 x6`;; let ldih2_x_126_s2 = new_definition `ldih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = lfun (sqrt x2 / #2.0) * dih2_x_126_s2 x1 x2 x3 x4 x5 x6`;; let ldih6_x_126_s2 = new_definition `ldih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = lfun (sqrt x6 / #2.0) * dih6_x_126_s2 x1 x2 x3 x4 x5 x6`;; let dih_x_135_s2 = new_definition `dih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih2_x_135_s2 = new_definition `dih2_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih2_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih3_x_135_s2 = new_definition `dih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih3_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih4_x_135_s2 = new_definition `dih4_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih4_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih5_x_135_s2 = new_definition `dih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih5_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih6_x_135_s2 = new_definition `dih6_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih6_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let ldih_x_135_s2' = new_definition `ldih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = lfun (sqrt x1/ #2.0) * dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let ldih3_x_135_s2 = new_definition `ldih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = lfun (sqrt x3/ #2.0) * dih3_x_135_s2 x1 x2 x3 x4 x5 x6 `;; let ldih5_x_135_s2 = new_definition `ldih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = lfun (sqrt x5/ #2.0) * dih5_x_135_s2 x1 x2 x3 x4 x5 x6 `;; let delta_x_126_s2 = new_definition `delta_x_126_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = delta_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let delta_x_135_s2 = new_definition `delta_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = delta_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let gamma3f_x_vLR_lfun = new_definition `gamma3f_x_vLR_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vLR_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_vLR0 = new_definition `gamma3f_x_vLR0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vLR0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_vL_lfun = new_definition `gamma3f_x_vL_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vL_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_vL0 = new_definition `gamma3f_x_vL0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vL0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_v_lfun = new_definition `gamma3f_x_v_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_v_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_v0 = new_definition `gamma3f_x_v0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_v0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let vol3_x_135_s2 = new_definition `vol3_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = vol3r (sqrt x1) (sqrt x3) (sqrt x5) sqrt2`;; (* let arclength6_x = new_definition `arclength6_x x1 x2 x3 x4 x5 x6 = arclength (sqrt x1) (sqrt x2) (sqrt x3)`;; *) let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;; let gamma3f_135_s_n = new_definition `gamma3f_135_s_n y1 y2 y3 y4 y5 y6 = sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 - (&2 * mm1 / pi) * (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;; let gamma3f_126_s_n = new_definition `gamma3f_126_s_n y1 y2 y3 y4 y5 y6 = sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 - (&2 * mm1 / pi) * (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler246_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;; let lmdih_x_n = new_definition `lmdih_x_n x1 x2 x3 x4 x5 x6 = sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let lmdih2_x_n = new_definition `lmdih2_x_n x1 x2 x3 x4 x5 x6 = sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let lmdih3_x_n = new_definition `lmdih3_x_n x1 x2 x3 x4 x5 x6 = sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let lmdih5_x_n = new_definition `lmdih5_x_n x1 x2 x3 x4 x5 x6 = sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let lmdih6_x_n = new_definition `lmdih6_x_n x1 x2 x3 x4 x5 x6 = sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let gamma3f_vLR_n = new_definition `gamma3f_vLR_n y1 y2 y3 y4 y5 y6 f = (dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - upper_dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;; let gamma3f_vL_n = new_definition `gamma3f_vL_n y1 y2 y3 y4 y5 y6 f = (dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;; let gamma3f_vLR_n0 = new_definition `gamma3f_vLR_n0 y1 y2 y3 y4 y5 y6 = gamma3f_vLR_n y1 y2 y3 y4 y5 y6 (\x. &0)`;; let gamma3f_vLR_nlfun = new_definition `gamma3f_vLR_nlfun y1 y2 y3 y4 y5 y6 = gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lfun`;; let gamma3f_vL_n0 = new_definition `gamma3f_vL_n0 y1 y2 y3 y4 y5 y6 = gamma3f_vL_n y1 y2 y3 y4 y5 y6 (\x. &0)`;; let gamma3f_vL_nlfun = new_definition `gamma3f_vL_nlfun y1 y2 y3 y4 y5 y6 = gamma3f_vL_n y1 y2 y3 y4 y5 y6 lfun`;; let ldih_x_n = new_definition `ldih_x_n x1 x2 x3 x4 x5 x6 = sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let ldih2_x_n = new_definition `ldih2_x_n x1 x2 x3 x4 x5 x6 = sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let ldih3_x_n = new_definition `ldih3_x_n x1 x2 x3 x4 x5 x6 = sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let ldih5_x_n = new_definition `ldih5_x_n x1 x2 x3 x4 x5 x6 = sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let ldih6_x_n = new_definition `ldih6_x_n x1 x2 x3 x4 x5 x6 = sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;; let gamma3f_vLR_x_nlfun = new_definition `gamma3f_vLR_x_nlfun x1 x2 x3 x4 x5 x6= gamma3f_vLR_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_vL_x_nlfun = new_definition `gamma3f_vL_x_nlfun x1 x2 x3 x4 x5 x6= gamma3f_vL_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_vLR_x_n0 = new_definition `gamma3f_vLR_x_n0 x1 x2 x3 x4 x5 x6= gamma3f_vLR_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_vL_x_n0 = new_definition `gamma3f_vL_x_n0 x1 x2 x3 x4 x5 x6= gamma3f_vL_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_135_x_s_n = new_definition `gamma3f_135_x_s_n x1 (x2:real) x3 (x4:real) x5 (x6:real) = gamma3f_135_s_n (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let gamma3f_126_x_s_n = new_definition `gamma3f_126_x_s_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_126_s_n (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let rr22 = REWRITE_RULE[GSYM sqrt2_sqrt2];; let ldih_x_126_n = rr22 (new_definition `ldih_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 = ldih_x_n x1 x2 (&2) (&2) (&2) x6`);; (* let ldih2_x_126_n = rr22 (new_definition `ldih2_x_126_n_ x1 x2 (x3:real) (x4:real) (x5:real) x6 = ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);; *) let ldih2_x_126_n = rr22 (new_definition `ldih2_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 = ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);; let ldih6_x_126_n = rr22 (new_definition `ldih6_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 = ldih6_x_n x1 x2 (&2) (&2) (&2) x6`);; let ldih_x_135_n = rr22 (new_definition `ldih_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = ldih_x_n x1 (&2) x3 (&2) x5 (&2)`);; let ldih3_x_135_n = rr22 (new_definition `ldih3_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = ldih3_x_n x1 (&2) x3 (&2) x5 (&2)`);; let ldih5_x_135_n = rr22 (new_definition `ldih5_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = ldih5_x_n x1 (&2) x3 (&2) x5 (&2)`);; (* let vol3f_sqrt2_lfun = new_definition `vol3f_sqrt2_lfun y1 y2 (y3:real) (y4:real) (y5:real) y6 = vol3f y1 y2 y6 sqrt2 lfun`;; *) (* remaining splits *) let gamma3f_126 = new_definition `gamma3f_126 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f = gamma3f y1 y2 y6 sqrt2 f`;; let gamma3f_135 = new_definition `gamma3f_135 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f = gamma3f y1 y3 y5 sqrt2 f`;; let gamma3f_vLR = new_definition `gamma3f_vLR (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;; let gamma3f_vL = new_definition `gamma3f_vL (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;; let gamma3f_v = new_definition `gamma3f_v (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;; let gamma23f = new_definition `gamma23f y1 y2 y3 y4 y5 y6 w1 w2 r f = (gamma3f y1 y2 y6 r f / &w1 + gamma3f y1 y3 y5 r f / &w2 + (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 r r r y6 - dih_y y1 y3 r r r y5) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)) `;; let gamma23f_126_03 = new_definition `gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 r f = (gamma3f y1 y2 y6 r f / &w1 + (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 r r r y6 - #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)) `;; let gamma23f_red_03 = new_definition `gamma23f_red_03 y1 y2 y3 y4 y5 y6 r f = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)`;; let gamma3f_vLR0 = new_definition `gamma3f_vLR0 y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) * (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) / (&2 * pi)`;; let gamma3f_vLR_lfun = new_definition `gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) * (vol2r y1 sqrt2 - ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) - (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) / (&2 * pi) `;; let gamma3f_vL0 = new_definition `gamma3f_vL0 y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) / (&2 * pi) `;; let gamma3f_vL_lfun = new_definition `gamma3f_vL_lfun y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) - (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) / (&2 * pi)`;; let gamma3f_v0 = new_definition `gamma3f_v0 y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) / (&2 * pi)`;; let gamma3f_v_lfun = new_definition `gamma3f_v_lfun y1 y2 y3 y4 y5 y6 = (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) - (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) / (&2 * pi)`;; let dih_x_126_s2 = new_definition `dih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih2_x_126_s2 = new_definition `dih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih2_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih3_x_126_s2 = new_definition `dih3_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih3_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih4_x_126_s2 = new_definition `dih4_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih4_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih5_x_126_s2 = new_definition `dih5_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih5_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let dih6_x_126_s2 = new_definition `dih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = dih6_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let ldih_x_126_s2 = new_definition `ldih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = lfun (sqrt x1 / #2.0) * dih_x_126_s2 x1 x2 x3 x4 x5 x6`;; let ldih2_x_126_s2 = new_definition `ldih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = lfun (sqrt x2 / #2.0) * dih2_x_126_s2 x1 x2 x3 x4 x5 x6`;; let ldih6_x_126_s2 = new_definition `ldih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 = lfun (sqrt x6 / #2.0) * dih6_x_126_s2 x1 x2 x3 x4 x5 x6`;; let dih_x_135_s2 = new_definition `dih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih2_x_135_s2 = new_definition `dih2_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih2_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih3_x_135_s2 = new_definition `dih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih3_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih4_x_135_s2 = new_definition `dih4_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih4_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih5_x_135_s2 = new_definition `dih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih5_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let dih6_x_135_s2 = new_definition `dih6_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = dih6_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let ldih_x_135_s2' = new_definition `ldih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = lfun (sqrt x1/ #2.0) * dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let ldih3_x_135_s2 = new_definition `ldih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = lfun (sqrt x3/ #2.0) * dih3_x_135_s2 x1 x2 x3 x4 x5 x6 `;; let ldih5_x_135_s2 = new_definition `ldih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) = lfun (sqrt x5/ #2.0) * dih5_x_135_s2 x1 x2 x3 x4 x5 x6 `;; let delta_x_126_s2 = new_definition `delta_x_126_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = delta_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;; let delta_x_135_s2 = new_definition `delta_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = delta_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;; let gamma3f_x_vLR_lfun = new_definition `gamma3f_x_vLR_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vLR_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_vLR0 = new_definition `gamma3f_x_vLR0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vLR0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_vL_lfun = new_definition `gamma3f_x_vL_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vL_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_vL0 = new_definition `gamma3f_x_vL0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_vL0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_v_lfun = new_definition `gamma3f_x_v_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_v_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let gamma3f_x_v0 = new_definition `gamma3f_x_v0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = gamma3f_v0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;; let vol3_x_135_s2 = new_definition `vol3_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = vol3r (sqrt x1) (sqrt x3) (sqrt x5) sqrt2`;; (* let dih_y_div_sqrtdelta_posbranch = new_definition `dih_y_div_sqrtdelta_posbranch = y_of_x dih_x_div_sqrtdelta_posbranch`;; *) (* let rhof_x = define `rhof_x x = rho (sqrt x)`;; *) (* let ineq_lemma = prove_by_refinement( `!a x b. &0 <= a /\ &0 <= b /\ a pow 2 <= x /\ x <= b pow 2 ==> a <= sqrt x /\ sqrt x <= b`, (* {{{ proof *) [ REPEAT GEN_TAC; STRIP_TAC; SUBGOAL_THEN `&0 <= x` MP_TAC; ASM_MESON_TAC [REAL_LE_TRANS;Collect_geom.REAL_LE_SQUARE_POW]; ASM_MESON_TAC[Collect_geom.POW2_COND;SQRT_WORKS]; ]);; (* }}} *) *) (* let arclength6_x = new_definition `arclength6_x x1 x2 x3 x4 x5 x6 = arclength (sqrt x1) (sqrt x2) (sqrt x3)`;; *) (* let sqrt_x8 = define `sqrt_x8 (x7:real) (x2:real) (x3:real) (x4:real) (x8:real) (x9:real) = sqrt x8`;; let sqrt_x9 = define `sqrt_x9 (x7:real) (x2:real) (x3:real) (x4:real) (x8:real) (x9:real) = sqrt x9`;; *)