The Epistemic Engine

Answers that carry their own proof.

Every incumbent sells compute that emits numbers. FrankenSim sells the thing the numbers were always a proxy for — justified belief at minimum cost. A result is not a float; it is a claim that arrives with its warrant attached.

verifiedvalidatedestimated

“A false certificate is worse than an ordinary wrong answer — a wrong answer wearing a badge.”

The entire type system exists to make that sentence impossible to violate by accident.

The Type System

Three Colors of Truth

Every quantity FrankenSim produces is stained one of three colors. The color is not a comment — it is part of the type, checked at every composition, and impossible to upgrade by wishful thinking.

select operands · press Combine
COMPOSITION — weakest grade winsverifiedclick to cycleestimatedclick to cycleoperatorTYPECHECKgrade latticean estimate can never be laundered into a certificateREGIME OF VALIDITY — leaving demotes to estimatedregime of validityboundaryoutside regimevalidated
  • verifiedinterval-certified — bounds proven
  • validatedanchored to data within a regime
  • estimatedbest-effort surrogate — no proof
composition lattice — click a cell to load operands
A\Bverivaliesti
veri
vali
esti
verified

Proven, not promised.

Bounds established by interval-certified numerics — outward-rounded intervals, exact geometric predicates, equilibrated-flux accept tests. The interval is guaranteed to contain the truth. This is the badge you can bet a bridge on.

fs-ivl · Newton–Krawczyk · Prager–Synge

validated

Reality signed off.

Anchored to experimental data inside a stated regime — a Buckingham-π envelope where the measurement was actually taken. Trusted because it matched the world, but only where the world was asked.

fs-regime · benchmark anchors · fidelity ladder

estimated

Useful, unproven.

Best-effort: a surrogate, a coarse solve, an ML proposal. Frequently excellent — but it has shown no proof and matched no experiment. It must wear amber until something certifies or validates it.

surrogates · coarse solves · proposers

The composition rule: the weakest link wins.

Color composes like a lattice meet. Feed an estimate into a proof and you get an estimate — never the reverse. There is no operator anywhere in the 54 crates that returns a color stronger than its weakest input. That is how FrankenSim makes laundering an estimate into a certificate a type error rather than a temptation.

verified
validated
estimated
estimated

Auto-demotion. A validated value silently reverts to estimated the instant it is evaluated outside the regime it was validated in. The badge is bound to its envelope; step past the boundary and the badge falls off by itself.

The Wrapper

Evidence Inside the Value

The color is the headline; the evidence is the dossier. Every result is an Evidence<T> — a value plus four uncertainty slices, a provenance hash, and an adjoint hook, all composed conservatively. Certified<T> is its refinement, reachable only through proof.

Certified<f64> · press Compose or Tighten
Certified<f64>12.47drag · Nverifiedtotal rel-err3.4e-2conservative linear budget · cap 8.0e-2∂value/∂inputs — adjoint hook attachedERROR BUDGET — stacked, composes conservativelycap12.0e-2 full-scalenumerical0.5e-2statistical0.8e-2model-form1.4e-2sensitivity0.7e-2blake3:bf5298+
the certificate travels inside the value provenance is content-addressed adjoint hook enables sensitivity back-prop
Numerical uncertainty

Discretization, rounding, and truncation error — the gap between the equation you solved and the one you meant. Bounded by interval and a-posteriori estimators.

Statistical uncertainty

Monte-Carlo and sampling variance carried as an anytime-valid confidence sequence, so peeking never inflates the claim.

Model-form uncertainty

The uncertainty of the model itself — the physics you left out. The honest, humbling slice most tools pretend does not exist.

Sensitivity uncertainty

How the answer moves as inputs move — supplied for free by the adjoint hook riding inside the value.

Provenance hash

A content address of exactly how the value was made. explain(artifact) can always reconstruct the derivation — the result knows its own history.

Adjoint hook

A gradient rides inside the value, computed through the implicit function theorem — so sensitivity is a property of the answer, not a second pipeline.

evidence.rs
01
use
fs_evidence::{Evidence, ProvenanceHash};
02 03
let
provenance = ProvenanceHash::of_bytes(b"laplacian kernel output");
04 05// A value that knows how it was made — and proves its own bound.06
let
drag = Evidence::exact(12.47, provenance)
07 .certified() // interval-certified numerics08 .expect("exact pure-math evidence is certifiable");09 10assert_eq!(drag.value, 12.47);11// drag carries: value + interval bound + provenance + adjoint hook + cancel scope
Syntax_Validation_Active
UTF-8_ENCODED
The Flywheel

