Goldbach21

21-state Turing machine halting-equivalent to the 25-state Goldbach machine.

@[reducible, inline]

abbrev ConjectureMachines.Goldbach21.refM : Machine 25 2

The original 25-state transition table used for the reference execution.

Equations

• ConjectureMachines.Goldbach21.refM = ConjectureMachines.Machines.goldbach25

@[reducible, inline]

abbrev ConjectureMachines.Goldbach21.candM : Machine 21 2

The compressed 21-state transition table.

Equations

• ConjectureMachines.Goldbach21.candM = ConjectureMachines.Machines.goldbach21

@[reducible, inline]

abbrev ConjectureMachines.Goldbach21.reference : BundledMachine 2

25-state Goldbach reference machine (goldbach_25, Yao & Leng 2024).

Equations

• ConjectureMachines.Goldbach21.reference = ConjectureMachines.Machines.goldbach25.bundle

@[reducible, inline]

abbrev ConjectureMachines.Goldbach21.candidate : BundledMachine 2

21-state Goldbach candidate machine (goldbach_21).

Equations

• ConjectureMachines.Goldbach21.candidate = ConjectureMachines.Machines.goldbach21.bundle

theorem ConjectureMachines.Goldbach21.candidate_fewer_states : candidate.states < reference.states

def ConjectureMachines.Goldbach21.edited : Machine 25 2

A 25-state intermediate machine with the candidate search order and redundant states.

Equations

• One or more equations did not get rendered due to their size.

def ConjectureMachines.Goldbach21.embed (q : Fin 21) : Fin 25

Embed the 21 candidate states into the reachable states of the intermediate machine.

Equations

• One or more equations did not get rendered due to their size.

theorem ConjectureMachines.Goldbach21.transition_embed (q : Fin 21) (a : Fin 2) : edited.transition (embed q) a = Option.map (fun (t : Fin 2 × Turing.Dir × Fin 21) => (t.1, t.2.1, embed t.2.2)) (candM.transition q a)

theorem ConjectureMachines.Goldbach21.step_embed (q : Fin 21) (T : Turing.Tape (Fin 2)) : step edited { state := embed q, tape := T } = Option.map (fun (c : Cfg 21 2) => { state := embed c.state, tape := c.tape }) (step candM { state := q, tape := T })

theorem ConjectureMachines.Goldbach21.respects_embed : StateTransition.Respects (step candM) (step edited) fun (c₁ : Cfg 21 2) (c₂ : Cfg 25 2) => c₂ = { state := embed c₁.state, tape := c₁.tape }

theorem ConjectureMachines.Goldbach21.candidate_iff_edited : ConjectureMachines.Halts candM ↔ (StateTransition.eval (step edited) { state := 2, tape := default }).Dom

def ConjectureMachines.Goldbach21.nSteps {states : ℕ} (M : Machine states 2) (n : ℕ) : Cfg states 2 → Option (Cfg states 2)

Execute exactly n transitions, returning none if a transition halts early.

Equations

• ConjectureMachines.Goldbach21.nSteps M 0 c = some c
• ConjectureMachines.Goldbach21.nSteps M (n + 1) c = (ConjectureMachines.step M c).bind (ConjectureMachines.Goldbach21.nSteps M n)

@[simp]

theorem ConjectureMachines.Goldbach21.nSteps_zero {states : ℕ} (M : Machine states 2) (c : Cfg states 2) : nSteps M 0 c = some c

@[simp]

theorem ConjectureMachines.Goldbach21.nSteps_succ {states : ℕ} (M : Machine states 2) (n : ℕ) (c : Cfg states 2) : nSteps M (n + 1) c = (step M c).bind (nSteps M n)

theorem ConjectureMachines.Goldbach21.nSteps_reaches {states : ℕ} {M : Machine states 2} {n : ℕ} {c c' : Cfg states 2} (h : nSteps M n c = some c') : StateTransition.Reaches (step M) c c'

theorem ConjectureMachines.Goldbach21.nSteps_eval_dom {states : ℕ} {M : Machine states 2} {n : ℕ} {c c' : Cfg states 2} (h : nSteps M n c = some c') : (StateTransition.eval (step M) c).Dom ↔ (StateTransition.eval (step M) c').Dom

theorem ConjectureMachines.Goldbach21.nSteps_add {states : ℕ} {M : Machine states 2} (m n : ℕ) (c : Cfg states 2) : nSteps M (m + n) c = (nSteps M m c).bind (nSteps M n)

theorem ConjectureMachines.Goldbach21.nSteps_bind_eq {states : ℕ} {M : Machine states 2} {m n : ℕ} {c c₁ c₂ : Cfg states 2} (h₁ : nSteps M m c = some c₁) (h₂ : nSteps M n c₁ = some c₂) : nSteps M (m + n) c = some c₂

theorem ConjectureMachines.Goldbach21.step_nSteps {states : ℕ} {M : Machine states 2} {n : ℕ} {c c₁ c₂ : Cfg states 2} (h₁ : step M c = some c₁) (h₂ : nSteps M n c₁ = some c₂) : nSteps M (n + 1) c = some c₂

theorem ConjectureMachines.Goldbach21.step_one {states : ℕ} {M : Machine states 2} {c c₁ : Cfg states 2} (h : step M c = some c₁) : nSteps M 1 c = some c₁

theorem ConjectureMachines.Goldbach21.mk_append_replicate_zero (l : List (Fin 2)) (n : ℕ) : Turing.ListBlank.mk (l ++ List.replicate n 0) = Turing.ListBlank.mk l

theorem ConjectureMachines.Goldbach21.boot_reference_47 : nSteps refM 47 init = some { state := 19, tape := { head := 1, left := Turing.ListBlank.mk [1, 1], right := Turing.ListBlank.mk [0, 1] } }

theorem ConjectureMachines.Goldbach21.boot_edited_125 : nSteps edited 125 { state := 2, tape := default } = some { state := 0, tape := { head := 1, left := Turing.ListBlank.mk [], right := Turing.ListBlank.mk [1, 1, 0, 1, 1, 1] } }

def ConjectureMachines.Goldbach21.Tape.mkL (L R : Turing.ListBlank (Fin 2)) : Turing.Tape (Fin 2)

A tape whose head is the first cell of the left list, facing the right list.

Equations

• ConjectureMachines.Goldbach21.Tape.mkL L R = { head := L.head, left := L.tail, right := R }

@[simp]

theorem ConjectureMachines.Goldbach21.Tape.mkL_cons (a : Fin 2) (L R : Turing.ListBlank (Fin 2)) : mkL (Turing.ListBlank.cons a L) R = { head := a, left := L, right := R }

@[simp]

theorem ConjectureMachines.Goldbach21.Tape.mk'_cons (a : Fin 2) (L R : Turing.ListBlank (Fin 2)) : Turing.Tape.mk' L (Turing.ListBlank.cons a R) = { head := a, left := L, right := R }

theorem ConjectureMachines.Goldbach21.step_right {states : ℕ} {M : Machine states 2} {q q' : Fin states} {a b : Fin 2} (h : M.transition q a = some (b, Turing.Dir.right, q')) (L R : Turing.ListBlank (Fin 2)) : step M { state := q, tape := { head := a, left := L, right := R } } = some { state := q', tape := { head := R.head, left := Turing.ListBlank.cons b L, right := R.tail } }

theorem ConjectureMachines.Goldbach21.step_right_cons {states : ℕ} {M : Machine states 2} {q q' : Fin states} {a b c : Fin 2} (h : M.transition q a = some (b, Turing.Dir.right, q')) (L R : Turing.ListBlank (Fin 2)) : step M { state := q, tape := { head := a, left := L, right := Turing.ListBlank.cons c R } } = some { state := q', tape := { head := c, left := Turing.ListBlank.cons b L, right := R } }

theorem ConjectureMachines.Goldbach21.step_mkL_left {states : ℕ} {M : Machine states 2} {q q' : Fin states} {a b : Fin 2} (h : M.transition q a = some (b, Turing.Dir.left, q')) (L R : Turing.ListBlank (Fin 2)) : step M { state := q, tape := Tape.mkL (Turing.ListBlank.cons a L) R } = some { state := q', tape := Tape.mkL L (Turing.ListBlank.cons b R) }

theorem ConjectureMachines.Goldbach21.step_mkL_right {states : ℕ} {M : Machine states 2} {q q' : Fin states} {a b : Fin 2} (h : M.transition q a = some (b, Turing.Dir.right, q')) (L R : Turing.ListBlank (Fin 2)) : step M { state := q, tape := Tape.mkL (Turing.ListBlank.cons a L) R } = some { state := q', tape := Turing.Tape.mk' (Turing.ListBlank.cons b L) R }

