Height doubling on normal ordinal notations below ε₀

The ordinal layer of Gentzen's cut elimination, on Mathlib's normal ordinal notations NONote (ordinals below ε₀): the height-doubling map twoPow a = 2 ^ a (computable, through NONote.opow) and the inequalities L1–L5 used to bound the height of a derivation after a cut is eliminated.

These statements go through NONote.repr and Mathlib's order on NONote, which is defined by repr, so they depend on Classical.choice (through Ordinal.lt_wf). The choice-free versions, stated with a syntactic order and normal form, are in Formalizations.SetTheory.Ordinal.Gentzen.Acc and Formalizations.SetTheory.Ordinal.Gentzen.TwoPow.

Main results

• twoPow, repr_twoPow: 2 ^ a as a normal notation;
• twoPow_lt_twoPow, twoPow_le_twoPow (L3), twoPow_max (L4);
• L1 (1 ≤ a → 2^a + 1 < 2^(a+1)) and L1_fails_at_zero;
• L2 (2 ≤ a → 2^a + 2 < 2^(a+1)) and L2_fails_at_one;
• L5 (2^a + 2 < 2^(a+2)), twoPow_add_le_max (2^a + 2^b ≤ 2^(max a b + 1));
• ti: transfinite induction below ε₀, from NONote.lt_wf.

References

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

Basic notations

@[instance_reducible]

instance Gentzen.Ordinals.instOneNONote_formalizations : One NONote

1 as a normal notation (Mathlib's NONote has no One instance).

Equations

• Gentzen.Ordinals.instOneNONote_formalizations = { one := NONote.ofNat 1 }

def Gentzen.Ordinals.two : NONote

2 as a normal notation.

Equations

• Gentzen.Ordinals.two = NONote.ofNat 2

@[simp]

theorem Gentzen.Ordinals.repr_ofNat (n : ℕ) : (NONote.ofNat n).repr = ↑n

@[simp]

theorem Gentzen.Ordinals.repr_one : NONote.repr 1 = 1

@[simp]

theorem Gentzen.Ordinals.repr_two : two.repr = 2

@[simp]

theorem Gentzen.Ordinals.repr_zero : NONote.repr 0 = 0

theorem Gentzen.Ordinals.lt_iff (a b : NONote) : a < b ↔ a.repr < b.repr

theorem Gentzen.Ordinals.le_iff (a b : NONote) : a ≤ b ↔ a.repr ≤ b.repr

theorem Gentzen.Ordinals.ext_repr {a b : NONote} (h : a.repr = b.repr) : a = b

The height-doubling map

def Gentzen.Ordinals.twoPow (a : NONote) : NONote

twoPow a is the notation of the ordinal 2 ^ a (computable, via ONote.opow).

Equations

• Gentzen.Ordinals.twoPow a = Gentzen.Ordinals.two.opow a

@[simp]

theorem Gentzen.Ordinals.repr_twoPow (a : NONote) : (twoPow a).repr = 2 ^ a.repr

theorem Gentzen.Ordinals.repr_add_one (a : NONote) : (a + 1).repr = Order.succ a.repr

theorem Gentzen.Ordinals.twoPow_succ (a : NONote) : (twoPow (a + 1)).repr = (twoPow a).repr + (twoPow a).repr

2^(a+1) = 2^a + 2^a.

theorem Gentzen.Ordinals.one_le_twoPow (a : NONote) : 1 ≤ (twoPow a).repr

L3: monotonicity

theorem Gentzen.Ordinals.twoPow_lt_twoPow {a b : NONote} (h : a < b) : twoPow a < twoPow b

theorem Gentzen.Ordinals.twoPow_le_twoPow {a b : NONote} (h : a ≤ b) : twoPow a ≤ twoPow b

theorem Gentzen.Ordinals.twoPow_strictMono : StrictMono twoPow

theorem Gentzen.Ordinals.twoPow_monotone : Monotone twoPow

L4: commutes with max

theorem Gentzen.Ordinals.twoPow_max (a b : NONote) : twoPow (max a b) = max (twoPow a) (twoPow b)

L1, L2: the tall-rule and disjunction-cut bounds

theorem Gentzen.Ordinals.two_le_twoPow {a : NONote} (h : 1 ≤ a) : 2 ≤ (twoPow a).repr

theorem Gentzen.Ordinals.L1 {a : NONote} (h : 1 ≤ a) : twoPow a + 1 < twoPow (a + 1)

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

theorem Gentzen.Ordinals.L1_fails_at_zero : ¬twoPow 0 + 1 < twoPow (0 + 1)

theorem Gentzen.Ordinals.L2 {a : NONote} (h : two ≤ a) : twoPow a + two < twoPow (a + 1)

L2. False at a = 1 (2^1 + 2 = 4 = 2^2), see L2_fails_at_one.

theorem Gentzen.Ordinals.L2_fails_at_one : ¬twoPow 1 + two < twoPow (1 + 1)

L5: bounds for a cut of height max + 2

theorem Gentzen.Ordinals.L5 (a : NONote) : twoPow a + two < twoPow (a + 1 + 1)

L5a. 2^a + 2 < 2^(a+2) for every a (no side condition).

theorem Gentzen.Ordinals.twoPow_add_le_max (a b : NONote) : twoPow a + twoPow b ≤ twoPow (max a b + 1)

L5b. Premises of heights a, b reduce to height at most 2^(max a b + 1).

Transfinite induction

theorem Gentzen.Ordinals.ti {P : NONote → Prop} (h : ∀ (a : NONote), (∀ b < a, P b) → P a) (a : NONote) : P a

Transfinite induction below ε₀, derived from NONote.lt_wf.

def Gentzen.Ordinals.omega : NONote

ω as a normal notation.

Equations

• Gentzen.Ordinals.omega = ⟨ONote.oadd 1 1 0, Gentzen.Ordinals.omega._proof_2⟩