Move Zeta23 into zeta23/ subdirectory (multi-project layout)

[jleder3]

Purpose

This repository has been renamed to formal-math and will host several independent Lean formalizations side by side, one self-contained Lake project per subdirectory. This PR moves the existing Zeta23 project into zeta23/ to make room; a percolation project follows in a separate PR.

What moved / what stayed

• Moved intact into zeta23/: Zeta23/, Zeta23.lean, comparator/, lakefile.toml, lake-manifest.json, lean-toolchain, README.md, AUDIT.md, NOTICE, formalization.yaml, .gitignore, plus a copy of LICENSE so the subdirectory remains a self-contained Apache-2.0 artifact.
• Stays at the root: LICENSE.
• New at the root: README.md (a short index of projects) and .gitignore (.lake/, **/.lake/).
• Only text edits: zeta23/README.md gains one sentence under the title saying the project lives in zeta23/ and is built from there; the stale github.com/anthropics/zeta-23-lean repository URL in zeta23/README.md and zeta23/AUDIT.md now points at github.com/anthropics/formal-math/tree/main/zeta23. comparator/README.md had no stale URL and is unchanged.

No .lean file, lakefile.toml, lake-manifest.json, lean-toolchain, formalization.yaml or comparator config changed. This is a pure rename: blob SHAs are unchanged, and the Zeta23/ and comparator/ tree SHAs on this branch are identical to those on main.

How to build now

cd zeta23
lake exe cache get
lake build
lake build Challenge Solution        # comparator libraries, likewise from zeta23/
lake env lean comparator/PrintAxioms.lean

All relative paths inside the project (srcDir = "comparator", comparator configs, README links) are project-relative and keep working from zeta23/.

Notes for maintainers

• Downstream Lake users that require this repository by git URL must add subDir = "zeta23" to that [[require]] entry once this lands. Tag v1.0 still points at the old root layout, so projects pinned to it are unaffected.
• Open PR Unconditional 0.6727556 simple-critical-line proportion: six-translate Montgomery–Taylor penalty with a kernel-checked 5D certificate (+ Union and LineDecimal topics) #17 targets the old root paths and will need a rebase onto zeta23/ (git rename detection should carry most of it).
• formalization.yaml moves with the project; its file: / comparator_config: paths are project-relative and unchanged. If the registry crawler only reads the repository root, that is a follow-up.
• The single commit was created through the GitHub API and is signed by GitHub (Verified).

Verification

• git diff --stat -M main...move-zeta23-subfolder: 340 files changed, 336 insertions(+), 120 deletions(-); name-status = 334 x R100, 1 x R099 (AUDIT.md, the URL fix), root README.md / .gitignore replaced, zeta23/README.md, zeta23/.gitignore, zeta23/LICENSE added. Zero content hunks in any .lean, .toml, .json, lean-toolchain or .yaml file.
• Tracked file count: 338 on main -> 341 on this branch (+ root README.md, root .gitignore, zeta23/LICENSE).
• zeta23/lakefile.toml, zeta23/lake-manifest.json, zeta23/lean-toolchain, zeta23/formalization.yaml, zeta23/Zeta23.lean, zeta23/NOTICE are byte-identical to their main counterparts; root is exactly LICENSE, README.md, .gitignore, zeta23/.
• A full lake build from zeta23/ was not run for this PR (the build machine available to me could not download the v4.33.0-rc2 toolchain); since no Lean source, lakefile, manifest or toolchain byte changed and the Zeta23/ and comparator/ trees are SHA-identical to main, the build is unaffected by construction. A reviewer with the toolchain cached can confirm with cd zeta23 && lake exe cache get && lake build.

[rfurman]

Approved with minor comment

[rfurman]

Not: could likely combine to just the top level gitignore