OAI/Combinatorics/ProgressionColoring/ComparisonOutputs.lean

Exact finite output families determined by affine comparisons

The output type may be infinite, for example an integer-valued floor word. One representative is selected for each realized ternary sign vector. The factorization hypothesis then proves that this finite image is exactly the actual output image on the specified parameter domain. This proves finiteness and a cardinality bound without assuming either conclusion about the outputs.