Read-back — declaration bundle (5 definitions, no theorems)

All five declarations live inside a single namespace, so their full names are qualified by it; the file contains definitions only — no lemma, no theorem, no proof obligation, and no sorry.

Board

Board is introduced as a reducible abbreviation for the type of finite multisets of natural numbers, $\mathrm{Multiset}\ \mathbb{N}$. It takes no arguments, declares no new type, and carries no invariant: a "board" is an unordered finite collection of natural numbers with multiplicities, and every natural number is allowed as an entry, including $0$ and $1$. Nothing constrains a board to be nonempty, to have a fixed cardinality, to consist of positive numbers, or to have distinct entries. Because the abbreviation is reducible, $\mathrm{Board}$ and $\mathrm{Multiset}\ \mathbb{N}$ are interchangeable everywhere below.

Move

$\mathrm{Move}$ takes two explicit arguments $s, t : \mathrm{Board}$ (no implicit or instance arguments) and returns a proposition. It asserts the existence of two natural numbers $m$ and $n$ — both existentially bound, both ranging over all of $\mathbb{N}$ — satisfying five conjoined conditions:

$$\exists\, m\, n \in \mathbb{N},\quad 1 < m \;\wedge\; 1 < n \;\wedge\; m \in s \;\wedge\; n \in (s \setminus\!\!\setminus m) \;\wedge\; t = \gcd(m,n) \,::\, \Bigl(\tfrac{\operatorname{lcm}(m,n)}{\gcd(m,n)}\Bigr) \,::\, \bigl((s \setminus\!\!\setminus m) \setminus\!\!\setminus n\bigr)$$

where $s \setminus\!\!\setminus x$ denotes multiset erasure, which removes exactly one copy of $x$ from $s$ (and returns $s$ unchanged if $x$ does not occur in $s$), and $a :: u$ denotes multiset insertion, which adds one copy of $a$ to $u$. Spelled out: $m$ is required to be strictly greater than $1$; $n$ is required to be strictly greater than $1$; $m$ is required to be a member of $s$; $n$ is required to be a member of the multiset $s$ after one copy of $m$ has been deleted; and $t$ is required to be equal, as a multiset, to the multiset obtained by deleting one copy of $m$ from $s$, then deleting one copy of $n$ from the result, and then inserting the two values $\gcd(m,n)$ and $\operatorname{lcm}(m,n) / \gcd(m,n)$. The final clause is an equation, not an inclusion or a membership: once $m$ and $n$ are fixed, $t$ is pinned down exactly, so $\mathrm{Move}\ s\ t$ holds precisely when some admissible choice of $m, n$ produces exactly the multiset $t$.

Distinctness. The two chosen numbers are not required to be distinct as values. The only separation imposed is positional: $m$ must occupy some copy in $s$, and $n$ must occupy some copy in the multiset that remains after one copy of $m$ has been removed. Concretely, if the board contains two (or more) copies of the same number $v > 1$, then $m = n = v$ is permitted, because after erasing one copy of $v$ the other copy is still present; in that case the move deletes both copies of $v$ and inserts $\gcd(v,v) = v$ together with $\operatorname{lcm}(v,v)/\gcd(v,v) = v/v = 1$, i.e. the board $\{v, v, \dots\}$ becomes $\{v, 1, \dots\}$. Conversely, if $v$ occurs exactly once in $s$, the requirement $n \in s \setminus\!\!\setminus m$ fails for $n = v$, $m = v$.

Re-use of a single position. The relation does not permit the same occurrence (position) to be used twice: the second element is drawn from $s \setminus\!\!\setminus m$, whose multiplicity of $m$ is one less than that of $s$, so a value occurring only once cannot serve as both $m$ and $n$. Two chosen values may coincide only when backed by two separate copies.

Entries not eligible. Entries equal to $0$ or $1$ can never be selected as $m$ or $n$, since $1 < 0$ and $1 < 1$ are false; such entries can only sit passively in the untouched remainder $(s \setminus\!\!\setminus m) \setminus\!\!\setminus n$.

Division. The quotient $\operatorname{lcm}(m,n)/\gcd(m,n)$ is natural-number (floor, truncating) division, the total operation that returns $0$ when the divisor is $0$. Under the hypotheses actually present, $m > 1$ forces $\gcd(m,n) \ge 1$, so no division by zero can occur here, and since $\gcd(m,n)$ divides $\operatorname{lcm}(m,n)$ the quotient is exact; the file nonetheless asserts nothing about exactness — the expression is whatever truncating division returns. Each move removes two copies and inserts two values, so cardinality is preserved by construction, but no declaration in the file states this.

Reachable