theorem ConjectureMachines.Goldbach21.step_mk'_right {states : ℕ} {M : Machine states 2} {q q' : Fin states} {a b : Fin 2} (h : M.transition q a = some (b, Turing.Dir.right, q')) (L R : Turing.ListBlank (Fin 2)) : step M { state := q, tape := Turing.Tape.mk' L (Turing.ListBlank.cons a R) } = some { state := q', tape := Turing.Tape.mk' (Turing.ListBlank.cons b L) R }

theorem ConjectureMachines.Goldbach21.step_mk'_left {states : ℕ} {M : Machine states 2} {q q' : Fin states} {a b : Fin 2} (h : M.transition q a = some (b, Turing.Dir.left, q')) (L R : Turing.ListBlank (Fin 2)) : step M { state := q, tape := Turing.Tape.mk' L (Turing.ListBlank.cons a R) } = some { state := q', tape := Tape.mkL L (Turing.ListBlank.cons b R) }

theorem ConjectureMachines.Goldbach21.append_replicate_cons (k : ℕ) (b : Fin 2) (L : Turing.ListBlank (Fin 2)) : Turing.ListBlank.append (List.replicate k b) (Turing.ListBlank.cons b L) = Turing.ListBlank.append (List.replicate (k + 1) b) L

theorem ConjectureMachines.Goldbach21.append_replicate_add (m n : ℕ) (b : Fin 2) (L : Turing.ListBlank (Fin 2)) : Turing.ListBlank.append (List.replicate m b) (Turing.ListBlank.append (List.replicate n b) L) = Turing.ListBlank.append (List.replicate (m + n) b) L

theorem ConjectureMachines.Goldbach21.nSteps_mkL_left_scan {states : ℕ} {M : Machine states 2} {q : Fin states} {a b : Fin 2} (h : M.transition q a = some (b, Turing.Dir.left, q)) (k : ℕ) (L R : Turing.ListBlank (Fin 2)) : nSteps M k { state := q, tape := Tape.mkL (Turing.ListBlank.append (List.replicate k a) L) R } = some { state := q, tape := Tape.mkL L (Turing.ListBlank.append (List.replicate k b) R) }

theorem ConjectureMachines.Goldbach21.nSteps_mk'_right_scan {states : ℕ} {M : Machine states 2} {q : Fin states} {a b : Fin 2} (h : M.transition q a = some (b, Turing.Dir.right, q)) (k : ℕ) (L R : Turing.ListBlank (Fin 2)) : nSteps M k { state := q, tape := Turing.Tape.mk' L (Turing.ListBlank.append (List.replicate k a) R) } = some { state := q, tape := Turing.Tape.mk' (Turing.ListBlank.append (List.replicate k b) L) R }

def ConjectureMachines.Goldbach21.B0 : Turing.ListBlank (Fin 2)

The all-blank one-sided binary tape.

Equations

• ConjectureMachines.Goldbach21.B0 = Turing.ListBlank.mk []

@[simp]

theorem ConjectureMachines.Goldbach21.B0_cons_zero : Turing.ListBlank.cons 0 B0 = B0

def ConjectureMachines.Goldbach21.counterTape (A B : ℕ) (L_base : Turing.ListBlank (Fin 2)) : Turing.ListBlank (Fin 2)

Two unary counters, of lengths B and A, separated by zero cells.

Equations

• One or more equations did not get rendered due to their size.

theorem ConjectureMachines.Goldbach21.sim_state6_d_ref (k : ℕ) (L_base R_rest : Turing.ListBlank (Fin 2)) : have L_cnt := Turing.ListBlank.append (List.replicate (k + 2) 1) (Turing.ListBlank.cons 0 L_base); have R_mid := Turing.ListBlank.cons 0 R_rest; nSteps refM (2 + (k + 2 + 2)) { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 L_cnt) (Turing.ListBlank.cons 1 R_rest) } = some { state := 10, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 0 L_base)) (Turing.ListBlank.append (0 :: (List.replicate k 0 ++ [1])) R_mid) }

theorem ConjectureMachines.Goldbach21.sim_state6_d_edit (k : ℕ) (L_base R_rest : Turing.ListBlank (Fin 2)) : have L_cnt := Turing.ListBlank.append (List.replicate (k + 2) 1) (Turing.ListBlank.cons 0 L_base); have R_mid := Turing.ListBlank.cons 0 R_rest; nSteps edited (2 + (k + 2 + (2 + (k + 1 + (6 + (k + 1)))))) { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 L_cnt) (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 R_rest)) } = some { state := 0, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 0 L_base)) (Turing.ListBlank.append (0 :: (List.replicate k 0 ++ [1])) (Turing.ListBlank.cons 1 R_mid)) }

theorem ConjectureMachines.Goldbach21.sim_state6_accept_ref (k : ℕ) (L_base R_end : Turing.ListBlank (Fin 2)) : have L_cnt := Turing.ListBlank.append (List.replicate (k + 2) 1) (Turing.ListBlank.cons 0 L_base); step refM { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 L_cnt) (Turing.ListBlank.cons 0 R_end) } = some { state := 5, tape := Tape.mkL (Turing.ListBlank.cons 1 L_cnt) (Turing.ListBlank.cons 0 R_end) }

