Encodings: constructed Gödel / Ackermann, constructed quotient bijection

• fromNat / toNat is the Ackermann coding of hereditarily finite sets. toNat (fromNat n) = n is a theorem; the other direction holds as ExtEq (syntactic HF trees are not unique).
• subToNat / natToSub is a Gödel numbering of the ISK fragment.
• layerToNat / natToLayer is a constructed noncomputable bijection Nat ≃ InvariantLayer: enumerate OperEq classes in min-Gödel order (k-th least code of a class). Not canonical_rep. natToLayer_inverse is not rfl on raw Gödel numbers of non-minimal terms (godelClass 3).

ISK Gödel numbering via Mathlib pairing

def ISAR.iskToNat : ITerm → ℕ

Equations

• ISAR.iskToNat ISAR.ITerm.norm = 0
• ISAR.iskToNat ISAR.ITerm.konst = 1
• ISAR.iskToNat ISAR.ITerm.sₛ = 2
• ISAR.iskToNat (f · x_1) = Nat.pair (ISAR.iskToNat f) (ISAR.iskToNat x_1) + 3
• ISAR.iskToNat (ISAR.ITerm.var a) = 0
• ISAR.iskToNat ISAR.ITerm.dup = 0
• ISAR.iskToNat ISAR.ITerm.swap = 0
• ISAR.iskToNat ISAR.ITerm.comp = 0

def ISAR.subToNat (t : ISKSubtype) : ℕ

Equations

• ISAR.subToNat t = ISAR.iskToNat ↑t

@[irreducible]

def ISAR.natToSub : ℕ → ISKSubtype

Equations

• ISAR.natToSub 0 = ⟨ISAR.ITerm.norm, ISAR.ISKTerm.norm⟩
• ISAR.natToSub 1 = ⟨ISAR.ITerm.konst, ISAR.ISKTerm.konst⟩
• ISAR.natToSub 2 = ⟨ISAR.ITerm.sₛ, ISAR.ISKTerm.sₛ⟩
• ISAR.natToSub n.succ.succ.succ = ⟨↑(ISAR.natToSub (Nat.unpair n).1) · ↑(ISAR.natToSub (Nat.unpair n).2), ⋯⟩

theorem ISAR.subToNat_inverse (t : ISKSubtype) : natToSub (subToNat t) = t

theorem ISAR.natToSub_inverse (n : ℕ) : subToNat (natToSub n) = n

Ackermann coding Nat → HF

def ISAR.fromNatInsert (n : ℕ) (rec : (m : ℕ) → m < n → HF) : ℕ → HF

Equations

• ISAR.fromNatInsert n rec 0 = HF.empty
• ISAR.fromNatInsert n rec k.succ = if h : k < n then if n.testBit k = true then (rec k h).insert (ISAR.fromNatInsert n rec k) else ISAR.fromNatInsert n rec k else ISAR.fromNatInsert n rec k

@[irreducible]

def ISAR.fromNat (n : ℕ) : HF

Equations

• ISAR.fromNat n = ISAR.fromNatInsert n (fun (m : ℕ) (x : m < n) => ISAR.fromNat m) n

theorem ISAR.nat_lt_two_pow (k : ℕ) : k < 2 ^ k

theorem ISAR.fromNatInsert_testBit (n : ℕ) (rec : (m : ℕ) → m < n → HF) (hrec : ∀ (m : ℕ) (hm : m < n), toNat (rec m hm) = m) (k i : ℕ) : (toNat (fromNatInsert n rec k)).testBit i = (decide (i < k) && n.testBit i)

theorem ISAR.toNat_fromNat (n : ℕ) : toNat (fromNat n) = n

theorem ISAR.fromNat_toNat_ext (x : HF) : ExtEq (fromNat (toNat x)) x

Syntactic HF trees are not unique; Ackermann codes identify extensionally equal sets.

Countable bijection on the OperEq quotient (min-Gödel enumeration)

def ISAR.godelClass (n : ℕ) : InvariantLayer

The OperEq class of the ISK term with Gödel number n. Surjective, not injective.

Equations

• ISAR.godelClass n = ⟦ISAR.natToSub n⟧

theorem ISAR.godelClass_surjective (q : InvariantLayer) : ∃ (n : ℕ), godelClass n = q

noncomputable def ISAR.minCode (q : InvariantLayer) : ℕ

Least Gödel number of an OperEq class.

Equations

• ISAR.minCode q = Nat.find ⋯

theorem ISAR.minCode_spec (q : InvariantLayer) : godelClass (minCode q) = q

theorem ISAR.minCode_min {q : InvariantLayer} {m : ℕ} (hm : m < minCode q) : godelClass m ≠ q

def ISAR.isMinCode (n : ℕ) : Prop

n is the least Gödel number of its class.

Equations

• ISAR.isMinCode n = ∀ m < n, ISAR.godelClass m ≠ ISAR.godelClass n

theorem ISAR.isMinCode_zero : isMinCode 0

theorem ISAR.minCode_isMin (q : InvariantLayer) : isMinCode (minCode q)

theorem ISAR.minCode_eq_iff (n : ℕ) : minCode (godelClass n) = n ↔ isMinCode n

noncomputable def ISAR.minCodeRank (n : ℕ) : ℕ

