# Theory of Reality — Verified Relation Reuse RE SAT structure laboratory, revision 0.3 · 5 September 2026 This release reduces the cost of checking the engine's answers. It preserves the earlier solver, learned policy, experiments, and full reference checker. On 34 fresh synthetic cases, all decisions passed both the new checker and the reference path. The ratio of summed per-case median **solving-plus-checking** times was 2.777, using an initially empty verifier cache on every timed call. This result is specific to the supplied suite and environment. The mathematical contribution of this note is an explicit soundness argument for the implemented transformation and reuse rule. No novelty, proof-assistant certification, general SAT complexity result, or physical dimensional discovery is claimed. ## 1. The representation refinement Let a group of clauses use exactly the same ordered set of distinct variables \[ S=(v_0,\ldots,v_{k-1}). \] The input is first normalized: duplicate literals and clauses are removed, tautological clauses are discarded, and every clause in the group must contain every variable in its scope exactly once. Define the local projection of a global assignment by \[ \rho_S(x)=(x_{v_0},\ldots,x_{v_{k-1}})\in\{0,1\}^k. \] **Lemma 1 — One forbidden pattern per full-scope clause.** For a clause \(C\), let \[ b_j(C)=\begin{cases}0&x_{v_j}\text{ occurs positively},\\1&x_{v_j}\text{ occurs negatively}.\end{cases} \] Then \[ C(x)=0\iff \rho_S(x)=b(C). \] **Proof.** An OR clause is false exactly when every literal is false. A positive literal is false at zero; a negative literal is false at one. Each scope variable occurs once, so these conditions specify precisely one local assignment. This also covers an empty clause: the zero-dimensional cube has one assignment and the empty clause forbids it. ∎ For a group \(G\), put \(B_G=\{b(C):C\in G\}\). Consequently, \[ \boxed{G(x)=1\iff\rho_S(x)\notin B_G.} \] This changes how the relation is evaluated without changing its satisfying assignments. It replaces repeated interpretation of all literals at every local point with construction of the forbidden patterns followed by membership checks. ## 2. Exactly what the cache certifies Write the claimed local affine equations over \(\mathbb F_2\) as \(Au=b\), and let \(e\) be a Boolean exactness flag. The cached proposition is keyed by the immutable tuple \[ K=(k,\operatorname{sort}(B_G),\operatorname{sort}(A,b),e). \] The independent checker examines all \(2^k\) local assignments and establishes \[ \forall u,\quad u\notin B_G\Longrightarrow Au=b, \] and, if \(e\) is true, \[ \forall u,\quad u\notin B_G\Longleftrightarrow Au=b. \] Only then is the key stored. A false exactness flag permits a partial affine consequence; the original nonlinear clauses remain binding. **Theorem 2 — Sound reuse under local renaming.** A successful check for key \(K\) remains valid for any later group with the identical recomputed key, irrespective of its global variable names. **Proof.** The key fixes the entire local relation and the entire claimed local proposition. Renaming only changes the coordinate restriction \(\rho_S\). Substituting \(u=\rho_S(x)\) into the universally checked implication or equivalence gives the corresponding statement for every global assignment. ∎ The implementation recomputes the key from the current clauses and equations. It does not trust a solver-supplied relation name, digest, or `verified` flag. Equation masks, right-hand sides, and exactness are all included, so changing a claim cannot inherit the old check. Python tuple equality, rather than hash equality alone, determines cache identity. The cache holds at most 4,096 accepted propositions and evicts the least recently used entry when full. Eviction affects performance only: a missing proposition must be checked again. No cache file is loaded or serialized. The certificate threat model assumes the checker process and its code are trusted; arbitrary mutation of its private memory is outside that model. ## 3. Local reuse does not replace the global proof Every call still validates: 1. The certificate describes the requested normalized CNF. 2. Groups partition its clauses exactly, with valid scopes and equation masks. 3. An asserted inconsistency has an explicit XOR combination yielding \(0=1\); or the asserted affine map is complete. 4. The final SAT/UNSAT answer agrees with the evidence, and a claimed SAT witness satisfies the original clauses. 5. Any reported model count is covered by the checked evidence. For the consistent case, let the complete equation system be \(Hx=h\), of independently computed rank \(r\). The certificate supplies a point \(p\) and basis columns \(N\). The checker establishes \[ Hp=h,\qquad HN=0,\qquad \operatorname{rank}N=n-r. \] **Theorem 3 — Complete affine coordinates.** Under these checks, \[ \{x:Hx=h\}=\{p+Nz:z\in\mathbb F_2^{n-r}\}, \] and every solution occurs once. **Proof.** The independent columns of \(N\) lie in the kernel of \(H\) and have its dimension, so they form a kernel basis. Translating this kernel by a valid point gives all solutions. Independence makes the free-coordinate parameterization injective. ∎ If all groups are exact affine relations, the model count is therefore \(2^{n-r}\). If nonlinear groups remain, the map restricts the candidates but does not establish that every candidate satisfies those groups. The new `verify_decision.py` closes that earlier reporting limitation. For a mixed residual UNSAT claim or an attached count, it enumerates the free coordinates, reconstructs each assignment, and checks the **whole original CNF**, without using the solver's residual tables or elimination order. This is allowed only with at most 16 free bits and the declared conservative work estimate at most 10,000,000. Above that budget the result is unverified, not established. A SAT claim without a count can instead be established by its directly checked witness. DPLL decisions retain the earlier independent witness/tree checker. A SAT witness alone is not accepted as a counting certificate. ## 4. Cost and the geometric-action analogy The supplied figure distinguishes an action sequence from a shorter equivalent action, and warns that a shadow may discard information. The corresponding rule here is equality of Boolean semantics for every supported local input. Visual agreement on sampled points would be insufficient. For a group of \(m\) full-scope clauses and width \(k\), direct local clause evaluation has a worst-case literal-evaluation cost proportional to \(2^k m k\). Constructing its forbidden patterns costs \(O(mk)\) elementary bit visits before sorting. Checking \(q\) affine equations at every local point uses \(O(2^k(q+1))\) bounded-width operations. The actual implementation also performs canonicalization, sorting, and validation. For a sequence of groups, the new total has the form \[ T=\sum_{\text{all groups}}T_{\rm validate+key} +\sum_{\text{cache misses}}T_{\rm exhaustive\ local} +T_{\rm global\ checks}+T_{\rm final\ decision}. \] With no eviction, a repeated key pays the exhaustive local cost once. With eviction, it may pay again. Validation and the global proof are never removed by a cache hit. This expression concerns the bounded local verifier and does not establish polynomial-time general SAT solving. This revision was designed from the earlier timing trace, where checking dominated several graph examples. The solver's previously learned policy and vocabulary were frozen throughout the new experiment. There was no autonomous source-code rewriting or retraining on the evaluation set. ## 5. Fresh experiment and controls The protocol was written before case evaluation. All 34 normalized input hashes differ from those found in the earlier saved input sets. There are 20 graph-parity instances, 12 fresh seeded affine/mixed/ordinary CNFs, and two larger scope-growth examples. Formula generation and expected answers are separate from the solver; it receives only the CNF. Each case has five timed repetitions per mode, in rotated order, after one excluded warm-up per mode. Timings include in-memory solving and complete decision/count verification. They exclude imports, model startup validation, and JSON I/O. Raw component and total times are saved; the median total is computed from total samples, not by adding separate medians. | Mode | Meaning | Sum of 34 per-case median totals | |---|---|---:| | Reference | Frozen solver plus original local checker and new final-answer checks | 605.161 ms | | Normalized, no cache | Forbidden-pattern checker; cache capacity zero | 225.139 ms | | Reuse, cold | New empty verifier cache per call; reuse within the formula | 217.949 ms | | Reuse, warm | Same-case cache primed by the excluded check | 215.585 ms | Thus the reference/cold ratio is **2.7766**, the reference/warm ratio is **2.8071**, and normalization/no-cache divided by cold reuse is **1.0330**. Most improvement comes from the relation representation. The cache adds a modest further improvement on this suite. The aggregate is weighted by case cost: the four complete-graph component examples account for much of the time. It is not a claim that every formula becomes 2.78 times faster. | Family | Cases | Reference median total | Cold-reuse median total | |---|---:|---:|---:| | Affine CNFs | 4 | 1.083 ms | 0.814 ms | | Mixed CNFs | 4 | 2.072 ms | 1.456 ms | | Ordinary CNFs | 4 | 1.338 ms | 1.436 ms | | Cubic rings | 8 | 3.391 ms | 2.435 ms | | Degree-four rings | 8 | 8.119 ms | 4.676 ms | | Complete-graph components | 4 | 109.355 ms | 25.812 ms | | Scope-growth examples | 2 | 4.581 ms | 4.473 ms | Ordinary cases use the unchanged DPLL proof path and show no consistent gain; their aggregate median regressed in this run. Five repetitions on one machine are not a robust cross-platform performance estimate. ### A concrete large exact result For the satisfiable degree-four ring with 128 vertices, the encoded CNF has **256 variables and 1,024 clauses**. The engine and both independent check paths establish \[ r=127,\quad n-r=129,\quad \#F=2^{129}=680564733841876926926749214863536422912. \] The fresh-cache verifier checks 32 local rows, reuses coverage of 2,016 more, and still validates the complete global affine map. Solve-plus-check medians are **31.071 ms** for the reference path and **22.070 ms** for cold reuse. For four disjoint copies of the complete graph on eight vertices, the satisfiable CNF has 112 variables and 2,048 clauses. The model count is \(2^{84}\); medians are **153.766 ms** and **36.932 ms** respectively. These are structured parity problems. For an undirected graph with \(v\) vertices, \(e\) edges, and \(c\) connected components, the edge-incidence equation matrix over \(\mathbb F_2\) has rank \(v-c\). Within each component the sum of vertex rows is zero, giving the upper bound; its spanning-tree columns have rank one less than the component's vertex count, by successive leaf elimination, giving equality. A consistent system therefore has \(2^{e-v+c}\) assignments. A component with odd total right-hand-side parity is inconsistent. Variable permutations and literal flips preserve these counts by a bijection of assignments. This independently supplies the expected graph answers; the engine is not given the graph description. Counting these assignments from a basis does not require visiting them individually. It does not imply comparable treatment of arbitrary nonlinear SAT instances. ## 6. Checks and reproducibility - All **37 test groups** passed, including nine added for this release. - The new tests cover every one of the 256 three-bit relations, global-map completeness, renaming, cache eviction, disabled reuse, attempted cache poisoning, empty formulas/clauses, wrong witnesses/counts, and explicit verification-budget refusal. - All **34 fresh cases** were solved and accepted in all four verification modes. - All **146 corrupted claims** in the saved campaign were rejected after first warming a cache on the corresponding valid decision. - The deployed checked entry point produced the 256-variable example; separate `python3 -I` invocations accepted it with both checkers. - The earlier policy still passes its separate finite-optimum checker. Policy and vocabulary hashes were unchanged. The local verification budget remains 256 declared variables, 20,000 clauses, scope width ten, and conservative local work at most 2,000,000. No larger limits were used to make the benchmark pass. Python 3.12.13 on Linux was used. Startup construction/validation, excluding imports and file I/O, had median 0.457 ms. The separately saved applied CLI run is a correctness demonstration, not an extra sample included in the benchmark; its timing can differ from the controlled medians. Run the checked engine on a PC after installing the existing requirements: ```powershell py -3 checked_engine.py reuse-results/inputs/ring4-128-0.json --output checked-decision.json py -3 -I verify_decision.py checked-decision.json reuse-results/inputs/ring4-128-0.json py -3 -I verify_decision.py checked-decision.json reuse-results/inputs/ring4-128-0.json --reference ``` Run tests with `py -3 -m unittest discover -v`. Run `py -3 reuse_experiment.py` to regenerate this experiment; it overwrites `reuse-results` measurement files. Use `python3` on Linux/macOS. Windows execution has not been independently tested here. See `reuse-results/protocol.json`, `evaluation.json`, `corruption-checks.json`, and the saved inputs/outputs for the complete evidence. The first invocation stopped during input generation because of an indexing error; it was corrected before any case was solved or timed, as recorded in `development-notes.json`. ## 7. What remains open in this engine The now-visible costs include repeated structural validation and complete global-map checking; arbitrary nonlinear residuals remain the deeper algorithmic obstacle. A future change needs another exact semantic argument and a separate cost comparison. Compressing or caching a known relation does not supply a polynomial-time method for every SAT formula. For the formal target, see Stephen Cook's [official P versus NP problem description](https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf). This release establishes neither P = NP nor P ≠ NP. The image's geometric operations and the successful finite computations also do not establish seven-dimensional physics.