Add reproducible moving-sofa certificate generation recipe

README.md

@@ -43,6 +43,9 @@ To work on a single project you don't need the whole pool built — see the
 To regenerate the preserved Zeta5 numerical certificates, see the
 [certificate reproduction guide](scripts/zeta5-certificates/README.md).
 
+The [moving-sofa certificate recipe](python/lean_pool/sofa_certificates/README.md)
+regenerates its optimized certificate modules from pinned public inputs.
+
 ### Challenge mode
 
 [`Challenge/`](Challenge/) is the other half of the pool: open *statements* rather than finished proofs. A challenge is a theorem written in Mathlib vocabulary and left as `sorry`, registered in [`Challenge/challenges.yml`](Challenge/challenges.yml) alongside the English statement it is supposed to say. It is the only place `sorry` is allowed, and only for the declarations the registry lists — everything else in the file must be closed, and every other gate still applies.

python/lean_pool/sofa_certificates/README.md

@@ -0,0 +1,131 @@
+# Reproducing the moving-sofa Part E certificates
+
+This recipe regenerates all **32** files in
+`LeanPool/MovingSofa/GerverSofa/KernelOnly/PartE/Certificates/`, byte for byte,
+at content commit `9ac84ed0910d4615a0238a6d465b471d7cee53a0` in PR #548
+(see `data/outputs.json`).
+That corpus contains 323,037 lines and 25,086 named declarations. The recipe
+also verifies the intermediate 47-file layout at content commit
+`0f0182131407cb4e2f7b1234f07f34271982d46a` against its original digests.
+The recipe contains transformations, subdivision witnesses, module assignments,
+and checksums; it does not embed the final Lean files or a compressed copy of them.
+
+The source input is the public
+[MovingSofa commit 4d556913](https://github.com/deancureton/MovingSofa/tree/4d5569131940815f47a9ccf3e90a4c5043c56127).
+Its vendored GerverSofa source is derived from Dawid Trela's MIT-licensed
+[GerverSofaLean v1.1.0 release](https://github.com/dawidmtrela-dotcom/GerverSofaLean/releases/tag/v1.1.0).
+The release ZIP has SHA-256
+`7c496150f709ac709ae01f4836e9a702a18f752450efa69f15cf44264c0c2f77`.
+MovingSofa has subsequently pruned imports and unused semantic declarations and
+normalized whitespace. This recipe therefore uses the exact MovingSofa snapshot,
+not an assumption that the two trees are identical. Every input source file has
+its own SHA-256 in `data/inputs.json`. The original copyright attribution survives
+the transformations; the complete MIT notice is in `LeanPool/MovingSofa.lean`.
+
+## Run from a clean directory
+
+Requires the repository's Python 3.13+ environment. Generation itself does not
+require a Lean build or network access once the archive is downloaded. From the
+repository root, with `$TMPDIR` pointing to a suitable scratch disk:
+
+```bash
+curl --fail --location \
+  https://codeload.github.com/deancureton/MovingSofa/tar.gz/4d5569131940815f47a9ccf3e90a4c5043c56127 \
+  --output "$TMPDIR/MovingSofa-4d556913.tar.gz"
+cd python
+uv run python -m lean_pool.sofa_certificates generate \
+  --archive "$TMPDIR/MovingSofa-4d556913.tar.gz" \
+  --workspace "$TMPDIR/sofa-certificates-replay"
+```
+
+The workspace must not already exist. The command checks archive SHA-256
+`88538a166208cdb7ba2c4079a296c8d7becf18758c9b4540750d81b271e79f70`,
+reads only named archive members without extracting arbitrary paths, validates
+all witness trees, and runs the ordered source transformations. It requires all
+32 expected output digests to match before reporting success. The generated
+files are under the workspace's `pool/LeanPool/MovingSofa/.../Certificates/`.
+`verification.json` records the archive digest, every final output digest, and elapsed
+wall time. Intermediate source and audit reports remain available for inspection.
+The command never writes to the content checkout.
+
+To compare a content checkout directly against the expected corpus:
+
+```bash
+uv run python -m lean_pool.sofa_certificates verify \
+  /path/to/content-checkout/LeanPool/MovingSofa/GerverSofa/KernelOnly/PartE/Certificates
+```
+
+## Recompute the subdivision witnesses
+
+The checked-in witnesses are search results, not trusted mathematical premises.
+Every generated terminal proof uses `decide +kernel`; every internal node uses
+the proved four-child cover lemma. An incorrect numerical witness fails Lean's
+kernel check. Structural validation also rejects missing quadrants, overlapping
+leaves, wrong remaining depths and invalid path digits before source generation.
+
+The separate search command recomputes all **10,801 leaves across 550 roots**.
+It requires the content checkout at the pinned commit, Lean v4.34.0 and Mathlib
+`5ed2965256430c3649e86755f9576b54eca72435`, with the semantic prerequisites built:
+
+```bash
+# In the content checkout:
+lake build LeanPool.MovingSofa.GerverSofa.KernelOnly.Core.Bundle005
+
+# In this tooling checkout's python/ directory:
+uv run python -m lean_pool.sofa_certificates.discover \
+  --pool /path/to/content-checkout \
+  --workspace "$TMPDIR/sofa-cover-search"
+```
+
+This creates an inspectable `Discover.lean`, runs the rational interval evaluator,
+and requires byte-identical results for both witness sets. Four subdivision digits
+mean LL, LH, HL, HH, in that order. Search checks physical irrelevance, membership
+of the already-certified local cell, and interval rejection before descending.
+All leaves in these particular inputs end in interval rejection. The standalone
+search uses evaluation to find witnesses; it does not add evaluation commands or
+trust assumptions to the imported library.
+
+## Transformation stages and maintenance
+
+1. Import the 814 pinned Part E source files with namespaced imports and headers.
+2. Factor large closed proof subtrees into named lemmas; share repeated subdivision
+   paths every four levels. Re-expansion checks the original source text exactly.
+3. Normalize visibility, module documentation, resource options, API names and
+   line wrapping. Rename source modules and split the long theta reconstruction.
+4. Expand 549 selected adaptive checks using the recorded quadtree witnesses,
+   plus the separately profiled depth-nine phi-above check. Leaves are checked
+   in the kernel and internal nodes compose existing soundness lemmas.
+5. Assemble the 804 resulting generated fragments into the recorded 46 batches.
+   Hoist private cell aliases, document public aliases, and expand roots whose
+   earlier aliases would otherwise become forward references. Expansion audits
+   check identical unary subdivision paths.
+6. Move 119 pure combination fragments to `Reconstruction.lean`, preserving all
+   25,086 public declaration names. This lets expensive leaf modules build in
+   parallel. Normalize trailing whitespace and check all 47 intermediate digests.
+7. Repack those modules into 32 certificate bundles, moving closed cell definitions
+   before proof bodies, removing vacuous namespaces and preserving all names.
+   This keeps the combined pool index below its size limit after main gained a
+   further project. Check every final output digest.
+
+`data/batch-assignment.json` records ordered source fragments;
+`data/module-consolidation-map.json` records import relocation, including semantic
+modules outside the emitted corpus. `data/cover-expansion-candidates.json` records
+each selected theorem, root region, subdivision path and recursion budget.
+`data/final-batch-assignment.json` and `data/final-module-map.json` record the
+subsequent packing and semantic import relocation. These are explicit inputs
+to the deterministic recipe. No current build timings,
+GitHub credentials, machine-specific source paths or private generator are needed.
+
+This is a reproduction of the **imported and optimized certificate corpus from
+public upstream source**, not a claim to recover the upstream author's private
+search history or regenerate the whole MovingSofa project from the paper alone.
+The 22 other imported modules contain semantic and geometric proofs and are
+outside this recipe. Mathematical changes to a cover domain or evaluator require
+new witness search, reviewed source changes and the usual full Lean validation;
+updating a checksum alone does not certify such a change. The expected digests
+are tied to this content version and intentionally fail after an unrecorded port.
+
+The initial clean replay verified all 47 intermediate modules in 25.42 seconds;
+the complete replay including all 32 final bundles took 70.14 seconds on the
+shared Azure VM. These measure source generation only. The import PR separately records
+controlled Lean compile benchmarks and complete CI validation.

python/lean_pool/sofa_certificates/__init__.py

@@ -0,0 +1 @@
+"""Reproduce the moving-sofa Part E certificate corpus."""

python/lean_pool/sofa_certificates/__main__.py

@@ -0,0 +1,211 @@
+"""Reproduce the moving-sofa Part E certificate modules from pinned inputs."""
+
+import argparse
+import hashlib
+import importlib
+import json
+import logging
+import re
+import shutil
+import time
+from pathlib import Path
+from tarfile import open as open_tar
+
+DATA = Path(__file__).parent / "data"
+ARCHIVE_SHA256 = "88538a166208cdb7ba2c4079a296c8d7becf18758c9b4540750d81b271e79f70"
+ARCHIVE_PREFIX = (
+    "MovingSofa-4d5569131940815f47a9ccf3e90a4c5043c56127/vendor/gerver-sofa/"
+)
+PROJECT = Path("LeanPool/MovingSofa")
+CERTIFICATES = PROJECT / "GerverSofa/KernelOnly/PartE/Certificates"
+STAGES = (
+    "split_proofs",
+    "share_cells",
+    "normalize",
+    "rename",
+    "module_names",
+    "wrap",
+    "split_reconstruction",
+    "expand",
+    "special_cover",
+    "consolidate",
+    "repair_roots",
+    "wrap_roots",
+    "public_root",
+    "separate_joins",
+    "bundle_certificates",
+)
+
+
+def digest(content: bytes) -> str:
+    """Return the content's SHA-256 digest."""
+    return hashlib.sha256(content).hexdigest()
+
+
+def validate_leaves(leaves: dict[str, int], depth: int) -> None:
+    """Reject incomplete, overlapping or incorrectly labelled cover trees."""
+    if not leaves:
+        raise ValueError("Empty cover")
+    nodes = {""}
+    for path, remaining in leaves.items():
+        if re.fullmatch("[0-3]*", path) is None or remaining != depth - len(path):
+            raise ValueError("Invalid cover path or remaining depth")
+        if remaining < 0:
+            raise ValueError("Cover exceeds its depth")
+        nodes.update(path[:index] for index in range(1, len(path) + 1))
+    for path in nodes:
+        children = {path + str(index) for index in range(4)}
+        if path in leaves:
+            if children & nodes:
+                raise ValueError("Overlapping cover leaves")
+        elif not children <= nodes:
+            raise ValueError("Incomplete cover")
+
+
+def validate_witnesses() -> None:
+    """Check every recorded tree before emitting any proof source."""
+    candidates = json.loads((DATA / "cover-expansion-candidates.json").read_text())
+    trees = {}
+    for line in (DATA / "cover-bulk-discovery.jsonl").read_text().splitlines():
+        identity, path, depth, reason = line.split("|")
+        tree = trees.setdefault(int(identity), {})
+        if reason != "rejected" or path in tree:
+            raise ValueError("Invalid or duplicate cover witness")
+        tree[path] = int(depth)
+    if set(trees) != {item["id"] for item in candidates}:
+        raise ValueError("Cover candidate IDs do not match the witnesses")
+    for item in candidates:
+        validate_leaves(trees[item["id"]], item["depth"])
+    special = {}
+    for line in (DATA / "cover-special-discovery.txt").read_text().splitlines():
+        marker, path, depth, reason = line.split("|")
+        if marker != "COVER" or reason != "rejected" or path in special:
+            raise ValueError("Invalid special-cover witness")
+        special[path] = int(depth)
+    validate_leaves(special, 9)
+
+
+def prepare_source(source: str) -> str:
+    """Apply the import's visibility, module prefix and attribution headers."""
+    source = re.sub(
+        r"^(?:public )?import\s+([\w.]+)",
+        lambda match: (
+            "public import "
+            + (
+                "LeanPool.MovingSofa." + match[1]
+                if match[1].startswith(("GerverSofa.", "LeanCert."))
+                else match[1]
+            )
+        ),
+        source,
+        flags=re.M,
+    )
+    header = (
+        "/-\nCopyright (c) 2026 Dawid Trela. All rights reserved.\n"
+        "Released under MIT license as described in the file LICENSE.\n"
+        "Authors: Dawid Trela\n-/\nmodule\n\n"
+    )
+    source = header + source
+    imports = list(re.finditer(r"^public import[^\n]*\n", source, re.M))
+    if imports:
+        index = imports[-1].end()
+        source = source[:index] + "\n@[expose] public section\n" + source[index:]
+    return source
+
+
+def read_sources(archive: Path) -> dict[str, str]:
+    """Read only checksum-pinned source members without extracting archive paths."""
+    if digest(archive.read_bytes()) != ARCHIVE_SHA256:
+        raise ValueError("Upstream release archive SHA-256 mismatch")
+    manifest = json.loads((DATA / "inputs.json").read_text())
+    sources = {}
+    with open_tar(archive) as zipped:
+        for module, expected in manifest.items():
+            if re.fullmatch(r"GerverSofa\.KernelOnly\.PartE\.[\w.]+", module) is None:
+                raise ValueError("Unexpected upstream module name")
+            member = ARCHIVE_PREFIX + module.replace(".", "/") + ".lean"
+            handle = zipped.extractfile(member)
+            if handle is None:
+                raise ValueError(f"Missing source: {module}")
+            content = handle.read()
+            if digest(content) != expected:
+                raise ValueError(f"Upstream source SHA-256 mismatch: {module}")
+            sources[module] = content.decode("utf-8")
+    return sources
+
+
+def verify_outputs(
+    folder: Path, manifest: Path = DATA / "outputs.json"
+) -> dict[str, str]:
+    """Require the exact expected file set and all expected source digests."""
+    expected = json.loads(manifest.read_text())
+    for entry in folder.iterdir():
+        if entry.is_dir() or entry.is_symlink():
+            raise ValueError(f"Unexpected directory or symbolic link: {entry.name}")
+    actual = {path.name: digest(path.read_bytes()) for path in folder.glob("*.lean")}
+    if actual != expected:
+        changed = sorted(
+            name
+            for name in actual.keys() | expected.keys()
+            if actual.get(name) != expected.get(name)
+        )
+        raise ValueError(f"Reproduction mismatch: {changed}")
+    return actual
+
+
+def reproduce(archive: Path, workspace: Path) -> None:
+    """Run the source pipeline in a new directory, refusing existing output."""
+    started = time.monotonic()
+    sources = read_sources(archive)
+    validate_witnesses()
+    workspace.mkdir(parents=True, exist_ok=False)
+    for resource in DATA.iterdir():
+        shutil.copyfile(resource, workspace / resource.name)
+    for module, source in sources.items():
+        target = workspace / "pool" / PROJECT / (module.replace(".", "/") + ".lean")
+        target.parent.mkdir(parents=True, exist_ok=True)
+        target.write_text(prepare_source(source))
+    for name in STAGES:
+        if name == "bundle_certificates":
+            for path in (workspace / "pool" / CERTIFICATES).glob("*.lean"):
+                path.write_text(path.read_text().rstrip() + "\n")
+            verify_outputs(
+                workspace / "pool" / CERTIFICATES, DATA / "intermediate-outputs.json"
+            )
+        print(f"Running {name}", flush=True)
+        stage = importlib.import_module(f"lean_pool.sofa_certificates.stages.{name}")
+        stage.run(workspace)
+    folder = workspace / "pool" / CERTIFICATES
+    for path in folder.glob("*.lean"):
+        path.write_text(path.read_text().rstrip() + "\n")
+    hashes = verify_outputs(folder)
+    report = {
+        "archive_sha256": ARCHIVE_SHA256,
+        "files": hashes,
+        "wall_seconds": time.monotonic() - started,
+    }
+    (workspace / "verification.json").write_text(json.dumps(report, indent=2) + "\n")
+    print(f"Verified {len(hashes)} byte-identical certificate modules in {folder}")
+
+
+def main() -> None:
+    """Run a fresh reproduction or verify an existing certificate directory."""
+    parser = argparse.ArgumentParser(description=__doc__)
+    commands = parser.add_subparsers(dest="command", required=True)
+    generate = commands.add_parser("generate")
+    generate.add_argument("--archive", type=Path, required=True)
+    generate.add_argument("--workspace", type=Path, required=True)
+    verify = commands.add_parser("verify")
+    verify.add_argument("directory", type=Path)
+    arguments = parser.parse_args()
+    logging.basicConfig(level=logging.INFO, format="%(message)s")
+    if arguments.command == "generate":
+        reproduce(arguments.archive.resolve(), arguments.workspace.resolve())
+    else:
+        print(
+            f"Verified {len(verify_outputs(arguments.directory))} certificate modules"
+        )
+
+
+if __name__ == "__main__":
+    main()