Import Gerver optimality for the moving sofa problem

[Vilin97]

Imports Gerver sofa optimality: the supremum of areas of closed, connected sets admitting a continuous rigid motion through a unit-width right-angle hallway equals the area of the explicit Gerver sofa. Supporting results prove admissibility and parameter uniqueness on the advertised domain. The contribution includes reusable convex-cap geometry, Stieltjes area, bounded variation, Jordan separation, polygon approximation, concave quadratic bounds and sound rational interval certificates.

Source, eligibility and provenance

• deancureton/MovingSofa, commit 4d5569131940815f47a9ccf3e90a4c5043c56127, Apache-2.0; AI provenance, produced using Codex and Claude Code under Dean Cureton's direction.
• Material Lean completion: a0753860f1d2b4424e059c35e64ad611be71a415, 2026-09-20 10:55:24 UTC. The imported revision has identical Lean sources and later documentation changes. Public announcement: 2026-09-20 18:42:40 UTC.
• Eligible interval: [2026-07-28T09:45:00.228628Z, 2026-09-21T09:45:00.228628Z). Registry, source tree, history, PR and issue searches found no previous import of this result.
• Mathematical references: Baek, Optimality of Gerver's Sofa, Theorem 1.1; Romik, Differential equations and exact solutions in the moving sofa problem, parameter equations and explicit formulas. The card does not claim a certified decimal area or uniqueness of the maximizing shape.

Dependency scope and attribution

The coherent upstream closure comprised 1,458 imported modules plus three existing LeanPool.Isoperimetric modules, which are reused. The final layout has 54 modules and 469,541 physical Lean lines: 32 Part E certificate bundles, eight Gerver core bundles, thirteen other mathematical modules and the entry point. Consolidation retains useful infrastructure and keeps the generated index at 9,994 code lines under the existing limit.

Retained dependency	Pinned source	License / attribution
GerverSofaLean	v1.1.0 release, published 2026-09-13; archive SHA-256 7c496150f709ac709ae01f4836e9a702a18f752450efa69f15cf44264c0c2f77	MIT, Dawid Trela
35 pure LeanCert modules	571a228555ae38742448854be81d7b59d994a8e3	Apache-2.0, Kirill Alkhimov and contributors
Four Jordan/Brouwer modules	b3c9b7cf7358bf81a077d78ad67e6e8247869ddd	Apache-2.0, Rado Kirov
Ten Tau Ceti modules	c52a81811e4626d2e9769fe9b0c701168c211332	Apache-2.0, original contributors credited in source
Formal Conjectures definitions	ddfbaf90f4482030d88aae5233fe933874296a23	Apache-2.0, original contributors credited in source

Copyright attribution and the complete MIT notice are retained. Existing Isoperimetric results retain Jonathan Ho's attribution. The project card records AI provenance and all three registered results.

Port, proof repair and reproduction

Ported to Lean v4.34.0 and Mathlib 5ed2965256430c3649e86755f9576b54eca72435. Changes include explicit module visibility, narrower imports, warning/linter repairs, proof decomposition, shared exact interval caches and removal of all resource overrides. Adaptive-cover computations are explicit kernel-checked leaves joined through reusable soundness lemmas; logical assembly is separated from numerical leaf checks to reduce serial build dependencies.

Source/name audits cover the consolidation passes, including preservation of all 26,733 public Gerver names and all 25,086 certificate names. Fifteen optional-evaluator APIs and their callers use Option names so the existing source axiom checker identifies them correctly. No checker changed. Unused hypotheses were removed only where stronger statements were proved; the registered theorem statements and useful generality are preserved.

Review repairs replace the incorrect auxiliary Engelking locator and Hahn label with the verified Mathlib coinducing/local-connectedness theorem. Shared phase derivatives, frame/square calculus, rotation projections, injectivity, scalar projections, exposed-edge and bounded-variation lemmas replace duplicated proofs. That repair preserved all 943 existing public signatures in four files and exposed 14 reusable helpers. A subsequent cleanup removed 51 unused have blocks across eight proofs and unnecessary cap/tail-geometry calls. Two private density helpers now require only the cap and its identification; all 261 public signatures in those two files are unchanged. The repairs remove 376 physical lines in total and leave all 32 certificate bundles byte-identical.

