Syntactic Separation Implies Computational Indistinguishability: An Abstract Obstruction Theorem Fabio Francesco Gabriele Buono Independent Researcher ORCID: 0009-0004-9199-2793
arXiv:2606.29177v1 [cs.LO] 28 Jun 2026
Preprint. June 30, 2026
Abstract We prove that syntactic separation implies computational indistinguishability. A local syntactic system R acts on terms within radius r0 without consulting any model; when two Skolem functions are syntactically separated in R, no derivation can prove their equivalence (Case 1), and any sound local extension requires Ω(n) steps, improving to Ω(2n ) under clause-per-configuration encoding (Case 2). Both bounds are new: the derivation-length lower bound does not appear in prior work on Skolemization or saturation proving, and the cryptographic reading, syntactic separation as ciphertext indistinguishability, derivation cost as negligible advantage, is original. The same obstruction, as formal instances of Case 1 and Case 2, governs the Natural Proofs barrier of Razborov and Rudich, the Type Omitting Theorem, and the unconditional AC0 barrier of Loff et al. [14].
Contents 1 Introduction 1.1 The phenomenon . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 The result . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4 Relation to prior work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.5 Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2 2 3 3 3 4
2 Definitions 2.1 Terms and positions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Local syntactic systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.3 Protected positions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.4 Syntactic invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.5 Skolem functions and syntactic separation . . . . . . . . . . . . . . . . . . . . . .
4 4 5 6 6 7
3 Main Theorem
8
4 Instantiations 4.1 Case 1: Superposition calculus and open induction . . . . . . . . . . . . . . . . . 4.2 Case 2: Gadget instances and the exponential lower bound . . . . . . . . . . . .
11 11 12
5 Cryptographic Connection 5.1 Formal correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 Correspondence table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
13 13 14
1
6 Cross-Domain Connections 6.1 Type theory and the Type Omitting Theorem . . . . . . . . . . . . . . . . . . . . 6.2 Circuit complexity and the Natural Proofs barrier . . . . . . . . . . . . . . . . .
16 16 18
7 Conclusions
21
8 Open Questions
21
A Full Gadget Construction A.1 Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A.2 Verification of Lemma 4.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
23 23 23
B Proofs of Auxiliary Lemmas
24
1
Introduction
1.1
The phenomenon
A syntactic system acts on the shape of expressions. A semantic property concerns what those expressions mean in a model. The two can be in conflict: a property that is visible to the model may be completely invisible to the syntactic system, even when every derivation the system can perform passes through terms in which the property is present. This paper proves that this conflict is not an accident of specific systems but a structural phenomenon: whenever a property is protected from the rules of a syntactic system, no derivation can cross the barrier, and any extension of the system that tries to do so pays an exponential price. The phenomenon appears across mathematics in forms that look unrelated: • In proof theory, the Skolem functions witnessing two different proofs of ∀x ∃y. ϕ(x, y) are semantically equal but a saturation-based prover cannot derive their equality, the relevant information is locked inside Skolem constants the rules cannot touch. • In cryptography, a ciphertext produced by the Mixed-Radix One-Time Pad [7] achieves Shannon perfect secrecy because the decomposition basis B encodes a numerical fact invisible to any syntactic test on the ciphertext; the same structure underlies the original construction of [12]. • In type theory, the Type Omitting Theorem says that a theory omits a type Φ(x) if and only if Φ is not principal, no syntactic formula pins it down. A constructive type system is blind to extensional properties of the functions it types: it sees the proof term, not the function computed (Typological Invariance Principle, Remark 6.2). • In circuit complexity, the Natural Proofs barrier of Razborov and Rudich shows that no proof technique that is both useful (holds for random functions) and constructive (checkable in polynomial time) can establish a super-polynomial circuit lower bound, the semantic invariant of circuit complexity is protected from every local syntactic inspection of the circuit graph. These are not analogies. They are instances of a single structural theorem, proved here in its abstract form and applied to each domain in Section 6.
2
1.2
The result
This paper proves an abstract theorem: whenever a local syntactic system R acts on a term structure in which a semantic invariant is protected from all rules, no derivation in R can reach that invariant (Case 1), and any sound extension that overcomes this barrier requires Ω(n) derivation steps, growing with the number of independent witnesses, and improving to Ω(2n ) under clause-per-configuration encoding (Case 2). The proof-theoretic structure of Case 2 is precisely the structure of computational hiding in cryptography: syntactic separation between two Skolem functions is ciphertext indistinguishability, and the derivation cost lower bound is the adversary’s negligible advantage. The starting point is [1], which isolates the mechanism for a specific calculus. That work resolves an open question of [2], the incomparability of open induction (OI) and clause set cycles (TCSC ), by observing that the addition rules fire only when the first argument of + is 0 or a successor, so a Skolem constant is permanently unreachable. From this observation, [1] extracts the Syntactic Invariance Principle (SIP, Lemma 5 of [1]). The present paper takes SIP as its structural starting point and proves something strictly stronger: a two-case theorem parametric in the signature, locality radius, and model, which applies to any rewriting calculus and yields the cryptographic and complexity-theoretic consequences described above. The formal framework for the structural blindness argument is the observational hierarchy of [10]: R defines a constrained observer OR ≺ O⊤ blind to positions in F. Proposition 9.6 of [10] shows observer-constrained classes collapse unconditionally: under the profile observer Oprof (which maps a string to its symbol-count vector), POprof = NPOprof ⊊ P. Theorem 3.1 is an instance of this collapse in the setting of term rewriting and Skolemization; whether it follows as a formal corollary of Proposition 9.6 is Question (Q6).
1.3
Contributions
(1) Abstract framework. We formalize local syntactic systems, protected positions, and syntactic invariants (Section 2) parametrically in the signature Σ, locality radius r0 , and model M. This generality is what allows the same theorem to instantiate as an impossibility result in proof theory, a hiding bound in cryptography, and a barrier result in circuit complexity. (2) Two-case obstruction theorem. Theorem 3.1 establishes: • Case 1 (impossibility): no derivation in R proves f ≡M g when the two Skolem functions are syntactically separated (subsumes [1]; Corollary 4.4); • Case 2 (lower bound): any local extension R′ of R requires L ≥ Ω(n) steps, improving to Ω(2n ) under clause-per-configuration encoding (Corollary 4.6). (3) Cryptographic connection. Section 5 establishes a formal correspondence between the proof-theoretic structure of Theorem 3.1 and computational hiding in cryptography, and proves a non-extraction corollary (Corollary 5.6). (4) Cross-domain connections. Section 6 shows that the Type Omitting Theorem and the Natural Proofs barrier of Razborov and Rudich are instances of the same obstruction. The result of [14] (the first unconditional Natural Proofs barrier) is a quantitatively precise instantiation of Corollary 6.3(i) for AC0 -natural proofs, and provides the first concrete confirmation of the observational framework in circuit complexity.
1.4
Relation to prior work
Proof theory. Case 1 takes SIP [1] as its structural starting point but applies it in a strictly more general setting, arbitrary local syntactic systems, not only the superposition calculus, and 3
with a formal two-case structure not present in [1]. Case 2 (the derivation-length lower bound) is entirely new. Prior work on clause set cycles [2, 4, 3, 5] studies provability and unprovability of specific formulas in specific proof systems; it does not establish lower bounds on derivation length for families of extensions of a given system, which is what Case 2 provides. Cryptography. The correspondence between the proof-theoretic structure and computational hiding is new. The Mixed-Radix One-Time Pad of [7] is a known construction; what is new here is the identification of its security as an instance of Case 1 of Theorem 3.1, placing it on the observational axis rather than the computational one. Natural Proofs. The Razborov–Rudich barrier [13] is a known result. The present paper does not reprove it. What is new is the following: • An unconditional lower bound of Ω(n) (Corollary 6.3(i)) on the inspection cost of any large and constructive technique, requiring no pseudo-random generator assumption. This bound does not appear in [13]. A sharper quantitative bound for the subclass of AC0 -natural proofs via a different technique is obtained in [14]; that result is an instance of Corollary 6.3 made quantitatively precise for that specific subclass. • A structural separation: the framework isolates precisely which step requires the PRG (supplying 2n locally indistinguishable instances) and which does not (the blindness of any local technique to circuit complexity). This separation is not made explicit in [13]. • A unifying explanation: both the barrier and the lower bound are consequences of the observational blindness of P to the circuit complexity of f . The Natural Proofs barrier is not a computational phenomenon but an observational one, and this is why it persists regardless of which of Impagliazzo’s worlds we inhabit. Type theory. The Type Omitting Theorem is classical. What is new is Corollary 6.1: the identification of extensional blindness in constructive type systems as an instance of Case 1, and the lower bound on any decision procedure for extensional equality as an instance of Case 2. Unification. No prior work treats proof theory, cryptography, type theory, and circuit complexity as instances of a single abstract theorem. The contribution of Section 6 is not to reprove known results but to show that they share a common structure, a constrained observer, a protected semantic invariant, and an impossibility or lower bound that is structural rather than computational, and that this structure is captured exactly by Theorem 3.1.
1.5
Organization
Section 2 gives all definitions. Section 3 states and proves Theorem 3.1. Section 4 provides instantiations for proof theory. Section 5 develops the cryptographic connection. Section 6 develops the cross-domain connections. Section 7 summarizes the conclusions. Section 8 lists open questions. Appendices A and B contain the gadget construction and auxiliary proofs.
2
Definitions
2.1
Terms and positions
Definition 2.1 (Signature and terms). A signature Σ is a finite set of function symbols, each with a fixed arity. Let V be a countable set of variables disjoint from Σ. The set T (Σ, V ) of terms over Σ and V is defined inductively:
4
• every x ∈ V is a term; • if f ∈ Σ has arity k ≥ 0 and t1 , . . . , tk ∈ T (Σ, V ), then f (t1 , . . . , tk ) is a term (constants are symbols of arity 0). Definition 2.2 (Positions). For a term t ∈ T (Σ, V ), the set Pos(t) ⊆ N∗ of positions is defined by: • ε ∈ Pos(t) (the root position); • if t = f (t1 , . . . , tk ) and p ∈ Pos(ti ), then i·p ∈ Pos(t). The subterm of t at position p is written t|p . The term obtained from t by replacing t|p with s is written t[s]p . The tree distance d(p, q) between two positions p, q ∈ Pos(t) is the number of edges in the unique path between them in the tree structure of t. Definition 2.3 (Context of radius r). For t ∈ T (Σ, V ), p ∈ Pos(t) (Definition 2.2), and r ∈ N, the context of radius r around p in t is the partial function Br (p)(t) := q 7→ t|p·q q∈N∗ , p·q∈Pos(t), d(p,p·q)≤r , (equivalently, |q| ≤ r, where |q| is the number of steps from p to p·q) mapping each extension q of p within distance r to the corresponding subterm t|p·q . Two terms t and t′ have equal contexts of radius r at p if Br (p)(t) and Br (p)(t′ ) have the same domain and agree as functions on that domain (i.e., they are equal as partial functions, including having the same set of defined positions). Example 2.4 (Contexts). Let t = s(a + b) and p = 1 (the position of a+b). Then B1 (p)(t) maps: ε 7→ a+b (the subterm at p itself, i.e., q = ε); 1 7→ a (left child, q = 1); 2 7→ b (right child, q = 2). The context does not include the parent s(a+b), since the parent is a prefix of p, not an extension: Definition 2.3 ranges over extensions q with p·q ∈ Pos(t), i.e., descendants of p, not ancestors. B0 (p)(t) maps only ε 7→ a+b.
2.2
Local syntactic systems
Definition 2.5 (Local syntactic system). A local syntactic system is a tuple R = (Σ, V, Rules, r0 ) where Σ and V are as in Definition 2.1, r0 ∈ N is the locality radius, and Rules is a finite set of rewriting rules. Each rule ρ ∈ Rules is specified by a finite left-hand side pattern ℓρ ∈ T (Σ, V ) and a finite right-hand side rρ ∈ T (Σ, V ), and defines a partial function on pairs (t, p) as follows. Rule ρ is applicable at position p in term t if there exists a substitution σ (a map V → T (Σ, V )) such that σ(ℓρ ) = t|p ; when applicable, it produces ρ(t, p) := t[σ(rρ )]p . We require the following two conditions. (i) Locality. The applicability of ρ at (t, p) depends only on Br0 (p)(t) (Definition 2.3). That is, if Br0 (p)(t) = Br0 (p)(t′ ) as partial functions, then ρ is applicable at p in t if and only if it is applicable at p in t′ . (ii) Model independence. The applicability of ρ at (t, p) depends only on the syntactic form of Br0 (p)(t), not on the truth value of any formula in any model.
5
A derivation in R from a clause set S is a finite or infinite sequence S = S0 , S1 , S2 , . . . where each Si+1 is obtained from Si by selecting a term t appearing in some literal of some clause C ∈ Si , choosing a position p ∈ Pos(t), and applying rule ρ ∈ Rules at p in t; the literal containing t is updated by replacing t with ρ(t, p), producing a new clause C ′ , and setting Si+1 = Si ∪ {C ′ }. The length of a finite derivation is the number of rule applications. Example 2.6 (Superposition calculus as a local system). The superposition calculus over the signature Σ = {0, s, +} with rules 0+x=x s(x) + y = s(x + y)
(A1) (A2)
is a local syntactic system with r0 = 1. Each rule inspects the outermost function symbol of the first argument of +: this symbol lies within distance 1 of the application position p in t (i.e., within B1 (p)(t)). Both left-hand sides are finite; applicability does not consult any model. Definition 2.7 (Soundness). Let M be a first-order Σ-structure. A local syntactic system R is sound with respect to M if every clause derivable by R from a set of clauses that are valid in M is also valid in M (a clause is valid in M if every ground instance of its disjunction is satisfied by M). Remark 2.8 (Theory-relative soundness). Alternatively, one may fix a theory T and require that every clause derivable by R from axioms of T is valid in every model of T . This is equivalent to soundness with respect to every model of T . In what follows we work with a fixed model M; the theory-relative version is formally analogous and all results carry over.
2.3
Protected positions
Definition 2.9 (Protected set). Let R = (Σ, V, Rules, r0 ) be a local syntactic system. A set of positions F is protected with respect to R if it satisfies the following two conditions for every term t and every p ∈ F ∩ Pos(t): (i) No rewriting at p. No rule ρ ∈ Rules is applicable at position p in t. (ii) No rewriting inside p. No rule ρ ∈ Rules is applicable at any position q ∈ Pos(t) such that q is a proper extension of p (i.e., q = p · q ′ for some nonempty q ′ ∈ N∗ ), meaning no rule rewrites inside the subterm t|p . In particular, F is not a fixed set of strings in N∗ ; it is a predicate on pairs (t, p) with p ∈ Pos(t), which must hold uniformly across all terms appearing in any derivation from R. Concretely, one writes p ∈ F (t) to mean that position p in term t is protected. Remark 2.10 (Protected sets are a property of R, not an axiom). Definition 2.9 is a property that can be verified by inspecting the left-hand sides of the rules in Rules. It is not an additional axiom imposed on R. In concrete systems, one verifies it by checking that certain unification problems have no solution (e.g., first-symbol clashes; see Section 4). Example 2.11 (Protected positions in the superposition calculus). In Example 2.6, let a and b be fresh Skolem constants (distinct from 0 and from every term of the form s(t)). The set F of positions headed by a or b is protected with respect to R. This is verified in Lemma 4.1 below.
2.4
Syntactic invariants
Definition 2.12 (Syntactic invariant). Let R = (Σ, V, Rules, r0 ) be a local syntactic system and let F be a protected set with respect to R. A property Inv of terms is a syntactic invariant for R anchored to F if the following five conditions hold. 6
(i) Local checkability. Whether Inv(t) holds depends only on the subterms of t at positions within distance r0 of some fixed finite set of reference positions. (ii) Initialization. Inv(t) holds for every term t in the initial clause set. (iii) Preservation. For every t with Inv(t) and every rule ρ ∈ Rules applicable at some position p in t, we have Inv(ρ(t, p)). (iv) Anchorage. If Inv(t) holds and Inv(t[s]p ) fails for some term s and position p, then p ∈ F. (v) Coherence. There exist two designated function symbols f0 , f1 ∈ Σ such that: no literal of any clause C with Inv holding on all its terms contains both f0 (·) and f1 (·) as subterms at comparable positions (i.e., positions syntactically equated by the literal, such as the two sides of an equation f0 (t1 ) = f1 (t2 )). (Inv is applied term-by-term to the terms in each literal. In the application to Skolemization, f0 = f and f1 = g, and the excluded literal is f (x) = g(x).) Remark 2.13 (Role of anchorage). Condition (iv) ensures that Inv is not merely preserved by R for trivial reasons (e.g., because R never produces any new terms at all), but that its violation is structurally tied to the protected set F. Without (iv), one could take Inv(t) = ⊤ (always true), which satisfies (i)–(iii) trivially (the conclusion is always true) but carries no information.
2.5
Skolem functions and syntactic separation
Definition 2.14 (Skolem functions and semantic equivalence). Let ψ = ∀x ∃y. ϕ(x, y) be a first-order formula. A Skolemization of ψ is a formula ψf = ∀x. ϕ(x, f (x)) where f is a fresh function symbol, the Skolem function for the existential quantifier. Two Skolem functions f and g (arising from two Skolemizations of ψ) are semantically equivalent in M if f (x) = g(x) holds in M for all x in the domain of M. We write f ≡M g as shorthand for this condition, and drop the subscript when M is clear from context. Remark 2.15 (Relation to [3]). The interaction between Skolem functions and induction in saturation-based theorem provers is studied in depth in [3], where Skolem symbols are shown to take the role of induction parameters. The present definition of syntactic separation (Definition 2.16 below) makes precise the structural condition under which two such parameters cannot be compared by the rewriting system. Definition 2.16 (Syntactic separation). Let R be a local syntactic system with protected predicates Ff and Fg for f and g respectively. Skolem functions f and g are syntactically separated in R if the following four conditions hold: (i) every occurrence of f in the initial clause set appears at a position in Ff ; (ii) every occurrence of g in the initial clause set appears at a position in Fg ; (iii) Ff and Fg are both non-empty; (iv) Ff and Fg are disjoint: no position (t, p) belongs to both. Remark 2.17 (On condition (iii) of Definition 2.16). Condition (iii) requires only that the protected sets are non-empty. The stronger property, that no derivation in R can produce a clause containing a literal of the form f (t1 ) = g(t2 ), is not assumed but proved in Case 1 of Theorem 3.1, using the syntactic invariant Inv and the disjointness of Ff and Fg .
7
3
Main Theorem
With all definitions in place, we can state the central result. Theorem 3.1 below applies to any local syntactic system satisfying the conditions of Section 2; the two instantiations of Section 4 verify those conditions in the specific settings of Skolemization and gadget complexity. Theorem 3.1 (Local Syntactic Obstruction). Let R = (Σ, V, Rules, r0 ) be a local syntactic system, sound with respect to a model M (Definitions 2.5 and 2.7). Let F be a set of positions protected with respect to R (Definition 2.9), and let Inv be a syntactic invariant for R anchored to F (Definition 2.12). Let f and g be Skolem functions that are semantically equivalent in M (Definition 2.14) and syntactically separated in R (Definition 2.16), with all occurrences of f in the initial clause set lying in Ff and all occurrences of g lying in Fg (where F = Ff ∪ Fg is the protected set of Definition 2.9). Assume further that f and g are fresh with respect to Σ: neither symbol appears in the left-hand side or right-hand side of any rule in Rules. Then the following two conclusions hold. Case 1 (Impossibility). No derivation in R proves f ≡ g (i.e., no derivation produces a clause asserting f (x) = g(x) for all x). Case 2 (Lower bound). Let R′ be any extension of R satisfying: • R′ is local with the same radius r0 and finite patterns; • R′ is sound with respect to M; • R′ is refutation-based: a proof of f ≡ g proceeds by refuting ¬(f (x) = g(x)) from the clause set In , and resolution of disjunctive clauses requires selecting a specific disjunct via unification. Suppose there exists a family of instances {In }n≥1 such that for each n ≥ 1: (n)
(n)
• In contains N (n) = 2n global configurations C1 , . . . , CN (n) ; (n)
• any two distinct configurations Ci
(n)
and Cj
(i = ̸ j) are indistinguishable within radius r0 , (n)
(n)
i.e., for every position p relevant to any rule of R′ , Br0 (p)(Ci ) = Br0 (p)(Cj ); (n)
• the configurations are globally distinct: Ci
(n)
̸= Cj
in M for i ̸= j.
Let c be the maximum number of globally distinct configurations that any single rule application in R′ can distinguish (a constant depending only on Σ, r0 , and the rule set of R′ , and in particular independent of n). A derivation in R′ correctly proves f ≡ g on In if it produces, for each gadget Gi , a refutation of the gadget clause by selecting a specific disjunct x = abi i as witness (thereby covering all 2n configurations). Every such derivation has length L ≥ Ω(n). Under the stronger clause-per-configuration encoding of In (see Remark 3.3 below), this improves to L ≥ Ω(2n ), at the cost of |In | = 2n . Proof of Case 1. The proof follows the structure of SIP (Lemma 5 of [1]), generalizing it to the abstract setting of Definition 2.12. By condition (ii) of Definition 2.12, Inv holds on the initial clause set. By condition (iii), every rule application preserves Inv. By induction on derivation length, Inv holds on every term in every clause reachable by R. Suppose for contradiction that a derivation D in R from the initial clause set S proves f ≡ g, i.e., produces a clause E that contains a literal of the form f (x) = g(x) for some term x. 8
By the induction argument above, every clause in every derivation from S satisfies Inv. In particular, E satisfies Inv. We derive a contradiction by showing that Inv(E) is incompatible with E containing a literal of the form f (x) = g(x). By the hypotheses of Theorem 3.1, all occurrences of f in the initial clause set lie in Ff , and all occurrences of g lie in Fg (Definition 2.16). By the freshness hypothesis of Theorem 3.1, no rule in Rules mentions f or g; consequently, rule applications cannot introduce new occurrences of f or g at positions outside Ff ∪ Fg . By Definition 2.9, no rule of R is applicable at any position in Ff or Fg . Therefore the occurrences of f remain within Ff and those of g remain within Fg throughout the derivation. (Condition (iv) (anchorage) confirms that any hypothetical violation of Inv would require acting on F, but since Inv is preserved, no such violation occurs.) By condition (v) of Definition 2.12 (coherence), with f0 = f and f1 = g as the designated symbols: no literal of any clause satisfying Inv has the form f (t1 ) = g(t2 ) (i.e., contains both f (·) and g(·) at positions equated by the literal). But E contains the literal f (x) = g(x) by assumption, which has exactly this form, a direct contradiction. Therefore no derivation of f ≡M g exists in R. Proof of Case 2. The proof proceeds in four steps. Step 1: Derivation trees. Fix n ≥ 1 and the instance In with N = 2n global configurations C1 , . . . , CN . A derivation in R′ that correctly proves f ≡ g on In must produce a correct conclusion for every configuration Ci . We represent the derivation as a tree D: internal nodes are rule applications; leaves are clauses at which the refutation goal ¬(f (x) = g(x)) is resolved for some specific input (i.e., some x = abi i is selected as the witness). Each branch of D handles a disjoint subset of configurations. Step 2: Capacity of local rules. Each rule ρ ∈ R′ is applicable based on Br0 (p)(t) for the relevant position p. Since any two distinct configurations Ci and Cj are indistinguishable within radius r0 (hypothesis of Case 2), a single application of ρ partitions the N configurations into at most c classes, where c is the number of distinct local contexts of radius r0 that ρ can observe, equivalently, the maximum number of globally distinct configurations that a single rule application can distinguish (as defined in the statement of Case 2). By the finiteness of patterns (Definition 2.5(i)), c is finite and independent of n. Step 3: Branching argument via syntactic distinguishability. We work with the specific family {In } from Lemma 4.5 (constructed and verified in Section 4.2). Recall that In is built from n independent gadgets G1 , . . . , Gn , each contributing two local constants a0i and a1i . A global configuration C(b1 ,...,bn ) selects one constant abi i from each gadget Gi . We say two configurations C(b1 ,...,bn ) and C(b′1 ,...,b′n ) are i-distinguished by a rule application if b′
the application acts on a position where the constants abi i and ai i differ. Claim 3.2. For each gadget index i ∈ {1, . . . , n} and each pair of configurations that differ only in gadget i (i.e., bj = b′j for j = ̸ i and bi ̸= b′i ), every correct derivation of f ≡ g on In must contain at least one rule application that i-distinguishes them. Proof of Claim 3.2: Suppose for contradiction that a derivation D of f ≡ g on In never applies any rule at a position where a0i and a1i differ. Then, by the opacity of a0i and a1i (Lemma 4.5(ii)), D applies the same rule applications at the same positions on C(b1 ,...,0,...,bn ) and C(b1 ,...,1,...,bn ) (the applicability of each rule is the same in both cases, since neither a0i nor a1i appears in any LHS pattern). By Lemma 4.5(i)–(ii), gadget Gi contributes the clause f (a0i ) ̸= g(a0i ) ∨ f (a1i ) ̸= g(a1i ). A refutation of ¬(f (x) = g(x)) against this clause must at some point resolve the disjunction, selecting a0i or a1i as the witness for x. Any rule performing this selection acts on the subterm
9
headed by a0i or a1i , and hence i-distinguishes the two configurations. Since D never i-distinguishes them by assumption, it cannot complete the refutation for this gadget, contradiction. □ Step 4: Derivation tree branching argument. We count the distinct rule applications in the derivation D that are required to resolve each gadget. To see this, observe that the n gadgets are resolved independently by Claim 3.2: for each gadget i, the derivation must at some point apply a rule that distinguishes a0i from a1i . By spatial separation (Lemma 4.5(ii) and Appendix A), the rule applied at gadget i lies in a context that does not overlap with any other gadget j ̸= i. Therefore the resolution of gadget i branches independently of the resolution of gadget j. We use a per-configuration trace argument. For each configuration C(b1 ,...,bn ) , define its gadget-i trace as the subsequence of rule applications in D that act at a position overlapping with gadget Gi in that configuration. By Claim 3.2, for every gadget i and every pair of configurations (C, C ′ ) differing only at gadget i, the derivation D must contain at least one rule application that i-distinguishes them. By spatial separation (Appendix A, d = 1), a rule of radius r0 overlaps with at most one gadget at a time; thus the rule i-distinguishing C and C ′ does not act on any other gadget j. Fix gadget i. The 2n−1 pairs of configurations differing only at gadget i have distinct contexts at all other gadgets. Since any rule overlapping gadget i sees only the local context of radius r0 around its application position, and since this context does not include any other gadget (spatial separation), by the Locality condition (Definition 2.5(i)), the rule i-distinguishing pair (C, C ′ ) acts only on the local context of radius r0 around its position, which lies within gadget Gi and is independent of the state of all other gadgets. Therefore for each gadget i there is at least one rule application that i-distinguishes some pair of configurations. Since the n gadgets are spatially separated, these n rule applications are distinct. Therefore L ≥ n = Ω(n). The stronger bound L ≥ Ω(2n ) follows under the clause-per-configuration encoding of Remark 3.3. Remark 3.3 (Stronger lower bound via explicit clause encoding). The bound L ≥ Ω(n) proved above follows from the gadget argument. A stronger bound L ≥ Ω(2n ) holds under a modified construction of In in which the instance contains one clause per global configuration: In = {E(b1 ,...,bn ) }(b1 ,...,bn )∈{0,1}n , where E(b1 ,...,bn ) encodes the equivalence condition for the specific configuration C(b1 ,...,bn ) . Each such clause E(b1 ,...,bn ) encodes a distinct refutation goal (the negation of f (x) = g(x) for the specific constants of configuration (b1 , . . . , bn )), and since R′ is refutation-based (as required by Case 2 of Theorem 3.1), each such goal requires at least one dedicated rule application to resolve. Since there are 2n clauses and each requires at least one step, the total derivation length satisfies L ≥ 2n = Ω(2n ). The trade-off is that |In | = 2n (the instance itself is exponential), so the lower bound holds for the derivation length relative to the number of clauses, not relative to n directly. Whether a superlinear-in-n bound holds for instances of polynomial size remains open (see Question (Q3) of Section 8). Remark 3.4 (Unconditional versus conditional lower bound). The lower bound in Case 2 is unconditional: it does not assume P ̸= NP or any other unproven hypothesis. It holds for any local syntactic system R′ satisfying the stated hypotheses, provided the family {In } with 2n locally indistinguishable configurations exists. The existence of such a family is established constructively in Lemma 4.5 (Appendix A). Remark 3.5 (Superpolynomial versus exponential). Under weaker hypotheses on the family {In } (e.g., N (n) superpolynomial but sub-exponential), the clause-per-configuration encoding (Remark 3.3) yields L ≥ N (n) = Ω(N (n)), which is superpolynomial in n. The exponential bound L = Ω(2n ) holds specifically when N (n) = 2n , as guaranteed by the gadget construction. 10
4
Instantiations
4.1
Case 1: Superposition calculus and open induction
We verify the hypotheses of Case 1 of Theorem 3.1 for the setting of [1], thereby recovering the incomparability result OI ̸⊆ TCSC as a corollary. Setup. Work in L = {0, s, +} with r0 = 1. The system R is the superposition calculus over rules (A1) and (A2) (Example 2.6), sound with respect to M = (N, 0, s, +) (standard arithmetic). Recall that OI admits recursive nonstandard models [6] and is therefore a weak theory; it proves commutativity not by strength but because W is an open identity. Clause set cycles abstract the cycle-detection methods used in automated inductive theorem proving, including the n-clause calculus of [15]. Let a and b be the fresh Skolem constants introduced in Example 2.11 (ground terms not in {0} ∪ {sn (0) | n ≥ 1}). Lemma 4.1 (Protected positions in R). Define F as the condition: a position p in any term t satisfies F if and only if t|p ∈ {a, b}. Equivalently, p ∈ F(t) := {q ∈ Pos(t) | t|q ∈ {a, b}} for each term t in the derivation. Under this definition, F is protected with respect to R: for every term t occurring in any derivation from R and every p ∈ F(t), no rule of R is applicable at p. Proof. The left-hand sides of (A1) and (A2) are 0+x and s(x)+y, requiring the first argument of + to be 0 or s(·). For any position p ∈ F, the subterm t|p is a or b, both of which are constants distinct from 0 and from every s(t′ ). The LHS of rule (A1) is 0+x, whose root symbol is +; the LHS of rule (A2) is s(x)+y, also rooted at +. For any position p ∈ F, the subterm t|p is a or b, both rooted at a or b respectively. Since + ̸= a and + ̸= b (pairwise distinct non-variable symbols), the root of each LHS cannot match the root of t|p ; this is a first-symbol clash [1, Section 3], and no substitution resolves a first-symbol clash. Therefore no rule of R is applicable at any position in F. Since a and b are constants (arity 0), they are leaves in any term tree and have no proper subterm positions; condition (ii) of Definition 2.9 (no rewriting inside p) is therefore satisfied vacuously. Remark 4.2 (Decidability in linear time). For the superposition calculus over {(A1), (A2)}, the existence of a non-trivial protected set F is decidable in linear time in the size of the clause set. The criterion is first-symbol clash: a position p is protected if and only if the subterm at p begins with a symbol that cannot unify with the first argument of + in any left-hand side. Since the left-hand sides are {0+x, s(x)+y}, any constant distinct from 0 and from the range of s qualifies in constant time. For such constants (which have arity 0), condition (ii) of Definition 2.9 (no rewriting inside p) holds trivially, since constants have no proper subterm positions. Lemma 4.3 (Syntactic invariant). Define Inv(t) as the property: every occurrence of a in t is a subterm of some a+u where u contains b, and every occurrence of b in t is a subterm of some b+v where v contains a. Then Inv is a syntactic invariant for R anchored to F in the sense of Definition 2.12. Proof. Full proof in Appendix B (Lemma B.1). Here we verify the five conditions. (i) Inv(t) depends only on the immediate subterms of each + occurrence, i.e., within distance 1 = r0 of the root of each +-subterm. (ii) The initial clause set contains only a+b = ̸ b+a, on which Inv holds: the only subterms containing a or b are a+b and b+a themselves, each of the required form. (iii) By Lemma 4.1, no rule touches positions in F, so no rule modifies a+b or b+a; Inv is preserved. (iv) Violating Inv requires moving a out of an a+u context or b out of a b+v context, both of which require acting on positions in F. (v) Coherence holds: no literal of the initial clause a+b = ̸ b+a has the form a(t1 ) = b(t2 ) (the literal is a disequation, not an equation comparing a and b as heads); by preservation, no derived clause contains such a literal. Full verification in Appendix B (Lemma B.1 (v)). 11
Corollary 4.4 (OI ̸⊆ TCSC ). The theory TCSC over rules (A1) and (A2) does not prove the commutativity of addition W : ∀x ∀y. x+y = y+x. Consequently, OI and TCSC are incomparable. Proof. a and b are semantically equivalent as witnesses for commutativity in M = (N, 0, s, +): since commutativity holds for all elements of the domain of M, we have a+b = b+a in M for any interpretation of the fresh constants a and b. The freshness hypothesis of Theorem 3.1 holds: a and b are fresh constants that do not appear in any left-hand side or right-hand side of rules (A1) or (A2). By Lemmas 4.1 and 4.3, the remaining hypotheses of Case 1 of Theorem 3.1 are satisfied. Therefore no derivation in R proves a+b = b+a; this corresponds to Lemma 9 of [1], which establishes that TCSC + {(A1), (A2)} ⊬ W . Since OI proves W (as an open identity, by standard induction on x; Lemma 8 of [1]), we obtain OI ̸⊆ TCSC . The direction TCSC ̸⊆ OI is Theorem 4.3 of [2] (the triangular numbers provide a witness provable by OI but not by TCSC ).1 Further unprovability results for clause set cycles, including a logical characterization of refutation by a clause set cycle, are given in [4]. The complete picture of the relationships between subsystems of OI, including the placement of TCSC as a restricted, parameter-free form of clause induction, is obtained in [5]. Case 1 gives an impossibility result for a specific calculus. Case 2 asks how expensive it is to escape that impossibility by extending the system, and gives a lower bound on any such escape.
4.2
Case 2: Gadget instances and the exponential lower bound
We construct the family {In } required by Case 2 of Theorem 3.1. The construction has a direct cryptographic reading: each gadget Gi contributes two locally indistinguishable configurations a0i and a1i , which function as two ciphertexts of the same plaintext. The 2n global configurations are 2n jointly indistinguishable ciphertexts; the lower bound of Case 2 is the statement that no local adversary can distinguish them in fewer than Ω(n) rule applications (improving to Ω(2n ) under clause-per-configuration encoding). This is why Section 5 is not a separate application but a restatement of the same bound in cryptographic language. The full construction and correctness proof are in Appendix A; here we state the key lemma and the resulting lower bound. Lemma 4.5 (Gadget family). For every n ≥ 1, there exists a set of clauses In satisfying: (n)
(n)
(i) In encodes N (n) = 2n global configurations C1 , . . . , C2n ; (n)
(ii) for any two distinct Ci
(n)
and Cj , and for every position p at which any rule of R′ is (n)
(n)
applicable (in the sense of Definition 2.5), Br0 (p)(Ci ) = Br0 (p)(Cj ); (n)
(iii) Ci
(n)
̸= Cj
in M for i ̸= j. r
The constant c (maximum configurations distinguished per rule application) satisfies c ≤ |Σ|k 0 where k is the maximum arity of any symbol in Σ, and in particular c is independent of n. (The r bound reflects that the number of distinct term trees of depth r0 over Σ grows as |Σ|k 0 in the worst case, which is a constant once Σ, k, and r0 are fixed.) Proof. See Appendix A. Corollary 4.6 (Lower bounds for local extensions). Under the hypotheses of Theorem 3.1, with R′ refutation-based (as in Case 2 of Theorem 3.1): (i) Any such local extension R′ of R sound with respect to M requires derivations of length L ≥ Ω(n) to prove f ≡ g on In . 1 In [2]: Theorem 2.8 establishes TCSC ⊆ I∃1 ; Theorem 4.3 establishes TCSC ̸⊆ OI. These are the theorem numbers in the published LMCS version (arXiv:1910.03917v5).
12
(ii) Under the clause-per-configuration encoding (Remark 3.3, |In | = 2n ), the bound improves to L ≥ Ω(2n ). Proof. Immediate from Case 2 of Theorem 3.1 and Lemma 4.5. The proof-theoretic analysis is now complete. The exponential bound of Case 2 rests on the local indistinguishability of the gadget configurations: any rule application that cannot see the difference between a0i and a1i is exactly an adversary that cannot break the hiding of the corresponding ciphertext. This is not an analogy: the next section formalizes the same bound as a statement about negligible cryptographic advantage, showing that the proof-theoretic and cryptographic frameworks are the same framework.
5
Cryptographic Connection
5.1
Formal correspondence
We establish a formal correspondence between the structure of Theorem 3.1 and the structure of cryptographic indistinguishability. Definition 5.1 (Syntactic adversary). A syntactic adversary for (R, F) is any deterministic algorithm A that operates by applying rules from a local extension R′ of R (with the same locality radius r0 ) to terms presented as inputs. We distinguish two classes: • A perfectly-constrained adversary cannot apply any rule at positions in F; this corresponds to Case 1 (base system R). • A computationally-bounded adversary operates via a local extension R′ of R (Definition 2.5) that may include rules applicable at positions in F, subject to a polynomial bound on total rule applications (steps in a deterministic RAM model with unit-cost arithmetic); this corresponds to Case 2. Each configuration C(b1 ,...,bn ) is parametrized by a bit vector (b1 , . . . , bn ) ∈ {0, 1}n (Definition 2.16). The advantage of A in identifying this bit vector on instance In is Adv(A, n) := Pr A(Ci ) correctly outputs which Skolem function is encoded in Ci − 21 , i∼Unif[N ]
where the probability is uniform over the N = 2n configurations C1 , . . . , CN of In . Here ”correctly outputs which Skolem function is encoded in Ci ” means: given Ci = C(b1 ,...,bn ) , A outputs the bit b
vector (b1 , . . . , bn ) that determines which constants ajj are selected in each gadget (equivalently, which disjunct of each gadget clause must be refuted). Both f and g appear in every Ci ; the task is to identify the configuration, not to distinguish which function is semantically present (both are, by semantic equivalence). Note that Adv(A, n) may in principle be negative (if A is systematically wrong); the bound Proposition 5.3 applies to the signed quantity, and the corollary Corollary 5.4 concerns adversaries achieving positive advantage. Proposition 5.2 (Case 1 implies zero advantage). Under the hypotheses of Case 1 of Theorem 3.1, Adv(A, n) = 0 for every syntactic adversary A and every n ≥ 1. Proof. By Case 1, no derivation in R produces any clause of the form f (t1 ) = g(t2 ) that would reveal which configuration (b1 , . . . , bn ) is active. Since A is constrained to apply rules from R (or a local extension with the same protected set), it produces the same output on every configuration, and therefore cannot identify the active bit vector (b1 , . . . , bn ) with any advantage. Therefore Adv(A, n) = 0.
13
Proposition 5.3 (Case 2 implies negligible per-step advantage). Under the hypotheses of Case 2 of Theorem 3.1, any syntactic adversary A running for L steps has Adv(A, n) ≤
L·c . 2n
In particular, to achieve Adv(A, n) ≥ δ for any constant δ > 0, the adversary must run for at least L ≥ δ · 2n /c = Ω(2n ) steps. Proof. We use the computationally-bounded adversary model (Definition 5.1). Each step of A applies one rule of R′ of locality radius r0 . By the indistinguishability hypothesis (Lemma 4.5(ii)), any rule application that does not act at a position occupied by some abi i produces the same output on all 2n configurations. A rule application that does act at such a position can alter the local context for at most c configurations (those that share the same local pattern at that position). Let D(L) denote the set of configurations that A has distinguished after L steps, i.e., configurations for which A has applied at least one rule that reads a gadget-specific constant. Each step adds to D(L) at most c configurations (those sharing the same local context at the position acted on); by induction on L, |D(L)| ≤ L · c. For configurations not in D(L), A has applied only rules that are blind to the gadget constants; its output on these configurations is independent of which configuration (b1 , . . . , bn ) is active. Since A’s output is the same for all configurations not in D(L), it must output the same bit vector for all of them; since each of the 2n configurations is equally likely by the uniform distribution, the probability that this fixed output is the correct bit vector is exactly 12 . The advantage of A is thus bounded by the fraction of configurations in D(L): Adv(A, n) ≤
|D(L)| L·c ≤ . n 2 2n
For Adv(A, n) ≥ δ > 0 we need L ≥ δ · 2n /c = Ω(2n ). Corollary 5.4 (Computational hiding from Case 2). Under the hypotheses of Case 2 of Theorem 3.1, the gadget family {In } is computationally hiding: no syntactic adversary running in polynomial time can identify which configuration (b1 , . . . , bn ) is active with non-negligible advantage. Specifically, any adversary achieving advantage ≥ δ > 0 requires Ω(2n ) rule applications, which is super-polynomial in n. Proof. Immediate from Proposition 5.3 with L = polynomial in n: for any polynomial L = L(n), L(n) · c/2n → 0 as n → ∞, so the advantage is negligible. Remark 5.5 (Observational vs. semantic hiding). Both f and g appear in every instance Ci of In ; the hiding of Corollary 5.4 is therefore observational, not semantic: it is the configuration (b1 , . . . , bn ) that is hidden, not a semantic distinction between two inequivalent functions.
5.2
Correspondence table
Table 1 summarizes the structural correspondence between the proof-theoretic and cryptographic frameworks. Corollary 5.6 (Non-extraction of Skolem witnesses). Under the hypotheses of Theorem 3.1, with R′ refutation-based (Case 2), no local syntactic system R′ can, given the clause set In encoding witnesses for ∀x ∃y. ϕ(x, y), identify which gadget configuration (b1 , . . . , bn ) ∈ {0, 1}n is active, and thereby determine which disjunct of each gadget clause must be refuted, using fewer than Ω(2n ) rule applications. (Both f and g are semantically equivalent by hypothesis; the barrier is observational, not semantic.) 14
Table 1: Structural correspondence between the proof-theoretic components of Theorem 3.1 and their cryptographic counterparts. Proof theory
Cryptography
Protected set F
Commitment scheme: the adversary sees the commitment but not the opening Syntactic separation of f and g Indistinguishability of two ciphertexts (or two keys) Syntactic invariant Inv anchored to Security invariant maintained F throughout the security game Case 1: no derivation exists Perfect (information-theoretic) hiding: advantage equals 0 Case 2: derivation costs Ω(n) Computational hiding: advantage is steps (or Ω(2n ) under clause-per- negligible for polynomial-time adverconfiguration encoding) saries (requires the Ω(2n ) regime) Skolem function f as existential wit- Secret witness or private key in a ness zero-knowledge protocol Local rule application in R′ Single query of a computationally bounded adversary Locality radius r0 Bound on adversary inspection per step (context window size)
Proof. Immediate from Case 2 of Theorem 3.1 and Proposition 5.3; see also Proposition 5.2 for the perfect-hiding case. Remark 5.7 (Witness indistinguishability). Corollary 5.6 is the proof-theoretic analogue of witness indistinguishability in zero-knowledge protocols: no efficient distinguisher can determine which of two valid witnesses was used in a proof. Here, the distinguisher is a syntactic adversary A, and efficiency is measured by the number of local rule applications. Remark 5.8 (Theorem 3.1 as a case of the observational collapse). The observational hierarchy of [10] introduces a formal framework in which the computational axis (the Chomsky hierarchy and complexity theory) and the observational axis are orthogonal and independent. An observer is a function O : Σ∗ → S that determines which information about the input is accessible to a computational system. The key result (Proposition 9.6 of [10]) is that under the profile observer Oprof , which maps a string to its symbol-count vector: POprof = NPOprof ⊊ P. This collapse is unconditional: it holds regardless of whether P = NP, because it is caused by structural blindness, not computational hardness. The observer Oprof discards the order of symbols entirely; no combinatorial structure remains on which nondeterminism could act. Theorem 3.1 of the present paper is an instance of this phenomenon. The local syntactic system R = (Σ, V, Rules, r0 ) defines a constrained observer OR that maps each term t and position p to the context Br0 (p)(t). By Definition 2.5, the applicability of every rule depends only on OR (t, p); information at distance > r0 from p and information inside F are invisible to R. In the language of [10]: • R is a constrained observer OR ≺ O⊤ ; • Case 1 (impossibility) says the equivalence f ≡M g is not OR -decidable: the two Skolem functions lie in disjoint protected regions that OR cannot see simultaneously; 15
• Case 2 (lower bound) says that any local extension R′ requires Ω(n) steps, a consequence of the structural blindness of OR′ with respect to the n independent gadgets. Whether OR admits a formal embedding into the canonical observer hierarchy of [10], which would make Theorem 3.1 a corollary of Proposition 9.6, is Question (Q6) of Section 8. The lower bound holds in every world of Impagliazzo [11], including Algorithmica (P = NP), because it arises from the observational axis, which is orthogonal to the computational axis that the five worlds parametrize. This orthogonality is made explicit in [8], which embeds the five worlds into a two-dimensional landscape. The same obstruction appears in the cipher of [12, 7]. The Mixed-Radix One-Time Pad encrypts as ci = (mi + ki ) mod bi ; Shannon perfect secrecy holds regardless of whether the base sequence B is public or secret (Section 4 of [7]: secret bases do not reduce key entropy). The base B functions as a syntactic invariant: it encodes the decomposition structure of the integer, a semantic fact invisible to any local syntactic observer, just as F encodes the separation between f and g that R cannot cross. The cryptographic and observational readings of Theorem 3.1 point to a general principle: the same obstruction appears wherever a system acts locally on a representation while a semantic invariant is encoded globally. The next section makes this precise in two further domains.
6
Cross-Domain Connections
Section 5 identified the core of Theorem 3.1: the protected invariant is a commitment, the syntactic separation is ciphertext indistinguishability, and the derivation cost is the adversary’s advantage. This section shows that the same identification works in two further domains, type theory and circuit complexity, not because these are analogies to cryptography, but because they have the same mathematical structure: a constrained observer that cannot see a semantic invariant above its observational level. In each case, what makes the impossibility or lower bound hold is the same hiding phenomenon formalized in Section 5. We present each connection as an explicit dictionary (Table 2 and Table 3) and state the corresponding obstruction as a corollary.
6.1
Type theory and the Type Omitting Theorem
Background. The Type Omitting Theorem (Henkin–Orey, 1956) states: a countable consistent theory T omits a type Φ(x), a set of formulas in one free variable, if and only if Φ is not principal, meaning no single formula θ(x) is consistent with T and implies every formula in Φ. Via the Curry–Howard correspondence, a type is a proposition and a term of that type is a proof. A type system T (Martin-Löf type theory, the Calculus of Constructions, or a dependent type system such as Coq or Agda) acts as a syntactic system: it inspects the syntactic structure of terms and decides type membership based on formation rules alone. Extensional properties of functions, what a function computes rather than how it is written, are semantically defined. Rice’s theorem is the limiting case: no non-trivial extensional property of a computable function is decidable by any syntactic inspection of its code. Within a constructive type system, this takes the following form: a type Φ expressing a semantic property of functions (e.g. “this term computes the Fibonacci sequence”) is semantically isolated if its membership depends on the function computed, not on the proof term, and syntactically dense if every proof term of a related type passes through subterms that look locally like Φ-witnesses. The dictionary.
16
Table 2: Dictionary between Theorem 3.1 and the constructive Type Omitting Theorem. Theorem 3.1
Type theory
Local syntactic system R
Type-checking algorithm T
Protected set F
Extensional kernel: positions where the semantic property of the function manifests, inaccessible to T Syntactic invariant Inv Typing invariant preserved by every reduction step (β-reduction, η-expansion) Skolem functions f , g Two proof terms t, u of the same proposition ϕ (propositional truncation: ∥ϕ∥) Semantic equivalence f ≡M g Extensional equality: t and u compute the same function Case 1: no derivation proves The type system cannot decide proposif ≡M g tional equality of t and u from syntactic structure alone Case 2: any extension costs Ω(n) Any decision procedure for extensional steps equality requires inspecting n independent semantic witnesses The obstruction. A constructive type system T with reduction rules of bounded depth is a local syntactic system in the sense of Definition 2.5, with locality radius r0 equal to the maximum depth of any reduction rule. The extensional kernel of a semantically isolated type Φ is a protected set: no reduction rule fires at positions where the semantic property of the function manifests, because the property is extensional and reductions preserve the computed function. Corollary 6.1 (Constructive Type Omitting). Let T be a constructive type system with reduction rules of bounded depth r0 . Let Φ be a type that is semantically isolated (membership depends on the function computed, not the proof term) and syntactically dense (every proof term of any related type passes through Φ-witnesses). Then T cannot derive the extensional equality of two distinct proof terms t and u of the same proposition. Any extension of T that decides extensional equality on a family of n independent witnesses requires at least Ω(n) reduction steps. Proof. The type system T is a local syntactic system (Definition 2.5) with locality radius r0 equal to the maximum depth of any reduction rule, and the extensional kernel as protected set. The typing invariant serves as the syntactic invariant: (i) it is checkable within depth r0 of each redex; (ii) it holds on any well-typed initial term by assumption; (iii) it is preserved under reduction by the subject reduction theorem; (iv) violation requires reducing inside the extensional kernel (a position where the function is determined), which is protected; (v) two proof terms t and u of the same proposition under propositional truncation (in the sense of homotopy type theory: all proofs of ϕ are identified, so t and u are distinct only at the level of their syntactic structure) occupy disjoint positions in the type structure, so no typing judgment in any derivation has the form t =ext u with t headed by f0 and u headed by f1 (the coherence condition of Definition 2.12(v)). The two proof terms t and u are semantically equivalent (extensionally equal) and syntactically separated in T . Theorem 3.1 applies directly. Remark 6.2 (Typological Invariance Principle). Corollary 6.1 can be restated as: a constructive type system cannot, from the syntactic structure of a proof term alone, determine the extensional property of the function the term computes. This is the Curry–Howard translation of Theorem 3.1: the syntactic machine (the type) is structurally blind to the semantic property of the model (the function computed). The Type Omitting Theorem is Case 1; the lower bound on decision procedures is Case 2. 17
6.2
Circuit complexity and the Natural Proofs barrier
What this section contributes. The Natural Proofs barrier of Razborov and Rudich [13] is a classical result. We do not reprove it. Instead, Theorem 3.1 yields two things that Razborov– Rudich does not contain: (1) An unconditional lower bound of Ω(n) on the number of inspection steps required by any large and constructive technique to decide circuit complexity on n independent witnesses, with no pseudo-random generator. This applies to all constructive techniques, not only those whose distinguishers are computable by AC0 circuits. The result of [14] on AC0 natural proofs is a quantitatively precise instance of the present framework (Remark 6.4): the distinguishers of [14] are local syntactic systems with r0 = AC0 circuit depth, and Corollary 6.3(i) gives the underlying unconditional Ω(n) bound; the sharper quantitative bound of [14] requires the Trevisan–Xue generator as gadget family. (2) A structural explanation: the barrier is not a consequence of computational hardness but of observational blindness. Any large, constructive technique is a constrained observer OP ≺ O⊤ that cannot see the circuit complexity of f because complexity is a property of the function, not of its truth table. The PRG assumption enters only to convert the unconditional Ω(n) bound into the Ω(2n ) bound by supplying 2n locally indistinguishable instances. Background. Let f : {0, 1}n → {0, 1} be a Boolean function and Cf a circuit computing it. A natural proof in the sense of Razborov and Rudich [13] is a property P of Boolean functions (equivalently, of their truth tables) satisfying: • Usefulness. P holds for functions not in P/poly (it witnesses circuit hardness); • Largeness. At least 2−poly(n) of all Boolean functions on n bits satisfy P; • Constructivity. Given the truth table of f (of length 2n ), membership f ∈ P is decidable in time 2O(n) , i.e., polynomial in the truth table size. The proof in [13] shows that if a secure pseudo-random generator (PRG) exists in P/poly, then no natural proof can establish a super-polynomial circuit lower bound. The PRG assumption is used to show that any large, constructive property P is falsified by the PRG: the PRG outputs a string that looks like the truth table of a function satisfying P even though the generator itself is in P/poly. The precise dictionary. is as follows.
The translation between Theorem 3.1 and the Natural Proofs barrier
n
The obstruction. Fix n. The truth table of f is a string in {0, 1}2 ; treat it as a term in a signature where each bit position is a constant symbol. A constructive property P decides membership by reading at most poly(n) bits of this string, making it a local syntactic system with locality radius r0 = poly(n). The largeness condition ensures P holds on the initial term (a random truth table), is preserved by the PRG’s local modifications to the string, and can only be falsified by accessing the circuit complexity of f , which is a property of the function, not of the truth table, and constitutes the protected set F . The PRG produces 2n pseudo-random truth tables T1 , . . . , T2n that are mutually locally indistinguishable: for any position p and any inspection window of size poly(n), the local view of Ti at p equals the local view of Tj at p. These are the 2n configurations of the gadget family {In }n≥1 , with the PRG security guaranteeing Lemma 4.5(ii) in this setting. 18
Table 3: Dictionary between Theorem 3.1 and the Natural Proofs barrier. Theorem 3.1
Natural Proofs
Local syntactic system R
Constructive property P (acts on truth tables via polynomial-time inspection) Locality radius r0 Inspection depth: P reads at most poly(n) bits of the truth table in any single evaluation Protected set F Circuit complexity: the hardness of f as a property of the function, not of the truth table Syntactic invariant Inv Largeness: P holds for most functions and is preserved by the PRG’s action on truth tables Syntactic separation of f , g Falsifiability by PRG: the PRG produces 2n truth tables each individually satisfying P while the underlying function is in P/poly Case 1: no derivation proves No natural proof separates P/poly from f ≡M g the hard functions (assuming PRG) Case 2: any extension costs Ω(n) Any technique that escapes the barrier steps must inspect Ω(n) independent truthtable witnesses
Corollary 6.3 (Structural Natural Proofs Barrier). Let P be a large and constructive property of Boolean functions (Definition 2.5 with locality radius r0 = poly(n)). (i) Unconditional lower bound. Any extension of P that correctly decides circuit complexity on n independent function witnesses requires at least Ω(n) truth-table inspection steps. This holds without any assumption on pseudo-random generators. (ii) PRG-conditional exponential bound. If a secure PRG in P/poly of output length 2n exists, it supplies exactly the 2n globally distinct but locally indistinguishable truth tables required by the gadget construction (Remark 3.3 below). Case 2 of Theorem 3.1 then gives L ≥ Ω(2n ), and the Razborov–Rudich barrier follows: no natural proof can establish a superpolynomial circuit lower bound. The PRG is used exclusively to supply these configurations; it does not enter the proof of structural blindness itself. Proof. The translation described above makes P a local syntactic system with the circuit complexity of f as protected set. We verify Definition 2.12: (i) P is checkable by inspecting at most r0 = poly(n) bits, giving the locality condition; (ii) largeness ensures P holds on any initial random truth table; (iii) treating the PRG’s action on the truth table as the analogue of a rewriting rule, P is preserved under this action (by PRG security: a poly(n)-bit local inspection cannot distinguish PRG output from random); making the identification of rewriting rules precise in this setting is part of Question (Q6); (iv) any violation of P requires accessing the circuit complexity of f , which lies in F; (v) the 2n PRG truth tables are locally indistinguishable (as in Lemma 4.5(ii)), so no local inspection sees two of them at comparable positions simultaneously. Part (i) applies Case 2 of Theorem 3.1 with n independent witnesses; the bound Ω(n) follows without the PRG assumption. Part (ii) applies Case 2 with N = 2n PRG instances as the clause-per-configuration family (Remark 3.3), giving Ω(2n ); the PRG is needed to guarantee local indistinguishability of the 2n instances.
19
Remark 6.4 (Loff–Sherif–Talebanfard–Ugazio in the observational hierarchy). The result of [14] admits a precise reading within the observational hierarchy of [10, 8]. Translation. An AC0 -natural proof in their sense is a property P whose distinguisher is a Boolean circuit of constant depth d. In the framework of Section 6.2, this makes P a local syntactic system with locality radius r0 = d, acting on truth tables viewed as strings of 2n bits. The induced constrained observer is OAC0 : it maps a truth table f to the output of a depth-d circuit d applied to f . Since OAC0 computes only depth-d functions of f , it satisfies OAC0 ≺ O⊤ , and the d d circuit complexity of f , a property of the function, not of any particular circuit representation, lies strictly above the observational level of OAC0 in the hierarchy of [10]. d The structural collapse. Proposition 9.6 of [10] gives: POAC0 = NPOAC0 ⊊ P. d
d
Applied to OAC0 , this says that no technique operating through depth-d observations can decide d circuit complexity, which accounts for their barrier at the structural level. Corollary 6.3(i) instantiates this collapse quantitatively: any such technique requires Ω(n) inspection steps on n independent witnesses, unconditionally. The PRG as gadget family. The localized Trevisan–Xue generator of [14] is computable by bounded-depth circuits and its security relies solely on the Switching Lemma — a combinatorial theorem that holds unconditionally. It produces truth tables that are locally indistinguishable to any AC0 distinguisher, supplying exactly the locally indistinguishable gadget family of Remark 3.3. With N = 2n such instances, Case 2 of Theorem 3.1 gives a lower bound of Ω(2n ) inspection 7/(d−5) steps; the localized generator achieves local indistinguishability for Neff = 2n effectively distinct instances at depth d (for d > 5, the regime where the Switching Lemma applies); applying 7/(d−5) Case 2 of Theorem 3.1 with N = Neff gives L ≥ Ω(Neff ) = Ω(2n ), matching the Switching Lemma frontier. Significance for the framework. This is the first concrete confirmation, with a quantitative bound, that the observational axis of [10] yields sharp results in circuit complexity. The barrier of [14] holds unconditionally in every world of Impagliazzo [11] (including Algorithmica, where P = NP) because its PRG is combinatorially secure, not cryptographically secure: it lives on the observational axis, not the computational one. The framework of Theorem 3.1 predicts this: barriers on the observational axis are independent of which computational world one inhabits. Remark 6.5 (P vs NP, derandomization, and the Observer World). Part (i) of Corollary 6.3 has an immediate consequence for the P vs NP question. If P = NP, then in particular P = PSPACE, and questions about circuit complexity would be decidable in polynomial time (the minimum circuit size problem lies in PSPACE). Part (i) shows that no technique for deciding circuit hardness can be both large (holding for 2−poly(n) of all Boolean functions) and constructive. Therefore: if P = NP, any proof of this fact via circuit-hardness decision must be either non-large or nonconstructive, it cannot be a natural proof in the sense of Razborov and Rudich. This is stronger than what Razborov–Rudich give under the PRG assumption: Part (i) holds unconditionally, so the structural blindness of any local syntactic technique to circuit complexity is independent of both P vs NP and the existence of a PRG. On derandomization: if P = BPP (randomness can be eliminated), the Nisan–Wigderson construction gives PRG in P/poly. Part (ii) then implies the full Razborov–Rudich barrier. But Part (i) already holds in the non-derandomizable world: the Ω(n) lower bound requires no PRG, no randomness assumption, and no separation hypothesis. The structural blindness identified in Theorem 3.1 precedes all of these and is not removed by derandomization. In the language of the Observer World [8], the technique P is a constrained observer OP ≺ O⊤ on truth tables. The circuit complexity of f lies strictly above the observational level of OP in the hierarchy of [10]. The P vs NP problem asks about the computational axis; the Natural Proofs barrier operates on the observational axis. The two axes are orthogonal [8]: resolving P vs NP 20
would not remove the observational barrier, and the observational barrier holds regardless of how P vs NP is resolved. The result of [14] — a quantitatively sharp unconditional barrier for AC0 -natural proofs, is a concrete confirmation of this: see Remark 6.4. Remark 6.6 (The observational reading). In the language of [10], both T (the type system of Section 6.1) and P (the lower-bound technique above) are constrained observers O ≺ O⊤ . The semantic invariant — extensional equality of proof terms in type theory, circuit complexity in the Razborov–Rudich setting — lies strictly above the observational level of O in the hierarchy. The impossibility results (Corollary 6.1 and Corollary 6.3(i)) are unconditional instances of the structural collapse PO = NPO ⊊ P (Proposition 9.6 of [10]): not because the problem is computationally hard, but because the observer cannot see the relevant invariant at all. The corollaries above (Corollaries 6.1 and 6.3) are formal results that follow from Theorem 3.1 given the stated hypotheses. The dictionaries (Tables 2 and 3) identify which component of Theorem 3.1 each component of the cited result corresponds to, explaining why each impossibility or lower bound is a consequence of observational blindness rather than computational hardness. Making the correspondences fully rigorous, verifying the hypotheses of Theorem 3.1 in the exact technical setting of each domain, raises the questions taken up next.
7
Conclusions
The central observation of this paper is that impossibility results and lower bounds in proof theory, cryptography, type theory, and circuit complexity share a single structure: a constrained observer cannot reach a semantic invariant that lies above its observational level. Theorem 3.1 formalizes this as an abstract obstruction with two faces, impossibility (Case 1) and a cost lower bound (Case 2), and the cross-domain connections of Section 6 show that the translation is not metaphorical but exact. These three components of the paper, the proof-theoretic analysis, the cryptographic connection, and the cross-domain connections, are not separable. The exponential lower bound of Case 2 is explained by the cryptographic hiding structure (Section 5): without it, the Ω(2n ) bound would appear as an artifact of the gadget construction rather than as a structural necessity. The cross-domain connections (Section 6) are accessible only because Section 5 has already identified computational hiding as the correct interpretation of syntactic separation: Type Theory and Natural Proofs barriers are then recognizable as instances of the same hiding phenomenon, not as separate results requiring separate arguments. The cryptographic content is not peripheral. The structure of Case 2 is the structure of computational hiding: protected positions are commitment schemes, syntactic separation is ciphertext indistinguishability, and the Ω(2n ) derivation cost is the adversary’s negligible advantage. The proof-theoretic and cryptographic frameworks are the same framework, seen from different sides of the same invariant. For circuit complexity, the framework provides two things. First, an unconditional Ω(n) lower bound on the inspection cost of any large and constructive technique, without pseudo-random generators. Second, a structural explanation: the Natural Proofs barrier is not a consequence of computational hardness but of observational blindness, and it holds in every world of Impagliazzo, including Algorithmica. The result of [14] is the first quantitative confirmation of this: its AC0 -natural-proofs barrier lives on the observational axis, not the computational one.
8
Open Questions
The following questions arise from Theorem 3.1 and the surrounding framework but are not answered in this paper.
21
(Q1) Decidability of protected sets. For which classes of local syntactic systems is the existence of a non-trivial protected set F decidable in time polynomial in the clause set? Remark 4.2 shows that linear-time decidability holds for ground atoms under first-symbol clash. The general case — patterns with deep nesting or variable overlap — is open. (Q2) Formal reduction between Cases 1 and 2. Does the existence of a syntactic invariant Inv in Case 1 imply the existence of a gadget family witnessing the Case 2 lower bound for some extension R′ ? A positive answer would unify the two cases into a single combinatorial criterion. (Q3) Instance complexity of the lower bound. The gadget family {In } grows with n. Is there a single clause set I of fixed size M such that any local extension R′ requires derivation length super-polynomial in M to prove f ≡ g on I? This is the Case 2 analogue of the single witness W (commutativity) in Case 1. (Q4) Commitment scheme construction. Corollary 5.4 shows that Case 2 implies computational hiding. Does every instance of Case 2 also yield an explicit binding property, making it a commitment scheme in the standard (hiding and binding) sense? Specifically, is there a polynomial-time reduction from breaking the binding to solving a derivation problem in R′ ? (Q5) Extensions to non-local systems. The results assume a fixed locality radius r0 . Can analogous obstruction theorems be proved for systems with unbounded inspection depth, or for global rules such as resolution? Corollary 6.3(i) shows unconditionally that no natural proof technique can establish circuit lower bounds; any extension to global systems that overcomes the syntactic barrier must therefore not be a natural proof in the sense of Razborov–Rudich [13]. (Q6) Formal embedding into the observational hierarchy. Remark 5.8 identifies R as a constrained observer OR ≺ O⊤ . Remark 6.4 carries this out concretely for AC0 -natural proofs: OAC0 ≺ O⊤ with the collapse POAC0 = NPOAC0 ⊊ P. The general case requires: d
d
d
(i) embedding (t, p) 7→ Br0 (p)(t) into the string-based formalism of [10]; (ii) identifying the canonical observer level of OR ; (iii) deriving Theorem 3.1 as a corollary of Proposition 9.6 of [10]. The mixed-radix decomposition of [9] provides a concrete observational invariant whose embedding may serve as a test case for step (i). (Q7) Obfuscation. The VBB impossibility [16] states that no algorithm (not necessarily syntactic) can obfuscate all circuits to black-box equivalence. This matches Case 1 structurally: the semantic invariant (the function computed) is protected from any local syntactic observer. Does Theorem 3.1 formally subsume VBB impossibility, and does the Case 2 bound correspond to the computational gap between iO and VBB? (Q8) Algebrization. The algebrization barrier [17] shows that arithmetization-based techniques cannot resolve complexity separations. Arithmetization acts locally on the syntactic representation of a circuit, and the semantic invariant (complexity class membership) is protected from this local action. Does the algebrization barrier fit Theorem 3.1 with r0 equal to the degree of the polynomial extension?
Acknowledgments The mathematical content of this paper was developed solely by the author and originated in Italian.
22
English translation, stylistic adaptation to standard mathematical prose, LATEX typesetting, bibliography formatting, cross-reference management, and iterative editorial review were carried out with the assistance of an AI language model.
A
Full Gadget Construction
This appendix contains the full construction and correctness proof for the family {In } used in Lemma 4.5 and Case 2 of Theorem 3.1.
A.1
Construction
For n ≥ 1, construct n independent gadgets G1 , . . . , Gn as follows. Single gadget Gi . Introduce two fresh constants a0i and a1i (the two local configurations of Gi ). Let the local state of Gi be a ground term τi ∈ {a0i , a1i }. The gadget Gi contributes a clause of the form f (a0i ) ̸= g(a0i ) ∨ f (a1i ) ̸= g(a1i ) (the disjunction of the two instances of the negated equivalence ¬(f (x) = g(x)) for x = a0i and x = a1i ). This encodes that at least one of the two instances must be refuted. A complete refutation of In must resolve the disjunction in each of the n gadget clauses (selecting a witness abi i for each Gi ), and also refute the universal negation clause ¬(f (x) = g(x)) by unifying x with each selected witness. The n resolutions are independent (one per gadget), so a complete refutation consists of at least n dedicated rule applications. Global configuration. A global configuration C(b1 ,...,bn ) is a choice of witness abi i for each gadget Gi , determined by a bit vector (b1 , . . . , bn ) ∈ {0, 1}n . The instance In is a fixed set of clauses; the 2n configurations represent the 2n possible refutation strategies, choices of which disjunct to resolve in each gadget clause. There are N = 2n global configurations. Encoding in In .
The instance In consists of:
• the axioms of the base system R (e.g., rules (A1) and (A2) in the superposition instantiation); • one clause per gadget Gi , as described above; • a negation clause ¬(f (x) = g(x)) for a fresh variable x. Spatial separation of gadgets. The constants a0i , a1i of gadget Gi and the constants a0j , a1j of gadget Gj (i ̸= j) appear in distinct clauses of In (each gadget clause mentions only its own constants), ensuring that no single rule application can act on constants from two different gadgets simultaneously. Within each gadget clause, the two constants a0i and a1i are placed at positions whose tree distance within that clause exceeds 2r0 , so no single rule of radius r0 can have both in its context simultaneously. Formally, within the clause for Gi , if a0i appears at position p0 and a1i at position p1 with d(p0 , p1 ) > 2r0 , then no context of radius r0 contains both. This is achievable for any fixed r0 by inserting separator nodes between the two occurrences. Under this construction, a rule of radius r0 overlaps with at most one gadget at a time, confirming the spatial separation used in Step 4 of the proof of Case 2.
A.2
Verification of Lemma 4.5
Proof of Lemma 4.5. (i) The 2n global configurations are indexed by (b1 , . . . , bn ) ∈ {0, 1}n , so N (n) = 2n .
23
(ii) Any two distinct configurations C(b1 ,...,bn ) and C(b′1 ,...,b′n ) differ in at least one gadget index i. The constants a0i and a1i are opaque with respect to R′ : they are fresh symbols not appearing in any left-hand side pattern of any rule in R′ , nor as proper subterms of any left-hand side pattern. Therefore, for any rule ρ ∈ R′ and any position p: even if Br0 (p)(t) contains the symbol abi i , the rule cannot use its identity (whether a0i or a1i ) to decide applicability, since both are fresh and absent from all LHS patterns. The applicability of ρ at p is thus the same in both configurations, and their local contexts of radius r0 are identical as seen by any rule of R′ . Hence the two configurations are indistinguishable within radius r0 . (iii) C(b1 ,...,bn ) = ̸ C(b′1 ,...,b′n ) in M because the constants a0i and a1i are interpreted as distinct elements of the domain of M (they are fresh Skolem constants). r The bound c ≤ |Σ|k 0 (where k is the maximum arity of symbols in Σ) follows from the fact r that the number of distinct term trees of depth r0 over Σ is at most |Σ|k 0 , which bounds the number of distinct local contexts of radius r0 any rule can observe, and hence the number of configuration classes a single rule application can create.
B
Proofs of Auxiliary Lemmas
Lemma B.1 (Full proof of Lemma 4.3). The property Inv defined in Lemma 4.3 satisfies conditions (i)–(v) of Definition 2.12. Proof. (i) Local checkability. Inv(t) is checked by examining, for each +-position p+ in t, the context B1 (p+ )(t): whether the left child of + (position p+ ·1) is a and the right child (position p+ ·2) contains b, and symmetrically. This requires inspecting subterms within distance 1 = r0 of each +-position, as given by Br0 (p+ )(t). (ii) Initialization. The initial clause set contains only the clause a+b = ̸ b+a. The term a+b has a at the left child of + and b at the right child; Inv holds. Symmetrically for b+a. (iii) Preservation. By Lemma 4.1, no rule of R is applicable at any position in F. In particular, no rule can rewrite inside a+b or b+a. Terms in the derived clause set may contain a+b embedded in larger contexts (carried over from the initial clause set or from earlier derivation steps), but no rule can alter the local context of a or b within those subterms. Therefore Inv is preserved under every rule application. (iv) Anchorage. Violating Inv requires either: (a) moving a to a position where its parent is not +, or the right sibling does not contain b; or (b) symmetrically for b. Both require a rule application at a position in F (the position of a or b, or their parent +-position). By Definition 2.9, no such rule application is possible in R. (v) Coherence. Reading the initial clause set {a+b = ̸ b+a} directly: the only occurrences of f = a and g = b in any clause satisfying Inv are inside the frozen subterms a+b and b+a respectively. Since a appears only as the left argument of + in a+b, and b appears only as the left argument of + in b+a, and since a+b and b+a are in separate positions of any clause (they cannot appear at the same position), no literal of any clause satisfying Inv has the form a(t1 ) = b(t2 ) (i.e., an equation with a and b as head symbols on its two sides): the only literal of the initial clause is a+b ̸= b+a, which is a disequation, not an equation comparing a and b as heads; and by Preservation, no derived clause introduces such a literal. Therefore Inv(t) implies coherence.
References [1] Fabio F.G. Buono. Syntactic systems cannot see semantic invariants. Preprint, arXiv:2606.17275 [cs.LO], June 2026. https://arxiv.org/abs/2606.17275. DOI: 10.5281/zenodo.20618697.
24
[2] Stefan Hetzl and Jannik Vierling. Clause set cycles and induction. Logical Methods in Computer Science, 16(4):11, 2020. DOI: 10.23638/LMCS-16(4:11)2020. arXiv:1910.03917v5 [cs.LO]. [3] Stefan Hetzl and Jannik Vierling. Induction and Skolemization in saturation theorem proving. Annals of Pure and Applied Logic, 174(1):103167, 2023. DOI: 10.1016/j.apal.2022.103167. arXiv:2105.07734 [cs.LO]. [4] Stefan Hetzl and Jannik Vierling. Unprovability results for clause set cycles. Theoretical Computer Science, 935:21–46, 2022. DOI: 10.1016/j.tcs.2022.09.002. [5] Stefan Hetzl and Johannes Weiser. Subsystems of open induction. Preprint, arXiv:2509.05653 [math.LO], September 2025. https://arxiv.org/abs/2509.05653. [6] John C. Shepherdson. A non-standard model for a free variable fragment of number theory. Bulletin de l’Académie Polonaise des Sciences, Série des sciences mathématiques, astronomiques et physiques, 12:79–86, 1964. [7] Fabio F.G. Buono. New ideas on a new old type of cipher: the mixed-radix one-time pad. Preprint, arXiv:2606.16040 [cs.CR], June 2026. https://arxiv.org/abs/2606.16040. [8] Fabio F.G. Buono. The observer world: a cryptographic extension of Impagliazzo’s five worlds. Preprint, arXiv:2606.27139 [cs.CR; cs.CC], June 2026. https://arxiv.org/abs/ 2606.27139. [9] Fabio F.G. Buono. From bits to mixed-radix keys: Horner decomposition, uniform sampling, and the information-theoretic QKD interface of the MR-OTP. Preprint, arXiv:2606.18526 [cs.CR; cs.IT], June 2026. https://arxiv.org/abs/2606.18526. [10] Fabio F.G. Buono. Observers, symmetries, and the hierarchy of language classes: a theory of computation parameterized by the observer. Preprint (draft), Zenodo, June 2026. DOI: 10.5281/zenodo. [11] Russell Impagliazzo. A personal view of average-case complexity. In Proceedings of the 10th Annual IEEE Conference on Structure in Complexity Theory, pages 134–147, 1995. [12] Fabio F.G. Buono. A new type of cipher. Preprint, arXiv:1202.2004 [cs.CR], 2012. https: //arxiv.org/abs/1202.2004. [13] Alexander A. Razborov and Steven Rudich. Natural proofs. Journal of Computer and System Sciences, 55(1):24–35, 1997. (Preliminary version in Proceedings of STOC 1994, pages 204–213.) DOI: 10.1006/jcss.1997.1494. [14] Bruno Loff, Suhail Sherif, Navid Talebanfard, and Francesca Ugazio. The Switching Lemma shows what the Switching Lemma cannot prove: an unconditional natural-proofs barrier. Preprint, arXiv:2606.12631 [cs.CC], June 2026. https://arxiv.org/abs/2606.12631. DOI: 10.48550/arXiv.2606.12631. [15] Abdelkader Kersani and Nicolas Peltier. Combining superposition and induction: A practical realization. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Frontiers of Combining Systems (FroCoS), volume 8152 of Lecture Notes in Computer Science, pages 7–22. Springer, 2013. DOI: 10.1007/978-3-642-40885-4 2. [16] Boaz Barak, Oded Goldreich, Russell Impagliazzo, Steven Rudich, Amit Sahai, Salil Vadhan, and Ke Yang. On the (im)possibility of obfuscating programs. In Advances in Cryptology — CRYPTO 2001, volume 2139 of Lecture Notes in Computer Science, pages 1–18. Springer, 2001. DOI: 10.1007/3-540-44647-8 1. 25
[17] Scott Aaronson and Avi Wigderson. Algebrization: A new barrier in complexity theory. ACM Transactions on Computation Theory, 1(1):2:1–2:54, 2009. DOI: 10.1145/1490270.1490272.
26