Skip to content

README.md

Latest commit

 

History

History
131 lines (112 loc) · 7.37 KB

README.md

File metadata and controls

131 lines (112 loc) · 7.37 KB
Raw

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. Its vendored GerverSofa source is derived from Dawid Trela's MIT-licensed GerverSofaLean v1.1.0 release. 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:

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:

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:

# 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.