Can all mathematical operations be encoded with a Turing Complete language? In High School Computing I was taught the Structured Program Theorem - that you could implement any mathematical operation using:


Sequence
Selection
Iteration


After completing a Computer Science degree - we can express what is required for any computable function more formally with M-recursive functions: 


The constant $0$ function
The successor function
Selecting parameters
Function composition
Primitive Recursion
The $\mu$-operator (look for the smallest $x$ such that...)


This being the minimal set of axioms. Translating this to code we get:


The constant 0
Incrementation _ + 1
Variable access x
Program/statement concatenation _; _
Countdown loops for ( x to 0 ) do _ end
While loops while ( x != 0 ) do _ end


But I've come away looking for proof. How do we know all this covers all computable functions? Is there an obvious branch of Mathematics for which this is not covered? Is there a shortcoming in Lambda Calculus where it is yet to cover off obscure Mathematical operations?

(Noting of course that 


Lambda Calculus is a subset of Term rewriting, 
that Mathematica chose Term-writing over Lambda Calculus as its foundation,    
and recent work in Univalent Foundations. )


My question is: Can all mathematical operations be encoded with a Turing Complete language?
But I've come away looking for proof. How do we know all this covers all computable functions? Is there an obvious branch of Mathematics for which this is not covered? Is there a shortcoming in Lambda Calculus where it is yet to cover off obscure Mathematical operations?


These are excellent questions! The best answer your question is for you to read Turing's 1936 paper On Computable Numbers, With an Application to the Entscheidungsproblem. It's a very surprisingly readable and accessible paper, and it is concerned with precisely this question. 

To gloss the paper, there is no way to give a purely mathematical characterization of the computable functions, because what is computable is partly a question of physics -- it matters what sorts of computers we can build to compute with. 

But something we can do is to think about the operations humans perform when doing computations, and once we have a list of these, then we can build a mathematical model of a machine performing these kinds of actions (as a state-transition system). Then we can mathematically analyze this model, of course -- for example to compare it with other proposed formalisms. Turing performed such an analysis, and built a model of the situation where you have a piece of paper and a pencil, and are permitted to write on the paper, and to read what you have written and perform new actions based on what you have read. 

All of these operations are obviously physically realizable, and it turns out that (for number-computability) that all the various proposed models of computation, such as Turing machines, Church's lambda calculus, Post's rewriting systems, and Godel's systems of guarded equations are all equivalent. 

So that's why people think that Turing-completeness = computability. However, note that it is not a priori impossible that we might discover some new physical principle letting us build machines that could let us decide the halting problem. If we did, then we would be compelled to revisit our definition of computability. (Or more likely, have the super-intelligent noncomputable AI we build using such exotic physics revisit the definitions for us!)