The diagonal identity: diag of a formula's code is the code of that formula applied to its own numeral

Identifier: F:fo-diagonal-identity
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

FO.Code.diagAux sends the code of a formula p to the code of p with the NUMERAL of p's own code substituted for de Bruijn index 0. This is the arithmetization half of the diagonal lemma -- the half that is a computation on Nat and needs no theory at all. The remaining half, that a theory PROVES the corresponding numeric fact and hence proves the biconditional, is not established here and is F:fo-diagonal-lemma.

Formal statement

theorem FO.Code.diagAux_code : ((x0 : FO.Formula) -> ((x1 : AxNat) -> ((x2 : AxNat) -> Eq.{1} AxNat (FO.Code.diagAux (AxNat.add x1 (FO.Formula.size x0)) (AxNat.add x2 (FO.Term.size (FO.Term.numeral (FO.Formula.code x0)))) (FO.Formula.code x0)) (FO.Formula.code (FO.Formula.subst x0 (FO.Subst.cons (FO.Term.numeral (FO.Formula.code x0)) FO.Subst.id))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

1 direct dependencies 1 direct dependents

Evidence

kernel-FO.Code.diagAux_code

Kind: kernel-term
Status: checked

Supports: FO.Code.diagAux_code is admitted by the trusted kernel gate with the type recorded in formal.statement and rests on no axiom. It is one application of FO.Code.substCodeAux_commutes at t := FO.Term.numeral (FO.Formula.code p).

Checker command

cargo run -q --release -p axeyum-lean-kernel --example fo_code_inventory -- FO.Code.diagAux_code --exact --require-axiom-free

Evidence notes

Declared in crates/axeyum-lean-kernel/src/fo_roundtrip.rs by declare_diag_aux_code. The checker fails on absence.

rendered-statement-is-pinned

Kind: kernel-term
Status: checked

Supports: The theorem's declared type is rendered with Kernel::render_lean and compared against a literal in the test module, so a silently weakened statement (a dropped binder, a different decoder, the fuel on the other side of the Nat.add) fails the suite rather than passing unnoticed.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_roundtrip::tests::the_commuting_lemma_and_the_image_lemma_have_the_stated_types

Provenance

{
  "date": "2026-09-05",
  "established_by": "lane fo-diagonal (ADR-1648), by proof-term construction in crates/axeyum-lean-kernel/src/fo_roundtrip.rs",
  "source": "roadmap W3-7 second slice; the theorem ADR-1640 sized and left open",
  "prior_art": [
    {
      "who": "Kurt Goedel",
      "what": "arithmetization of syntax: a numbering of formulas whose decoding and substitution are primitive-recursive, and the diagonal identity that the code of a formula with its own numeral substituted is a computable function of the formula's code",
      "year": 1931,
      "where": "Goedel, 'Ueber formal unentscheidbare Saetze der Principia Mathematica und verwandter Systeme I', Monatshefte fuer Mathematik und Physik 38 (1931)",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}