Triangular subsets and ordered closure

Abstract

The literal Mazorchuk-Xu triangular family has a repeated-point closure rule equivalent to two universal rules on ordered edges.

Definition 1.1 (The source triangle).

$$\forall n\in \mathrm{Nat}\left(\right),\mathrm{triangle}\left(n\right)=\{p\in \mathrm{Prod}\left(\mathrm{Nat}\left(\right),\mathrm{Nat}\left(\right)\right)|(\mathrm{fst}\left(p\right)\le \mathrm{snd}\left(p\right))\wedge (\mathrm{snd}\left(p\right)\le n)\}$$

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.triangle (✓ std3).

Citation. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

Natural coordinates represent the nonnegative integer coordinates in Section 3, before Section 3.1. No nonempty-row condition is imposed.

Definition 1.2 (Repeated-point closure).

$$\forall Y\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathrm{Nat}\left(\right),\mathrm{Nat}\left(\right)\right)\right),(\mathrm{Star}\left(Y\right))\iff (\forall a\in \mathrm{Nat}\left(\right),\forall b\in \mathrm{Nat}\left(\right),\forall c\in \mathrm{Nat}\left(\right),\forall d\in \mathrm{Nat}\left(\right),\forall e\in \mathrm{Nat}\left(\right),\forall f\in \mathrm{Nat}\left(\right),((((((((((a,b)\in Y)\wedge ((c,d)\in Y))\wedge ((e,f)\in Y))\wedge (a\le c))\wedge (c\le b))\wedge (a\le e))\wedge (e\le b))\wedge (b\le d))\wedge (b\le f))\Rightarrow (((\max \left(c,e\right),\max \left(d,f\right))\in Y)\wedge ((b<\min \left(d,f\right))\Rightarrow ((b+1,\min \left(d,f\right))\in Y))))$$

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.Star (✓ std3).

Citation. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

The three selected points may coincide. Both forced points, including the conditional successor/minimum point, are retained.

Definition 1.3 (First-column count).

$$\forall Y\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathrm{Nat}\left(\right),\mathrm{Nat}\left(\right)\right)\right),\mathrm{firstColumnCard}\left(Y\right)=\mathrm{card}\left(\{p\in Y|\mathrm{fst}\left(p\right)=0\}\right)$$

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.firstColumnCard (✓ std3).

Citation. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

Only points whose first coordinate is zero are counted.

Definition 1.4 (The finite family R(n,k)).

$$\forall n\in \mathrm{Nat}\left(\right),\forall k\in \mathrm{Nat}\left(\right),\mathrm{family}\left(n,k\right)=\{Y\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathrm{Nat}\left(\right),\mathrm{Nat}\left(\right)\right)\right)|((Y\subseteq \mathrm{triangle}\left(n\right))\wedge (\mathrm{Star}\left(Y\right)))\wedge (\mathrm{firstColumnCard}\left(Y\right)=k)\}$$

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.family (✓ std3).

Citation. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

All subsets of the triangle are tested. Empty subsets and empty rows remain in the domain.

Definition 1.5 (The cardinal r(n,k)).

$$\forall n\in \mathrm{Nat}\left(\right),\forall k\in \mathrm{Nat}\left(\right),\mathrm{count}\left(n,k\right)=\mathrm{card}\left(\mathrm{family}\left(n,k\right)\right)$$

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.count (✓ std3).

Citation. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

The first argument is a natural number. This definition introduces no recurrence value at minus one.

Definition 1.6 (The complete polynomiality question).

$$(\mathrm{Conjecture}\left(\right))\iff (\forall i\in \mathrm{Nat}\left(\right),\exists p\in \mathrm{Polynomial}\left(\mathrm{Rat}\left(\right)\right),((\mathrm{natDegree}\left(p\right)=2\cdot i)\wedge (\mathrm{leadingCoeff}\left(p\right)=\mathrm{inv}\left(\mathrm{castRat}\left(\mathrm{factorial}\left(i\right)\right)\right)))\wedge (\forall n\in \mathrm{Nat}\left(\right),(i\le n+1)\Rightarrow (\mathrm{eval}\left(p,\mathrm{castRat}\left(n\right)\right)=\mathrm{castRat}\left(\mathrm{count}\left(n,n+1-i\right)\right))))$$

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.Conjecture (✓ std3).

Citation. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

For each deficit one rational polynomial must work at every valid natural rank, with exact degree and leading coefficient. Rational coefficients embed into real numerical values. This is the question’s statement; no proof of this proposition is asserted here. Deficits zero through three are prior source results.

