Megalodon 1.8 (23257 "Conjectures")

by Brown, Saturday, November 27, 2021, 12:09 (8 days ago) @ Brown

Here's one of the provable ones:

Variable x:set.
Variable y:set.
Variable z:set.
Variable w:set.
Hypothesis H0: SNo x.
Hypothesis H1: SNo y.
Hypothesis H2: SNo z.
Hypothesis H3: (forall u:set, u :e SNoS_ (SNoLev x) -> u + y + z = (u + y) + z).
Hypothesis H4: SNo (x + y).
Hypothesis H5: w :e SNoL x.
Hypothesis H7: w < x.
Theorem Conj_add_SNo_assoc__12__6: w + y + z = (w + y) + z -> (w + y + z) < (x + y) + z.

This comes from the middle of the proof of associativity of addition on surreals. The assumption that w is a surreal number has been dropped. However, assumptions H0 and H5 imply w is a surreal number:

claim L1: SNo w.
{ apply SNoL_E x H0 w H5.
assume Hw _ _. exact Hw.
}

From this we can finish the proof. Note that the proof does not use H3 and could avoid using assumuptions H4 and H7, so three of the other conjectures corresponding to this property would be similarly provable.

assume H8: w + y + z = (w + y) + z.
rewrite H8.
prove (w + y) + z < (x + y) + z.
apply add_SNo_Lt1 (w + y) z (x + y).
- prove SNo (w + y).
exact SNo_add_SNo w y L1 H1.
- prove SNo z. exact H2.
- prove SNo (x + y). exact H4.
- prove w + y < x + y.
apply add_SNo_Lt1 w y x.
+ prove SNo w. exact L1.
+ prove SNo y. exact H1.
+ prove SNo x. exact H0.
+ prove w < x. exact H7.
Qed.