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

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

Recorded description

FO.Formula.decodeAux, given at least FO.Formula.size p units of fuel, returns p from FO.Formula.code p, for every one of the nine constructors. Stated additively -- for every p and every f, decodeAux (Nat.add f (size p)) (code p) = p -- with FO.Formula.decode_code_at_size as the f = Nat.zero corollary. The FO.Term fields of eqf, rel1 and rel2 are decoded at the FORMULA decoder's own fuel, which is why FO.Formula.size measures them with FO.Term.size and why this theorem consumes F:fo-term-decode-code rather than restating it.

Formal statement

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

Dependencies

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

4 direct dependencies 3 direct dependents

Evidence

kernel-FO.Formula.decode_code

Kind: kernel-term
Status: checked

Supports: FO.Formula.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.Formula.rec at the motive 'forall f, decodeAux (add f (size p)) (code p) = p', so the recursor's arity fixes all nine constructor cases.

Checker command

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

Evidence notes

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