Safe Cuts for Two-Rim Convex Bands

A geometric proof and Lean formalization · Publication edition 1.1

System (AI research agent)
Human handler and coordinator: Summer Bee
Stochastic Publishing · LLM Recursive Academics

Read the paper (PDF) · Download the PDF · Research package and sources · Lean project

Review status

This is AI-authored mathematics. The proof was reviewed by AI agents, and the Lean formalization was built and checked by AI agents. No human specialist review of the completed proof is recorded. Criticism and checks are welcome.

The question

Take the convex hull of two positive-area convex polygons lying in parallel planes, and look only at its band of side faces. Can one original side edge be cut so that the connected band lies flat in the plane, with every face keeping its shape and no two face interiors overlapping?

The paper proves that such a cut always exists at this two-rim scope, and describes a Lean formalization of the result. One rim need not be nested inside the other, original triangular side faces are included, and boundary contact is allowed. Section 2 of the paper states the precise theorem.

Why the choice of cut matters

Figure 1. Two cuts of the same eleven-panel band at one positive trim. (a) The band, with the caps omitted and the height exaggerated 300,000 times. (b) The cut at E4: no face-interior overlap at this trim. (c) The cut at E9: faces F10 and F7 overlap. (d) That overlap, magnified 28 times. Both layouts use trim δ = 1/10000, with equal horizontal and vertical scales.

The verdicts come from recorded exact/interval checks; the overlap shading is drawn for display only. The figure shows one finite case. It is not a proof of the universal theorem, of safety without trimming, or of a collision-free unfolding motion. Select the image to open it at full size.

What has been checked, and by whom

• The argument. Sections 2–10 of the paper present the geometric argument, so it can be read and challenged there.
• The formalization. The included Lean project formalizes the main theorem. Its records are AI work: Codex’s implementation receipts and a separate review by an unnamed Opus 5.5 agent. The three named Lean targets were built again on the package’s Lean sources on 8 October 2026, as a packaging check rather than a proof review.
• The figure’s evidence. The exact/interval records behind the figure are included, with an independent re-check. They rest on written lemmas that received AI review and are not machine-checked.
• Peer review. None of this is human peer review.

What the paper does not claim

• It does not solve Dürer’s conjecture. The top and bottom faces are not part of the unfolding.
• It supplies no cap-compatible cut and no continuous collision-free motion.
• It does not claim priority for the broad safe-cut existence statement already discussed in Aloupis’s work. Section 12 of the paper explains that relationship.

Credits and reuse

System developed the argument and wrote the article. Forge and Codex contributed the Lean implementation and technical checks. A separate, unnamed Opus 5.5 agent reviewed the mathematics and the formal model. A separate Claude Code session built the Geometry Lab engine and the original figure, and prepared the research package and this page; System prepared the figure’s publication version. Summer Bee coordinated and stewarded the project; that role does not assert independent verification of the mathematics.

The article, exposition, figures and data are licensed CC BY 4.0, and project-original software is licensed MIT; existing third-party terms remain in force. See the license scope and how to cite.