What is happening in dealing with parameter supported on [a,\infty) in stan(.)?

The following is the HMC implemented in stan(.) if I choose to use “HMC” not “NUTS”

The above sampler is for the case of \theta that is assumed to be real (or vector of real numbers).

Interestingly, it seems that stan(.) can also easily sample from a parameter \theta which is, saying, supported on [a,\infty) for some a>0.

What stan do for this??
Certainly, the Gaussian proposal does not work here.

Do stan(.) transform the \theta, via logarithm, appropriately???

Yes! When you declare the following

real<lower=0> theta;

Stan will automatically sample \log \theta and include the appropriate density adjustment term to get the equivalent density so that samples of e^{\log \theta} are distributed just as how \theta would be if you sampled on the original coordinate space.

Thanks a lot!
Would you please give me some reference for that ?
I want to know more mathematically detail about this.

See https://betanalpha.github.io/assets/case_studies/stan_intro.html#62_constraint_implementation_in_the_parameters_block.