Skip to content

Commit

Permalink
State and prove Theorem 2.36 (#202)
Browse files Browse the repository at this point in the history 
* Add theorems `Finite.Equation28394_implies_Equation2` and
`Equation28394_not_implies_Equation2` closing #125.
* Introduce Equation28394, a fixed version of Equation28393.

---------

Co-authored-by: teorth <tao@math.ucla.edu>
  • Loading branch information
@jscanvic @teorth
jscanvic and teorth authored Oct 7, 2024
1 parent 81bc942 commit 75b8b81
Show file tree
Hide file tree
Showing 4 changed files with 349 additions and 8 deletions.
10 changes: 5 additions & 5 deletions blueprint/src/chapter/infinite_models.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,15 +7,15 @@ \chapter{Infinite models}\label{infinite-model-chapter}
We note some selected laws of order more than $5$, used for such non-implications.

\begin{definition}[Equation 5105]
\label{eq5105}\uses{magma-def}\lean{Equation28393}\leanok
\label{eq5105}\uses{magma-def}\lean{Equation5105}\leanok
Equation 5105 is the law $0 \formaleq 1 \op (1 \op (1 \op (0 \op (2 \op 1))))$ (or the equation $x = y \op (y \op (y \op (x \op (z \op y))))$).
\end{definition}

This law of order $5$ was mentioned in \cite{Kisielewicz2}.

\begin{definition}[Equation 28393]
\label{eq28393}\uses{magma-def}\lean{Equation28393}\leanok
Equation 28393 is the law $0 \formaleq (((0 \op 0) \op 0) \op 1) \op (0 \op 2)$ (or the equation $x = (((x \op x) \op x) \op y) \op (x \op z)$).
\begin{definition}[Equation 28770]
\label{eq28770}\uses{magma-def}\lean{Equation28770}\leanok
Equation 28770 is the law $0 \formaleq (((1 \op 1) \op 1) \op 0) \op (1 \op 2)$ (or the equation $x = (((y \op y) \op y) \op x) \op (y \op z)$).
\end{definition}

This law of order $5$ was introduced by Kisielewicz \cite{Kisielewicz}.
Expand Down Expand Up @@ -65,7 +65,7 @@ \chapter{Infinite models}\label{infinite-model-chapter}

An even shorter law (order $5$) was obtained by the same author in a follow-up paper \cite{Kisielewicz2}:

\begin{theorem}[Kisielewicz's second Austin law]\label{kis-thm2}\uses{eq2, eq28393} \Cref{eq28393} is an Austin law.
\begin{theorem}[Kisielewicz's second Austin law]\label{kis-thm2}\uses{eq2, eq28770} \Cref{eq28770} is an Austin law.
\end{theorem}

\begin{proof} Using the $y^2$ and $y^3$ notation as before, the law reads
Expand Down
4 changes: 3 additions & 1 deletion equational_theories/Equations.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,8 +123,10 @@ abbrev Equation4656 (G: Type _) [Magma G] := ∀ x y z : G, (x ◇ y) ◇ y = (x
/-- Mentioned in a paper of Kisielewicz as a conjectural Austin law -/
equation 5105 := x = y ◇ (y ◇ (y ◇ (x ◇ (z ◇ y))))

equation 28381 := x = (((x ◇ x) ◇ x) ◇ y) ◇ (x ◇ z)

/-- Kisielewicz's second Austin law -/
equation 28393 := x = (((x ◇ x) ◇ x) ◇ y) ◇ (x ◇ z)
equation 28770 := x = (((y ◇ y) ◇ y) ◇ x) ◇ (y ◇ z)

/- Some order 6 laws -/

Expand Down
339 changes: 339 additions & 0 deletions equational_theories/InfModel.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,345 @@ theorem Finite.Equation5105_implies_Equation2 (G : Type*) [Magma G] [Finite G] (
_= x ◇ (x ◇ (x ◇ (y ◇ (x ◇ x)))) := by rw [hhhh]
_= y := by rw [← h y x x]

theorem Finite.Equation28770_implies_Equation2 (G : Type*) [Magma G] [Finite G] (h : Equation28770 G) :
Equation2 G := by
have : ∀ (y z u : G), y ◇ z = y ◇ u := by
intro y
let f (x : G) := ((y ◇ y) ◇ y) ◇ x
let g (x : G) := x ◇ (y ◇ y)
have : Function.RightInverse f g := by
intro x
simp [f, g, ← h]
intro z u
apply this.injective
obtain ⟨finv, hf⟩ := (Finite.surjective_of_injective this.injective).hasRightInverse
let fy := finv ((y ◇ y) ◇ y)
replace hf : ((y ◇ y) ◇ y) ◇ fy = (y ◇ y) ◇ y := hf _
have := h fy y
simp only [hf] at this
simp [f, ← this]
intro x u
have y := x
have z := x
rw [h x y z, this ((y ◇ y) ◇ y) x u, ← this ((y ◇ y) ◇ y) u u, ← h]

theorem Equation28770_not_implies_Equation2 : ∃ (G : Type) (_ : Magma G), Equation28770 G ∧ ¬Equation2 G := by
have : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
have : Fact (Nat.Prime 3) := ⟨Nat.prime_three⟩
have : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩
letI : Magma ℕ+ := { op := fun a b ↦ if a = b then 2^b.val else
if a = 2^b.val then 3^b.val else
if a = 3^(padicValNat 3 a) then a * 5^b.val else
if a = 3^(padicValNat 3 a) * 5^(padicValNat 5 a) then Nat.toPNat' (padicValNat 5 a) else
if a = 2^(3^(padicValNat 3 (padicValNat 2 a))) then 3^(padicValNat 3 (padicValNat 2 a)) else 1}
refine ⟨ℕ+, this, ⟨?_, fun x ↦ nomatch (x 1 2)⟩⟩
intro x y z
-- t1 is from the proof of Equation374794_not_implies_Equation2
have t1 (y : ℕ+) : 2 ^ (y : ℕ) ≠ y := by
apply_fun PNat.val
simp [ne_of_gt, Nat.lt_pow_self]
have h1 : ∀ (y: ℕ+), y ◇ y = 2^y.val := by
intro y
unfold Magma.op
simp only [ite_true]
have h2 : ∀ (y: ℕ+), (2^y.val) ◇ y = 3^y.val := by
intro y
unfold Magma.op
simp [t1]
have h3 : ∀ (x y: ℕ+), x ≠ 3^y.val → (3^y.val) ◇ x = 3^y.val * 5^x.val := by
intro x y hxy
unfold Magma.op
simp
rw [if_neg]
case hnc =>
intro h''
apply hxy
simp [h'']
simp
contrapose
intro _
apply_fun PNat.val
simp only [PNat.pow_coe, PNat.val_ofNat, ne_eq]
intro nh
apply eq_of_prime_pow_eq at nh
· contradiction
· exact Nat.prime_three.prime
· exact Nat.prime_two.prime
· simp
have h4 : ∀ (x y z: ℕ+), z ≠ 3^y.val * 5^x.val → (3^y.val * 5^x.val) ◇ z = x := by
intro x y z hxyz
unfold Magma.op
simp
rw [if_neg]
case hnc =>
intro h'
apply hxyz
simp [h']
rw [if_neg]
case hnc =>
apply_fun PNat.val
simp [PNat.pow_coe, PNat.val_ofNat, ne_eq]
intro nh
apply PNat.ne_zero z
calc ↑z
_ = padicValNat 2 (3^y.val * 5^x.val) := by simp [nh]
_ = 0 := by simp [padicValNat.mul, padicValNat_prime_prime_pow]
rw [if_neg]
case hnc =>
intro hc
apply PNat.ne_zero x
calc ↑x
_ = padicValNat 5 ↑((3: ℕ+)^y.val * (5: ℕ+)^x.val) := by simp [padicValNat_prime_prime_pow, padicValNat.mul]
_ = padicValNat 5 ((3: ℕ+)^(padicValNat (3: ℕ) ((3: ℕ)^y.val * (5: ℕ)^x.val))) := by simp [hc]
_ = 0 := by simp [padicValNat_prime_prime_pow]
rw [if_pos]
case hc =>
simp [padicValNat.mul, padicValNat_prime_prime_pow]
simp [this, Subtype.ext_iff, padicValNat.mul, padicValNat_prime_prime_pow]
have h5 : ∀ (y z: ℕ+), z ≠ 3^y.val ∧ z ≠ 2^(3^y.val) → (2^(3^y.val)) ◇ z = 3^y.val := by
intro y z hyz
unfold Magma.op
simp
rw [if_neg, if_neg, if_neg, if_neg]
.
intro hc
apply PNat.ne_zero ((3: ℕ+)^y.val)
calc ↑((3: ℕ+)^y.val)
_ = padicValNat 2 ↑(2^3^y.val: ℕ+) := by simp
_ = padicValNat 2 _ := by rw [hc]
_ = 0 := by simp [padicValNat_prime_prime_pow]
.
intro hc
apply PNat.ne_zero ((3: ℕ+)^y.val)
calc ↑((3: ℕ+)^y.val)
_ = padicValNat 2 ↑(2^3^y.val: ℕ+) := by simp
_ = padicValNat 2 _ := by rw [hc]
_ = 0 := by simp [padicValNat_prime_prime_pow]
.
intro hc
apply hyz.1
calc z
_ = z.val.toPNat' := by simp
_ = (padicValNat 2 (2^z.val: ℕ+)).toPNat' := by simp
_ = (padicValNat 2 ↑(2^3^y.val: ℕ+)).toPNat' := by rw [←hc]
_ = (3^y.val: ℕ).toPNat' := by simp
_ = 3^↑y := by rw [←PNat.coe_inj]; simp
.
intro hc
apply hyz.2
simp [hc]
rw [h1, h2]
by_cases hx : x = 3^y.val
.
rw [hx, h1]
by_cases hyz : y ◇ z = 2^(3^y.val)
.
simp [hyz, h1]
exfalso
have : padicValNat 2 ↑(y ◇ z) = ↑(3^y.val) := by simp [hyz]
unfold Magma.op at this
simp at this
repeat rw [apply_ite PNat.val] at this
repeat rw [apply_ite (padicValNat 2)] at this
simp only [PNat.pow_coe, PNat.val_ofNat] at this
simp only [padicValNat.prime_pow] at this
simp [padicValNat_prime_prime_pow] at this
repeat rw [apply_ite (padicValNat 2)] at this
simp [padicValNat.mul, padicValNat_prime_prime_pow] at this
repeat simp only [ite_eq_iff] at this
simp at this
have this' : (0: ℕ) = (3: ℕ)^y.val ↔ False := by
apply Iff.intro
.
simp
intro h
apply pow_ne_zero y.val (by simp: 3 ≠ 0)
simp [h]
.
intro h
contradiction
simp [this'] at this
repeat simp [and_or_left, and_or_left] at this
cases this with
| inl h =>
rw [h.1] at h
simp at h
have this2 := Nat.lt_pow_self (by simp: 1 < 3) z.val
have this3 := ne_of_gt this2
exact this3 (Eq.symm h)
| inr this => _
cases this with
| inl h =>
have h1 := h.2.2.1
have h2 := h.2.2.2
rw [h1] at h2
simp at h2
simp [padicValNat_prime_prime_pow] at h2
have h2 := Eq.symm h2
have := pow_ne_zero (3^padicValNat 3 y.val) (by simp: 3 ≠ 0)
apply pow_ne_zero y.val (by simp: 3 ≠ 0)
contradiction
| inr this => _
have this' := this.2.2.2.2.2
apply_fun padicValNat 3 at this'
simp [padicValNat.prime_pow] at this'
have this' := Eq.symm this'
have this2 := calc y.val
_ > Nat.log 5 y.val := by simp [Nat.log_lt_self]
_ ≥ padicValNat 5 y.val := by simp [padicValNat_le_nat_log]
_ ≥ Nat.log 2 (padicValNat 5 y.val) := by simp [Nat.log_le_self]
_ ≥ padicValNat 2 (padicValNat 5 y.val) := by simp [padicValNat_le_nat_log]
_ ≥ Nat.log 3 (padicValNat 2 (padicValNat 5 y.val)) := by simp [Nat.log_le_self]
_ ≥ padicValNat 3 (padicValNat 2 (padicValNat 5 y.val)) := by simp [padicValNat_le_nat_log]
have this3 := ne_of_gt this2
exact this3 this'
.
by_cases hyz' : y ◇ z = 3^y.val
.
rw [←hyz', h2, hyz']
exfalso
have : padicValNat 3 ↑(y ◇ z) = ↑y.val := by simp [hyz']
unfold Magma.op at this
simp at this
repeat rw [apply_ite PNat.val] at this
repeat rw [apply_ite (padicValNat 3)] at this
simp only [PNat.pow_coe, PNat.val_ofNat] at this
simp only [padicValNat.prime_pow] at this
simp [padicValNat_prime_prime_pow] at this
repeat rw [apply_ite (padicValNat 3)] at this
simp [padicValNat.mul, padicValNat_prime_prime_pow] at this
repeat simp only [ite_eq_iff] at this
simp at this
have this' : ((0: ℕ) = y.val) ↔ False := by
simp [false_iff]
intro hc
have hc := Eq.symm hc
have hc' := PNat.ne_zero y
contradiction
simp [this'] at this
repeat simp [and_or_left, and_or_left] at this
cases this with
| inl h =>
have h1 := h.2.1
have h2 := h.2.2
rw [h2] at h1
have h1 := Eq.symm h1
apply_fun PNat.val at h1
simp at h1
have this2 := Nat.lt_pow_self (by simp: 1 < 2) y.val
have this3 := ne_of_gt this2
exact this3 h1
| inr this => _
cases this with
| inl h =>
have h1 := h.2.2.1
have h2 := h.2.2.2
rw [h2] at h1
have h1 := Eq.symm h1
apply_fun PNat.val at h1
simp at h1
have this2 := Nat.lt_pow_self (by simp: 1 < 3) y.val
have this3 := ne_of_gt this2
exact this3 h1
| inr this => _
cases this with
| inl h =>
have h := Eq.symm h.2.2.2.2.2
have h' := calc y.val
_ > Nat.log 5 y.val := by simp [Nat.log_lt_self]
_ ≥ padicValNat 5 y.val := by simp [padicValNat_le_nat_log]
_ ≥ Nat.log 3 (padicValNat 5 y.val) := by simp [Nat.log_le_self]
_ ≥ padicValNat 3 (padicValNat 5 y.val) := by simp [padicValNat_le_nat_log]
exact (ne_of_gt h') h
| inr this => _
have this := Eq.symm this.2.2.2.2.2
have this' := calc y.val
_ > Nat.log 2 y.val := by simp [Nat.log_lt_self]
_ ≥ padicValNat 2 y.val := by simp [padicValNat_le_nat_log]
_ ≥ Nat.log 3 (padicValNat 2 y.val) := by simp [Nat.log_le_self]
_ ≥ padicValNat 3 (padicValNat 2 y.val) := by simp [padicValNat_le_nat_log]
exact (ne_of_gt this') this
.
have : (y ◇ z) ≠ 3^y.val ∧ (y ◇ z) ≠ 2^(3^y.val) := And.intro hyz' hyz
simp [h5 y (y ◇ z) this]
.
rw [h3 x y hx]
by_cases hyz : y ◇ z = 3^y.val * 5^x.val
.
rw [hyz, h1]
exfalso
unfold Magma.op at hyz
simp at hyz
simp only [PNat.pow_coe, PNat.val_ofNat] at hyz
repeat simp only [ite_eq_iff] at hyz
cases hyz with
| inl h =>
have h' := h.2
apply_fun padicValNat 2 at h'
simp [padicValNat_prime_prime_pow, padicValNat.mul] at h'
| inr hyz => _
have hyz := hyz.2
cases hyz with
| inl h =>
have h' := Eq.symm h.2
apply_fun padicValNat 5 at h'
simp [padicValNat_prime_prime_pow, padicValNat.mul] at h'
| inr hyz => _
have hyz := hyz.2
cases hyz with
| inl h =>
rw [h.1] at h
have h' := h.2
apply_fun padicValNat 3 at h'
simp [padicValNat_prime_prime_pow, padicValNat.mul] at h'
have this2 := Nat.lt_pow_self (by simp: 1 < 3) (padicValNat 3 y.val)
have this2 := ne_of_gt this2
exact this2 (Eq.symm h')
| inr hyz => _
have hyz := hyz.2
cases hyz with
| inl h =>
rw [h.1] at h
have h' := h.2
simp [padicValNat_prime_prime_pow, padicValNat.mul, Nat.pow_mul] at h'
apply_fun PNat.val at h'
simp at h'
repeat simp only [ite_eq_iff] at h'
cases h' with
| inl this =>
have this := this.2
have this' := calc 3 ^ (3 ^ padicValNat 3 y.val * 5 ^ padicValNat 5 y.val) * 5 ^ x.val
_ ≥ 3 ^ (3 ^ padicValNat 3 y.val * 5 ^ padicValNat 5 y.val) := by simp [one_le_pow₀]
_ = 3 ^ (5 ^ padicValNat 5 y.val * 3 ^ padicValNat 3 y.val) := by simp [mul_comm]
_ = (3 ^ (5 ^ padicValNat 5 y.val)) ^ (3 ^ padicValNat 3 y.val) := by simp [pow_mul]
_ ≥ 3 ^ (5 ^ padicValNat 5 y.val) := by apply le_self_pow; simp [one_le_pow₀]; apply pow_ne_zero; simp
_ > 5 ^ padicValNat 5 y.val := by simp [Nat.lt_pow_self (by simp: 1 < 3)]
_ > padicValNat 5 y.val := by simp [Nat.lt_pow_self (by simp: 1 < 5)]
exact (ne_of_gt this') (Eq.symm this)
| inr this =>
have this := Eq.symm this.2
apply_fun padicValNat 5 at this
simp [padicValNat_prime_prime_pow, padicValNat.mul] at this
| inr hyz => _
have hyz := hyz.2
cases hyz with
| inl h =>
have h := Eq.symm h.2
apply_fun padicValNat 3 at h
simp [padicValNat_prime_prime_pow, padicValNat.mul, Nat.pow_mul] at h
have this' := calc y.val
_ > Nat.log 2 y.val := by simp [Nat.log_lt_self]
_ ≥ padicValNat 2 y.val := by simp [padicValNat_le_nat_log]
_ ≥ Nat.log 3 (padicValNat 2 y.val) := by simp [Nat.log_le_self]
_ ≥ padicValNat 3 (padicValNat 2 y.val) := by simp [padicValNat_le_nat_log]
exact (ne_of_gt this') h
| inr hyz => _
have h := Eq.symm hyz.2
apply_fun padicValNat 3 at h
simp [padicValNat_prime_prime_pow, padicValNat.mul, Nat.pow_mul] at h
.
rw [h4 x y (y ◇ z) hyz]

theorem Finite.Equation3994_implies_Equation3588 (G : Type*) [Magma G] [Finite G] (h : Equation3994 G) :
Equation3588 G := by
intro x y z
Expand Down
Loading

0 comments on commit 75b8b81

Please sign in to comment.