Definition 1.7 (Point-to-edge relation).

$$\forall Y\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathrm{Nat}\left(\right),\mathrm{Nat}\left(\right)\right)\right),\forall a\in \mathrm{Nat}\left(\right),\forall b\in \mathrm{Nat}\left(\right),(\mathrm{pointEdges}\left(Y,a,b\right))\iff ((a<b)\wedge ((a,b-1)\in Y))$$

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.pointEdges (✓ std3).

Source. Repository-derived.

Acknowledgement. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

The source point (a,b) becomes the strict edge (a,b+1). Natural subtraction appears only after strict endpoint order has ensured a positive upper endpoint.

Definition 1.8 (The rules P and J).

$$\forall A\in \mathrm{Type}\left(\right),[\mathrm{LinearOrder}\left(A\right)]\forall E\in A\to \left(A\to \mathrm{Prop}\left(\right)\right),(\mathrm{Rules}\left(E\right))\iff (((\forall a\in A,\forall b\in A,(E\left(a,b\right))\Rightarrow (a<b))\wedge (\forall a\in A,\forall b\in A,\forall c\in A,\forall d\in A,(((((E\left(a,b\right))\wedge (E\left(c,d\right)))\wedge (a\le c))\wedge (c<b))\wedge (b<d))\Rightarrow (E\left(b,d\right))))\wedge (\forall a\in A,\forall b\in A,\forall c\in A,\forall d\in A,\forall e\in A,\forall f\in A,(((((((((E\left(a,b\right))\wedge (E\left(c,d\right)))\wedge (E\left(e,f\right)))\wedge (a\le c))\wedge (c<b))\wedge (a\le e))\wedge (e<b))\wedge (b\le d))\wedge (b\le f))\Rightarrow (E\left(\max \left(c,e\right),\max \left(d,f\right)\right))))$$

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.Rules (✓ std3).

Source. Repository-derived.

Acknowledgement. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

P propagates an overlapping pair to its upper-right edge. J joins the two lower endpoints and the two upper endpoints by maxima. Ordered edges are strict.

Theorem 1.9 (Triangle membership).

$$\forall n\in \mathrm{Nat}\left(\right),\forall a\in \mathrm{Nat}\left(\right),\forall b\in \mathrm{Nat}\left(\right),((a,b)\in \mathrm{triangle}\left(n\right))\iff ((a\le b)\wedge (b\le n))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.mem_triangle (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

The finite range construction is exactly a less-than-or-equal b less-than-or-equal n.

Theorem 1.10 (Literal source equivalence).

$$\forall Y\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathrm{Nat}\left(\right),\mathrm{Nat}\left(\right)\right)\right),(\forall a\in \mathrm{Nat}\left(\right),\forall b\in \mathrm{Nat}\left(\right),((a,b)\in Y)\Rightarrow (a\le b))\Rightarrow ((\mathrm{Star}\left(Y\right))\iff (\mathrm{Rules}\left(\mathrm{pointEdges}\left(Y\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.star_iff_rules (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

Repeating the second source point gives P. J is the source’s maximum conclusion. Conversely P, applied to the premise with the smaller upper endpoint, recovers the entire successor/minimum conclusion. This proves both directions for every triangular subset, including repetitions and empty subsets.

Theorem 1.11 (Exact finite-family membership).

$$\forall n\in \mathrm{Nat}\left(\right),\forall k\in \mathrm{Nat}\left(\right),\forall Y\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathrm{Nat}\left(\right),\mathrm{Nat}\left(\right)\right)\right),(Y\in \mathrm{family}\left(n,k\right))\iff (((Y\subseteq \mathrm{triangle}\left(n\right))\wedge (\mathrm{Rules}\left(\mathrm{pointEdges}\left(Y\right)\right)))\wedge (\mathrm{firstColumnCard}\left(Y\right)=k))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.mem_family_iff (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Volodymyr Mazorchuk, Shuoyang Xu (2026). On the number of cokernel-closed additive subcategories for uniformly oriented A_n quivers. DOI: 10.48550/arXiv.2610.07999. URL: https://arxiv.org/html/2610.07999v2.

Commentary.

The source-family test retains the triangle bound, both ordered-edge rules and the exact first-column statistic.

References

• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.Conjecture
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.Rules
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.Star
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.count
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.family
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.firstColumnCard
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.mem_family_iff
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.mem_triangle
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.pointEdges
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.star_iff_rules
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuClosure.triangle