Source-linked AI summary
Computational free will as global selection: from sheaf-theoretic gluing to a conditional separation of P and NP
Jerome Clech
TL;DR
The paper asks how to formalise a choice that is constrained by prior information without being computationally anticipated. It separates admissible global continuations from the realised selection and adds a uniform retrospective trace. Under the stated assumptions, this yields a total FNP search relation without a deterministic polynomial-time selector, conditionally implying P ≠ NP.
Problem
The paper addresses how to distinguish multiple globally admissible continuations from the particular continuation realised at an occurrence.
Method
It formalises GLUE and SELECT using a finite local-to-global model, a uniform trace relation, and unique projection of accepted certificates onto the realised continuation.
Results
LAc implies FPsearch ≠ FNPsearch, and hence P ≠ NP, when the specified uniformity, balance, traceability, and unique-projection assumptions hold.
Takeaways & Limitations
The paper isolates a conditional bridge from computational free-will processes with retrospective certification and non-anticipability to a search-class separation.
Takeaways & Limitations
The result is conditional and does not establish human, artificial, or abstract free will or an unconditional separation of P and NP.
Abstract
from arXiv · showhide
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.
1. Introduction
The paper formalises computational free will by separating admissible global continuations from the selection of the continuation realised at a particular occurrence. Under explicit assumptions, this distinction conditionally yields a separation between polynomially verifiable and polynomially solvable search, and hence P ≠ NP.
- Core distinction: GLUE characterises global continuations compatible with local constraints, while SELECT singles out the continuation that becomes the historical outcome.The paper uses sheaf-theoretic language for local-to-global structure and finite constraint satisfaction to make it effective.
- Definition: LAc requires at least two admissible continuations, an outcome-independent occurrence identifier, realised selection, retrospective certification, and polynomial-time non-anticipability.The notion concerns encoded choice processes rather than metaphysical free will.
- Main result: LAc implies FPsearch ≠ FNPsearch under the paper’s uniformity, balance, traceability, and unique-projection assumptions.The first implication is the paper’s formal contribution; the search-to-decision consequence is standard under stated conventions.
- Safeguards: The sheaf-theoretic motivation and restricted Tseitin witness do not independently prove P ≠ NP or establish universal non-anticipability.The general theorem remains conditional on an infinite uniform family satisfying LAc.
2. Sheaf-theoretic conceptual framework
The conceptual framework treats choice as a local-to-global problem in which compatible local determinations may admit multiple global continuations. Because admissibility alone does not identify the realised continuation, an additional selection operation is required, but this conceptual argument does not yet establish a complexity lower bound.
- Local-to-global regimes: A choice problem asks whether compatible local determinations admit global sections and whether those sections are unique.The framework distinguishes unique globalisation, obstruction to gluing, and plurality of globalisations.
- Plurality of globalisations: The relevant regime is plurality: at least two globally coherent continuations remain compatible with the same prior determinations.This differs from both causal absence and inconsistency.
- Selection: When compatible globalisations have cardinality at least two, the prior sheaf structure does not itself single out the realised continuation.The proposition therefore requires an additional selection operation for actualisation.
- Scope: The conceptual argument does not establish polynomial-time bounds: neither categorical equivalence nor an obstruction automatically supplies a computational lower bound.The paper proceeds to finite models, GLUE/SELECT separation, certification, uniformity, and complexity classes.
3. Computational free will
The paper defines computational free will, LAc, as a property of encoded choice processes whose prior state leaves multiple structured continuations while one is realised and retrospectively certifiable. Its non-anticipability condition is computational rather than ontological and becomes complexity-theoretic only when combined with independent traceability requirements.
- Definition: LAc is defined for q = (x, e), where x encodes prior determinations and e is a pre-registered occurrence identifier independent of the realised continuation.The identifier may be a session or experiment identifier but is neither a hidden seed nor post-event information.
- Conditions: The prior state determines a globally coherent set GLUE(x) with at least two continuations, while the occurrence realises one value SELECT(q) in that set.The six conditions include prior determinations, admissible plurality, global coherence, singularisation, traceability, and non-anticipability.
- Traceability: A fixed uniform predicate uses a finite post-actualisation trace to certify the realised continuation at its occurrence.This formalises verification after the act without making the continuation uniformly predictable beforehand.
- Non-anticipability: Non-anticipability excludes a uniform polynomial-time procedure that computes SELECT from q across the encoded family and admissible representation changes.It is distinct from ontological indeterminacy and does not by itself imply a search-class separation.
- Exclusions: The definition excludes unresolved plurality, untraceable singularisation, randomness alone, and uniformly polynomial-time deterministic preference functions.These phenomena fail different components of the LAc conditions.
4. A finite sheaf model and its associated CSP
The paper models finite sheaf choices as a constraint-satisfaction problem: global sections are exactly assignments satisfying every local relation. Their cardinality distinguishes inconsistency, prior singularisation, and multiple admissible continuations, but does not select one.
- The ambient assignment presheaf is a sheaf, so compatible local assignments glue uniquely to a global assignment.
- A finite choice model assigns variables finite domains and local constraint relations on contexts.
- The associated CSP uses the same variables, domains, and constraint relations as the finite choice model.
- Global sections are canonically bijective with solutions of the associated CSP.
- The gluing set is empty for inconsistency, singleton under prior singularisation, and non-singleton when several admissible continuations remain.
5. From gluing to selection
The paper separates GLUE, which identifies continuations compatible with prior constraints, from SELECT, which identifies the continuation realised at a specified occurrence. This distinction is structural rather than a complexity lower bound and requires certification beyond admissibility.
- For an occurrence input, GLUE answers which continuations satisfy all constraints, whereas SELECT answers which continuation is historically realised.
- A selection operator maps an occurrence input to the continuation realised at its identified occurrence.
- The act is represented as adding the realised continuation to the prior state and occurrence identifier.
- Selection is not equated with arbitrary randomness or with a polynomial-time preference rule fixed by the prior state.
- When at least two admissible continuations exist, the GLUE set alone cannot identify the historically realised member.
- A fixed trace relation is introduced so the realised value can be certified after the act rather than inferred from admissibility alone.
6. Traceability and retrospective verification
The paper makes retrospective certification precise with a fixed polynomial-time trace predicate: post-act witnesses certify the realised continuation while remaining absent from the prior input. Historical completeness, soundness, unique projection, and polynomial balance place the relation in FNP search, while non-anticipability rules out an efficient selector.
- Admissibility alone does not certify actualisation, because a member of GLUE(x) need not equal SELECT(q).
- A trace system uses a fixed uniform predicate V to certify which continuation was historically realised at an occurrence.
- Historical completeness supplies an accepted trace, soundness keeps accepted continuations in GLUE(x), and unique projection prevents different accepted continuations for one occurrence.
- Polynomial balance and polynomial-time verification make the selection relation polynomially balanced and decidable.
- The trace is retrospective: the verifier is fixed beforehand, but the realised continuation and valid trace become available only after actualisation.
- The verification proposition alone does not imply class separation; that conclusion additionally requires the independent non-anticipability condition.
7. A restricted witness: Tseitin formulas on expanders
Tseitin formulas on bounded-degree expanders provide a restricted local-to-global obstruction: locally extendible constraints can be globally inconsistent, and their specified CNF encodings require exponential-size resolution refutations. The witness illustrates proof complexity rather than universal hardness of selection.
- Tseitin formulas are used as an explicit model in which locally simple constraints create a global obstruction.
- Summing all vertex constraints cancels each edge variable twice, exposing a necessary global charge condition.
- When the total charge is odd, proper local regions may be extendible even though the full system is inconsistent and has no global section.
- Expansion preserves large boundary interfaces for sufficiently small vertex sets, motivating the local-to-global interpretation without asserting a new sheaf-width invariant.
- A restricted family of contradictory Tseitin encodings on bounded-degree expanders requires exponential-size resolution refutations.
- The theorem applies to a specified encoding and proof system, not every representation of the parity structure or selection itself.
8. Effective changes of representation
The section makes non-anticipability representation-robust by restricting comparisons to uniformly translatable encoding schemes with polynomial overhead. Under effective equivalence, polynomial-time computability of the selected continuation transfers between representations, so non-computability is preserved.
- Scope: The argument does not infer a representation-independent width lower bound and retains the encoding- and proof-system-specific scope of Theorem 7.1.The general claim relies on condition (A) and Lemma 8.2 rather than on one syntax-specific lower bound.
- Admissible effective equivalence: Semantic equivalence alone is insufficient because an encoding may contain the answer or require superpolynomial work to obtain it.The comparison therefore concerns entire encoding schemes rather than abstractly equivalent representations.
- Admissible effective equivalence: Effective equivalence requires uniform polynomial-time translations for instances and continuations in both directions, with polynomially bounded size distortion.The translations must preserve valid instances, continuation correspondence, and certified actualisation.
- Invariance of polynomial computability: A polynomial-time selector under one effectively equivalent encoding yields a polynomial-time selector under the other through translation, selection, and inverse continuation translation.Certified actualisation and unique projection ensure that the transferred continuation remains the selected one.
- Invariance of polynomial computability: Non-computability in polynomial time is therefore preserved under admissible effective equivalence by contraposition.The robust condition requires that no uniformly polynomial-time selector computes the certified continuation under any effectively equivalent representation.
9. The search relation and the conditional separation
The section constructs a total, polynomially verifiable search relation whose accepted outputs project uniquely to the historically realised continuation. Under the LAc assumptions, any deterministic polynomial-time selector would compute SELECT, contradicting non-anticipability and yielding the conditional implication FPsearch ≠ FNPsearch, hence P ≠ NP.
- Search relation: The selected continuation is represented through a certified-actualisation relation rather than an undefined mathematical oracle.The search formulation uses the relation introduced earlier to encode the physical event computationally.
- Search relation: FNPsearch contains polynomially balanced, polynomial-time decidable relations, while FPsearch additionally requires a deterministic polynomial-time selector.The convention distinguishes potentially multivalued certificate pairs from the uniquely projected selected value.
- Search relation: SEARCHSEL asks for an accepted pair (s, τ), and under the stated assumptions it belongs to FNPsearch.The relation is polynomially decidable, historically complete, sound with respect to GLUE(x), and uniquely projected onto s.
- Functional projection: Unique projection onto s is indispensable because multiple traces may certify one actualisation, but a solver must not be able to return another admissible continuation.Witness uniqueness is unnecessary; uniqueness is required only for the projected selected value.
- Total search problem: Extending the relation with a default output ⊥ on invalid inputs makes it total over all binary strings and places it in TFNP, hence FNP.On valid instances, the extension coincides with SEARCHSEL.
- Conditional separation: SEARCHSEL ∈ FPsearch would imply SELECT ∈ FP because projecting any accepted solver output onto its first component recovers the unique certified value.The extraction is linear in the output length, and historical adequacy identifies the projection with SELECT(q).
- Conditional separation: Under the theorem’s uniformity, balance, verification, historical-completeness, unique-projection, and non-anticipability assumptions, FPsearch ≠ FNPsearch.The resulting total FNP problem cannot have a deterministic polynomial-time solver without contradicting condition (A).
- Conditional separation: Because P = NP would imply FNPsearch = FPsearch through polynomial-time witness reconstruction, the functional separation conditionally yields P ≠ NP.The conclusion is explicitly an implication from the LAc assumptions, not an unconditional class separation.
10. Conclusion
The conclusion presents computational free will as a local-to-global choice structure separating admissible continuations from historical selection. It identifies a conditional bridge from uniform retrospective certification and non-anticipability to a total hard FNP search relation, while leaving existence and adequacy as open questions.
- Conclusion: Computational free will is formalised as prior constraints permitting several global continuations without efficiently predicting which one will be realised.GLUE captures admissibility, whereas SELECT captures historical singularisation.
- Conclusion: A fixed trace relation makes the realised continuation efficiently certifiable after actualisation, and unique projection makes the search functional at the selected-value level.The certificate may include a trace, while the projected continuation remains unique.
- Conclusion: Tseitin formulas on expanders illustrate how simple local constraints can generate a hard global obstruction in a restricted explicit setting.Effective equivalence prevents treating this illustration as a representation-independent lower bound.
- Open questions: The remaining frontier is to establish an adequate non-artificial LAc family, specify a trace without encoding the selected value in advance, and prove non-anticipability independently.These questions define the stated programme linking sheaf theory, search complexity, information flow, cognition, and formal analysis.