Documentation

Formalizations.SetTheory.Ordinal.Gentzen.TwoPow

Choice-free `2 ^ α` and the cut-elimination inequalities below `ε₀` #

The height-doubling map twoPow' (2 ^ α) and the inequalities L1–L5 of Gentzen's cut elimination on Mathlib's ONote, stated with the syntactic order slt / sle and the syntactic normal form SNF of Formalizations.SetTheory.Ordinal.Gentzen.Acc, without Ordinal or repr. Writing α = ω·γ + m, twoPow' α = ω ^ γ · 2 ^ m. Syntactic addition sadd is Mathlib's ONote.add (as data), and ssucc is the syntactic successor.

All results before the bridge section depend only on propext. (Mathlib's ONote.opow and the core lemma Nat.pow_lt_pow_right depend on Classical.choice; they are not used.) The bridge section, which does use choice, proves that twoPow', sadd and ssucc denote 2 ^ α, α + β and α + 1, and that twoPow' agrees with Mathlib's ONote.opow, hence with Gentzen.Ordinals.twoPow.

Main results #

twoPow', ssucc, sadd, smax and their closure under SNF (SNF_twoPow', SNF_ssucc, SNF_sadd, SNF_smax);
twoPow'_slt, twoPow'_sle (L3), twoPow'_smax (L4);
L1, L2, L5 and the counterexamples L1_fails_at_zero, L2_fails_at_one;
twoPow'_add_le: 2^a + 2^b ≤ 2^(max a b + 1) (two-premise cut);
bridge: repr_sadd, repr_ssucc, repr_twoPow', twoPow'_eq_opow, ssucc_eq_add_one.

References #

B. Bryce, R. Goré, arXiv:2603.00487 (2026): Gentzen's consistency proof for PA in Coq.

Constructive facts about `cmp` #

theorem Gentzen.TwoPow.natCmp_of_lt {m n : ℕ} (h : m < n) :

cmp m n = Ordering.lt

theorem Gentzen.TwoPow.natCmp_self (n : ℕ) :

cmp n n = Ordering.eq

theorem Gentzen.TwoPow.two_pow_lt {i j : ℕ} (h : i < j) :

2 ^ i < 2 ^ j

2^i < 2^j for i < j (own proof; Nat.pow_lt_pow_right pulls Classical.choice).

theorem Gentzen.TwoPow.cmp_self (a : ONote) :

a.cmp a = Ordering.eq

theorem Gentzen.TwoPow.cmp_swap' (a b : ONote) :

(a.cmp b).swap = b.cmp a

theorem Gentzen.TwoPow.slt_irrefl (a : ONote) :

theorem Gentzen.TwoPow.cmp_gt_of_slt {a b : ONote} (h : Acc.slt a b) :

b.cmp a = Ordering.gt

theorem Gentzen.TwoPow.slt_of_cmp_gt {a b : ONote} (h : a.cmp b = Ordering.gt) :

theorem Gentzen.TwoPow.zero_slt_oadd (e : ONote) (n : ℕ+) (a : ONote) :

Acc.slt ONote.zero (e.oadd n a)

theorem Gentzen.TwoPow.exp_slt {γ γ' x y : ONote} {c d : ℕ+} (h : Acc.slt γ γ') :

