No I don’t think it’s accurate to say they’re built on untyped lambda calculus, any more than simply typed lambda calculus is built on utyped lambda calculus. They’re very much related, and there’s a strong sense in which they are built on each other, but the kinds of programs available and what can be proved or guaranteed are different.

but (for the simply typed LC anyway) the 'mechanism of action' is just the untyped LC under beta reduction surely? I mean, the type annotations don't actually do anything when the program is run/reduced?

You are essentially identifying the semantic divergence between Church and Curry style types. Church-style or Intrinsically typed Lambda Calculus does not give any meaning to ill-typed expressions and there for beta-reduction can not proceed for these invalid expressions. Where as Curry-style or Extrinsically typed lambda calculus gives meaning to expression that do not consider the type alleged to be possessed by that expression.

The crucial difference between Church and Curry is that Curry allows each term to be ascribed a set of types - perhaps 0, 1 or many - whereas Church insists on each term having exactly one (often annotated). Both are systems for proving type correctness of terms.