Choreographic programming (CP) is a programming paradigm for the correct-by-construction development of concurrent and distributed systems: programmers write the intended overall behaviour of a system from a global perspective in a choreography, which is then automatically compiled into communicating endpoint programs by a procedure known as endpoint projection (EPP). The central promise is that the projected endpoint programs, when executed together, are behaviourally equivalent to the source choreography. Fulfilling this promise becomes delicate for expressive CP languages. Existing mechanisations of CP treat only restricted fragments, while textbook and general purpose language implementations with rich features leave crucial interactions informal. In particular, general branching in knowledge of choice, general recursion, and nondeterministic choice in choreographies have not yet been integrated in a machine-checked theory. We present Mech, a new mechanisation of CP in Lean 4 that captures these features. There are two central technical challenges in our development of Mech. First, the sketched semantics from the literature does not correctly capture how nondeterministic choice interacts with concurrency. We therefore formulate new semantics that align nondeterministic choreographic executions with the behaviours of projected endpoint programs. Second, managing all these features in proofs is complex. We address this by uncovering new algebraic laws for choreographies, the operators used in their semantics, EPP, and their combinations. Using our development, we prove completeness and soundness of EPP and derive communication safety and deadlock-freedom for projected networks, yielding the most extensive mechanised theory of CP to date.