What mathematical terminology exists for "embellished trees"?
A good framework for reasoning about this is research on "ornaments" which were introduced by Conor McBride here: https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf .

The idea of ornamentation is that you start with a simple algebraic data type and then you have a separate "ornamented" version of it where the constructors might have more information, which is especially useful in dependently typed programming because a lot of times you want to "adjoin" invariants to a datatype. For more on this, there is another article in the JFP: https://josh-hs-ko.github.io/manuscripts/JFP17.pdf

However, it seems like you are not interested in dependent type theory and have noticed that ornaments arise naturally in everyday programming. For that I would recommend reading about the work on using ornaments in OCaml, specifically this paper (http://pauillac.inria.fr/~remy/ornaments/mlorn-2017-09.pdf) which also has a tutorial for the library here: http://pauillac.inria.fr/~remy/ornaments/ocamlorn/doc/tutorial.html