theorem ConjectureMachines.Goldbach21.sim_state6_accept_edit (k : ℕ) (L_base R_end : Turing.ListBlank (Fin 2)) : have L_cnt := Turing.ListBlank.append (List.replicate (k + 2) 1) (Turing.ListBlank.cons 0 L_base); nSteps edited (2 + (k + 2 + (2 + (k + 1 + (6 + (k + (1 + (k + 3)))))))) { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 L_cnt) (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 0 R_end)) } = some { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 L_cnt)) (Turing.ListBlank.cons 0 R_end) }

theorem ConjectureMachines.Goldbach21.sim_state19_to_0_ref (L₁ R₁ : Turing.ListBlank (Fin 2)) : nSteps refM 2 { state := 19, tape := { head := 1, left := L₁, right := Turing.ListBlank.cons 0 R₁ } } = some { state := 0, tape := Turing.Tape.mk' (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 1 L₁)) R₁ }

theorem ConjectureMachines.Goldbach21.sim_state19_to_0_mkL_ref (L₁ R₁ : Turing.ListBlank (Fin 2)) : nSteps refM 2 { state := 19, tape := Tape.mkL (Turing.ListBlank.cons 1 L₁) (Turing.ListBlank.cons 0 R₁) } = some { state := 0, tape := Turing.Tape.mk' (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 1 L₁)) R₁ }

theorem ConjectureMachines.Goldbach21.sim_state0_p1 (L₁ L₂ R₁ R₂ : Turing.ListBlank (Fin 2)) : nSteps refM 2 { state := 0, tape := Turing.Tape.mk' L₁ (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 0 R₁)) } = some { state := 16, tape := Tape.mkL (Turing.ListBlank.cons 1 L₁) (Turing.ListBlank.cons 0 R₁) } ∧ nSteps edited 3 { state := 0, tape := Turing.Tape.mk' L₂ (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 0 R₂))) } = some { state := 16, tape := Tape.mkL (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 L₂)) (Turing.ListBlank.cons 0 R₂) }

theorem ConjectureMachines.Goldbach21.sim_state0_p2_ref (L₁ R₁ : Turing.ListBlank (Fin 2)) : nSteps refM 3 { state := 0, tape := Turing.Tape.mk' L₁ (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 0 R₁))) } = some { state := 5, tape := Tape.mkL (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 L₁)) (Turing.ListBlank.cons 0 R₁) }

theorem ConjectureMachines.Goldbach21.sim_state0_p2_edit (L₂ R₂ : Turing.ListBlank (Fin 2)) : nSteps edited 3 { state := 0, tape := Turing.Tape.mk' L₂ (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 0 R₂)))) } = some { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 L₂))) (Turing.ListBlank.cons 0 R₂) }

theorem ConjectureMachines.Goldbach21.sim_state0_p_ge3 (L₁ L₂ R₁ R₂ : Turing.ListBlank (Fin 2)) : nSteps refM 3 { state := 0, tape := Turing.Tape.mk' L₁ (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 R₁))) } = some { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 L₁))) R₁ } ∧ nSteps edited 3 { state := 0, tape := Turing.Tape.mk' L₂ (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 R₂)))) } = some { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 L₂))) (Turing.ListBlank.cons 1 R₂) }

theorem ConjectureMachines.Goldbach21.nSteps_state16_to_19_right {M : Machine 25 2} (h16_1 : M.transition 16 1 = some (1, Turing.Dir.left, 16)) (h16_0 : M.transition 16 0 = some (1, Turing.Dir.left, 17)) (h17_1 : M.transition 17 1 = some (0, Turing.Dir.left, 19)) (d : ℕ) (L_p1 R_p2 : Turing.ListBlank (Fin 2)) : nSteps M (d + 2) { state := 16, tape := Tape.mkL (Turing.ListBlank.append (List.replicate d 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 1 L_p1))) R_p2 } = some { state := 19, tape := Tape.mkL L_p1 (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate d 1) R_p2))) }

theorem ConjectureMachines.Goldbach21.nSteps_state16_to_19_left {M : Machine 25 2} (h16_1 : M.transition 16 1 = some (1, Turing.Dir.left, 16)) (h16_0 : M.transition 16 0 = some (1, Turing.Dir.left, 17)) (h17_0 : M.transition 17 0 = some (0, Turing.Dir.right, 10)) (h10_1 : M.transition 10 1 = some (0, Turing.Dir.right, 18)) (h18_1 : M.transition 18 1 = some (1, Turing.Dir.right, 18)) (h18_0 : M.transition 18 0 = some (1, Turing.Dir.left, 17)) (h17_1 : M.transition 17 1 = some (0, Turing.Dir.left, 19)) (d m : ℕ) (L_blank R_p2 : Turing.ListBlank (Fin 2)) : nSteps M (d + (3 + (d + m + 1 + 2))) { state := 16, tape := Tape.mkL (Turing.ListBlank.append (List.replicate d 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 0 L_blank))) (Turing.ListBlank.append (List.replicate (m + 1) 1) (Turing.ListBlank.cons 0 R_p2)) } = some { state := 19, tape := Tape.mkL (Turing.ListBlank.append (List.replicate (d + m) 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 0 L_blank))) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 1 R_p2)) }

theorem ConjectureMachines.Goldbach21.nSteps_pass_11_to_13 {M : Machine 25 2} (h11_1 : M.transition 11 1 = some (0, Turing.Dir.right, 12)) (h12_1 : M.transition 12 1 = some (1, Turing.Dir.right, 12)) (h12_0 : M.transition 12 0 = some (1, Turing.Dir.right, 13)) (m : ℕ) (L R : Turing.ListBlank (Fin 2)) : nSteps M (1 + (m + 1)) { state := 11, tape := Turing.Tape.mk' L (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate m 1) (Turing.ListBlank.cons 0 R))) } = some { state := 13, tape := Turing.Tape.mk' (Turing.ListBlank.append (List.replicate (m + 1) 1) (Turing.ListBlank.cons 0 L)) R }

