Add reproducible moving-sofa certificate generation recipe

[Vilin97]

The generated-certificate review finding on #548 needs a public regeneration recipe. This adds a deterministic source pipeline from checksum-pinned public upstream input to all 47 intermediate Part E certificate modules at 0f018213 and all 32 final bundles at 9ac84ed0. The pipeline preserves all 25,086 declaration names and checks every output digest.

The recipe includes the actual subtree factoring, shared-cell generation, cover expansion, batching, root repairs and parallel reconstruction layout. Its inputs are the original public Lean source, recorded subdivision trees and module assignments; it contains no embedded final certificate corpus. A separate Lean search recomputes all 10,801 leaves over 550 roots and verifies the recorded witnesses exactly. The documentation distinguishes this scope from regenerating the whole upstream mathematical project.

Validation:

• Clean end-to-end reproduction: all 47 intermediate files and 32 final bundles byte-identical in 70.14 seconds.
• Independent rational-interval search: all 10,801 witness leaves match.
• Full Python suite: 512 tests passed; Ruff check and format check passed.
• Existing output directories are refused; archive and per-source checksums are required; no content checkout is mutated.

This companion PR keeps tooling separate from the content-only import. The final packing in #548 is reproduced exactly. The independent search now imports only Core.Bundle005, so it does not require the generated Part E corpus to be built first.

[Vilin97]

/review

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low risk] Adds a reproducible recipe for generating mathematical certificate files.

No new actionable issue was identified, and the PR appears safe to merge.

Summary

The PR adds a checksum-pinned recipe for regenerating the moving-sofa Part E certificate modules, plus witness-search tooling and a representative transformation fixture. Since the previous review, it also rejects nested entries during output verification and adds regression coverage.

_{Reviews (2) · Last reviewed commit: "Cover nested files and production transf..."}

[Vilin97]

🤖 LLM review — refactor (gpt-6-astra)

Reviewed head: b2726a0cc37ec1a2958649213d2a87f3c2587238

Verdict: ✅ approve

This adds a staged certificate regeneration recipe with pinned inputs, structural witness checks, declaration-name audits and exact output verification, without changing pooled Lean proofs. A clean replay reproduced all 47 intermediate modules and 32 final bundles; all 79 digests also matched the pinned content commits. The 12 focused tests passed. The separate Lean search was inspected but not rerun because compiled prerequisites were unavailable. The tooling improves reproducibility without introducing a concrete maintainability regression.

Aspect	Value
Scope	certificate regeneration tooling
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The explicit transformation stages and verified reproduction make the certificate corpus easier to maintain, with no actionable regression found.

---

Tokens: 909,689 in / 7,448 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $18.7524 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Substantive review of b2726a0cc37ec1a2958649213d2a87f3c2587238: the SHA-pinned public archive and per-module input digests bound the recipe's source. An independent bounded replay checked all 47 intermediate and 32 final manifest entries; the 32 generated certificates are byte-identical to #548 at 9ac84ed0910d4615a0238a6d465b471d7cee53a0, with the same 25,086 certificate declaration names. The two P2 findings on the earlier head are addressed: verification rejects nested directories and symlinks, and a production-subtree fixture exercises ordered transformations. I ran the exact current head locally: 512 Python tests pass, and Ruff check and formatting pass. I found no remaining substantive blocker in this infrastructure PR.

Disposition: approved, integration/checks pending. The protected separation and documentation preflight checks and Python CI are green. Build project is still pending in Lean Action CI run 36483811961. Re-read the branch head, main, unresolved threads, and required checks before an ordinary protected squash merge. #548's separate content build remains its own merge gate.

[Vilin97]

/review