Pure Time Theory - Chapter VII - Deterministic 3SAT decision in polynomial time via structural amortization and multi-modular closure

Pure Time Theory – from Intuition to Genesis Chapter VII – Deterministic 3SAT decision in polynomial time via structural amortization and multi-modular closure Essam Allou October 14, 2025 Abstract We present a minimal deterministic framework for deciding 3sat, based on (i) a global order T(stratification of choices), (ii) a local perceived time τ defined by dτ = dt/g ( ρ ), with ρ an information density satisfying structural properties (P1–P5) and g increasing, and (iii) a weighted discrete potential Φ ? measuring only the reducible heads (unit, binary local binary projection handled by R β –BinClose , triplet motifs) and the linear defects defectp for p∈ { 2 , 3 , 5 } . The multi-mod scheme relies on a deterministic syntactic detection of linear gadgets mod p and on Gaussian elimination mod p over extracted subsystems. We establish two structural lemmas: (L1) deterministic fairness in τ , and (L2) amortization of Φ ? (each valid operation ensures ∆ ˜τ Φ ?≤ − 1, with g ( ρ ) = (1 + ρ ) α and α∈ (1 / 2 , 1]). We further use aCombined Lyapunov Λ := Φ ? + εM to make the episode bound scheduler-independent. A key lemma, No-False-Silence under T , formalizes that every active stratum carries either a local operation or an interface flux triggering one at the next step, the only allowed “silence” being a certified one (Φk=Jk= 0). Results. (T1) Unconditional SAT completeness: the dynamics reaches a window where the local readout stabilizes, and then R β –BinClose+UP complete the assignment (witness verifiable in O ( m )). (T2) UNSAT ⇒ unconditional certificate: Boolean conflict or 0=1 mod p for at least one p∈ { 2 , 3 , 5 } , with a verifiable Gaussian trace. (T3) Unconditional polynomial bound: with Φ ? init ≤poly ( n, m )and the minimal decrease above, the number of episodes is poly ( n, m ); each episode has polynomial cost (at most O ( n3 )for a linear block). The framework remains strictly discrete and deterministic (no tuning) with three global constants fixed a priori: α in g ( ρ ) = (1 + ρ ) α , the set P = { 2 , 3 , 5 } , and a lexicographic tie-break order. After R7.5 (unique external injection and constant threshold), the local cell is canonically ripple + repli (fold-back); this yields a purely structural reading of q (without any state “simulation”). We establish the bijective local classification (the only admissible pattern under span ≤ 1and external degree 1 is ripple), the complete normalization of linear constraints (XOR/counters/equalities), and the SPC bifurcation (Small-Prime Completeness): non-saturated ⇒ multi-mod conflict { 2 , 3 , 5 } , saturated ⇒ controlled fall into the scalar regime and empty clause. The bit-complexity satisfies log q = O ( |F| )and the cost of R8bin qis O(Klog q). It follows that 3SAT ∈P, hence P=NP. All per-step cost bounds (UP,R β –BinClose, LinClose + ( p ), R8 bin q , detection) are polynomial and gathered in Proposition 12 and Theorem 19. 1 Contents 1 Introduction and framework overview 4 2 Formal definitions 4 2.1 Instance, implication graph, and global order T................... 4 2.2 Information density ρ(Properties P1–P5) ...................... 4 2.3 Class gand perceived time τ............................. 5 2.4 Weighted discrete potential Φ?............................ 5 2.5 Valid operations and deterministic selection ..................... 5 2.6 Detection mod p(deterministic scheme) ....................... 6 3 Lemma (L1): deterministic fairness in τ21 4 Linear completion and Small-prime completeness 23 4.1 Post-normalization linear completion (algorithm & proof) ............. 23 4.2 Small-prime completeness {2,3,5}.......................... 24 5 Causal encoding of thresholds and PTT refutation of PHP in polynomial time 26 5.1 Causal encoding of cardinalities ............................ 26 5.2 Bounded-CRT refutation for S=n+ 1 with nbits ................. 27 5.3 Verifiable example PHP(3,2) .............................. 27 5.4 Implementation notes ................................. 28 6 Lemma (L2): amortization of Φ?31 7 Theorems (T1–T3) 32 8 Deterministic algorithm (pseudocode) and complexity 32 9 Certificates and verifiability 34 9.1 SAT witness ....................................... 34 9.2 Linear certificate mod p................................ 34 9.3 Deterministic 3-pass verifier .............................. 34 10 Mod 3 obstruction & multi-mod resolution (R1) 35 10.1 CNF family mod 3 incompatible, mod 2 compatible ................ 35 10.2 Why {2,3,5}suffices (Occam) ............................. 35 11 Reproducibility 36 12 Conclusion 36 A Table of rules R1–R7 38 B Adversarial traces 38 C Pair or implicative cycle 38 D Canonical Tseitin library 39 E Exhibits (ledger & replayability) 40 ∗Unity of Truth, [email protected] 2 Motivation The present work originates not from an attempt to solve P versus NP in isolation, but from a deeper inquiry into the fundamental grammar of reality itself. Over the past years, I have developed Pure Time Theory (PTT), a framework rooted in the spectral structure of the Riemann zeta function, which proposes that all physical phenomenagravitational coupling, particle masses, quantum operators, and cosmic structureemerge from a single causal-temporal architecture indexed by the nontrivial zeros {γk}. PTT has yielded concrete, falsifiable predictions: Newton’s constant G computed to relative error 3 . 9 × 10 −7 , Planck’s constant ~ derived as the minimal cycle action A∗ , and 77 . 8% of PDG particle mass ratios reproduced from spectral encodingsall without free parameters. These results suggest that PTT captures something fundamental about the structure of our universe. The logical necessity. If PTT truly describes reality, then every structure that exists in the physical worldincluding computational processesmust admit a natural representation within the ( T, τ, ρ, Φ ? )framework. Computation is not an abstract Platonic realm disconnected from physics; it is a physical process, subject to the same causal and informational constraints as particle interactions or gravitational dynamics. The conjecture P 6 =NP, viewed through this lens, would imply the existence of problems whose intrinsic complexity transcends the polynomial-time orchestration that governs all other known physical phenomena. Such a dichotomy seems philosophically and physically unnatural: Why would the universe permit polynomial-time resolution of quantum scattering, protein folding dynamics, and gravitational N-body evolution, yet forbid it for satisfiability testing? A test of the framework. This work is therefore not merely an attempt to claim P=NP, but a falsifiable test of PTT itself. If the normalisation procedure ( R 1 −R 8), the multi-modular closure { 2 , 3 , 5 } , and the amortised descent of Φ ? under pure-time ordering T fail to yield polynomial-time certificatesif hidden exponential barriers emerge despite the local determinism of the frameworkthen PTT’s claim to universality would be undermined. I seek neither reputation nor prize money. I seek truth. If PTT is correct, P=NP follows as a theorem, not a conjecture. If PTT is flawed, this work will expose that flaw, and I will refine or abandon the framework accordingly. The mathematics and algorithms presented here are fully transparent, deterministic, and verifiable. I invite the community to test them rigorously. Intellectual honesty. I am not a professional complexity theorist. I approach this problem as an outsider, guided by a unifying vision rather than by established barriers (relativisation, natural proofs, algebrisation). This may be a weaknessor it may be a strength. History shows that paradigm shifts often come from those unburdened by the constraints of the dominant framework. I offer this work in that spirit: as a sincere, rigorous attempt to see whether the grammar that unifies physics can also unify complexity theory. If I am wrong, I will learn. If I am right, we will have learned something profound about the deep unity of nature. 3 1 Introduction and framework overview Goal. Decide 3sat via a discrete dynamics governed by: (i) a global order T(topological stratification {Tk} ), (ii) a perceived time τ locally satisfying dτ = dt/g ( ρ )(slowdown in dense zones), (iii) a weighted discrete potential Φ ? ensuring amortized decrease, (iv) fully deterministic valid operations (pure literal, BinClose+UP, linear closure mod p∈ {2,3,5}, triplet motif). Contributions. (0) R7.5 and constant threshold. Unique external injection of xt and Cmp≥qcomparators at constant threshold (local normalization, span ≤1). (1) Bijective local classification. Under span ≤ 1, external degree 1, F0 = Id and F1 bijective, the update is necessarily ripple (Lemma 23). (2) Structural reading of q .After R7.5, q is read directly in the CNF (Lemma 26,Corollary 4). (3) Complete linear normalization. Every linear constraint rewrites into XOR/counters/equalities (Lemma 43). (4) Multi-mod scheme. Detection mod p∈ { 2 , 3 , 5 } and Gaussian elimination on extracted blocks. (5) Fairness (L1). Uniformized minimal budget in τ. (6) Amortization (L2). Amortized decrease of Φ?per episode. (7) SPC bifurcation. Non-saturated ⇒ multi-mod conflict; saturated ⇒ scalar empty clause (Proposition 10,Theorem 11,Theorem 7). (8) Bit-complexity and costs. log q = O ( |F| )(Lemma 14,15) and R8 bin q at O ( Klog q ) (Lemma 13,Corollary 2). (9) UNSAT certificates (T2). A Boolean or linear conflict (0=1mod p ) arises in polynomial time; the elimination trace forms a verifiable certificate. (10) Polynomial bound (T3). By Lemma 42 and (L2), the number of episodes is poly ( n, m )and the total cost is polynomial (with no additional assumption). (11) Confluence R1–R7. Unicité de la forme normale par Newman (Lemma 12). (12) Combined Lyapunov. Λ=Φ ? + εM rend la borne dépisodes indépendante du scheduler (Lemma 48). Scope. Results (L1), (L2), (T1)(T3) follow from the definitions and Lemma 42. 2 Formal definitions 2.1 Instance, implication graph, and global order T Given. An instance F= (Var,Cl)with |Var|=n,|Cl|=m, clauses of size ≥1. Definitions. We build the signed implication graph G : one vertex per literal ( x )and ( ¬x ), and for every binary clause ( ¬a∨b )we add the edge a→b (and symmetrically). We compress G by strongly connected components (SCC), yielding a DAG D . We then define the stratification {Tk} by topological BFS over D : an SCC source lies in T0 , then Tk+1 groups the SCCs whose predecessors are all contained in Sj≤kTj .Cost: O ( m ). The invariant T does not change during the decision (single construction) and the global soundness theorem (Thm. 18) ensures no spurious contradictions are introduced. 2.2 Information density ρ(Properties P1–P5) Required properties (P1–P5). (P1) ρ≥ 0; ρ ( empty state ) = Θ( m/n ); ρ ( complete SAT )=0; ρ ( conflict ) = + ∞ (or very large bound). (P2) Monotonicity under non-conflicting assignment. (P3) Invariance under renaming. (P4) (Sub-)additivity. (P5) Update in polynomial time. Chosen (simple) realization. 4 ρ(s) := ρratio(s) + X p∈{2,3,5} ρ⊕,p(s), ρratio(s) := 1 nX v∈Var degs(v),degs(v) = number of active occurrences of vor ¬vafter simplification, ρ⊕,p(s) := 1 np(s)rankF(p)Xp(s), np(s) := max{1,number of active variables touched by Xp}. Remark: in any state, ρratio ≤m and Ppρ⊕,p ≤ 3; hence 1 /g ( ρ ) ≥ 1 / (1+ m + n ) α≥ 1 /poly ( n, m ). Remark 1 (On the properties of ρ ).The proofs of (L1) (fairness), (L2) (amortization), and (T3) (polynomial bound) use only properties (P1)–(P5). The explicit realization ρ = ρratio + Pp∈{2,3,5}ρ⊕,p satisfies (P1)–(P5) and is computable in polynomial time. 2.3 Class gand perceived time τ Given. g(ρ) = (1 + ρ)αwith α∈(1/2,1] and dτ =dt/g(ρ). Consequence. If ρ≤m + n , then 1 /g ( ρ ) ≥ (1 + m + n ) −α = Ω(1 /poly ), and thus each step dt = 1 creates aminimal advance ∆τmin = Ω(1/poly). 2.4 Weighted discrete potential Φ? Principle. The potential counts only reducible heads (unit, binary local binary projection , triplets) and the linear defects defectp. Let HUP ( s )be the set of active units, HBIN ( s )the set of active binaries (local binary projection), H4 ( s )the set of active injective triplet motifs. For p∈ { 2 , 3 , 5 } , define the nullity defectp(s) := #varsp(s)−rankF(p)Xp(s)≥0. We then set Φ?(s) := X e∈HUP(s)∪HBIN(s)∪H4(s) 1 g(ρe(s)) +X p∈{2,3,5} defectp(s) g(ρ⊕,p(s)), g(ρ) = (1+ρ)α, α ∈(1/2,1]. (1) Initial bound. # HUP + # HBIN + # H4≤ (2 + κ4 ) m , and Ppdefectp≤ 3 n , hence Φ ? init ≤ (2 + κ4)m+ 3n= poly(n, m). Remark 2 ( κ4 constant).By definition of the injective triplet motif, one clause can support at most κ4 disjoint occurrences of the motif; κ4 is a universal constant fixed a priori by the motif shape (typically κ4≤3). This implies #H4≤κ4m, whence Φ? init ≤(2 + κ4)m+ 3n. 2.5 Valid operations and deterministic selection (i) UP (unit propagation). (ii) Safe linear closure LinClose+ ( p ), p∈ { 2 , 3 , 5 } : extract Xp (cf. Subsection 2.6) and run the incremental pivot test (online Gaussian elimination): if the candidate row is independent, integrate it (rank increases by one); otherwise if a combination yields 0 = 1, emit UNSAT (mod p); else skip (no modification, ∆Φ?= 0). (iii) Local injective triplet: finite discrete motif (no parameter) enabling an equi-satisfiable contraction (detail in the technical appendix). (iv) Local binary closure R β –BinClose: on the binary projection F(2) of a Tk -anchored block, build G , compute SCCs; if x∼ ¬x in the same SCC ⇒ UNSAT; otherwise inject units (UP) in a topological order (cf. Rule 2.3). 5 Lemma 1 (Strict decrease under LinClose+ ( p )).Each effective application of LinClose+ ( p ) achieves ∆defectp≥1and, consequently, ∆˜τΦ?≤ −1. Rule 2.1 (No-Retest per epoch).Fix an anchored block and a prime p∈ { 2 , 3 , 5 } . An epoch is the execution interval between (and excluding) two successive rank ↑ events (or the appearance of a 0 = 1 row). During an epoch, each candidate row r submitted to the incremental pivot test of LinClose+ ( p )is classified accepted (independent), contradictory (0 = 1), or rejected (linear combination). Rule. Any rejected row is marked (with its fingerprint) and cannot be retested within the same epoch. Marks are reset only when the basis evolves (rank ↑). Proposition 1 (Strict bound on skips per block corrected version).Let a block be anchored over F ( p )and consider an epoch (interval between two rank increases or a 0=1row). Under the no-retest rule (Rule 2.1), the number of rejected attempts (skips) during an epoch is at most the number of unmarked rows, in particular ≤mp .Reset. Marks are cleared only when an independent pivot is accepted (rank ↑) never otherwise. Hence, no repeated-test (livelock) loop is possible: over the whole execution, each row is tested only a number of epochs ≤ the number of rank increases, so the total number of skips is polynomial. Proof. Each rejected row is marked and will not be tested again during the current epoch. Thus the number of rejections is bounded by the remaining unmarked rows. As soon as an independent pivot appears, rank increases and the epoch ends. Corollary 1 (Global attempt bound for LinClose + ( p )).Let mp be the number of candidate rows over F ( p )extracted across all blocks. Under Rule 2.1, the total number of rejected attempts over the whole run is OPpmp·rankp≤O ( mn ). Hence the wallclock overhead of failed tests is polynomial. Definition 2.1 (LinClose + ( p )ledger mandatory rejections).The ledger records, for each block and for each p:(i) the ordered list of accepted pivots (columns, indices), (ii) the list of rejected rows (row hash + causal pivot column), (iii) abasis_fingerprint_at_rejection (hash of the basis just before the rejection). The verifier replays Gaussian elimination, checks each rejection against the logged basis fingerprint, and confirms that the rejected row is a linear combination of the previous ones. Lemma 2 (Injective triplet: decrease of M +BinClose).Under the measure M of Definition 2.5, substituting C = ( a∨b∨z )by y↔ ( a∨b )and ( y∨z )then applying R β –BinClose (cf. Rule 2.3) on the induced binary projection in the Tk -anchored block yields either a local contradiction (SCC with y and ¬y ), or additional unit injections (UP). In all cases, ∆ M≤− 1and, by (L2), ∆˜τΦ?≤ −1. Proof. The triplet introduces ( y∨¬a ),( y∨¬b ),( ¬y∨a∨b )and replaces C by ( y∨z ). The local binary projection over {a, b, y, z} is handled by R β –BinClose: either it detects a conflict (SCC y∼ ¬y ) ⇒ UNSAT, or it yields units (UP) that strictly reduce M . In both cases, the added clauses belong to Canon and the decrease ∆ M ≤ − 1holds; (L2) then gives the bound in τ . Priority rule (fixed). UP >LinClose+(p)>Rβ–BinClose >triplet , then lexicographic tie-break ( Tk,type,indices ). Selection seeks the arg max of ∆Φ ? within the minimal layer Tk that has an active defect. 2.6 Detection mod p(deterministic scheme) We use a fixed palette of canonical CNF gadgets for linear constraints over F(p): •XOR mod 2: standard parity templates (staircase clauses) for Pxi≡b(mod 2). 6 • Sum mod 3: ternary adder networks on the Boolean alphabet via modular counters (sum gates encoded in CNF with no free parameter). • Sum mod 5: same principle with a small modulo-5 counter (5 states), size O ( k )for k inputs. The detection scans subgraphs isomorphic to the templates (bounded sizes, deterministic local signatures), reconstructs the matrix Xp (one row per gadget), and adds the corresponding equation. Total detection cost: O ( m )per pass; ≤O ( poly )with a bounded number of passes. The verifiable conversion CNF↔ Xpis deterministic and standard. Definition 2.2 (Canonical local signatures (PTT)).In b F (after R0, R1–R7.5), a subgraph is said to be: 1. aLinear block if it is a connected component (CC) of the canonical graph Glin containing only gadgets Xor (parities mod 2), G2/G3 (counters mod 3/5), Eq, and/or an additive automaton ripple+repli (R8bin q) verifying CstThresh (Proposition 8). 2. aCandidate conservation pack if one can read, only through canonical motifs, an aggregate S = PK i=1 zi with zi∈ {tj} (occupation bits, Definition 5.2) and/or zi∈ {uC} (R0 witnesses), and local incident constraints providing demands (AT-LEAST/EXACT) and capacities (AT-MOST/EXACT-ONE), all anchored and with span ≤1. 3. a Scalar remainder otherwise (the allowed corridor is UP/Rβ–BinClose/triplet). Algorithm 1 PTT-Pattern-Detector(F0)(where F0=R0TL(F)then R1–R7.5) 1: Build Glin (nodes = vars/gadgets Eq/Xor/G2/G3/R8bin q). 2: (i) Linear blocks: take the CCs of Glin; in each, check CstThresh (Proposition 8). 3: (ii) Candidate packs: collect Z := {tj} ∪ {uC} ; for each anchor Tk , take the connected components of the subgraph incident to Z; in each component, aggregate L:= X(EXACT/AT-LEAST demands), U := X(AT-MOST/EXACT-ONE capacities), K := |S|. 4: (iii) Scalar remainder: everything that is neither (i) nor (ii). 5: Output: partition (L,P,S)(linear, packs, scalar). Lemma 3 (Exhaustive partition ( L,P,S )).For F0 after R0–TL and R1–R7.5, the algorithm PTT-Pattern-Detector (Algorithm 1) produces a disjoint partition ( L,P,S )such that every gadget/clause of F0 belongs to exactly one of the three classes. In particular, every z∈Z := {tj} ∪ {uC} belongs to a unique connected component of the subgraph incident to Z ; this very decomposition indexes the packs. Proof. By definition (Definition 2.2), a subgraph is classified (i) linear if it contains only canonical gadgets Xor, G2/G3, Eq and/or an additive automaton ripple+repli satisfying CstThresh; (ii) conservation pack if it is generated by bits Z := {tj}∪{uC} and their incident constraints EXACT/AT-LEAST/AT-MOST/EXACT-ONE; (iii) scalar otherwise. The signatures are disjoint by construction (canonical library and anchoring/span ≤ 1); the scan covers all gadgets instantiated by R0 and R1–R7.5. Hence the partition is exhaustive. Lemma 4 (Partition invariance under R1–R8, UP, R β –BinClose, triplet).Let ( L,P,S )be the partition of F0 returned by PTT-Pattern-Detector (Lemma 3). After applying any single valid operation among R1–R7.5, R8 bin q , UP, R β –BinClose, LinClose + ( p ), or the injective triplet, the updated instance admits a (re)computed partition ( L0,P0,S0 )such that: (i) every object belongs to exactly one class, (ii) no object switches class unless its local signature has changed to 7 match the canonical library of another class, and (iii) new objects introduced by the operation are all canonical and therefore classified deterministically. Proposition 2 (100% syntactic detection, no SAT oracle).PTT-Pattern-Detector (Algorithm 1) uses no implication test nor SAT search: it only reads finite local signatures from the canonical library (Tseitin/counters/constant-threshold comparators). Its complexity is O(poly(|F0|)). Proposition 3 (Correctness and complexity of PTT-Pattern-Detector).Detection relies only on canonical signatures (Definition 2.2), hence with no internal SAT. The partition ( L,P,S ) is computed in O(poly(|F|)). Lemma 5 (No false positives/negatives for PTT-Pattern-Detector).Restricted to the canonical library (Appendix D), PTT-Pattern-Detector returns linear if and only if the subgraph is a composition of Eq/Xor/G2/G3/R8 bin q gadgets with span ≤ 1 and constant thresholds. It returns pack if and only if the subgraph is generated by Z := {tj}∪{uC} and their incident (EXACT/AT-LEAST/AT-MOST/EXACT-ONE) constraints. Otherwise it returns scalar. Universal PTT normalization (R1–R7). We fix a finite base of local rewrites, all deterministic Definition 2.3 (Canonical Tseitin library).Boolean networks are encoded in CNF by Tseitin definitions over the gates Eq,Not,And,Or,Xor,Mux, and the comparator Cmp ≥q . The exact clauses of these gates are listed in Section D. Rule 2.2 (R0 – PTT-Universal-Threshold-Lift).For each clause C = ( `1∨`2∨`3 )anchored at Tk , introduce a local counter fC∈ { 0 , 1 , 2 , 3 } implementing fC = `1 + `2 + `3 via a constant-size binary network (2-bit ripple, Section D) and a constant-threshold comparator uC↔Cmp≥1 ( fC ) (threshold 1 wired by Eq). Declare uCas required. Proposition 4 (R0: equi-SAT, span and anchoring, cost).Transformation R0 is equi-satisfiable ( C true iff uC = 1), preserves span ≤ 1and the anchoring Tk , and its total cost is O ( |Cl| ) (constant per clause). The Xor/And/Eq/Cmp gadgets used belong to Canon. Definition 2.4 (R0 ledger).For each C , record ( ID ( C ) ,ID ( fC ) ,ID ( uC )) and the hash of the definition clauses added (gadget ID from the library). Theorem 1 (R0–Universal-Threshold-Lift: equi-SAT, span ≤ 1, anchoring, size).Let F be a 3-CNF (possibly after R1–R7.5). Apply Rule 2.2 to each clause C = ( `1∨`2∨`3 )anchored at Tk , introducing the counter fC = `1 + `2 + `3 (Sum3 constant size) and uC↔Cmp≥1 ( fC ), and declare uCrequired. Then: 1. (Equi-SAT)Cis true iff uC= 1. 2. (Span/anchoring) The R0 gadget lives within span ≤1and remains anchored in Tk. 3. (Size) Total cost O(|Cl|)(constant per clause), all gadgets in Canon. 4. (Ledger) For each C , record ( ID ( C ) ,ID ( fC ) ,ID ( uC )) and the hashes of the definition clauses. Definition 2.5 (Extended termination measure).We split M into pre-anchoring M0 (independent of H(ů)) and post-anchoring M1. M0(F) := X C∈F\Canon (|C| − 2)++ #Intneutre(F) + #Supplin6anc(F) + #Gates6∈Canon(F), M1(F) := X p∈{2,3,5} defectp(F)and M(F) := M0(F) + M1(F). Here Canon contains all internal canonical clauses/gadgets (equality Tseitin, exactly-one, XOR, counters mod 3/5, R8bin qlogic), see Definitions 2.3 and 2.14. 8 Lemma 6 (Measure impact of R0).The clauses of R0 belong to Canon ; introducing uC does not degrade M0 . The bounded terminals instantiated by PTT-Cut induce heads (terminal clauses) that consume Φ?; in case of falsification, one obtains UNSAT immediately. Lemma 7 (Decrease per effective step).Every effective operation (UP, R β –BinClose, injective triplet, LinClose + ( p )pivot, conform R8 insertion) achieves ∆ M≤− 1.Skips do not consume Φ?nor Mand are bounded by Proposition 1. Proposition 5 (Final size and number of steps).The number of effective steps is ≤ M ( F0 ) = poly ( |F0| ), and the size of b F remains polynomial: each step adds O (1) canonical objects outside R8 and O(log q)per transition inside R8 (Lemma 21). In particular |b F|= poly(|F0|). Definition 2.6 (R1 – PTT-Scalar Write).For any clause C = ( `1∨ · · · ∨ `q )of size q≥ 4, anchored at Tk (minimal touched layer), introduce q− 3fresh variables y1, . . . , yq−3 anchored at Tkand replace Cby the 3-CNF chain: (`1∨`2∨y1)∧(¬y1∨`3∨y2)∧ · · · ∧ (¬yq−3∨`q−1∨`q). Selection: R1 is triggered only if C is (i) mixed Tk / ≥Tk+1 or (ii) marked long linear (see R6). Equi-SAT. Standard 3CNF Tseitin (eliminating the yi⇒C ). Cost. q− 3variables/clauses. Measure. The selection ensures ∆# Intneutre ≤ − 1 or ∆# Supplin6anc ≤ − 1(cf. R3/R6), hence ∆M ≤ −1. Definition 2.7 (R2 – PTT-Anchor Split).In any clause/gadget anchored at Tk , for any literal ` ( v )whose minimal layer is >k , introduce an eq-clone v(k) anchored at Tk and replace ` ( v )by `(v(k)), adding (¬v∨v(k))∧(v∨ ¬v(k)). Equi-SAT. Equivalences. Cost. 2 binaries/clone. Measure. ∆#Supplin6anc ≤ −1. Definition 2.8 (R3 – PTT-Interface Guard).For any mixed clause ( A∨B )with A (anchored Tk) and B(anchored ≥Tk+1)without active border, add a guard gkanchored at Tk: (A∨B) (A∨gk)∧(B∨ ¬gk). Equi-SAT. Tseitin. Measure. ∆#Intneutre =−1. Definition 2.9 (R4 – PTT-Parity Lift).A chordless odd cycle in the 2-CNF skeleton ⇒ XOR gadget (G1) anchored at Tkenforcing Liui=b. Equi-SAT. Standard. Measure. ∆#Supplin6anc ≤ −1. Definition 2.10 (R5 – PTT-Counter Lift).Triadic motif ⇒ counter mod 3/5 (G2/G3) anchored, size O(k), connected to the original clauses. Equi-SAT. Standard. Measure. ∆#Supplin6anc ≤ −1. Definition 2.11 (R6 – PTT-H-Enforce).If a linear support touches Tk and Tk+r ( r≥ 2), apply eq-clones (R2) toward Tkor Tk+1 until span ≤1. Equi-SAT. By R2. Measure. Each iteration strictly reduces #Supplin6anc. Definition 2.12 (R7 – PTT-Eq-Clone Canonical).In each layer, merge all equalities v(k)↔v(k) j into a canonical clone v(k); propagate/substitute. Equi-SAT. Logical redundancies. Measure. Contraction (residuals ↓). Rule 2.3 (R β –BinClose (local binary closure)).In a Tk -anchored block, let F(2) be the anchored binary projection (Def. 2.13) of the clauses (literals over {x, ¬x} ). Build the implication graph G(edges u→vfor each binary (¬u∨v)), compute strongly connected components (SCC). • Conflict: if there exists a variable x such that x and ¬x belong to the same SCC, conclude UNSAT (local binary contradiction). • Propagation: otherwise, choose a compatible orientation (topological order) and inject the corresponding units (UP) into the corridor (layers Tk/Tk+1). 9 at least one bit st+1 j , we obtain a dependency Ut st+1 j independent of xt , contradicting F0 = Id (for at least one pair Ut, U0 t ). The only possibility consistent with F0 = Id is that each qi be constant under xt= 0: ∀UtGi(Ut,0) ≡ci∈ {0,1}. B2) Case xt = 1 (bijectivity of F1 and span ≤ 1). Assume for contradiction that there exists isuch that Gi(Ut,1) depends on at least one bit st `. Two subcases: • Global fan-out of geq .In the canonical library (cf. Section D), geq typically drives one Mux per bit ( b distinct MUX) to choose between S0 and S0−q . There are then edges geq →st+1 k for all k . Since Gi depends on st ` , there exists a path st ` geq st+1 k for all k . Choose k /∈ {`, `−1}: this violates the span ≤1constraint. • Realization by a borrow chain (ripple subtraction). Even without a global MUX, the conditional subtraction by borrows has b−1 := geq and bi := Bor ( s0 i, qi, bi−1 ). If some qi depends on st ` with ` < i − 1, then st ` qi bi bi+1 · · · st+1 k for all k≥i , again yielding non-local dependencies (span >1). In both subcases, any dependence of q on Ut violates either span ≤ 1or (if one tried to mask it) the local injectivity of F1 via collisions. It follows that, under xt = 1 as well, each qi must be constant. Since in B1 we already had qi≡ciunder xt= 0, we conclude qi≡ciglobally. B3) Local rewrite sequence. For each rail qi produced by a cone Gi , introduce an Eq qnew i↔ci (unit ci∈ { 0 , 1 } ), substitute qnew i in place of Gi in the comparator, then eliminate the cone Gi by propagating equalities (Eq). All these steps are equi-SAT and local. Span ≤ 1is unchanged (replacement by constants). C) Complexity. Each rewrite (local Eq, substitution, removal of a cone by propagation) touches a number of clauses/variables bounded by the size of the node at hand; the full sequence visits at most O(|C|)nodes. Hence an overhead O(|C|). Corollary 3 (Ripple+fold-back uniqueness without assumptions).Combining Lemma 25 with Lemma 24, any cell (span ≤ 1) satisfying F0 = Id and F1 bijective is equivalent (local Tseitin rewrites, equi-SAT, span preserved) to ripple ( c−1 = xt , st+1 i = st i⊕ci−1 , ci = st i∧ci−1 ) possibly followed by a fold-back Cmp≥qwith constant threshold + MUX. Theorem 4 (Complete local classification).In any canonized cell (R7.5) with span ≤ 1such that F0 = Id and F1 is a degree-1 bijection, Proposition 8 holds and ReadQ (Algorithm 2) returns qin O(|C|). The proof combines Lemmas 23 to 25 and the structural read Lemma 26. Lemma 26 (Canonical reading of q in polynomial time).Let C be an update cell (span ≤ 1) after R7.5. In time O ( |C| )we can: (i) detect the carry chain c−1→c0→· · ·→cb−1 (ripple), (ii) decide whether a fold-back exists and, if so, (iii) read the constant vector ( qb−1, . . . , q0 )of the reference rails of Cmp ≥q and reconstruct q = Pi 2 iqi . If there is no fold-back, the period is q= 2b. Proof. After R7.5 and Lemma 25, xt has external degree 1and any Cmp ≥q is constant-threshold. A local DFS of the DAG extracts c−1, . . . , cb−1 by following the canonical And/Xor motifs. We then test for a fan-out from S0 to a Cmp ≥q (or an equivalent borrow chain) and read its reference rails, which are tied to constants via Eq. Absence of the comparator implies q = 2 b . All operations are local and in O(|C|). Proposition 8 (Syntactic CstThresh criterion ⇔ ripple+fold-back).In a cell C (span ≤ 1), conditions (i) external degree 1for xt , (ii) Cmp ≥q at constant threshold (Definition 2.23), (iii) F0 = Id and F1 a degree-1bijection (Def. 2.21) are necessary and sufficient for the update to be isomorphic to ripple followed by an optional fold-back. 16 Algorithm 2 ReadQ(C)structural reading of qin O(|C|) 1: Check CstThresh (Proposition 8); otherwise return None (non-derivable). 2: DFS of the Xor/And cones: extract c−1, . . . , cb−1(ripple chain). 3: Detect a possible Cmp≥q; read its constant rails (qb−1, . . . , q0). 4: If Cmp absent then q←2belse q←Pi2iqi. 5: return q. Corollary 4 (Detection of q without guessing).For any constraint σt+1 = σt + xt ( modq ) encoded after R7.5, q is uniquely determined by the structural reading provided by Lemma 26; no simulation on unassigned xtis required. Theorem 5 (Universal normalization in polynomial time (R1–R8)).Any 3SAT instance F is transformed, by deterministic pre-processing in O ( poly ( n, m )) preserving satisfiability, into an instance b F satisfying H(T–anchor)+H(T–lin), where all linear constraints are expressed via G1–G3 (mod 2,3,5) and Boolean equalities. Proof. By R1–R7: unique anchoring, span ≤ 1, removal of neutral interfaces (Lemmas 11 and 27). By R8 bin q : exact emulation of mod q constraints via a binary register (ripple + fold-back), G1–G3 and finite CRT tables; all steps are local and polynomial. Equi-SAT follows from local proofs of each rule; termination follows from the strict decrease of Mat each application. By Lemma 12, the R1–R7 normal form is unique up to equality isomorphisms. Lemma 27 (H-enforcement).After exhausting R1–R7, H (T -anchor )and H (T -lin )hold on b F : every object (clause, variable, gadget) admits a unique anchor Tk , and every linear support is an internal block or an immediate cut Tk–Tk+1 (span ≤1). Proof. Literals off-anchor are systematically cloned to the anchor (R2); equalities are canonically normalized (R7), hence uniqueness of anchoring. Any linear support with span ≥ 2is contracted by R6 (repeated anchor splits) down to span ≤ 1. Mixed interfaces without active border are guarded by R3, thus ceasing to be neutral; the block/cut classification follows. Lemma 28 (Disjoint decomposition of aggregates after R1–R7).In b F , the canonical graph Glin (nodes = variables/clones, edges = Eq/Xor/mod-3/5 comparators, R8 bin q comparators/MUX) decomposes into connected components {A`}such that: (i) each A`supports exactly one aggregate anchored at Tk(internal block or immediate cut), (ii) two distinct aggregates have disjoint supports in the primary variables, (iii) any equality/cloning between two aggregates merges these components under R7, and is thus absorbed into a single aggregate. Proof. By R2, any off-anchor literal is cloned to the anchor; by R6, any span ≥ 2is contracted to span ≤ 1; by R7, all equalities between clones are merged. The connected components of Glin then coincide with the CCs of linear gadgets and equalities: if two aggregates shared a variable or a clone, they would lie in the same CC and hence be the same aggregate. Lemma 29 (Scalar separation of crossing clauses).In b F after R1–R7, let C = ( `1∨`2∨`3 ) be anchored at Tk and mix at least two distinct aggregates. Then, in the allowed corridor (BinClose+UP, triplet), one of the two alternatives occurs in O(1) steps: 1. Guarding (R3): if no Tk→Tk+1 border is active, R3 yields ( A∨gk ) ∧ ( B∨ ¬gk ), which decouples the aggregates. 2. Local head: otherwise, 17 (a) if two literals of C belong to the same aggregate, a triplet factorization y↔ ( `i∨`j )creates an incident binary (y∨`r)anchored at Tk; (b) else, UP on the Tk+1 side contracts in at most |C| − 2steps down to an incident binary. In (a) and (b) we apply R β –BinClose on the local binary projection (then UP), and ∆ M ≤ − 1, ∆˜τΦ?≤ −1. Definition 2.24 (Saturated CRT table).For a terminal ( q, K, b ), Tq,K ( b )is said saturated if Rq,K ( b ) = {r∈ { 0 , . . . , 29 } | ∃m∈ [0 ..K ] , m ≡b ( mod q ) , r ≡m ( mod 30) } coincides with the full image of the coset b+qZin Z/30Z(i.e., size 30/gcd(q, 30)). Lemma 30 (Independence under saturated tables).Let aggregates be disjoint (disjoint supports by Lemma 28). Assume that for each active terminal uK`,b` , Tq`,K` ( b` )is saturated (size 30 /gcd ( q`, 30)). Denote by Vars(`) ctr ⊆Var the set of counter variables (G1/G2/G3 and selectors V(`) r) attached to aggregate `. Then: 1. Factorization of selectors. The selector families are pairwise disjoint: Vars(`) ctr ∩Vars(`0) ctr = ∅ for `6 = `0 , since each aggregate receives a distinct copy of G1/G2/G3 and an exact-one family {V(`) r}29 r=0. 2. No residual coupling. Coherence clauses ( V(`) r⇒bits of G1/G2/G3 )mention only Vars(`) ctr and local {xt} of the same aggregate. No canonical gadget (Eq/Xor/G2/G3/Cmp) bridges two distinct aggregates after R1–R7 (Lemma 28). 3. Independent choice of residues. Saturation implies that for each ` and each admissible residue class mod 30 in the coset b` + q`Z , there exists m`∈ [0 ..K` ]realizing it. Hence we can fix m`independently for each `and satisfy all constrained triplets (r2, r3, r5)in parallel. Therefore the global CNF factorizes conjunctively across aggregates on the counter/selector side, and any residual UNSAT must lie in the scalar remainder S(where Theorem 7 applies). Proof. Since the aggregates are disjoint, G1/G2/G3 and the selectors Vr factor by component. Saturation means that, for any m≡b` ( modq` ), the class mmod 30 is allowed; thus the local outputs ( r2, r3, r5 )no longer introduce coupling. We therefore choose m`∈ [0 ..K` ]independently for each aggregate. The only remaining clauses linking components are scalar; by Lemma 29, they are guarded or yield a head. If UNSAT persists, it falls into the scalar remainder, treated by Lemma 52. Moreover, the families of selectors {Vr} are disjoint by aggregate (distinct variable names), so no inter-pack exact-one exists and no hidden coupling is introduced. Lemma 31 (No recoupling post saturation).After R1–R7 and saturation of all active Tq,K ( b ) tables, no canonical edge (Eq/Xor/G2/G3/Cmp with constant thresholds) connects two distinct linear connected components; any scalar clause touching two components is either guarded by R3 or becomes a local head in O(1) corridor steps. Lemma 32 (No re-coupling under saturated CRT and corridor steps).Assume all active terminals are saturated and selectors are aggregate-scoped (Def. 2.18). Then any sequence of corridor steps (UP, R β –BinClose, injective triplet) applied to scalar clauses cannot create a cross-aggregate canonical edge nor a clause whose variables break the disjointness of linear supports. Proof. By Lemma 8,R β –BinClose stays inside the anchored block; the triplet is local; UP does not introduce new variables. With Def. 2.18 and Lemma 17, no selector/counter is shared; hence no canonical bridge can appear between aggregates. 18 Theorem 6 (SmallPrime Sufficiency under H(Tanchor/lin)).Let b F be obtained from F by R1–R8 with gated R8 (Definition 2.15) and assume H (T -anchor )and H (T -lin )hold. If no linear block produces 0=1over any p∈ { 2 , 3 , 5 } and, for each active terminal uK,b , the table Tq,K (b)is saturated (Definition 2.24), then: 1. any remaining UNSAT necessarily lies in the scalar remainder S and is derivable by the corridor (Theorem 7); 2. conversely, if the scalar remainder Sis satisfiable, then b Fis satisfiable. In particular, no prime p > 5is ever needed by the decision pipeline under these hypotheses. Proof. By Lemma 28, linear supports are disjoint; by Lemma 31 together with Lemma 30, saturated CRT removes any residual coupling through canonical gadgets. By Lemma 29, any crossing scalar clause is guarded or localized into heads. Hence any remaining UNSAT lives in the scalar remainder where Theorem 7 applies : no multi-mod constraint remains. Therefore any remaining contradiction lives in S, and Theorem 7 concludes. Lemma 33 (Linear reduction to CRT-30 (single block, bounded width)).Let there be a single contradictory linear block of width K≤K0 (library constant), and no 0=1modulo 2 , 3 , 5. Then the contradiction yields a combined violation captured by the bounded CRT-30 table via the terminals (Definitions 2.16 and 2.17). Proof. Let d := gcd ( q, 30) and let π : Z→Z/ 30 Z be the projection. The image π ( b + qZ )is a coset of the subgroup dZ/ 30 Z and has cardinality 30 /d . Under the sequential read, only values m∈[0..K]are reachable; hence R:= {π(m)|m∈[0..K], m ≡b(modq)}satisfies |R| ≤ min(K+1,30/d). By the product isomorphism Z/ 30 Z≃Z/ 2 Z×Z/ 3 Z×Z/ 5 Z , the bounded compatibility set Tq,K ( b )(Def. 2.16) is exactly the set of triplets ( r2, r3, r5 )induced by R . If there is a single contradictory linear block of width K≤K0 and no 0 = 1 over p∈ { 2 , 3 , 5 } , the counters produce a triplet ( r2, r3, r5 )that cannot arise from any m∈ [0 ..K ]with m≡b ( modq ); i.e. ( r2, r3, r5 ) /∈ Tq,K ( b ). By Theorem 3, the terminal clause ( ¬uK,b ∨Wr∈Rq,K (b)Vr )is therefore falsified, yielding a bounded CRT30 conflict. The verifier recomputes R from ( q, K, b )and replays G1/G2/G3 in O(K), so the certificate is polynomial. Definition 2.25 (Alternating graph Galt = ( L∪P, E )).For an anchored (span ≤ 1) 3-CNF Fscal without units or peelable binaries: •L= set of active literals; •P=negative pairs {¬a, ¬b}such that there exists (a∨b∨z)∈Fscal; • for each ( a∨b∨z ) ∈Fscal , add the arcs ¬a→ {¬a, ¬b} , ¬b→ {¬a, ¬b} and {¬a, ¬b} → z , as well as the two cyclic variants by permuting (a, b, z). Lemma 34 (Properties of Galt).Under span ≤1and absence of units/peeling: (i) Galt is finite; (ii) every literal in L has out-degree ≥ 2(otherwise an incident binary (handled by R β –BinClose) would exist); (iii) if a pair (a, b)repeats, then two clauses share (a∨b). 19 Lemma 35 (No new repeated pair outside the corridor under Tseitin).Under span ≤ 1and after R7 canonization, introducing the three definition clauses Tseitin ( ¬y∨a∨b ),( y∨ ¬a ), ( y∨ ¬b )for y↔ ( a∨b )does not induce any new repeated pair {¬a0,¬b0} among original literals outside the touched clauses. In particular, any repeated pair {¬a0,¬b0} post-operation either comes from the modified clauses, or was already present before. Lemma 36 (Stability of Galt under a single triplet).Under span ≤ 1and after R7, let there be an alternating cycle `0→p0→`1→ · · · → `r with `r = ¬`0 . Choose an edge pj = {¬a, ¬b} → z issued from (a∨b∨z), and apply a single triplet factorization y↔(a∨b). Then: 1. The induced binary subsystem on {a, b, y, z} is fully handled by R β –BinClose in the Tk - anchored block. 2. No new escaped alternating cycle is created: y does not introduce a repeated pair on the original literals (span ≤1, clones merged by R7). 3. The outcome of BinClose is either a local contradiction (SCC u∼ ¬u ), or units (UP) that propagate along the cycle until forcing u∧ ¬u , yielding the empty clause. In both cases, ∆M ≤ −1. Lemma 37 (Cycle propagation ⇒ empty clause).Let Galt contain an alternating cycle `0→ p0→`1→ · · · → pr−1→`r with `r = ¬`0 in an anchored span ≤ 1 scalar remainder. After applying a single triplet y↔ ( a∨b )on any edge pj = {¬a, ¬b} → z and running R β –BinClose, unit propagation forces the empty clause in O(r)steps. Proof. By Lemma 36,( y∨z )is an incident binary; R β –BinClose orients the binary projection consistently with the implication flow. We prove by induction on the cycle length r . For r = 2, the two-step implication yields u∧ ¬u immediately. Assume true up to r− 1. For length r , the oriented edges around the cycle and the Tseitin clauses ( y∨ ¬a ),( y∨ ¬b )propagate one unit along the cycle at each step (no escape by Lemma 35); after O ( r )steps we reduce to the r− 1 case, forcing u∧ ¬u. Locality and span ≤1 ensure no cross-component effect. Lemma 38 (Corridor pre-conditions ensured for the remainder S ).If, in F0 , all linear blocks in L are saturated (no 0=1mod p nor CRT falsified) and all packs in P satisfy L≤U , then the remainder S is an anchored (span ≤ 1) 3-CNF without units or peelable binaries. In particular, Ssatisfies the hypotheses of Theorem 7. Example 1 (Scalar corridor: repeated pair vs alternating cycle (minimal log)).Case 1 (pair). Two clauses share ( a∨b ): C1 = ( a∨b∨z1 ), C2 = ( a∨b∨z2 ). Apply once y↔ ( a∨b ), replace Ci by ( y∨zi ), then R β –BinClose+UP on {a, b, y, z1, z2} : we obtain either an SCC ( u∼ ¬u ), or units that propagate to the empty clause; at each step ∆M ≤ −1. Case 2 (cycle). If there is no repeated pair, the alternating graph (Definition 2.25) contains a cycle u→ · · · → ¬u . Choose an edge {¬a, ¬b} → z issued from ( a∨b∨z ), apply one factorization y↔ ( a∨b ), then R β –BinClose+UP; propagation along the cycle forces u∧ ¬u (empty clause). No free resolvents are used. Lemma 39 (Exhaustive corridor invariant).Within the allowed corridor (UP, injective triplet, R β –BinClose) on an anchored span ≤ 1 scalar remainder, each step strictly decreases M by at least 1, and no step can recreate a non-corridor configuration. In particular, the pair-orcycle alternative remains invariant under a single triplet followed by R β –BinClose+UP, and no inter-component coupling is introduced. Sketch. Immediate from Lemmas 7,9,35 and 36 and the locality/anchoring of all gadgets. Theorem 7 (Scalar local completeness).Let Fscal be an anchored (span ≤ 1) 3-CNF that is unsatisfiable, with no units and no incident binary (handled by R β –BinClose). Then there exists a finite sequence of allowed operations (UP, injective triplet, R β –BinClose on the local binary 20 projection) that derives an empty clause. At each step, ∆ M ≤ − 1and ∆ ˜τ Φ ?≤ − 1. The length of the sequence is poly ( |Fscal| ).Note. The corridor uses no free resolvent: only UP, R β –BinClose and the injective triplet (Tseitin extensions). Proof. By Lemma 39 and Lemma 37, each allowed step strictly decreases M and preserves the corridor structure. Two cases. (1) Repeated pair. If there exist C1 = ( a∨b∨z1 )and C2 = ( a∨b∨z2 ), apply the triplet once (fresh variable y ): y↔ ( a∨b )(cf. Section D), C17→ ( y∨z1 ), C27→ ( y∨z2 ). Apply R β –BinClose on the local binary projection {a, b, y, z1} (then UP) ⇒ ∆ M≤− 1; by (L2) ∆˜τΦ?≤ −1. Iterate UP/Rβ–BinClose up to a unit contradiction. (2) No repeated pair: signed alternating cycle. Perform an alternating BFS in Galt from u∈L : finiteness + non-repetition ⇒ a cycle u = `0→p0→`1→ · · · → `r with `r = ¬`0 . Choose an edge pj = {¬a, ¬b} → z issued from ( a∨b∨z ); apply exactly once y↔ ( a∨b ):( y∨z ) is an incident binary;R β –BinClose+UP suffice. The clauses ( ¬y∨z ),( y∨ ¬a ),( y∨ ¬b )activate the implications around the cycle and force a pair y, ¬y by UP, whence the empty clause. Each step is local, respects the span, and ∆M ≤ −1,∆˜τΦ?≤ −1. Corollary 5 (Mechanical script for deriving the empty clause).Under the conditions of Theorem 7, there exists a deterministic sequence ( op1, . . . , opr )with r = poly ( |Fscal| )such that, for each t, 1. Construction of Galt (Definition 2.25) and test repeated pair vs alternating cycle. 2. If repeated pair ( a∨b ): apply a single factorization y↔ ( a∨b )(Lemma 35), then R β –BinClose on the local binary projection; inject units (UP) or conclude UNSAT;∆ M ≤ −1. 3. Otherwise (alternating cycle): choose an edge pj = {¬a, ¬b} → z , apply one factorization (Lemma 36), then Rβ–BinClose and propagate (UP) along the cycle up to u∧ ¬u. 4. Logging: record (opt,∆M)and the BinClose ledger. Each step is local, respects the span, and satisfies ∆˜τΦ?≤ −1. Design commitments (taken a priori) and consequences. Taken: T (global order via SCC+BFS), properties (P1–P5) for ρ , g ( ρ ) = (1 + ρ ) α ( α∈ (1 / 2 , 1]), weighted Φ ? , fixed set P = { 2 , 3 , 5 } , rules R1–R7 and modules R8 bin q , linear detection mod p , deterministic scheduling. Derived: Fairness (L1), amortization (L2), No-False-Silence, linear completion and SPC( { 2 , 3 , 5 } ) with certificates. 3 Lemma (L1): deterministic fairness in τ Taken. Order Tby topological BFS; g(ρ) = (1 + ρ)α,α∈(1/2,1]. Statement. For any active pack P at t0 , there exists ∆ τmin = Ω(1 /poly ( n, m )) such that P receives an operation within a τbudget of at most ∆τmin, repeatedly (no starvation). Proof. The DAG D issued from the SCCs has at most 2 n vertices; its depth (number of layers) L≤ 2 n . The scheduler serves the minimal active layer at every episode, with an equity quota: each active layer obtains a fairness service at most every Q := 2 n episodes if it has not been minimal in that window (interface escalation kept unchanged). Passing to τ gives a local advance ∆τ= 1/g(ρlocal)≥1/(1 + ρmax)α. 21 Theorem 8 (Quota fairness (deterministic)).With Q := 2 n and the selection rule minimal active layer with interfaceescalation; grant one fairness tick to any other active layer once its local counter reaches Q , every active layer Th with Φ ? h> 0is served within O ( n )episodes. In τ units, each such service occurs within at most O(n)·∆τmin, where ∆τmin = (1 + m+n)−α. Algorithm 3 Min-Layer+Quota (fair scheduler) 1: Initialize counters q[h]←0for all layers Th; fix Q:= 2n. 2: for episode t= 1,2, . . . do 3: k←min{h:Thhas an active defect} 4: if q[k]< Q then 5: serve Tk;q[k]←q[k]+1;continue 6: end if 7: (fairness tick) serve the smallest h with an active defect and q [ h ] ≥Q ; then set q [ h ] ← 0 8: if Jk>0then 9: allow interface escalation to Tk+1 at the next episode 10: end if 11: end for Now, by § 2.2, ρ = ρratio + Pp∈{2,3,5}ρ⊕,p with ρratio ≤m and Ppρ⊕,p ≤ 3, whence ρmax ≤m + 3 and 1 /g ( ρmax ) ≥ (1 + m + 3) −α . Thus ∆ τ≥ (1 + m + 3) −α = Ω(1 /poly ). Over a full cycle ( L≤ 2 n ), each pack is served at least once; hence the minimal budget is ∆τmin ≥1 L·(1 + m+n)−α= Ω 1/poly(n, m). Therefore, explicitly: ∆τmin ≥1 2n(1 + m+ 3)−α. Reminder potential Φ ? .We recall the definition (1) and its initial bounds; no redefinition is necessary here. Interface escalation rule. If the minimal active stratum Tk satisfies Rk = 0 and Jk> 0, selection at the next step is allowed in Tk+1 (same priorities as previously). Local quantities per stratum. For a state s and the minimal active stratum Tk , define: Φ ? k ( s )as the contribution of Φ ? restricted to the objects (heads and defects) supported in Tk or anchored at Tk for the incident interfaces; Jk ( s )as the number of active interfaces crossing Tk→Tk+1 (non-neutral incidences after simplification); Rk ( s ) ∈ { 0 , 1 } equals 1if there exists at least one valid operation (UP, R β –BinClose, mod p , triplet) entirely in Tk , else 0. A certified silence means Φ? k(s) = 0 and Jk(s) = 0. Structural hypotheses and progress of stubs Hypothesis 3.1 (H(T-anchor)).Every active object (CNF clause, variable, linear gadget mod p) has a unique anchor defined as the minimal stratum Tktouched by its support: k= min{j:supp(X)∩Tj6=∅}. Hypothesis 3.2 (H(T-lin)).Every active linear constraint is either (a) an internal block (supp ⊆Tkfor its anchor k), or (b) an interface cut (supp ∩Tk6=∅and supp ∩Tk+1 6=∅). Proposition 9 (Verifiability in O ( m )).Under (G1)–(G3), multi-mod R1 and local normalization, the hypotheses Hypotheses 3.1 and 3.2 are verifiable in time O(m). Remark 3 (Evolution of stubk ).If a clause C anchored at Tk and of size ≥ 3is shortened by UP/R β –BinClose on the Tk+1 side, its contribution to stubk strictly decreases; after ≤ |C| − 2 steps, Cbecomes binary ⇒Φ? k>0. 22 Lemma 40 ( stubk⇒ future operation).Under Hypotheses 3.1 and 3.2, if stubk ( s ) > 0with Φ ? k ( s )=0and Jk ( s )=0in the minimal active stratum Tk , then in at most O ( m )episodes one of the following occurs: 1. the creation of a local head anchored at Tk (incident binary (handled by R β –BinClose) or injective triplet), hence Φ? k>0and ∆˜τΦ?≤ −1; 2. the activation of an interface flux Jk>0. Proof idea. Any mixed clause Tk – Tk+1 without active border is guarded (R3), whence ∆ M ≤ − 1 (removal of a neutral interface). R1 chains are shortened at each episode; after ≤ |C| − 2steps, an incident binary anchored at Tk appears and is handled by R β –BinClose (then UP). Finally, R2/R6/R7 contract supports toward the anchor (∆ M ≤ − 1). Since M ( F0 ) = O ( m )and these effects persist as long as stubk>0, one of the two alternatives occurs in O(m). Chain details (drop of M and link ∆ τ Φ ? ). Case F1 (scalar Tk – Tk+1 ). The R1 chain introduces q− 3variables yi anchored at Tk . At each served episode, a propagation on the Tk+1 side shortens at least one link: as soon as a binary ( y∨z )appears (anchored at Tk ), we apply R β –BinClose on the local binary projection (then UP), which yields ∆ M≤− 1; by (L2), the head created satisfies ∆˜τΦ?≤ −1. Case F2 (dormant linear block). R4/R5 activate an anchored gadget ( ⊕ , mod 3/5). If no border is active, R3 inserts a guard gk and a neutral interface is removed: ∆ M≤− 1. At the first activation of a border, a linear defect or an incident binary appears, giving the same bound (L2). Case F3 (equalities/clones). R2/R7 substitute/merge and remove at least one off-anchor occurrence: ∆ M ≤ − 1. In all three cases, after O ( m )episodes (initial measure O ( m ), drop ≥ 1 per episode), we obtain (i) a local head or (ii) a flux Jk>0. Lemma 41 (Non-circular enforcement of H(T-anchor) and H(T-lin)).Without assuming H(ů), rules R1R7 are equi-SAT and satisfy ∆ M0≤ − 1at each application. After exhausting R1R7, H(T-anchor) and H(T-lin) hold (Lemma 27). Only then do results invoking H(ů) (including Lemma 42) apply. Remark 4 (Non-circularity).The hypotheses H (T -anchor )and H (T -lin )are never invoked before exhausting R1R7. Lemma 41 formalizes exactly this pre-stabilization step. Lemma 42 (Reinforced No-False-Silence).Let s be a state and Tk the minimal active stratum. Then exactly one of the following occurs: (A) Local operation:Rk= 1 and ∆˜τΦ?≤ −1; (B) Interface flux: Rk = 0 but Jk> 0; at the next step, Tk or Tk+1 admits an operation with the same bound; (C) Certified silence:Φ? k= 0 and Jk= 0. Moreover, if Rk = 0, Jk = 0 but stubk> 0, then by Lemma 40 we reach (A) or (B) in O ( m ) episodes. 4 Linear completion and Small-prime completeness 4.1 Post-normalization linear completion (algorithm & proof) Lemma 43 (Complete normalization of linear constraints).After R1–R7, any CNF subformula encoding a linear constraint over bits {xi} via the canonical library is equi-satisfiable to a composition of Xor (mod 2) gadgets, mod-3 / 5counters (G2/G3), and equalities. In particular, the extraction of X2,X3,X5by motif scanning (Subsection 2.6) is complete. 23 Proof. (i) Any Boolean sum is realized by a network of binary additions; after R7.5, these additions are in ripple form (cf. Lemmas 23 and 24). (ii) Mod 2, the ripple realizes a Xor parity. (iii) Mod 3or 5, the local reduction of the conditional increment is exactly G2/G3 (binary register + fold-back at p ). (iv) The MUX/comparators do not create new linearity; they select branches determined by constants or a threshold. Hence the stated factorization. Theorem 9 (Constructive linear completion).After R1–R7, any implicit linear aggregate S = Paixi is detected and factorized into an anchored network (XOR mod 2, mod-3/5 counters, equalities) of span ≤ 1,and any local additive automaton σt+1 = σt + xt ( modq )encoded by a Boolean network (AND/OR/equality gates) is detected without guessing q and canonized into R8bin q, with bounded compatibility Tq,K(b). All in time O(poly(n, m)). Theorem 10 (Normalization completeness).After exhausting R1–R7, any Boolean CNF subformula that encodes a linear constraint over bits is equi-satisfiable to a network from the canonical library (Xor/mod-3/mod-5/Eq) with span ≤ 1and constant thresholds; otherwise it is absorbed by the scalar corridor. Outline. (i) R2/R6 enforce anchoring and reduce linear supports to span ≤ 1; R7 merges eq-clones. (ii) R7.5 gating (Lemma 25) yields unique external injection and constant-threshold comparators; by Lemma 22, the only bijective cell is ripple with optional fold-back, i.e., additive automata. (iii) Consequently, linear constraints factor through Xor/G2/G3/Eq. Any residual clause not matching these signatures is scalar; by Lemma 29, it is either guarded (R3) or becomes a local head handled in the corridor. Termination of normalization follows from the measure drop (Lemma 11). Algorithm (detection and instantiation without guessing q). 1. Canonical graph G : nodes = variables (primary/aux), edges = XOR/eq/cmp(3/5)/canonical gates (after R1–R7). Mark the anchor (R2/R6) and restrict to the linear subgraph. 2. Aggregate extraction: connected components C consisting only of XOR/eq/cmp(3/5) ⇒ topological order of inputs {xt}, width K. 3. Additive automaton detection: in each C , scan the sequential subnetworks ( Ut→Ut+1 )where Ut is a state register (binary) and the local logic is a deterministic update conditioned by xt . Check locally (bounded sizes) the two cases xt = 0 / 1to establish σt+1 = σt or σt+1 = σt + 1 and thus read the state cycle: its length gives qstructurally. 4. Canonization: replace the detected subnetwork by R8 bin q anchored at the same Tk ; fix the table Tq,K (b); log [ID aggregate, q, K, transitions]. Proof. R2/R6 enforce unique anchoring and span ≤ 1. The aggregates are the CCs of XOR/eq/cmp(3/5). The gates are local with bounded size, hence the reading of the rule σt+1 = σt + xt by local exhaustive test and the reading of the cycle (thus q ). Substitution by R8 bin q preserves the anchor and the span. The complexity is linear in the subgraph size; overall O(poly(n, m)). 4.2 Small-prime completeness {2,3,5} Proposition 10 (SPC( { 2 , 3 , 5 } ) bifurcation de décision).For each terminal uK,b of an R8 bin q aggregate: 1. if Tq,K ( b )is not saturated, then ( r2, r3, r5 ) /∈ Tq,K ( b )entails a multi-mod conflict { 2 , 3 , 5 } (cf. Theorem 3); 24 2. if Tq,K ( b )is saturated for all active terminals, the aggregates satisfy independently (Lemma 30) and any residual UNSAT falls into the scalar remainder where Theorem 7 derives an empty clause. Lemma 44 (Detection fallback without regression).If ReadQ( C )returns None, then no R8 is instantiated on C , the state remains in the scalar corridor (UP/R β –BinClose/triplet), and the extended measure M(Definition 2.5) does not degrade outside Canon (Lemma 19). Corollary 6 (System SPC by aggregates + scalar).Under Lemmas 28 and 30 and Definition 2.15: local SPC (per aggregate) + independence of supports + controlled fall into the scalar (Theorem 7) imply system-level SPC, in the sense of Theorem 11. Theorem 11 (SPC( { 2 , 3 , 5 } ) after R1–R7 + R8 bin q (bounded)).Let b F be normalized as in Theorem 9 and R8 bin q be instantiated with the bounded compatibility Tq,K ( b ). Any linear contradiction triggers, in poly time, (i) a Boolean conflict (exactly-one within the same aggregate), or (ii) a multi-mod conflict via { 2 , 3 , 5 } when the triplet ( r2, r3, r5 )produced by the counters exits Tq,K ( b ). The ledger (aggregate IDs, q,K, transitions, table Tq,K(b)) is polynomial. Proof (stratified, CRT and scalar elements made explicit). (1) Partition & disjoint supports. After normalization R1–R7, the linear forest decomposes into anchored, disjoint aggregates and the rest is scalar. Formally, Lemma 28 gives the connected-component decomposition of the canonical graph Glin (disjoint supports). (2) Crossing clauses ⇒ guard or local head. Any scalar clause mixing two aggregates is either guarded (R3), or produces in O (1) a local ( binary/triplet) head anchored by Lemma 29. Thus, reasoning per aggregate loses no contradiction: interactions are either neutralized or localized as heads. (3) Non-saturated case (CRT). Consider an aggregate whose terminal uK,b is active. If the actually computed triplet ( r2, r3, r5 ) /∈ Tq,K ( b ), the terminal clause is falsified by bounded CRT-30 soundness/completeness, cf. Theorem 3: a multi-mod conflict {2,3,5}follows. (4) Saturated case (all active tables saturated). If, for each active aggregate, the table Tq,K ( b )is saturated (at most 30 /d residues with d = gcd ( q, 30)), Lemma 30 ensures that aggregates are satisfied independently (via the choice of some m∈ [0 ..K ]in the progression) without creating coupling through G1/G2/G3; any residual UNSAT then manifests necessarily in the scalar remainder. (5) Controlled scalar fall (no free resolution). On the anchored scalar remainder (span ≤ 1), Theorem 7 provides a finite sequence in the allowed corridor (BinClose+UP, injective triplet) deriving an empty clause. Each step achieves ∆M ≤ −1and ∆˜τΦ?≤ −1. (6) Conclusion. In all cases, if b F is UNSAT, the dynamics produces in polynomial time either: (i) a Boolean conflict (contradictory unit/empty clause, or exactly-one violated within an aggregate), or (ii) a multi-mod conflict { 2 , 3 , 5 } when ( r2, r3, r5 ) /∈ Tq,K ( b ). Termination bounds follow from (L2) and polynomial verification costs. Remark 5 (Sufficiency of { 2 , 3 , 5 } ).If no contradiction is detected mod 2 , 3 , 5and, moreover, all active tables Tq,K ( b )are saturated, any possible UNSAT is necessarily scalar (Theorem 6); there is thus no need to invoke a p > 5in this framework. Example 2 ( q = 7, K = 30).Two constraints S≡ 0 ( mod 7) and S≡ 30 ( mod 7) force two terminals u30,0 and u30,2 ; the exact-one P29 r=0 Vr = 1 explodes (Boolean conflict). The diagnosis is purely structural by Definition 2.17. Example 3 ( q = 10 (d=10), K≥ 3 · 30 /d = 9).Here d = gcd (10 , 30) = 10, hence |Tq,K ( b ) | ≤ 30 / 10 = 3. For sufficiently large K , the table is saturated: no multi-mod conflict can come from Definition 2.16 and Definition 2.17. Any UNSAT (if it persists) then falls into the scalar remainder. 25 Proof. By Lemma 7, every effective step satisfies ∆ M≤− 1. By (L2), every valid operation has ∆Φ ?≤ − 1 /γmax in raw units and ∆ ˜τ Φ ?≤ − 1in normalized time ˜τ = γmaxτ . Choose any ε≤1/γmax. For an effective step, ∆Λ = ∆Φ?+ε∆M ≤ − 1 γmax −ε≤ − 1 γmax . Dividing by ∆ ˜τ≥ 1(since ∆ ˜τ = γmax/g ( ρ ) ≥ 1) yields ∆ ˜τ Λ ≤ − 1. Skips (no state change) are not counted as episodes. Thus the descent bound and the episode budget do not depend on the scheduler. 7 Theorems (T1–T3) T1 (SAT completeness) unconditional Theorem 15 (T1).If F is satisfiable, then by Lemma 42 and (L2), the dynamics reaches a window where the local readout stabilizes; R β –BinClose+UP complete the assignment in O ( m ) and provide a deterministic witness. Proof sketch. By (L1), no active part is starved; by (L2), Φ ? strictly decreases at each episode in τ . Lemma 42 guarantees that an active stratum always yields a local operation or, via the interface, at the next step. It follows that after at most Φ ? init/ (1 /g ( ρmax )) episodes (in units of τ ), a window is reached where the readout is stable; R β –BinClose+UP then finish the assignment, verifiable in O(m). T2 (UNSAT ⇒certificate) unconditional Theorem 16 (T2).If F is unsatisfiable, then in polynomial time the dynamics produces either (i) a basic Boolean conflict (contradictory unit or empty clause), or (ii) a linear conflict 0=1 for at least one p∈ { 2 , 3 , 5 } . In case (ii), the Gaussian trace (sequence of linear combinations) and the deterministic reconstruction F 7→ Xpform a certificate verifiable in O(n3). Proof. By (L2), at each episode the total linear defect Ppdefectp or the sum of clause sizes decreases. The defect cannot decrease indefinitely without either saturating rank (then forcing substitutions/UP), or exposing a row 0=1. Since Φ ? init ≤poly and each drop is ≥ 1 /γmax , the number of episodes is poly . Verification redoes: (a) gadget detection F 7→ Xp , (b) the certified Gauss leading to 0 = 1. T3 (polynomial bound) unconditional Theorem 17 (T3).With g (0) = 1, we have Φ ? init ≤ (2+ κ4 ) m +3 n . By (L2), ∆ ˜τ Φ ?≤ − 1, hence the number of episodes in ˜τ is ≤ Φ ? init = poly ( m, n ). Since ˜τ = γmaxτ with γmax ≤ (1 + m + n ) α , this unit change does not affect polynomiality. Each operation has polynomial cost (Gauss mod p in O(n3)per block), therefore the total time is polynomial. Proof. (L2) gives ∆ ˜τ Φ ?≤ − 1; thus Φ ? drops from Φ ? init to 0within ≤ Φ ? init units of τ . (L1) gives a minimal step ∆ τmin = Ω(1 /poly )per pack; the total in ticks t is therefore poly . Per-episode cost is bounded by Gauss O(n3); the rest is linear in the local size. 8 Deterministic algorithm (pseudocode) and complexity Terminology. An episode is an effective operation that changes the state (UP, accepted pivot, successful R β –BinClose, triplet, etc.). An attempt is a candidate check that may be rejected without changing the state (e.g., a dependent row under LinClose+(p)). 32 Inputs→Outputs discipline (section) Taken. Fixed order T,g,Φ?,P={2,3,5}, detection rules, priority, tie-break. Derived. Trajectory s0→s1→ · · · , SAT witness or UNSAT certificate, verifiable ledger. Algorithm 6 Det-3Sat-R1(F) 1: Build Tonce (SCC + BFS); initialize state s← F; ledger L ← ∅. 2: while true do 3: In the minimal active layer Tk, compute all valid operations and their ∆Φ?. 4: if no valid operation exists then 5: if all clauses satisfied then return SAT-witness sand L 6: end if 7: promote focus from Tkto Tk+1; recompute valid operations and priorities 8: continue 9: end if 10: Pick operation with priority (UP > LinClose + ( p ) > R β –BinClose > triplet), then tie-break lexicographically. 11: If the chosen operation is LinClose+(p), run the incremental pivot test; 12: apply only if independent or 0 = 1;skip otherwise (no ∆Φ?consumption). 13: Apply operation, update s, update ρand Φ?locally, append step to ledger L. 14: if a clause becomes empty or a row 0 = 1 mod p appears then return UNSAT-cert (Boolean or mod p) + L 15: end if 16: end while Proposition 12 (Link τ↔ wallclock time: per-operation costs).Let N := |F| be the input size and n, m as in the text. (a) Local evaluation of the gains ∆Φ ? and of eligibility is O ( deglocal ) per candidate head. (b) Linear detection (scan of XOR/mod 3/5/equality templates) is O ( m ) per pass (Proposition 2). (c) Gauss mod p on a block of size ≤n is O ( n3 )per epoch, with a strict bound on skips (Rule 2.1,Proposition 1). (d) R β –BinClose (SCC + local UP) is O ( |F(2)| ) (Proposition 6). (e) R8bin q: overhead O(Klog q)for width K(Lemma 13 and Corollary 2). By (L2) we have ∆ ˜τ Φ ?≤ − 1, hence #episodes ≤ Φ ? init = poly (Thm. T3). Since each episode costs only one of items (a)–(e), each in poly(N), the total time is poly(N). Clone bound and passes Lemma 49 (Amortized clone bound for R2/R6).Let F have size ( n, m ). After R1, the total number of anchor clones introduced by R2 and the R6 splits is bounded by O ( m )and the number of passes per layer is O (1). In particular, the final (variable/clause) size of NormR1–R7 ( F )is O(m). Proof. R1 adds PC ( |C| − 3) +≤O ( m )variables/clauses. Each R2 clone consumes a nonconforming interface; R6 strictly decreases the span (counter non-anchored supports of M ). Since ∆M ≤ −1at each application, the total is ≤ M(F0) = O(m). Lemma 50 (Total cost with R8 bin q ).If we instantiate R8 bin q` on L aggregates of widths K` , the additional overhead is PL `=1 O ( K`log q` ). Under Lemma 49, the final size remains polynomial in (n, m)and in the binary size of the modules q`. Lemma 51 (Local confluence under ∆Φ ? -priority).Let two valid operations opA,opB be simultaneously eligible in the same episode. If both strictly decrease Φ ? , then applying them in either order produces states sAB, sBA such that Φ ? ( sAB ) = Φ ? ( sBA )and both states remain within the 33 same partition class of Lemma 4. In particular, the global bound on the number of episodes and the termination proofs (L2,T3) are schedule-independent. Theorem 18 (Global soundness no spurious UNSAT).Every transformation invoked by the pipeline (R0–R7, R8 bin q , UP, R β –BinClose, injective triplet, bounded CRT terminals, and PTT-Cut/min-cut) preserves satisfiability. The only ways to derive UNSAT are: (i) a Boolean contradiction (empty clause / contradictory unit), (ii) a linear contradiction 0 = 1 over some p∈ { 2 , 3 , 5 } , (iii) a falsified bounded CRT terminal under an asserted uK,b = 1. Consequently, if Fis satisfiable, no step of the pipeline can produce a spurious contradiction. Proof sketch. R0–R7 are equi-SAT by their local lemmas; R8 bin q is equi-SAT (Prop. 7); UP/R β –BinClose/triplet sont des extensions/propagations Tseitin; les terminaux CRT najoutent aucune solution et ne retirent quen présence de uK,b = 1 incohérent (Thm. 3); PTT-Cut/min-cut ne falsifie quen cas de fenêtre vide (Thm. 13, Lem. 47). 9 Certificates and verifiability 9.1 SAT witness The trace L allows replaying UP/R β –BinClose and linear substitutions (back-subst) to reconstruct s?. Verification in O(m). 9.2 Linear certificate mod p Minimal content: (i) identified templates ⇒ matrix Xp and vector b (hash of clause IDs), (ii) pivots and Gaussian combinations leading to 0 = 1. Verification: reconstruct Xp from F , replay Gauss and check the contradictory row. Cost O(n3). 9.3 Deterministic 3-pass verifier Input. Ledger L containing: order T , the sequence of rewrites R1–R7 (IDs), modules R8 bin q with ( q, K ), hashed transitions, terminal constraints and tables Tq,K ( b ), plus the extract of the mod 2/3/5 gadgets used. Output. SAT-witness or UNSAT-cert (Boolean or multi-mod). Algorithm 7 Verify-PTT (3 passes) 1: Pass 1 (R0 + R1–R7.5): replay R0 (Theorem 1) then R1–R7.5; check Canon and anchors. 2: Pass 2 (LinClose+/ Gauss / CRT / PTT-Hall): 3: (Pass 2 pre-check): verify aggregate-scoped selectors (Def. 2.18); reject any name collision across `. 4: Check that each invocation of R β –BinClose references the anchored binary projection (Def. 2.13). 1. Linear blocks: rebuild Xp(p∈ {2,3,5}) and replay Gauss (pivots/rejections). 2. R8bin qaggregates: simulate the registers, verify the tables Tq,K (b)(CRT-30). 3. Cuts: run Verify-PTT-Hall (Algorithm 4) and test terminal falsification. 5: Pass 3 (Decision): empty clause/contradictory unit ⇒ Boolean-UNSAT; falsified CRT ⇒ multi-mod-UNSAT; otherwise SAT-witness. Proposition 13 (Costs and replayability).Each pass is O ( poly ( |F| )); Gauss per block O ( n3 ), R8 bin q simulation O ( Klog q ), cuts O ( poly )(local min-cut included). The ledgers (Definition 2.4, Definition 5.5,Definition 5.7,Certificate 9.1) suffice for replayability. 34 Complexity. Each pass is O ( poly ( |F| )); in particular Pass 2 is O ( Klog q )per aggregate (Lemma 13), and log q=O(|F|)(Lemma 15). Certificate 9.1 (Linear certificate mod p MANDATORY pivots and rejections).An UNSAT certificate mod p must contain: (i) the extracted matrix Xp (clause IDs), (ii) the ordered list of accepted pivots, (iii) the list of rejected rows (never retested, Rule 2.1). The verifier (cost O ( n3 )) replays Gauss, checks each rejection and the 0 = 1 row. 10 Mod 3 obstruction & multi-mod resolution (R1) 10.1 CNF family mod 3 incompatible, mod 2 compatible Consider Boolean variables x1, . . . , xkand impose simultaneously: (A) k X i=1 xi≡1 (mod 3), (B) 2 k X i=1 xi≡0 (mod 3). Over Z/ 3 Z , (B) implies Pxi≡ 0, which contradicts (A); unsatisfiable. Reducing mod 2: (B) becomes 0 ≡ 0(trivial) and (A) becomes an odd parity perfectly satisfiable. Thus mod-2closure alone does not detect the refutation, motivating the addition of p = 3. Both constraints are realizable in CNF via a modulo-3 (resp. modulo-2) counter of size O ( k ); our R1 detection isolates them and forms X3. Gaussian elimination over F(3) derives 0 = 1 immediately (certificate). 10.2 Why {2,3,5}suffices (Occam) The triplet { 2 , 3 , 5 } is small, fixed, and already captures weak obstructions to even/odd parities, ternary sums, and a pentamodal cycle typical of addition encodings. Extending P would burden detection with no demonstrated benefit here; the bound ρ≤m + 3 keeps g under polynomial control. 35 11 Reproducibility The ledger L contains: (i) order T , (iv) for mod p , the pair ( Xp,Gaussian trace )including the list of accepted pivots and of rejected rows (dependent) by LinClose+ ( p ). A verification script replays Land outputs either the witness or the certificate. All costs are poly(n, m). Theorem 19 (Global complexity summary).After normalization R1R7, the size NormR1–R7 ( F )  is poly ( |F| )(Lemma 49 and Proposition 5). The total overhead due to R8 bin q modules is P`O ( K`log q` )with log q = O ( |F| )(Lemmas 13 to 15 and Corollary 2). The number of episodes satisfies #episodes ≤Φ? init ·(1 + m+n)α= poly (Equation (1), (L2), Thm. T3), and the per-episode cost is polynomial (Proposition 12). Therefore the total time is polynomial in |F| . By Lemma 48, the same episode bound holds with Λin place of Φ ? , which makes the episode count schedulerindependent. Corollary 7 (Explicit bound on the number of episodes).With Φ ? init ≤ (2 + κ4 ) m + 3 n and γmax ≤(1 + m+n)α, the number of effective episodes is at most #episodes ≤(2 + κ4)m+ 3n·(1 + m+n)α. Selectors and counters are aggregate-scoped per Def. 2.18 (the verifier rejects name collisions). 12 Conclusion We established (L1) and (L2) in a strictly discrete and deterministic corridor, proved a confluence lemma for R1–R7, and made the episode bound scheduler-independent via the Combined Lyapunov Λ(Lemma 48), together with an unconditional T2. Local normalization R1–R7.5 (unique injection, constant threshold) yields local classification (ripple), the structural read of q , and the complete normalization of linear constraints (XOR/counters/equalities). With R8 bin q , the SPC bifurcation (non-saturated vs saturated) provides either a multi-mod conflict { 2 , 3 , 5 } , or the scalar empty clause, and the algorithm decides any 3sat instance in polynomial time with a verifiable certificate. Corollary 8 (P=NP).By deterministic normalization R1–R7 and instantiation of R8 bin q (Theorem 9,11), any 3sat instance is decided in polynomial time with witness/certificate: •SAT ⇒witness produced (T1). •UNSAT ⇒Boolean conflict or 0 = 1 mod pwith p∈ {2,3,5}(T2). The global bound is polynomial (T3). Since 3sat is NP-complete, it follows that P=NP. Complexity budget. The only globally fixed constants/functions are α (fixed a priori), P={2,3,5}, and the tie-break order. No data-driven tuning is involved. Executable summary (checklist). •Build T(SCC+BFS). •Fix αand g(ρ) = (1 + ρ)α. •Initialize Φ?(reducible heads, linear defects mod p). • Loop: in the minimal layer Tk with a defect, apply the priority operation maximizing ∆Φ ? . •If Boolean conflict or 0 = 1 mod p, exit with certificate (T2). 36 •Else, if no more operation is available and all clauses are satisfied, exit with witness (T1). •Else, apply interface escalation (Lemma 42) and continue selection. References [1] G. S. Tseitin, On the complexity of derivations in propositional calculus, in: Studies in Constructive Mathematics and Mathematical Logic, Part II, (1968). (English translation in: J. Siekmann and G. Wrightson (eds.), Automation of Reasoning, Vol. 2, Springer, 1983.) [2] S. A. Cook, The complexity of theorem-proving procedures, Proc. STOC 1971, 151–158. [3] C. H. Papadimitriou, Computational Complexity, AddisonWesley, 1994. [4] A. Biere, M. Heule, H. van Maaren, T. Walsh (eds.), Handbook of Satisfiability, IOS Press, 2009. [5] R. E. Tarjan, Depth-first search and linear graph algorithms, SIAM J. Comput. 1(2):146–160, 1972. [6] T. H. Cormen, C. E. Leiserson, R. L. Rivest, C. Stein, Introduction to Algorithms, 3rd ed., MIT Press, 2009. [7] G. H. Golub, C. F. Van Loan, Matrix Computations, 4th ed., Johns Hopkins University Press, 2013. [8] F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press, 1998. [9] K. Ireland, M. Rosen, A Classical Introduction to Modern Number Theory, 2nd ed., Springer, 1990. [10] E. Ben-Sasson, A. Wigderson, Short proofs are narrowResolution made simple, J. ACM 48(2):149–169, 2001. 37 A Table of rules R1–R7 Rule Local action (scheme) Equi-SAT Guaranteed drop of M R1 q≥4:(`1∨· · ·∨`q)7→ 3-CNF chain with yianchored at Tk Tseitin 3CNF via R3/R6 (selection) R2 Anchor clone v(k)+(v↔v(k))equivalences ↓#Supplin6anc R3 ( A∨B ) 7→ ( A∨gk ) ∧ ( B∨ ¬gk )with gk anchored at Tk Tseitin ↓#Intneutre R4 Odd chordless cycle ⇒ anchored XOR gadget (G1) standard ↓#Supplin6anc R5 Triadic motif ⇒ anchored mod 3/5 counter (G2/G3) standard ↓#Supplin6anc R6 Linear span ≥ 2 ⇒ eq-clone splits down to span ≤1 via R2 ↓#Supplin6anc R7 Canonicalization of clones/equalities trivial contraction, residual ↓ Rewrite ledger and auditability. Each step logs: (i) IDs of touched clauses, (ii) variable/clone mapping ( v↔v(k) ), (iii) gadget ID (XOR/mod 3/5) and anchor position Tk , (iv) measure deltas (∆M,∆|Cl|,∆|Var|). Verification replays in O(poly(n, m)). R8 bin q ledger (minimal elements). For each aggregate: (ID, anchor Tk ), width K , modulus q (read by cycle detection), ordered list of transitions (hash), terminal constraint s K =b, table Tq,K (b)(list of allowed r), IDs of the mod 2/3/5 counters used for (r2, r3, r5). B Adversarial traces Family 1 (30 vs q ). S = P30 i=1 xi ,( A ) S≡ 0 ( modq ),( B ) S≡ 30 ( modq ). Steps: (i) aggregate detection; (ii) R8 bin q :30 transitions (binary register) ut+1,•⇔ ( ut,•, xt ); (iii) units u30,0 = 1, u30,c = 1 ( c = 30 mod q ) ⇒ exactly-one conflict. Deltas: ∆ M = − 1,∆ |Cl| = O(30 ·log q)(i.e. O(log q)), ∆|Var|=O(31 ·log q)(i.e. O(log q)). Family 2 (CRT compatibility). S≡b ( modq )and S≡r? ( mod 30) with ( r?mod 2 , 3 , 5) /∈ Tq ( b ). Steps: R8 bin q + G1–G3 ⇒uK,b = 1, Vr? = 1; the final clause uK,b ⇒Wr∈Rq,K (b)Vr is falsified ⇒multi-mod conflict {2,3,5}. C Pair or implicative cycle Lemma 52 (Pair or implicative cycle under span ≤ 1).Let Fscal be an anchored (span ≤ 1) 3-CNF, without units and without incident binaries (handled by R β –BinClose). Then, in the corridor (UP, R β –BinClose, triplet), we obtain in polynomial time: (a) either two clauses sharing ( a∨b )(factorizable pair) ⇒ triplet ⇒ incident binary; apply R β –BinClose (then UP), (b) or a signed cycle u ¬u in the alternating graph literals ↔ pairs, and a single triplet factorization on one edge suffices to create an incident binary;R β –BinClose+UP unwind to the empty clause. At each step, ∆M ≤ −1and ∆˜τΦ?≤ −1. Proof. Construction of the alternating graph, degree analysis (min-degree ≥ 2), alternative repeated pair vs signed cycle as in the proof of Theorem 7. In (a), the triplet y↔ ( a∨b )creates an incident binary (handled by R β –BinClose); in (b), a single triplet on an edge of the cycle 38 suffices to engage UP towards y∧ ¬y . Each step is local, respects span, and decreases the measure; see (L2) for the link ∆τΦ?. D Canonical Tseitin library All variables below are Boolean. Equalities y↔φare encoded in CNF by definitional clauses. Eq (equality): y↔x.(¬y∨x)∧(y∨ ¬x). Not: y↔ ¬x.(¬y∨ ¬x)∧(y∨x). And: y↔(a∧b).(¬y∨a)∧(¬y∨b)∧(y∨ ¬a∨ ¬b). Or: y↔(a∨b).(y∨ ¬a)∧(y∨ ¬b)∧(¬y∨a∨b). Xor: y↔(a⊕b).(y∨a∨b)∧(y∨ ¬a∨ ¬b)∧(¬y∨a∨ ¬b)∧(¬y∨ ¬a∨b). Mux: y↔(c?b:a).(¬c∨ ¬a∨y)∧(¬c∨a∨ ¬y)∧(c∨ ¬b∨y)∧(c∨b∨ ¬y). Ripple addition (bit i): s0 i↔(si⊕ci−1),ci↔(si∧ci−1).Xor +And above. Ripple subtraction (difference di, borrow bi). b−1:= geq. For each i: di↔s0 i⊕qi⊕bi−1, bi↔(¬s0 i∧(qi∨bi−1)) ∨(qi∧bi−1). (The disjunction is encoded with an auxiliary variable and And/Or.) Cmp ≥q (lexicographic). Constants ( qb−1, . . . , q0 ) ∈ { 0 , 1 }b . Auxiliary variables eqi,gti (i=b, . . . , 0), with eqb:= 1 (unit) and gtb:= 0. For i=b−1, . . . , 0: eqi↔eqi+1 ∧(si↔qi), ti↔si∧ ¬qi,gti↔gti+1 ∨(eqi+1 ∧ti). Output geq ↔gt0∨eq0. Sum3 counter and comparator ≥ 1(canonical) Two state bits ( a0, a1 )encode fC∈ { 0 , 1 , 2 , 3 } ; ripple update (2 bits) while reading `1, `2, `3 .Cmp ≥1 : binary lexicographic ( a1a0 )vs 01 (reference rails via Eq). All reference rails are wired through Eq ∈Canon ; span ≤ 1, anchor preserved. Card-AT-MOST-ONE over {z1, . . . , zk}.For all 1≤a < b ≤k, binary clause (¬za∨ ¬zb). Card-EXACT-ONE (recall). AT-MOST-ONE + comparator Cmp ≥1 (or standard 3-CNF chain) on {zi}. Occupation bit t↔ ( z1∨ · · ·∨zk ).( ¬t∨z1∨ · · ·∨zk ) ∧Vi ( t∨¬zi ). Under AT-MOST-ONE, we get t=Pizi(Boolean equality). 39 E Exhibits (ledger & replayability) (i) Local PHP 32 (non-trivial cut) already in your text Subsection 5.3. Minimal ledger below: Certificate E.1 (Ledger Local PHP cut 3 → 2). S = ta + tb ; K = 2; demands L = 3 (3 Row-EXACT lines); capacities U = 2 (Col-AT-MOST-ONE on {a, b} ). Terminal: u2,3 ; Attached table Tq,2 (3) (CRT-30) (hash= h_TqK_2_3 ). Conclusion: terminal clause falsified ⇒ multi-mod UNSAT. (ii) Two required tasks, one resource (non-PHP local cut) already Certificate E.2. Ledger: Certificate E.2 (Ledger Two tasks, one resource). S := uC1 + uC2 (or x1r + x2r ), K = 2; L = 2 (Row-EXACT), U = 1 (AT-MOST-ONE resource). Terminal u2,2 ; attached table Tq,2 (2) (hash=h_TqK_2_2). Immediate falsification. (iii) No-linear instance captured by PTT-Cut Build a small sub-schedule: three jobs A, B, C must all start (AT-LEAST-ONE per job), but only one slot r is available and A, B are mutually exclusive with C (schema: A or B and C required). Local 3-CNF: (a)EXACT-ONE (b)EXACT-ONE (c)EXACT-ONE (ňaňc)(ňbňc)AT-MOST-ONE on the unique resource r where the EXACT-ONE are encoded à la Card-EXACT (R0 provides the uC ). Choose the unique resource r with tr↔ ( a∨b∨c )+ AT-MOST-ONE ⇒tr∈ { 0 , 1 } . PTT-Cut takes S := ua + ub + uc (or a + b + c ), K = 3, L = 3 (jobs required) and U = 1 (resource capacity). Ledger: (iv) Pure scalar instance that goes to the corridor Consider the following 3-CNF (no linear gadgets nor capturable packs: no explicit ATMOST/EXACT, hence (A) and (B) fail): Fscal = (a∨b∨c)∧(¬a∨d∨e)∧(¬b∨ ¬d∨f)∧(¬f∨ ¬c∨ ¬e). It is UNSAT (alternating cycle a ¬a in Galt ). Corridor script: apply a single triplet factorization on the pair ( d, e )in ( ¬a∨d∨e ): introduce y↔ ( d∨e ), replace ( ¬a∨d∨e )by ( ¬a∨y ), then peel ( ¬a∨y )(degree ≤ 2of y ). UP propagates along the cycle up to forcing a∧ ¬a⇒empty clause. Minimal ledger: Certificate E.3 (Ledger Scalar remainder, corridor ⇒ empty clause).Triplet applied on ( d, e ): add y↔ ( d∨e ), replace ( ¬a∨d∨e )by ( ¬a∨y ),R β –BinClose on the local binary projection (then UP)⇒aand ¬a. Deltas: ∆M ≤ −1at each step. 40