theorem ConjectureMachines.Goldbach21.nSteps_pass_13_one_to_21 {M : Machine 25 2} (h13_1 : M.transition 13 1 = some (0, Turing.Dir.left, 20)) (h20_1 : M.transition 20 1 = some (1, Turing.Dir.left, 20)) (h20_0 : M.transition 20 0 = some (1, Turing.Dir.left, 21)) (m : ℕ) (L R : Turing.ListBlank (Fin 2)) : nSteps M (1 + (m + 1 + 1)) { state := 13, tape := Turing.Tape.mk' (Turing.ListBlank.append (List.replicate (m + 1) 1) (Turing.ListBlank.cons 0 L)) (Turing.ListBlank.cons 1 R) } = some { state := 21, tape := Tape.mkL L (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate (m + 1) 1) (Turing.ListBlank.cons 0 R))) }

theorem ConjectureMachines.Goldbach21.nSteps_pass_13_zero_to_15 {M : Machine 25 2} {b14 : Fin 2} (h13_0 : M.transition 13 0 = some (0, Turing.Dir.left, 14)) (h14_1 : M.transition 14 1 = some (1, Turing.Dir.left, 14)) (h14_0 : M.transition 14 0 = some (b14, Turing.Dir.left, 15)) (m : ℕ) (L R : Turing.ListBlank (Fin 2)) : nSteps M (1 + (m + 1 + 1)) { state := 13, tape := Turing.Tape.mk' (Turing.ListBlank.append (List.replicate (m + 1) 1) (Turing.ListBlank.cons 0 L)) (Turing.ListBlank.cons 0 R) } = some { state := 15, tape := Tape.mkL L (Turing.ListBlank.cons b14 (Turing.ListBlank.append (List.replicate (m + 1) 1) (Turing.ListBlank.cons 0 R))) }

theorem ConjectureMachines.Goldbach21.nSteps_pass_21_b0_to_11 {M : Machine 25 2} {q_mid : Fin 25} (h21_0 : M.transition 21 0 = some (0, Turing.Dir.left, 22)) (h22_1 : M.transition 22 1 = some (0, Turing.Dir.left, 22)) (h22_0 : M.transition 22 0 = some (0, Turing.Dir.right, q_mid)) (hq_0 : M.transition q_mid 0 = some (0, Turing.Dir.right, 11)) (h11_0 : M.transition 11 0 = some (1, Turing.Dir.right, 11)) (A : ℕ) (L_base R : Turing.ListBlank (Fin 2)) : nSteps M (1 + (A + (2 + A))) { state := 21, tape := Tape.mkL (counterTape A 0 L_base) R } = some { state := 11, tape := Turing.Tape.mk' (counterTape 0 A L_base) R }

theorem ConjectureMachines.Goldbach21.nSteps_pass_21_bsucc_to_11 {M : Machine 25 2} {q_mid : Fin 25} (h21_1 : M.transition 21 1 = some (0, Turing.Dir.left, 9)) (h9_1 : M.transition 9 1 = some (0, Turing.Dir.left, 9)) (h9_0 : M.transition 9 0 = some (1, Turing.Dir.right, q_mid)) (hq_0 : M.transition q_mid 0 = some (0, Turing.Dir.right, 11)) (h11_0 : M.transition 11 0 = some (1, Turing.Dir.right, 11)) (A b : ℕ) (L_base R : Turing.ListBlank (Fin 2)) : nSteps M (1 + (b + (2 + b))) { state := 21, tape := Tape.mkL (counterTape A (b + 1) L_base) R } = some { state := 11, tape := Turing.Tape.mk' (counterTape (A + 1) b L_base) R }

theorem ConjectureMachines.Goldbach21.nSteps_pass_15_bsucc_to_6_ref (A b : ℕ) (L_base R : Turing.ListBlank (Fin 2)) : nSteps refM (1 + (b + (1 + (b + 1 + 2)))) { state := 15, tape := Tape.mkL (counterTape A (b + 1) L_base) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 1 R)) } = some { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate (A + b + 3) 1) (Turing.ListBlank.cons 0 L_base))) R }

theorem ConjectureMachines.Goldbach21.nSteps_pass_15_bsucc_to_6_edit (A b : ℕ) (L_base R : Turing.ListBlank (Fin 2)) : nSteps edited (1 + (b + (1 + (b + 3)))) { state := 15, tape := Tape.mkL (counterTape A (b + 1) L_base) (Turing.ListBlank.cons 1 (Turing.ListBlank.cons 1 R)) } = some { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate (A + b + 3) 1) (Turing.ListBlank.cons 0 L_base))) R }

theorem ConjectureMachines.Goldbach21.nSteps_pass_15_b0_to_16_ref (A m : ℕ) (L_base R_end : Turing.ListBlank (Fin 2)) : nSteps refM (2 + (A + 1)) { state := 15, tape := Tape.mkL (counterTape A 0 L_base) (Turing.ListBlank.cons 0 (Turing.ListBlank.append (List.replicate (m + 1) 1) (Turing.ListBlank.cons 0 R_end))) } = some { state := 16, tape := Tape.mkL (Turing.ListBlank.cons 0 L_base) (Turing.ListBlank.append (List.replicate (A + m + 3) 1) (Turing.ListBlank.cons 0 R_end)) }

theorem ConjectureMachines.Goldbach21.nSteps_pass_15_b0_to_16_edit (A m : ℕ) (L_base R_end : Turing.ListBlank (Fin 2)) : nSteps edited (1 + A) { state := 15, tape := Tape.mkL (counterTape A 0 L_base) (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate (m + 1) 1) (Turing.ListBlank.cons 0 R_end))) } = some { state := 16, tape := Tape.mkL (Turing.ListBlank.cons 0 L_base) (Turing.ListBlank.append (List.replicate (A + m + 3) 1) (Turing.ListBlank.cons 0 R_end)) }

theorem ConjectureMachines.Goldbach21.nSteps_pass_11_b0 {M : Machine 25 2} {q_mid : Fin 25} (h11_1 : M.transition 11 1 = some (0, Turing.Dir.right, 12)) (h12_1 : M.transition 12 1 = some (1, Turing.Dir.right, 12)) (h12_0 : M.transition 12 0 = some (1, Turing.Dir.right, 13)) (h13_1 : M.transition 13 1 = some (0, Turing.Dir.left, 20)) (h20_1 : M.transition 20 1 = some (1, Turing.Dir.left, 20)) (h20_0 : M.transition 20 0 = some (1, Turing.Dir.left, 21)) (h21_0 : M.transition 21 0 = some (0, Turing.Dir.left, 22)) (h22_1 : M.transition 22 1 = some (0, Turing.Dir.left, 22)) (h22_0 : M.transition 22 0 = some (0, Turing.Dir.right, q_mid)) (hq_0 : M.transition q_mid 0 = some (0, Turing.Dir.right, 11)) (h11_0 : M.transition 11 0 = some (1, Turing.Dir.right, 11)) (A m : ℕ) (L_base R : Turing.ListBlank (Fin 2)) : nSteps M (1 + (m + 1) + (1 + (m + 1 + 1) + (1 + (A + (2 + A))))) { state := 11, tape := Turing.Tape.mk' (counterTape A 0 L_base) (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate m 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 1 R)))) } = some { state := 11, tape := Turing.Tape.mk' (counterTape 0 A L_base) (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate (m + 1) 1) (Turing.ListBlank.cons 0 R))) }

