Add deeply embedded first-order Peano Arithmetic

Cryptids.lean

@@ -13,6 +13,7 @@ public import Cryptids.Riemann120
 public import Cryptids.Zf380
 public import Cryptids.Zf393
 public import Cryptids.Semantics.Goldbach
+public import Cryptids.Semantics.PA
 public import Cryptids.Semantics.Riemann
 public import Cryptids.Semantics.Riemann120
 public import Cryptids.Semantics.Riemann95
@@ -29,7 +30,9 @@ known baseline machines (`goldbach_25`, `zf_432`, `zf_393`, `riemann_744`, `riem
 linking every machine's blank-tape halting problem to Mathlib's statements:
 
 - `Cryptids.Propositions` — Shared definitions of `GoldbachConjecture`,
-  `MatiyasevichRiemannCounterexample`, `ZFInconsistent`, and `WadeZFInconsistent`.
+  `MatiyasevichRiemannCounterexample`, `ZFInconsistent`, `WadeZFInconsistent`, and deeply embedded
+  first-order Peano Arithmetic (`PATerm`, `PAFormula`, `PAProvable`, `paHalts`,
+  `paZFInconsistent`).
 - `Cryptids.Machines` — Turing machine execution model, bundled machines (`BundledMachine`), and
   machine table definitions (`ConjectureMachines.Machines.*`).
 - `Cryptids.Goldbach21`, `Cryptids.Zf380`, `Cryptids.Riemann104` — Proofs of
@@ -47,6 +50,11 @@ linking every machine's blank-tape halting problem to Mathlib's statements:
 - `Cryptids.Riemann95`, `Cryptids.Semantics.Riemann95` — A 95-state machine with an exact
   3,634-step blank initializer, unconditional equivalence to the 104-state machine, and
   `Halts candidate ↔ ¬ RiemannHypothesis`.
+- `Cryptids.Semantics.PA` — First-order Peano Arithmetic metatheory: arbitrary `[PAModel M]`
+  soundness (`paProvable_sound`, `paProvable_sound_nat`), constructive consistency
+  (`not_paProvable_false`), constructive $\Sigma_1^0$ standard-model adequacy
+  (`paHalts_holds_iff_halts`, `paZFInconsistent_holds_iff_zfInconsistent`), and Gödel–Henkin
+  completeness (`paProvable_iff_holdsIn_all_models`).
 - `Cryptids.Semantics.Goldbach`, `Cryptids.Semantics.Zf`, `Cryptids.Semantics.Riemann` —
   End-to-end proofs linking halting from the blank tape to the corresponding mathematical
   conjectures across all baseline machines (`goldbach25`, `zf432`, `riemann744`).

Cryptids/README.md

@@ -24,6 +24,7 @@ All proofs in [`Cryptids/`](./) are checked by the Lean 4 kernel (`v4.35.0-rc4`)
 1. **State reductions:** Each reduced machine (`goldbach_21`, `zf_380`, `riemann_104`, `riemann_95`) has fewer states than its reference machine (`goldbach_25`, `zf_393`, `riemann_120`, `riemann_104`) and halts from the blank tape if and only if the reference machine halts ([`Goldbach21.lean`](./Goldbach21.lean), [`Zf380.lean`](./Zf380.lean), [`Riemann104.lean`](./Riemann104.lean), [`Riemann95.lean`](./Riemann95.lean)). The direct simulation reductions (`goldbach_21`, `zf_380`, `riemann_104`) and all four `candidate_fewer_states` theorems are completely constructive (`["propext", "Quot.sound"]`, zero `Classical.choice`), audited via [`comparator/constructive.json`](../comparator/constructive.json), [`comparator/goldbach_21.json`](../comparator/goldbach_21.json), [`comparator/zf_380.json`](../comparator/zf_380.json), and [`comparator/riemann_104.json`](../comparator/riemann_104.json), while [`riemann_95`](./Riemann95.lean) routes through the arithmetic stage predicate `ShuniaCounterexample` (`Nat.Prime`, audited via [`comparator/riemann_95.json`](../comparator/riemann_95.json)).
 2. **End-to-end mathematical semantics ([`Cryptids/Semantics/`](./Semantics/README.md)):**
    - **ZF Consistency (`zf_380`, `zf_393`, and `zf_432`):** Both `zf_380` and Wade's 393-state machine `zf_393` (incorporating upstream fix `10fcf152b3`) halt if and only if O'Rear's `zf2.nql` Hilbert system proves $v_0 \in v_0$ (`Halts candidate ↔ ZFInconsistent`, `Halts zf393 ↔ ZFInconsistent`), while `zf_432` halts if and only if the 20-clause deductive system enumerated by `zf_432_wade.tm` derives $v_0 \in v_0$ (`WadeZFInconsistent`). **All three proof-search equivalences are proved constructively in Lean using only `["propext", "Quot.sound"]` (no `Classical.choice`, no Excluded Middle, and no Markov's Principle)** and audited via [`comparator/constructive.json`](../comparator/constructive.json), blocking classical `Con(ZF)` shortcuts via [`Zf/Soundness.lean`](./Semantics/Zf/Soundness.lean) or `Classical.em` (while internalizing the reduction inside `PA`/`ZF` and establishing full `ZF`-independence remain separate from this Lean meta-level correspondence; see [`Semantics/README.md`](./Semantics/README.md#foundational-note-conzf-in-lean-and-constructive-equivalence)). Separately, [`Zf/Soundness.lean`](./Semantics/Zf/Soundness.lean) uses classical `ZFSet.{0}` (`Classical.choice`) to establish `not_zfInconsistent` and deduce unconditional non-halting (`not_halts_zf393`, `not_halts_candidate`) inside Lean's stronger meta-theory.
+   - **First-Order Peano Arithmetic (`PAProvable`, [`Semantics/PA.lean`](./Semantics/PA.lean)):** Deeply embeds first-order Peano Arithmetic (`PATerm`, `PAFormula`, `PAProvable`) and $\Sigma_1^0$ encodings `paHalts M` and `paZFInconsistent` in [`Propositions.lean`](./Propositions.lean) and [`Challenge.lean`](../Challenge.lean), proving constructive consistency (`not_paProvable_false`), constructive standard-model adequacy (`paHalts_holds_iff_halts`, `paZFInconsistent_holds_iff_zfInconsistent`; all three audited without `Classical.choice` in [`comparator/constructive.json`](../comparator/constructive.json)), standard-model soundness (`paProvable_sound_nat`), and Gödel–Henkin completeness (`paProvable_iff_holdsIn_all_models`) across arbitrary `[PAModel M]`.
    - **Goldbach (`goldbach_21` and `goldbach_25`):** Both `goldbach_21` and `goldbach_25` constructively satisfy `Halts M ↔ ∃ w, ¬ HasGoldbachPair (2 * w + 4)` without `Classical.choice` ([`Goldbach21.lean`](./Goldbach21.lean)), and with `Classical.choice` (for Markov's Principle on `¬ ∀ n, ...`) satisfy `Halts candidate ↔ ¬ GoldbachConjecture` ([`Semantics/Goldbach.lean`](./Semantics/Goldbach.lean)).
    - **Riemann Hypothesis (`riemann_95`, `riemann_104`, `riemann_120`, and `riemann_744`):** All four machines (`riemann_95`, `riemann_104`, Shunia's 120-state machine `riemann_120`, and the 744-state machine `riemann_744`) halt if and only if Mathlib's `RiemannHypothesis` is false (`Halts candidate ↔ ¬ RiemannHypothesis`, `Halts riemann120 ↔ ¬ RiemannHypothesis`, and `Halts riemann744 ↔ ¬ RiemannHypothesis`).
 

Cryptids/Semantics/PA.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Google LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+module
+
+public import Cryptids.Semantics.PA.Syntax
+public import Cryptids.Semantics.PA.Adequacy
+public import Cryptids.Semantics.PA.Completeness
+
+/-!
+# First-Order Peano Arithmetic Semantics, Adequacy, and Completeness (`Cryptids.Semantics.PA`)
+
+Re-exports the foundational metatheory of the deeply embedded Peano Arithmetic system `PAProvable`
+(`Cryptids.Propositions`):
+
+1. [`Cryptids.Semantics.PA.Syntax`](./PA/Syntax.lean):
+   General $\mathcal{L}_{\mathrm{PA}}$-structures (`PAStructure`), models (`PAModel`), classical
+   soundness (`paProvable_sound`, `paProvable_sound_nat`), and constructive consistency via the
+   Gödel–Gentzen negative translation (`not_paProvable_false`, zero `Classical.choice`).
+2. [`Cryptids.Semantics.PA.Adequacy`](./PA/Adequacy.lean):
+   Constructive standard-model adequacy of the $\Sigma_1^0$ arithmetizations of binary Turing
+   machine halting and `ZF` inconsistency (`paHalts_holds_iff_halts` and
+   `paZFInconsistent_holds_iff_zfInconsistent`, zero `Classical.choice`).
+3. [`Cryptids.Semantics.PA.Completeness`](./PA/Completeness.lean):
+   Gödel–Henkin soundness and completeness across all first-order `PAModel`s
+   (`paProvable_iff_holdsIn_all_models`).
+-/