Exact source reconstruction and coordinate counting

Abstract

Bounded weak coordinate data and literal triangular closure have exactly the same finite objects and first-column count. The coordinate description permits every zero and tie, while ordered exceptional bits make reconstruction unique.

Definition 1.1 (Reconstruct the labelled finite edges).

$$\forall M\in \mathrm{Nat}\left(\right),\forall i\in \mathrm{Nat}\left(\right),\forall p\in \mathrm{Fin}\left(i\right)\to \mathrm{Nat}\left(\right),\forall c\in \mathrm{Fin}\left(i\right)\to \mathrm{Nat}\left(\right),\forall B\in \mathrm{Fin}\left(i\right)\to \left(\mathrm{Fin}\left(i\right)\to \mathrm{Prop}\left(\right)\right),\forall a\in \mathrm{Nat}\left(\right),\forall b\in \mathrm{Nat}\left(\right),((a,b)\in \mathrm{coordinateEdgeSet}\left(M,p,c,B\right))\iff (\exists u\in \mathrm{BoundedCoordinateVertex}\left(M,p\right),\exists v\in \mathrm{BoundedCoordinateVertex}\left(M,p\right),((\mathrm{coordinateEdges}\left(p,c,B\right)(\mathrm{val}\left(u\right),\mathrm{val}\left(v\right)))\wedge (\mathrm{coordinateLabel}\left(p,\mathrm{val}\left(u\right)\right)=a))\wedge (\mathrm{coordinateLabel}\left(p,\mathrm{val}\left(v\right)\right)=b))$$

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

Take all pairs of bounded coordinate vertices joined by coordinateEdges and apply the canonical natural label to both endpoints. This definition keeps actual edges; it contains no assumed counting formula. For a weakly increasing position list the label map is increasing and bijective onto zero through M+i.

Theorem 1.2 (Reconstruction preserves the complete literal family).

