vertical_dist_convexity[H:posreal] : THEORY
BEGIN

  IMPORTING analysis@convex_function_props,
       vectors@vectors_3D
             
  s,v,w  : VAR Vect3
  ttt,tw,tx,ty : VAR real

         % 1.A Vertical Distance

             % 1.A.1 Definitions

  % Vertical Distance
  vert_dist_scaf(s)(t: real,v): real = abs(s`z+t*v`z)-H

  % The Squared Version...
  vert_dist_sq_scaf(s)(t: real, v): real = sq(s`z + t*v`z) - sq(H)


      % 1.A.2 Convexity

  vert_dist_convex_scaf: LEMMA convex?((LAMBDA (ttt): vert_dist_scaf(s)(ttt,v)))

  vert_dist_strictly_convex_scaf: LEMMA v`z /= 0 IMPLIES strictly_convex?((LAMBDA (ttt): vert_dist_sq_scaf(s)(ttt,v)))


      % 1.A.4 Relationship to Squared Version

  vert_dist_scaf_quad_eq_0: LEMMA vert_dist_scaf(s)(ttt,v) = 0 IFF sq(s`z + ttt*v`z) = sq(H)

  vert_dist_scaf_quad_ge_0: LEMMA vert_dist_scaf(s)(ttt,v) >= 0 IFF sq(s`z + ttt*v`z) >= sq(H)

  vert_dist_scaf_quad_gt_0: LEMMA vert_dist_scaf(s)(ttt,v) > 0 IFF sq(s`z + ttt*v`z) > sq(H)

  vert_dist_scaf_quad_le_0: LEMMA vert_dist_scaf(s)(ttt,v) <= 0 IFF sq(s`z + ttt*v`z) <= sq(H)

  vert_dist_scaf_quad_lt_0: LEMMA vert_dist_scaf(s)(ttt,v) < 0 IFF sq(s`z + ttt*v`z) < sq(H)

END vertical_dist_convexity