The Goedel numbering of first-order terms is injective

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

Recorded description

FO.Term.code assigns to every first-order term a natural number -- FO.Code.pair tag payload, one distinct tag per constructor, the payload nesting field codes to the right -- and the assignment is injective: if two terms have the same code they are the same term.

Formal statement

theorem FO.Term.code_injective : ((x0 : FO.Term) -> ((x1 : FO.Term) -> ((x2 : Eq.{1} AxNat (FO.Term.code x0) (FO.Term.code x1)) -> Eq.{1} FO.Term x0 x1)))

Dependencies

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

1 direct dependencies 3 direct dependents

Evidence

kernel-FO.Term.code_injective

Kind: kernel-term
Status: checked

Supports: FO.Term.code_injective is admitted by the trusted kernel gate with the type recorded in formal.statement, and rests on no axiom. It is a double recursion -- an outer FO.Term.rec at the motive 'forall u, code t = code u -> t = u', with an inner FO.Term.rec case analysis on u -- so the recursors' arities fix 4 x 4 = 16 cases and a skipped case is not possible.

Checker command

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

Evidence notes

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

statement-is-injectivity-not-congruence

Kind: kernel-term
Status: checked

Supports: The theorem's INFERRED type is rebuilt in the test module from FO.Term.code and Eq and compared by Kernel::def_eq. The negative control is the CONVERSE, 'forall t u, t = u -> code t = code u' -- true, but congruence rather than injectivity, and the statement a proof term built the wrong way round would carry. The two must NOT be def_eq.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_numbering::tests::term_code_injective_states_injectivity_not_congruence --test-threads=4

Evidence notes

Without this row the fact would rest on a rendered string nobody compared against a rebuilt term.

the-numbering-computes-and-separates-constructors

Kind: kernel-term
Status: checked

Supports: FO.Term.code is a Definition; admission says nothing about what it computes. Six term codes are pinned by Kernel::def_eq against hand-computed numerals -- var 0 |-> 0, var 2 |-> 3, f0 0 |-> 2, f0 1 |-> 4, f1 0 (var 0) |-> 5, f2 0 (var 0) (var 0) |-> 9 -- and the separating control is code (var 0) != code (f0 0), the pair that differs ONLY in its tag and that a numbering giving two constructors the same tag would collapse.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_numbering::tests::term_code_at_small_terms fo_numbering::tests::different_constructors_at_the_same_argument_get_different_codes --test-threads=4

Evidence notes

The expected values are computed from FO.Code.pair a b = tri (a + b) + a, and tri itself is re-derived in the same test file at 6, 7 and 8 rather than trusted.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum-lean-kernel build_fo_numbering_prelude, lane arithmetization (W3-7, ADR-1640)",
  "source": "authored from the roadmap item; the encoding and both proofs are written here",
  "prior_art": [
    {
      "who": "Kurt Goedel",
      "what": "arithmetization of syntax -- assigning natural numbers to formal expressions so that syntactic operations become arithmetic ones",
      "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"
    }
  ]
}