theorem ConjectureMachines.Goldbach21.nSteps_pass_11_bsucc {M : Machine 25 2} {q_mid : Fin 25} (h11_1 : M.transition 11 1 = some (0, Turing.Dir.right, 12)) (h12_1 : M.transition 12 1 = some (1, Turing.Dir.right, 12)) (h12_0 : M.transition 12 0 = some (1, Turing.Dir.right, 13)) (h13_1 : M.transition 13 1 = some (0, Turing.Dir.left, 20)) (h20_1 : M.transition 20 1 = some (1, Turing.Dir.left, 20)) (h20_0 : M.transition 20 0 = some (1, Turing.Dir.left, 21)) (h21_1 : M.transition 21 1 = some (0, Turing.Dir.left, 9)) (h9_1 : M.transition 9 1 = some (0, Turing.Dir.left, 9)) (h9_0 : M.transition 9 0 = some (1, Turing.Dir.right, q_mid)) (hq_0 : M.transition q_mid 0 = some (0, Turing.Dir.right, 11)) (h11_0 : M.transition 11 0 = some (1, Turing.Dir.right, 11)) (A b m : ℕ) (L_base R : Turing.ListBlank (Fin 2)) : nSteps M (1 + (m + 1) + (1 + (m + 1 + 1) + (1 + (b + (2 + b))))) { state := 11, tape := Turing.Tape.mk' (counterTape A (b + 1) L_base) (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate m 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 1 R)))) } = some { state := 11, tape := Turing.Tape.mk' (counterTape (A + 1) b L_base) (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate (m + 1) 1) (Turing.ListBlank.cons 0 R))) }