Certified Speculation

How do you get the speed of a guess and the trust of a proof? You let anything propose, and let only mathematics accept.

proposed 0 · verified 0 · rejected 0 · cost saved 0%
PROPOSER BANK · cheap, possibly-wrongCERTIFIED VERIFIERVERIFIED ✓ · accumulatessurrogate modelNN emulatorcoarse solveh/2 meshML guesslearned priorpropose →Prager–Synge accept testequilibrated-flux a-posteriori boundfail-closed ↓→ certify (expensive) only survivorsmachine learning proposes · certified numerics disposes
verified ✓ (accepted, cyan)rejected · fail-closedproposer — never trusted alonethe cheap verifier screens most candidates; only survivors pay for expensive certification

Machine learning proposes; certified numerics disposes.

A surrogate, a coarse solver, or an untrusted ML model produces a candidate in microseconds. It arrives estimated and unloved. Then a cheap, independent verifier — an equilibrated-flux Prager–Synge a-posteriori accept test — checks whether the candidate actually satisfies the governing equations to tolerance. If it passes, it is stamped verified. If it does not, it is rejected.

Propose

Untrusted, fast, plural. ML, surrogates, coarse solves — race them all.

Verify

One cheap certified test decides. The verifier is the only thing that must be right.

Fail closed

No accept, no answer. A rejected speculation never leaks out wearing a badge.

Correctness Program

The Gauntlet

Certificates are only as good as the thing that issues them. The Gauntlet is six graded tiers that every merge must survive — and the discipline of certifying the certifiers so the judge is never above the law.

idle · press Run Gauntlet
G0Property lawsalgebraic-law suitesG1Order-of-accuracymanufactured solutionsG2Physics envelopescanonical benchmarksG3Metamorphicrelation testsG4Chaos / faultscancellation stormsG5Determinismcross-ISA · bit-identicalpress Run Gauntlet — every gate must pass to merge · G1 must match theory within Δ0.2
G0
Property & algebraic laws

Adjointness, symmetry, conservation, d∘d = 0 — the invariants a correct kernel can never violate.

G1
Manufactured solutions & orderFails the build

The build fails if the observed convergence slope drifts more than 0.2 from the theoretical order. Silent accuracy loss is a red build.

G2
Canonical benchmarks

Lid-driven cavity, Taylor–Green, NAFEMS — the problems the field already agreed on the answers to.

G3
Metamorphic tests

Relations that must hold even when the exact answer is unknown: refine, rotate, rescale, and check the invariant.

G4
Chaos & cancellation storms

Inject cancellation mid-solve, starve budgets, race speculators — correctness must survive the storm, resources must never leak.

G5
Determinism & cross-ISA

Bit-identical across runs, thread counts, and instruction sets. Any divergence is a diff, not a shrug.

Certifying the certifiers. Every verifier and error estimator is itself tested against manufactured solutions with known bounds — a certificate is trusted only after the thing issuing it has passed its own Gauntlet. The Goodhart guard treats each optimizer endpoint as an adversarial example and re-checks it out of band, because a measure that becomes a target stops being a good measure.

The Sheaf View

Watertight by Cohomology

Geometry gluing is not eyeballed. Watertightness is defined as an algebraic fact — the vanishing of an interface cocycle — so a surface either provably seals or names exactly why it cannot.

H¹ = 0 — watertight ✓ manifold
AU_A chartBU_B chartCU_C chartDU_D chartclick a seam to toggle its interface cochain · δ = coboundary operator
seam consistent (δc = 0)seam obstruction (δc ≠ 0)H¹ = 0 ⇔ watertight manifold

Watertight ≡ H¹ = 0

Model the surface as a cellular sheaf: each patch carries local data, each shared edge carries a compatibility constraint. Watertightness is precisely the vanishing of the first cohomology — the interface cocycle is zero. No gaps, no double walls, no self-lies. A seal is now a theorem you can check, not a rendering you squint at.

Conflicts classify themselves

When a merge fails, the cocycle tells you which kind of failure it is. A coboundary conflict is a bookkeeping mismatch — mechanically auto-fixable. A harmonic conflict is structural — a genuine topological disagreement no amount of retopo can paper over. The math sorts the fixable from the fundamental for you.

Structured Errors

A Refusal That Teaches

The most epistemically honest thing a system can do is decline — and the most useful thing it can do while declining is explain. When a request is infeasible, FrankenSim does not fail with a stack trace; it returns a structured, ranked set of ways forward.

