Microlocality conjecture for the HUM control operator

Let $\Omega$ be the domain, let $\chi(t,x)$ be the control function, let $\Lambda$ be the HUM control operator, and let the optical rays be the associated bicharacteristic rays. Assume that the geometric control condition GCC holds, that $\chi(t,x)$ is smooth, and that the optical rays have no infinite-order contact with the boundary. Microlocality conjecture. Then $\Lambda$ is a microlocal operator. The conjecture is motivated by the density of rays meeting the boundary transversally and by numerical experiments, but the cited discussion does not establish the claimed microlocal analysis near rays tangent to the boundary.