Why this question matters

You have a neural network that works. You trained it on a powerful computer, in floating point — the default computation mode of laboratory machines. Now you want to put it inside an object: a sensor, a prosthesis, a drone, an implant. Those objects have no floating-point unit, or not enough power to afford one. They compute in integers.

A simple question with heavy consequences: does the embedded network behave like the one you validated? If it diverges, even slightly, your validation is worth nothing — you certified one system and are deploying another. In a prosthesis or a critical system, that is not an academic detail.

The usual answer is: “run both versions and compare”. That is slow, expensive, and above all says nothing about the millions of situations you did not test. This work proposes something else: a guarantee computed in advance, covering all inputs at once, or honestly declining to pronounce.

What a useful answer must guarantee

Before proposing a method, the paper sets the bar. A genuinely useful answer must satisfy three requirements, and everything that follows should be judged against them:

Remember the third: it returns at the end, and it is what separates a true certificate from a mere predictor.

The certificate formula

For each neuron i and each time step t, write E_i(t) for an upper bound on the gap between the floating-point potential and the integer potential, and m_i(t) for the real margin — the distance from the potential to the threshold θ. The certificate is the worst ratio of the two, over the whole simulation:

R_cert = min_(i,t)   m_i(t) / E_i^eff(t)

The decision rule fits on one line: if R_cert > 1, the uncertainty never reaches the threshold anywhere — the spike trains are bit-identical.

Under which hypotheses

A guarantee is worth something only if its domain is stated. The certificate is proved exactly under these five conditions — no more, no less:

The nine-term error model

Where does the uncertainty E_i(t) come from? It accumulates step by step, from identified sources. This is the technical heart of the paper: seven terms that add error, and two state-update rules. Term 6 is the one that changes everything — the reason appears below.

The proof sketch

The reasoning is an induction over time. If every decision up to step t−1 agrees between the two versions, then they share exactly the same history — so the fan-in sum ranges over the same set of pre-synaptic neurons, and E_i(t) is a valid upper bound. If in addition the margin exceeds the uncertainty for every active neuron, the integer potential is necessarily on the same side of the threshold as the floating-point potential. The decision cannot flip.

It is this induction that makes the certificate global: R_cert > 1 asserts that no decision flips anywhere, at any instant. Keep this mechanism in mind — it also explains, further down, why the method fails for spike counts.

The result, shown directly

This is the most important figure in the paper — the one that carries the entire claim. Take the 18,375 configurations, compute each one’s certificate, and sort them by ground truth: those genuinely bit-exact in green, those that diverge in pink. Then look at where the certification gate falls.

It is as striking as it is simple: the “zero false positives” claim is not a number in a table, it is a visible absence — the emptiness to the right of the line, on the pink side.

The decision matrix

The same result, in accounting form. What the certificate says is crossed with what is true:

Reading: precision 1.000 (everything certified is exact), specificity 1.000 (no divergence certified), recall 0.886 (88.6% of exact cases are recognised). Coverage — the share of the corpus guaranteed — is 74.17%. The flip side: 1,758 configurations that are bit-exact are nonetheless not certified. The certificate is cautious; faced with doubt, it stays silent rather than risk an error.

The certificate spreads over an enormous range: its median is 12.4, its 95th percentile 5,256. In other words, most certified configurations are not “just above” the gate — they are far above it. The safety margin is comfortable where it exists.

Is it stable?

A result that holds only on a lucky seed is worth nothing. So the soundness is checked against both the random draw and the network architecture.

The same holds by architecture: AUC from 0.9925 to 0.9972, coverage from 71.27% to 75.71%, and still no false positive. The guarantee does not depend on which network is being certified — only on how much of it gets certified.

The decisive ingredient

Here is the most instructive result in the paper, and it is a negative one. It concerns term 6 of the error model: synaptic fan-in.

What happens if it is omitted? An envelope bounding each neuron in isolation, without counting the error arriving through the synapses, wrongly certifies 1,898 configurations that in fact diverge. It is not merely imperfect: it is dangerous, because a certificate that lies once certifies nothing at all.

