Substitution on Goedel codes agrees with substitution on first-order syntax

Identifier: F:fo-subst-code-commutes
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

FO.Code.substCodeAux decodes a formula code and a term code, substitutes the term for de Bruijn index 0, and re-encodes; the theorem says that on genuine codes this computes the code of the genuine substitution. This is the arithmetized substitution operation every representability argument is built on: it turns a syntactic operation into a function Nat -> Nat with a proof that the two agree. FO.Code.isFormulaCodeAux_code is the companion image lemma -- everything FO.Formula.code produces is accepted by the decide-and-re-encode test.

Formal statement

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

Dependencies

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

2 direct dependencies 2 direct dependents

Evidence

kernel-FO.Code.substCodeAux_commutes

Kind: kernel-term
Status: checked

Supports: FO.Code.substCodeAux_commutes is admitted by the trusted kernel gate with the type recorded in formal.statement and rests on no axiom. Its proof is two congruences over the two round trips and nothing else; the whole cost of the statement was F:fo-formula-decode-code.

Checker command

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

Evidence notes

Declared in crates/axeyum-lean-kernel/src/fo_roundtrip.rs by declare_subst_code_aux_commutes. 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"
    }
  ]
}