finite_not_onto_infinite
plain-language theorem explainer
A function from a finite domain to an infinite codomain cannot be surjective. This supplies the elementary finite-capacity veto used in Pinch Algebra arguments that bound the number of operations under positive cost and finite budget. The term proof assumes surjectivity, invokes preservation of finiteness under surjective images, and obtains an immediate contradiction with the infinitude hypothesis.
Claim. If $A$ is finite and $B$ is infinite, then no function $f:A→B$ is surjective.
background
Pinch Algebra (F5) develops mutual divisibility in unique factorization domains together with Fredholm-type obstructions. The local setting treats finite budgets and positive per-operation costs as limiting the total number of admissible operations, with the present result supplying the underlying set-theoretic obstruction. Upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the non-negative J-cost that turns the veto into a concrete bound on operation count.
proof idea
The term proof opens by assuming surjectivity. It then applies the standard preservation lemma that the surjective image of a finite set remains finite, yielding that the codomain is finite. This directly negates the infinitude hypothesis via the negation of finiteness.
why it matters
The declaration occupies the F5.3.2 slot and supplies the simplest form of the finite-capacity veto. It is cited by the BSD primary development and the Yang-Mills secondary construction, both of which rely on finite resources preventing coverage of infinite possibility spaces. The result closes the elementary step that links positive cost plus finite budget to only finitely many operations being admissible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.