Paper deep dive
Toward a Tractability Frontier for Exact Relevance Certification
Tristan Simas
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 94%
Last extracted: 4/10/2026, 4:03:13 AM
Summary
The paper investigates the tractability of exact relevance certification in coordinate-structured decision problems. It establishes a meta-impossibility theorem, proving that no efficiently checkable, closure-law-invariant classifier can provide an exact characterization of tractability across four identified obstruction families (dominant-pair concentration, margin masking, ghost-action concentration, and additive/statewise offset concentration). The authors define a finite primitive basis for current tractable families and demonstrate that while quotient-based structural classification is a natural approach, it is fundamentally limited by the existence of same-orbit disagreements.
Entities (7)
Relation Signals (2)
Dominant-pair concentration → preventstractabilityclassification → Exact Relevance Certification
confidence 95% · no correct tractability classifier on a closure-closed domain yields an exact characterization over these families
Exact Relevance Certification → isconstrainedby → Optimizer-Quotient Framework
confidence 90% · exact certification, sufficiency, certification statistics, and zero-distortion summaries all factor through the optimizer quotient
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Exact relevance certification asks which coordinates are necessary to determine the optimal action in a coordinate-structured decision problem. The tractable families treated here admit a finite primitive basis, but optimizer-quotient realizability is maximal, so quotient shape alone cannot characterize the frontier. We prove a meta-impossibility theorem for efficiently checkable structural predicates invariant under the theorem-forced closure laws of exact certification. Structural convergence with zero-distortion summaries, quotient entropy bounds, and support-counting arguments explains why those closure laws are canonical. We establish the theorem by constructing same-orbit disagreements for four obstruction families, namely dominant-pair concentration, margin masking, ghost-action concentration, and additive/statewise offset concentration, using action-independent, pair-targeted affine witnesses. Consequently no correct tractability classifier on a closure-closed domain yields an exact characterization over these families. Here closure-orbit agreement is forced by correctness rather than assumed as an invariance axiom. The result therefore applies to correct classifiers on closure-closed domains, not only to classifiers presented through a designated admissibility package.
Tags
Links
- Source: https://arxiv.org/abs/2604.07349v1
- Canonical: https://arxiv.org/abs/2604.07349v1
Trouble viewing inline? Open PDF directly →
Full Text
92,727 characters extracted from source content.
Expand or collapse full text
Toward a Tractability Frontier for Exact Relevance Certification Tristan Simas McGill University tristan.simas@mail.mcgill.ca April 9, 2026 Abstract Exact relevance certification asks which coordinates are necessary to determine the optimal action in a coordinate-structured decision problem. The tractable families treated here admit a finite primitive basis, but optimizer-quotient realizability is maximal, so quotient shape alone cannot characterize the frontier. We prove a meta-impossibility theorem for efficiently checkable structural predicates in- variant under the theorem-forced closure laws of exact certification. Structural convergence with zero-distortion summaries, quotient entropy bounds, and support-counting arguments ex- plains why those closure laws are canonical. We establish the theorem by constructing same- orbit disagreements for four obstruction families, namely dominant-pair concentration, margin masking, ghost-action concentration, and additive/statewise offset concentration, using action- independent, pair-targeted affine witnesses. Consequently no correct tractability classifier on a closure-closed domain yields an exact characterization over these families. Here closure-orbit agreement is forced by correctness rather than assumed as an invariance axiom. The result therefore applies to correct classifiers on closure-closed domains, not only to classifiers presented through a designated admissibility package. 1 Introduction Exact relevance certification asks: given a coordinate-structured decision problem, which coor- dinates are necessary to determine the optimal action set? Under succinct encodings the ambient problem is hard, coNP-complete in static settings and PSPACE-complete in sequential settings [29], so any tractability statement must be genuinely structural. The optimizer-quotient framework of [29] isolates the semantic object on which exact certification depends, and identifies it categorically as the coimage of Opt in Set. We show independently in Section 6 that this object is canonical for the certification problem itself: exact certification, sufficiency, certification statistics, and zero-distortion summaries all factor through the optimizer quotient (Proposition 6.1, Corollary 6.2, Corollary 6.4, and Proposition 6.5), and the closure laws used in this paper’s no-go theorem are forced by that factoring. The categorical route [29] and the operational route of Section 6 therefore agree on the same object, so canonicity is established by two independent arguments. This paper asks whether that canonical object admits a finite structural tractability classifier at the representation level. The orbit-gap contradiction depends only on closure-law invariance (Theorem 4.9), and closure- law invariance is itself forced by correctness (Theorem 6.17). Closure-equivalent representations encode the same certification problem, so a correct tractability classifier must assign them the same verdict. The no-go therefore applies to any correct classifier on a closure-closed domain containing the obstruction families, regardless of whether the underlying procedure tracks closure-invariant 1 arXiv:2604.07349v1 [cs.C] 8 Apr 2026 features internally. The specific admissibility package of Definition 6.16 is one natural instantiation, but the package itself is not load-bearing. On the positive side, we prove that the tractable families treated here split into three roles: primitive core mechanisms, regime lifts, and degenerate collapses. This yields a finite primitive basis. On its own, however, this does not establish a frontier theorem: finite inventory is not finite characterization. The natural next move is to classify by optimizer-induced quotient structure. We show this is impossible in the unconstrained sense: optimizer realizability is maximal, and arbitrary labeling kernels are realizable. Thus quotient shape is too expressive to carry the boundary by itself. Exactness is not arbitrary. At zero distortion, any summary that preserves optimal actions must still separate distinct optimizer classes: if two different optimizer classes were assigned the same summary value, the summary would merge states with different optimal-action sets and would cease to be lossless. Exact relevance therefore marks the theoretical floor for lossless abstraction. One may study approximate summaries for other purposes, but once the goal is exact decision preservation, the optimizer quotient is already the unavoidable reference object. The realizability barrier motivates the organizing principle of the paper: tractability predicates must be evaluated on representation-level structural classes, but modulo theorem-forced equivalences of presentation. In particular, closure under relabelings, positive affine utility reparameterizations, duplication, and binary irrelevant-coordinate extension is not a modeling preference; it is inherited from the fact that exact certification depends only on the induced decision quotient relation. Standing Semantics For a decision problem with state space S, action space A, and utility U, write Opt(s) =a∈ A : U (a,s) is maximal among all actions at s. This induces the decision-equivalence relation s∼ Opt s ′ ⇐⇒ Opt(s) = Opt(s ′ ). The associated optimizer quotient is the quotient set S/∼ Opt . A coordinate set I is sufficient when agreement on I forces equality of optimizer classes, and a coordinate is relevant when deleting it destroys sufficiency. These are the semantic objects studied throughout the paper; later closure laws and obstruction families are all phrased relative to this quotient viewpoint. At the same time, unrestricted predicates trivialize any impossibility theorem via oracle encod- ing. We therefore isolate an admissibility layer: polynomial-time checkability, structural extractabil- ity, closure-law invariance, and bounded-pattern definability. This class excludes direct semantic encoding while still covering the structural results established here. The proof-load-bearing clause is closure-law invariance (Theorem 4.9); the remaining clauses act as guardrails that keep the search space structural rather than oracle-like. Within this admissibility class, we prove a four-family no-go template. For each obstruction fam- ily we construct two slices with different obstruction status in the same closure orbit. The key mech- anism is an action-independent, pair-targeted additive affine term (the statewise “α-component” of positive affine transport), which changes the obstruction predicate while preserving closure equiv- alence. Closure-law invariance then transports any candidate predicate across the orbit and forces contradiction. The dominant-pair family is the canonical instance, and the same mechanism now applies to mar- gin masking, ghost-action concentration, and additive/statewise offset concentration. The resulting 2 theorem depends only on closure-soundness: any package of candidate classifiers whose members are closure-law invariant inherits the same impossibility, while the other admissibility clauses serve as guardrails. Conceptually, the result belongs to the same impossibility lineage as Rice-style and Arrow-style theorems: once one fixes a natural invariance package and a nontrivial expressivity domain, the desired classifier does not exist. The open problem is to identify a stronger structural principle, if one exists, that yields a correct frontier theorem. An accompanying Lean development mechanically verifies the realizability constructions, the generic orbit-gap argument, and the family-level admissible no-go theorems used in the collapse argument; the archived artifact is available at https://doi.org/10.5281/zenodo.19457896. 2 Finite Basis for the Current Positive Landscape We distinguish between tractable families treated here and primitive tractability mechanisms. A tractable family is any named positive condition included in the present analysis. A primitive mechanism is a smaller conceptual source of tractability that may explain several families at once. The positive theory organizes into three roles: six core structural families, four regime lifts, and five degenerate collapses. Projecting those families to primitive mechanisms leaves eight sources of tractability: the six core subcases together with constant-optimizer collapse and finite explicit enumeration. Theorem 2.1 1 (Explicit Partition of the Current Positive Landscape). The fifteen tractable families considered here admit an explicit disjoint partition into three blocks: 1. six core structural families, 2. four lifted families that reduce to existing core subcases, and 3. five degenerate families that become tractable by optimizer collapse or finite explicit enumer- ation. Moreover, each family is classified into exactly one of these three blocks by an explicit classification map. Proposition 2.2 2 (Explicit Inventory). The fifteen tractable families considered here are exactly the following: 1. core: bounded actions, separable utility, low tensor rank, tree structure, bounded treewidth, coordinate symmetry; 2. lifts: product distribution, bounded support, bounded horizon, full observability; 3. degenerate: single action, bounded state space, strict global dominance, constant optimal set, multiplicative-separable constant-sign. Corollary 2.3 3 (Finite Basis for the Current Positive Landscape). Projecting the partition of Theo- rem 2.1 to primitive mechanisms yields an explicit finite list of eight primitive tractability mecha- nisms. The list consists of the six core structural subcases bounded actions, separable utility, low tensor rank, tree structure, bounded treewidth, coordinate symmetry, together with two degenerate mechanisms: constant-optimizer collapse andfinite explicit enumeration. 1 Lean: FR1-2 2 : FR25-28 3 : FR3 3 Proposition 2.4 4 (Explicit Primitive Basis). The current primitive basis consists exactly of bounded actions, separable utility, low tensor rank, tree structure, bounded treewidth, coordinate symmetry, constant-optimizer collapse, and finite explicit enumeration. The current positive landscape therefore contains fifteen tractable families accounted for by eight primitive mechanisms. Proposition 2.5 5 (All Independent Core Mechanisms Are Nondegenerate). The analysis already con- tains witness families showing that five core mechanisms are individually indispensable in the sense of basis coverage: 1. a low-rank-only witness family, 2. a separable-only witness family, 3. a bounded-actions-only witness family, 4. a bounded-treewidth-only witness family, and 5. a symmetry-only witness family. Each of these families remains tractable by its designated mechanism while failing the corresponding versions of the other independent core mechanisms. Proposition 2.5 settles the independent part of the basis question on the present surface. Every core mechanism that is not merely contained in another is shown to be genuinely needed. Concretely, the present theory contains five kinds of “only-by” witness: low-rank only, separable only, bounded-actions only, bounded-treewidth only, and symmetry only. Proposition 2.6 6 (Weak Tree Ordering Does Not Imply Width One). There exists a dependency presentation satisfying the older monotone tree-order predicate TreeStructured whose dependency graph has real treewidth greater than one. Width-one containment requires the stricter parent-tree condition from Proposition 2.8, not merely monotone ordering. Proposition 2.7 7 (Cyclic Dependencies Recover Hardness). The reduction family for exact relevance certification yields coNP-hard instances with cyclic dependency structure. Thus the tree-structured regime is not only sufficient for tractability; leaving it also reaches the hard side. Proposition 2.8 8 (Parent-Tree Structure Gives Width-One Decompositions). Suppose a dependency presentation is tree-structured in the strict parent sense: every dependency points to a smaller coordinate and every coordinate has at most one parent. Then the induced dependency graph admits a genuine tree decomposition of width at most one. Proposition 2.8 is the containment theorem behind the intended “tree structure is the treewidth- one special case” slogan. It distinguishes this parent-tree notion from the weaker monotone-order predicate currently named TreeStructured. Proposition 2.9 9 (Current Positive Interfaces Factor Through Role Classification). The current posi- tive theorem surface factors through the role classifier of Theorem 2.1. Concretely, the family-indexed interfaces for 1. subcase-facing tractability, 2. degenerate-case witnesses, and 3. complexity-class summaries 4 : FR29 5 : FR101, FR105-106, FR108, FR112-113 6 : FR114 7 : FR115 8 : FR100, FR110-111 9 : FR4 4 all factor through the map family7−→ role∈core, lifted, degenerate. Proposition 2.9 shows that the exported positive API is already controlled by the role partition rather than by fifteen unrelated theorem schemas. 3 Lifts and Degeneracies The extra named families beyond the six core subcases split naturally into two groups. Regime Lifts Four stochastic/sequential positive results do not introduce new primitive mechanisms. They reduce directly to existing core subcases: 1. product distributions reduce to separable utility; 2. bounded support reduces to bounded actions; 3. bounded horizons reduce to bounded treewidth; 4. full observability reduces to tree structure. These are mathematically useful because they transfer the static tractable theory into richer regimes. But they do not enlarge the primitive basis. They are best understood as lifts, not new frontier points. Proposition 3.1 10 (Lifted Cases Introduce No New Primitive). Each stochastic/sequential tractable case considered here is classified into one of the six core structural subcases. In particular, these positive results do not enlarge the primitive basis from Corollary 2.3. Degenerate Cases The remaining positive cases considered here are degenerate in a precise sense. Single-action systems, strict global dominance, constant optimal-set systems, and multiplicative- separable constant-sign models all collapse the optimizer so strongly that the relevant-coordinate question disappears: the optimal-action set is constant across states, so the empty coordinate set is sufficient. These are not new structural tractability mechanisms for the relevance problem; they are constant-optimizer collapses. Bounded state space behaves differently. It does not force a constant optimizer. Instead, it makes exact certification feasible by brute-force enumeration over a finite universe. This is polynomial only because the instance family already carries a hard external bound on its search space. Proposition 3.2 11 (Degenerate Positive Cases). Every non-core tractable case considered here that is not a regime lift belongs to one of two degenerate buckets: 1. constant-optimizer collapse, or 2. finite explicit enumeration. Taken together with Proposition 3.1, Proposition 3.2 sharpens Theorem 2.1: every positive result considered here is exactly one of three things, a primitive core case, a lift, or a degenerate collapse. 10 : FR5 11 : FR1, FR6 5 4 Toward the Frontier Theorem Sections 2 and 3 motivate a frontier question. Do the tractable families already suggest a finite optimizer-compatible criterion? In the strongest form, could exact relevance certification admit a representation-sensitive dichotomy theorem analogous to the classical dichotomy programs for satisfiability and constraint satisfaction? The most direct version of that program fails. Quotient shape is too expressive, and later in the section even structurally restricted finite classifiers fail on a theorem-forced surface. Any future frontier theorem must therefore avoid both sources of failure. Three obstacles remain. Realizability is not the bottleneck: Theorem 5.1 shows that arbitrary labeling kernels already arise as optimizer quotients, so no frontier theorem can be driven by quotient realizability alone. Even on the positive side one must separate primitive mechanisms from lifts and degeneracies; otherwise a finite inventory confuses genuine sources of tractability with derived or collapsed cases. And although the long-term target remains an algebraic description analogous to the CSP dichotomy program, the negative results below show that no direct optimizer-compatible classifier can play that role. A Stabilized Binary Pairwise Subregime One piece of the frontier program already admits a clean canonical theorem. On binary coordinate domains, define the mixed difference along coordinates i,j for action a by evaluating the utility on the four assignments (0, 0), (1, 1), (0, 1), (1, 0) while holding all other coordinates fixed at 0. For pairwise utilities, this mixed difference is the canonical witness of genuine pair interaction. Proposition 4.1 12 (Binary Pairwise Symmetry Dichotomy). Let the coordinate alphabet be binary. If a utility admits a pairwise decomposition and is invariant under coordinate permutations, then either: 1. it admits a unary-coordinate decomposition, so every pairwise term collapses into single- coordinate contributions, or 2. every distinct coordinate pair carries a genuine pair interaction, witnessed by a nonzero mixed difference for some action. Within the binary pairwise-symmetric regime, there is no intermediate sparse interaction pattern hiding between unary collapse and the complete-pair case. Once a single nonzero pair witness exists, symmetry propagates it to every coordinate pair. This removes one plausible source of additional primitive mechanisms from the frontier search. The optimizer-relevant version needs one extra layer. Raw pair interaction is still too coarse, be- cause action-independent pairwise terms can be structurally dense without changing the optimizer. The correct invariant is the mixed difference of action gaps U (a,·)− U (b,·). Proposition 4.2 13 (Decision-Relevant Binary Pairwise Dichotomy). In the same binary pairwise- symmetric regime, either all action-dependent pair effects collapse into a unary-coordinate reduction after removing an action-independent base state term, or every distinct coordinate pair is decision- relevantly interacting for some action gap. A coarse hardness heuristic therefore fails. The obstruction theorem shows that even complete genuine pair interaction and failure of coordinate symmetry do not force hardness by themselves: one can still have a constant optimizer. Any eventual frontier theorem must therefore quotient out optimizer-degenerate phenomena, not just declared or utility-level interaction density. 14 12 : FR118-120 13 : FR121-124 14 : FR124 6 The obstruction is stronger than that first formulation suggests. Action-specific utility offsets leave the decision-relevant interaction graph unchanged, yet they can turn a family with nonconstant optimizer behavior into one with a constant optimizer while preserving dense decision-relevant structure. Any true hardness theorem in this regime must therefore normalize away action offsets explicitly, not merely require dense decision-relevant interaction. 15 Identify utilities up to action-dependent, state-independent offsets, and the offset-normalized decision-relevant graph becomes well-defined on those equivalence classes. But the resulting di- chotomy attempt still fails. The offset-normalized obstruction theorem shows that even after pass- ing to offset classes, one can retain complete decision-relevant interaction and unbounded treewidth while exact certification remains trivial. 16 The next refinement is to restrict the interaction graph to optimizer-supported actions. This removes two earlier collapse mechanisms: the offset-collapse family and a ghost-action family whose all-action decision-relevant graph is complete even though a single coordinate remains sufficient. But even that support-filtered graph is not enough. The optimizer-supported obstruction theorem exhibits a margin-masking family with complete optimizer-supported decision-relevant interaction and unbounded treewidth, yet the optimizer still depends only on coordinate 0. The third collapse mechanism is therefore not ghost support or offset collapse, but large unary margins that mask dense supported pairwise interactions. 17 One might hope that a strict unary-to-pair margin bound rescues the dichotomy. Define margin- bounded pairwise utilities by requiring every unary term to be at most twice the largest binary mixed-difference magnitude. This still fails. The dominant-pair family is margin-bounded because its unary terms vanish, while its optimizer-supported decision-relevant graph remains complete. Yet the obstruction theorem shows that exact certification is still controlled by the two-coordinate set 0, 1. The fourth collapse mechanism is therefore pair-weight concentration rather than unary masking: one supported pair dominates the optimizer while the remaining dense interactions are too weak to matter. 18 Admissible Closure-Orbit No-Go Program The obstruction families above lead to a uniform negative statement because they admit explicit disagreements inside a single closure orbit. Proposition 4.3 19 (Orbit-Gap Template). Let Q be a slice predicate. Suppose there exist slices U,V such that U and V lie in the same closure orbit, Q(U ) holds, and Q(V ) fails. Then no closure-law- invariant predicate P can satisfy P (W ) ⇐⇒ Q(W ) for all slices W. Proof idea. Closure-law invariance gives P (U ) ⇐⇒ P (V ). Exact agreement with Q would then imply Q(U ) ⇐⇒ Q(V ), contradicting the assumed orbit gap.■ For each obstruction family, the argument constructs two same-orbit slices with different ob- struction status. In all four cases the witness is a positive-affine step whose α-component is an action-independent state term supported on a single coordinate pair. Pure relabeling cannot change the relevant obstruction statistics, and a global scale factor preserves all pairwise magnitudes up to common rescaling. The statewise additive term is what allows one to move mass onto a chosen pair while remaining inside the theorem-forced closure laws. The fact that the same mechanism works for four structurally different obstruction families is strong evidence that the collapse theorem captures a genuine phenomenon rather than a collection of unrelated counterexamples. 15 : FR125-127 16 : FR128-129 17 : FR130-136 18 : FR137-140 19 : FR185 7 There is also a transport interpretation of these witnesses. Once transport is computed on optimizer-quotient classes, a singleton quotient admits zero-cost diagonal transport, whereas genuine branching forces positive off-diagonal transport when distinct classes carry mass. The pair-targeted affine witnesses exploit exactly this sensitivity. They do not introduce arbitrary perturbations unre- lated to the decision geometry; rather, they move mass across a selected branch of the quotient while staying inside the same closure orbit. The affine witnesses therefore track the intrinsic transport geometry of the quotient instead of functioning as purely syntactic tricks. 20 Theorem 4.4 21 (Dominant-Pair Admissible No-Go). No admissible normalization predicate can de- cide the dominant-pair obstruction family exactly. Proof sketch. The target predicate is unique dominant-pair status: one pair/action realizes the maximal interaction magnitude and that maximizer is unique. Start from a slice whose unique dominant pair is 0, 1. Add an action-independent affine state term supported on a different pair, say 1, 2. This produces a slice in the same closure orbit but with a different unique dominant pair. Proposition 4.3 then rules out every closure-law-invariant classifier, hence every admissible one.■ Theorem 4.4 gives the first instance. The remaining three families use the same orbit-gap scheme, but each isolates a different structural obstruction. Theorem 4.5 22 (Margin-Masking Admissible No-Go). No admissible normalization predicate can decide margin-boundedness exactly. Proof sketch. For margin masking, the target predicate is margin-boundedness itself. This family is structurally different from the dominant-pair family because it is governed by a threshold comparing unary mass against the largest pair interaction. The affine witness leaves unary terms unchanged but raises the largest pair interaction past the relevant threshold, so the translated slice becomes margin-bounded while the base slice is not. Proposition 4.3 therefore rules out every closure-law- invariant classifier, hence every admissible one.■ Theorem 4.6 23 (Ghost-Action Admissible No-Go). No admissible normalization predicate can decide the ghost-action concentration signature exactly. Proof sketch. For ghost actions, the target predicate says that there is an action whose unary contribution on the first coordinate is −1 on both binary values and whose anchor-pair interaction has unit mixed-difference magnitude. This family is local in appearance but unstable under the same pair-targeted affine move. A pair-supported affine term preserves the closure orbit while destroying the signature, so Proposition 4.3 applies.■ Theorem 4.7 24 (Offset Admissible No-Go). No admissible normalization predicate can decide the additive/statewise offset signature exactly. Proof sketch. For additive/statewise offset concentration, the target predicate requires two actions with distinct anchor-pair interaction magnitudes, namely 1 and 0. This family isolates the action- specific mismatch that survives after earlier offset normalizations. A pair-supported affine term changes the anchor-pair statistics while remaining in the same closure orbit. Again, Proposition 4.3 yields the contradiction.■ Theorem 4.8 25 (Admissible Collapse Across the Four Obstruction Families). Let P be a normaliza- tion predicate satisfying the admissibility axioms. Then P is not a tractability characterization. 20 : FR183-184 21 : FR186 22 : FR187 23 : FR188 24 : FR189 25 : FR190 8 Proof idea. If P were an admissible tractability characterization, it would have to decide each of the four obstruction predicates above. Theorem 4.4, Theorem 4.5, Theorem 4.6, and Theorem 4.7 show that this is impossible. Hence no admissible normalization predicate yields the desired frontier theorem.■ The four obstruction families are witnesses for the orbit-gap template (Proposition 4.3), not the scope of Theorem 4.8. The theorem ranges over the entire admissibility class. Four structurally distinct families are included because the same pair-targeted affine transport defeats classifiers across families that share no surface structure, and Proposition 4.12 shows that orbit gaps are the complete obstruction criterion for exact classification by closure-law-invariant predicates. The four families are therefore theorem-backed witnesses of a complete mechanism rather than an ad hoc list. Abstractly, let Γ be a class of slice predicates, and call a predicate Γ-admissible when it be- longs to Γ. Call Γ closure-sound if every Γ-admissible predicate is closure-law invariant. Call Γ a reasonable guardrail package if it is closure-sound and also imposes auxiliary restrictions such as efficient checkability, structural extractability, and bounded-pattern definability. The proof below uses only closure-soundness; the remaining clauses explain which non-oracular search spaces the no-go is meant to cover. 26 Theorem 4.9 27 (Closure-Sound Package No-Go). Let Γ be any class of slice predicates such that every Γ-admissible predicate is closure-law invariant. Then no Γ-admissible predicate can simulta- neously characterize the four obstruction families. In particular, the no-go theorem depends only on closure-law invariance; the remaining clauses of Definition 6.16 justify the admissibility package as a meaningful notion but do not enter the contradiction. Proof sketch. Closure-law invariance suffices to invoke Proposition 4.3 against each of the four ob- struction families. The same orbit-gap proofs underlying Theorem 4.4, Theorem 4.5, Theorem 4.6, and Theorem 4.7 then yield the contradiction directly. Any one of the four families independently witnesses the collapse; we state all four to make explicit that the obstruction is robust across struc- turally distinct witnesses.■ Theorem 4.9 is the load-bearing form of Theorem 4.8. Any reasonable formalization of admissi- bility, whether the specific package of Definition 6.16 or any alternative whose admissible predicates are closure-law invariant, inherits the impossibility conclusion. Proposition 6.1 identifies closure-law invariance as the semantic core, and Theorem 6.17 shows that exact correctness forces the same invariance on any tractability classifier. The admissibility package is one natural instantiation; the theorem is robust to its replacement. Corollary 4.10 28 (Reasonable Guardrail Packages). The same conclusion holds for every reasonable guardrail package. In particular, efficient checkability, structural extractability, bounded-pattern de- finability, and the informal exclusion of oracle encodings are guardrails rather than proof-load-bearing hypotheses. Proof. Immediate from Theorem 4.9, since only the closure-soundness clause is used.■ Corollary 4.11 (No Correct Tractability Classifier). Let C be any correct tractability classifier on a domain that is closed under the closure laws and contains the four obstruction families. Then C cannot yield an exact tractability characterization across those families. In particular, no procedure assigning verdicts to representations can correctly predict tractability across the four obstruction families, regardless of whether the procedure tracks closure-invariant features internally. 26 : FR191-192 27 : FR193 28 : FR194 9 Proof. By Theorem 6.17, any such classifier must agree on closure orbits and is therefore closure- law invariant on its domain. Theorem 4.9 then rules out exact characterization across the four obstruction families.■ Corollary 4.11 is the universal-scope form of the no-go. Theorem 4.9 isolates closure-law invari- ance as the load-bearing hypothesis, and Theorem 6.17 removes even that as an explicit assumption by forcing the same invariance from correctness itself. Proposition 4.12 (Orbit-Gap Completeness for Exact Classification). For any slice predicate Q, the following are equivalent: 1. there exists a closure-law-invariant predicate P such that P (S) ⇐⇒ Q(S) for every slice S; 2. Q is itself closure-law invariant; 3. Q is constant on closure orbits. Equivalently, exact classification of Q by closure-law-invariant predicates fails if and only if Q admits an orbit-gap witness: two closure-equivalent slices with different Q-status. Proof sketch. The implication (1) ⇒ (2) transfers closure-law invariance across exact equivalence. The implication (2) ⇒ (3) says exactly that a closure-law-invariant predicate cannot change value inside a closure orbit. For (3)⇒ (2), every primitive closure-law step is already a closure equivalence, so orbit constancy supplies the six invariance clauses. The final equivalence is the contrapositive of orbit constancy.■ 29 This is the precise true version of mechanism completeness used in the paper. The four ob- struction families are not claimed to exhaust all hard-side phenomena. Rather, orbit gaps are the complete obstruction criterion for exact classification of any fixed target predicate by closure-law- invariant classifiers, and the four families provide structurally distinct witnesses of that criterion. Corollary 4.13 (Orbit-Gap Completeness on Closure-Closed Domains). Let D be a closure-closed domain of slices, and let T be a target predicate on D. Then T admits an exact characterization on D by a closure-law-invariant predicate if and only if T has no orbit-gap witness inside D. Equivalently, exact characterization on D by closure-law-invariant predicates fails if and only if there exist U,V ∈ D in the same closure orbit with different T-status. 30 Proof sketch. This is the domain-restricted version formalized in Lean. The forward implication is immediate from closure-law invariance. For the reverse implication, take the closure hull of D∩ T; if T has no orbit-gap witness inside D, that closure hull agrees with T on D.■ Applied to exact tractability, Theorem 6.17 places every correct tractability classifier on a closure-closed domain inside this regime. Orbit gaps are therefore the complete obstruction cri- terion for the universal-scope no-go once correctness is imposed. 29 : FR201-204 30 : FR210-213 10 5 The Realizability Barrier One possible route to a finite tractability taxonomy would be to show that optimizer-induced quo- tients realize only a narrow subclass of equivalence relations, so that the frontier would emerge from realizability alone. In the unconstrained setting, this route fails. Theorem 5.1 31 (Every Labeling Kernel Is Optimizer-Realizable). Let φ : S → T be any function. There exists a decision problem with action space T and state space S such that for every state s∈ S, Opt(s) =φ(s). Consequently, for all states s,s ′ ∈ S, Opt(s) = Opt(s ′ ) ⇐⇒ φ(s) = φ(s ′ ). Equivalently, the decision quotient of the constructed problem is exactly the kernel partition of φ. Proof. Take the action set to be T itself and define U (a,s) = ( 1 if a = φ(s), 0 otherwise. Then the unique maximizer at state s is the designated action φ(s), so the optimizer set is exactly φ(s). Two states therefore have the same optimizer set if and only if they receive the same label under φ.■ Theorem 5.1 is the key negative fact for the frontier program. It shows that optimizer realizability by itself is extremely permissive. If arbitrary label kernels are already optimizer-induced, then no finite taxonomy can come merely from asking which abstract quotients are realizable. Proposition 5.2 32 (Every Equivalence Relation Is Optimizer-Realizable). For every equivalence rela- tion on the state space, there exists a decision problem whose decision quotient relation is exactly that equivalence relation. Moreover, the quotient object of the realizing problem is canonically equivalent to the corresponding setoid quotient. Proof. Let ≈ be an equivalence relation on S, and let π : S → S/≈ be the quotient map. Apply Theorem 5.1 to the labeling map π. The resulting decision problem satisfies Opt(s) = Opt(s ′ ) ⇐⇒ π(s) = π(s ′ ), and the right-hand side is exactly the original equivalence relation. Since the realizing quotient identifies states precisely by equality of quotient labels, its quotient object is canonically equivalent to the setoid quotient itself.■ Proposition 5.2 is the maximal realizability statement available in the present framework. The labeling-kernel theorem is a special case. Thus the realizability barrier is not merely broad; at the level of abstract quotient relations, it is maximal. Proposition 5.3 33 (The Realized Quotient Is Exactly the Label Range). For every labeling map φ : S → T, the decision quotient of the realizing problem is canonically equivalent to the range of φ. In finite settings, the quotient cardinality is therefore exactly | range(φ)|. 31 : FR7-8 32 : FR45-47 33 : FR39-40 11 Proof. By Theorem 5.1, two states lie in the same decision class if and only if they receive the same label under φ. Therefore the quotient class of a state depends only on the value φ(s), and sending the class of s to φ(s) defines a well-defined map from the decision quotient to range(φ). This map is surjective by definition of the range and injective because equality in the range means equality of labels, hence equality of quotient classes.■ Proposition 5.3 strengthens Theorem 5.1. The realizing construction does not merely realize the induced equivalence relation abstractly; it realizes the quotient object itself with exactly the expected image size. Corollary 5.4 34 (Realizability Alone Cannot Be the Frontier). Any future optimizer-compatible tractability metatheorem must use more than quotient realizability alone. Additional restrictions have to enter through representation, coordinate structure, utility structure, closure properties of the family under study, or comparable algebraic invariants. This shifts the burden of the metatheorem. The hard question is not which quotients can arise in principle; almost all kernels can. The hard question is which natural structural families of decision problems force tractability or preserve hardness once coordinate structure and utility representation are taken seriously. 6 Necessary Conditions on Any Frontier Statement The realizability barrier leaves a more precise frontier question. If quotient shape alone is too expressive, what should replace it as the organizing unit of the metatheorem? At minimum, the tractability frontier should not classify arbitrary sets of decision problems. It should range over representation-level structural classes and it should ignore benign changes of presentation. The right eventual condition list will almost certainly be stronger than this minimal principle. For example, a mature frontier theorem may also require closure under adding explicitly irrele- vant coordinates, adjoining dummy actions, or other representation-preserving refinements. But action/state relabel invariance is the irreducible starting point. Proposition 6.1 35 (Exact Certification Depends Only on the Decision Quotient Relation). If two decision problems on the same state space induce the same decision-equivalence relation, then they induce the same exact-certification structure. In particular, they have the same sufficient coordinate sets, the same minimal sufficient coordinate sets, and the same relevant and irrelevant coordinates. Moreover, their quotient objects are canonically equivalent; in finite settings, those quotient objects therefore have the same cardinality. Proposition 6.1 is the canonical statement behind the frontier program. Exact certification is determined by the decision quotient relation itself. Equality of optimizer maps is only a sufficient route to this conclusion, because equal optimizer maps induce the same decision-equivalence relation. Corollary 6.2 36 (Sufficiency Is Relation Refinement). A coordinate set I is sufficient if and only if the coordinate-agreement relation induced by I refines the decision quotient relation. Corollary 6.2 is the cleanest relational form of exact certification. It removes utility language entirely: sufficiency asks whether one state relation is contained in another. Corollary 6.3 37 (Relevance Is Failure of Erased Sufficiency). A coordinate i is irrelevant if and only if deleting it leaves a sufficient coordinate set, namely univ\i. Equivalently, i is relevant if and only if that erased set is not sufficient. 34 : FR7-8 35 : FR30-35, FR37, FR51 36 : FR48 37 : FR49-50 12 Corollary 6.3 makes the role of individual coordinates canonical: relevance is exactly the ob- struction to retaining sufficiency after coordinate erasure. Corollary 6.4 38 (Certification Statistics Factor Through the Quotient Relation). Any statistic that is a function of the sufficient-set family and relevant-coordinate set is invariant under equality of the decision quotient relation. In particular, the number of sufficient coordinate sets, the number of minimal sufficient coordinate sets, and the number of relevant coordinates are quotient invariants. Corollary 6.4 records the next logical consequence of Proposition 6.1. Once exact certification is identified with quotient data, every certification statistic built from sufficient sets or relevant coordinates factors automatically through that quotient data as well. Proposition 6.5 39 (Zero-Distortion Summaries Refine the Optimizer Quotient). Let σ : S → C be a summary map. Suppose that σ(s) = σ(s ′ ) =⇒ Opt(s) = Opt(s ′ ) for all s,s ′ ∈ S. Then each summary fiber is contained in a single optimizer-quotient class. Equivalently, σ factors through the optimizer quotient relation, and distinct optimizer classes require distinct summary symbols. Proof. If σ(s) = σ(s ′ ), the hypothesis gives Opt(s) = Opt(s ′ ). So every σ-fiber is contained in one decision-equivalence class. This is exactly the statement that σ refines the optimizer quotient. Conversely, if two distinct optimizer classes shared a summary symbol, choosing representatives from those classes would violate the zero-distortion premise.■ Proposition 6.5 explains why exact relevance is not merely one point on an approximation spectrum. Once distortion is required to be zero, lossless decision-preserving abstraction is already constrained by the optimizer quotient itself. Approximate summaries may still be useful for other goals, but they no longer certify exact preservation of the decision boundary. Corollary 6.6 40 (Constant-Optimizer Collapse Forces Trivial Certification). If the optimizer set is constant across all states, then the empty coordinate set is sufficient and every coordinate is irrele- vant. Corollary 6.6 isolates the first genuinely degenerate mechanism in the tractable basis. The certification problem disappears because there is no state dependence left to certify. Proposition 6.7 41 (Explicit Enumeration Is Parameter-Dependent, Not Structural). For every fixed exponent k, there exists a Boolean-cube family with state space size 2 n > n k . Thus explicit-state enumeration can outrun any fixed monomial bound in the ambient dimension parameter. Proposition 6.7 is weaker than a full polynomial lower-bound metatheorem, but it already cap- tures the structural point needed here: tractability by brute-force state enumeration depends on a separate size parameter and does not arise from an optimizer-compatible mechanism like symmetry, low rank, or tree structure. Proposition 6.8 42 (Positive Affine Utility Reparameterizations Are Invisible). Statewise positive affine transformations of utility leave exact certification unchanged. In particular, replacing U (a,s) by α(s) + β(s)U (a,s) with β(s) > 0 for every state s does not change sufficient coordinate sets or relevance judgments. 38 : FR41-44 39 : FR176-177 40 : FR52-53 41 : FR66-67 42 : FR13-16 13 Proposition 6.8 is another direct consequence of Proposition 6.1. It records a standard utility- theoretic invariance in the exact-certification language: only the induced decision quotient matters, not the particular positive affine scale used to encode utility. Proposition 6.9 43 (Duplicate Actions and Duplicate States Preserve Certification). Duplicating a single action without changing its utility profile preserves the decision quotient relation and hence preserves sufficiency and relevance. At the optimizer-set level, the only possible change is the ad- dition of the duplicate action itself: original optimal actions remain optimal, and the duplicate is optimal exactly when the original action was. Duplicating a single state without changing its util- ity profile preserves the decision quotient up to the obvious quotient equivalence and also preserves sufficiency and relevance. Proposition 6.9 gives two more theorem-forced closure laws. These are not modeling conventions; they are consequences of the fact that exact certification factors through quotient data rather than through accidental multiplicity in the presentation. Proposition 6.10 44 (Relabeling Invariance Is Forced by Exact Certification). Action relabeling pre- serves optimizer equivalence and exact sufficiency. State relabeling does so as well once the coor- dinate structure is transported along the state bijection. Consequently, any structural tractability frontier for exact relevance certification must be closed under these relabelings. Proposition 6.10 is now best read as a corollary of Proposition 6.1. Bijective relabelings do not change the optimizer map up to the obvious identification, so they cannot change exact certification. The second necessary ingredient is a genuine expressivity restriction. Call a class kernel-universal if, for every labeling map φ : S → T, it contains some decision problem whose optimizer quotient realizes exactly the kernel partition of φ. By Theorem 5.1, kernel universality is an extremely strong property. The canonical finite invariant here is the size of the optimizer quotient, equivalently the number of distinct optimal-action sets. The quotient is identified with the range of the optimizer map, so quotient size is not auxiliary bookkeeping; it is intrinsic. Proposition 6.11 45 (Quotient Size Is Unbounded Under Realizability). For every m∈N, there exists a finite decision problem whose optimizer quotient has size exactly m. Proof. Take m = k + 1 and realize the identity labeling on Fin(k + 1). Proposition 5.3 identifies the quotient object with the range of that identity labeling, which has cardinality k + 1. Equivalently, Proposition 5.2 realizes the discrete equivalence relation on Fin(k + 1).■ A meaningful frontier statement cannot range over classes that are simultaneously relabel- invariant and kernel-universal, because quotient shape alone then becomes too expressive to isolate the boundary. Proposition 6.12 46 (Invariance Alone Is Too Weak). The universal class of all decision problems satisfies action relabeling invariance and state relabeling invariance, but it is kernel-universal. Con- sequently, relabeling invariance by itself is far too weak to isolate a tractability frontier. Proposition 6.12 separates two kinds of conditions that can otherwise be conflated. 1. Benign invariance axioms say the family should ignore arbitrary naming choices. 2. Expressivity-limiting axioms say the family should not realize arbitrary quotient structure wholesale. 43 : FR54-56, FR68-73 44 : FR17-20 45 : FR24, FR38 46 : FR21-23 14 Any genuine optimizer-compatible frontier theorem will need both. Without decision-quotient invariance and its immediate corollaries such as relabel invariance and positive affine invariance, the statement is not structural. Without an expressivity restriction excluding kernel universality or something comparably strong, the realizability theorem and Proposition 6.11 make the class too large for quotient shape alone to carry the boundary. Proposition 6.13 47 (Independent Summary Frameworks Converge on the Same Structural Core). Write r = srank(D) for the number of relevant coordinates of a Boolean decision problem, and let m be the number of optimizer-quotient classes. Then: 1. m≤ 2 r , so the counting entropy log 2 m is at most r; 2. the diagonal 0/1 relevance-support matrix has rank exactly r; 3. every zero-distortion decision-preserving summary requires at least m distinct summary sym- bols. Hence quotient entropy, Fisher-style support counting, and zero-distortion summary size are all controlled by the same support/quotient core. Proof. If two states agree on all relevant coordinates, then they differ only on irrelevant ones. Changing those irrelevant coordinates one at a time cannot change the optimizer, so the relevant coordinates already determine the optimizer class. Therefore there are at most 2 r optimizer classes, one for each Boolean assignment on the relevant support, and log 2 m≤ r follows. For the second clause, the diagonal relevance-support matrix has a 1 exactly on relevant coor- dinates and a 0 elsewhere. Its rank is therefore the number of relevant coordinates, namely r. The third clause is exactly Proposition 6.5: a zero-distortion summary must assign distinct symbols to distinct optimizer classes.■ Proposition 6.13 does not identify entropy, support counting, and lossless summaries as identical notions. It shows that they already converge on the same structural content before any admissibility axiom is imposed. Closure-law invariance follows from this convergence: once several independent frameworks ignore surface presentation in favor of the support/quotient core, a structural tractability classifier should do the same. The remaining admissibility clauses serve as algorithmic and semantic guardrails. From Necessary Conditions to an Admissibility Class The closure properties above are theorem-forced by exact-certification semantics, but they are not enough on their own to support a meaningful impossibility theorem. If one allows unrestricted predicates, a semantic predicate can simply encode the target complexity class and trivialize the statement. Proposition 6.14 48 (Unrestricted Predicates Trivialize Exact Characterization). Without admissibil- ity restrictions, there exist normalization predicates whose membership condition directly encodes the intended polynomial-time side of the landscape, so unrestricted collapse-impossibility claims fail. Proposition 6.14 is not a by-product of the proof method. It is the expected behavior of un- restricted semantic predicates. Therefore any meaningful frontier theorem must be parameterized by an admissibility class that simultaneously (i) respects theorem-forced invariances and (i) blocks direct semantic encoding. 47 : FR178-182 48 : FR145 15 Proposition 6.15 (Closure Operations Preserve Exact Certification). The theorem-forced closure op- erations preserve the exact-certification problem itself. More precisely: 1. action relabeling, coordinate relabeling, and statewise positive affine reparameterization pre- serve sufficient coordinate sets and relevant coordinates under the evident transport; 2. action duplication and state duplication preserve sufficient coordinate sets and relevant coor- dinates exactly; 3. binary irrelevant-coordinate extension preserves sufficiency after lifting coordinate sets, pre- serves relevance on the original coordinates, and makes the new coordinate irrelevant. In particular, each closure step induces the same exact-certification decision problem up to an ex- plicit coordinate-set transport. For the irrelevant-coordinate case in the present binary-pairwise formalization, the encoding blowup is only constant-factor because the added coordinate is binary. 495051 Proof sketch. Each clause is verified directly in the artifact at the level of exact-certification se- mantics. The relabeling and positive-affine cases preserve the decision-equivalence relation, hence preserve sufficiency and relevance. The duplication cases preserve decision-equivalence through the explicit quotient projections back to the original problem. The irrelevant-coordinate case is formal- ized as binary noise extension: I ⊆ [d] is sufficient for the base slice if and only if its lift is sufficient after extension, the original coordinates remain exactly the relevant ones, and the new coordinate is irrelevant. The size remarks in the right-hand column are direct from the concrete binary-pairwise encoding and are not separate Lean claims. OperationExact-certification transportEncoding effect Action/state relabelingsame sufficient sets and relevant coordi- nates after transport relabeling only Positive affine reparameteriza- tion same sufficient sets and relevant coordi- nates same arity, same action set; util- ity magnitudes rescaled Action/state duplicationsame sufficient sets and relevant coordi- nates carrier duplica- tion only Binary irrelevant-coordinate extension I ↔ lift(I), old relevance preserved, new coordinate irrelevant arity increases by one binary coor- dinate ■ Definition 6.16 (Admissible Normalization Predicate). A normalization predicate is admissible when it satisfies all of the following: 1. polynomial-time checkability at the slice level; 2. invariance under the closure laws forced by exact certification (relabelings, positive affine reparameterizations, duplication operations, and binary irrelevant-coordinate extension); 3. structural extractability of the associated dependency graph; 49 : FR15-20 50 : FR55-60 51 : FR83-85 16 4. bounded-pattern definability. More explicitly, let |U| denote the encoding size of a binary pairwise slice U, and let X(U ) be its canonical finite pairwise syntax. Polynomial-time checkability means that there exist constants c,k ∈N and a decision procedure A such that A(U ) = 1 ⇐⇒ Q(U ),time A (U )≤ c(|U| + 1) k + c. Structural extractability means that whenever Q(U ) holds, the associated coordinate graph is ob- tained from syntax alone: there exists a uniform extractor E : X 7→ G E (X) on finite pairwise syntactic presentations such that the graph attached to U is exactly G E (X(U )). Bounded-pattern definability is likewise finite and explicit. There must exist uniform bounds on radius, neighborhood size, action alphabet size, and coefficient magnitude, together with finite lists of permitted and forbidden rooted local patterns, such that membership in Q is determined by the presence of one witness pattern or the absence of all forbidden patterns in the rooted interaction neighborhoods of X(U ). No unbounded global computation is hidden inside the definition. Polynomial-time checkability is the minimal algorithmic requirement. A tractability characteri- zation that cannot itself be recognized efficiently has little explanatory value: it would only relocate the computational difficulty from exact certification to the membership test for the classifier. Closure-law invariance is the semantic requirement used in the orbit-witness arguments of Sec- tion 4. It is forced by the Block 6 invariance theorems, because exact certification itself is un- changed by relabelings, positive affine utility reparameterizations, duplication operations, and bi- nary irrelevant-coordinate extensions. Structural extractability distinguishes structural characterizations from purely semantic ones. Without such a condition, one can define predicates directly on optimizer behavior or on the solved certification instance itself, bypassing the stated aim of classifying tractability by representation- level structure. Bounded-pattern definability is the locality guardrail. Its role is to exclude predicates whose membership test secretly performs an unbounded global computation under a structural name. In particular, it prevents one from reintroducing oracle power through an arbitrarily large finite schema. Theorem 6.17 (Tractability Classifiers Are Forced to Be Closure-Invariant). Let C be any procedure assigning to each representation in a closure-closed domain Γ a verdict in tractable, intractable, and suppose that C correctly predicts whether exact certification is polynomial-time decidable on the underlying problem. Then C must agree on representations within the same closure orbit. Equiv- alently, every correct tractability classifier on a closure-closed domain is closure-invariant on that domain, regardless of whether its internal features are themselves invariant. 52 Proof sketch. This is the tractability instance of the abstract correctness-on-domain theorem for- malized in Lean. If U,V ∈ Γ lie in the same closure orbit, Proposition 6.15 shows that they induce the same exact-certification problem up to the explicit coordinate-set transport attached to the rel- evant closure step. The theorem uses the semantic notion of correctness stated above: tractability is attached to that underlying exact-certification problem, not to arbitrary relabelings or duplicate- label presentations of the same problem. Correctness of C therefore forces the same verdict on both. ■ 52 : FR197-199 17 This answers the natural objection that Section 4 excludes only classifiers that advertise closure invariance as an explicit axiom. Exact correctness already forces the same orbit agreement. The closure laws therefore supply the representation-level congruence needed for the orbit-gap program: once two slices are related by these theorem-forced presentation equivalences, any exact tractability classifier must identify them. Theorem 4.9 therefore applies to any exact classifier on a closure-closed domain once the target notion is tractability itself: if the classifier separates same-orbit witnesses, it is simply wrong on at least one of them. Proposition 6.18 (The Admissibility Layer Is Nonempty). Definition 6.16 is not vacuous. There exist admissible normalization predicates; in fact both the constant-true and constant-false slice predicates are admissible. 53 Proof sketch. Both predicates are decidable in constant time and are automatically invariant un- der all closure laws. Their graph extractors are fixed graphs independent of the input slice. For bounded-pattern definability, use a single impossible local pattern: a radius-zero pattern with two distinct vertices cannot occur in any slice. Taking that pattern as forbidden yields the constant-true predicate, and taking it as a required witness yields the constant-false predicate.■ Thus the impossibility theorem is not an emptiness statement about Definition 6.16. The admis- sibility layer already contains explicit predicates; the point of the no-go theorem is that correctness across the obstruction families forces a contradiction once closure-orbit agreement is respected. Proposition 6.19 (Bounded Distinct Action Profiles Compress to Bounded Actions). For a binary pairwise slice U, let d(U ) be the number of distinct action utility profiles. Then there exists a compressed slice U prof with exactly d(U ) actions such that a coordinate set is sufficient for U if and only if it is sufficient for U prof , and a coordinate is relevant for U if and only if it is relevant for U prof . Consequently, if d(U ) ≤ k, the bounded-actions tractability theorem applies to U prof , so the bounded-distinct-profile subcase is polynomial on the exact-certification side. 54 Proof sketch. Replace each action by its full utility profile over states and quotient the action set by profile equality. Duplicated actions collapse to a single profile action, but exact certification is unchanged because optimizer equality depends only on which profiles are optimal, not on how many labels realize a given profile. The compressed slice has exactly d(U ) actions by construction, and the artifact proves equality of the sufficient-coordinate and relevant-coordinate predicates between U and U prof . The existing bounded-actions polynomial-time theorem then applies to the compressed slice.■ Proposition 6.19 isolates a genuine positive tractable subcase by compression to bounded ac- tions. It is stated as a compression theorem rather than direct admissibility membership because Definition 6.16 fixes a bounded-pattern action alphabet in advance. The proposition still shows that nontrivial positive classification work is available through closure-law-respecting reduction inside the present framework. Proposition 6.20 (Bounded-Pattern Predicates Stabilize Above a Finite Action Bound). For every bounded-pattern definable predicate Q, there exists a finite bound B such that Q is constant on all slices with more than B actions. Equivalently, once the action alphabet exceeds the action bound built into the defining pattern scheme, the scheme can no longer distinguish between such slices. 55 53 : FR200 54 : FR205-209 55 : FR214-216 18 Proof sketch. In a bounded-pattern scheme every witness and forbidden pattern has action alphabet size at most a fixed bound B. If a slice has more than B actions, then no listed local pattern can occur in it, because occurrence requires an action-set equivalence between the pattern and the slice. The witness branch of the scheme is therefore impossible, while the forbidden branch is determined only by whether the forbidden list is empty. Hence the predicate is constant above the fixed action bound.■ This is why Proposition 6.19 is stated as a compression theorem rather than as direct admissi- bility membership for the distinct-profile predicate. Unbounded profile counting does not naturally fit a definition whose bounded-pattern clause fixes a finite action alphabet in advance. Closure-law invariance (clause 2) is not an arbitrary stylistic restriction. Theorem 6.17 shows that exact correctness already forces closure-orbit agreement, and Theorem 4.9 shows that this theorem-forced congruence is the only load-bearing hypothesis in the no-go theorem. The remaining clauses are the minimal guardrails against the failure modes identified in Proposition 6.14; the specific guardrail formulation of clauses 1, 3, and 4 is one natural choice but is not load-bearing. 7 Related Work Rough Sets, Feature Selection, and Exact Relevance At the static level, rough-set reduct theory [19, 30] is the clearest classical comparison point. That literature studies which attributes can be deleted while preserving decision distinctions. Exact static sufficiency can be viewed as a reduct condition for the induced decision table. The question here is different: which tractable mechanisms admit a finite characterization? A separate literature studies feature selection, variable importance, and model explanation in machine learning and AI, including wrapper and filter methods [15], general surveys [13], and attri- bution methods based on Shapley-style decompositions [16]. These works matter here by motivation rather than by technique. They typically optimize predictive performance, explanatory salience, or approximation quality under data-dependent criteria. Exact relevance certification instead asks for a semantic preservation property: which coordinates are necessary to preserve the optimizer relation exactly. Decision-theoretic informativeness and value of information, beginning with Blackwell’s com- parison of experiments and subsequent decision-theoretic treatments [4, 23, 14], provide a second comparison point. Both settings ask when one representation retains all decision-relevant distinc- tions of another. The difference here is the combinatorial complexity of certifying exact preservation under coordinate deletion. Information-Theoretic and Transport Viewpoints The zero-distortion discussion belongs to the classical information-theoretic tradition of exact distin- guishability and lossless coding boundaries, going back to Shannon and standard modern treatments of source coding and rate-distortion theory [25, 26, 27, 6]. Fisher-style support counting supplies an- other classical comparison lens on relevant support [8]. These viewpoints are used only structurally. There is no general coding or statistical estimation problem here. Zero distortion, entropy, and support counting appear only to show that several independent summary frameworks are already constrained by the same optimizer-quotient core. The Wasserstein language in Section 4 plays the same role: a qualitative description of quotient branching rather than a full transport-theoretic model. 19 Backdoors, Tractable Islands, and Dichotomy Programs The nearest complexity-theoretic analogue is backdoor tractability for constraint satisfaction [31, 3, 9]. There, a small structural set exposes membership in a tractable class even when the ambient problem is hard. The comparison is direct: exact relevance certification also asks which coordinates matter, and polynomial-time behavior emerges when the source of hardness is restricted by structure. Bessiere et al. [3] make especially clear that exploiting a known tractable structure and discovering the responsible structure are different algorithmic tasks; later parameterized work sharpened that distinction. This is closely aligned with the present paper’s separation between positive tractable mechanisms and the harder meta-level problem of recognizing a correct frontier classifier. The broader analogy is the dichotomy tradition for satisfiability and constraint satisfaction, from Schaefer’s Boolean dichotomy theorem [24] to the finite-domain CSP dichotomy theorems of Bulatov and Zhuk [5, 34]. The expectation that a clean tractability boundary should exist was articulated in the Feder–Vardi program [7], and later algebraic work of Barto and Kozik clarified why finite structural boundaries are plausible in that setting [2]. The point here is narrower: for exact relevance certification, quotient realizability and closure-law invariance defeat the most direct admissible optimizer-compatible classifier. Any successful frontier theorem in this domain must therefore use stronger representation-sensitive structure. The quotient viewpoint also touches the literature on exact abstraction and aggregation in stochastic control, Markov decision processes, and reinforcement learning [18, 11, 20]. Those works study when states may be aggregated while preserving value or policy structure. Our setting is narrower: we ask for exact preservation of optimizer classes under coordinate-hiding maps rather than arbitrary state abstractions. Still, the common theme is that semantic invariants of decision behavior should survive presentation-level simplification. Meta-Impossibility Traditions The closest analogy is Rice-style impossibility. Rice’s theorem [21] shows that nontrivial extensional properties of partial recursive functions are undecidable, with extensionality forced by what “seman- tic” means rather than chosen as an axiom. Refinements such as the Myhill–Shepherdson theorem and the Rice–Shapiro theorem extend this pattern to broader structured semantic domains [17, 28]. The present theorem has the same structure with a different forced invariance. Proposition 6.1 shows that exact certification depends only on quotient data, and Theorem 6.17 lifts this to tractability classification: any correct tractability classifier must agree on closure-equivalent representations. The no-go then depends on this forced invariance alone (Theorem 4.9), with Corollary 4.11 giving the resulting impossibility for correct classifiers. The remaining admissibility clauses play the role of algorithmic and structural guardrails that exclude classifiers admissible in name only, but they do not enter the contradiction. At the foundational level, Gödel’s incompleteness theorems show that sufficiently expressive formal systems cannot internalize all truths about their own proof theory [12]. In learning and op- timization, no-free-lunch results show that universal guarantees disappear on overly broad problem domains [32, 33]. In social choice, Arrow’s theorem and the Gibbard–Satterthwaite theorems show that natural axiomatic requirements become jointly unsatisfiable on rich enough domains [1, 10, 22]. We place the present theorem in that same impossibility tradition: a natural invariance package is fixed, and no exact classifier survives on the intended domain. 20 8 Conclusion The frontier question now has both a positive and a negative answer. On the positive side, the tractable landscape studied here factors into primitive mechanisms, lifts, and degeneracies. Propo- sition 6.19 shows that this positive side remains substantive at the representation level: bounded distinct action profiles compress to bounded-action slices without changing exact certification, so the existing bounded-actions theorem already yields a genuine structural classifier on that subcase. On the negative side, quotient realizability is maximal, so quotient shape cannot classify tractability by itself, and an admissibility-layer collapse theorem rules out direct finite classifiers even after impos- ing theorem-forced closure laws together with computational and structural restrictions. Moreover, Theorem 4.9 isolates the load-bearing hypothesis: the collapse depends only on closure-law invari- ance, so any guardrail package whose admissible predicates respect this single forced invariance inherits the impossibility. Theorem 6.17 strengthens the conclusion further: exact correctness itself forces closure-orbit agreement, and Corollary 4.11 makes the scope explicit. Proposition 6.18 shows that the admissibility layer is nonempty, while Proposition 6.19 shows that the positive classification problem itself is nontrivial. The no-go is therefore universal over correct classifiers on closure-closed domains, not merely over classifiers that build invariance into their definitions. Technically, the mechanism is closure-orbit disagreement via pair-targeted action-independent affine transport. The same template now applies to four obstruction families (dominant pair, margin masking, ghost action, and additive/statewise offset), yielding an admissible-collapse theorem. The open problem is now sharper. Simple finite lists and unconstrained quotient predicates cannot characterize the boundary, and admissible closure-invariant classifiers of the present kind cannot do so either. Any successful frontier theorem must therefore invoke stronger representation- sensitive structure than the one ruled out here. Declaration of Generative AI and AI-assisted technologies in the writing process During the preparation of this work the author used Codex, Claude Code, Augment, Kilo, and OpenCode in order to refine prose, clean up notation, edit the L A T E X source, and test alternative phrasings and structural arrangements. After using these tools, the author reviewed and edited the content as needed and takes full responsibility for the content of the published article. Generative AI tools were used throughout the manuscript, across all sections and across all stages from initial drafting to final revision. The tools were used for boilerplate generation, prose and notation refinement, L A T E X/structure cleanup, translation of informal proof ideas into candidate formal artifacts (Lean/L A T E X), and repeated adversarial reviewer-style critique passes to identify blind spots and clarity gaps. The author retained full intellectual and editorial control, including problem selection, theo- rem statements, assumptions, novelty framing, acceptance criteria, and final inclusion/exclusion decisions. No technical claim was accepted solely from AI output. Formal claims reported as machine-verified were admitted only after Lean verification (no sorry in cited modules) and direct author review. The author is solely responsible for all statements, citations, and conclusions. Acknowledgments The author thanks Tobias Fritz for identifying the optimizer quotient as the coimage of Opt in Set in earlier work [29], the categorical statement that licenses the canonicity claims in Sections 1 and 6 21 of the present paper. References [1] Kenneth J. Arrow. A difficulty in the concept of social welfare. Journal of Political Economy, 58(4):328–346, 1950. [2] Libor Barto and Marcin Kozik. Constraint satisfaction problems solvable by local consistency methods. Journal of the ACM, 61(1):3:1–3:19, 2014. [3] Christian Bessiere, Clement Carbonnel, Emmanuel Hebrard, George Katsirelos, and Toby Walsh. Detecting and exploiting subproblem tractability. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI), pages 468–474, 2013. [4] David Blackwell. Equivalent comparisons of experiments. The Annals of Mathematical Statis- tics, 24(2):265–272, 1953. [5] Andrei A. Bulatov. A dichotomy theorem for nonuniform csps. In 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS), pages 319–330. IEEE, 2017. [6] Thomas M. Cover and Joy A. Thomas. Elements of Information Theory. Wiley-Interscience, 2nd edition, 2006. [7] Tomás Feder and Moshe Y. Vardi. The computational structure of monotone monadic snp and constraint satisfaction: A study through datalog and group theory. SIAM Journal on Computing, 28(1):57–104, 1998. [8] Ronald A. Fisher. On the mathematical foundations of theoretical statistics. Philosophical Transactions of the Royal Society of London. Series A, 222:309–368, 1922. [9] Robert Ganian, M. S. Ramanujan, and Stefan Szeider. Discovering archipelagos of tractabil- ity for constraint satisfaction and counting. In Proceedings of the 27th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1670–1681. SIAM, 2016. [10] Allan Gibbard. Manipulation of voting schemes: A general result. Econometrica, 41(4):587– 601, 1973. [11] Robert Givan, Thomas Dean, and Matthew Greig. Equivalence notions and model minimization in markov decision processes. Artificial Intelligence, 147(1-2):163–223, 2003. [12] Kurt G"odel. "Uber formal unentscheidbare s"atze der Principia Mathematica und verwandter systeme I. Monatshefte f"ur Mathematik und Physik, 38(1):173–198, 1931. [13] Isabelle Guyon and André Elisseeff. An introduction to variable and feature selection. Journal of Machine Learning Research, 3:1157–1182, 2003. [14] Ronald A. Howard. Information value theory. IEEE Transactions on Systems Science and Cybernetics, 2(1):22–26, 1966. [15] Ron Kohavi and George H. John. Wrappers for feature subset selection. Artificial Intelligence, 97(1-2):273–324, 1997. 22 [16] Scott M. Lundberg and Su-In Lee. A unified approach to interpreting model predictions. In Advances in Neural Information Processing Systems 30 (NeurIPS), pages 4765–4774, 2017. [17] John Myhill and John C. Shepherdson. Effective operations on partial recursive functions. Zeitschrift f"ur mathematische Logik und Grundlagen der Mathematik, 1(5):310–317, 1955. [18] Christos H. Papadimitriou and John N. Tsitsiklis. The complexity of markov decision processes. Mathematics of Operations Research, 12(3):441–450, 1987. [19] Zdzisław Pawlak. Rough sets. International Journal of Parallel Programming, 11(5):341–356, 1982. [20] Balaraman Ravindran. An Algebraic Approach to Abstraction in Reinforcement Learning. PhD thesis, University of Massachusetts Amherst, 2004. [21] Henry Gordon Rice. Classes of recursively enumerable sets and their decision problems. Trans- actions of the American Mathematical Society, 74(2):358–366, 1953. [22] Mark Allen Satterthwaite. Strategy-proofness and Arrow’s conditions: Existence and corre- spondence theorems for voting procedures and social welfare functions. Journal of Economic Theory, 10(2):187–217, 1975. [23] Leonard J. Savage. The Foundations of Statistics. John Wiley & Sons, 1954. [24] Thomas J. Schaefer. The complexity of satisfiability problems. In Proceedings of the Tenth Annual ACM Symposium on Theory of Computing, pages 216–226. ACM, 1978. [25] Claude E. Shannon. A mathematical theory of communication. Bell System Technical Journal, 27(3):379–423, 1948. [26] Claude E. Shannon. Zero-error capacity of a noisy channel. IRE Transactions on Information Theory, 2(3):8–19, 1956. [27] Claude E. Shannon. Coding theorems for a discrete source with a fidelity criterion. IRE National Convention Record, 7:142–163, 1959. Part 4. [28] Norman Shapiro. Degrees of computability. Transactions of the American Mathematical Soci- ety, 82(2):281–299, 1956. [29] Tristan Simas. The optimizer quotient and the certification trilemma. arXiv:2603.14689, 2026. https://arxiv.org/abs/2603.14689. [30] Roman Slowinski and Daniel Vanderpooten. Decision under uncertainty: A rough set approach. European Journal of Operational Research, 80(2):277–289, 1995. [31] Ryan Williams, Carla P. Gomes, and Bart Selman. Backdoors to typical case complexity. In Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI), pages 1173–1178. Morgan Kaufmann Publishers Inc., 2003. [32] David H. Wolpert. The lack of a priori distinctions between learning algorithms. Neural Computation, 8(7):1341–1390, 1996. [33] David H. Wolpert and William G. Macready. No free lunch theorems for optimization. IEEE Transactions on Evolutionary Computation, 1(1):67–82, 1997. 23 [34] Dmitriy Zhuk. A proof of csp dichotomy conjecture. In 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS), pages 331–342. IEEE, 2017. 24 Supplementary Material for “Toward a Tractability Frontier for Exact Relevance Certification” Tristan Simas April 9, 2026 The archived artifact for this paper is available at https://doi.org/10.5281/zenodo.19457896. 1 Full Lean Handle Ledger This supplement provides the complete Lean handle ledger cited by the manuscript. It includes every handle identifier, declaration name, and source module path. IDLean Handle / SourceIDLean Handle / Source FR1 currentFamilies_partition_by_role Paper4dFrontier/Classification.lean FR2 currentFamilies_partition_counts Paper4dFrontier/Classification.lean FR3 current_families_have_finite_basis Paper4dFrontier/Classification.lean FR4 current_positive_interfaces_factor_through_ role Paper4dFrontier/Classification.lean FR5 lifted_families_reduce_to_core Paper4dFrontier/Classification.lean FR6 degenerateFamilies_complete Paper4dFrontier/Classification.lean FR7 exists_decisionProblem_realizing_labeling Paper4dFrontier/Realizability.lean FR8 realizingProblem_decisionEquiv_iff Paper4dFrontier/Realizability.lean FR13 isOptimal_positiveAffineTransform_iff Paper4dFrontier/FamilyAxioms.lean FR14 opt_eq_positiveAffineTransform Paper4dFrontier/FamilyAxioms.lean FR15 isSufficient_positiveAffineTransform_iff Paper4dFrontier/FamilyAxioms.lean FR16 isRelevant_positiveAffineTransform_iff Paper4dFrontier/FamilyAxioms.lean FR17 decisionEquiv_relabelActions_iff Paper4dFrontier/FamilyAxioms.lean FR18 decisionEquiv_relabelStates_iff Paper4dFrontier/FamilyAxioms.lean FR19 isSufficient_relabelActions_iff Paper4dFrontier/FamilyAxioms.lean FR20 isSufficient_relabelStates_iff Paper4dFrontier/FamilyAxioms.lean FR21 allProblems_relabelInvariant Paper4dFrontier/FamilyAxioms.lean FR22 allProblems_kernelUniversal Paper4dFrontier/FamilyAxioms.lean FR23 relabelInvariant_not_enough Paper4dFrontier/FamilyAxioms.lean FR24 optRangeCard_realizingIdentity Paper4dFrontier/FamilyAxioms.lean FR25 currentFamilies_explicit Paper4dFrontier/Classification.lean FR26 coreFamilies_explicit Paper4dFrontier/Classification.lean FR27 liftedFamilies_explicit Paper4dFrontier/Classification.lean FR28 degenerateFamilies_explicit Paper4dFrontier/Classification.lean FR29 primitiveMechanisms_explicit Paper4dFrontier/Classification.lean FR30 isSufficient_iff_of_decisionEquiv_iff Paper4dFrontier/FamilyAxioms.lean FR31 isRelevant_iff_of_decisionEquiv_iff Paper4dFrontier/FamilyAxioms.lean FR32 isIrrelevant_iff_of_decisionEquiv_iff Paper4dFrontier/FamilyAxioms.lean FR33 isMinimalSufficient_iff_of_decisionEquiv_iff Paper4dFrontier/FamilyAxioms.lean FR34 sufficientSets_eq_of_decisionEquiv_iff Paper4dFrontier/FamilyAxioms.lean FR35 relevantSet_eq_of_decisionEquiv_iff Paper4dFrontier/FamilyAxioms.lean FR37 quotientCard_eq_of_decisionEquiv_iff Paper4dFrontier/FamilyAxioms.lean FR38 quotientCard_realizingIdentity Paper4dFrontier/FamilyAxioms.lean FR39 realizingProblemQuotientEquivLabelRange_apply_ quotientMap Paper4dFrontier/Realizability.lean (continued... ) 1 IDLean Handle / SourceIDLean Handle / Source FR40 realizingProblem_quotientCard_eq_ labelRangeCard Paper4dFrontier/Realizability.lean FR41 certificationStatistic_eq_of_decisionEquiv_iff Paper4dFrontier/FamilyAxioms.lean FR42 sufficientSetCount_eq_of_decisionEquiv_iff Paper4dFrontier/FamilyAxioms.lean FR43 minimalSufficientSetCount_eq_of_decisionEquiv_ iff Paper4dFrontier/FamilyAxioms.lean FR44 relevantCoordCount_eq_of_decisionEquiv_iff Paper4dFrontier/FamilyAxioms.lean FR45 setoidRealizingProblem_decisionEquiv_iff Paper4dFrontier/Realizability.lean FR46 setoidRealizingProblemQuotientEquivSetoidQuotient_ apply_quotientMap Paper4dFrontier/Realizability.lean FR47 exists_decisionProblem_realizing_setoid Paper4dFrontier/Realizability.lean FR48 isSufficient_iff_agreementRel_le_decisionEquiv Paper4dFrontier/FamilyAxioms.lean FR49 isIrrelevant_iff_sufficient_erase Paper4dFrontier/FamilyAxioms.lean FR50 isRelevant_iff_not_sufficient_erase Paper4dFrontier/FamilyAxioms.lean FR51 quotientEquiv_of_decisionEquiv_iff_apply_ quotientMap Paper4dFrontier/FamilyAxioms.lean FR52 empty_sufficient_of_constant_opt Paper4dFrontier/ClosureLaws.lean FR53 irrelevant_of_constant_opt Paper4dFrontier/ClosureLaws.lean FR54 decisionEquiv_duplicateAction_iff Paper4dFrontier/ClosureLaws.lean FR55 isSufficient_duplicateAction_iff Paper4dFrontier/ClosureLaws.lean FR56 isRelevant_duplicateAction_iff Paper4dFrontier/ClosureLaws.lean FR57 decisionEquiv_duplicateState_iff Paper4dFrontier/ClosureLaws.lean FR58 isSufficient_duplicateState_iff Paper4dFrontier/ClosureLaws.lean FR59 isRelevant_duplicateState_iff Paper4dFrontier/ClosureLaws.lean FR60 duplicateStateQuotientEquivOriginal_apply_ quotientMap Paper4dFrontier/ClosureLaws.lean FR66 booleanCube_card Paper4dFrontier/EnumerationBounds.lean FR67 exists_booleanCube_larger_than_monomial Paper4dFrontier/EnumerationBounds.lean FR68 decisionEquiv_addDuplicateState_iff Paper4dFrontier/ClosureLaws.lean FR69 isSufficient_addDuplicateState_iff Paper4dFrontier/ClosureLaws.lean FR70 isRelevant_addDuplicateState_iff Paper4dFrontier/ClosureLaws.lean FR71 addDuplicateStateQuotientEquivOriginal_apply_ quotientMap Paper4dFrontier/ClosureLaws.lean FR72 some_mem_opt_addDuplicateAction_iff Paper4dFrontier/ClosureLaws.lean FR73 none_mem_opt_addDuplicateAction_iff Paper4dFrontier/ClosureLaws.lean FR83 isSufficient_noiseExtended_iff Paper4dFrontier/DimensionalNoiseExtension.lean FR84 isRelevant_noiseExtended_iff Paper4dFrontier/DimensionalNoiseExtension.lean FR85 lastCoord_irrelevant_noiseExtended Paper4dFrontier/DimensionalNoiseExtension.lean FR100 parentTree_realTreewidth_one Paper4dFrontier/ParentTreewidth.lean FR101 low_rank_only_witness Paper4dFrontier/LowRankOnlyWitness.lean FR105 separable_only_witness Paper4dFrontier/SeparableOnlyWitness.lean FR106 bounded_actions_only_witness Paper4dFrontier/BoundedActionsOnlyWitness2.lean FR108 all_independent_core_mechanisms_nondegenerate Paper4dFrontier/Block2Progress.lean FR110 parentTreeStructured_implies_treeStructured Paper4dFrontier/ParentTreewidth.lean FR111 treeStructured_and_unique_parent_iff_ parentTreeStructured Paper4dFrontier/ParentTreewidth.lean FR112 bounded_treewidth_only_witness Paper4dFrontier/BoundedTreewidthOnlyWitness.lean FR113 symmetry_only_witness Paper4dFrontier/SymmetryOnlyWitness.lean FR114 weak_tree_structured_not_width_one Paper4dFrontier/LegacyTreeGap.lean FR115 tree_structure_hardness_bridge Paper4dFrontier/TreeStructureHardnessBridge.lean FR118 pairCrossDifference_eq_binaryCrossDifference_ of_lt Paper4dFrontier/BinaryPairwiseDichotomy.lean FR119 pairwise_zero_crossDifference_ unaryDecomposition Paper4dFrontier/BinaryPairwiseDichotomy.lean FR120 binary_pairwise_symmetry_dichotomy Paper4dFrontier/BinaryPairwiseDichotomy.lean FR121 actionGapCrossDifference_eq_ binaryCrossDifference_of_lt Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean FR122 decisionRelevant_zero_actionGap_implies_ unaryReduction Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean FR123 binary_pairwise_symmetry_decision_relevant_ dichotomy Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean FR124 block6_genuine_interaction_dichotomy_ obstruction Paper4dFrontier/Block6Obstruction.lean (continued... ) 2 IDLean Handle / SourceIDLean Handle / Source FR125 decisionRelevantInteractionGraph_ addActionOffset Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean FR126 action_offset_can_force_constant_optimizer Paper4dFrontier/Block6Obstruction.lean FR127 block6_action_offset_obstruction Paper4dFrontier/Block6Obstruction.lean FR128 offsetNormalizedDecisionRelevantInteractionGraph_ wellDefined Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean FR129 block6_offset_normalized_obstruction Paper4dFrontier/Block6Obstruction.lean FR130 neverOptimalGhost_decisionRelevantGraph_eq_top Paper4dFrontier/Block6Obstruction.lean FR131 neverOptimalGhost_supportedGraph_eq_bot Paper4dFrontier/Block6Obstruction.lean FR132 support_filtering_removes_known_block6_ obstructions Paper4dFrontier/Block6Obstruction.lean FR133 block6_ghost_action_obstruction Paper4dFrontier/Block6Obstruction.lean FR134 marginMasking_supportedGraph_eq_top Paper4dFrontier/Block6Obstruction.lean FR135 marginMasking_zero_sufficient Paper4dFrontier/Block6Obstruction.lean FR136 block6_optimizer_supported_obstruction Paper4dFrontier/Block6Obstruction.lean FR137 MarginBounded Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean FR138 dominantPair_marginBounded Paper4dFrontier/Block6Obstruction.lean FR139 dominantPair_supportedGraph_eq_top Paper4dFrontier/Block6Obstruction.lean FR140 block6_margin_bounded_obstruction Paper4dFrontier/Block6Obstruction.lean FR145 not_collapseLandscapeInfinity_of_oracle_ predicate Paper4dFrontier/MetaCharacterization.lean FR176 DecisionQuotient.DecisionProblem.quotient_is_ coarsest paper4/DecisionQuotient/Quotient.lean FR177 DecisionQuotient.DecisionProblem.quotient_has_ unique_factorization paper4/DecisionQuotient/Quotient.lean FR178 DecisionQuotient.DecisionProblem.srank_eq_ relevant_card paper4/DecisionQuotient/Tractability/ StructuralRank.lean FR179 DecisionQuotient.quotientEntropy_le_srank_ binary paper4/DecisionQuotient/Information.lean FR180 DecisionQuotient.Statistics.fisherMatrix_rank_ eq_srank paper4/DecisionQuotient/Statistics/ FisherInformation.lean FR181 DecisionQuotient.Information.compression_ below_srank_fails paper4/DecisionQuotient/Information/ RDSrank.lean FR182 DecisionQuotient.Information.srank_bits_ sufficient paper4/DecisionQuotient/Information/ RDSrank.lean FR183 DecisionQuotient.Physics.single_future_zero_ cost paper4/DecisionQuotient/Physics/ WassersteinIntegrity.lean FR184 DecisionQuotient.Physics.transportCost_pos_of_ offDiag paper4/DecisionQuotient/Physics/ WassersteinIntegrity.lean FR185 no_closureInvariant_predicate_of_orbit_gap Paper4dFrontier/ObstructionPredicateCandidates.lean FR186 no_admissibleNormalizationPredicate_decides_ dominantPair Paper4dFrontier/ObstructionPredicateCandidates.lean FR187 no_admissibleNormalizationPredicate_decides_ marginBounded Paper4dFrontier/ObstructionPredicateCandidates.lean FR188 no_admissibleNormalizationPredicate_decides_ ghostActionTwoPairCrossOne Paper4dFrontier/ObstructionPredicateCandidates.lean FR189 no_admissibleNormalizationPredicate_decides_ offsetActionZeroPairCrossOne Paper4dFrontier/ObstructionPredicateCandidates.lean FR190 admissibleCollapseLandscapeInfinity_full_paper Paper4dFrontier/ObstructionPredicateCandidates.lean FR191 ClosureSoundPackage Paper4dFrontier/ObstructionPredicateCandidates.lean FR192 ReasonableGuardrailPackage Paper4dFrontier/ObstructionPredicateCandidates.lean FR193 no_closureSoundPackage_predicate_decides_four_ obstruction_families Paper4dFrontier/ObstructionPredicateCandidates.lean FR194 no_reasonableGuardrailPackage_predicate_ decides_four_obstruction_families Paper4dFrontier/ObstructionPredicateCandidates.lean FR197 classifier_agrees_on_closureEquivalent_of_ correctOnDomain Paper4dFrontier/AdmissibleCharacterization.lean FR198 no_correctOnDomain_classifier_of_orbit_gap Paper4dFrontier/AdmissibleCharacterization.lean FR199 correct_classifier_inherits_ closureLawInvariant Paper4dFrontier/AdmissibleCharacterization.lean FR200 admissibleNormalizationPredicate_has_explicit_ inhabitants Paper4dFrontier/AdmissibleCharacterization.lean FR201 closureLawInvariant_of_iff_of_ closureEquivalent Paper4dFrontier/AdmissibleCharacterization.lean FR202 exists_orbit_gap_of_not_closureLawInvariant Paper4dFrontier/AdmissibleCharacterization.lean (continued... ) 3 IDLean Handle / SourceIDLean Handle / Source FR203 closureLawInvariant_iff_no_orbit_gap Paper4dFrontier/AdmissibleCharacterization.lean FR204 no_exact_closureLawInvariant_classifier_iff_ exists_orbit_gap Paper4dFrontier/AdmissibleCharacterization.lean FR205 distinctActionCount Paper4dFrontier/DistinctActionProfiles.lean FR206 actionCount_profileCompressedSlice Paper4dFrontier/DistinctActionProfiles.lean FR207 decisionEquiv_profileCompressedSlice_iff Paper4dFrontier/DistinctActionProfiles.lean FR208 profileCompressedSlice_preserves_ exactCertification Paper4dFrontier/DistinctActionProfiles.lean FR209 profileCompressedSlice_bounded_actions Paper4dFrontier/DistinctActionProfiles.lean FR210 OrbitGapOn Paper4dFrontier/AdmissibleCharacterization.lean FR211 no_orbitGapOn_of_exact_classifiable_by_ closureLawInvariant_onDomain Paper4dFrontier/AdmissibleCharacterization.lean FR212 exact_classifiable_by_closureLawInvariant_ onDomain_iff_no_orbitGapOn Paper4dFrontier/AdmissibleCharacterization.lean FR213 no_exact_closureLawInvariant_classifier_ onDomain_iff_orbitGapOn Paper4dFrontier/AdmissibleCharacterization.lean FR214 boundedPatternScheme_holds_largeActionCount_ iff Paper4dFrontier/AdmissibleCharacterization.lean FR215 boundedPatternDefinable_eventually_constant_ in_actionCount Paper4dFrontier/AdmissibleCharacterization.lean FR216 boundedPatternDefinable_largeActionCount_ agrees Paper4dFrontier/AdmissibleCharacterization.lean 2 Claim-to-Lean Handle Mapping This section maps each paper claim to its corresponding Lean formalization. Paper claimLean handle Corollary 6.6: Constant-Optimizer Collapse Forces Trivial CertificationFR52, FR53 Corollary 2.3: Finite Basis for the Current Positive LandscapeFR3, FR29 Corollary 4.11: No Correct Tractability Classifier(no derived Lean handle found) Corollary 4.13: Orbit-Gap Completeness on Closure-Closed DomainsFR210, FR212, FR213, FR211 Corollary 5.4: Realizability Alone Cannot Be the FrontierFR7, FR8 Corollary 4.10: Reasonable Guardrail PackagesFR194 Corollary 6.3: Relevance Is Failure of Erased SufficiencyFR49, FR50 Corollary 6.4: Certification Statistics Factor Through the Quotient RelationFR41, FR43, FR44, FR42 Corollary 6.2: Sufficiency Is Relation RefinementFR48 Proposition 6.18: The Admissibility Layer Is NonemptyFR200 Proposition 6.8: Positive Affine Utility Reparameterizations Are InvisibleFR13, FR16, FR15, FR14 Proposition 4.1: Binary Pairwise Symmetry DichotomyFR120, FR118, FR119 Proposition 6.20: Bounded-Pattern Predicates Stabilize Above a Finite Action Bound FR215, FR216, FR214 Proposition 6.15: Closure Operations Preserve Exact Certification FR57, FR17, FR18, FR60, FR56, FR59, FR16, FR55, FR58, FR15, FR19, FR20 Proposition 4.2: Decision-Relevant Binary Pairwise DichotomyFR121, FR123, FR124, FR122 Proposition 3.2: Degenerate Positive CasesFR1, FR6 Proposition 6.1: Exact Certification Depends Only on the Decision Quotient Relation FR32, FR33, FR31, FR30, FR37, FR51, FR35, FR34 Proposition 6.19: Bounded Distinct Action Profiles Compress to Bounded ActionsFR206, FR207, FR205, FR209, FR208 4 Paper claimLean handle Proposition 6.9: Duplicate Actions and Duplicate States Preserve Certification FR71, FR68, FR54, FR70, FR56, FR69, FR55, FR73, FR72 Proposition 6.7: Explicit Enumeration Is Parameter-Dependent, Not StructuralFR66, FR67 Proposition 2.4: Explicit Primitive BasisFR29 Proposition 2.2: Explicit InventoryFR26, FR25, FR3, FR28, FR27 Proposition 2.5: All Independent Core Mechanisms Are Nondegenerate FR108, FR106, FR112, FR101, FR105, FR113 Proposition 2.9: Current Positive Interfaces Factor Through Role ClassificationFR4 Proposition 6.12: Invariance Alone Is Too WeakFR22, FR21, FR23 Proposition 2.6: Weak Tree Ordering Does Not Imply Width OneFR115, FR114 Proposition 3.1: Lifted Cases Introduce No New PrimitiveFR5 Proposition 6.14: Unrestricted Predicates Trivialize Exact CharacterizationFR145 Proposition 4.12: Orbit-Gap Completeness for Exact Classification(no derived Lean handle found) Proposition 4.3: Orbit-Gap TemplateFR185 Proposition 2.8: Parent-Tree Structure Gives Width-One DecompositionsFR110, FR100, FR111 Proposition 6.11: Quotient Size Is Unbounded Under RealizabilityFR24, FR38 Proposition 5.3: The Realized Quotient Is Exactly the Label RangeFR39, FR40 Proposition 6.10: Relabeling Invariance Is Forced by Exact CertificationFR17, FR18, FR19, FR20 Proposition 5.2: Every Equivalence Relation Is Optimizer-RealizableFR47, FR46, FR45 Proposition 6.13: Independent Summary Frameworks Converge on the Same Structural Core FR178, FR181, FR182, FR180, FR179 Proposition 2.7: Cyclic Dependencies Recover HardnessFR110, FR100, FR111, FR115 Proposition 6.5: Zero-Distortion Summaries Refine the Optimizer QuotientFR177, FR176 Theorem 4.8: Admissible Collapse Across the Four Obstruction FamiliesFR190 Theorem 4.9: Closure-Sound Package No-GoFR193 Definition 6.17: Admissible Normalization PredicateFR197, FR199, FR198 Theorem 2.1: Explicit Partition of the Current Positive LandscapeFR26, FR25, FR1, FR2, FR28, FR27 Theorem 4.4: Dominant-Pair Admissible No-GoFR186 Theorem 4.6: Ghost-Action Admissible No-GoFR188 Theorem 5.1: Every Labeling Kernel Is Optimizer-RealizableFR7, FR8 Theorem 4.5: Margin-Masking Admissible No-GoFR187 Theorem 4.7: Offset Admissible No-GoFR189 Notes: (1) Full rows come from theorem-local inline anchors in this paper. (2) Derived rows are filled by dependency/scaffold claim-handle derivation (same paper-handle label across proof dependencies). (3) Unmapped means no local anchor and no derivable dependency support were found. Auto summary: mapped 45/47 (full=45, derived=0, unmapped=2). 5