Observer Determinacy of Termination Certificates: Sufficient Statistics, Blackwell Comparison, and Simple Projections for Step-Duplicating Recursion
Moses Rahnama
cs.LO
Apr 21, 2026 · v5
TL;DR
Results on observer licensing, Blackwell comparison, and termination-orientation barriers for the step-duplicating recursor are mechanized in Lean 4, with named module identifiers.
Abstract
The recursor $F(x,y,0)\to x$, $F(x,y,S(n))\to G(y,F(x,y,n))$ terminates and is confluent under all contexts, yet every orienting expression of the stated direct-measure grammar ignores the copied argument $y$; a payload-sensitive orienter exists outside it. An observer $q:X\to Q$ licenses a target $P:X\to V$ when $P$ is constant on its fibers. For a sound and complete language whose observer sees the input dimension, operational inexpressibility is equivalent to two context-sharing worlds with equal observations and different target values; each hypothesis is necessary. The counter observer licenses an orienting target outside the grammar's definable class. On finite sets with a rational prior, the least weight refused by a repair with $k\ge1$ side symbols is $1-V_k(μ)$, where $V_k$ is the best probability of guessing the target within $k$ tries per observation; this curve is weakly decreasing and convex. For set-valued certificate tasks with a certificate at every state, the least side alphabet is the maximum fiber chromatic number of the hypergraph of subsets whose common certificate set is empty. Observer refinement equals deterministic Blackwell comparison, and licensing equals statistical sufficiency under deterministic observation and a full-support prior. In every faithful recursor realization, natural-valued root and extracted-call rankings each have infinitely many full-order classes, and counter-determined extracted-call rankings have one. The occurrence-role channel separates the active and frame copies of one payload and resolves one bit under the uniform binary law. Every signature homomorphism constant in the counter slot identifies two terms that the counter projection separates. The declared cost model gives quadratic omitted mass against linear residual work. The general results and recursor instances are formalized in Lean 4.
Problem
The step-duplicating recursor F(x,y,S(n)) → G(y,F(x,y,n)) terminates, yet no direct whole-term measure in a stated grammar can orient it, because every such measure ignores the copied argument y. The paper asks why this happens and how to characterize which observations of a term are enough to certify termination.
Approach
An observer q licenses a target P when P is constant on q's fibers. The paper uses this notion to prove an equivalence between operational inexpressibility and the existence of two indistinguishable worlds with different target values. It relates observer refinement to deterministic Blackwell comparison and licensing to statistical sufficiency. It also gives quantitative bounds: guessing-probability curves for repairs that use side symbols, and fiber chromatic numbers for set-valued certificate tasks. The general results and recursor instances are formalized in Lean 4 modules such as Meta/SchemaOperationalIncompleteness.lean and Meta/SchemaWitnessOrder.lean, building on a companion Lean artifact.
Results
Direct aggregation is proved operationally inexpressible at the step-argument dimension, and the counter observer is shown to license an orienting target outside the grammar. Further results:
- The least refused weight is 1 − V_k(μ), and this curve is weakly decreasing and convex.
- Natural-valued rankings in faithful realizations are shown to have infinitely many full-order classes.
- Signature homomorphisms that are constant in the counter slot identify two terms that the counter projection separates.