The diagonal lemma for the first-order calculus (OPEN; the arithmetization half and the Leibniz rule are landed, representability in Q is not)

Recorded description

For every formula psi with one free variable there is a sentence delta such that the theory proves delta if and only if it proves psi applied to the numeral of delta's own Goedel number. STILL NOT ESTABLISHED HERE, but both prerequisites this row recorded are now discharged and the remaining obstruction is a different one. (i) The diagonalization function is built and its identity is PROVED: FO.Code.diagAux sends the code of p to the code of p with the numeral of its own code substituted, and FO.Code.diagAux_code says so (F:fo-diagonal-identity), on top of the decoder round trip and the commuting lemma. (ii) The calculus HAS a Leibniz rule as of ADR-1648: FO.Provable.eqf_subst, the seventeenth constructor, with its soundness case, so a proof that substitutes one numeral for another under a formula IS expressible. What remains is neither of those: the biconditional needs Gamma_Q to PROVE the numeric fact diag m-bar = code delta, i.e. the diagonal function must be REPRESENTABLE in Q, which for a Nat.rec-defined function is Sigma-1 completeness. Nothing in fo_*.rs relates FO.Provable to a computation on Nat in either direction; FO.Formula has no Iff connective (it would be and_ (imp a b) (imp b a)); and representing diag means representing FO.Code.pair, FO.Code.tri, FO.Code.unpair and the fuel recursion. That is a strand, not a step.