Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Weak coordinate patterns and literal graph realization

Abstract

Coordinate graphs keep zero, repeated positions and cutoffs, arbitrary exceptional edges, and an ordinary clique. Their admissibility is unchanged by increasing coordinate refinements or by a universal ordinary tail.

Definition 1.1 (Ordinary ranks and labelled exceptions).

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.CoordinateVertex (✓ 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 two constructors are ordinary(r) for every natural rank r, including the anchor zero, and exceptional(j) for j in Fin i. The position list is a type parameter, so each graph has its own order. The displayed equivalence describes the two constructors; it does not identify their order with a sum order.

Definition 1.2 (Lexicographic vertex keys).

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.coordinateKey (✓ 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.

Keys are ordered lexicographically. Ordinary r precedes every exception in position r, and the exceptional index breaks position ties. Distinct vertices have distinct keys. The coordinate linear order is pulled back along this injection.

Definition 1.3 (Edges with every tie and exceptional bit retained).

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.coordinateEdges (✓ 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.

Only increasing endpoint pairs are edges. All ordinary pairs are adjacent. The pair involving exceptional j and ordinary rank r is adjacent exactly when c(j)<r, in either possible endpoint order. The ordered exceptional pair j,k is adjacent exactly when B(j,k). No condition on B, positivity, distinctness or monotonicity of p or c is built into this definition.

Theorem 1.4 (Increasing refinements preserve all weak patterns).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.coordinate_rules_refinement_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.

For an increasing map e, send ordinary rank r to the least k with r<=e(k), and leave each exceptional label fixed. This collapse is monotone. Its increasing section sends ordinary k to e(k), again fixing exceptional labels. Incidence transforms because e(c)<r is equivalent to c<ceil_e(r). Hence the expanded graph is exactly the clique lift of the original graph, including all collapsed ordinary fibers and every equality between coordinate entries. The clique-lift equivalence proves both directions of Rules. The hypothesis e(0)=0 retains the distinguished zero used for source patterns.

Definition 1.5 (A universal tail above an initial segment).

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.universalTail (✓ 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.

Every increasing pair ending outside S is added; edges within S are read from E. When S is downward closed and E is supported there, this operation preserves and reflects both ordered closure rules, even for an infinite tail.

Definition 1.6 (The finite coordinate segment).

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.coordinateInside (✓ 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 segment contains ordinary ranks zero through M and every exceptional vertex. Under p(j)<=M it is an initial segment in the coordinate order.

Definition 1.7 (Edges on the finite coordinate segment).

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.boundedCoordinateEdges (✓ 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.

Retain coordinate edges whose upper endpoint belongs to the finite segment. When positions are bounded by M the lower endpoint belongs to the segment as well.

Theorem 1.8 (Coordinate segments are initial segments).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.coordinateInside_downward (✓ 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.

If every exceptional position is at most M, every vertex preceding a vertex in the segment is also in the segment. An ordinary vertex before exception j has rank at most p(j); all exceptions belong to the segment.

Theorem 1.9 (Deleting every universal ordinary tail).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.coordinate_rules_bounded_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.

When positions and cutoffs are at most M, each ordinary vertex of rank greater than M follows every exception and is adjacent to every earlier vertex. The infinite graph is exactly the universal-tail extension of the bounded graph. The universal-tail argument gives equivalence, including M=0 and tied or zero entries.

Definition 1.10 (The finite vertex subtype).

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.BoundedCoordinateVertex (✓ 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.

This subtype inherits the coordinate order. It includes the anchor even when there are no positive ordinary vertices.

Definition 1.11 (Canonical natural labels).

Formalization. D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.coordinateLabel (✓ 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.

An ordinary vertex of rank r has r earlier ordinary vertices and one earlier exceptional vertex for each p(j)<r. Exception j has p(j) earlier positive ordinary vertices, the anchor, and j earlier exceptions. These formulas include every zero and tied position.

Theorem 1.12 (Labels preserve the coordinate order).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.coordinateLabel_strictMono (✓ 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.

For an increasing position list, the number of positions below r is a nondecreasing function of r. Its value is at most j when r<=p(j), and exceeds j when p(j)<r. These inequalities prove the two mixed vertex comparisons; ordinary and exceptional comparisons follow from the rank and index increments.

Theorem 1.13 (Labels stay in the full finite interval).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.coordinateLabel_bound (✓ 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.

There are i exceptional positions in total. Ordinary rank r<=M therefore has label at most M+i. The j-th exception has p(j)<=M and j<i, giving the same bound. Monotonicity is not needed for this bound.

Theorem 1.14 (Every finite label occurs exactly once).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.coordinateLabel_bijective (✓ 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 vertex set has M+1 ordinary vertices and i exceptions. The strict label map injects it into the M+i+1 labels zero through M+i, so equal finite cardinalities give bijectivity. This includes the single anchor when M=i=0. The theorem states bijectivity of the map into Fin(M+i+1); the display gives its equivalent uniqueness and full natural-interval surjectivity clauses.

Theorem 1.15 (An exact increasing realization of every source graph).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns.edgeFamily_coordinate_realization (✓ 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.

Extract the ordinary and exceptional lists from the literal edge family. Ordinary rank zero maps to the anchor; positive ordinary rank r maps to entry r-1 of the ordered ordinary list; exceptional j maps to the j-th missing anchor neighbor. Position and cutoff laws give the mixed edges, the ordinary vertices form a clique, and B retains each actual exceptional edge. The map is increasing and bijects onto every natural vertex from zero through n+1. Thus this is an exact edge correspondence, including zero positions, coinciding coordinates and an empty positive ordinary list. It does not count coordinate patterns or assert polynomiality.

References