$\mathrm{Reachable}$ is defined, with no arguments written on the left-hand side, as a relation on boards: it is the reflexive–transitive closure of $\mathrm{Move}$. Thus $\mathrm{Reachable}\ s\ t$ holds exactly when there is a finite — possibly empty — chain of boards

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

with $\mathrm{Move}\ u_{i}\ u_{i+1}$ for each $0 \le i < k$. In particular $\mathrm{Reachable}\ s\ s$ holds for every board $s$, including the empty board and boards from which no move is possible, because the empty chain ($k = 0$) is allowed. The relation is directed: $\mathrm{Reachable}\ s\ t$ does not entail $\mathrm{Reachable}\ t\ s$. No bound on the length $k$ is asserted, and nothing asserts that such a chain terminates or that any particular board is reachable from any other.

IsTerminal

$\mathrm{IsTerminal}$ takes one explicit argument $s : \mathrm{Board}$ and asserts the negation of an existential over boards:

$$\neg\, \exists\, t : \mathrm{Board},\ \mathrm{Move}\ s\ t,$$

i.e. there is no board $t$ to which $s$ is related by $\mathrm{Move}$. Unfolding $\mathrm{Move}$, and using that the target $t$ is uniquely determined by the choice of $m$ and $n$ (so a witness $t$ exists as soon as an admissible pair exists), this says exactly: there do not exist $m, n \in \mathbb{N}$ with $1 < m$, $1 < n$, $m \in s$ and $n \in s \setminus\!\!\setminus m$. In terms of entries, $\mathrm{IsTerminal}\ s$ holds precisely when $s$ does not contain two distinct occurrences (counted with multiplicity) of entries exceeding $1$ — equivalently, when at most one entry of $s$ is strictly greater than $1$. Boards with zero such entries and boards with exactly one such entry are both terminal; a board with a single entry $v > 1$ repeated twice is not terminal. Entries equal to $0$ or $1$ never obstruct terminality, regardless of how many of them there are. The quantification is over all boards $t$ of type $\mathrm{Multiset}\ \mathbb{N}$; no restriction to boards of the same size or reachable boards is imposed.

bigPart

$\mathrm{bigPart}$ takes one explicit argument $s : \mathrm{Board}$ and returns a board: the sub-multiset of $s$ consisting of those entries $x$ satisfying $1 < x$, retained with their multiplicities, and with all entries equal to $0$ and $1$ discarded. The filtering predicate $x \mapsto (1 < x)$ requires a decidability instance, which is supplied automatically by the decidability of the strict order on $\mathbb{N}$; this is the declaration's only instance argument and it imposes no mathematical content. $\mathrm{bigPart}$ of the empty board is the empty board, $\mathrm{bigPart}$ of a board of all $1$s (or all $0$s, or any mixture of $0$s and $1$s) is the empty board, and $\mathrm{bigPart}$ of a singleton $\{a\}$ is $\{a\}$ if $a > 1$ and $\varnothing$ otherwise. This definition is not referenced by any other declaration in the file; in particular no connection between $\mathrm{bigPart}$ and $\mathrm{IsTerminal}$, $\mathrm{Move}$ or $\mathrm{Reachable}$ is stated anywhere.

gcdExp

$\mathrm{gcdExp}$ takes two explicit arguments, a natural number $p$ and a board $s$, and returns a natural number. It first maps every entry $x$ of $s$ to $\operatorname{ord}_p(x)$, the exponent of $p$ in the prime factorisation of $x$ (the multiplicity of $p$ in the list of prime factors of $x$), producing a multiset of natural numbers of the same cardinality as $s$; it then folds that multiset with the binary operation $\gcd$ on $\mathbb{N}$, starting from the initial value $0$:

$$\mathrm{gcdExp}(p, s) \;=\; \gcd\bigl(0,\ \operatorname{ord}_p(x_1),\ \dots,\ \operatorname{ord}_p(x_k)\bigr),\qquad s = \{x_1, \dots, x_k\}.$$

The fold is over an unordered multiset and is therefore well-defined only because $\gcd$ is commutative and associative; those two facts are supplied as typeclass instance arguments (the commutativity and associativity instances for $\gcd$ on $\mathbb{N}$) and are the declaration's only implicit/instance content.

The starting value. Since $\gcd(0, a) = a$ for every $a \in \mathbb{N}$, the seed $0$ is the identity element of $\gcd$ and therefore contributes nothing to a nonempty board; its only visible effect is to fix the value on the empty board, where $\mathrm{gcdExp}(p, \varnothing) = 0$.

An entry of valuation zero. For the same reason, an entry $x$ with $\operatorname{ord}_p(x) = 0$ does not collapse the result to $0$: taking $\gcd$ with $0$ leaves the accumulated value unchanged. The result is $0$ exactly when every entry has valuation $0$ (or the board is empty); otherwise it is the greatest common divisor of the nonzero valuations present.