The table below compares four ways of scoring the same corpus. It sums up the whole issue:

Where divergence hides

A natural question: what makes a network diverge? The answer is clear-cut, and it is not the architecture.

The stress test

A certificate is not judged on easy cases. So 520 configurations were built to trap it: maximal synaptic synchronisation, saturation, thresholds sitting exactly on a rounding boundary, weights pushed to their limits, firing at the very first instant, very long memory close to threshold.

Two rows say something. The 160 “half a step from threshold” configurations are all genuinely bit-exact — and none is certified. The certificate is maximally cautious there: it is not wrong, it is silent, and that row measures the price of its caution. The “long memory close to threshold” row is the only one where real divergences exist (11 out of 30): the certificate certifies 17 of them, none divergent.

The crucial distinction: of 520 traps, 460 lie within the theorem’s domain and 0 defeat it. The 60 saturating cases fall outside hypothesis H3: the criterion exceeds 1 there with no divergence observed, but that is not certification by the theorem. The domain where a proof applies and the domain where good behaviour has been observed are two different things, and this site never conflates them.

Where the method fails

The paper’s subtitle is “and why the same technique fails for counts”. Here is the exact frontier of the technique, and why it falls precisely there.

The tempting idea would be to extend the certificate from spike timings to the mere number of spikes. One might accept that spikes shift a little, as long as their count stays the same. But the per-neuron bound that worked for timings becomes unsound for counts: it is violated on 2,660 of the 18,375 configurations.

Why does it fail? It traces directly back to the induction in the proof. A neuron’s bound assumes it receives the same incoming signal in both versions. That holds as long as nothing has diverged. But as soon as a single neuron diverges, the assumption falls for every neuron downstream — and their bounds no longer mean anything.

Local, neuron-by-neuron certification is not closed under the causality of the network: one local divergence can invalidate the bounds of every neuron it can reach.

A sound bound for counts does exist — but it is empty of meaning. On 193 configurations whose real count error is exactly zero, this “safe” bound still certifies a possible error of 4,807 on average. It is technically right, and it is useless. The paper presents it for what it is — a universal fallback after loss of synchronisation — and never as a rate certificate.

Three nested requirements

This diagnosis opens an elegant structure. On this corpus, three levels of requirement nest inside one another, from strictest to loosest:

Two shades of statistical honesty the paper is careful to state. The outer shell of 88 configurations with perfect correlation but unequal counts is not an anomaly: a correlation of 1 means “affine relation”, not “equal vectors”. And two configurations show a negative correlation — flagged as a real, undiagnosed regime decorrelation rather than dismissed as noise.

Certifying the decision, not the spike

For a classification task, requiring every spike to coincide is stricter than necessary. What actually matters is that the winning class stays the same. Decision survival can therefore be measured directly.

The catch is requirement 3 from the beginning. To be computed, this decision predictor needs to know the real error of each output — which requires having already run the integer version. It is therefore post-execution: excellent, but not an a priori certificate. Calling it a “certificate” would break the rule set at the outset.

Scope and limitations

Algorithmic reproducibility

The artefacts, with their fingerprints

The complete sweep, the analysis file and the reconstruction scripts accompany the deposit, each with its SHA-256 fingerprint. Here are the first sixteen characters, as frozen on 21 July 2026:

rcert_pertick_sweep_v2.jsonl   041394d161497d0c   (18,375 raw rows)
rcert_analysis_v2.json         91e864d4b1a88a7a   (main analysis)
rcert_adversarial_summary.json 7ccfa73c94467e35   (the 520 traps)
sweep driver                   9fcf5b3661c32213   (measurement script)
frozen simulation core         21332f7d25e1c15f

Checking the integrity of the whole archive takes one command:

sha256sum -c SHA256SUMS.txt

Every figure on this page was recomputed from those files rather than copied from the PDF. The false-positive count in figure 1, the decay thresholds in figure 4: each is reproducible in a few lines against the raw file.