feat: sign expansion of surreal

[plp127]

We define the truncation of a surreal and prove a uniquely characterizing property. We define the sign expansion of a surreal as the sequence of inequalities with its truncations. We prove the birthday of a surreal is the length of its sign sequence, and that the sign sequence of the truncation of a surreal is the truncation of its sign sequence. We show that taking the sign sequence of a surreal defines an order isomorphism with the subset of sign sequences of ordinal length.

[vihdzp]

The analogous function on sign expansions is called restrict, so maybe this should too?

[plp127]

This operation doesn't really feel like "restricting" the surreal, so I wouldn't like this rename.

[vihdzp]

Conversely, should restrict be renamed to truncate? Or maybe trunc to match HahnSeries.trunc.

[plp127]

these are certainly possibilities

[vihdzp]

Is it any easier to define truncate o x = !{{y < x| y.birthday < o} | {y > x| y.birthday < o}}? That is, without going through IGame. If not, can we at least have this as a lemma?

[plp127]

There's not enough API for inequalities of ofSets in Surreal for this to work easily.

[vihdzp]

If it doesn't work easily, then we should make it work easily! After #402, this works:

def truncate (o : NatOrdinal) : Surreal →o Surreal where
  toFun x := !{Set.Iio x ∩ {y | y.birthday < o} | Set.Ioi x ∩ {y | y.birthday < o}}'(by
    aesop (add apply unsafe [lt_trans])
  )
  monotone' x y hxy := by
    rw [Surreal.ofSets_le_ofSets_iff]
    aesop (add apply unsafe [lt_of_le_of_lt, lt_of_lt_of_le])

[vihdzp]

Would it be worth making a subtype SmallSignExpansion? That way ofSurreal could be an order isomorphism.

[plp127]

There are approximately three things we care about that can be represented as sign expansions:

• surreals correspond to sign expansions which are eventually 0
• numeric cuts (something in the range of leftSurreal or rightSurreal) correspond to sign expansions which end in a + followed by all -s or a - followed by all +s
• short cuts (those with an ordinal birthday) correspond to sign expansions which are either eventually constant + or eventually constant constant -
• arbitrary cuts correspond to sign expansions without 0s

[vihdzp]

Do you think #395 is a good idea? If so, what about defining SignExpansion.toSurreal (x : SignExpansion) (hx : Short x) : Surreal by using this theorem?

[vihdzp]

Do you think #395 is a good idea? If so, what about defining SignExpansion.toSurreal (x : SignExpansion) (hx : Short x) : Surreal by using this theorem?

[plp127]

-awaiting-author

[vihdzp]

These are unused now.

Suggested change

	public theorem ite_lt_iff {α : Type*} [LT α] {P : Prop} [Decidable P] {a b c : α} :
	(if P then a else b) < c ↔ P ∧ a < c ∨ ¬P ∧ b < c := by split <;> simp_all
	public theorem lt_ite_iff {α : Type*} [LT α] {P : Prop} [Decidable P] {a b c : α} :
	a < (if P then b else c) ↔ P ∧ a < b ∨ ¬P ∧ a < c := by split <;> simp_all
	public theorem ite_le_iff {α : Type*} [LE α] {P : Prop} [Decidable P] {a b c : α} :
	(if P then a else b) ≤ c ↔ P ∧ a ≤ c ∨ ¬P ∧ b ≤ c := by split <;> simp_all
	public theorem le_ite_iff {α : Type*} [LE α] {P : Prop} [Decidable P] {a b c : α} :
	a ≤ (if P then b else c) ↔ P ∧ a ≤ b ∨ ¬P ∧ a ≤ c := by split <;> simp_all

[vihdzp]

For consistency

Suggested change

	# Sign Expansions
	# Sign expansions

[vihdzp]

The file SignExpansion/Basic already defines what a sign expansion is. This docstring should rather explain how the correspondence works. Maybe something like:

In this file we define the correspondence between surreals and sign expansions. This map can be
uniquely characterized as the order-preserving map such that every surreal gets mapped to a sign
sequence whose length equals its birthday.

[vihdzp]

This is what I meant, makes more sense to me to have all the haves together.

Suggested change

	rw [lt_iff_toLex]
	have hdcc (d : Surreal) (hd : d.birthday < c.birthday) : d ∉ Set.Icc x y := by
	contrapose! hd
	apply Cut.birthday_simplestBtwn_le_of_fits
	exact hd
	have hcxy (j : NatOrdinal) (hj : j ≤ c.birthday)
	(z : Surreal) (hz : z ∈ Set.Icc x y) : z.truncate j = c.truncate j := by
	apply truncate_eq_of_birthday_le_of_forall_lt_gt_iff (birthday_truncate_le j c) <;> grind
	have hdcc (d : Surreal) (hd : d.birthday < c.birthday) : d ∉ Set.Icc x y := by
	contrapose! hd
	apply Cut.birthday_simplestBtwn_le_of_fits
	exact hd
	have hcxy (j : NatOrdinal) (hj : j ≤ c.birthday)
	(z : Surreal) (hz : z ∈ Set.Icc x y) : z.truncate j = c.truncate j := by
	apply truncate_eq_of_birthday_le_of_forall_lt_gt_iff (birthday_truncate_le j c) <;> grind
	rw [lt_iff_toLex]

[vihdzp]

If it doesn't work easily, then we should make it work easily! After #402, this works:

def truncate (o : NatOrdinal) : Surreal →o Surreal where
  toFun x := !{Set.Iio x ∩ {y | y.birthday < o} | Set.Ioi x ∩ {y | y.birthday < o}}'(by
    aesop (add apply unsafe [lt_trans])
  )
  monotone' x y hxy := by
    rw [Surreal.ofSets_le_ofSets_iff]
    aesop (add apply unsafe [lt_of_le_of_lt, lt_of_lt_of_le])