# Universes and Proof Bridges

Reality Bit Engine 0.19.0 — 5 September 2026  
Research direction: Anthony Michael Collado

The engine now implements an exact bridge from finite transition systems to
SAT, a checked direction for transferring safety through a state map, and a
conditional algebraic theorem that can close a contracting loop of error
bounds. It also enumerates the eight truth assignments to the three research
targets. **None of the three Millennium problems is solved by this release.**
No assignment has been eliminated by a new arithmetic or analytic theorem.

The distinction is substantive: finite tests can establish a universal result
when a proved completeness bound covers everything the claim quantifies over.
The finite-system theorem below has that bound. Our proposed reductions of
RH, P versus NP, and general fluid regularity do not yet have one.

## 1. Define the cases before connecting them

We work with these classical propositions:

| Atom | Exact intended proposition |
|---|---|
| R | Every nontrivial zero of the Riemann zeta function has real part 1/2. |
| P | P = NP for ordinary deterministic and nondeterministic polynomial-time decision classes. |
| N | At viscosity one, every real, smooth, mean-zero, divergence-free initial velocity on the periodic torus [0,2pi]^3 has a global smooth unforced three-dimensional Navier–Stokes solution. |

N fixes the periodic, unforced research target; its negation is the negation
of that quantified statement, not an arbitrary numerical instability. The
normalization and the mean-zero restriction must be tracked when relating it
to a full official prize formulation. See the official descriptions by
[Bombieri](https://www.claymath.org/wp-content/uploads/2022/05/riemann.pdf),
[Cook](https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf), and
[Fefferman](https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf)
for the corresponding mathematical problem statements.

There are eight propositional cases:

| Case | R | P | N | Unconditional status in this engine |
|---|---|---|---|---|
| 000 | false | false | false | Open |
| 001 | false | false | true | Open |
| 010 | false | true | false | Open |
| 011 | false | true | true | Open |
| 100 | true | false | false | Open |
| 101 | true | false | true | Open |
| 110 | true | true | false | Open |
| 111 | true | true | true | Open |

These rows are hypothetical Boolean assignments. We have not proved that
each row is consistent with arithmetic, that the propositions are mutually
independent, or that actual physical universes instantiate them. Classical
case analysis is valid without making those stronger claims.

Suppose, for example, a common base theory really proves both

\[
P\Rightarrow R,\qquad \neg P\Rightarrow R.
\]

Then excluded middle gives R. Our truth-table checker verifies this
**conditional rule**. It does not prove either premise about arithmetic.
Removing either premise leaves a Boolean counterassignment.

Even assuming all three implications

\[
R\Rightarrow P,\qquad P\Rightarrow N,\qquad N\Rightarrow R
\]

leaves both 000 and 111. Equivalence, if established, would let one resolved
target settle the others. A circular chain alone does not resolve its truth.
Inconsistent premises yield a vacuous propositional consequence; the checker
explicitly marks this and never upgrades it to a prize proof.

The engine screens the 24 directed implications between signed literals of
different atoms. None is a propositional tautology. Each record retains a
counterassignment and an obligation to supply a real bridge theorem. This
screen does **not** disprove those implications as statements of mathematics,
and is not a search through all possible mathematical proofs.

## 2. A quantitative loop that really does close

Here is a rigorous version of the proposed mutually constraining errors.
Let d be a **finite** nonnegative real column vector of length three. Suppose

\[
d\le Ad+b
\]

componentwise, where A and b are nonnegative. Suppose a nonnegative matrix B
is supplied with

\[
B(I-A)=I.
\]

**Theorem.** Under these hypotheses,

\[
\boxed{d\le Bb.}
\]

**Proof.** Rearrange to (I-A)d <= b. Multiplication by a nonnegative matrix
preserves componentwise inequalities. Therefore B(I-A)d <= Bb, so d <= Bb.
This proof requires no numerical limit or approximation. In particular, b=0
forces d=0 because d is nonnegative. All entries of the implemented A, B,
and b are exact rationals. The unknown d may be any finite real vector.

For a square matrix, a left inverse is an inverse. Thus B(I-A)=I also gives
(I-A)B=I. Let w=B(1,1,1)^T. Then w=1+Aw, so w>=1 and

\[
\kappa=\max_i\frac{(Aw)_i}{w_i}<1.
\]

The checker independently computes this strict weighted contraction as an
additional witness. It does not infer contraction from small floating-point
roundoff or from a visually convergent simulation.

The frozen example is

\[
A=\begin{pmatrix}0&1/2&0\\0&0&1/2\\1/2&0&0\end{pmatrix},
\qquad
B=\frac17\begin{pmatrix}8&4&2\\2&8&4\\4&2&8\end{pmatrix}.
\]

Here w=(2,2,2)^T and kappa=1/2. With zero forcing, d=0. With
b=(1/100,0,0)^T, the exact bound is

\[
\boxed{d\le(2/175,\;1/350,\;1/175)^T.}
\]

This bound is attained by d=Bb, which satisfies d=Ad+b. A nonzero forcing
term is retained, rather than erased to manufacture a zero error.

For a pure three-cycle with gains a,b,c>=0, direct substitution gives
d1 <= abc*d1. If abc<1, all three finite nonnegative errors vanish. Strictness
matters: at a=b=c=1, d=(1,1,1) is an exact nonzero solution. That failure is
frozen in the research report. Infinity also cannot be treated as an ordinary
finite coordinate in the argument: infinity <= infinity provides no bound.

This is an elementary nonnegative-matrix comparison argument, with no
mathematical novelty claim. To use it on the prizes, we would still need to:

1. Define three actual defects, with a proved relationship between each
   defect's vanishing and its intended target proposition.
2. Prove that these defects are finite and nonnegative on the full required
   domains, including all input sizes or all admissible initial data.
3. Derive the coupling inequalities from arithmetic, complexity theory, and
   analysis, with the same assumptions and uniform coefficients.
4. Prove that the actual resulting matrix has a nonnegative inverse of I-A,
   or otherwise establish a sufficient strict contraction.

No such cross-prize defects or inequalities have been established here.
Assigning the names R, P, and N to arbitrary numbers would not supply them.
For example, a worst-case running time is a function of input length and an
algorithm, not a single unexplained distance from truth.

## 3. A complete finite bridge from dynamics to SAT

Let S=(Q,I,E,F) be an explicitly enumerated finite transition system, with
N=|Q|>=1, nonempty initial set I, edge relation E, and bad set F. Safety means
that no path starting in I reaches F. No determinism assumption is needed.

**Finite completeness theorem.** A bad state is reachable if and only if
some bad state is reachable in at most N-1 transitions.

**Proof.** Choose a shortest bad-reaching path. If a state repeats, remove
the segment between the two occurrences. The resulting path still starts
initially, ends badly, and follows valid edges, contradicting minimality.
Hence every state on the shortest path is distinct, giving at most N-1
edges. The reverse implication is immediate.

For horizon K, add a self-loop at every state. This permits padding a path
of length at most K to exactly K without changing which bad states can be
reached. Conversely, deleting padding steps recovers a path in the original
system. This also handles dead ends and initially bad states.

Use Boolean variables x[t,s] for 0<=t<=K and s in Q. The CNF contains:

- Exactly one active state at every time: one positive row clause and every
  pairwise exclusion clause.
- A clause restricting time zero to I and time K to F.
- For each t<K and state s, the implication from x[t,s] to the disjunction
  of its next-time successors, including s itself for padding.

Thus

\[
\operatorname{SAT}(\Phi_K(S))
\iff \text{a bad state of S is reachable in at most K steps}.
\]

Combining this exact encoding with the finite completeness theorem gives

\[
\boxed{\operatorname{UNSAT}(\Phi_{N-1}(S))\iff
       \text{every reachable state of S is safe}.}
\]

This is a universal statement about path lengths for a fixed finite system.
When K<N-1, UNSAT establishes only the bounded statement. The included
late-failure example is safe through its short horizon and reaches its bad
state later; the checker refuses to promote the shorter certificate.

The encoding uses (K+1)N variables and

\[
(K+1)\left(1+\binom N2\right)+2+KN
\]

clauses, including an empty final clause when F is empty. At K=N-1 the
explicit encoding has O(N^3) size. Explicit finite graph reachability is
already solvable by ordinary graph traversal; translating this special
problem into SAT does not establish a fast algorithm for arbitrary SAT.
For a graph described succinctly by b bits of state, N may be 2^b; a
polynomial bound in explicit N is not a polynomial bound in b.

## 4. Independently check the solver, including UNSAT

The generator performs DPLL search, with unit propagation and a deterministic
shortest-clause branching choice. A SAT certificate gives every assignment
bit; the checker verifies every independently reconstructed clause.

An UNSAT certificate is a finite postorder tree. Every node records each
unit inference with its clause index. A leaf identifies a clause whose
literals have all become false. An internal node splits an unassigned
variable and supplies both children. The checker reconstructs each branch
context, validates every unit reason, checks both children, and rejects
shared nodes, unused nodes, invalid indices, or a missing branch.

Soundness is induction on this finite tree: a conflict excludes all
extensions of its current assignment; a forced unit preserves every possible
model; and two impossible children exclude both values of their split
variable. The root therefore excludes every assignment.

The standalone verifier imports no generator or earlier engine module.
The two CNF compilers are separately implemented and tested against direct
reachability. Hashes bind proof content to the intended encoding; the
checker still verifies the mathematics. Hash agreement alone is insufficient.
An optional separately supplied system binds acceptance to the caller's
requested input, rather than merely accepting some system in a certificate.

The implementation has explicit resource budgets and can return unresolved.
DPLL search and the size of general UNSAT trees have no claimed uniform
polynomial bound. The Python checker is independently implemented software,
not a proof-assistant kernel. The mathematical justification is written here.

## 5. Transfer safety in the correct direction

Let f map the source states Qs to target states Qt. Require:

\[
f(I_s)\subseteq I_t,\qquad f(F_s)\subseteq F_t,
\]

and, for every source edge a->b, either f(a)=f(b) or f(a)->f(b) is a target
edge. These conditions are checked over the complete declared finite systems.

**Safety transfer theorem.** If the target is safe, the source is safe.

**Proof.** Map any supposed source path from an initial to a bad state through
f. Its endpoints are respectively initial and bad in the target. Each step
is a target edge or a stutter; remove the stutters to obtain a target bad
path. This contradicts target safety.

The reverse direction is not established by these hypotheses. The target
may have extra paths with no source realization. The checker requires an
independently verified all-path target certificate; a finite-horizon target
certificate cannot be used to bypass the completeness obligation.

In the frozen example, five source states map to three target states by
f=(0,0,1,1,2). Proving target safety uses 9 Boolean variables and 20 clauses,
compared with 25 variables and 77 clauses for the direct source encoding.
This is a size reduction for this declared example, not a global optimum or
a measured speed guarantee. All five source edges are checked by the map.

## 6. What actually transfers to the three research targets

| Target | Reusable machinery | Argument still required before universal transfer |
|---|---|---|
| RH | Exact inequality witnesses, counterexample search, and verified finite reductions | A proved bound or induction controlling every remaining integer or nontrivial zero; no finite truth table supplies it |
| P versus NP | Encodings, SAT certificates, branch refutation, and tracked reduction direction | A uniform polynomial algorithm for all SAT inputs, or a sufficient lower bound applying to all permitted algorithms |
| Three-dimensional Navier–Stokes | Sound state abstractions, comparison inequalities, and validated residual bounds | A justified abstraction of the full PDE or a continuation bound covering every admissible datum, including unresolved modes and all necessary times |

A polynomial reduction A<=pB transfers an efficient solver for B to A.
A polynomial solver for an NP-complete problem establishes P=NP. Our
finite graph encoding does not supply such a solver. These directions follow
[Cook's official problem description](https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf).

For a polynomial-time proof verifier, existence of a proof within a
unary-encoded length bound is an NP question: the proof is its witness.
A constructive P=NP result could accelerate this bounded search and witness
recovery. It would not guarantee provability in the chosen system, a short
proof, or truth of the searched statement. This is the qualification needed
when applying Cook's discussion of automated proof discovery here.

The engine's existing fluid certificate remains attached to its exact initial
datum and written analytic dependencies. The existing RH checks remain
attached to their proved finite coverage. This release does not rerun or
enlarge those analytic certificates, and does not turn a discretized flow
graph into an exact representation of the infinite-dimensional PDE.

## 7. Executed validation and reproducibility

The release includes 16 passing targeted test methods:

- 384 exhaustive comparisons spanning every two-state directed graph,
  nonempty initial set, bad set, and horizon zero or one.
- 256 comparisons from 128 seeded larger graphs at two horizons, giving
  640 graph/horizon comparisons in these two groups. Additional edge cases
  cover a singleton, dead-end padding, and a late failure.
- 80 seeded general four-variable CNFs compared with all 16 assignments,
  plus a genuine branching UNSAT tree and context-corruption attacks.
- 64 seeded rational nonnegative matrix bounds, with the computed upper
  bound satisfying the comparison equation exactly.
- Case splitting, circularity, vacuity, input identity, strict JSON,
  standalone and optimized Python runs, and stale output replacement after
  an exhausted search budget.

The separate corruption suite has six accepted positive controls and
32 rejected changes to claims, coverage, encodings, proof steps, maps,
premises, and inverse matrices. These are tests of implementation soundness;
they are not evidence that all mathematical propositions have been explored.

From the extracted project folder on Windows:

```powershell
py -3 tools/universe_engine.py
py -3 tools/verify_universe_bridge.py results/universes-v019/transfer.json
py -3 tools/verify_universe_bridge.py results/universes-v019/coupled-zero.json
py -3 tools/challenge_universe_bridge.py
py -3 -m unittest discover -s tests -p "test_universe_bridges.py" -v
```

Use `python3` instead of `py -3` on Linux or macOS. These modules use only
the Python standard library. The C++ numerical implementation is unchanged.
For another explicit graph, use `--system input.json --output results/my-run`;
`--horizon K` requests bounded coverage and `--max-work` limits DPLL work.
Exit 0 means accepted output, 1 invalid or rejected input, and 2 exhausted
search resources. General proofs are not inferred from those exit codes.

The immediate research target is an actual uniform extension argument or
a derived contracting comparison for a precisely defined quantity. The
engine can now check and reuse certain bridges once supplied. It cannot
replace a missing bridge with a shared name, a metaphor, or a cycle of
unproved assumptions.