Rank of a min-code among all strictly smaller min-codes.

Equations

• ISAR.minCodeRank n = (Finset.filter ISAR.isMinCode (Finset.range n)).card

theorem ISAR.minCodeRank_mono {n m : ℕ} (hn : isMinCode n) (hlt : n < m) : minCodeRank n < minCodeRank m

theorem ISAR.minCodeRank_inj {n m : ℕ} (hn : isMinCode n) (hm : isMinCode m) (heq : minCodeRank n = minCodeRank m) : n = m

theorem ISAR.minCodeRank_lt_of_mem {N n : ℕ} (hn : n ∈ Finset.filter isMinCode (Finset.range N)) : minCodeRank n < (Finset.filter isMinCode (Finset.range N)).card

theorem ISAR.exists_minCode_of_rank_aux {N k : ℕ} (hk : k < (Finset.filter isMinCode (Finset.range N)).card) : ∃ n < N, isMinCode n ∧ minCodeRank n = k

def ISAR.kSpine : ℕ → ITerm

Equations

• ISAR.kSpine 0 = ISAR.ITerm.konst
• ISAR.kSpine k.succ = ISAR.ITerm.konst · ISAR.kSpine k

theorem ISAR.kSpine_ISK (n : ℕ) : ISKTerm (kSpine n)

def ISAR.kSpineSub (n : ℕ) : ISKSubtype

Equations

• ISAR.kSpineSub n = ⟨ISAR.kSpine n, ⋯⟩

theorem ISAR.kSpine_NormalI (n : ℕ) : NormalI (kSpine n)

theorem ISAR.kSpine_injective {i j : ℕ} (h : kSpine i = kSpine j) : i = j

theorem ISAR.kSpine_OperEq_eq {i j : ℕ} (h : OperEq (kSpineSub i) (kSpineSub j)) : i = j

theorem ISAR.kSpine_layer_inj {i j : ℕ} (h : toInvariantLayer (kSpineSub i) = toInvariantLayer (kSpineSub j)) : i = j

theorem ISAR.minCode_kSpine_inj {i j : ℕ} (h : minCode (toInvariantLayer (kSpineSub i)) = minCode (toInvariantLayer (kSpineSub j))) : i = j

theorem ISAR.exists_minCode_of_rank (k : ℕ) : ∃ (n : ℕ), isMinCode n ∧ minCodeRank n = k

noncomputable def ISAR.minCodeEnum (k : ℕ) : ℕ

k-th least min-Gödel code (enumeration of distinct OperEq classes).

Equations

• ISAR.minCodeEnum k = Nat.find ⋯

theorem ISAR.minCodeEnum_isMin (k : ℕ) : isMinCode (minCodeEnum k)

theorem ISAR.minCodeEnum_rank (k : ℕ) : minCodeRank (minCodeEnum k) = k

noncomputable def ISAR.layerToNat (q : InvariantLayer) : ℕ

Index of an OperEq class in min-Gödel order. Not the raw Gödel number.

Equations

• ISAR.layerToNat q = ISAR.minCodeRank (ISAR.minCode q)

noncomputable def ISAR.natToLayer (k : ℕ) : InvariantLayer

The k-th OperEq class in min-Gödel order. Not Quotient.mk (natToSub k).

Equations

• ISAR.natToLayer k = ISAR.godelClass (ISAR.minCodeEnum k)

theorem ISAR.layerToNat_inverse (q : InvariantLayer) : natToLayer (layerToNat q) = q

theorem ISAR.natToLayer_inverse (n : ℕ) : layerToNat (natToLayer n) = n

theorem ISAR.godelClass_three_eq_zero : godelClass 3 = godelClass 0

Raw Gödel number 3 is norm · norm, which joins to norm (code 0). The inverse is therefore not rfl on non-minimal codes.

theorem ISAR.layerToNat_godelClass_three_ne : layerToNat (godelClass 3) ≠ 3

noncomputable def ISAR.HF_encode (c : HF) : InvariantLayer

Equations

• ISAR.HF_encode c = ISAR.natToLayer (toNat c)

noncomputable def ISAR.encode_raw (c : HF) : ISKSubtype

Equations

• ISAR.encode_raw c = (ISAR.HF_encode c).canonical_rep

noncomputable def ISAR.decode_layer (q : InvariantLayer) : HF

Equations

• ISAR.decode_layer q = ISAR.fromNat (ISAR.layerToNat q)

noncomputable def ISAR.decode_term (t : ISKSubtype) : HF

Equations

• ISAR.decode_term t = ISAR.decode_layer ⟦t⟧

theorem ISAR.decode_layer_HF_encode (c : HF) : ExtEq (decode_layer (HF_encode c)) c

theorem ISAR.HF_encode_decode_layer (q : InvariantLayer) : HF_encode (decode_layer q) = q

theorem ISAR.decode_term_encode_raw (c : HF) : ExtEq (decode_term (encode_raw c)) c

theorem ISAR.encode_raw_decode_term (t : ISKSubtype) : OperEq (encode_raw (decode_term t)) t

theorem ISAR.HF_encode_eq_of_ExtEq {c1 c2 : HF} (h : ExtEq c1 c2) : HF_encode c1 = HF_encode c2