theorem ConjectureMachines.Goldbach21.nSteps_pass_11_to_6_ref (A b m : ℕ) (L_base R_end : Turing.ListBlank (Fin 2)) : nSteps refM (1 + (m + 1) + (1 + (m + 1 + 1) + (1 + (b + (1 + (b + 1 + 2)))))) { state := 11, tape := Turing.Tape.mk' (counterTape A (b + 1) L_base) (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate m 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 0 R_end)))) } = some { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate (A + b + 3) 1) (Turing.ListBlank.cons 0 L_base))) (Turing.ListBlank.append (List.replicate m 1) (Turing.ListBlank.cons 0 R_end)) }

theorem ConjectureMachines.Goldbach21.nSteps_pass_11_to_6_edit (A b m : ℕ) (L_base R_end : Turing.ListBlank (Fin 2)) : nSteps edited (1 + (m + 1) + (1 + (m + 1 + 1) + (1 + (b + (1 + (b + 3)))))) { state := 11, tape := Turing.Tape.mk' (counterTape A (b + 1) L_base) (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate m 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 0 R_end)))) } = some { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate (A + b + 3) 1) (Turing.ListBlank.cons 0 L_base))) (Turing.ListBlank.append (List.replicate m 1) (Turing.ListBlank.cons 0 R_end)) }

theorem ConjectureMachines.Goldbach21.nSteps_pass_11_to_16_ref (A m : ℕ) (L_base R_end : Turing.ListBlank (Fin 2)) : nSteps refM (1 + (m + 1) + (1 + (m + 1 + 1) + (2 + (A + 1)))) { state := 11, tape := Turing.Tape.mk' (counterTape A 0 L_base) (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate m 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 0 R_end)))) } = some { state := 16, tape := Tape.mkL (Turing.ListBlank.cons 0 L_base) (Turing.ListBlank.append (List.replicate (A + m + 3) 1) (Turing.ListBlank.cons 0 R_end)) }

theorem ConjectureMachines.Goldbach21.nSteps_pass_11_to_16_edit (A m : ℕ) (L_base R_end : Turing.ListBlank (Fin 2)) : nSteps edited (1 + (m + 1) + (1 + (m + 1 + 1) + (1 + A))) { state := 11, tape := Turing.Tape.mk' (counterTape A 0 L_base) (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate m 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 0 R_end)))) } = some { state := 16, tape := Tape.mkL (Turing.ListBlank.cons 0 L_base) (Turing.ListBlank.append (List.replicate (A + m + 3) 1) (Turing.ListBlank.cons 0 R_end)) }

theorem ConjectureMachines.Goldbach21.sim_state5_to_0_left_from_0_ref (p1 p2 : ℕ) (L_blank R_end : Turing.ListBlank (Fin 2)) : nSteps refM (3 + (p1 + (1 + (p1 + 1 + 1)))) { state := 5, tape := Tape.mkL (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 0 L_blank)) (Turing.ListBlank.append (List.replicate p1 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.append (List.replicate p2 1) (Turing.ListBlank.cons 0 R_end)))) } = some { state := 0, tape := Turing.Tape.mk' (Turing.ListBlank.cons 0 L_blank) (Turing.ListBlank.append (List.replicate (p1 + p2 + 2) 1) (Turing.ListBlank.cons 0 R_end)) }

Primality Predicate and refM Semantics

def ConjectureMachines.Goldbach21.NoFactorFrom (k p : ℕ) : Prop

No integer from k + 2 up to p - 1 divides p.

Equations

• ConjectureMachines.Goldbach21.NoFactorFrom k p = ∀ (d : ℕ), k + 2 ≤ d → d < p → ¬d ∣ p

def ConjectureMachines.Goldbach21.IsPrime (p : ℕ) : Prop

Trial-division primality: at least two, with no smaller nontrivial divisor.

Equations

• ConjectureMachines.Goldbach21.IsPrime p = (2 ≤ p ∧ ConjectureMachines.Goldbach21.NoFactorFrom 0 p)

theorem ConjectureMachines.Goldbach21.not_isPrime_zero : ¬IsPrime 0

theorem ConjectureMachines.Goldbach21.not_isPrime_one : ¬IsPrime 1

theorem ConjectureMachines.Goldbach21.isPrime_two : IsPrime 2

def ConjectureMachines.Goldbach21.HasGoldbachPair (n : ℕ) : Prop

The natural number is the sum of two trial-division primes.

Equations

• ConjectureMachines.Goldbach21.HasGoldbachPair n = ∃ (a : ℕ), ∃ (b : ℕ), ConjectureMachines.Goldbach21.IsPrime a ∧ ConjectureMachines.Goldbach21.IsPrime b ∧ a + b = n

def ConjectureMachines.Goldbach21.LBase1 : Bool → ℕ → Turing.ListBlank (Fin 2)

The left tape suffix used to encode the reference machine search orientation.

Equations

• ConjectureMachines.Goldbach21.LBase1 true x✝ = Turing.ListBlank.append (List.replicate (x✝ + 1) 1) ConjectureMachines.Goldbach21.B0
• ConjectureMachines.Goldbach21.LBase1 false x✝ = ConjectureMachines.Goldbach21.B0

def ConjectureMachines.Goldbach21.REnd1 : Bool → ℕ → Turing.ListBlank (Fin 2)

The right tape suffix used to encode the reference machine search orientation.

Equations

• ConjectureMachines.Goldbach21.REnd1 true x✝ = ConjectureMachines.Goldbach21.B0
• ConjectureMachines.Goldbach21.REnd1 false x✝ = Turing.ListBlank.append (List.replicate x✝ 1) ConjectureMachines.Goldbach21.B0

def ConjectureMachines.Goldbach21.cfg0 (is_right : Bool) (q p : ℕ) : Cfg 25 2

Reference primality-test entry with orientation is_right and unary parameters q, p.

Equations

• One or more equations did not get rendered due to their size.

def ConjectureMachines.Goldbach21.cfg6 (is_right : Bool) (q k r : ℕ) : Cfg 25 2

Reference trial-division entry, with divisor k + 2 and remaining unary length r.

Equations

• One or more equations did not get rendered due to their size.

def ConjectureMachines.Goldbach21.cfg11 (is_right : Bool) (q A B m r : ℕ) : Cfg 25 2

Reference division-loop configuration with unary counters A, B, m, r.

Equations

• One or more equations did not get rendered due to their size.

def ConjectureMachines.Goldbach21.cfgExit (is_right is_prime : Bool) (q p : ℕ) : Cfg 25 2

Reference primality-test exit, selecting its continuation from the primality result.

Equations

• One or more equations did not get rendered due to their size.

theorem ConjectureMachines.Goldbach21.cfg11_step_b0 (is_right : Bool) (q A m r' : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfg11 is_right q A 0 m (r' + 1)) = some (cfg11 is_right q 0 A (m + 1) r')

theorem ConjectureMachines.Goldbach21.cfg11_step_bsucc (is_right : Bool) (q A b m r' : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfg11 is_right q A (b + 1) m (r' + 1)) = some (cfg11 is_right q (A + 1) b (m + 1) r')

theorem ConjectureMachines.Goldbach21.drain_counters {states : ℕ} {M : Machine states 2} (configuration : ℕ → ℕ → ℕ → ℕ → Cfg states 2) (zero_step : ∀ (A m r : ℕ), ∃ (s : ℕ), 1 ≤ s ∧ nSteps M s (configuration A 0 m (r + 1)) = some (configuration 0 A (m + 1) r)) (successor_step : ∀ (A b m r : ℕ), ∃ (s : ℕ), 1 ≤ s ∧ nSteps M s (configuration A (b + 1) m (r + 1)) = some (configuration (A + 1) b (m + 1) r)) (k r A B m : ℕ) (hAB : A + B = k + 1) (hdvd : k + 2 ∣ B + m + 2) : ∃ (A' : ℕ), ∃ (B' : ℕ), A' + B' = k + 1 ∧ k + 2 ∣ B' + (m + r) + 2 ∧ ∃ (s : ℕ), nSteps M s (configuration A B m r) = some (configuration A' B' (m + r) 0)

Drain a unary counter loop from its zero-counter and successor-counter update rules.

theorem ConjectureMachines.Goldbach21.cfg11_drain (is_right : Bool) (q k r A B m : ℕ) (hAB : A + B = k + 1) (hdvd : k + 2 ∣ B + m + 2) : ∃ (A' : ℕ), ∃ (B' : ℕ), A' + B' = k + 1 ∧ k + 2 ∣ B' + (m + r) + 2 ∧ ∃ (s : ℕ), nSteps refM s (cfg11 is_right q A B m r) = some (cfg11 is_right q A' B' (m + r) 0)

theorem ConjectureMachines.Goldbach21.cfg6_step_enter (is_right : Bool) (q k r' : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfg6 is_right q k (r' + 1)) = some (cfg11 is_right q 1 k 0 r')

theorem ConjectureMachines.Goldbach21.cfg6_pass_succ_dvd (is_right : Bool) (q k r' : ℕ) (hdvd : k + 2 ∣ k + 4 + r') : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfg6 is_right q k (r' + 1)) = some (cfgExit is_right false q (k + 4 + r'))

theorem ConjectureMachines.Goldbach21.cfg6_pass_succ_not_dvd (is_right : Bool) (q k r' : ℕ) (hdvd : ¬k + 2 ∣ k + 4 + r') : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfg6 is_right q k (r' + 1)) = some (cfg6 is_right q (k + 1) r')

theorem ConjectureMachines.Goldbach21.cfg6_eval (is_right : Bool) (q k r : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfg6 is_right q k r) = some (cfgExit is_right (decide (NoFactorFrom k (k + 3 + r))) q (k + 3 + r))

theorem ConjectureMachines.Goldbach21.cfg0_eval (is_right : Bool) (q p : ℕ) (hp : 1 ≤ p) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfg0 is_right q p) = some (cfgExit is_right (decide (IsPrime p)) q p)

theorem ConjectureMachines.Goldbach21.cfgExit_tt (q p : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfgExit true true q p) = some (cfg0 false p (q + 1))

theorem ConjectureMachines.Goldbach21.cfgExit_tf_succ (q' p : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfgExit true false (q' + 1) p) = some (cfg0 true q' (p + 1))

theorem ConjectureMachines.Goldbach21.cfgExit_tf_zero (p : ℕ) : ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps refM s (cfgExit true false 0 p) = some c ∧ step refM c = none

theorem ConjectureMachines.Goldbach21.cfgExit_ft (q p : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfgExit false true q p) = some (cfg0 false 0 (p + q + 2))

theorem ConjectureMachines.Goldbach21.cfgExit_ff_succ (q p' : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfgExit false false q (p' + 2)) = some (cfg0 true p' (q + 1))

theorem ConjectureMachines.Goldbach21.cfgExit_ff_one (q : ℕ) : ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps refM s (cfgExit false false q 1) = some c ∧ step refM c = none

def ConjectureMachines.Goldbach21.stageCfg (w : ℕ) : Cfg 25 2

Reference search entry for the even number 2 * w + 4.

Equations

• ConjectureMachines.Goldbach21.stageCfg w = ConjectureMachines.Goldbach21.cfg0 true (2 * w + 2) 1

theorem ConjectureMachines.Goldbach21.cfg0_partner_pass (w q p : ℕ) (hp : 1 ≤ p) (hsum : q + p = 2 * w + 3) (hp_prime : IsPrime p) (hq_prime : IsPrime (q + 1)) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfg0 true q p) = some (stageCfg (w + 1))

theorem ConjectureMachines.Goldbach21.cfg0_partner_fail_succ (q' p : ℕ) (hp : 1 ≤ p) (hfail : ¬(IsPrime p ∧ IsPrime (q' + 2))) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfg0 true (q' + 1) p) = some (cfg0 true q' (p + 1))

theorem ConjectureMachines.Goldbach21.cfg0_partner_fail_zero (p : ℕ) (hp : 1 ≤ p) : ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps refM s (cfg0 true 0 p) = some c ∧ step refM c = none

