The fuel-additive decoder round trip for first-order terms

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

Recorded description

FO.Term.decodeAux, given at least FO.Term.size t units of fuel, returns t from FO.Term.code t. Stated additively -- for every t and every f, decodeAux (Nat.add f (size t)) (code t) = t -- so the theorem covers every sufficient fuel at once rather than one distinguished amount, and the corollary FO.Term.decode_code_at_size is the case f = Nat.zero. Together with F:fo-term-code-injective this makes FO.Term.code a genuine numbering: injective, and inverted by a total computable function of the code.

Formal statement

theorem FO.Term.decode_code : ((x0 : FO.Term) -> ((x1 : AxNat) -> Eq.{1} FO.Term (FO.Term.decodeAux (AxNat.add x1 (FO.Term.size x0)) (FO.Term.code x0)) x0))

Dependencies

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

3 direct dependencies 3 direct dependents

Evidence

kernel-FO.Term.decode_code

Kind: kernel-term
Status: checked

Supports: FO.Term.decode_code is admitted by the trusted kernel gate with the type recorded in formal.statement and rests on no axiom. It is one FO.Term.rec at the motive 'forall f, decodeAux (add f (size t)) (code t) = t', so the recursor's arity fixes all four constructor cases and a skipped case is not possible.

Checker command

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

Evidence notes

Declared in crates/axeyum-lean-kernel/src/fo_roundtrip.rs by declare_decode_code, the same builder that produces FO.Formula.decode_code; the two differ only in the constructor table they are handed. 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_round_trip_theorems_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"
    }
  ]
}