Complete maximal noncrossing carrier

Abstract

Licensed exact polygon Catalan supplier

The count-only transplant is from AxiomMath/ClusterAlgebras revision a9174706bce3bcb0fa342b4614f98ef2acb7f91c. Complete license, authors, source spans and hashes, metadata adaptations and receiver-pinned retirement condition are in docs/reports/licenses/cluster-algebras-polygon-third-party.md. This supplies reused enumeration to PolygonConditionalCounts; it supplies no new escape content, actual ear contraction, fan positivity or flip conclusion.

All interval endpoints are integers. pair(i,j) is an ordered integer pair, two(p,q) is its two-element finite set, Ioo(a,b) is the finite open integer interval, and toNat is Int.toNat. Sides(a,b)=intervalSides(a,b), D(a,b)=intervalDiagonals(a,b), Seg(a,b,S)=intervalSegments(a,b,S)=S union Sides(a,b). I(a,b,S)=IsIntervalTriangulation(a,b,S): S subset D(a,b), pairwise noninterleaving, and each missing diagonal in D(a,b) interleaves an S member. tau(a,b)=intervalTriangulationCount(a,b). L(a,b) is the subtype of all S satisfying I(a,b,S), and W(a,b) is the dependent sum over k in Set.Ioo(a,b) of L(a,k) times L(k,b). For an element of W, apex is its integer k, left and right are its two interval triangulations, and val takes the entire underlying finite set.

For polygons, symPair(u,v) is the unordered pair in Sym2(ZMod(m)); Symtwo denotes Sym2. DiagonalSet(m) is the set of all internal diagonals, PolygonTriSet(m) the set of all finite original chord sets satisfying ClusterAlgebras.IsTriangulation, and A(m) the subtype of that entire set. IntervalTriSet(a,b) is the set of all interval triangulations. BijOn includes injection, surjection and mapping into the displayed sets. ENatcard is extended cardinality; coeENat and intCast are the indicated casts. catalanNumber is definitionally Mathlib catalan. The consumer’s carrier is identical on whole chord sets, preserving all diagonal, crossing, noncrossing and maximality fields.

Theorem 1.1 (catalanNumber_zero).

$$(\mathrm{catalanNumber}\left(0\right)=1)$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.2 (catalanNumber_succ).

