# Independent certificate verification **Reality Bit Engine 0.12.0 — 4 September 2026** **Research framework:** Anthony Michael Collado **Status:** Independently implemented algorithmic verification of scoped results. No Millennium solution or formal proof-kernel verification is claimed. Version 0.12 adds a standalone verifier that imports neither the engine nor the code that generated its mathematical results. Its input is a portable certificate containing the necessary numbers and a narrowly defined claim scope. It computes acceptance itself; a producer's `passed` flag is not accepted as evidence. The valid certificate passed. All 26 deliberate corruptions were rejected. Ten new test methods passed, including an isolated execution with only the checker and certificate present, and a test showing that Python's `-O` option cannot disable rejection. | Result | Earlier computation | Independent verification | |---|---|---| | 1,023 Lagarias base cases | 128-bit outward-rounded intervals and divisor-pair sums | Exact rational lower polynomials, exact harmonic sums, and a divisor sieve | | 21 pigeonhole CNF histograms | Enumeration of every assignment | A row-counting recurrence with an exact quotient by column permutations | | Fluid energy/enstrophy identities | Complex exponential Fourier polynomials and differentiated transport | Real trigonometric polynomials, exact moments, and vortex stretching | All three checks still rely on mathematical definitions and standard arithmetic. Different implementations reduce shared implementation risks; they do not independently establish that the definitions describe seven-dimensional physics. ## 1. Portable workflow From the project root, using Python 3.10 or later: ```sh python3 tools/verify_certificate.py results/portable-certificate-v1.json ``` On Windows: ```powershell py -3 tools/verify_certificate.py results/portable-certificate-v1.json ``` The verifier and JSON certificate can be copied into a directory by themselves. No engine installation, C++ build, NumPy, or network connection is needed. Acceptance has exit code 0; a rejected certificate has exit code 1 with a reason. To regenerate the portable input and repeat the corruption checks: ```sh python3 tools/export_certificate.py results/proof-routes-v1.json --output results/portable-certificate-v1.json python3 tools/verify_certificate.py results/portable-certificate-v1.json --output results/my-verifier-result.json python3 tools/challenge_certificate.py results/portable-certificate-v1.json --output results/my-challenges.json python3 -m unittest discover -s tests -p 'test_certificate_verifier.py' -v ``` Export does not imply acceptance. The exporter can emit a false witness if its source is wrong; the verifier must then reject it. The standalone checker does not import `export_certificate`, `proof_routes`, `residual_audit`, or the challenge harness. The schema is deliberately narrow. It specifies the restricted RH scope, exact SAT encoding and finite instance coverage, and the particular fluid fields, parameters, and periodic domain. Unsupported broader claims are rejected. This checker is not a universal proof assistant or a checker for arbitrary mathematical formulas. ## 2. Independent rational verification of the RH base cases For each integer from 1 through 1,023, the portable witness stores its divisor sum and a 24-bit lower harmonic coordinate \(h=a/2^{24}\). The verifier independently computes the exact rational harmonic sum and checks \[ h\le H_n\sigma(n) \] for every \(2\le n\le1023\), and checks equality at 1. These comparisons all passed. It does not import or reproduce the producer's rounded exponential/logarithm interval code. No upper transcendental bound is needed to establish these base-case inequalities. The checker also confirms the rational constants used by the written large-integer argument. The number-theoretic product estimate and convexity argument extending the result to all integers with at most two distinct prime factors remain written proofs in `PROOF_ATTEMPTS.md`. The program does not represent those arguments in a formal proof calculus. The restriction on prime support remains essential; RH for all integers has not been proved here. ## 3. Exact counting through a projection The SAT computation provides a concrete application of the framework's projection idea. A partial assignment, after processing some pigeons, gives a vector of hole occupancies and an accumulated clause cost. Let \[ c=(c_1,\ldots,c_h),\qquad e\in\mathbb N_0. \] The next pigeon may choose any subset \(M\subseteq\{1,\ldots,h\}\), including the empty set. This permits every Boolean row, including rows that violate the intended constraints. Adding that row produces the exact cost increment \[ \Delta(c,M)=\mathbf1_{M=\varnothing} +\binom{|M|}{2}+\sum_{j\in M}c_j. \] The three terms count the new unassigned-pigeon violation, new within-row exclusivity violations, and new conflicts with earlier pigeons in selected holes. Define the projection \[ \alpha(c,e)=(\operatorname{sort}(c),e). \] Let \(F_r(c,e)\) count all labeled assignments of the first \(r\) pigeons whose projected state is \((c,e)\), with \(c\) sorted. Initialize \[ F_0((0,\ldots,0),0)=1. \] Then, for each subset \(M\), add \[ F_r(c,e) \quad\text{to}\quad F_{r+1}\!\left(\operatorname{sort}(c+\mathbf1_M),e+\Delta(c,M)\right). \tag{C} \] ### Why sorting preserves the count Take any two labeled occupancy vectors related by a permutation of the holes. That permutation gives a bijection between their subsets \(M\). Corresponding subsets have the same cardinality, the same sum of selected occupancies, and the same sorted successor vector. They therefore have equal cost increments and identical projected successors. It follows that every labeled vector represented by a sorted state has the same multiset of projected transitions. We may multiply those transitions by the accumulated number of represented assignments. Starting from the unique empty assignment, induction on the number of rows proves recurrence (C) counts every labeled Boolean assignment exactly once. In operator notation, if \(T\) adds every possible next row and \(\bar T\) applies (C), their actions on count measures satisfy \[ \alpha_*T=\bar T\alpha_*. \] This is an exact correspondence between an upper description and a reduced counting rule. It depends on the symmetry of the specified CNF. It is not a claim that any individually fixed labeled row update descends to the sorted representation, or that arbitrary weighted or asymmetric hole rules would do so. ### What must not be discarded Keeping only column occupancies would lose necessary information. These two row assignments both have occupancies \((1,1)\): \[ \begin{pmatrix}1&0\\0&1\end{pmatrix}, \qquad \begin{pmatrix}1&1\\0&0\end{pmatrix}. \] The first has cost 0. The second has cost 2: one pigeon occupies two holes while another occupies none. The reduced state must therefore retain the accumulated cost as well as occupancies. This is a concrete counterexample to dropping a coordinate without checking what distinctions it carries. For the 21 declared instances, recurrence (C) used **4,632 row transitions**, with a largest intermediate table of **215 states**, and recovered histograms representing **112,938 assignments**. Every histogram matched the independently generated certificate. Transitions and complete assignments are different units of work; these numbers are not a measured runtime speedup and do not establish a polynomial algorithm for arbitrary SAT. ## 4. Independent fluid identities The checker expresses the initial vertical component as \[ \cos x-\cos(x+y)=\cos x-\cos x\cos y+\sin x\sin y. \] It works in polynomials of \(\sin x,\cos x,\sin y,\cos y\), differentiating with the ordinary chain rule. The spatial average of each monomial factors into two circle averages. Odd powers integrate to zero; for even powers it uses \[ \left\langle\sin^{2m}x\cos^{2n}x\right\rangle =\frac{(2m)!(2n)!}{4^{m+n}m!n!(m+n)!}. \] This elementary moment formula follows from integration by parts and the identity \(\sin^2x+\cos^2x=1\), starting with the mean of 1. The formula and exact rational arithmetic are part of the checker's trusted mathematical implementation. The producer computed nonlinear enstrophy production from the differentiated transport term. The checker instead constructs \(\omega=\nabla\times u\) and computes vortex stretching: \[ Z'=\langle\omega\cdot(\omega\cdot\nabla)u\rangle -\nu\langle|\nabla\omega|^2\rangle. \] For the documented field with \(A=1\), \(\nu=1/100\), it independently recovers \[ E=\frac34,\quad Z=1,\quad E'=-\frac1{50},\quad Z'=\frac{11}{50}. \] It also checks the five specified weighted-functional witnesses and six fixed-energy/high-frequency examples. The latter use the explicit \(N^2\) derivative scaling and the circle moments for sine and cosine. These identities reject the particular estimates discussed in `PROOF_ATTEMPTS.md`. They do not establish a singularity or general regularity. The checker accepts only these specified smooth periodic fields; it cannot certify arbitrary numerical fluid solutions. ## 5. Frozen corruption tests The challenge harness retains the name, digest, rejection result, and reason for each deliberate corruption. The valid input is a positive control. The 26 negative controls include: - Unsupported schemas, injected pass flags, and broader theorem claims. - A removed prime restriction, missing or duplicate RH cases, a wrong divisor sum, a false harmonic lower bound, and an excessive arithmetic budget. - Boolean values substituted for integers, duplicate JSON keys, floats, NaN, and infinity. - Changed SAT encoding or coverage, a contradiction relabeled as zero, and a histogram whose total count remains correct while its distribution is wrong. - Altered fluid assumptions, energy signs, enstrophy growth, weighted rates, frequency scaling, malformed rationals, and missing examples. All 26 were rejected. The verifier uses explicit exception-based checks rather than Python `assert`, so `-O` does not remove its validation. Integer type checks reject Boolean aliases, and typed memoization preserves that distinction even after a valid integer case has been cached. These are finite adversarial tests. They are not an exhaustive proof that the parser or verifier has no defects. ## 6. What is still trusted | Layer | What this release checks | What remains outside that check | |---|---|---| | Certificate data | Required scope, complete declared coverage, arithmetic witnesses, counts, and identities | Unspecified mathematical statements and empirical claims | | Producer implementation | Results are rechecked without importing its code or trusting its flags | Source attribution and mathematical novelty | | Verifier implementation | Independent methods, mutation rejection, type guards, isolated execution | A formal proof of the verifier's soundness | | Mathematical arguments | Exact finite facts and constants used by the written derivations | Formalization of all analytic and combinatorial proof steps | | Physical interpretation | No new physical validation in this release | Seven physical dimensions, metaphysical claims, or a universal law of nature | An established proof assistant could reduce the trusted mathematical code by checking explicit proof terms. Lean's [official introduction](https://lean-lang.org/doc/reference/latest/Introduction/) describes its small trusted kernel and independently implementable design. This release does not run Lean, emit checked Lean proofs, or claim equivalent assurance. A proof assistant would also require that the formal statement correctly express the intended theorem. The strongest justified description is **independently checkable, scoped mathematical evidence with explicit written proofs and frozen counterexamples**. Calling the complete framework “irrefutable” would exceed that evidence. The frozen files are `results/portable-certificate-v1.json`, `results/verifier-v012.json`, and `results/certificate-challenges-v012.json`. The earlier proof-route source/document fingerprints still match because their generator, proofs, and input report were preserved unchanged.