1. Cryptids
  2. Propositions
Imports
/- Copyright (c) 2026 Google LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ module public import Mathlib.Computability.TuringMachine.PostTuringMachine public import Mathlib.Data.Nat.Prime.Basic public import Mathlib.Algebra.GCDMonoid.Finset public import Mathlib.Order.Interval.Finset.Nat public import Mathlib.NumberTheory.LSeries.RiemannZeta public import Mathlib.SetTheory.ZFC.Basic

Target Mathematical Propositions (Cryptids.Propositions)

This module collects the mathematical propositions and formal deductive systems targeted by the conjecture-checking Turing machines in this repository, separated from the Turing machine tape constructions and halting proofs:

    Goldbach's Conjecture (GoldbachConjecture): Every even integer greater than 2 is the sum of two primes (goldbach_25, goldbach_21).

    Riemann Hypothesis (RiemannHypothesis and MatiyasevichRiemannCounterexample): Mathlib's RiemannHypothesis (riemann_744, riemann_120, riemann_104), together with the elementary harmonic/LCM counterexample inequality MatiyasevichRiemannCounterexample directly tested by riemann_744.

    Zermelo–Fraenkel Set Theory Consistency (ZFInconsistent vs. WadeZFInconsistent): Formula encoding via Cantor pairing (cantorPair, ZFFormula) and the two Hilbert systems analyzed in Cryptids.Semantics.Zf:

      ZFProvable / ZFInconsistent: Stefan O'Rear's zf2.nql (and Andrew Wade's post-10fcf152b3 zf2.py) Hilbert system, proved sound in Mathlib's ZFSet.{0} (not_zfInconsistent).

      WadeZFProvable / WadeZFInconsistent: the 20-clause Hilbert system actually enumerated by Andrew Wade's published 432-state Turing machine zf_432_wade.tm (zf2.py prior to commit 10fcf152b3), which differs from ZFProvable in clauses B6a, B8a, and B8c due to a register-restoration bug in B6a (main().n_140.1 restoring scratch1 into param1 instead of param3).

@[expose] public sectionnamespace ConjectureMachines

1. Goldbach's Conjecture

Goldbach's Conjecture: every even integer greater than 2 is the sum of two primes.

def GoldbachConjecture : Prop := ∀ n : ℕ, 2 < n → Even n → ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q

2. Riemann Hypothesis

Unreduced harmonic numerator computed by the loop num = num * i + denom; denom = denom * i in riemann.nql: harmNum n / n! = ∑_{i=1}^n 1 / i = harmonic n.

def harmNum : ℕ → ℕ | 0 => 0 | n + 1 => harmNum n * (n + 1) + n.factorial

The elementary integer inequality tested at stage x by riemann.nql (Matiyasevich, Aaronson, and O'Rear 2016): for $x > 253$ and $L_x = \operatorname{lcm}(1, \dots, x)$, $$b \cdot c < a \cdot d \iff H_{L_x} > x ;\wedge; (H_{L_x} - x)^2 > x \cdot H_x^4.$$ In Cryptids.Semantics.Riemann, (∃ x : ℕ, MatiyasevichRiemannCounterexample x) is proved equivalent to ¬ RiemannHypothesis.

def MatiyasevichRiemannCounterexample (x : ℕ) : Prop := 253 < x ∧ let lcm := (Finset.Icc 1 x).lcm id let a := (harmNum lcm - lcm.factorial * x) ^ 2 let b := lcm.factorial ^ 2 let c := harmNum x ^ 4 * x let d := x.factorial ^ 4 b * c < a * d

3. Zermelo–Fraenkel Set Theory Consistency (ZFInconsistent vs. WadeZFInconsistent)

The Cantor pairing function $\operatorname{cantorPair}(x, y) = x + \frac{(x+y)(x+y+1)}{2}$ computed by builtin_pair in zf2.nql.

def cantorPair (x y : ℕ) : ℕ := x + (x + y) * (x + y + 1) / 2

Gödel number of the atomic equality formula $v_x = v_y$ (weq in zf2.nql).

def zfEq (x y : ℕ) : ℕ := cantorPair (cantorPair x y) 0

Gödel number of the atomic membership formula $v_x \in v_y$ (wel in zf2.nql).

def zfMem (x y : ℕ) : ℕ := cantorPair (cantorPair x y) 1

Gödel number of the implication formula $\varphi \to \psi$ (wim in zf2.nql).

def zfImp (φ ψ : ℕ) : ℕ := cantorPair (cantorPair φ ψ) 2

Gödel number of the negation formula $\neg \varphi$ (wn in zf2.nql).

def zfNot (φ : ℕ) : ℕ := cantorPair φ 3

Gödel number of the universal formula $\forall v_x, \varphi$ (wal in zf2.nql).

def zfAll (x φ : ℕ) : ℕ := cantorPair (cantorPair x φ) 4

Gödel number of the existential abbreviation $\exists v_x, \varphi \equiv \neg \forall v_x \neg \varphi$ (wex in zf2.nql).

def zfEx (x φ : ℕ) : ℕ := zfNot (zfAll x (zfNot φ))

Gödel number of the conjunction abbreviation $\varphi \land \psi \equiv \neg (\varphi \to \neg \psi)$ (wa in zf2.nql).

def zfAnd (φ ψ : ℕ) : ℕ := zfNot (zfImp φ (zfNot ψ))

Well-formed formulas of first-order set theory with variables indexed by ℕ.

inductive ZFFormula : Type where | eq (x y : ℕ) : ZFFormula | mem (x y : ℕ) : ZFFormula | imp (φ ψ : ZFFormula) : ZFFormula | not (φ : ZFFormula) : ZFFormula | all (x : ℕ) (φ : ZFFormula) : ZFFormula deriving DecidableEq, Reprnamespace ZFFormula

Existential quantification abbreviation $\exists v_x, \varphi \equiv \neg \forall v_x \neg \varphi$.

def ex (x : ℕ) (φ : ZFFormula) : ZFFormula := .not (.all x (.not φ))

Conjunction abbreviation $\varphi \land \psi \equiv \neg (\varphi \to \neg \psi)$.

def and (φ ψ : ZFFormula) : ZFFormula := .not (.imp φ (.not ψ))

The Gödel number of a ZFFormula, matching zf2.nql.

def code : ZFFormula → ℕ | .eq x y => zfEq x y | .mem x y => zfMem x y | .imp φ ψ => zfImp φ.code ψ.code | .not φ => zfNot φ.code | .all x φ => zfAll x φ.code

Tarski satisfaction of a ZFFormula in Mathlib's cumulative hierarchy ZFSet.{u} under a variable assignment v : ℕ → ZFSet.{u}.

def Holds (v : ℕ → ZFSet.{u}) : ZFFormula → Prop | .eq x y => v x = v y | .mem x y => v x ∈ v y | .imp φ ψ => φ.Holds v → ψ.Holds v | .not φ => ¬ φ.Holds v | .all x φ => ∀ s : ZFSet.{u}, φ.Holds (Function.update v x s)end ZFFormula

Axiom scheme B1: $(\varphi \to \psi) \to ((\psi \to \chi) \to (\varphi \to \chi))$.

def axB1 (φ ψ χ : ℕ) : ℕ := zfImp (zfImp φ ψ) (zfImp (zfImp ψ χ) (zfImp φ χ))

Axiom scheme B2: $(\neg \varphi \to \varphi) \to \varphi$.

def axB2 (φ : ℕ) : ℕ := zfImp (zfImp (zfNot φ) φ) φ

Axiom scheme B3: $\varphi \to (\neg \varphi \to \psi)$.

def axB3 (φ ψ : ℕ) : ℕ := zfImp φ (zfImp (zfNot φ) ψ)

Axiom scheme B4: $\forall v_x (\varphi \to \psi) \to (\forall v_x \varphi \to \forall v_x \psi)$.

def axB4 (x φ ψ : ℕ) : ℕ := zfImp (zfAll x (zfImp φ ψ)) (zfImp (zfAll x φ) (zfAll x ψ))

Axiom scheme B6a: $(v_x = v_y \to \forall v_z, v_x = v_y) \land (v_x \in v_y \to \forall v_z, v_x \in v_y)$.

def axB6a (x y z : ℕ) : ℕ := zfAnd (zfImp (zfEq x y) (zfAll z (zfEq x y))) (zfImp (zfMem x y) (zfAll z (zfMem x y)))

Axiom scheme B6b: $\forall v_x \forall v_y \varphi \to \forall v_y \forall v_x \varphi$.

def axB6b (x y φ : ℕ) : ℕ := zfImp (zfAll x (zfAll y φ)) (zfAll y (zfAll x φ))

Axiom scheme B6c: $\exists v_x \forall v_x \varphi \to \varphi$.

def axB6c (x φ : ℕ) : ℕ := zfImp (zfEx x (zfAll x φ)) φ

Axiom scheme B7: $\exists v_x, v_x = v_y$.

def axB7 (x y : ℕ) : ℕ := zfEx x (zfEq x y)

Axiom scheme B8a: $v_x = v_y \to (v_x = v_z \to v_y = v_z)$.

def axB8a (x y z : ℕ) : ℕ := zfImp (zfEq x y) (zfImp (zfEq x z) (zfEq y z))

Axiom scheme B8b: $v_x = v_y \to (v_x \in v_z \to v_y \in v_z)$.

def axB8b (x y z : ℕ) : ℕ := zfImp (zfEq x y) (zfImp (zfMem x z) (zfMem y z))

Axiom scheme B8c: $v_x = v_y \to (v_z \in v_x \to v_z \in v_y)$.

def axB8c (x y z : ℕ) : ℕ := zfImp (zfEq x y) (zfImp (zfMem z x) (zfMem z y))

Axiom of Extensionality (EXT): $\forall v_2 ((v_2 \in v_0 \to v_2 \in v_1) \land (v_2 \in v_1 \to v_2 \in v_0)) \to v_0 = v_1$.

def axExt : ℕ := zfImp (zfAll 2 (zfAnd (zfImp (zfMem 2 0) (zfMem 2 1)) (zfImp (zfMem 2 1) (zfMem 2 0)))) (zfEq 0 1)

Helper formula $\exists v_3 (v_3 \in v_0 \land \forall v_1 \varphi)$ used in axRep.

def axRepRhs (φ : ℕ) : ℕ := zfEx 3 (zfAnd (zfMem 3 0) (zfAll 1 φ))

Axiom scheme of Replacement (REP): $\forall v_3 \exists v_1 \forall v_2 (\forall v_1 \varphi \to v_2 = v_1) \to \exists v_1 \forall v_2 ((v_2 \in v_1 \to \exists v_3 (v_3 \in v_0 \land \forall v_1 \varphi)) \land (\exists v_3 (v_3 \in v_0 \land \forall v_1 \varphi) \to v_2 \in v_1))$.

def axRep (φ : ℕ) : ℕ := zfImp (zfAll 3 (zfEx 1 (zfAll 2 (zfImp (zfAll 1 φ) (zfEq 2 1))))) (zfEx 1 (zfAll 2 (zfAnd (zfImp (zfMem 2 1) (axRepRhs φ)) (zfImp (axRepRhs φ) (zfMem 2 1)))))

Axiom of Power Set (POW): $\exists v_1 \forall v_2 (\forall v_3 (v_3 \in v_2 \to v_3 \in v_0) \to v_2 \in v_1)$.

def axPow : ℕ := zfEx 1 (zfAll 2 (zfImp (zfAll 3 (zfImp (zfMem 3 2) (zfMem 3 0))) (zfMem 2 1)))

Axiom of Union (UNI): $\exists v_1 \forall v_2 (\exists v_3 (v_2 \in v_3 \land v_3 \in v_0) \to v_2 \in v_1)$.

def axUni : ℕ := zfEx 1 (zfAll 2 (zfImp (zfEx 3 (zfAnd (zfMem 2 3) (zfMem 3 0))) (zfMem 2 1)))

Helper singleton-characterization formula $\forall v_1 ((v_1 \in v_2 \to v_1 = v_0) \land (v_1 = v_0 \to v_1 \in v_2))$ used in axInf.

def axInfSingleton : ℕ := zfAll 1 (zfAnd (zfImp (zfMem 1 2) (zfEq 1 0)) (zfImp (zfEq 1 0) (zfMem 1 2)))

Axiom of Infinity (INF): $\exists v_1 (v_0 \in v_1 \land \forall v_0 (v_0 \in v_1 \to \exists v_2 (v_2 \in v_1 \land \forall v_1 (v_1 \in v_2 \leftrightarrow v_1 = v_0))))$.

def axInf : ℕ := zfEx 1 (zfAnd (zfMem 0 1) (zfAll 0 (zfImp (zfMem 0 1) (zfEx 2 (zfAnd (zfMem 2 1) axInfSingleton)))))

3a. O'Rear's zf2.nql Hilbert System (ZFProvable, ZFInconsistent)

The inductive provability predicate ZFProvable φ of Stefan O'Rear's zf2.nql (and Andrew Wade's post-10fcf152b3 zf2.py) Hilbert system for Zermelo–Fraenkel set theory, combining Tarski's substitution-free first-order system $S_2$ (B1..B8c, mp, gen) with the ZF axioms (ext, rep, pow, uni, inf). Proved sound in Mathlib's ZFSet.{0} in Cryptids.Semantics.Zf.Soundness.

inductive ZFProvable : ℕ → Prop where | moot : ZFProvable (zfEq 0 0) | mp {φ ψ : ℕ} : ZFProvable φ → ZFProvable (zfImp φ ψ) → ZFProvable ψ | gen (x : ℕ) {φ : ℕ} : ZFProvable φ → ZFProvable (zfAll x φ) | b1 (φ ψ χ : ℕ) : ZFProvable (axB1 φ ψ χ) | b2 (φ : ℕ) : ZFProvable (axB2 φ) | b3 (φ ψ : ℕ) : ZFProvable (axB3 φ ψ) | b4 (x φ ψ : ℕ) : ZFProvable (axB4 x φ ψ) | b6a (x y z : ℕ) (hxz : x ≠ z) (hzy : z ≠ y) : ZFProvable (axB6a x y z) | b6b (x y φ : ℕ) : ZFProvable (axB6b x y φ) | b6c (x φ : ℕ) : ZFProvable (axB6c x φ) | b7 (x y : ℕ) : ZFProvable (axB7 x y) | b8a (x y z : ℕ) : ZFProvable (axB8a x y z) | b8b (x y z : ℕ) : ZFProvable (axB8b x y z) | b8c (x y z : ℕ) : ZFProvable (axB8c x y z) | ext : ZFProvable axExt | rep (φ : ℕ) : ZFProvable (axRep φ) | pow : ZFProvable axPow | uni : ZFProvable axUni | inf : ZFProvable axInf

Inconsistency of O'Rear's ZFProvable Hilbert system: the contradiction formula $v_0 \in v_0$ (zfMem 0 0 = 1) is provable.

def ZFInconsistent : Prop := ZFProvable (zfMem 0 0)

3b. Wade's zf_432_wade.tm Hilbert System (WadeZFProvable, WadeZFInconsistent)

Provability predicate of the 20-clause Hilbert system implemented by Andrew Wade's published 432-state Turing machine zf_432_wade.tm (zf2.py prior to his August 31, 2025 bugfix commit 10fcf152b3).

Compared to ZFProvable, in zf_432_wade.tm the first distinctness check of clause B6a (param1 ≠ param3) restores scratch1 into param1 instead of param3 (main().n_140.1), draining param3 to 0. Consequently:

    b6a_wade tests x ≠ z ∧ y ≠ 0 instead of x ≠ z ∧ z ≠ y, and

    b8a_zero and b8c_zero instantiate z = 0 (param3 = 0).

inductive WadeZFProvable : ℕ → Prop where | moot : WadeZFProvable (zfEq 0 0) | mp {φ ψ : ℕ} : WadeZFProvable φ → WadeZFProvable (zfImp φ ψ) → WadeZFProvable ψ | gen (x : ℕ) {φ : ℕ} : WadeZFProvable φ → WadeZFProvable (zfAll x φ) | b1 (φ ψ χ : ℕ) : WadeZFProvable (axB1 φ ψ χ) | b2 (φ : ℕ) : WadeZFProvable (axB2 φ) | b3 (φ ψ : ℕ) : WadeZFProvable (axB3 φ ψ) | b4 (x φ ψ : ℕ) : WadeZFProvable (axB4 x φ ψ) | b6a_wade (x y z : ℕ) (hxz : x ≠ z) (hy : y ≠ 0) : WadeZFProvable (axB6a x y z) | b6b (x y φ : ℕ) : WadeZFProvable (axB6b x y φ) | b6c (x φ : ℕ) : WadeZFProvable (axB6c x φ) | b7 (x y : ℕ) : WadeZFProvable (axB7 x y) | b8a_zero (x y : ℕ) : WadeZFProvable (axB8a x y 0) | b8b (x y z : ℕ) : WadeZFProvable (axB8b x y z) | b8c_zero (x y : ℕ) : WadeZFProvable (axB8c x y 0) | ext : WadeZFProvable axExt | rep (φ : ℕ) : WadeZFProvable (axRep φ) | pow : WadeZFProvable axPow | uni : WadeZFProvable axUni | inf : WadeZFProvable axInf

Inconsistency of the WadeZFProvable Hilbert system enumerated by zf_432_wade.tm (zf_432): the contradiction formula $v_0 \in v_0$ (zfMem 0 0 = 1) is provable.

def WadeZFInconsistent : Prop := WadeZFProvable (zfMem 0 0)end ConjectureMachines