[mo271]

No description provided.

[TomZahavy]

Thanks, this is a nice foundation! I went through the trusted-base changes (Challenge.lean, Propositions.lean, comparator configs, READMEs) in detail and skimmed the proof modules. CI is green.

Spec check. I compared every PAProvable constructor against a textbook Hilbert-style PA:

• gen is unrestricted, which is fine since there are no hypotheses.
• all_elim/ex_intro/eq_subst are guarded by freeFor, and all_vacuous/ex_elim by hasFree.
• pa_ind substitutes S x for x, which is always free for x.
• PAModel.ind is the first-order schema.

I found no extra axioms. Together with not_paProvable_false and paProvable_sound_nat, that makes me comfortable with the definition. I also like that paHalts/paZFInconsistent don't need to be trusted by eye: the adequacy theorems pin their meaning in ℕ to the existing Halts/ZFInconsistent.

Requested changes:

1. Layering / instance perturbation. Propositions.lean now imports Cryptids.Machines, which declares global priority-10000 instances (e.g. instPreorderNatConstructive : Preorder ℕ). As a result, the existing MatiyasevichRiemannCounterexample had to be changed to (@Finset.Icc ℕ Nat.instPreorder Nat.instLocallyFiniteOrder 1 x), while Challenge.lean still has Finset.Icc 1 x. The comparator accepts this, but it silently edits an existing trusted definition, and future additions to Propositions.lean will hit the same trap. Could the TM-dependent PA definitions (paStep, paHalted, paHalts, possibly all of §4) move to their own module that imports Propositions + Machines, with the Icc change reverted? At minimum, please add a comment explaining the pinned instance.

2. Docs claim more is audited than is. Cryptids.lean, Cryptids/README.md and Semantics/README.md list paProvable_iff_holdsIn_all_models (and paProvable_sound) next to the audited theorems. Neither is in Challenge.lean or any comparator config. Please either add them to the challenge and to all.json/pa_semantics.json (this needs PAStructure/PAModel/HoldsIn in the challenge), or reword the docs as "proved, not comparator-audited". This matters more in #20, where completeness becomes load-bearing.

3. Doc accuracy nits:

   • Semantics/README.md says "positive formulas (PAFormula)", but they include imp/bot.
   • The README signature of paProvable_iff_holdsIn_all_models omits [PAStructure M].
   • "without relying on Lean's ambient type-theoretic strength" overstates this PR. All theorems here are still metatheoretic; the object-level PAProvable results only arrive in #20.
   • "PAProvable … cannot prove Con(PA) or Con(ZF)" (Challenge docstring) is Gödel II under the assumption that PA is consistent. Please say so, or soften it.

4. Housekeeping:

   • Please add a PR description: what's added, the trusted-base delta, and which theorems are constructive vs classical.
   • The branch currently conflicts with main in comparator/README.md (after #18). Please rebase and refresh the theorem counts.
   • FYI: CI only runs constructive.json and all.json, so pa_semantics.json is covered only indirectly. That's consistent with the other per-module configs.

Happy to approve once 1–3 are addressed.