# Shared proof structure and directed refinement **Reality Bit Engine 0.18.0 — 5 September 2026** **Originating research framework:** Anthony Michael Collado **Status:** Implemented research methods, written sufficient arguments, independently checked scoped certificates, and explicit unresolved universal obligations. ## 1. What are we actually trying to solve? The common task is to find a description that retains enough information to justify a claim under every extension allowed by that claim. A finite list of successful calculations does not supply that extension argument by itself. | Target | Required scope | Useful existing evidence | Essential missing step | |---|---|---|---| | Riemann Hypothesis through the Lagarias formulation | Every positive integer | Exact finite checks; written canonical/record reductions; historical bounded verification through \(10^{24}\) | Control the remaining infinite record sequence with adequate error terms | | P versus NP | A uniform polynomial-time algorithm, or a lower bound covering every allowed algorithm | Exact bounded SAT certificates and restricted-family arguments | A general complexity argument with the correct quantifiers | | Navier–Stokes | Every admissible initial field and the required time domain, or an admissible breakdown example | Exact certificates for specified periodic initial fields | An all-data continuation estimate or a valid breakdown construction | The official target descriptions are available from the [Clay Mathematics Institute](https://www.claymath.org/millennium-problems/). These are shared proof-engineering requirements, not a demonstrated equivalence between the three mathematical problems. Improvements on one target do not automatically resolve the other two. For a positive solution of P versus NP via SAT, the relevant shape is \[ \exists A,c,k\quad\forall F: \quad A(F)\text{ decides SAT correctly and } \operatorname{time}_A(F)\le c(1+|F|)^k. \] A lower bound on one solver, one formula family, or one restricted summarization strategy has different quantifiers. No amount of finite success silently changes those quantifiers. The new direction is therefore **maximize independently verified coverage per declared computational budget**, using sound abstractions, inductive arguments, explicit residuals, and reusable certificate work. This is an engineering objective. No globally optimal discovery strategy or probability of solving a Millennium problem is claimed. ## 2. The common algebraic contract For a transition relation \(T\) on states \(X\), define \[ \operatorname{Post}(S)=\{y:\exists x\in S,\ (x,y)\in T\}. \] Let \(S_0\) be the allowed initial states and \(B\) the forbidden states. A set \(I\) satisfying \[ \boxed{ S_0\subseteq I,\qquad \operatorname{Post}(I)\subseteq I,\qquad I\cap B=\varnothing } \tag{1} \] proves \[ \forall n\in\mathbb N:\quad \operatorname{Post}^{,n}(S_0)\cap B=\varnothing. \tag{2} \] **Proof.** The initial inclusion supplies the base case. If every state after \(n\) transitions belongs to \(I\), transition closure puts every state after \(n+1\) transitions in \(I\). Induction gives the inclusion for every finite \(n\); disjointness from \(B\) gives (2). Every prefix of an infinite trajectory is also safe. This does not prove that trajectories terminate, that infinite trajectories exist, or that a fairness/liveness property holds. For an abstraction \(\alpha:X\to A\), its state distinctions must be sufficient for the property being proved. An abstract transition relation may overapproximate concrete transitions, but may not discard a possible concrete transition. A coarse abstraction can therefore produce a false alarm: individually possible abstract edges may combine into a path that no concrete state can follow. In the fluid calculation, the corresponding mechanism is an error tube whose boundary cannot be crossed under the verified differential inequalities, followed by entry into a region controlled for all future time. In the number-theoretic and complexity targets, a suitable all-case extension argument is still missing. Writing those targets in a shared interface does not create that argument. Encoding an answer as a bit or a distance from zero does not bound the work needed to compute it. Likewise, a small number of abstract blocks does not imply a compact membership map or an efficient way to discover that map. Representation size, search cost, and proof scope must be tracked separately. ## 3. An executable refinement method for finite systems `induction_engine.py` accepts an explicit finite, possibly nondeterministic transition system and a partition of its states. It computes the abstract transition graph and searches for a path from an initial block to a block containing a forbidden state. If no such path exists, the reached blocks define an inductive invariant. If a path exists, the engine checks whether it has a concrete realization. For an abstract path \(a_0,\ldots,a_m\), define backward suffix sets \[ S_m=\alpha^{-1}(a_m)\cap B, \] \[ S_i=\{x\in\alpha^{-1}(a_i):\exists y\in S_{i+1},\ (x,y)\in T\}. \] If \(S_0\) intersects the concrete initial set, following these witnesses yields a real counterexample. Otherwise the abstract path is spurious. The engine splits a block at a nonempty proper suffix subset and tries again. Such a split exists on a spurious abstract path: if each nonempty suffix set were its entire block, the preceding abstract edge would keep the preceding suffix nonempty, eventually giving a concrete initial realization. Each split strictly increases the number of blocks. For \(N\) concrete states, at most \(N-1\) splits are possible from a single initial block. A smaller user budget can stop the search with an unresolved result. No claim of a minimal partition or optimal search order is made. The standalone `verify_induction.py` does not reproduce the search. It checks a complete, disjoint partition and uses integer bit masks to verify all three conditions in (1) directly on the supplied concrete transitions. For a counterexample it checks every edge and both endpoints. Optional `--system` binds the certificate to a separately supplied requested system, preventing a changed premise from being accepted for the original problem. The supported certificate domain is at most 4,096 declared states and 65,536 transitions. The resulting safety theorem covers arbitrary path length **in that fixed system**, not all systems or all input sizes. JSON floats, nonfinite values, duplicate keys, invalid indices, unknown claims, incomplete partitions, false closure, and false traces are rejected. The supplied edges are the complete declared transition relation. A conclusion about that finite model does not cover additional possible transitions omitted from a model of an external system. ### Executed example The safe example has transitions \[ 0\to1,\quad 1\to1,\quad2\to3,\quad3\to4,\quad4\to4, \] initial state zero, and forbidden state four. Starting with all five states in one block produces three spurious abstract paths. Three refinements yield the invariant \(I=\{0,1\}\), which proves safety for arbitrary execution length. Changing the first edge to \(0\to2\) produces the real trace \(0,2,3,4\). It is returned as a counterexample, not repaired by relabeling the forbidden state. Tests also compare 160 seeded finite systems against an independently implemented concrete reachability calculation. ## 4. Direct computation toward the actual missing fluid modes The frozen v0.17 failure uses viscosity one and \[ u_0=(2\sin y+\varepsilon\sin z,\varepsilon\sin 2x, \varepsilon\sin y),\qquad\varepsilon=\frac12. \] Its initial \(\chi^{-1}\) norm is \(\sqrt{4+\varepsilon^2}+3\varepsilon/2>2.8\), outside the older total-smallness region. The eighteen-mode reference leaves nonzero interactions outside its support. For a conjugate omitted-mode pair \(\{k,-k\}\), the new engine assigns the exact rational score \[ W_k=\sum_j h_j\bigl(U_{j,k}+U_{j,-k}\bigr), \] where \(U_{j,k}\) bounds that mode's \(\chi^{-1}\) residual contribution throughout interval \(j\). It selects the highest-scoring pairs that fit the declared mode budget and wavevector limits. Seven pairs account for approximately **91.214%** of the old integrated omitted-residual upper bound. Adding them expands the reference from eighteen to thirty-two modes. The first interval's full residual upper bound drops from approximately **0.115940** to **0.020422**. This ranking is a heuristic for choosing a new reference. Adding modes changes the approximate dynamics, so the removed share of the old residual is not a guaranteed reduction in the new residual. The new trajectory and its complete residual must be constructed and checked again. Every interval of the release's refined reference contains 32 nonzero modes. A development test exposed a separate false expectation: at lower precision, a selected mode can round to the zero polynomial. The observed small example had 14 active modes within a 32-mode selection budget. The corrected contract is that the actual support contains the initial modes and is contained in the selected support, with exact constraints and full residual checks retained. This observation is preserved in `refinement-development-v018.json`. ## 5. Reuse expensive work without trusting a cache as a proof The engine compiles each reference interval into its exact rational polynomial coefficients, full residual witnesses, velocity bounds, and endpoint/initial-error bounds. Certificate parameter searches reuse that cache. The cache has a canonical content hash. A changed datum or witness changes its identity. A matching hash establishes content integrity, not the truth of its inequalities. A test deliberately replaces residual bounds with zero and recomputes the hash; the independent mathematical checker still rejects the resulting certificate. All fixed-cap and local-cap trials reuse the same interval bounds. Their search phase performs zero new residual reconstructions. The final standalone checker independently recomputes the complete residual across all intervals. This is where proof acceptance occurs, and in this run it costs far more than the cached parameter search. The CLI refuses simultaneous `--cache` and `--epsilon`: cached initial data are fixed. To change the input, rebuild without `--cache`. This prevents a successful certificate for one field from being mistaken for a result about a newly requested field. ## 6. Local error caps and their analytic justification The previous error estimate remains valid. With \[ E=\|u-v\|_{\chi^{-1}},\quad E_1=\|u-v\|_{\chi^1}, \quad V=\|v\|_{\chi^0},\quad R=\|r\|_{\chi^{-1}}, \] choose \(c>0\), \(\mu>0\), and \(D=\nu-c-\mu>0\). While \(E\le c\), \[ D^+E+\mu E_1\le\Lambda(V,D)E+R, \] \[ \Lambda(V,D)=\max_{x\ge1}(-Dx^2+2Vx) =\begin{cases}V^2/D,&V\ge D,\\2V-D,&V0\), so their minimum remaining damping is positive. Integrating the stronger inequality (3) with the fixed positive \(\mu\) bounds \(\int E_1dt\). Together with the smooth finite reference, this bounds the time integral of \(\|\nabla u\|_\infty\). The same standard local existence and Sobolev continuation argument used in v0.17 extends the solution through the certified interval. At the endpoint, the checker again requires \[ \|v(T)\|_{\chi^{-1}}^{\rm upper}+q(T)<\nu. \tag{5} \] The all-time small-data theorem in `GLOBAL_FLUID_BOUND.md` then applies to the full exact solution, whose spectrum need not remain finite. The analytic dependencies are written arguments, not formalized proof-assistant objects. This develops established approximate-solution validation; see [Morosi and Pizzocchero](https://arxiv.org/abs/1405.3421). The local search uses \(\mu=\nu/1024\), caps on a grid of \(\nu/1024\), and 64-bit outward envelope values. It tries 16, 64, then 256 affine segments per reference interval and stops at the first independently accepted certificate. Cap ticks and arithmetic bits are computational choices, not measurements of minimal physical increments. The local control policy also changes the reserve and envelope resolution; the comparison below evaluates the complete declared policies, not an isolated causal effect of a single parameter. ## 7. The formerly unresolved input is now certified All comparisons use the identical \(\varepsilon=0.5\) initial field, degree-six rational reference polynomials, 32 reference intervals, and final time four. | Reference | Fixed-cap policy: five declared configurations | Local-cap policy: declared refinement ladder | |---|---|---| | Eighteen modes | All unresolved | All three resolutions unresolved | | Thirty-two selected modes | All unresolved | 16 segments per interval unresolved; **64 independently accepted** | The 256-segment fallback is not visited for the refined reference. This is first-success search over declared configurations, not a global optimum. The accepted certificate establishes exact rational bounds with these outward decimal comparisons: | Quantity | Accepted result | |---|---:| | Reference intervals | 32 | | Active reference modes per interval | 32 | | Affine error segments | 2,048 | | Maximum error \(\|u-v\|_{\chi^{-1}}\) through time four | \(<0.73674\) | | Maximum local cap | \(0.7373046875\) | | Minimum remaining damping \(\nu-c_\ell-\mu\) | \(0.26171875\) | | Positive dissipation reserve | \(1/1024\) | | Full norm bound at time four | \(<0.70240<1\) | | Omitted output-mode occurrences across intervals | 4,032 | Every reference interval has a nonzero full residual. The omitted-mode occurrence count is summed across intervals, not a count of distinct modes. Modes of the exact solution outside the reference's entire quadratic support are still controlled by the full error norm. Subject to the stated analytic dependencies, (5) supplies global smoothness for this particular input. It expands the engine's sufficient-certificate coverage. No previously unknown regularity class, general large-data theorem, or mathematical priority claim is made. ## 8. A director that keeps proof scope explicit `proof_director.py` invokes the independent backends and constructs evidence scopes from their accepted results. It compares property, mathematical domain, problem identity, and finite versus unbounded coverage before allowing a claim to be supported. It independently rechecked: - The portable certificate's 1,023 RH base cases and its stated restricted tail constants. - Twenty-one bounded pigeonhole SAT instances, counting 112,938 assignments through the existing symmetry-reduced dynamic program. - The finite system's inductive safety certificate. - The new local-cap fluid certificate. The historical \(10^{24}\) RH result remains preserved with its written reduction and implementation dependencies; this release does not rerun or upgrade it to formal verification. The director deliberately records the newly rechecked RH scope as the finite prefix its backend directly checks. Scope containment prevents a finite prefix from becoming an all-integer proof, an all-time result for one field from becoming an all-data theorem, or a restricted formula calculation from becoming a bound on every algorithm. A finite-system invariant can support arbitrary path length only for the same specified system and safety property. The director is a typed audit and orchestration layer. It does not check arbitrary mathematical proof texts, synthesize missing RH or complexity lemmas, or establish an equivalence between the prize problems. Supporting a new class of proof requires an appropriate mathematical argument and checker. All three universal target nodes therefore remain **OPEN**. This is an exact account of missing arguments, not a forecast about when they will be solved. ## 9. Validation, limitations, and the next useful work Twenty-three targeted test methods cover cache reuse and identity, forged caches with recomputed hashes, exact reference constraints and joins, local-cap inequalities and coverage, nonzero initial error, stale-output replacement, requested-input binding, finite-system refinement, concrete counterexamples, scope containment, isolated standalone execution, and rejection under optimized Python. The finite-system tests include 160 seeded comparisons against direct concrete reachability. All 24 deliberate corruptions of a small two-interval nonlinear local-cap certificate are rejected. The positive control passes. These challenge results are not 24 repeated verifications of the large release certificate. The next work should target proof dependencies rather than merely extend a test counter: | Direction | Concrete next obligation | |---|---| | Formal verification | Formalize a selected analytic bridge and its dependencies; the present checkers are independent programs, not a proof-assistant development | | RH | Construct and rigorously check a proposed infinite-tail comparison on the record sequence; the already-refuted fixed \(c<\gamma\) route is not repaired by increasing its cutoff | | P versus NP | State and prove a uniform complexity claim with explicit algorithm and input-size quantifiers; finite abstraction refinement can still require all concrete distinctions | | Fluids | Extend certificates to neighborhoods or families of initial data with verified uniform bounds, or improve the norm/control estimate; pointwise successes alone do not cover all data | | Computation | Profile and reduce the independent full-residual check, which is now more expensive than the cached candidate search, while preserving a separately implemented acceptance path | Finite-state refinement can require up to all \(N\) states and does not establish polynomial complexity in a succinct description of that system. No empirical seven-dimensional physics, quantum hardware, or theological claim follows from these certificates. ## 10. Run it on a PC Python 3.10 or later and the standard library suffice. On Windows, use `py -3` in place of `python3`. The new research companions do not require C++ compilation. To verify the included main result: ```sh python3 tools/verify_local_trajectory.py results/local-cap-certificate-v018.json ``` To rerun candidate search from the included refined reference cache: ```sh python3 tools/refinement_engine.py --cache results/refinement-certificate-v018-cache.json --local-caps --output results/repeated-local-certificate.json ``` To rebuild the reference, its residual bounds, mode selection, local search, and independent acceptance from the initial field: ```sh python3 tools/refinement_engine.py --refine --local-caps --output results/rebuilt-certificate.json ``` The default input is \(\varepsilon=1/2\). Rebuilding and independent checking can take several minutes; machine-dependent elapsed times in the records are observations, not performance guarantees. Failed searches return exit code 2 and retain an unresolved result. Invalid inputs return 1. An accepted search returns 0 only after the independent checker accepts. For a custom finite transition system, save an object with `states`, nonempty `initial`, `bad`, and `edges`, using state indices from zero through `states-1`: ```sh python3 tools/induction_engine.py --system system.json --output safety.json python3 tools/verify_induction.py safety.json --system system.json ``` To reproduce the included abstract-safety examples and the cross-target audit: ```sh python3 tools/induction_engine.py python3 tools/induction_engine.py --unsafe-demo --output results/induction-counterexample-v018.json python3 tools/proof_director.py python3 tools/challenge_refinement.py python3 -m unittest discover -s tests -p 'test_refinement.py' -v python3 -m unittest discover -s tests -p 'test_induction.py' -v ``` The old proof modules and their frozen documents remain unchanged. The v0.18 addition directs work toward missing information and valid extension arguments while preserving the distinction between an accepted scoped theorem, a real counterexample, a failed sufficient bound, and an open mathematical question.