Conway names, the simplicity hierarchy and the surreal number tree

PHILIP EHRLICH

A tree ⟨A,<ₛ⟩ is a partially ordered class such that for each x ∈ A, the class {y ∈ A : y <ₛ x} of predecessors of x, written ‘pr_A(x)’, is a set well ordered by <ₛ.

We prove that the usual ordering of ℕ is a tree in this sense.

instance instPartialOrderNat_marginis : PartialOrder ℕ

Equations

• instPartialOrderNat_marginis = LinearOrder.toPartialOrder

def «term_<ₛ_» : Lean.TrailingParserDescr

Equations

• «term_<ₛ_» = Lean.ParserDescr.trailingNode `term_<ₛ_ 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ₛ ") (Lean.ParserDescr.cat `term 0))

def «term_≤ₛ_» : Lean.TrailingParserDescr

Equations

• «term_≤ₛ_» = Lean.ParserDescr.trailingNode `term_≤ₛ_ 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₛ ") (Lean.ParserDescr.cat `term 0))

def pr (x : ℕ) : Type

Equations

• pr x = { y : ℕ // y < x }

instance instIsTrichotomousSubtypeNatLt_marginis (x : ℕ) : IsTrichotomous { y : ℕ // y < x } fun (u v : { y : ℕ // y < x }) => u < v

Equations

• ⋯ = ⋯

instance instIsTransSubtypeNatLt_marginis (x : ℕ) : IsTrans { y : ℕ // y < x } fun (u v : { y : ℕ // y < x }) => u < v

Equations

• ⋯ = ⋯

instance instIsWellFoundedSubtypeNatLt_marginis (x : ℕ) : IsWellFounded { y : ℕ // y < x } fun (u v : { y : ℕ // y < x }) => u < v

Equations

• ⋯ = ⋯

instance ehrlich_tree (x : ℕ) : IsWellOrder { y : ℕ // y < x } fun (u v : { y : ℕ // y < x }) => u < v

Equations

• ⋯ = ⋯

def branch (P : ℕ → Prop) : Prop

Equations

• branch P = ((WellFounded fun (a b : { k : ℕ // P k }) => a < b) ∧ ∀ (Q : ℕ → Prop), (WellFounded fun (a b : { k : ℕ // Q k }) => a < b) → (∀ (k : ℕ), P k → Q k) → ∀ (k : ℕ), P k ↔ Q k)

theorem branchℕ : branch fun (x : ℕ) => True

def pr' (x : List ℕ) : Type

Equations

• pr' x = { y : List ℕ // y <+: x }

theorem le_refl₀ (a : List ℕ) : a <+: a

theorem le_trans₀ (a : List ℕ) (b : List ℕ) (c : List ℕ) : a <+: b → b <+: c → a <+: c

theorem prefix_antisymm (a : List ℕ) (b : List ℕ) (h : a <+: b) (h₀ : b <+: a) : a = b

theorem lt_iff_le_not_le₀ (a : List ℕ) (b : List ℕ) : a <+: b ∧ a ≠ b ↔ a <+: b ∧ ¬b <+: a