Here's an example (credit: Paul Russell) of the sort of bijection you want to rule out.

Question: Find an explicit bijection $f$ between the size-$k$ and size-$k+1$ subsets of $\{1, 2, \dots, 2k+1\}$, such that $x \subset f(x)$ for all $x$.

Answer: Consider the bipartite graph with a vertex class $X$ for the size-$k$ subsets and a vertex class $Y$ for the size-$k + 1$ subsets; let edges $x, y$ denote $x \subset y$. The graph is regular, so a matching exists by Hall. Take the lexicographically first such matching (represented as a binary adjacency matrix).

If you try to rule this out by stipulating 'polynomial time' in your definition of explicit, then Russell's construction can be modified by replacing the last sentence with:

"Apply the Hopcroft-Karp algorithm to the initially empty matching"

Another attempt to rule out Russell's construction is to disallow someone from mentioning 'the set of all matchings', such as by type-theoretically restricting the answer to only mention sets of integers. But this approach doesn't work either, because finite sets can be encoded as integers.

Gowers' answer would rule this out if it could be made precise: by the time we invoke Hall, we know a matching exists. But if we didn't know about Hall's marriage theorem and avoided proving it until after applying the Hopcroft-Karp algorithm, we could 'cheat' the Gowers test. Also, a proof could be obfuscated, IOCCC-style, to hide the part that proves the existence of at least one matching.

What would rule out the Russell construction, whilst allowing the genuine explicit construction, is to stipulate that the bijection is computable with polynomial memory as a function of the description length of the individual objects being bijected: the full bipartite graph is exponential in $k$, whereas the objects (sets of integers) are expressible in $O(k \log k)$ symbols.

I'm going to suggest this definition unless anyone can provide a non-contrived example of an explicit combinatorial bijection that fails my test.

Here's an example (credit: Paul Russell) of the sort of bijection you want to rule out.

Question: Find an explicit bijection $f$ between the size-$k$ and size-$(k + 1)$ subsets of $\{1, 2, \dots, 2k+1\}$, such that $x \subset f(x)$ for all $x$.

Answer: Consider the bipartite graph with a vertex class $X$ for the size-$k$ subsets and a vertex class $Y$ for the size-$(k + 1)$ subsets; let edges $x, y$ denote $x \subset y$. The graph is regular, so a matching exists by Hall. Take the lexicographically first such matching (represented as a binary adjacency matrix).

If you try to rule this out by stipulating 'polynomial time' in your definition of explicit, then Russell's construction can be modified by replacing the last sentence with:

"Apply the Hopcroft-Karp algorithm to the initially empty matching"

Another attempt to rule out Russell's construction is to disallow someone from mentioning 'the set of all matchings', such as by type-theoretically restricting the answer to only mention sets of integers. But this approach doesn't work either, because finite sets can be encoded as integers.

Gowers' answer would rule this out if it could be made precise: by the time we invoke Hall, we know a matching exists. But if we didn't know about Hall's marriage theorem and avoided proving it until after applying the Hopcroft-Karp algorithm, we could 'cheat' the Gowers test. Also, a proof could be obfuscated, IOCCC-style, to hide the part that proves the existence of at least one matching.

What would rule out the Russell construction, whilst allowing the genuine explicit construction, is to stipulate that the bijection is computable with polynomial memory as a function of the description length of the individual objects being bijected: the full bipartite graph is exponential in $k$, whereas the objects (sets of integers) are expressible in $O(k \log k)$ symbols.

I'm going to suggest this definition unless anyone can provide a non-contrived example of an explicit combinatorial bijection that fails my test.