$$\forall N\in Nat,(\mathrm{catalanNumber}\left((N+1)\right)=\sum _{i\in \mathrm{range}\left((N+1)\right)}((\mathrm{catalanNumber}\left(i\right)\cdot \mathrm{catalanNumber}\left((N-i)\right))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.3 (Interleave.symm).

$$\forall p\in \mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right),\forall q\in \mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right),(\mathrm{Interleave}\left(p,q\right)⟹\mathrm{Interleave}\left(q,p\right))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.4 (mem_intervalTriangulations).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall S\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((S\in \mathrm{intervalTriangulations}\left(a,b\right))⟺I\left(a,b,S\right))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.5 (mk_mem_intervalDiagonals_iff).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall i\in \mathbb{Z},\forall j\in \mathbb{Z},((\mathrm{pair}\left(i,j\right)\in D\left(a,b\right))⟺((a\le i)\wedge ((j\le b)\wedge (((i+2)\le j)\wedge \neg (((i=a)\wedge (j=b)))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.6 (mk_mem_intervalSides_iff).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall i\in \mathbb{Z},\forall j\in \mathbb{Z},((\mathrm{pair}\left(i,j\right)\in \mathrm{Sides}\left(a,b\right))⟺(((i=a)\wedge (j=b))\vee ((a\le i)\wedge ((i<b)\wedge (j=(i+1))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.7 (not_interleave_of_mem_intervalSides).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall i\in \mathbb{Z},\forall j\in \mathbb{Z},\forall k\in \mathbb{Z},\forall l\in \mathbb{Z},((\mathrm{pair}\left(i,j\right)\in \mathrm{Sides}\left(a,b\right))⟹((a\le k)⟹((l\le b)⟹\neg (\mathrm{Interleave}\left(\mathrm{pair}\left(i,j\right),\mathrm{pair}\left(k,l\right)\right)))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.8 (IsIntervalTriangulation.bounds_of_mem_intervalSegments).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall S\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<b)⟹(I\left(a,b,S\right)⟹(\forall i\in \mathbb{Z},\forall j\in \mathbb{Z},((\mathrm{pair}\left(i,j\right)\in \mathrm{Seg}\left(a,b,S\right))⟹((a\le i)\wedge ((i<j)\wedge (j\le b)))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.9 (IsIntervalTriangulation.not_interleave).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall S\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<b)⟹(I\left(a,b,S\right)⟹(\forall p\in \mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right),\forall q\in \mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right),((p\in \mathrm{Seg}\left(a,b,S\right))⟹((q\in \mathrm{Seg}\left(a,b,S\right))⟹\neg (\mathrm{Interleave}\left(p,q\right)))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.10 (IsIntervalTriangulation.exists_interleave).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall S\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<b)⟹(I\left(a,b,S\right)⟹(\forall i\in \mathbb{Z},\forall j\in \mathbb{Z},((a\le i)⟹((i<j)⟹((j\le b)⟹(\neg ((\mathrm{pair}\left(i,j\right)\in \mathrm{Seg}\left(a,b,S\right)))⟹(\exists q\in \mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right),((q\in S)\wedge \mathrm{Interleave}\left(\mathrm{pair}\left(i,j\right),q\right))))))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.11 (IsIntervalTriangulation.existsUnique_apex).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall S\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<b)⟹(I\left(a,b,S\right)⟹(\forall i\in \mathbb{Z},\forall k\in \mathbb{Z},(((i+2)\le k)⟹((\mathrm{pair}\left(i,k\right)\in \mathrm{Seg}\left(a,b,S\right))⟹(\exists j\in \mathbb{Z},(((i<j)\wedge ((j<k)\wedge ((\mathrm{pair}\left(i,j\right)\in \mathrm{Seg}\left(a,b,S\right))\wedge (\mathrm{pair}\left(j,k\right)\in \mathrm{Seg}\left(a,b,S\right)))))\wedge (\forall z\in \mathbb{Z},(((i<z)\wedge ((z<k)\wedge ((\mathrm{pair}\left(i,z\right)\in \mathrm{Seg}\left(a,b,S\right))\wedge (\mathrm{pair}\left(z,k\right)\in \mathrm{Seg}\left(a,b,S\right)))))⟹(z=j))))))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.12 (IsIntervalTriangulation.le_or_le_of_apex).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall S\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<b)⟹(I\left(a,b,S\right)⟹(\forall k\in \mathbb{Z},((\mathrm{pair}\left(a,k\right)\in \mathrm{Seg}\left(a,b,S\right))⟹((\mathrm{pair}\left(k,b\right)\in \mathrm{Seg}\left(a,b,S\right))⟹(\forall i\in \mathbb{Z},\forall j\in \mathbb{Z},((\mathrm{pair}\left(i,j\right)\in S)⟹((j\le k)\vee (k\le i)))))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.13 (IsIntervalTriangulation.eq_union_of_apex).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall S\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<b)⟹(I\left(a,b,S\right)⟹(\forall k\in \mathbb{Z},((a<k)⟹((k<b)⟹((\mathrm{pair}\left(a,k\right)\in \mathrm{Seg}\left(a,b,S\right))⟹((\mathrm{pair}\left(k,b\right)\in \mathrm{Seg}\left(a,b,S\right))⟹(S=\mathrm{union}\left(\mathrm{union}\left(\mathrm{inter}\left(S,D\left(a,k\right)\right),\mathrm{inter}\left(S,D\left(k,b\right)\right)\right),\mathrm{inter}\left(\mathrm{two}\left(\mathrm{pair}\left(a,k\right),\mathrm{pair}\left(k,b\right)\right),D\left(a,b\right)\right)\right)))))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.14 (IsIntervalTriangulation.inter_left_of_apex).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall S\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<b)⟹(I\left(a,b,S\right)⟹(\forall k\in \mathbb{Z},((k<b)⟹((\mathrm{pair}\left(a,k\right)\in \mathrm{Seg}\left(a,b,S\right))⟹((\mathrm{pair}\left(k,b\right)\in \mathrm{Seg}\left(a,b,S\right))⟹I\left(a,k,\mathrm{inter}\left(S,D\left(a,k\right)\right)\right)))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.15 (IsIntervalTriangulation.inter_right_of_apex).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall S\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<b)⟹(I\left(a,b,S\right)⟹(\forall k\in \mathbb{Z},((a<k)⟹((\mathrm{pair}\left(a,k\right)\in \mathrm{Seg}\left(a,b,S\right))⟹((\mathrm{pair}\left(k,b\right)\in \mathrm{Seg}\left(a,b,S\right))⟹I\left(k,b,\mathrm{inter}\left(S,D\left(k,b\right)\right)\right)))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.16 (mk_mem_union_intervalDiagonals_iff).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall k\in \mathbb{Z},\forall Sone\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),\forall Stwo\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),\forall i\in \mathbb{Z},\forall j\in \mathbb{Z},((\mathrm{pair}\left(i,j\right)\in \mathrm{union}\left(\mathrm{union}\left(Sone,Stwo\right),\mathrm{inter}\left(\mathrm{two}\left(\mathrm{pair}\left(a,k\right),\mathrm{pair}\left(k,b\right)\right),D\left(a,b\right)\right)\right))⟺((\mathrm{pair}\left(i,j\right)\in Sone)\vee ((\mathrm{pair}\left(i,j\right)\in Stwo)\vee ((((i=a)\wedge (j=k))\vee ((i=k)\wedge (j=b)))\wedge (\mathrm{pair}\left(i,j\right)\in D\left(a,b\right))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.17 (IsIntervalTriangulation.union).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall k\in \mathbb{Z},\forall Sone\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),\forall Stwo\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<k)⟹((k<b)⟹(I\left(a,k,Sone\right)⟹(I\left(k,b,Stwo\right)⟹I\left(a,b,\mathrm{union}\left(\mathrm{union}\left(Sone,Stwo\right),\mathrm{inter}\left(\mathrm{two}\left(\mathrm{pair}\left(a,k\right),\mathrm{pair}\left(k,b\right)\right),D\left(a,b\right)\right)\right)\right)))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.18 (union_inter_intervalDiagonals_left).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall k\in \mathbb{Z},\forall Sone\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),\forall Stwo\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),(I\left(a,k,Sone\right)⟹(I\left(k,b,Stwo\right)⟹(\mathrm{inter}\left(\mathrm{union}\left(\mathrm{union}\left(Sone,Stwo\right),\mathrm{inter}\left(\mathrm{two}\left(\mathrm{pair}\left(a,k\right),\mathrm{pair}\left(k,b\right)\right),D\left(a,b\right)\right)\right),D\left(a,k\right)\right)=Sone)))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.19 (union_inter_intervalDiagonals_right).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall k\in \mathbb{Z},\forall Sone\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),\forall Stwo\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<k)⟹(I\left(a,k,Sone\right)⟹(I\left(k,b,Stwo\right)⟹(\mathrm{inter}\left(\mathrm{union}\left(\mathrm{union}\left(Sone,Stwo\right),\mathrm{inter}\left(\mathrm{two}\left(\mathrm{pair}\left(a,k\right),\mathrm{pair}\left(k,b\right)\right),D\left(a,b\right)\right)\right),D\left(k,b\right)\right)=Stwo))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.20 (union_apex_mem_intervalSegments).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},\forall k\in \mathbb{Z},\forall Sone\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),\forall Stwo\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathbb{Z},\mathbb{Z}\right)\right),((a<k)⟹((k<b)⟹((\mathrm{pair}\left(a,k\right)\in \mathrm{Seg}\left(a,b,\mathrm{union}\left(\mathrm{union}\left(Sone,Stwo\right),\mathrm{inter}\left(\mathrm{two}\left(\mathrm{pair}\left(a,k\right),\mathrm{pair}\left(k,b\right)\right),D\left(a,b\right)\right)\right)\right))\wedge (\mathrm{pair}\left(k,b\right)\in \mathrm{Seg}\left(a,b,\mathrm{union}\left(\mathrm{union}\left(Sone,Stwo\right),\mathrm{inter}\left(\mathrm{two}\left(\mathrm{pair}\left(a,k\right),\mathrm{pair}\left(k,b\right)\right),D\left(a,b\right)\right)\right)\right)))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.21 (exists_equiv_intervalTriangulation).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},(((a+2)\le b)⟹(\exists e\in \mathrm{Equiv}\left(L\left(a,b\right),W\left(a,b\right)\right),\forall S\in L\left(a,b\right),((\mathrm{pair}\left(a,\mathrm{apex}\left(\mathrm{app}\left(e,S\right)\right)\right)\in \mathrm{Seg}\left(a,b,\mathrm{val}\left(S\right)\right))\wedge ((\mathrm{pair}\left(\mathrm{apex}\left(\mathrm{app}\left(e,S\right)\right),b\right)\in \mathrm{Seg}\left(a,b,\mathrm{val}\left(S\right)\right))\wedge ((\mathrm{val}\left(\mathrm{left}\left(\mathrm{app}\left(e,S\right)\right)\right)=\mathrm{inter}\left(\mathrm{val}\left(S\right),D\left(a,\mathrm{apex}\left(\mathrm{app}\left(e,S\right)\right)\right)\right))\wedge (\mathrm{val}\left(\mathrm{right}\left(\mathrm{app}\left(e,S\right)\right)\right)=\mathrm{inter}\left(\mathrm{val}\left(S\right),D\left(\mathrm{apex}\left(\mathrm{app}\left(e,S\right)\right),b\right)\right)))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.22 (card_subtype_isIntervalTriangulation).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},(\mathrm{Fintypecard}\left(L\left(a,b\right)\right)=\mathrm{tau}\left(a,b\right))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.23 (intervalTriangulationCount_eq_sum).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},(((a+2)\le b)⟹(\mathrm{tau}\left(a,b\right)=\sum _{k\in \mathrm{Ioo}\left(a,b\right)}((\mathrm{tau}\left(a,k\right)\cdot \mathrm{tau}\left(k,b\right)))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.24 (intervalTriangulationCount_self_add_one).

$$\forall a\in \mathbb{Z},(\mathrm{tau}\left(a,(a+1)\right)=1)$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.25 (intervalTriangulationCount_eq_catalanNumber).

$$\forall a\in \mathbb{Z},\forall b\in \mathbb{Z},((a<b)⟹(\mathrm{tau}\left(a,b\right)=\mathrm{catalanNumber}\left(\mathrm{toNat}\left(((b-a)-1)\right)\right)))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.26 (basePosSeg_mk).

$$\forall m\in Nat,\forall c\in \mathrm{ZMod}\left(m\right),\forall u\in \mathrm{ZMod}\left(m\right),\forall v\in \mathrm{ZMod}\left(m\right),(\mathrm{basePosSeg}\left(c,\mathrm{symPair}\left(u,v\right)\right)=\mathrm{pair}\left(\min \left(\mathrm{basePos}\left(c,u\right),\mathrm{basePos}\left(c,v\right)\right),\max \left(\mathrm{basePos}\left(c,u\right),\mathrm{basePos}\left(c,v\right)\right)\right))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.27 (basePos_nonneg).

$$\forall m\in Nat,\forall c\in \mathrm{ZMod}\left(m\right),\forall v\in \mathrm{ZMod}\left(m\right),(0\le \mathrm{basePos}\left(c,v\right))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.28 (basePos_lt).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\forall v\in \mathrm{ZMod}\left(m\right),(\mathrm{basePos}\left(c,v\right)<\mathrm{intCast}\left(m\right))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.29 (basePos_eq_ite).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\forall v\in \mathrm{ZMod}\left(m\right),(\mathrm{basePos}\left(c,v\right)=\mathrm{ite}\left((\mathrm{val}\left(c\right)\le \mathrm{val}\left(v\right)),(\mathrm{intCast}\left(\mathrm{val}\left(v\right)\right)-\mathrm{intCast}\left(\mathrm{val}\left(c\right)\right)),((\mathrm{intCast}\left(\mathrm{val}\left(v\right)\right)-\mathrm{intCast}\left(\mathrm{val}\left(c\right)\right))+\mathrm{intCast}\left(m\right))\right))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.30 (basePos_injective).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\mathrm{Injective}\left(\mathrm{basePos}\left(c\right)\right)$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.31 (exists_basePos_eq).

$$\forall m\in Nat,\forall c\in \mathrm{ZMod}\left(m\right),\forall k\in \mathbb{Z},((0\le k)⟹((k<\mathrm{intCast}\left(m\right))⟹(\exists v\in \mathrm{ZMod}\left(m\right),(\mathrm{basePos}\left(c,v\right)=k))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.32 (sbtw_iff_val).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall x\in \mathrm{ZMod}\left(m\right),\forall y\in \mathrm{ZMod}\left(m\right),\forall z\in \mathrm{ZMod}\left(m\right),(\mathrm{sbtw}\left(x,y,z\right)⟺(((\mathrm{val}\left(x\right)<\mathrm{val}\left(y\right))\wedge (\mathrm{val}\left(y\right)<\mathrm{val}\left(z\right)))\vee (((\mathrm{val}\left(y\right)<\mathrm{val}\left(z\right))\wedge (\mathrm{val}\left(z\right)<\mathrm{val}\left(x\right)))\vee ((\mathrm{val}\left(z\right)<\mathrm{val}\left(x\right))\wedge (\mathrm{val}\left(x\right)<\mathrm{val}\left(y\right))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.33 (sbtw_iff_sbtw_basePos).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\forall u\in \mathrm{ZMod}\left(m\right),\forall x\in \mathrm{ZMod}\left(m\right),\forall v\in \mathrm{ZMod}\left(m\right),(\mathrm{sbtw}\left(u,x,v\right)⟺\mathrm{sbtw}\left(\mathrm{basePos}\left(c,u\right),\mathrm{basePos}\left(c,x\right),\mathrm{basePos}\left(c,v\right)\right))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.34 (basePos_add_one).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\forall u\in \mathrm{ZMod}\left(m\right),(\mathrm{basePos}\left(c,(u+1)\right)=\mathrm{ite}\left(((\mathrm{basePos}\left(c,u\right)+1)=\mathrm{intCast}\left(m\right)),0,(\mathrm{basePos}\left(c,u\right)+1)\right))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.35 (basePosSeg_injective).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\mathrm{Injective}\left(\mathrm{basePosSeg}\left(c\right)\right)$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.36 (IsSegment.exists_basePos_lt).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\forall s\in \mathrm{Symtwo}\left(\mathrm{ZMod}\left(m\right)\right),(\mathrm{IsSegment}\left(s\right)⟹(\exists u\in \mathrm{ZMod}\left(m\right),\exists v\in \mathrm{ZMod}\left(m\right),((s=\mathrm{symPair}\left(u,v\right))\wedge (\mathrm{basePos}\left(c,u\right)<\mathrm{basePos}\left(c,v\right)))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.37 (basePosSeg_mk_of_lt).

$$\forall m\in Nat,\forall c\in \mathrm{ZMod}\left(m\right),\forall u\in \mathrm{ZMod}\left(m\right),\forall v\in \mathrm{ZMod}\left(m\right),((\mathrm{basePos}\left(c,u\right)<\mathrm{basePos}\left(c,v\right))⟹(\mathrm{basePosSeg}\left(c,\mathrm{symPair}\left(u,v\right)\right)=\mathrm{pair}\left(\mathrm{basePos}\left(c,u\right),\mathrm{basePos}\left(c,v\right)\right)))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.38 (isSide_mk_iff).

$$\forall m\in Nat,\forall u\in \mathrm{ZMod}\left(m\right),\forall v\in \mathrm{ZMod}\left(m\right),(\mathrm{IsSide}\left(\mathrm{symPair}\left(u,v\right)\right)⟺((v=(u+1))\vee (u=(v+1))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.39 (cross_mk_iff).

$$\forall m\in Nat,\forall u\in \mathrm{ZMod}\left(m\right),\forall v\in \mathrm{ZMod}\left(m\right),\forall x\in \mathrm{ZMod}\left(m\right),\forall y\in \mathrm{ZMod}\left(m\right),(\mathrm{Cross}\left(\mathrm{symPair}\left(u,v\right),\mathrm{symPair}\left(x,y\right)\right)⟺((\mathrm{sbtw}\left(u,x,v\right)\wedge \mathrm{sbtw}\left(v,y,u\right))\vee (\mathrm{sbtw}\left(u,y,v\right)\wedge \mathrm{sbtw}\left(v,x,u\right))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.40 (cross_mk_iff_basePos).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\forall u\in \mathrm{ZMod}\left(m\right),\forall v\in \mathrm{ZMod}\left(m\right),\forall x\in \mathrm{ZMod}\left(m\right),\forall y\in \mathrm{ZMod}\left(m\right),(\mathrm{Cross}\left(\mathrm{symPair}\left(u,v\right),\mathrm{symPair}\left(x,y\right)\right)⟺((\mathrm{sbtw}\left(\mathrm{basePos}\left(c,u\right),\mathrm{basePos}\left(c,x\right),\mathrm{basePos}\left(c,v\right)\right)\wedge \mathrm{sbtw}\left(\mathrm{basePos}\left(c,v\right),\mathrm{basePos}\left(c,y\right),\mathrm{basePos}\left(c,u\right)\right))\vee (\mathrm{sbtw}\left(\mathrm{basePos}\left(c,u\right),\mathrm{basePos}\left(c,y\right),\mathrm{basePos}\left(c,v\right)\right)\wedge \mathrm{sbtw}\left(\mathrm{basePos}\left(c,v\right),\mathrm{basePos}\left(c,x\right),\mathrm{basePos}\left(c,u\right)\right))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.41 (isSide_mk_iff_basePos).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\forall u\in \mathrm{ZMod}\left(m\right),\forall v\in \mathrm{ZMod}\left(m\right),((\mathrm{basePos}\left(c,u\right)<\mathrm{basePos}\left(c,v\right))⟹(\mathrm{IsSide}\left(\mathrm{symPair}\left(u,v\right)\right)⟺((\mathrm{basePos}\left(c,v\right)=(\mathrm{basePos}\left(c,u\right)+1))\vee ((\mathrm{basePos}\left(c,u\right)=0)\wedge (\mathrm{basePos}\left(c,v\right)=(\mathrm{intCast}\left(m\right)-1))))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.42 (bijOn_basePosSeg_isDiagonal).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\mathrm{BijOn}\left(\mathrm{basePosSeg}\left(c\right),\mathrm{DiagonalSet}\left(m\right),\mathrm{coeSet}\left(D\left(0,(\mathrm{intCast}\left(m\right)-1)\right)\right)\right)$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.43 (cross_iff_interleave).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\forall s\in \mathrm{Symtwo}\left(\mathrm{ZMod}\left(m\right)\right),\forall t\in \mathrm{Symtwo}\left(\mathrm{ZMod}\left(m\right)\right),(\mathrm{IsSegment}\left(s\right)⟹(\mathrm{IsSegment}\left(t\right)⟹(\mathrm{Cross}\left(s,t\right)⟺\mathrm{Interleave}\left(\mathrm{basePosSeg}\left(c,s\right),\mathrm{basePosSeg}\left(c,t\right)\right))))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.44 (bijOn_basePosTri).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],\forall c\in \mathrm{ZMod}\left(m\right),\mathrm{BijOn}\left(\mathrm{basePosTri}\left(c\right),\mathrm{PolygonTriSet}\left(m\right),\mathrm{IntervalTriSet}\left(0,(\mathrm{intCast}\left(m\right)-1)\right)\right)$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

Theorem 1.45 (encard_setOf_isTriangulation).

$$\forall m\in Nat,[\mathrm{NeZero}\left(m\right)],((3\le m)⟹(\mathrm{ENatcard}\left(A\left(m\right)\right)=\mathrm{coeENat}\left(\mathrm{catalanNumber}\left((m-2)\right)\right)))$$

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

Citation. Ashvin A. Swaminathan and Alexey Sorokin (2026). ClusterAlgebras: interval and polygon triangulation enumeration. URL: https://github.com/AxiomMath/ClusterAlgebras/tree/a9174706bce3bcb0fa342b4614f98ef2acb7f91c.

Commentary.

Exact licensed source support consumed by the complete polygon-count proof. Its source proof body is unchanged.

References

• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.basePosSeg_injective
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.basePosSeg_mk
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.basePosSeg_mk_of_lt
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.basePos_add_one
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.basePos_eq_ite
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.basePos_injective
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.basePos_lt
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.basePos_nonneg
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.bijOn_basePosSeg_isDiagonal
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.bijOn_basePosTri
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.bounds_of_mem_intervalSegments
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.card_subtype_isIntervalTriangulation
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.catalanNumber_succ
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.catalanNumber_zero
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.cross_iff_interleave
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.cross_mk_iff
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.cross_mk_iff_basePos
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.encard_setOf_isTriangulation
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.eq_union_of_apex
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.existsUnique_apex
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.exists_basePos_eq
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.exists_basePos_lt
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.exists_equiv_intervalTriangulation
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.exists_interleave
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.inter_left_of_apex
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.inter_right_of_apex
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.intervalTriangulationCount_eq_catalanNumber
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.intervalTriangulationCount_eq_sum
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.intervalTriangulationCount_self_add_one
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.isSide_mk_iff
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.isSide_mk_iff_basePos
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.le_or_le_of_apex
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.mem_intervalTriangulations
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.mk_mem_intervalDiagonals_iff
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.mk_mem_intervalSides_iff
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.mk_mem_union_intervalDiagonals_iff
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.not_interleave
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.not_interleave_of_mem_intervalSides
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.sbtw_iff_sbtw_basePos
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.sbtw_iff_val
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.symm
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.union
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.union_apex_mem_intervalSegments
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.union_inter_intervalDiagonals_left
• Truth anchor: D5/S3/Geometry/Polygons/PolygonCatalanSupplier.union_inter_intervalDiagonals_right