Remarks on Primitive Regulation

We prove, and mechanize in Rocq, an abstract obstruction theorem for closure predicates $C:\mathsf{F}\mathsf{o}\mathsf{r}\mathsf{m}\to \mathsf{P}\mathsf{r}\mathsf{o}\mathsf{p}$ over the closed implication-falsity fragment $A,B::=\mathrm{\perp }\mid A\to B$. Evaluation completeness, $\mathsf{E}\mathsf{v}\mathsf{a}\mathsf{l}(C)$, says that every formula-valued behavior of codes is represented up to closure equivalence, where $A{\simeq }_{C}B$ abbreviates $C(A\to B)\wedge C(B\to A)$. For any $C$ closed under modus ponens and satisfying consistency, this completeness principle is incompatible with the internal excluded-middle schema $\mathsf{L}\mathsf{E}\mathsf{M}(C)$, namely $\mathrm{\forall }A,C(A)\vee C(\mathrm{\neg }A)$. Thus $\mathsf{E}\mathsf{v}\mathsf{a}\mathsf{l}(C),\mathsf{M}\mathsf{P}(C),\mathsf{C}\mathsf{o}\mathsf{n}\mathsf{s}(C)$, and $\mathsf{L}\mathsf{E}\mathsf{M}(C)$ cannot hold jointly. The proof uses evaluation completeness to obtain a formula $B$ such that $B{\simeq }_C\mathrm{\neg }B$. Applying $\mathsf{L}\mathsf{E}\mathsf{M}(C)$ to this $B$, either alternative gives $C(\mathrm{\perp })$ by detachment, contradicting consistency. Consequently, any Boolean decision procedure for $C$ induces the obstructed excluded-middle schema. Mere refutation behaves differently: its false branch carries no closure condition, and is therefore inhabited by the always-false classifier.