$$\forall n\in \mathrm{Nat}\left(\right),\forall i\in \mathrm{Nat}\left(\right),(i\le n+\mathrm{one}\left(\right))\Rightarrow (\forall p\in \mathrm{Fin}\left(i\right)\to \mathrm{Nat}\left(\right),\forall c\in \mathrm{Fin}\left(i\right)\to \mathrm{Nat}\left(\right),\forall B\in \mathrm{Fin}\left(i\right)\to \left(\mathrm{Fin}\left(i\right)\to \mathrm{Prop}\left(\right)\right),((((\mathrm{Monotone}\left(p\right))\wedge (\forall j\in \mathrm{Fin}\left(i\right),p(j)\le n+\mathrm{one}\left(\right)-i))\wedge (\forall j\in \mathrm{Fin}\left(i\right),c(j)\le n+\mathrm{one}\left(\right)-i))\wedge (\mathrm{Rules}\left(\mathrm{boundedCoordinateEdges}\left(n+\mathrm{one}\left(\right)-i,p,c,B\right)\right)))\Rightarrow (\mathrm{coordinateEdgeSet}\left(n+\mathrm{one}\left(\right)-i,p,c,B\right)\in \mathrm{edgeFamily}\left(n,n+\mathrm{one}\left(\right)-i\right)))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.coordinateEdgeSet_mem_edgeFamily (✓ 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 increasing image transports both ordered closure rules and their maxima. The endpoint labels stay between zero and n+1. The anchor is ordinary rank zero; its neighbors are exactly ordinary ranks one through M, independently of all cutoffs and exceptional bits. Filtering the image edges by first coordinate zero therefore has cardinality M. The literal edge family and its triangle-point bijection retain the repeated-point source condition and both forced conclusions.

Theorem 1.3 (Every source graph has canonical weak coordinate data).

$$\forall n\in \mathrm{Nat}\left(\right),\forall i\in \mathrm{Nat}\left(\right),(i\le n+\mathrm{one}\left(\right))\Rightarrow (\forall A\in \mathrm{Finset}\left(\mathrm{Prod}\left(\mathrm{Nat}\left(\right),\mathrm{Nat}\left(\right)\right)\right),(A\in \mathrm{edgeFamily}\left(n,n+\mathrm{one}\left(\right)-i\right))\Rightarrow (\exists p\in \mathrm{Fin}\left(i\right)\to \mathrm{Nat}\left(\right),\exists c\in \mathrm{Fin}\left(i\right)\to \mathrm{Nat}\left(\right),\exists B\in \mathrm{Fin}\left(i\right)\to \left(\mathrm{Fin}\left(i\right)\to \mathrm{Prop}\left(\right)\right),(((((\mathrm{Monotone}\left(p\right))\wedge (\forall j\in \mathrm{Fin}\left(i\right),p(j)\le n+\mathrm{one}\left(\right)-i))\wedge (\forall j\in \mathrm{Fin}\left(i\right),c(j)\le n+\mathrm{one}\left(\right)-i))\wedge (\forall j\in \mathrm{Fin}\left(i\right),\forall k\in \mathrm{Fin}\left(i\right),(B\left(j,k\right))\Rightarrow (j<k)))\wedge (\mathrm{Rules}\left(\mathrm{boundedCoordinateEdges}\left(n+\mathrm{one}\left(\right)-i,p,c,B\right)\right)))\wedge (\mathrm{coordinateEdgeSet}\left(n+\mathrm{one}\left(\right)-i,p,c,B\right)=A)))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.edgeFamily_eq_coordinateEdgeSet (✓ 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 exact source realization gives an increasing bijection into the full finite natural interval. Its range equals the range of coordinateLabel, so uniqueness of increasing enumerations identifies the two maps. Restriction and extension across the supported finite vertex set give bounded Rules. Every actual source edge then agrees with the reconstructed edge set. Exceptional bits imply increasing exceptional labels, leaving no unused reverse or loop bits.

Definition 1.4 (The finite coordinate carrier).

$$\forall M\in \mathrm{Nat}\left(\right),\forall i\in \mathrm{Nat}\left(\right),\mathrm{CoordinateDataCarrier}\left(M,i\right)=\mathrm{Prod}\left(\mathrm{Fin}\left(i\right)\to \mathrm{Fin}\left(M+\mathrm{one}\left(\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(i\right)\to \mathrm{Fin}\left(M+\mathrm{one}\left(\right)\right),\mathrm{Finset}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(i\right),\mathrm{Fin}\left(i\right)\right)\right)\right)\right)$$

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

A datum consists of a position array, a cutoff array, and a finite set of labelled exceptional edges. Both arrays take values zero through M. There are no positivity or distinctness assumptions.

Definition 1.5 (The finite admissible data family).

$$\forall M\in \mathrm{Nat}\left(\right),\forall i\in \mathrm{Nat}\left(\right),\forall d\in \mathrm{CoordinateDataCarrier}\left(M,i\right),(d\in \mathrm{coordinateDataFamily}\left(M,i\right))\iff (((\mathrm{Monotone}\left(\mathrm{values}\left(\mathrm{fst}\left(d\right)\right)\right))\wedge (\forall j\in \mathrm{Fin}\left(i\right),\forall k\in \mathrm{Fin}\left(i\right),((j,k)\in \mathrm{snd}\left(\mathrm{snd}\left(d\right)\right))\Rightarrow (j<k)))\wedge (\mathrm{Rules}\left(\mathrm{boundedCoordinateEdges}\left(M,\mathrm{values}\left(\mathrm{fst}\left(d\right)\right),\mathrm{values}\left(\mathrm{fst}\left(\mathrm{snd}\left(d\right)\right)\right),\mathrm{membership}\left(\mathrm{snd}\left(\mathrm{snd}\left(d\right)\right)\right)\right)\right)))$$

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

Filter the finite carrier by a weakly increasing position array, exceptional bits supported on j<k, and the exact bounded closure rules. The notation values(f) in the display denotes the pointwise natural values of a Fin-valued array. Bounds are built into the carrier, and the empty exceptional index set is allowed.

Theorem 1.6 (Exact coordinate enumeration on every original rank).

$$\forall n\in \mathrm{Nat}\left(\right),\forall i\in \mathrm{Nat}\left(\right),(i\le n+\mathrm{one}\left(\right))\Rightarrow (\mathrm{count}\left(n,n+\mathrm{one}\left(\right)-i\right)=\mathrm{card}\left(\mathrm{coordinateDataFamily}\left(n+\mathrm{one}\left(\right)-i,i\right)\right))$$

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

Reconstruction maps the finite admissible data family into edgeFamily. For injectivity, the increasing missing anchor-neighbor labels p(j)+j+1 recover p; ordinary incidence at rank c(j)+1 distinguishes any two bounded cutoffs; the remaining increasing exceptional edges recover B. The source reconstruction supplies surjectivity. The finite bijection and the literal point-edge count bridge give the displayed equality for every valid n and i, including M=0, i=0 and n=0. The separate binomial-basis coefficient identity and its top coefficient are not asserted by this cardinality theorem.

Theorem 1.7 (Generic admissibility forces the exceptional bits).

$$\forall M\in \mathrm{Nat}\left(\right),\forall i\in \mathrm{Nat}\left(\right),\forall p\in \mathrm{Fin}\left(i\right)\to \mathrm{Nat}\left(\right),\forall c\in \mathrm{Fin}\left(i\right)\to \mathrm{Nat}\left(\right),\forall B\in \mathrm{Fin}\left(i\right)\to \left(\mathrm{Fin}\left(i\right)\to \mathrm{Prop}\left(\right)\right),((((((\mathrm{StrictMono}\left(p\right))\wedge (\forall j\in \mathrm{Fin}\left(i\right),p(j)\le M))\wedge (\forall j\in \mathrm{Fin}\left(i\right),c(j)\le M))\wedge (\forall j\in \mathrm{Fin}\left(i\right),\mathrm{zero}\left(\right)<p(j)))\wedge (\forall j\in \mathrm{Fin}\left(i\right),\forall k\in \mathrm{Fin}\left(i\right),\neg (c(j)=p(k))))\wedge (\forall j\in \mathrm{Fin}\left(i\right),\forall k\in \mathrm{Fin}\left(i\right),(B\left(j,k\right))\Rightarrow (j<k)))\Rightarrow ((\mathrm{Rules}\left(\mathrm{boundedCoordinateEdges}\left(M,p,c,B\right)\right))\Rightarrow (\forall j\in \mathrm{Fin}\left(i\right),\forall k\in \mathrm{Fin}\left(i\right),(B\left(j,k\right))\iff (((j<k)\wedge (c(j)<p(k)))\wedge (c(k)<p(j)))))$$

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

Assume positive strictly increasing positions, bounded cutoffs, no cutoff equal to any position, and exceptional bits supported on j<k. Transport the actual coordinate graph to the natural canonical labels. The existing generic_exceptional_edge theorem applies with the ordinary rank list and its exact Position and Cutoff statements. It forces every exceptional bit by the displayed criterion. This theorem assumes admissibility and does not count arrays.

Theorem 1.8 (The generic exceptional criterion is sufficient as well).

$$\forall M\in \mathrm{Nat}\left(\right),\forall i\in \mathrm{Nat}\left(\right),\forall p\in \mathrm{Fin}\left(i\right)\to \mathrm{Nat}\left(\right),\forall c\in \mathrm{Fin}\left(i\right)\to \mathrm{Nat}\left(\right),\forall B\in \mathrm{Fin}\left(i\right)\to \left(\mathrm{Fin}\left(i\right)\to \mathrm{Prop}\left(\right)\right),((((((\mathrm{StrictMono}\left(p\right))\wedge (\forall j\in \mathrm{Fin}\left(i\right),p(j)\le M))\wedge (\forall j\in \mathrm{Fin}\left(i\right),c(j)\le M))\wedge (\forall j\in \mathrm{Fin}\left(i\right),\mathrm{zero}\left(\right)<p(j)))\wedge (\forall j\in \mathrm{Fin}\left(i\right),\forall k\in \mathrm{Fin}\left(i\right),\neg (c(j)=p(k))))\wedge (\forall j\in \mathrm{Fin}\left(i\right),\forall k\in \mathrm{Fin}\left(i\right),(B\left(j,k\right))\Rightarrow (j<k)))\Rightarrow ((\mathrm{Rules}\left(\mathrm{boundedCoordinateEdges}\left(M,p,c,B\right)\right))\iff (\forall j\in \mathrm{Fin}\left(i\right),\forall k\in \mathrm{Fin}\left(i\right),(B\left(j,k\right))\iff (((j<k)\wedge (c(j)<p(k)))\wedge (c(k)<p(j)))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.coordinate_generic_rules_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 forward direction uses coordinate_generic_bits. For the converse, apply the existing exists_cutoff_completion to the canonical ordinary and exceptional labels. Verify every bounded coordinate edge against that graph: ordinary clique edges, mixed cutoff incidence including rank zero, and the supplied exceptional criterion. Pullback and restriction transport both closure rules. This gives actual admissibility of the specified bits, rather than a presumed generic graph. Zero cutoffs and empty index sets remain allowed under the stated positive-position and separation hypotheses.

References

• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.CoordinateDataCarrier
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.coordinateDataFamily
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.coordinateEdgeSet
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.coordinateEdgeSet_mem_edgeFamily
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.coordinate_generic_bits
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.coordinate_generic_rules_iff
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.count_eq_coordinateDataFamily_card
• Truth anchor: D5/S3/Combinatorics/BinomialBases/MazorchukXuReconstruction.edgeFamily_eq_coordinateEdgeSet
• Dependency: D5/S3/Combinatorics/BinomialBases/MazorchukXuPatterns