Acc.slt (γ.oadd c x) (γ'.oadd d y)

theorem Gentzen.TwoPow.coef_slt {γ x y : ONote} {c d : ℕ+} (h : ↑c < ↑d) :

Acc.slt (γ.oadd c x) (γ.oadd d y)

Syntactic order `sle`, max, numerals #

def Gentzen.TwoPow.sle (a b : ONote) :

Weak syntactic order.

Equations

Gentzen.TwoPow.sle a b = (Gentzen.Acc.slt a b ∨ a = b)

Instances For

def Gentzen.TwoPow.smax (a b : ONote) :

Max via cmp.

Equations

Gentzen.TwoPow.smax a b = match a.cmp b with | Ordering.lt => b | x => a

Instances For

theorem Gentzen.TwoPow.smax_of_lt {a b : ONote} (h : a.cmp b = Ordering.lt) :

smax a b = b

theorem Gentzen.TwoPow.smax_of_eq {a b : ONote} (h : a.cmp b = Ordering.eq) :

smax a b = a

theorem Gentzen.TwoPow.smax_of_gt {a b : ONote} (h : a.cmp b = Ordering.gt) :

smax a b = a

theorem Gentzen.TwoPow.coef_sle {γ : ONote} {c d : ℕ+} (h : ↑c ≤ ↑d) :

sle (γ.oadd c ONote.zero) (γ.oadd d ONote.zero)

def Gentzen.TwoPow.one' :

The notation 1.

Equations

Gentzen.TwoPow.one' = ONote.zero.oadd 1 ONote.zero

Instances For

def Gentzen.TwoPow.two' :

The notation 2.

Equations

Gentzen.TwoPow.two' = ONote.zero.oadd 2 ONote.zero

Instances For

def Gentzen.TwoPow.num :

Finite numerals.

Equations

Gentzen.TwoPow.num 0 = ONote.zero
Gentzen.TwoPow.num k.succ = ONote.zero.oadd k.succPNat ONote.zero

Instances For

theorem Gentzen.TwoPow.num_slt {i j : ℕ} :

i < j → Acc.slt (num i) (num j)

theorem Gentzen.TwoPow.SNF_num (k : ℕ) :

Acc.SNF (num k)

Syntactic addition, successor, and 2^α #

def Gentzen.TwoPow.sadd (a b : ONote) :

Syntactic addition: Mathlib's ONote.add (data only; choice-free as a definition).

Equations

Gentzen.TwoPow.sadd a b = a.add b

Instances For

def Gentzen.TwoPow.ssucc :

ONote → ONote

Syntactic successor.

Equations

Gentzen.TwoPow.ssucc ONote.zero = Gentzen.TwoPow.one'
Gentzen.TwoPow.ssucc (ONote.zero.oadd n a) = ONote.zero.oadd (n + 1) a
Gentzen.TwoPow.ssucc (e.oadd n a) = e.oadd n (Gentzen.TwoPow.ssucc a)

Instances For

def Gentzen.TwoPow.dec :

ONote → ONote

"Left predecessor" of a nonzero exponent: 1 + dec e = e.

Equations

Gentzen.TwoPow.dec (ONote.zero.oadd n a) = Gentzen.TwoPow.num (↑n - 1)
Gentzen.TwoPow.dec x✝ = x✝

Instances For

def Gentzen.TwoPow.ssplit :

ONote → ONote × ℕ

Split α = ω·γ + m (γ, m) on Cantor normal forms.

Equations

Gentzen.TwoPow.ssplit ONote.zero = (ONote.zero , 0)
Gentzen.TwoPow.ssplit (ONote.zero.oadd n a) = (ONote.zero , ↑n)
Gentzen.TwoPow.ssplit (e.oadd n a) = ((Gentzen.TwoPow.dec e).oadd n (Gentzen.TwoPow.ssplit a).1, (Gentzen.TwoPow.ssplit a).2)

Instances For

def Gentzen.TwoPow.pow2 (m : ℕ) :

2 ^ m as a positive natural.

Equations

Gentzen.TwoPow.pow2 m = ⟨2 ^ m, ⋯⟩

Instances For

def Gentzen.TwoPow.twoPow' (a : ONote) :

2 ^ α = ω ^ γ · 2 ^ m where α = ω·γ + m.

Equations

Gentzen.TwoPow.twoPow' a = (Gentzen.TwoPow.ssplit a).1.oadd (Gentzen.TwoPow.pow2 (Gentzen.TwoPow.ssplit a).2) ONote.zero

Instances For

theorem Gentzen.TwoPow.ssplit_fin (n : ℕ+) (x : ONote) :

ssplit (ONote.zero.oadd n x) = (ONote.zero , ↑n)

theorem Gentzen.TwoPow.ssplit_inf (g z x : ONote) (m n : ℕ+) :

ssplit ((g.oadd m z).oadd n x) = ((dec (g.oadd m z)).oadd n (ssplit x).1, (ssplit x).2)

theorem Gentzen.TwoPow.ssplit_ssucc (a : ONote) :

ssplit (ssucc a) = ((ssplit a).1, (ssplit a).2 + 1)

SNF closure #

theorem Gentzen.TwoPow.snf_tail_zero {n : ℕ+} {x : ONote} (h : Acc.SNF (ONote.zero.oadd n x)) :

theorem Gentzen.TwoPow.dec_slt {e e' : ONote} :

Acc.SNF e → Acc.SNF e' → e ≠ ONote.zero → Acc.slt e e' → Acc.slt (dec e) (dec e')

theorem Gentzen.TwoPow.SNF_dec {e : ONote} :

Acc.SNF e → Acc.SNF (dec e)

theorem Gentzen.TwoPow.topBelow_ssplit {g z x : ONote} {m n : ℕ+} (h : Acc.SNF ((g.oadd m z).oadd n x)) :

Acc.topBelow (ssplit x).1 (dec (g.oadd m z))

theorem Gentzen.TwoPow.SNF_ssplit (a : ONote) :

Acc.SNF a → Acc.SNF (ssplit a).1

theorem Gentzen.TwoPow.SNF_twoPow' {a : ONote} (h : Acc.SNF a) :

Acc.SNF (twoPow' a)

theorem Gentzen.TwoPow.topBelow_ssucc {e : ONote} (he : Acc.slt ONote.zero e) {a : ONote} :

Acc.topBelow a e → Acc.topBelow (ssucc a) e

theorem Gentzen.TwoPow.SNF_ssucc {a : ONote} :

Acc.SNF a → Acc.SNF (ssucc a)

theorem Gentzen.TwoPow.SNF_addAux {e : ONote} (n : ℕ+) (he : Acc.SNF e) {o : ONote} :

Acc.SNF o → Acc.SNF (e.addAux n o)

theorem Gentzen.TwoPow.SNF_sadd {a b : ONote} :

Acc.SNF a → Acc.SNF b → Acc.SNF (sadd a b)

theorem Gentzen.TwoPow.SNF_smax {a b : ONote} (ha : Acc.SNF a) (hb : Acc.SNF b) :

Acc.SNF (smax a b)

L3: monotonicity #

theorem Gentzen.TwoPow.ssplit_mono (a b : ONote) :

Acc.SNF a → Acc.SNF b → Acc.slt a b → Acc.slt (ssplit a).1 (ssplit b).1 ∨ (ssplit a).1 = (ssplit b).1 ∧ (ssplit a).2 < (ssplit b).2

The split (γ, m) is lexicographically monotone.

theorem Gentzen.TwoPow.twoPow'_slt {a b : ONote} (ha : Acc.SNF a) (hb : Acc.SNF b) (h : Acc.slt a b) :

Acc.slt (twoPow' a) (twoPow' b)

L3 (strict).

theorem Gentzen.TwoPow.twoPow'_sle {a b : ONote} (ha : Acc.SNF a) (hb : Acc.SNF b) (h : sle a b) :

sle (twoPow' a) (twoPow' b)

L3 (weak).

L4: commutes with `smax` #

theorem Gentzen.TwoPow.twoPow'_smax {a b : ONote} (ha : Acc.SNF a) (hb : Acc.SNF b) :

twoPow' (smax a b) = smax (twoPow' a) (twoPow' b)

Addition of the special shapes #

theorem Gentzen.TwoPow.sadd_lt {γa γb x : ONote} {ca cb : ℕ+} (h : γa.cmp γb = Ordering.lt) :

sadd (γa.oadd ca ONote.zero) (γb.oadd cb x) = γb.oadd cb x

theorem Gentzen.TwoPow.sadd_eq {γa γb x : ONote} {ca cb : ℕ+} (h : γa.cmp γb = Ordering.eq) :

sadd (γa.oadd ca ONote.zero) (γb.oadd cb x) = γa.oadd (ca + cb) x

theorem Gentzen.TwoPow.sadd_gt {γa γb x : ONote} {ca cb : ℕ+} (h : γa.cmp γb = Ordering.gt) :

sadd (γa.oadd ca ONote.zero) (γb.oadd cb x) = γa.oadd ca (γb.oadd cb x)

theorem Gentzen.TwoPow.twoPow'_ssucc (a : ONote) :

twoPow' (ssucc a) = (ssplit a).1.oadd (pow2 ((ssplit a).2 + 1)) ONote.zero

theorem Gentzen.TwoPow.pow2_succ (m : ℕ) :

↑(pow2 (m + 1)) = 2 ^ m + 2 ^ m

theorem Gentzen.TwoPow.le_fin_part {a : ONote} {j : ℕ+} (ha : Acc.SNF a) (hγ : (ssplit a).1 = ONote.zero) (h : sle (ONote.zero.oadd j ONote.zero) a) :

↑j ≤ (ssplit a).2

If a is finite (γ = 0) and j ≤ a, then j ≤ m.

L1, L2, L5 #

theorem Gentzen.TwoPow.twoPow'_add_num_lt {a : ONote} {j : ℕ+} (hfin : (ssplit a).1 = ONote.zero → ↑j < 2 ^ (ssplit a).2) :

Acc.slt (sadd (twoPow' a) (ONote.zero.oadd j ONote.zero)) (twoPow' (ssucc a))

Generic form: 2^α + j < 2^(α+1) when j < 2^m in the finite case.

theorem Gentzen.TwoPow.L1 {a : ONote} (ha : Acc.SNF a) (h : sle one' a) :

Acc.slt (sadd (twoPow' a) one') (twoPow' (ssucc a))

L1. False at a = 0 (2^0 + 1 = 2^1).

theorem Gentzen.TwoPow.L2 {a : ONote} (ha : Acc.SNF a) (h : sle two' a) :

Acc.slt (sadd (twoPow' a) two') (twoPow' (ssucc a))

L2. False at a = 1 (2^1 + 2 = 2^2).

theorem Gentzen.TwoPow.L5 (a : ONote) :

Acc.slt (sadd (twoPow' a) two') (twoPow' (ssucc (ssucc a)))

L5. 2^α + 2 < 2^(α+2) for every α.

Two-premise cut bound #

theorem Gentzen.TwoPow.sum_bound_right {γa γb : ONote} {ma mb : ℕ} (h : Acc.slt γa γb ∨ γa = γb ∧ ma ≤ mb) :

sle (sadd (γa.oadd (pow2 ma) ONote.zero) (γb.oadd (pow2 mb) ONote.zero)) (γb.oadd (pow2 (mb + 1)) ONote.zero)

theorem Gentzen.TwoPow.sum_bound_left {γa γb : ONote} {ma mb : ℕ} (h : Acc.slt γb γa ∨ γb = γa ∧ mb ≤ ma) :

sle (sadd (γa.oadd (pow2 ma) ONote.zero) (γb.oadd (pow2 mb) ONote.zero)) (γa.oadd (pow2 (ma + 1)) ONote.zero)

theorem Gentzen.TwoPow.twoPow'_add_le {a b : ONote} (ha : Acc.SNF a) (hb : Acc.SNF b) :

sle (sadd (twoPow' a) (twoPow' b)) (twoPow' (ssucc (smax a b)))

Cut with premises of heights a, b: 2^a + 2^b ≤ 2^(max a b + 1).

Counterexamples at the excluded points (choice-free, by evaluation) #

theorem Gentzen.TwoPow.L1_fails_at_zero :

¬Acc.slt (sadd (twoPow' ONote.zero) one') (twoPow' (ssucc ONote.zero))

L1 fails at a = 0: 2^0 + 1 = 2 = 2^1.

theorem Gentzen.TwoPow.L2_fails_at_one :

¬Acc.slt (sadd (twoPow' one') two') (twoPow' (ssucc one'))

L2 fails at a = 1: 2^1 + 2 = 4 = 2^2.

Bridge to `Ordinal` (uses choice): these are the right functions #

theorem Gentzen.TwoPow.nf_of_snf {a : ONote} (h : Acc.SNF a) :

a.NF

theorem Gentzen.TwoPow.snf_of_nf {a : ONote} (h : a.NF) :

theorem Gentzen.TwoPow.repr_sadd (a b : ONote) [a.NF] [b.NF] :

(sadd a b).repr = a.repr + b.repr

theorem Gentzen.TwoPow.repr_ssucc (a : ONote) :

a.NF → (ssucc a).repr = a.repr + 1

theorem Gentzen.TwoPow.repr_num (k : ℕ) :

(num k).repr = ↑k

theorem Gentzen.TwoPow.one_add_repr_dec {e : ONote} :

e.NF → e ≠ ONote.zero → 1 + (dec e).repr = e.repr

theorem Gentzen.TwoPow.repr_ssplit (a : ONote) :

a.NF → a.repr = Ordinal.omega0 * (ssplit a).1.repr + ↑(ssplit a).2

theorem Gentzen.TwoPow.repr_twoPow' (a : ONote) (h : a.NF) :

(twoPow' a).repr = 2 ^ a.repr

twoPow' denotes 2 ^ α.

theorem Gentzen.TwoPow.twoPow'_eq_opow (a : ONote) [h : a.NF] :

twoPow' a = ↑2 ^ a

twoPow' agrees with Mathlib's ONote.opow (hence with Gentzen.Ordinals.twoPow, whose underlying notation is ONote.ofNat 2 ^ a).

theorem Gentzen.TwoPow.ssucc_eq_add_one (a : ONote) [h : a.NF] :

ssucc a = a + 1

Checks on samples (by `decide`) #

def Gentzen.TwoPow.samples :

Samples: 0, 1, 2, ω, ω+1, ω·2, ω^ω.

Equations

Gentzen.TwoPow.samples = [0, 1, ↑2, ONote.oadd 1 1 0, ONote.oadd 1 1 1, ONote.oadd 1 2 0, (ONote.oadd 1 1 0).oadd 1 0]

Instances For