Mfcttrf

This is a very abstract question, I hope this is appropriate.

Suppose $T$ is some claim over some infinite set $A$, for example, let $A$ be the set of all loopless planar graphs, and $T$ be the claim "for every element $a in A$, the chromatic number of $a$'s dual graph is $leq 4$" (this is known as "Four-color Theorem"); or, let $A = mathbbN$, and $T$ be the claim "there are no 3 elements $x, y, z in A$ such that $x^5 + y^5 =z^5$" (a specific case of Fermat's last theorem).

In the first example, it is possible to prove the claim $T$ by testing some claim $T'$ over finite set $A' subset A$, see proof by computer section. This is done by a series of reductions, showing that if all the elements in some finite set satisfy a property, then the (original) claim holds.

In some sense, mathematical induction is similar: we test a claim on finite set ("the base case"), then proving $a_n rightarrow a_n+1$, which shows the claim is correct for all space.

Are there more known cases like that? i.e. proving (a combinatorial) claim by reduction to finite cases?

In 1972, I have developed a general theory of isometric embeddings of finite metric spaces into finite-dimensional Banach spaces, in particular, the injective case, i.e. into metrically injective spaces $ mathbb R^n $ with metrics given by $ max.$ An announcement has appeared a couple of years later in AMS Notices. One of the theorems fits the present thread:

For every natural $ k n $ there is an EXPLICIT natural constant $ mu(k n) $ such that the following two statements are equivalent:

(i) every $k$-element metric space can be isometrically embedded
into $ mathbb R^n$ with the distance given by $ max;$

(ii) every $k$-element metric space with integer distances, and of diameter
$ le mu(k n), $ can be isometrically embedded into subspace
$, 0 ldots mu(k n)^n $ of $ mathbb R^n$ with the distance
given by $ max$.

For each natural $ n $ there exists a maximal $ u(n)=k $ as above; and also
$ U(n) $ similar to $ u(n) $ but for ALL $ n$-dimensional Banach spaces TOGETHER (for each fixed dimension $ n. $) Then in the non-trivial case of $ nge 2 $ we get

$$ n+2 le u(n) le U(n) le biglceilfrac3cdot n2bigrceil + 1 $$

We see from (i)+(ii) that finding $ u(n) $ got reduced to a finite computation.

It is very common, when finding solutions to Diophantine equations, to use Baker's method of linear forms in logarithms to reduce the problem to a finite computation (that is, to find an upper bound for the solutions).

For the sake of completeness, let me mention the direction which is opposite to the OP's Question.

There are combinatorial optimizations problems which deal with a finite (but large) input set at the start, and the point is to optimize a real function over the input. Such problems are often messy.

Then, some time ago, Hungarian mathematicians started to embed the input set into a Euclidean n-space, and they'd extend the said function to a linear or convex function over the convex hull of the input. Since the optimum over the whole hull is reached at a vertex then... etc.

We see that sometimes situations which are strictly finite (looking for an exact answer) get hm-reduced to infinite situations.