Ideal membership in $MvPolynomial (Fin k) ℚ$ is decidable in the propositional sense: there is a $Bool$-valued function $dec$ with $dec p = true$ exactly when $p$ lies in the ideal generated by $gens$. The proof is classical — excluded middle supplies the characteristic function $if p ∈ span ↑gens then true else false$ — and not the constructive Gröbner-basis decision procedure (Buchberger's algorithm), which mathlib does not yet provide and which is out of scope for this submission. This statement is the propositional shadow of the paper's effective-decidability claim; the three automaton equality theorems reduce to it via the ideal-chain argument.