This sequence comes up in the complexity analysis of a search algorithm. The algorithm is an attempt at Dijkstra's algorithm modified to use iterative deepening in such a way that it is efficient for search trees with both large branching factors and branching factors close to 1. In this algorithm, $T(n)$ measures the amount of nodes of the search tree that are visited on every iteration of the iterative deepening. Or in other words, $T(n)$ measures the computational budget available for search in a particular node, and how this budget is decreased when jumping to children.

Thanks for the careful analysis! Now that I know this simplified recurrence, it is easier to find closely related OEIS sequences: Sequence A000123 is equal to $\{U(0) = 1; U(n) = U(n-1) + U(\lfloor n/2 \rfloor)\}$.

Interesting. In fact, it appears that $T(n)$ is equal to the recurrence $\{U(0) = 1/2; U(n) = U(n-1) + U(\lfloor n/2 \rfloor)\}$ for $n > 0$. Although I don't understand why yet.

Oops, $x = n$, and I had a typo in the sum. Good eye!

Well, technically yes. But from a style perspective something is usually only a corollary, if it follows almost directly from the preceding lemma/theorem.

Having said that, after one proofs something in a theorem prover, often one wants to write a paper. In this paper, you would like to follow the structure of the formal proof as precisely as possible, for easy of comparison. So in my opinion, this problem also transfers to a paper setting. But do I understand from the text in your parenthesis, that you advocate using a theorem for B and a corollary for A?

Not everyone agrees with you that mixing content and presentation is an anti-pattern. For example, Knuth specificly invented literate programming to mix content and presentation. Theorem provers like Coq consciously support literate programming, and therefore have styling options.