The process halts: a terminal board is reachable

IMO2026P1.exists_terminal

What the statement says. For every finite multiset $s$ of natural numbers — the type Board is Multiset ℕ, so $s$ is unordered, repetitions count, and it may be empty — if every element $x$ occurring in $s$ satisfies $x > 0$, then there exists a finite multiset $t$ of natural numbers such that $t$ is reachable from $s$ and $t$ is terminal.

The two notions unfolded.

A move from a board $u$ to a board $v$ means: there exist natural numbers $m$ and $n$ with

$$m > 1,\qquad n > 1,\qquad m \in u,\qquad n \in u \setminus \{\!\{m\}\!\},$$

where $u \setminus \{\!\{m\}\!\}$ is $u$ with one occurrence of $m$ deleted, and

$$v \;=\; \{\!\{\,\gcd(m,n)\,\}\!\} \;+\; \Bigl\{\!\Bigl\{\,\tfrac{\operatorname{lcm}(m,n)}{\gcd(m,n)}\,\Bigr\}\!\Bigr\} \;+\; \bigl( u \setminus \{\!\{m\}\!\} \setminus \{\!\{n\}\!\} \bigr).$$

So $v$ is obtained by deleting one occurrence of $m$ and one occurrence of $n$ and adjoining the two numbers $\gcd(m,n)$ and $\operatorname{lcm}(m,n)/\gcd(m,n)$. The quotient is natural-number division, which truncates in general; here $m,n>1$ gives $\gcd(m,n)>0$ and $\gcd(m,n) \mid \operatorname{lcm}(m,n)$, so it is exact. The numbers $m$ and $n$ need not be different numbers: they are two different occurrences, so $m=n$ is allowed when that value occurs at least twice (e.g. $u=\{\!\{2,2\}\!\}$, $m=n=2$, giving $v=\{\!\{2,1\}\!\}$). The move relation is existential in $m,n$: for a given $u$ many different $v$ may stand in the relation.

Reachable is the reflexive–transitive closure of the move relation: $t$ is reachable from $s$ iff there is a finite chain

$$s = u_0,\; u_1,\; \dots,\; u_k = t \qquad (k \ge 0)$$

with a move from $u_i$ to $u_{i+1}$ at each step. The length $k=0$ is permitted, so every board is reachable from itself.

Terminal for a board $t$ means: there is no board $v$ with a move from $t$ to $v$. Unfolding the move relation, this says there do not exist two occurrences in $t$ (an occurrence of $m$, and an occurrence of $n$ in what remains after deleting that one) both carrying values greater than $1$ — once such $m,n$ are chosen, the resulting board always exists, so terminality is exactly the absence of such a pair.

1. Hypotheses, and what they exclude. The only hypothesis is $h_{\mathrm{pos}}: \forall x \in s,\; 0 < x$ (the board $s$ itself is a binder, not a hypothesis; there are no typeclass or implicit arguments beyond the multiset machinery).

• The conclusion does not mention it. The conclusion is "$\exists t$, $t$ is reachable from $s$ and $t$ is terminal"; positivity appears nowhere in it, neither for the entries of $s$ nor for the entries of $t$.
• Boards excluded: every board containing at least one $0$ entry. Concretely $s = \{\!\{0\}\!\}$, $s = \{\!\{0,4,6\}\!\}$, and $s = \{\!\{0,1,1\}\!\}$ are outside the statement's scope; for these the statement asserts nothing at all. Boards with no $0$ entry — including the empty board and boards of all $1$s — are all inside the scope.

3. Is it conditional on a move being available? No. Because reachability admits chains of length $0$, the board $s$ is always among the candidates for $t$. The statement asserts only that some board reachable from $s$ in zero or more moves is terminal; it never requires that a move be performed, and it does not require $t \neq s$. For a board from which no move is possible — e.g. $\{\!\{\,\}\!\}$, $\{\!\{7\}\!\}$, $\{\!\{1,1,1\}\!\}$, all of which satisfy the positivity hypothesis — the asserted existential is about the same collection of candidates, with $s$ itself both reachable in zero steps and terminal.

4. Size. No hypothesis constrains the number of entries of $s$: it may be empty, a singleton, or arbitrarily large. No relation between the sizes of $s$ and $t$ is stated. (Unfolding a move, each step deletes two occurrences and adjoins two, so every board in a chain carries the same number of entries as $s$; this follows from the definition and is not separately asserted.)

5. Degenerate cases.

• Empty board $s = \{\!\{\,\}\!\}$: the positivity hypothesis holds vacuously, so the empty board is in scope. No move exists from it.
• All $1$s, e.g. $s = \{\!\{1,1,1\}\!\}$: positivity holds ($1>0$), so it is in scope; no entry exceeds $1$, so no move exists from it.
• Contains $0$, e.g. $s = \{\!\{0,6,10\}\!\}$: excluded by the hypothesis; nothing is asserted.
• Exactly one entry above $1$, e.g. $s = \{\!\{1,1,12\}\!\}$ or $s = \{\!\{7\}\!\}$: in scope; the move relation needs an occurrence $>1$ and a second occurrence $>1$ in the remainder, so no move exists from such a board.
• Hypothesis unsatisfiable: the hypothesis is exactly "$0$ does not occur in $s$". For any board containing $0$ it is false and the implication carries no content; for every other board it is satisfied, so the statement is not vacuous overall.

Not asserted. The statement does not claim uniqueness of $t$ (it is a plain existential, not "exists a unique"); does not bound the number of moves needed; does not claim that every sequence of moves terminates, nor that the process is well-founded, nor that all terminal boards reachable from $s$ agree; says nothing about the entries of $t$ — not that they are positive, not how many exceed $1$ beyond what terminality states, not their gcd, product, sum, or relation to the entries of $s$; says nothing about the number of entries of $t$; makes no use of bigPart (the sub-multiset of entries $>1$, defined in the bundle but absent from this statement) and no use of any prime, exponent, or factorization notion; and does not assert that $s$ is or is not itself terminal.