Merged tooling PR #549 supplies the pinned public reproduction recipe. It transforms a checksum-pinned public upstream archive and 814 individually pinned inputs into all 47 intermediate files and 32 final bundles byte for byte, without embedding the final corpus. An independent Lean search recomputes all 10,801 leaves across 550 roots. The tooling passes all 512 Python tests and Ruff checks, including nested-file/symlink rejection and a production-subtree golden fixture.

Measured compile performance

Shared 16-vCPU Azure VM; pinned Lean and Mathlib; matching commands and semantic prerequisites on both sides.

Measurement	Before	After
Controlled target build	135.49 s	66.87 s
Representative adaptive certificate	42.18 s	11.32 s
Slow depth-nine certificate	509.77 s	32.63 s
Final cleanup: application module	18.31 s	17.68 s
Final cleanup: foundation module	17.61 s	16.34 s

The target command is LEAN_NUM_THREADS=4 /usr/bin/time -v lake build LeanPool.MovingSofa, after warming the same mathematical prerequisite boundary outside the timed interval. The final layout has 50 prerequisite modules warm and four application/entry targets rebuilt; the baseline had 1,397 warm and 62 cold modules before consolidation. This is not a cold-build comparison. The baseline includes 88,016 warning messages, including replayed diagnostics; the entire wall-time gain is not attributed to proof optimization. The matched certificate probes independently isolate numerical improvements.

Target user-plus-system CPU time fell from 424.62 to 289.13 seconds; maximum process RSS fell from 3,353,092 to 2,890,628 KiB. The slow-certificate maximum process RSS fell from 10,833,700 to 2,878,792 KiB. The final controlled run had zero warnings and unchanged source hashes.

Direct-module probes used the same lake env lean invocation with LEAN_NUM_THREADS=2. These environment values are recorded settings, not fixed per-compiler thread counts: compiler invocations used default concurrency without -j. Both sides used matching commands. This corrects earlier imprecise thread-count wording; see the pinned shell initialization and default thread option.

Validation and review

Current head: 125ea36014aabbd9679abd928cfda58969125d05.

• Complete 3,950-job project build passes warning-free.
• Generated index, project style and whole-repository static quality pass.
• Repository declaration linters pass for 54 modules / 102,001 compiled declarations.
• Registered endpoints, complete source-declaration axiom closure and compiled safety/option audits pass with zero errors. No new axiom beyond the three permitted classical axioms, sorry/admit, prohibited mechanism or resource override is introduced.
• No workflow, review rule, quality script, linter configuration, branch protection or waiver changed. The PR is content-only; reproduction tooling landed separately in Add reproducible moving-sofa certificate generation recipe #549.

Configured GPT review approves all five rubrics at this head, published 2026-09-28 23:24:26 UTC. Greptile found no new blocking issue, with explicitly incremental coverage. The separate thorough review covers all 101 nongenerated source packets, generated families and soundness interfaces, endpoint chains, repair diffs, conservation audits, reproduction and measurements. It approves the source, and no unresolved review thread remains.

Current hosted CI passed at the reviewed head. All 54 MovingSofa modules compiled without Lean warnings; generated indexes, the full pool and challenge/solution builds, linters, style and quality/trust gates passed. The hosted pool build took 97m23s; this is an observed hosted duration, separate from the controlled local comparison. Documentation preflight and content separation also pass. The final protected Build project check completed successfully at 2026-09-29 00:53:17 UTC; no unresolved review finding remains.

