A pairing of the naturals whose inverse is a plain structural recursion on the code

Identifier: F:fo-code-pairing-round-trip
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

FO.Code.pair a b := tri (a + b) + a is the index of (a, b) in the anti-diagonal enumeration of pairs of naturals, and FO.Code.unpair -- the iterate of a single step function from (0, 0) -- inverts it: unpair (pair a b) = Nat.Pair.mk a b for all a and b. The two scalar projections FO.Code.fst and FO.Code.snd read the components back, and left and right injectivity of the pairing follow.

Formal statement

theorem FO.Code.unpair_pair : ((x0 : AxNat) -> ((x1 : AxNat) -> Eq.{1} AxNat.Pair (FO.Code.unpair (FO.Code.pair x0 x1)) (AxNat.Pair.mk x0 x1)))

Dependencies

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

0 direct dependencies 6 direct dependents

Evidence

kernel-FO.Code.unpair_pair

Kind: kernel-term
Status: checked

Supports: FO.Code.unpair_pair is admitted by the trusted kernel gate with the type recorded in formal.statement, and rests on no axiom. The proof is ONE structural induction, on the CODE rather than on either component, at the motive P n := forall a b, pair a b = n -> unpair n = mk a b; the theorem is P (pair a b) applied to Eq.refl. The whole slice imports exactly four Nat theorems: zero_add, succ_add, succ_injective, succ_ne_zero.

Checker command

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

Evidence notes

The checker FAILS on absence rather than reporting an empty set: a named filter matching nothing exits 1. --exact matters here because FO.Code.pair also prefixes pair_succ, pair_zero_succ, pair_inj_left and pair_inj_right. Declared in crates/axeyum-lean-kernel/src/fo_code.rs by declare_unpair_pair.

the-enumeration-computes

Kind: kernel-term
Status: checked

Supports: pair, unpair, tri, step, fst and snd are Definitions, so admission says nothing about what they compute. Every one is pinned by Kernel::def_eq at concrete arguments: the whole enumeration for a + b <= 3 (ten entries, hand-listed in the test), unpair at all ten codes, tri at 0..5, and step at both of its branches. The asymmetry control pair 1 2 != pair 2 1 is what a transposed implementation (tri (a+b) + b) fails; it agrees with the intended one at every diagonal endpoint.

Checker command

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

Evidence notes

Seven tests. A step function with its two branches swapped is invisible at (0, 0) alone, which is why the table runs to a + b = 3 rather than stopping at the first diagonal.

footprint-whole-slice

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- for all 48 declarations the arithmetization package (fo_syntax + fo_code + fo_numbering + fo_decode) adds on top of the Nat prelude, not only the headline theorem. The row set is a SET DIFFERENCE against a kernel carrying only build_nat_prelude, recomputed on every run, so it is derived from the environment rather than from a hand-maintained list.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example fo_code_inventory -- --require-axiom-free --expect-count 48

Evidence notes

--expect-count fails on drift in EITHER direction, so a declaration silently disappearing is a failure too. The same set difference is recomputed inside the test suite by fo_numbering::tests::the_whole_chain_this_prelude_adds_is_axiom_free (42 rows, the numbering package) and fo_decode::tests::the_whole_arithmetization_package_is_axiom_free (48 rows, the whole chain), each with a coverage control requiring known names to be IN the difference so the sweep cannot pass vacuously.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum-lean-kernel build_fo_code_prelude, lane arithmetization (W3-7, ADR-1640)",
  "source": "authored from the roadmap item; the pairing is the classical Cantor anti-diagonal one, the inverse and both proofs are written here",
  "prior_art": [
    {
      "who": "Georg Cantor",
      "what": "the anti-diagonal enumeration of pairs of naturals",
      "year": 1878,
      "where": "Cantor, 'Ein Beitrag zur Mannigfaltigkeitslehre', Crelle 84 (1878)",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}