Mutually inverse maps on actual triangulations

Abstract

Complete polygon ear slide maps

Theorem 1.1 (Ear-centre exclusion).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),((6\le n)⟹(\mathrm{IsTriangulation}\left(T\right)⟹((\mathrm{ear}\left(2\right)\in T)⟹((e\in T)⟹\mathrm{AvoidTwo}\left(e\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonEarSlideMaps.avoidTwo_of_mem_triangulation (✓ std3). ∎

Source. Repository-derived.

Commentary.

A triangulation containing t has no internal diagonal incident with its centre 2.

Definition 1.2 (Forward complete chord map).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),(\mathrm{phi}\left(T\right)=\mathrm{insert}\left(\mathrm{ear}\left(1\right),\mathrm{image}\left(chordSwap,\mathrm{erase}\left(T,\mathrm{ear}\left(2\right)\right)\right)\right))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideMaps.phi (✓ std3).

Source. Repository-derived.

Commentary.

Erase t, exchange vertices 1 and 2 in every retained chord, and insert s.

Definition 1.3 (Inverse complete chord map).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),(\mathrm{psi}\left(T\right)=\mathrm{insert}\left(\mathrm{ear}\left(2\right),\mathrm{image}\left(chordSwap,\mathrm{erase}\left(T,\mathrm{ear}\left(1\right)\right)\right)\right))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideMaps.psi (✓ std3).

Source. Repository-derived.

Commentary.

Erase s, apply the same vertex exchange, and insert t.

Theorem 1.4 (Forward actual triangulation preservation).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),((6\le n)⟹(\mathrm{IsTriangulation}\left(T\right)⟹((\mathrm{ear}\left(2\right)\in T)⟹\mathrm{IsTriangulation}\left(\mathrm{phi}\left(T\right)\right))))$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonEarSlideMaps.phi_isTriangulation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Diagonal and crossing preservation use ear-centre exclusion; maximality handles the fresh s separately.

Theorem 1.5 (Inverse actual triangulation preservation).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),((6\le n)⟹(\mathrm{IsTriangulation}\left(T\right)⟹((\mathrm{ear}\left(1\right)\in T)⟹\mathrm{IsTriangulation}\left(\mathrm{psi}\left(T\right)\right))))$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonEarSlideMaps.psi_isTriangulation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The inverse preserves the full maximal diagonal carrier.

Theorem 1.6 (Left inverse on complete chord sets).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),((6\le n)⟹((\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),((e\in T)⟹\mathrm{IsDiagonal}\left(e\right)))⟹((\mathrm{ear}\left(2\right)\in T)⟹(\neg ((\mathrm{ear}\left(1\right)\in T))⟹(\mathrm{psi}\left(\mathrm{phi}\left(T\right)\right)=T)))))$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonEarSlideMaps.psi_phi (✓ std3). ∎

Source. Repository-derived.

Commentary.

The inverse law requires only diagonal membership and the stated included and excluded ears.

Theorem 1.7 (Right inverse on complete chord sets).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall T\in \mathrm{Finset}\left(Sym2\left(\mathrm{ZMod}\left(n\right)\right)\right),((6\le n)⟹((\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),((e\in T)⟹\mathrm{IsDiagonal}\left(e\right)))⟹((\mathrm{ear}\left(1\right)\in T)⟹(\neg ((\mathrm{ear}\left(2\right)\in T))⟹(\mathrm{phi}\left(\mathrm{psi}\left(T\right)\right)=T)))))$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Polygons/PolygonEarSlideMaps.phi_psi (✓ std3). ∎

Source. Repository-derived.

Commentary.

This equality holds for the entire finite chord set.

References

• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideMaps.avoidTwo_of_mem_triangulation
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideMaps.phi
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideMaps.phi_isTriangulation
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideMaps.phi_psi
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideMaps.psi
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideMaps.psi_isTriangulation
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideMaps.psi_phi
• Dependency: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry