The source's Claim: the gcd of the $p$-adic valuations is invariant under a move

IMO2026P1.gcdExp_invariant

What the statement says. For every natural number $p$, if $p$ is prime, then for all finite multisets $s$ and $t$ of natural numbers (both left implicit, to be inferred from the move hypothesis) such that there is a move from $s$ to $t$, the two natural numbers $G_p(t)$ and $G_p(s)$ are equal:

The quantity $G_p$ unfolded. For a board $u$, $G_p(u)$ is obtained by replacing each entry $x$ of $u$ by $\nu_p(x)$ — the exponent of $p$ in the prime factorization of $x$, as given by Mathlib's Nat.factorization, with the conventions $\nu_p(0)=0$, $\nu_p(1)=0$, and $\nu_p(x)=0$ for every $x$ whenever $p$ is not prime — and then folding the resulting multiset of exponents with $\gcd$, starting from $0$:

Since $\gcd$ is commutative and associative and $\gcd(0,a)=a$, the value does not depend on the order of the fold: it is the greatest common divisor of the multiset of $p$-adic exponents of the entries, where exponent-$0$ entries are neutral (they do not force the result to $0$), the empty board yields $0$, and a board all of whose entries have exponent $0$ yields $0$. Example: $G_2(\{\!\{2,3\}\!\}) = \gcd(1,0) = 1$; $G_2(\{\!\{1,1,8\}\!\}) = \gcd(0,0,3) = 3$.

The move relation is as in the other statement: there exist $m,n$ with $m>1$, $n>1$, an occurrence of $m$ in $s$ and an occurrence of $n$ in $s$ with that copy of $m$ deleted, and

1. Hypotheses, and what they exclude. There are two: $h_p$ ($p$ is prime) and $h$ (there is a move from $s$ to $t$).

• $h_p$ — the conclusion does not mention it. The conclusion mentions $p$ only as the index of the exponent function; nothing in it requires $p$ prime. This hypothesis excludes no boards: it restricts the index $p$, so for every board pair the instances $p=0$, $p=1$, $p=4$, $p=6$, $p=9$, … are outside the scope. Concretely, with $s=\{\!\{4,6\}\!\}$ and $t=\{\!\{2,12\}\!\}$, the instance $p=4$ is excluded even though both boards are otherwise in scope.
• $h$ — the conclusion does not mention it. The conclusion is a bare equality of two numbers computed from $s$ and from $t$; it refers to no move, no $m$, no $n$. This hypothesis excludes every pair of boards not related by a single move:
  • any $s$ having fewer than two occurrences of values greater than $1$ is excluded entirely (no $t$ whatsoever is in scope with it): e.g. $s = \{\!\{1,1,9\}\!\}$, $s = \{\!\{0,30\}\!\}$, $s = \{\!\{\,\}\!\}$;
  • pairs related by zero moves or by more than one move are excluded: e.g. $s = t = \{\!\{4,6\}\!\}$ is excluded, and so is the pair $s=\{\!\{4,6\}\!\}$, $t=\{\!\{1,2,6\}\!\}$ if it is not produced by one move;
  • a board that is not the exact output of a move is excluded as target: with $s = \{\!\{4,6\}\!\}$, the target $t = \{\!\{2,12\}\!\}$ is in scope while $t = \{\!\{2,12,1\}\!\}$ is not.

2. The prime, and the non-prime case. Each side computes the greatest common divisor of the $p$-adic exponents of the entries of the board in question: the left side over the entries of $t$, the right side over the entries of $s$ (with the $\gcd$-with-$0$ conventions above). When $p$ is not prime — including $p=0$ and $p=1$ — the exponent function Nat.factorization is supported on primes, so $\nu_p(x)=0$ for every entry $x$ of every board; both sides are then the greatest common divisor of a multiset of zeros, namely $0$, and the claimed equality would read $0=0$. The hypothesis $h_p$ rules this case out: the statement is asserted only for prime $p$ and says nothing whatsoever for composite $p$, for $p=1$, or for $p=0$.

3. Existence / availability of a move. Not applicable in the sense asked of the other statement: this statement has no existential conclusion. It is stated only for pairs already related by a move, and therefore says nothing about any board from which no move is possible.

4. Size. No hypothesis constrains the number of entries of $s$ or of $t$, and no size relation is asserted in the conclusion. Unfolding the move hypothesis, however, $s$ must contain at least two occurrences (an $m$, and an $n$ in the remainder), and $t$ is built by deleting two occurrences and adjoining two, so any pair in scope satisfies $|t| = |s| \ge 2$. That is a consequence of the definition, not a separate claim, and no upper bound of any kind appears.

5. Degenerate cases.

• Empty board: $G_p(\{\!\{\,\}\!\}) = 0$, but the empty board can be neither $s$ nor $t$ under the move hypothesis ($s$ needs at least two entries, and $t$ receives two adjoined entries), so it is out of scope.
• All $1$s, e.g. $\{\!\{1,1,1\}\!\}$: $G_p = \gcd(0,0,0) = 0$. Such a board admits no move, so it is out of scope as $s$; and since $m,n>1$ forces at least one of $\gcd(m,n)$, $\operatorname{lcm}(m,n)/\gcd(m,n)$ to exceed $1$, it is out of scope as $t$ as well.
• Contains $0$: not excluded — this statement has no positivity hypothesis. A $0$ entry can never be selected as $m$ or $n$ (both must exceed $1$), so it survives any move, and $\nu_p(0)=0$ makes it neutral in the $\gcd$ (a junk convention: $0$ is divisible by every power of $p$, yet the exponent returned is $0$). Concretely $s = \{\!\{0,4,6\}\!\}$ with $m=4$, $n=6$ gives $t = \{\!\{2,12,0\}\!\}$, and for $p=2$ the statement asserts $\gcd(1,2,0) = \gcd(2,1,0)$, i.e. $1 = 1$.
• Exactly one entry above $1$: as a source, e.g. $s = \{\!\{1,1,8\}\!\}$ (where $G_2 = 3$), no move exists, so it is out of scope. As a target it can occur: $s = \{\!\{2,2\}\!\}$ with $m=n=2$ gives $t = \{\!\{2,1\}\!\}$, and the statement asserts $\gcd(1,0) = \gcd(1,1)$, i.e. $1=1$.
• Hypotheses unsatisfiable: for non-prime $p$ the first hypothesis is false and the statement is vacuous at that $p$; for any $s$ with fewer than two entries exceeding $1$, or any pair not related by exactly one move, the second hypothesis is false and the statement is vacuous there. The two hypotheses are jointly satisfiable (e.g. $p=2$, $s=\{\!\{4,6\}\!\}$, $t=\{\!\{2,12\}\!\}$), so the statement is not vacuous overall.

Not asserted. The statement covers a single move only: it says nothing about reachability, about chains of moves, about terminal boards, or about invariance along a whole play. It does not assert that the common value is positive, nonzero, or bounded; does not assert anything for non-prime $p$; does not assert anything about the ordinary gcd of the entries themselves, nor about their product, sum, or cardinality; does not assert any inequality or monotonicity, only equality of two natural numbers; does not identify which entry realizes the exponent-gcd; does not claim that $m$ and $n$ are unique or determined by $s$ and $t$; does not claim a converse (that equality of these quantities implies a move); makes no use of bigPart (the exponents are taken over all entries of the board, including entries equal to $0$ or $1$), and imposes no positivity hypothesis on the entries.