Reduce the Riemann Hypothesis machine from 104 to 95 states

[winger]

Adds a 95-state, two-symbol Turing machine that halts from the blank tape if and only if Mathlib's RiemannHypothesis is false, reducing the existing bound by nine states.

The construction retains the stage counter in x after FOLD and permutes the physical register banks. The proof covers the exact 3,634-step blank initializer, physical execution, and unbounded stage progression, then connects the resulting arithmetic criterion to the existing Riemann104 semantics. Auxiliary machine presentations are derived from the literal transition table by state expansion and renaming.

Proof entry points

• Cryptids/Semantics/Riemann95.lean: unconditional end-to-end theorem.
• Cryptids/Riemann95.lean: blank-tape counterexample criterion and equivalence to Riemann104.
• Cryptids/ReductionSupport/Riemann95/README.md: proof structure and reading order.
• artifacts/riemann_95/: transition table and initializer verification.

Verification

lake build
lake comparator --config comparator/all.json
python3 verify.py

The comparator includes an independent specification of the machine and its three public theorems.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[mo271]

Hey, fantastic to see a newer, shorter machine for RH!
Thanks for the contribution!

I know this is still marked as draft, so probably some of the following points would have been addressed, but since I had taken a look anyhow:

• Proofs: The reduction and Lean proofs look great and completely kernel-sound
• Challenge & machine loading: Instead of adding Riemann95Challenge.lean and hardcoding the table literal in Cryptids/Riemann95Definition.lean, please load artifacts/riemann_95/machine.txt via load_machine_rows% directly in Cryptids/Machines.lean and Challenge.lean (like all other machines). That also keeps comparator/all.json pointed at Challenge.
• Verifier: Please fold the SHA-256 and 3,634-step bootstrap checks into the root verify.py instead of adding a standalone artifacts/riemann_95/verify.py.
• Copyright headers: 19 of the 47 new Lean files are missing the Copyright (c) 2026 Google LLC. All rights reserved. line (WordGuard.lean is also missing Google LLC).
• Docs: Please add the author credit to the riemann_95 row in RELATED_WORK.md, add a bullet for riemann_95 under ## Runtime Step Behavior in Cryptids/README.md, and fix the missing space in Literal95-state in Cryptids/Riemann95Definition.lean (if kept).

[winger]

Thanks for the careful review! I’ve pushed an update addressing each point:

• RH95 now loads machine.txt through load_machine_rows% in both Cryptids/Machines.lean and Challenge.lean. The separate challenge and hardcoded table are removed, and the comparator uses Challenge.
• SHA-256 and complete 3,634-step bootstrap checks now live in root verify.py; the standalone verifier is removed.
• Added the requested Google copyright headers throughout.
• Added the author credit and runtime entry, and corrected the machine-definition wording.
  The build, full comparator with default-kernel replay, and root verifier passed locally. Ready for another look!