theorem ConjectureMachines.Goldbach21.search_advance (w q p : ℕ) (hp : 1 ≤ p) (hsum : q + p = 2 * w + 3) {q' : ℕ} (hq' : q' ≤ q) (hq1 : IsPrime (q' + 1)) (hp1 : IsPrime (2 * w + 3 - q')) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (cfg0 true q p) = some (stageCfg (w + 1))

theorem ConjectureMachines.Goldbach21.search_halt (w q p : ℕ) (hp : 1 ≤ p) (hsum : q + p = 2 * w + 3) (hno : ∀ (q' : ℕ), q' ≤ q → ¬(IsPrime (q' + 1) ∧ IsPrime (2 * w + 3 - q'))) : ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps refM s (cfg0 true q p) = some c ∧ step refM c = none

theorem ConjectureMachines.Goldbach21.stage_advance (w : ℕ) (h : HasGoldbachPair (2 * w + 4)) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps refM s (stageCfg w) = some (stageCfg (w + 1))

theorem ConjectureMachines.Goldbach21.stage_halt (w : ℕ) (h : ¬HasGoldbachPair (2 * w + 4)) : ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps refM s (stageCfg w) = some c ∧ step refM c = none

theorem ConjectureMachines.Goldbach21.reaches_imp_nSteps {states : ℕ} {M : Machine states 2} {a b : Cfg states 2} (h : StateTransition.Reaches (step M) a b) : ∃ (k : ℕ), nSteps M k a = some b

theorem ConjectureMachines.Goldbach21.nSteps_eq_none_of_step_none {states : ℕ} {M : Machine states 2} {k : ℕ} (s : ℕ) {a b : Cfg states 2} (hk : nSteps M k a = some b) (hnone : step M b = none) (hks : k < s) : nSteps M s a = none

theorem ConjectureMachines.Goldbach21.stage_iter_all (hall : ∀ (w : ℕ), HasGoldbachPair (2 * w + 4)) (N : ℕ) : ∃ (s : ℕ), N ≤ s ∧ nSteps refM s (stageCfg 0) = some (stageCfg N)

theorem ConjectureMachines.Goldbach21.stage_reach_or_halt (w : ℕ) : (∃ (s : ℕ), nSteps refM s (stageCfg 0) = some (stageCfg w)) ∨ ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps refM s (stageCfg 0) = some c ∧ step refM c = none

theorem ConjectureMachines.Goldbach21.boot_chk0_ref : nSteps refM 49 init = some (stageCfg 0)

theorem ConjectureMachines.Goldbach21.halts_reference_iff_exists_counterexample : ConjectureMachines.Halts refM ↔ ∃ (w : ℕ), ¬HasGoldbachPair (2 * w + 4)

edited Semantics (L-First Goldbach Machine)

def ConjectureMachines.Goldbach21.LBaseE : Bool → ℕ → Turing.ListBlank (Fin 2)

The left tape suffix for the intermediate machine search orientation.

Equations

• ConjectureMachines.Goldbach21.LBaseE true x✝ = Turing.ListBlank.append (List.replicate (x✝ + 1) 1) ConjectureMachines.Goldbach21.B0
• ConjectureMachines.Goldbach21.LBaseE false x✝ = ConjectureMachines.Goldbach21.B0

def ConjectureMachines.Goldbach21.REndE : Bool → ℕ → Turing.ListBlank (Fin 2)

The right tape suffix for the intermediate machine search orientation.

Equations

• ConjectureMachines.Goldbach21.REndE true x✝ = ConjectureMachines.Goldbach21.B0
• ConjectureMachines.Goldbach21.REndE false x✝ = Turing.ListBlank.append (List.replicate (x✝ + 1) 1) ConjectureMachines.Goldbach21.B0

def ConjectureMachines.Goldbach21.cfg0E (is_right : Bool) (q p : ℕ) : Cfg 25 2

Intermediate primality-test entry with orientation and unary search parameters.

Equations

• One or more equations did not get rendered due to their size.

def ConjectureMachines.Goldbach21.cfg6E (is_right : Bool) (q k r : ℕ) : Cfg 25 2

Intermediate trial-division entry, with divisor k + 2 and remainder parameter r.

Equations

• One or more equations did not get rendered due to their size.

def ConjectureMachines.Goldbach21.cfg11E (is_right : Bool) (q A B m r : ℕ) : Cfg 25 2

Intermediate division-loop configuration with unary counter parameters.

Equations

• One or more equations did not get rendered due to their size.

def ConjectureMachines.Goldbach21.cfgExitE (is_right is_prime : Bool) (q p : ℕ) : Cfg 25 2

Intermediate primality-test exit, selecting the prime or composite continuation.

Equations

• One or more equations did not get rendered due to their size.

theorem ConjectureMachines.Goldbach21.cfg11E_step_b0 (is_right : Bool) (q A m r' : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfg11E is_right q A 0 m (r' + 1)) = some (cfg11E is_right q 0 A (m + 1) r')

theorem ConjectureMachines.Goldbach21.cfg11E_step_bsucc (is_right : Bool) (q A b m r' : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfg11E is_right q A (b + 1) m (r' + 1)) = some (cfg11E is_right q (A + 1) b (m + 1) r')

theorem ConjectureMachines.Goldbach21.cfg11E_drain (is_right : Bool) (q k r A B m : ℕ) (hAB : A + B = k + 1) (hdvd : k + 2 ∣ B + m + 2) : ∃ (A' : ℕ), ∃ (B' : ℕ), A' + B' = k + 1 ∧ k + 2 ∣ B' + (m + r) + 2 ∧ ∃ (s : ℕ), nSteps edited s (cfg11E is_right q A B m r) = some (cfg11E is_right q A' B' (m + r) 0)

theorem ConjectureMachines.Goldbach21.cfg6E_step_enter (is_right : Bool) (q k r' : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfg6E is_right q k (r' + 1)) = some (cfg11E is_right q 1 k 0 r')

theorem ConjectureMachines.Goldbach21.cfg6E_pass_succ_dvd (is_right : Bool) (q k r' : ℕ) (hdvd : k + 2 ∣ k + 4 + r') : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfg6E is_right q k (r' + 1)) = some (cfgExitE is_right false q (k + 4 + r'))

theorem ConjectureMachines.Goldbach21.cfg6E_pass_succ_not_dvd (is_right : Bool) (q k r' : ℕ) (hdvd : ¬k + 2 ∣ k + 4 + r') : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfg6E is_right q k (r' + 1)) = some (cfg6E is_right q (k + 1) r')

theorem ConjectureMachines.Goldbach21.cfg6E_eval (is_right : Bool) (q k r : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfg6E is_right q k r) = some (cfgExitE is_right (decide (NoFactorFrom k (k + 3 + r))) q (k + 3 + r))

theorem ConjectureMachines.Goldbach21.cfg0E_eval (is_right : Bool) (q p : ℕ) (hp : 1 ≤ p) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfg0E is_right q p) = some (cfgExitE is_right (decide (IsPrime p)) q p)

theorem ConjectureMachines.Goldbach21.cfgExitE_ft (q p : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfgExitE false true q p) = some (cfg0E true p q)

theorem ConjectureMachines.Goldbach21.nSteps_state18_to_0_edit (k : ℕ) (L_base R_p2 : Turing.ListBlank (Fin 2)) : nSteps edited (1 + (k + 1 + 1)) { state := 18, tape := Tape.mkL (Turing.ListBlank.cons 1 (Turing.ListBlank.append (List.replicate (k + 1) 1) (Turing.ListBlank.cons 0 L_base))) R_p2 } = some { state := 0, tape := Turing.Tape.mk' (Turing.ListBlank.cons 0 L_base) (Turing.ListBlank.append (List.replicate (k + 1) 1) (Turing.ListBlank.cons 0 R_p2)) }

theorem ConjectureMachines.Goldbach21.cfgExitE_tf_succ (p0 q : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfgExitE true false (p0 + 1) q) = some (cfg0E false (q + 1) p0)

theorem ConjectureMachines.Goldbach21.nSteps_state16_left_split_edit (k : ℕ) (L_blank R_end : Turing.ListBlank (Fin 2)) : nSteps edited (3 + (k + 2 + 1) + (1 + (k + 1 + 1))) { state := 16, tape := Tape.mkL (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 0 L_blank)) (Turing.ListBlank.append (List.replicate (k + 2) 1) (Turing.ListBlank.cons 0 R_end)) } = some { state := 0, tape := Turing.Tape.mk' (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 0 L_blank)) (Turing.ListBlank.append (List.replicate (k + 1) 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 1 R_end))) }

theorem ConjectureMachines.Goldbach21.cfgExitE_ff (q p0 : ℕ) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfgExitE false false q (p0 + 1)) = some (cfg0E false (q + 1) p0)

theorem ConjectureMachines.Goldbach21.cfg0E_halt_zero (q : ℕ) : ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps edited s (cfg0E false q 0) = some c ∧ step edited c = none

theorem ConjectureMachines.Goldbach21.nSteps_state6_merge_to_16_edit (p q0 : ℕ) (L_base R_end : Turing.ListBlank (Fin 2)) : nSteps edited (4 + (q0 + 1 + (1 + (q0 + 1 + 3))) + (p + q0 + 5)) { state := 6, tape := Turing.Tape.mk' (Turing.ListBlank.append (List.replicate (q0 + 2) 1) (Turing.ListBlank.cons 0 (Turing.ListBlank.append (List.replicate (p + 1) 1) (Turing.ListBlank.cons 0 L_base)))) (Turing.ListBlank.cons 0 (Turing.ListBlank.cons 0 R_end)) } = some { state := 16, tape := Tape.mkL (Turing.ListBlank.cons 0 L_base) (Turing.ListBlank.append (List.replicate (p + q0 + 5) 1) (Turing.ListBlank.cons 0 R_end)) }

theorem ConjectureMachines.Goldbach21.cfgExitE_tt (w p q0 : ℕ) (hsum : p + (q0 + 1) = 2 * w + 4) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfgExitE true true p (q0 + 1)) = some (cfg0E false 0 (2 * w + 6))

def ConjectureMachines.Goldbach21.stageCfgE (w : ℕ) : Cfg 25 2

Intermediate search entry for the even number 2 * w + 4.

Equations

• ConjectureMachines.Goldbach21.stageCfgE w = ConjectureMachines.Goldbach21.cfg0E false 2 (2 * w + 2)

theorem ConjectureMachines.Goldbach21.cfg0E_partner_fail_succ (q p0 : ℕ) (hq : 1 ≤ q) (hfail : ¬(IsPrime (p0 + 2) ∧ IsPrime q)) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfg0E false q (p0 + 2)) = some (cfg0E false (q + 1) (p0 + 1))

