Explainable but Not Contestable

Abstract

A public rule can remain explainable while case and appeal evidence cannot determine its outcome.

Theorem 1.1 (A public rule need not make its outcome contestable).

$$\begin{array}{c}\exists q_R,q_L,q_C,q_A:Bool\times Bool\to Bool,T:Bool\times Bool\to Bool,\\ \mathrm{Refines}\left(q_R,q_L\right)\wedge (\forall x,y:Bool\times Bool,q_A(x)=q_A(y))\wedge \\ \neg \mathrm{Refines}\left(\mathrm{canonicalTargetReadout}\left(T\right),\mathrm{conceptJoin}\left(q_C,q_A\right)\right)\wedge \\ \exists x,y:Bool\times Bool,T(x)\ne T(y)\wedge \mathrm{conceptJoin}\left(q_C,q_A\right)(x)=\mathrm{conceptJoin}\left(q_C,q_A\right)(y).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Appeal/ExplainableNotContestable.explainable_not_contestable (✓ std3). ∎

Source. Repository-derived.

Commentary.

Take the state space to be two Boolean coordinates. The rule, its public language, and the case record all reveal the first coordinate, so the rule is fully explainable through the public language.

The appeal readout is constant and therefore contributes no new distinction. The classification target is the second coordinate, which the joined case-and-appeal evidence does not reveal.

In particular, the states (false, false) and (false, true) have the same case record and the same appeal evidence, but their target outcomes differ. Hence no function of the available joined evidence can recover the canonical target readout.

This finite witness separates publication of the governing rule from contestability of an individual outcome: knowing the rule does not supply the case-specific coordinate needed to challenge the classification.

References

• Truth anchor: D5/S3/ConceptDynamics/Appeal/ExplainableNotContestable.explainable_not_contestable
• Dependency: D5/S3/ConceptDynamics/Interventions/RedundantAppealDefectPersistence
• Dependency: D5/S3/ConceptDynamics/Sufficiency/UniversalSufficiencyFactorization