Exact certification has a quotient: states are equivalent when they have the same correct outputs. A tractability proxy must first define a predicate on this quotient before ordinary hardness or algorithmic questions arise. Raw syntactic proxies can fail at that earlier step, because correctness-preserving presentation moves may change the statistics they inspect while preserving the exact-certification problem. Orbit gaps are the complete obstruction. An orbit gap occurs when one closure orbit contains both positive and negative presentations of a target. Exact closure-invariant classification is possible if and only if the positive and negative orbit hulls are disjoint. When the hulls are disjoint, the closure hull is the least exact classifier. With computable orbit representatives, this hull classifier becomes a quotient-level algorithm. These are predicate-level results: they establish when a proxy defines a property of the certification problem at all, a precondition logically prior to class lower bounds on the resulting recovery task and deliberately not a substitute for them. The structural transfer applies to every fixed correctness relation, independent of whether that relation is polynomial-time accessible. In the direct finite-local regime, where local routing tests are computed from raw pairwise syntax, three binary-pairwise proxy families and one offset-normalization witness exhibit same-orbit disagreement. Positive results arise from quotient-preserving normalizations, computable orbit catalogues whose descended predicates compose under Boolean operations, and predicates defined directly on the correctness quotient. The result complements the Rice-analog line of Borchert, Stephan, Hemaspaandra, and Rothe. All numbered results are mechanized in Lean 4; the supplementary ledger maps each claim to its formal identifier.

翻译：精确验证具有一个商集：当状态产生相同正确输出时，它们被视为等价。在常规的复杂度下界或算法问题产生之前，可处理性代理必须首先在此商集上定义一个谓词。原始的句法代理可能在该前期步骤中失效，因为保正确性的表示变换可能在保持精确验证问题的同时，改变这些代理所检查的统计量。轨道间隙是这种失效的完全阻碍。当某个闭包轨道同时包含目标的正例和反例表示时，即出现轨道间隙。当且仅当正例和反例的轨道凸包不相交时，才有可能实现精确的闭包不变分类。当凸包不相交时，闭包凸包即为最简精确分类器。若轨道代表元可计算，该凸包分类器就转化为一个商集层面的算法。这些是谓词层面的结论：它们确立了代理何时能够定义验证问题的性质——这是逻辑上先于后续恢复任务类别下界的前提条件，并且有意不作为后者的替代。该结构迁移适用于任意固定的正确性关系，无论该关系是否可在多项式时间内访问。在直接的有限局部约束中，局部路由测试由原始成对句法计算得出，三个二元成对代理族和一个偏移归一化见证展现出同一轨道上的不一致性。正面结果源于保商集的归一化、可计算的轨道编目（其下降后的谓词在布尔运算下封闭），以及直接定义在正确性商集上的谓词。该结果补充了Borchert、Stephan、Hemaspaandra和Rothe提出的类比莱斯定理的研究路线。所有编号结果已在Lean 4中机械化实现；补充记录将每条声明映射至其形式化标识符。