We formalise computational free will by separating locally constrained admissibility from the selection of one global continuation. Global sections of a finite choice presheaf form an admissible set, GLUE; SELECT singles out the continuation realised at a pre-identified occurrence. A uniform trace relation certifies that continuation efficiently after the act, although it is assumed not to be uniformly anticipable in polynomial time from the prior occurrence input. Under explicit uniformity, balance, historical-completeness, and unique-projection assumptions, this trace defines a total FNP search relation with no deterministic polynomial-time selector. Thus existence of computational free will in the stated sense implies a separation between polynomially verifiable and polynomially solvable search, and hence that P differs from NP. The result is conditional and gives no unconditional class separation.

翻译：暂无翻译