feat(Geometry/Polygon): simple polygons and boundary map by A-M-Berns · Pull Request #35069 · leanprover-community/mathlib4

A-M-Berns · 2026-02-10T07:19:24Z

This PR introduces Simple polygons with the predicate IsSimple, which captures the idea of a non-self-intersecting boundary, in the file Simple.lean. In the file Boundary.lean, a boundary map from AddCircle n is defined. I prove that the range of this map is the boundary and that this map is injective if and only if the polygon is simple. I kept Boundary.lean and Simple.lean separate because future results will include stuff just about the boundary map independent of simplicity (e.g. that it is continuous in the appropriate setting) and stuff just about simple polygons independent of the boundary map (e.g. that for n = 3, IsSimple iff HasNondegenerateVertices.) I used Claude Code to help generate some of the proof material, but I golfed and edited all AI contribution.

depends on: [Merged by Bors] - feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle #34598

github-actions · 2026-02-10T07:20:37Z

PR summary aac298aee3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Geometry.Polygon.Simple` (new file)	1398
`Mathlib.Geometry.Polygon.Boundary` (new file)	1601

Declarations diff

+ IsSimple
+ boundaryMap
+ continuous_boundaryMap
+ finRotate_apply
+ isSimple_iff_boundaryMap_injective
+ range_boundaryMap

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

wwylele · 2026-02-10T13:36:29Z

Mathlib/Geometry/Polygon/Simple.lean

+variable (R) in
+/-- A polygon is simple if edges are nondegenerate, non-adjacent edges are disjoint,
+and adjacent edges meet only at their shared vertex. -/
+def IsSimple (poly : Polygon P n) : Prop :=


Maybe consider turning this into a structure so you can name each condition?

wwylele · 2026-02-10T13:44:05Z

Not necessarily in this PR but should we connect this to https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Path.html#Path in some way?

A-M-Berns · 2026-02-10T19:22:50Z

Not necessarily in this PR but should we connect this to https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Path.html#Path in some way?

My next PR will prove the map is continuous, and then I think the connection to Path wouldn't be hard from there although idk how valuable it would be

vihdzp · 2026-02-10T23:48:43Z

Mathlib/Geometry/Polygon/Simple.lean

+variable (R) in
+/-- A polygon is simple if edges are nondegenerate, non-adjacent edges are disjoint,
+and adjacent edges meet only at their shared vertex. -/
+structure IsSimple (poly : Polygon P n) : Prop where


Why does this need its own file? Can we put this in the Boundary file, and move later if needed?

Like I mentioned in the PR description, I think there are results about simple polygons that don't have anything to do with the boundary that will come later. For example, the theorem that if n = 3 then the polygon is simple if and only if it HasNondegenerateVertices.

vihdzp · 2026-02-10T23:51:10Z

Mathlib/Geometry/Polygon/Boundary.lean

+variable (R) in
+/-- The boundary parametrization on `R` formed by concatenating edges using `edgePath`. -/
+noncomputable def boundaryParam (poly : Polygon P n) (t : R) : P :=
+  let i : Fin n := ⟨(Int.floor t).toNat % n, Nat.mod_lt _ (Nat.pos_of_neZero n)⟩


What about this?

Suggested change

let i : Fin n := ⟨(Int.floor t).toNat % n, Nat.mod_lt _ (Nat.pos_of_neZero n)⟩

let i : Fin n := .ofNat (.floor t)

Making this suggestion directly creates a bunch of typeclass errors

maybe my dot notation was wrong, I meant Fin.ofNat (Nat.floor t)

That gives me the same errors, first complaining about FloorSemiring R and then about NeZero \lfloor t \rfloor

Mathlib/Geometry/Polygon/Boundary.lean

Mathlib/Geometry/Polygon/Basic.lean

mathlib-merge-conflicts · 2026-02-13T15:52:24Z

This pull request has conflicts, please merge master and resolve them.

This reverts commit f1075e1.

A-M-Berns · 2026-02-17T21:13:35Z

The theorem continuous_boundaryMap ended up being simpler than I thought, so I've added it to this PR.

mathlib-dependent-issues · 2026-02-25T17:49:11Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle #34598~~
By Dependent Issues (🤖). Happy coding!

vihdzp · 2026-02-25T20:06:36Z

I suspect we must be missing some kind of API about paths. The boundary of a polygon is intuitively just "all the edge paths concatenated together", not some weird operation involving floors and moduli.

What about adding an unbundled version of Path.concat (one without the continuity assumptions), adding whatever relevant API there is to it, and redefine the boundary map of a polygon by using it?

eric-wieser · 2026-02-25T21:43:28Z

Mathlib/Geometry/Polygon/Boundary.lean

+/-- A map from `AddCircle n` to the boundary points of the polygon. -/
+noncomputable def boundaryMap (poly : Polygon P n) : AddCircle (n : R) → P :=
+  let boundaryParam : R → P := fun t =>
+    let i : Fin n := ⟨(Int.floor t).toNat % n, Nat.mod_lt _ (Nat.pos_of_neZero n)⟩


I think perhaps this is worth extracting as AddCircle.floor : AddCircle (n : R) -> Fin n?

eric-wieser · 2026-02-26T02:49:20Z

I suspect we must be missing some kind of API about paths. The boundary of a polygon is intuitively just "all the edge paths concatenated together", not some weird operation involving floors and moduli.

What about adding an unbundled version of Path.concat (one without the continuity assumptions), adding whatever relevant API there is to it, and redefine the boundary map of a polygon by using it?

I think one difference is that Path has distinct endpoints, whereas here we explicitly want wraparound behavior.

vihdzp · 2026-02-27T06:15:09Z

Path doesn't necessarily have distinct endpoints. One can always write Path x x.

What I'm arguing for here is rather some other type Curve x y (we can call it something else), for a function f : unitInterval → X with f 0 = x and f 1 = y (notably, there are no continuity hypotheses!). We can then transfer all the standard constructions on paths; in particular, we can have Curve.concat which would join a Fin-indexed family of curves at the endpoints. This is exactly what we want here. Separately, we can have a theorem which says that the Curve.concat of continuous curves is continuous, which would make it trivial to construct the Path version of the boundary map of a polygon.

joneugster · 2026-02-27T23:27:28Z

t-euclidean-geometry

A-M-Berns · 2026-03-02T04:34:43Z

@vihdzp I think your proposed design is more elegant but it's at least a full separate PR worth of missing infrastructure plus a complete refactor of this PR. My opinion is that the most important results about the boundaryMap are the ones already in the file, so the work that builds on top of this to e.g. define polygon interiors will not care greatly about the internals of boundaryMap. I would prefer for this PR to still be merged with that refactor as a planned change later, but if others agree that the current definition is too inelegant for mathlib I would be happy to take direction.

vihdzp · 2026-03-02T04:39:19Z

I would rather not add tech debt upon ourselves. Mathlib isn't just about proving things, but building good infrastructure.

A-M-Berns · 2026-03-02T04:57:22Z

Personally I don't think it's really tech debt when the refactor would be mostly about elegance and this is a functional API surface as is especially for the obvious things that will depend on this boundaryMap, but again I'd like to hear others' thoughts.

jsm28 · 2026-03-29T20:28:32Z

I agree with the previous comments that some general API for joining paths together at their endpoints would be an appropriate basis for this PR (I haven't checked whether any such API already exists).

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Feb 10, 2026

wwylele reviewed Feb 10, 2026

View reviewed changes

A-M-Berns force-pushed the simple-clean branch from c0194d1 to a91c05f Compare February 10, 2026 20:09

vihdzp reviewed Feb 10, 2026

View reviewed changes

eric-wieser reviewed Feb 13, 2026

View reviewed changes

Mathlib/Geometry/Polygon/Basic.lean Outdated Show resolved Hide resolved

mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 13, 2026

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 13, 2026

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 13, 2026

A-M-Berns force-pushed the simple-clean branch from 5aaa044 to 78046cf Compare February 13, 2026 19:20

github-actions bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 13, 2026

A-M-Berns force-pushed the simple-clean branch from 4f5e0dc to 0378ee4 Compare February 17, 2026 01:20

github-actions bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 17, 2026

A-M-Berns added 12 commits February 16, 2026 20:30

moved to clean branch

6b0256f

added previous PR changes to Basic.lean

b36626f

cleanup

9a9a8cb

polished for PR

4af42f5

changed to structure

f01abd4

changed to variable (R) in pattern

cc4130d

restructured per comments by @vihdzp

bb95980

updated docstring

db702ad

updated simple docstring

93db8fd

used finRotate per PR leanprover-community#35229

4d6547c

undid changes

8defd42

Revert "undid changes"

58a3929

This reverts commit f1075e1.

A-M-Berns added 2 commits February 16, 2026 20:33

Fixed finRotate usage and added simp lemma

52cf63e

Added continuity theorem

af9f995

A-M-Berns force-pushed the simple-clean branch from 429fb9c to af9f995 Compare February 17, 2026 01:34

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 25, 2026

Merge branch 'master' into simple-clean

3d9ce8b

eric-wieser reviewed Feb 25, 2026

View reviewed changes

github-actions bot added the t-euclidean-geometry Affine and axiomatic geometry label Feb 27, 2026

mathlib-triage bot assigned JovanGerb Mar 6, 2026

grunweg added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 16, 2026

mathlib-triage bot assigned jsm28 and unassigned JovanGerb Mar 28, 2026

	let i : Fin n := ⟨(Int.floor t).toNat % n, Nat.mod_lt _ (Nat.pos_of_neZero n)⟩
	let i : Fin n := .ofNat (.floor t)

Conversation

A-M-Berns commented Feb 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary aac298aee3

Import changes for modified files

Declarations diff

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wwylele commented Feb 10, 2026

Uh oh!

A-M-Berns commented Feb 10, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Feb 13, 2026

Uh oh!

A-M-Berns commented Feb 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-dependent-issues bot commented Feb 25, 2026

Uh oh!

vihdzp commented Feb 25, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser commented Feb 26, 2026

Uh oh!

vihdzp commented Feb 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

joneugster commented Feb 27, 2026

Uh oh!

A-M-Berns commented Mar 2, 2026

Uh oh!

vihdzp commented Mar 2, 2026

Uh oh!

A-M-Berns commented Mar 2, 2026

Uh oh!

jsm28 commented Mar 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

A-M-Berns commented Feb 10, 2026 •

edited

Loading

github-actions bot commented Feb 10, 2026 •

edited

Loading

A-M-Berns commented Feb 17, 2026 •

edited

Loading

vihdzp commented Feb 27, 2026 •

edited

Loading