Ask a mathematician what is known about Navier-Stokes regularity and you get a paragraph that is out of date by the time it is finished. Ask a registry and you get a list of theorems with links. Neither gives you what a working programme actually needs: for any statement, how established is it, what does it rest on, what would knock it down, and what falls with it. Those are properties of a graph, and in September 2026 we built the graph as governed data in 8DB. This article is the design.
Atoms carry intervals, not scores
Each statement is an atom: a theorem, an open alternative, a hypothesis, a proposed route. Each carries a sourced anchor with the URL, the date, the commit where there is one, and the source class, which ranges from a kernel-checked development through a refereed paper to a self-deposited preprint or a public statement on a social network. And each carries an interval, not a number. The interval is an imprecise probability that the statement is established on the recorded evidence, and its semantics are strict. An open statement has a lower bound of zero, always. A theorem kernel-checked against a third-party pinned statement sits at [0.90, 0.98], with the upper bound held below 0.99 while there is no refereed publication and while the sandbox in our own replay was reduced. An unreviewed preprint claiming eleven proved links sits at [0.0, 0.40], because a claim is not evidence of itself.
| Atom, as exported 11 September 2026 | Interval |
|---|---|
| Forced Navier-Stokes breakdown, Theorem 1.1 | [0.90, 0.98] |
| Clay (C), breakdown on R3 with a smooth force | [0.90, 0.98] |
| Clay (D), breakdown on the periodic box | [0.90, 0.956] |
| Unforced Euler blow-up, Theorem 1.1 | [0.90, 0.98] |
| Forced blow-up for IPM, Boussinesq, Euler (second group) | [0.88, 0.97] |
| Conditional regularity under two hypotheses (July 2026 paper) | [0.60, 0.90] |
| Links 1 to 11 of an unreviewed preprint | [0.0, 0.40] |
| Clay (A), Clay (B), unforced blow-up, the open lemma, the two hypotheses | lower bound 0.0 |
Edges refuse to let a conclusion outrank its premise
An implication is an edge from premise to conclusion, and every edge carries a restriction map. Forward, the map is confidence-minimum and it is hard: a conclusion can never be more established than the premise it rests on, and an edge that would violate this is rejected at write time, so it never lands in the store. Backward, the map is confidence-containment and it is soft: a violation is logged rather than refused, and the export lists the two that exist. A control test writes a deliberately mis-ordered edge and confirms it does not land.
That single rule did real work this week. When the (D) fidelity concern reduced the upper bound on Clay (D), the reduction had nowhere to leak. When the Formal Conjectures project relabelled (C) and (D) as solved, the relabel was recorded as a registration event and moved no interval, because a label is not evidence. And an obstruction, such as the public scaling objection to removing the force, is neither an implication nor a refutation, so it enters as a hypothesis atom with its own falsifier and no edge at all; the relation to the open blow-up statement lives in that statement's gap.
Open problems are typed gaps, not nulls
The open alternatives, the open lemma and the two hypotheses of the conditional theorem are not blank cells. Each is a gap section with an epistemic state capped at provisional, a cost, a falsifier, and either a trigger that a governed tool could fire or an explicit reason no trigger exists. The gap on Clay (D) has a trigger: a request for a ruling from the Institute, with a thirty-day timeout. The gap on the specialist sign-off has none, and says why: a sign-off is a human judgement over five listed items and no tool produces one. The gap on unforced blow-up records the dyadic-model exercise proposed publicly on 8 September and notes that the substrate has no validated integrator for it. Six gaps, each answerable by a query.
Tiers are derived, never assigned
Nobody types a trust tier into this twin. A statement requests a tier and receives at most the ceiling that its recorded verification events earn. A static audit that passes earns the lowest formal tier. An independent build and an axiom audit that pass earn the next. Adding a Comparator match against a pinned statement earns the top formal tier. A refereed publication earns a separate tier of its own. A statement-fidelity pass or a kernel replay pass raises nothing by itself, by rule, and any failure of any of those kinds voids the formal ladder entirely. Pending events are ignored; the latest non-pending event of each kind is effective. A registry that says a result is peer reviewed, with no publication identifier, does not reach the refereed tier. And a tier earned from a registry's events persists as observational, while one earned from our own replay persists as proven, because the truth type depends on who earned it.
As of the 11 September export the derived tiers are: the Navier-Stokes theorem, Clay (C), Clay (D) and the Euler theorem at the top formal tier, from our own events; the second group's three results at the static-audit tier;1 the conditional theorem and the preprint at the source-attested tier; and no tier at all on the nine open statements.
Retraction is a query
Point the cascade query at the Navier-Stokes theorem and ask what falls if it is retracted. The answer is Clay (C) and Clay (D), and nothing else. Point it at the unreviewed preprint's links and the route through them falls while the Clay alternatives are untouched, because that route was never connected to them by an edge the maps would accept. That is the behaviour a research programme needs the day a premise is withdrawn, and it is the behaviour our own April record lacked.
Registries are ingested losslessly
Two public registries track formal results: the Palomar registry, and the formalization.yaml sidecar that Lean projects now carry. The twin ingests both and re-emits them with every input pointer preserved plus one extra object carrying the held tier, its ceiling, who earned it, the cascade dependents, the falsifier kinds and the gaps. Three live registry records were ingested on 11 September and round-tripped without loss. The registries record that something was checked. The twin records what that lets you conclude, and what would change it.
Counts as of 11 September 2026
| Property | Value |
|---|---|
| Atoms | 20 |
| Implication edges | 9 |
| Connected components | 11 |
| Hard restriction violations | 0 |
| Soft violations, logged | 2 |
| Typed gaps | 6 |
| Fidelity clauses, concerns | 17, 1 |
| Verification events on the Navier-Stokes theorem | 10 |
| Distinct provenance fingerprints in the export | 19 |
| Library tests, this module | 265 passed, 0 failed, 6 ignored |
The binary that builds, queries, persists and exports the twin exits non-zero if any hard violation is present or the counts differ from the constants in the source, so the table above is a test, not a description.2
Evidence notes
This twin computes nothing about fluids. Every number it holds is a count, an interval recorded from a cited source, or a hash. Its contribution is the governance layer: the write-time audit, the derived tiers, the typed gaps, the cascade and the lossless interop. The same layer underlies our regulated-clearing and evaluation work, where the statements are controls and the events are test runs, and it is the reason a database company had anything to add in a week that belonged to analysts.
What to bring us
- Your frontier. Any research programme whose state is a graph of claims with evidence. We will build the twin from your sources and hand you the cascade query.
- A registry. If you maintain one, the lossless round trip is the integration we would like to test against your live records.
- A rule we got wrong. The tier ladder and the interval semantics are published above so that they can be argued with.
Write to hello@8braid.com with the subject "Evidence twin: build one for our problem". You will hear back from an engineer.
Sources and further reading
- Palomar registry
- mathlib-initiative/formalization.yaml
- Walley, Statistical Reasoning with Imprecise Probabilities (1991), the interval semantics used here
- 8DB: What a Claim Ledger Must Catch: A Live Case From the Navier-Stokes Frontier
- 8DB: Kernel-Checked Is Not Verified: Auditing a Millennium Statement Clause by Clause
- 8DB: Compliance You Can Replay
All intervals, tiers and counts are as exported from the twin on 11 September 2026 and describe the recorded evidence on that day, not the truth of any mathematical statement. Intervals are imprecise probabilities that a statement is established on that evidence and are our assessment, not a community consensus. 8Braid makes no mathematical claim about the Navier-Stokes equations and has no affiliation with any registry, institution or author referenced here.
Footnotes
Continue the technical conversation
Where could this help your work?
Bring a research question, a database workload or an application you want to build. Let’s connect the ideas in this article to an evaluation that matters to your team.
Discuss this work