refusal.json
01{02  "error": "BudgetInfeasible",03  "stage": "flux.lbm",04  "need": { "wall": "5.1h" },05  "have": { "wall": "2h" },06  "fixes": [07    { "action": "relax qoi-rel-error to 4e-2", "est_wall": "1.7h", "est_qoi_impact": "+1.8e-2" },08    { "action": "surrogate screen, certify top-4 only", "est_wall": "1.9h" }09  ]10}
Syntax_Validation_Active
UTF-8_ENCODED

“A refusal that teaches is worth ten silent successes.”

A BudgetInfeasible is not a dead end — it is a conversation. It states exactly what the plan needed, exactly what it was given, and a ranked list of concrete fixes, each with an estimated wall-clock cost and its impact on the quantity of interest. An agent swarm reads this and re-plans; a human reads it and understands the trade in seconds. The system refuses to guess, and refuses to hide why.

The Backbone

Principles the Epistemics Rest On

None of the above is a bolt-on. The three colors, the evidence, the refusals — all of it falls out of ten non-negotiable principles and five things that are never, ever left implicit.

The Decalogue
P1
Pure, memory-safe Rust

One language, Franken-constellation dependencies only. Unsafe lives only in audited leaf capsules under 300 lines, each behind a safe façade.

P2
Determinism is a feature

Bit-identical across runs, thread counts, and (best-effort) ISAs — via fixed-shape reduction trees, counter-based RNG keyed by logical identity, and compensated summation.

P3
Differentiable or certifiable

Every operator is differentiable, certifiable, or ideally both. Gradients are checked at the merge gate; error bounds are first-class.

P4
Budgets first

Every operation takes an accuracy / time / memory budget. The Error Ledger and Time Ledger compose them end-to-end and attribute every digit and every second.

P5
Structure over brute force

Exact discrete de Rham (d∘d = 0), symplectic integrators, power-conserving ports. Preserve the math instead of resolving it away.

P6
Matrix-free & roofline-honest

Kernels ship their arithmetic-intensity analysis against machine peak. No dense assembly where a matrix-free apply will do.

P7
Cancellation-correct compute

Cancellation is a numerical primitive. Bounded latency-to-cancel of ≤ 200 µs; speculative races kill their losers mid-solve.

P8
One data model

Complexes and cochains, everywhere. Geometry, fields, and operators share a single typed algebra instead of six incompatible schemas.

P9
Provenance-complete

Content-addressed artifacts, event-sourced operations, and explain(artifact): a result always knows how it was made.

P10
Agent-first ergonomics

The Five Explicits — units, seeds, budgets, versions, and capabilities — are never implicit, ever. Built for the swarm, compatible with humans.

The Five Explicits
Units

Dimensional quantities are compile-time typed. A meter never silently becomes a second.

Seeds

Counter-based RNG keyed by logical identity. Every random draw is reproducible by construction.

Budgets

Accuracy, time, and memory ceilings travel with every call and compose across the whole plan.

Versions

The constellation is locked by hash. The kernels that produced a result are always recoverable.

Capabilities

The Cx context grants exactly what an operation may touch — arena, cancel token, ledger, budget.

What No Incumbent Can Retrofit

You cannot add evidence to a value that was never designed to carry it. Composition, error bounds, provenance, and the three colors are load-bearing structure, not a reporting layer — which is exactly why they cannot be sprinkled onto a stack of six tools that only speak floats to each other.

Capability
FrankenSim
COMSOLOpenFOAM + FEniCSSciPy + Dakota
Language & memory model
One safe RustC / Java GUIC++Python + C/Fortran
Evidence inside values
Certified<T>NoNoNo
Error bounds cross tools
Composed ledgerPer-solverManualNone
Provenance / replay
Content-addressedProject fileCase dirAd hoc
Determinism
Bit-identicalBest-effortMPI-dependentBLAS-dependent
Cancellation
≤ 200 µs, structuredKill processKill processKill process
Geometry ↔ physics
CutFEM on SDFMesh requiredMesh requiredExternal
Gradients
Adjoint-nativeAdd-onadjoint solverautograd (external)
Anytime-valid stats
e-processesNoNoFixed-sample
Meshing in the loop
OptionalRequiredRequiredn/a
Agent-first API
FrankenScript IRGUI / Javadict filesPython
Runtime dependencies
Franken-onlyProprietaryMPI stackNumPy / SciPy stack

The kernel is where the proofs live.

See how seven acyclic layers turn these epistemics into running Rust — or watch them earn their keep in the three flagship pipelines.