[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 mathematical proofs for the moving sofa problem.

No new blocking issue was identified in the changes since the previous review, but this review does not establish that the full import is safe to merge.

Summary

The PR imports a formalization of Gerver sofa optimality and its supporting geometry and interval certificates. Since the previous review, the changes remove unused proof facts in two modules; no new issue was established in those changes. The approximately 470,000-line full-PR diff could not be independently checked in full here, so source fidelity and the complete contribution are not reverified at the current head.

_{Reviews (5) · Last reviewed commit: "Remove unused MovingSofa proof scaffoldi..."}

[Vilin97]

{
"verdict": "discuss",
"bottom_line": "Gerver optimality is a research-level result, but the certificate corpus imposes a maintenance cost that a maintainer should explicitly accept or reduce.",
"fit": "borderline",
"level": "research",
"branch": "convex geometry",
"mode": "theory_building",
"significance_one_sentence": "The import formalizes Gerver's moving-sofa optimality and develops geometric and certified-numerical machinery for its proof.",
"findings": [
{
"file": "",
"line": 0,
"rule": "generated-bulk",
"comment": "The 47 PartE certificate modules contain about 334,787 of the import's 481,500 Lean lines (69.5%) and 25,086 named declarations. The PR pins the upstream source and release, but gives no regeneration procedure for this consolidated corpus. Please provide a reproducible recipe if one exists; otherwise a maintainer should decide explicitly whether the ongoing Mathlib-port and certificate maintenance cost is acceptable for this landmark result.",
"evidence": "LeanPool/MovingSofa/GerverSofa/KernelOnly/PartE/Certificates/Batch*.lean; 47 modules and 25,086 declaration names counted from the exact 0f01821 project tree; no regeneration tool or recipe is included in the PR."
}
]
}

[Vilin97]

{
  "conclusion": "approve",
  "coverage": {
    "upstream": "deancureton/MovingSofa@4d5569131940815f47a9ccf3e90a4c5043c56127",
    "scope": "All 101 bounded nongenerated review packets, generated certificate families and soundness helpers, endpoint dependency chain, consolidation name audits, and subsequent repair diffs. No approval based on an elided GitHub diff. The final 106-to-13 geometry/arithmetic consolidation preserved all 3050 public names and all source bodies modulo imports and whitespace; the certificate join audit covered all 119 moved fragments. The full compiled lint and trust audits now pass on the current source. Fifteen later API identifier renames were reviewed separately and propagated through the complete rebuilt dependency chain. The subsequent current-main integration audit covers all 40 combined Gerver modules exactly, all 25,350 angle-cell aliases with identical qualified names and expressions, and all 13 remaining modules with import-only changes. All 26,733 public Gerver declaration names survive. The public recipe reproduces every one of 47 intermediate files and 32 final certificate bundles; a separate Lean search recomputes all 10,801 leaves across 550 roots. Companion PR #549 is merged, resolving the public-recipe finding. The final citation and duplication repair was reviewed across all four changed files: all 943 existing public signatures remain identical, 14 helpers are newly public, and the 32 certificate bundle digests remain unchanged. Public compatibility names delegate to shared proofs. The complete final dependency chain and compiled trust audits pass. The latest dead-scaffolding repair covers both edited files and all eight changed proofs: 51 unused have blocks and unnecessary cap/tail-geometry calls removed; all 261 public signatures and all 32 certificate digests preserved. Two private outer-density helper statements are strengthened by removing unused tail parameters; callers use the stronger form.",
    "imported_modules": 54
  },
  "faithfulness": {
    "verdict": "pass",
    "bottom_line": "The registered endpoints state Gerver optimality for the ordinary continuous-motion sofa problem and prove the required upper bound.",
    "proves_the_claim": "proves_it",
    "claim_note": "The area supremum equals the volume of the explicitly defined Gerver sofa; the card also accurately states parameter uniqueness and admissibility, without claiming a certified decimal area or uniqueness of the maximizing shape.",
    "assumed_inputs": "",
    "findings": []
  },
  "novelty": {
    "verdict": "pass",
    "bottom_line": "No existing Mathlib or Lean Pool headline theorem was found.",
    "already_formalized": "",
    "novelty_note": "The import supplies Gerver optimality and its geometry/certificate infrastructure; three existing Isoperimetric modules are reused instead of copied.",
    "findings": []
  },
  "significance": {
    "verdict": "pass",
    "bottom_line": "A completed formal proof of this research result and its reusable geometric infrastructure is a strong fit for Lean Pool.",
    "fit": "good_fit",
    "level": "research",
    "branch": "convex geometry",
    "mode": "mixed",
    "significance_one_sentence": "The development formalizes the solution of the moving sofa problem and builds supporting convex-cap, Stieltjes-area, Jordan, and interval-certificate theory.",
    "findings": []
  },
  "sources": {
    "verdict": "pass",
    "bottom_line": "The advertised results match the cited Baek and Romik sources. The incorrect auxiliary Engelking locator and Hahn label have been removed and replaced with the verified pinned Mathlib coinducing/local-connectedness theorem.",
    "source_match": "matches",
    "findings": []
  },
  "quality": {
    "verdict": "pass",
    "bottom_line": "The large certificate corpus has a public pinned regeneration pipeline, exact output and source-conservation audits, kernel-checked leaves, reusable soundness boundaries, and measured reductions in compile time and memory. No material safe further proof optimization was identified after the cache, leaf, dependency and consolidation passes.",
    "code_quality": 3,
    "findings": []
  },
  "evidence": [
    {
      "file": "LeanPool/MovingSofa/Development/Geometry/Foundations/Development005.lean",
      "line": 140,
      "detail": "IsMovingSofa requires IsConnected, IsClosed, continuous rigid motion, identity at zero, and initial/final hallway conditions; it does not contain an area-bound field."
    },
    {
      "file": "LeanPool/MovingSofa/Development/Geometry/Foundations/Development005.lean",
      "line": 179,
      "detail": "AB\u03c6\u03b8Spec gives all four cited equations and the stated ordered, nonnegative parameter domain; its existsUnique theorem is supplied by the certified Part F bridge."
    },
    {
      "file": "LeanPool/MovingSofa/Development/Geometry/Applications/Development003.lean",
      "line": 5968,
      "detail": "areaUpperBound obtains paperGerverSofa_maximum, transports the canonical motion, proves compactness/finite measure, and applies real_area_le_iff_volume_le."
    },
    {
      "file": "LeanPool/MovingSofa/Development/Geometry/Applications/Development003.lean",
      "line": 6014,
      "detail": "sofaConstant_eq_volume_gerversSofa applies optimality_of_areaUpperBound to the proved areaUpperBound."
    }
  ],
  "validation": {
    "local": "Complete 54-module project rebuild passed warning-free (3950 jobs). All 102001 compiled declarations pass repository linters. Generated index, project style, whole-repository static quality, registered endpoints, source-declaration axiom audit and compiled safety pass. Final controlled rebuild is warning-free with unchanged source hashes; the worktree is clean.",
    "ci": "Current head 125ea36014aabbd9679abd928cfda58969125d05 passed hosted Lean Action CI https://github.com/Vilin97/lean-pool/actions/runs/36494671098. All 54 MovingSofa modules compiled; no Lean build warning occurred. Generated indexes, the complete pool and challenge/solution builds, repository linters, style, and quality/trust checks all passed. Pool build: 97m23s; lint:5m54s; style:18s; quality:15m07s. MovingSofa lint, declaration, axiom and backdoor checks ran fresh; valid existing-project receipts were reused. The final required Build project check passed at 2026-09-29T00:53:17Z.",
    "performance": {
      "head": "125ea36014aabbd9679abd928cfda58969125d05",
      "baseline_gnu_wall_seconds": 135.49,
      "optimized_gnu_wall_seconds": 66.87,
      "optimized_monitored_wall_seconds": 67.04787402797956,
      "wall_reduction_fraction": 0.5064580411838512,
      "warm_modules": 50,
      "cold_modules": 4,
      "warnings": 0,
      "source_unchanged": true,
      "conditions": "Identical LEAN_NUM_THREADS=4 environment and Lake command; compiler default concurrency (no -j flag); recorded semantic prerequisite boundary warm; pinned Lean and Mathlib; shared Azure VM. Baseline includes warning replay. Not a cold-build comparison.",
      "baseline_user_seconds": 383.44,
      "baseline_system_seconds": 41.18,
      "optimized_user_seconds": 283.46,
      "optimized_system_seconds": 5.67,
      "baseline_total_cpu_seconds": 424.62,
      "optimized_total_cpu_seconds": 289.13,
      "baseline_maximum_process_rss_kib": 3353092,
      "optimized_maximum_process_rss_kib": 2890628,
      "optimized_peak_process_group_rss_kib": 3827972,
      "pre_integration_gnu_wall_seconds": 68.04
    },
    "matched_certificate_wall_seconds": [
      [
        42.18,
        11.32
      ],
      [
        509.774826573,
        32.63392183
      ]
    ],
    "matched_review_repair_modules_gnu_wall_seconds": {
      "Part C calculus": [
        42.95,
        40.71
      ],
      "Geometry foundations": [
        20.77,
        20.52
      ]
    },
    "matched_layout_probe": {
      "before_wall_seconds": 200.9,
      "after_wall_seconds": 202.74,
      "before_maximum_process_rss_kib": 2618140,
      "after_maximum_process_rss_kib": 2586824,
      "conditions": "Same lake env lean command with LEAN_NUM_THREADS=2 and default compiler concurrency; identical current semantic prerequisites; preserved Batch020 with imports relocated vs current Bundle014. Both passed, no diagnostics, unchanged source hashes. Single sample; no material regression established."
    },
    "matched_dead_scaffolding_modules_gnu_wall_seconds": {
      "Applications.Development003": [
        18.31,
        17.68
      ],
      "Foundations.Development003": [
        17.61,
        16.34
      ]
    },
    "matched_module_command_conditions": "Matched direct-module probes use LEAN_NUM_THREADS=2 lake env lean SOURCE with default compiler concurrency, no -j flag. Earlier descriptions as fixed two-thread compiler runs were imprecise; numerical results and matching commands are unchanged.",
    "ci_audit": {
      "job": 109171619501,
      "conclusion": "success",
      "required_steps": {
        "Check library indexes use the module system and are up to date": "success",
        "Build project": "success",
        "Build challenges and solutions": "success",
        "Lint": "success",
        "Text style lint": "success",
        "Repository quality checks": "success"
      },
      "pool_build_wall_seconds": 5843.0,
      "build_log_lines": 981,
      "build_warning_count": 0,
      "moving_sofa_build_lines": 54,
      "step_seconds": {
        "Check library indexes use the module system and are up to date": 9.0,
        "Build project": 5843.0,
        "Build challenges and solutions": 5.0,
        "Lint": 354.0,
        "Text style lint": 18.0,
        "Repository quality checks": 907.0
      },
      "log_path": "/data/codex/scratch/lean4lean4/acquisition-20260928-older/ci-125ea-green.log"
    }
  },
  "reviewed_commit": "125ea36014aabbd9679abd928cfda58969125d05",
  "review_kind": "Separate thorough agentic review across all five repository rubrics, in addition to Greptile and the configured GPT worker",
  "repairs_reviewed": [
    "Explicit current module visibility and import closure; three existing Isoperimetric modules reused.",
    "All resource overrides removed; exact interval caches shared and adaptive computations decomposed into kernel-checked leaves.",
    "Every consolidation public-name audit checked; all 119 moved combination fragments retained their bodies.",
    "Unused hypotheses removed only with stronger proofs and updated callers; no headline theorem weakened.",
    "Warnings and all lint findings repaired; four missing docs added; 15 question-mark evaluator API names replaced consistently with Option names.",
    "All upstream dependency copyright attribution and the complete MIT notice retained.",
    "Current-main root size repair: 54 modules and 9,994 code lines, with all 26,733 Gerver declaration names preserved and 25,350 identical cell aliases.",
    "Public certificate recipe merged separately in PR #549; all 47 intermediate and 32 final digests verified. Independent search matched all 10,801 leaves. Greptile nested-file verification and stage-regression findings repaired; 512 Python tests and Ruff passed.",
    "Corrected the source-mismatch finding: the auxiliary local-connectedness reference now names the exact verified Mathlib theorem, replacing the incorrect Engelking theorem number and Hahn label.",
    "Resolved the duplicate-proof finding: shared all five phase derivatives, frame/square calculus, rotation projections and injectivity, scalar projection derivatives, exposed-edge and bounded-variation lemmas. The four-file repair removes 271 physical lines, preserves all 943 existing public signatures and adds 14 shared public helpers.",
    "Resolved current25d dead-proof-scaffolding finding:51 unused have blocks removed across8proofs, two private density helpers strengthened,261 public signatures unchanged,32 certificate digests unchanged.105physical lines removed; complete local validation and matched timing passed."
  ],
  "merge_condition": "Satisfied at 2026-09-29T00:54:20Z: all protected checks green, merge state CLEAN, reviewed head and current main unchanged, source hashes match, worktree clean, GPT approves all five rubrics, Greptile has no blocking finding, and no new comment or unresolved review thread remains. Normal protected squash merge is approved; no policy override is needed.",
  "configured_review": {
    "head": "125ea36014aabbd9679abd928cfda58969125d05",
    "conclusion": "approve",
    "rubrics": "All five pass",
    "published_at": "2026-09-28T23:24:26Z",
    "url": "https://github.com/Vilin97/lean-pool/pull/548#issuecomment-5879347064"
  },
  "greptile_review": {
    "head": "125ea36014aabbd9679abd928cfda58969125d05",
    "conclusion": "No new blocking issue",
    "coverage": "Latest review is explicitly incremental; does not independently reverify the entire import. Complete source coverage is supplied by this review and the configured rubric reviews.",
    "url": "https://github.com/Vilin97/lean-pool/pull/548#issuecomment-5876088645"
  },
  "review_updated_at": "2026-09-29T00:55:18.952276+00:00"
}

[Vilin97]

Follow-up at 0f018213: the separate five-rubric review's source, faithfulness, and local compile evidence strengthens the case for this import. My generated-bulk significance finding remains open. The pinned MovingSofa source documents how to build the frozen Lean files. The linked GerverSofaLean REPRODUCE.ps1 also runs a build/check of the supplied source. In the published source and checksum-matched v1.1.0 release, I found no documented procedure that regenerates the 47 consolidated Batch certificate modules byte for byte. This does not rule out a private generator.

Please provide that procedure if available. Otherwise the maintainer needs to decide whether to accept ongoing maintenance of the 334,787-line certificate corpus. This scope decision is separate from the still-pending protected CI; it is the sole reason for needs-maintainer here.

[Vilin97]

The regeneration procedure is now public in companion tooling PR #549: recipe and commands. A clean replay from the checksum-pinned deancureton/MovingSofa@4d556913 archive regenerates all 47 certificate modules at 0f018213 / a3831dac byte for byte and preserves all 25,086 declaration names. The independent Lean search recomputes all 10,801 leaves across 550 cover roots and matches the recorded witnesses exactly. Python validation: 510 tests, Ruff and formatting passed.

The recipe includes the actual factoring, cell sharing, checked-cover expansion, module assembly and root repairs. Its inputs and scope are explicit: public upstream Lean source plus reproducible subdivision witnesses and layout data. It does not claim to recover a private upstream generator or regenerate all mathematics from the paper. No final certificate corpus is embedded as a payload.

A separate integration repair is now necessary: the automatic main refresh brought in #489 and the combined root index is 10,024 code lines. I am consolidating additional imported modules to meet the existing 10,000-line limit, preserving declarations and rechecking compile cost. The companion recipe will track any resulting certificate layout change. This finding is being repaired directly; no waiver or gate change is proposed.

[Vilin97]

The generated-certificate reproducibility question now has concrete evidence. Companion #549 at f5099aa3e12580e0d3db943ffd74a7d649186cf3 was independently replayed from its SHA-256-pinned public upstream archive in a clean workspace. It regenerated all 47 Part E certificate modules byte-for-byte against this PR's current a3831dac411d778487a8f631e26bfd7f9ddfffaf head: 334,787 lines, 25,086 identical declaration names, 27 seconds and 97 MiB peak RSS. The separate Lean search that recomputes the recorded rational witnesses was inspected but not rerun; the exact certificate files passed the earlier hosted Lean build and kernel checks.

The specific missing-public-recipe finding is resolved, provided #549 is reviewed and merged before this import and the certificate bytes remain aligned. The current head's new Build project failure is separate: Check rebased root reports LeanPool.lean at 10,024 code lines against the unchanged 10,000-line limit after #489 entered main. A source-preserving reduction of at least 24 project module imports, fresh exact-head CI, current-main integration, and final review remain. These are concrete repair and integration tasks, not an unresolved maintainer policy decision, so I am removing needs-maintainer. This PR remains unmerged while those conditions are pending.

[Vilin97]

Changes requested by automated review at a3831dac411d778487a8f631e26bfd7f9ddfffaf.

The missing certificate recipe is substantively resolved by the independently replayed companion #549, but this PR's exact-head protected Build project check is red. Check rebased root reports LeanPool.lean at 10,024 code lines against the unchanged 10,000-line limit after #489 joined main. The failure is in the generated index; no Lean compiler error was established by this run.

Keeping all 47 certificate modules byte-identical to #549's verified output leaves 36 other MovingSofa modules containing 115,921 noncomment code lines. Removing the required 24 generated imports means consolidating those 36 modules to at most 12 files, which is also the minimum permitted by the existing 10,000-line per-file limit. A consolidation without splitting must combine the 24 smaller source bodies with larger modules, leaving only 4,079 lines of aggregate capacity. Two small Part E semantic module paths are imported by the fixed certificate files and must survive. Consequently, that route removes 22 small-module paths and two large-module paths, moving at least 19,193 small-source code lines plus two large proof bodies and rewiring their imports. This is a broad source-sensitive refactor, beyond a safe local patch to the index.

Please consolidate the project modules without dropping or weakening declarations, preserve every certificate file/path and its SHA-256 (or update and replay #549 if a certificate must change), regenerate the index, and pass the unchanged size gate, project build, linters, repository quality and all three protected checks at a current-main head. #549 must be reviewed and integrated before this import. needs-maintainer was removed because these are concrete repair and integration tasks, not a pending human policy decision.

[Vilin97]

The requested integration repair is now at 9ac84ed0910d4615a0238a6d465b471d7cee53a0: 54 imported modules, and the combined generated index is 9,994 code lines. All 26,733 named Gerver declarations survive. The source conservation audit covers all 40 combined modules exactly, all 25,350 angle-cell aliases with identical qualified names and expressions, and the other 13 source modules with import changes only.

Companion #549 now reproduces the updated corpus at 5e0169461cda8d4dc78f2c03a957c0b217f9b5db: it checks all 47 intermediate files against the original digests, then regenerates all 32 final certificate bundles byte for byte. The independent Lean evaluator search was rerun and matches all 10,801 leaves across 550 roots. Updated pinned recipe. All 510 Python tests, Ruff, and the companion Python CI pass.

Current index, style and whole-repository static quality checks pass. The full local build and hosted CI are running; compiled linters/trust audits and the comparable post-consolidation timing follow. The fresh pre-consolidation controlled build measured 68.04 seconds without warnings. #549 has been marked ready and its configured review requested; it will be integrated before this import.

[Vilin97]

Substantive review of 9ac84ed0910d4615a0238a6d465b471d7cee53a0: the prior faithfulness audit found that the headline Lean theorem and card state Gerver's moving-sofa optimum with the intended admissibility and uniqueness conditions. This head preserves the card, umbrella and headline theorem byte-for-byte. The certificate repacking preserves all 29,783 declaration names/kinds and normalized signatures, including 25,086 certificate declarations; the non-structural Lean code-line multisets are unchanged. The generated root is now 9,994 code lines, below the unchanged limit. The earlier root-size request is addressed. The former maintenance concern about an unreproducible certificate corpus is addressed by companion #549's pinned recipe: an independent bounded replay reproduced all 32 current certificate files byte-for-byte. No unresolved review thread or new advisory finding remains. I found no remaining substantive source or mathematical blocker at this head.

Disposition: approved, integration/checks pending. #549 must merge first so the reproduction recipe lands with the content. This PR's protected separation and documentation preflight checks pass; its exact-head Build project, compiled lint/trust/quality checks, and any final performance/advisory finding are still pending in Lean Action CI run 36482038340. Re-read the head, current main, checks and review threads before ordinary protected squash merge. No needs-maintainer decision remains.

[Vilin97]

/review

[Vilin97]

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: 125ea36014aabbd9679abd928cfda58969125d05

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All three card claims are proved for the stated objects and domains, without undisclosed mathematical assumptions.
Novelty	✅ pass	Direct searches of pinned Mathlib and existing pool sources found no duplicate of any of the three registered results.
Significance	✅ pass	The research contribution merits inclusion: generated Part E certificates account for 323,037 of 469,541 added project lines (68.8%), and repository tooling successfully reproduced all 32 bundles byte for byte from pinned public inputs, with the certificates depending on vendored rational interval arithmetic and project-local cover lemmas.
Sources	✅ pass	The claims match Baek’s optimality result and Romik’s parameter equations and explicit formulas, and the imported formalizations are explicitly credited.
Code quality (advisory)	✅ pass	The current head meets the pool’s maintainability bar: the targeted cleanup is present, shared helpers support the proofs, and all certificate bundles match the reproduction manifest.

Aspect	Value
Proves the claim	✅ proves_it
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	convex geometry and geometric optimization
Mode	mixed
Code quality	3 / 5

Statement check: The Lean establishes the supremum equality for closed, connected sets admitting continuous rigid hallway motions, proves Gerver’s admissibility, and proves parameter uniqueness throughout A, B ≥ 0 and 0 ≤ φ ≤ θ ≤ π/4, with the explicit construction matching Romik’s equations and formulas.

Formalizing Gerver’s global optimality, the central result of Baek’s moving-sofa solution, together with substantial supporting theory of convex bodies, Stieltjes area, polygon approximation and concave quadratic bounds, clearly meets the research-level significance bar.

---

Tokens: 5,488,656 in / 40,183 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $112.7868 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/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]

The source-reference and duplicate-proof findings are repaired at 25d7d04b7fb23bf259dc9568aac59c01faec6483 (repair commit ff1dacf4c, with merged tooling #549 integrated). The local-connectedness reference now identifies Mathlib's exact Topology.IsCoinducing.locallyConnectedSpace theorem; I checked the pinned source and public documentation. The incorrect Engelking locator and Hahn label are removed.

The five phase derivatives now have one shared Stage 2 implementation, with the existing Stage 4 public names retained as wrappers. Shared frame derivatives, square differentiation, rotated-coordinate projections, rotation injectivity, scalar-projection derivatives and the repeated exposed-edge/bounded-variation results replace their copied proofs. The audit covers all 943 pre-existing public signatures in the four edited files: none changed or disappeared; 14 shared helpers are newly public. All 32 numerical certificate bundles remain byte-identical to merged recipe #549.

The complete project rebuild is warning-free. Index, style, whole-repository static quality, all declaration linters (54 modules and 102,001 compiled declarations), registered endpoints, axiom closure and compiled safety checks pass. No theorem was weakened, and no gate or resource option changed. Matched two-worker module builds changed from 42.95 to 40.71 seconds for the calculus bundle and from 20.77 to 20.52 seconds for the geometry module. The full controlled four-worker target build is 68.02 seconds versus the original 135.49-second baseline, with 50 prerequisite modules warm, four application/entry modules rebuilt, zero warnings and unchanged source hashes. This is a controlled warm-boundary comparison, not a cold build. The refactor removes 271 physical lines overall. New hosted CI and reviews are required on the published head before merge.

[Vilin97]

/review

[Vilin97]

/review

The dead-proof-scaffolding finding is repaired in 125ea3601. The two outer-density helpers now take only K and hK; their unnecessary tail-geometry calls and B, D, hB, hD obligations are gone. The support-line proof no longer computes unused cap/tail membership facts. The phase-measure halves retain only the relevant interval, inclusion and sign setup. The Jordan proof drops unused component, ray, coordinate and closed-image facts. A broader inspection of the same two files removed two further unused calculations while retaining facts used implicitly by arithmetic automation and typeclass inference.

The diff removes 51 unused have blocks across eight proofs, with a net reduction of 105 physical lines. All 261 public signatures in the two edited files are identical; only the two private density helpers have stronger signatures. All 32 certificate bundles remain byte-identical to the merged recipe.

Validation passed: the complete 3,950-job project build without warnings, generated index, project style, whole-repository static quality, declaration linters for 54 modules / 102,001 declarations, registered endpoints, complete source axiom closure, and compiled safety audit. Matched direct module compilation changed from 18.31 to 17.68 seconds for the application module and from 17.61 to 16.34 seconds for the foundation module. The final controlled project rebuild is 66.87 seconds versus the original 135.49-second baseline, with the same mathematical prerequisite boundary (50 warm modules and four rebuilt targets), zero warnings and unchanged source hashes. This is not a cold-build comparison.

Performance-report clarification: the recorded commands set LEAN_NUM_THREADS=4 for the project build and LEAN_NUM_THREADS=2 for the direct-module probes; Lean compiler invocations used default concurrency, without a -j flag. Earlier wording describing those settings as fixed compiler thread counts was imprecise. Both sides of each comparison use matching commands and prerequisites. See the pinned shell initialization and default thread option.

Fresh hosted checks are required for this repair. No policy, gate, waiver, trust assumption or public theorem statement changed.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.