Actual carrier and cyclic crossing geometry

Abstract

Actual polygon ear slide geometry

Definition 1.1 (Segments).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),(\mathrm{IsSegment}\left(e\right)⟺\neg (\mathrm{IsDiag}\left(e\right)))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.IsSegment (✓ std3).

Source. Repository-derived.

Commentary.

A segment has distinct endpoints in the symmetric square.

Definition 1.2 (Boundary sides).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),(\mathrm{IsSide}\left(e\right)⟺(\exists i\in \mathrm{ZMod}\left(n\right),(e=\mathrm{symPair}\left(i,(i+1)\right))))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.IsSide (✓ std3).

Source. Repository-derived.

Commentary.

An unordered boundary side joins successive cyclic vertices. symPair denotes the unordered pair s(a,b).

Definition 1.3 (Internal diagonals).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),(\mathrm{IsDiagonal}\left(e\right)⟺(\mathrm{IsSegment}\left(e\right)\wedge \neg (\mathrm{IsSide}\left(e\right))))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.IsDiagonal (✓ std3).

Source. Repository-derived.

Commentary.

Internal diagonals are segments that are not boundary sides.

Definition 1.4 (Actual cyclic crossing).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),\forall f\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),(\mathrm{Cross}\left(e,f\right)⟺(\exists a\in \mathrm{ZMod}\left(n\right),\exists b\in \mathrm{ZMod}\left(n\right),\exists c\in \mathrm{ZMod}\left(n\right),\exists d\in \mathrm{ZMod}\left(n\right),((e=\mathrm{symPair}\left(a,b\right))\wedge ((f=\mathrm{symPair}\left(c,d\right))\wedge (\mathrm{sbtw}\left(a,c,b\right)\wedge \mathrm{sbtw}\left(b,d,a\right))))))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.Cross (✓ std3).

Source. Repository-derived.

Commentary.

Crossing uses strict cyclic betweenness witnesses.

Definition 1.5 (Maximal noncrossing finite diagonal carrier).

$$\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{IsTriangulation}\left(T\right)⟺((\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),((e\in T)⟹\mathrm{IsDiagonal}\left(e\right)))\wedge ((\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),\forall f\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),((e\in T)⟹((f\in T)⟹\neg (\mathrm{Cross}\left(e,f\right)))))\wedge (\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),(\mathrm{IsDiagonal}\left(e\right)⟹(\neg ((e\in T))⟹(\exists f\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),((f\in T)\wedge \mathrm{Cross}\left(e,f\right)))))))))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.IsTriangulation (✓ std3).

Source. Repository-derived.

Commentary.

The carrier contains every maximal noncrossing finite set of internal diagonals; no completion is selected.

Definition 1.6 (Ear diagonal at a cyclic centre).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall i\in \mathrm{ZMod}\left(n\right),(\mathrm{ear}\left(i\right)=\mathrm{symPair}\left((i-1),(i+1)\right))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.ear (✓ std3).

Source. Repository-derived.

Commentary.

The local names sEar, tEar, uEar denote ear(1), ear(2), ear(3).

Definition 1.7 (Exchange the two local vertices).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall i\in \mathrm{ZMod}\left(n\right),(\mathrm{vertexSwap}\left(n,i\right)=\mathrm{swap}\left(1,2,i\right))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.vertexSwap (✓ std3).

Source. Repository-derived.

Commentary.

The vertex permutation exchanges 1 and 2 and fixes every other vertex.

Definition 1.8 (Induced unordered-chord exchange).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),(\mathrm{chordSwap}\left(e\right)=\mathrm{map}\left(\mathrm{vertexSwap}\left(n\right),e\right))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.chordSwap (✓ std3).

Source. Repository-derived.

Commentary.

Symmetric-square map transports each unordered pair.

Definition 1.9 (Avoid the deleted centre).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),(\mathrm{AvoidTwo}\left(e\right)⟺(\forall x\in \mathrm{ZMod}\left(n\right),\neg ((e=\mathrm{symPair}\left(2,x\right)))))$$

Formalization. D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.AvoidTwo (✓ std3).

Source. Repository-derived.

Commentary.

Every endpoint avoids vertex 2.

Theorem 1.10 (Crossing transport away from centre 2).

$$\forall n\in Nat,[\mathrm{NeZero}\left(n\right)],\forall e\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),\forall f\in Sym2\left(\mathrm{ZMod}\left(n\right)\right),((6\le n)⟹(\mathrm{AvoidTwo}\left(e\right)⟹(\mathrm{AvoidTwo}\left(f\right)⟹(\mathrm{Cross}\left(\mathrm{chordSwap}\left(e\right),\mathrm{chordSwap}\left(f\right)\right)⟺\mathrm{Cross}\left(e,f\right)))))$$

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

Source. Repository-derived.

Commentary.

Crossing is transported in both directions, including across the cyclic seam.

References

• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.AvoidTwo
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.Cross
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.IsDiagonal
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.IsSegment
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.IsSide
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.IsTriangulation
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.chordSwap
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.cross_chordSwap_of_avoidTwo
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.ear
• Truth anchor: D5/S3/Geometry/Polygons/PolygonEarSlideGeometry.vertexSwap