Is there some extra capability of functions that Theorem + postulates doesn't include?

Oh yes, tons. Try constructing a value with type Theorem Integer :-) The world under Theorem is much more restricted.

A→□A doesn't mean "all true statements are provable", it means "all statements we can construct a proof term for are provable"

Well, not quite. The □ operator in the original proof doesn't mean provability from the premises of the theorem, it means provability in bare bones PA, starting from nothing. We want to only use assumptions that are true under that interpretation of □, which means they must hold in provability logic (GL). And the assumption A→□A doesn't hold in GL.

The assumptions used in the original proof are ⊢A→⊢□A and ⊢(□A→□□A), both of which hold in GL. I think the simplest way to encode these is to use separate constructs for ⊢ and □, as I did in the post.