MATH.6:8 - Common Anti-Patterns and How to Avoid Them
Put the desired conclusion among the assumptions. This excludes countermodels by construction. Keep the conclusion outside the retained assumptions, and inspect an unexpected empty search.
Use a failing case outside the stated domain. The infinite shift in :5.2 refutes the unrestricted self-map claim while the finite claim remains true. Carry the actual domain into the returned conclusion.
Keep one witness while reversing quantifier order. The witness in :5.3 depends on the input. Preserve that dependence, or establish a uniform witness as a different result.
Treat a search limit as the theorem’s limit. Recover which mathematical cases were represented. Change the construction or retain the bounded result when the desired claim reaches beyond them.