theorem ConjectureMachines.Goldbach21.cfg0E_partner_pass (w q0 p : ℕ) (hp : 1 ≤ p) (hsum : p + (q0 + 1) = 2 * w + 4) (hp_prime : IsPrime p) (hq_prime : IsPrime (q0 + 1)) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfg0E false (q0 + 1) p) = some (stageCfgE (w + 1))

theorem ConjectureMachines.Goldbach21.cfg0E_partner_fail_one (q : ℕ) : ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps edited s (cfg0E false q 1) = some c ∧ step edited c = none

theorem ConjectureMachines.Goldbach21.searchE_advance (w q p0 : ℕ) (hq : 1 ≤ q) (hsum : q + (p0 + 1) = 2 * w + 4) {p' : ℕ} (hp' : p' ≤ p0) (hp1 : IsPrime (p' + 1)) (hq1 : IsPrime (2 * w + 4 - (p' + 1))) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (cfg0E false q (p0 + 1)) = some (stageCfgE (w + 1))

theorem ConjectureMachines.Goldbach21.searchE_halt (w q p0 : ℕ) (hq : 1 ≤ q) (hsum : q + (p0 + 1) = 2 * w + 4) (hno : ∀ (p' : ℕ), p' ≤ p0 → ¬(IsPrime (p' + 1) ∧ IsPrime (2 * w + 4 - (p' + 1)))) : ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps edited s (cfg0E false q (p0 + 1)) = some c ∧ step edited c = none

theorem ConjectureMachines.Goldbach21.stageE_advance (w : ℕ) (h : HasGoldbachPair (2 * w + 4)) : ∃ (s : ℕ), 1 ≤ s ∧ nSteps edited s (stageCfgE w) = some (stageCfgE (w + 1))

theorem ConjectureMachines.Goldbach21.stageE_halt (w : ℕ) (h : ¬HasGoldbachPair (2 * w + 4)) : ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps edited s (stageCfgE w) = some c ∧ step edited c = none

theorem ConjectureMachines.Goldbach21.stageE_iter_all (hall : ∀ (w : ℕ), HasGoldbachPair (2 * w + 4)) (N : ℕ) : ∃ (s : ℕ), N ≤ s ∧ nSteps edited s (stageCfgE 0) = some (stageCfgE N)

theorem ConjectureMachines.Goldbach21.stageE_reach_or_halt (w : ℕ) : (∃ (s : ℕ), nSteps edited s (stageCfgE 0) = some (stageCfgE w)) ∨ ∃ (s : ℕ), ∃ (c : Cfg 25 2), nSteps edited s (stageCfgE 0) = some c ∧ step edited c = none

theorem ConjectureMachines.Goldbach21.boot_chk0_edit : nSteps edited 125 { state := 2, tape := default } = some (stageCfgE 0)

theorem ConjectureMachines.Goldbach21.halts_edited_iff_exists_counterexample : (StateTransition.eval (step edited) { state := 2, tape := default }).Dom ↔ ∃ (w : ℕ), ¬HasGoldbachPair (2 * w + 4)

theorem ConjectureMachines.Goldbach21.candidate_equivalent : candidate.Halts ↔ reference.Halts