Hiddenness as a Structural Law of Emergence

Abstract

On a finite set of computation histories, two families of tests induce two equivalence relations: a current quotient, from tests that read only what is visible at the present stage, and a predictive quotient, from tests that may also read witness and continuation data. We study these quotients when the histories are generated by a deterministic procedure with an internal state and a class of loops acts on both. The main statement is a four-clause lemma under six explicitly stated premises on the carrier and the loops. It concerns the loop-action asymmetry—a loop moving the predictive class while fixing the current class—and a binary visibility predicate, exposure, which holds when some current test factors through a function of the internal state that is non-constant on the states reached. Under exposure the asymmetry disappears; without exposure and with a strictly finer predictive quotient it persists; and without strict refinement the two quotients agree. These clauses are short consequences of the premises: the first composes three of them, the second and the fourth (that the coupling strength used to generate the histories plays no role) restate premises, and two premises follow from the definitions of the quotients, one of them under a mild extension hypothesis. The premises are not derived for any class of algorithms; the contribution is their formulation, and exposure measures factorization through the internal state rather than the hiddenness of a particular datum. A second theorem, a minimal example, exhibits a finite carrier in which two histories with different predictive classes and the same current class have equal selected Boolean outputs, so strict refinement of histories can vanish when one passes to outputs. No map to the complexity classes P or NP is constructed and no consequence for P ≠ NP is claimed. The numbered theorems, lemma and propositions are formalized in Lean 4, with the premises as explicit hypotheses and "polynomial time" as a declared label.