The SELF-fuelled decoder inverts the numbering (OPEN, and NOT reachable from the size bound; the fuel-additive round trip IS proved)

Recorded description

FO.Formula.decode : Nat -> FO.Formula, which is decodeAux n n -- the code is its own fuel -- inverts the Goedel numbering: decode (code p) = p for every formula p. STILL NOT PROVED, and the reason changed. The FUEL-ADDITIVE round trip IS now proved (F:fo-formula-decode-code, F:fo-term-decode-code): decodeAux (Nat.add f (size p)) (code p) = p for every f. What that does NOT give is the self-fuelled wrapper, which would need Nat.le (size p) (code p) -- and that statement is FALSE, measured: FO.Formula.code FO.Formula.bot and FO.Term.code (FO.Term.var 0) are both Nat.zero while both sizes are 1, pinned by Kernel::def_eq in fo_roundtrip/tests.rs::size_is_not_bounded_by_the_code. So ADR-1640's item (3) is not an unproved lemma but a refuted one, and the remaining route is different work: a strong induction on the code using Nat.lt (FO.Code.snd n) n -- true, because FO.Code.pair a b is strictly larger than b -- which needs monotonicity of FO.Code.tri, a Nat.lt development on top of it, and a well-founded Nat recursion. That is a slice, not a step, and it buys only the removal of one Nat argument from four statements, which is why this lane routed every downstream theorem through fuel-explicit siblings (FO.Code.substCodeAux, FO.Code.isFormulaCodeAux, FO.Code.diagAux) instead.