width_pos

formal source

  76  velocity_pos : 0 < m
  77  closure : b + f + m = 1
  78
  79theorem width_pos (h : HydraulicExponents) : 0 < h.b := h.width_pos
  80theorem depth_pos (h : HydraulicExponents) : 0 < h.f := h.depth_pos
  81theorem velocity_pos (h : HydraulicExponents) : 0 < h.m := h.velocity_pos
  82
  83/-- σ-conservation forces b + f + m = 1. -/
  84theorem closure_identity (h : HydraulicExponents) :
  85    h.b + h.f + h.m = 1 := h.closure
  86
  87/-- Each individual exponent strictly less than 1. -/
  88theorem each_lt_one_b (h : HydraulicExponents) : h.b < 1 := by
  89  have hf : 0 < h.f := h.depth_pos
  90  have hm : 0 < h.m := h.velocity_pos
  91  have hclose : h.b + h.f + h.m = 1 := h.closure
  92  linarith
  93
  94theorem each_lt_one_f (h : HydraulicExponents) : h.f < 1 := by
  95  have hb : 0 < h.b := h.width_pos
  96  have hm : 0 < h.m := h.velocity_pos
  97  have hclose : h.b + h.f + h.m = 1 := h.closure
  98  linarith
  99
 100theorem each_lt_one_m (h : HydraulicExponents) : h.m < 1 := by
 101  have hb : 0 < h.b := h.width_pos
 102  have hf : 0 < h.f := h.depth_pos
 103  have hclose : h.b + h.f + h.m = 1 := h.closure
 104  linarith
 105
 106/-! ## §2. Canonical inhabited triples -/
 107
 108/-- The equipartition triple `(1/3, 1/3, 1/3)`: the zero-prior
 109canonical partition forced by σ-conservation when no axis is