Primality. The definition places no hypothesis on $p$: $p$ is an arbitrary natural number, and no assumption, typeclass or otherwise, requires $p$ to be prime. For $p = 0$, $p = 1$, or any composite $p$, the exponent $\operatorname{ord}_p(x)$ is $0$ for every $x$ (a non-prime never occurs in a list of prime factors), so $\mathrm{gcdExp}(p, s) = 0$ for every board $s$.

Degenerate entries. $\operatorname{ord}_p(0) = 0$ and $\operatorname{ord}_p(1) = 0$ by the totality of the factorisation function (the factor list of $0$ and of $1$ is empty); in particular an entry equal to $0$ is treated as having valuation $0$, not an infinite or undefined valuation, and thus leaves $\mathrm{gcdExp}$ unchanged. On a singleton board $\{a\}$ the value is $\gcd(0, \operatorname{ord}_p(a)) = \operatorname{ord}_p(a)$; on a board of all $1$s it is $0$; on the empty board it is $0$.

Degenerate cases across the file

• Empty board $\varnothing$. No $m$ can satisfy $m \in \varnothing$, so no move exists: $\mathrm{IsTerminal}\ \varnothing$ holds, $\mathrm{Reachable}\ \varnothing\ t$ holds only for $t = \varnothing$, $\mathrm{bigPart}\ \varnothing = \varnothing$, and $\mathrm{gcdExp}(p,\varnothing) = 0$ for every $p$.
• Singleton board $\{a\}$. After erasing the unique copy of $a$ nothing remains, so no second element exists and $\{a\}$ is terminal for every $a$, including $a > 1$. $\mathrm{gcdExp}(p,\{a\}) = \operatorname{ord}_p(a)$.
• Board of all $1$s (any multiplicity). $1 < 1$ is false, so no entry is eligible; the board is terminal, $\mathrm{bigPart}$ is empty, and $\mathrm{gcdExp}$ is $0$.
• An entry equal to $0$. Ineligible for selection ($1 < 0$ is false), discarded by $\mathrm{bigPart}$, and assigned valuation $0$ by $\mathrm{gcdExp}$. A board such as $\{0, 5\}$ is terminal.
• Division. The only division is $\operatorname{lcm}(m,n)/\gcd(m,n)$, in truncating natural-number division; under the standing hypothesis $1 < m$ the divisor is nonzero, and no statement in the file asserts that this division is exact or that its result is positive. Multiset erasure is likewise total and silently returns the multiset unchanged when the erased element is absent, though both erasures in $\mathrm{Move}$ occur under explicit membership hypotheses.
• Duplicate entries. Multiplicities matter throughout: membership, erasure, filtering and mapping all respect multiplicity, and two equal entries count as two occurrences for the purposes of $\mathrm{Move}$ and $\mathrm{IsTerminal}$.

What is NOT asserted anywhere in this file

• No theorem of any kind. The file contains only definitions and an abbreviation; it proves nothing, states no lemma, and contains no proof or sorry.
• Nothing asserts that $p$ is prime, or that $\mathrm{gcdExp}$ has any relationship to $\mathrm{Move}$, $\mathrm{Reachable}$, $\mathrm{IsTerminal}$ or $\mathrm{bigPart}$ — in particular no invariance of $\mathrm{gcdExp}$ under a move is claimed.
• Nothing asserts that $\mathrm{bigPart}$ is related to terminality, to the number of eligible entries, or to anything else; it is defined and never used.
• Nothing asserts that $\mathrm{Move}$ preserves cardinality, the product of the entries, the multiset of prime factorisations, or any other quantity.
• Nothing asserts that $\gcd(m,n)$ divides $\operatorname{lcm}(m,n)$, that the displayed quotient is exact, or that the two inserted values are positive, distinct, or different from $m$ and $n$.
• Nothing asserts termination: there is no claim that iterating $\mathrm{Move}$ halts, that a terminal board is reachable from every board, that the process is well-founded, or that any decreasing measure exists.
• Nothing asserts confluence, determinism, or uniqueness of the terminal board reachable from a given board; $\mathrm{Move}$ is a relation and may relate one board to many.
• Nothing asserts that $\mathrm{Reachable}$ is symmetric or an equivalence, nor any bound on the number of steps.
• Nothing constrains a board to be nonempty, finite in a bounded sense, free of $0$s and $1$s, of fixed cardinality, or with distinct entries.
• No characterisation of $\mathrm{IsTerminal}$ in terms of counting entries greater than $1$ is stated as a lemma; that reading is obtained by unfolding the definition, not by an asserted equivalence.
• No existence claim is made: nothing states that any board admits a move, or that any board is terminal.