teal-sea / zeta-labstate of record · compiled 14 Aug 2026 · revision 9ebdea0 · source

Library · meta/asymmetry-experiment.md

Independent vs shared verification — an experiment design

1,316 words · 160 lines · source

Pre-registration draft, 2026-08-10. Nothing here has been run. Predictions are stated before any data exists, and the whole point of writing them down now is that they can embarrass me later.

The observation that prompted it

Across this repository, checks sort cleanly by whether they were independent of the artifact they check:

checkindependentdeterministiccheapcaught real defects
Lean kernelyesyesnoyes
Fraction mirror vs the rung-3 planyesyesyesyes, decisively
Arb vs mpmath cross-checkyesyesnoyes
outside model reading the public repoyesnoyesyes
integrity audit vs batteriesnoyesyes2 of 6
promotion gate vs claim reportsnoyesyesno — loses to its null control

Why the observation is not yet a result

Three variables are confounded. Independence, determinism and cheapness co-vary across every row above, so the table cannot distinguish:

There is also a fourth candidate nobody has controlled for: the co-designed checks in this tree may simply be weaker artifacts, built later and with less care, and the asymmetry may be about effort rather than architecture.

Until those are separated, "independent verification beats shared verification" is a hunch with a suggestive table under it. This design separates them.

Design

A factorial over three factors, with planted faults, blind authorship, and one arena outside mathematics.

Factor A — relationship to the artifact. Independent: the checker's author never saw the artifact or its author's reasoning. Co-designed: checker and artifact authored by the same process, as harness/integrity.py was against the batteries it audits.

Factor B — decision procedure. Deterministic: a program with no model in the loop at check time (kernel, mirror, compile-and-run). Probabilistic: a model asked to find the defect.

Factor C — cost. Cheap: runnable in seconds, before commitment. Expensive: minutes to hours, run once at the end.

Eight cells; six are populatable now. (Independent + probabilistic + expensive and co-designed + probabilistic + expensive can be dropped in round one.)

Arenas. Two, deliberately:

  1. Mathematics — interval-arithmetic claims, where a cheap exact independent oracle is available (the Fraction mirror pattern) and an expensive one is too (the Lean kernel).
  2. Programs — the compiler/ department's LLVM IR rewrites, which already has an executable oracle (compile and run) and a foreign vocabulary. Chosen because it breaks any explanation that depends on the subject being mathematics.

Faults. Planted, from three sources so that no single author's imagination bounds the fault space: the existing SHAM_MODES catalog, compiler/FINDINGS.md's recorded incidents, and faults authored by a party who sees no checker.

Blinding, and how it is enforced rather than declared. Fault authors and checker authors exchange only SHA-256 digests of their bundles before reveal, per the procedure already specified in the E1–E3 logistics. harness/preregistration.py records the digests of evidence existing at freeze time, so independence is derived from artifacts rather than asserted in a README. That mechanism is the reason this experiment is worth running here rather than anywhere else.

Measurements

Five, and the fifth is the one nobody currently takes.

  1. Defect detection rate — planted faults found / planted.
  2. False confidence rate — artifacts containing a planted fault that the checker grades sound. This is the quantity that matters for deployment, and it is not one minus detection: a checker may refuse everything and have zero false confidence while being useless.
  3. Specificity — clean artifacts graded unsound. Without it, a checker that always says "no" scores perfectly on 1 and 2. This is the repo's own admission rule applied to the experiment.
  4. Cost — wall-clock and tokens per artifact.
  5. Independence, measured as conditional detection lift. For checkers A and B: does B catch A's misses at more than B's own base rate? If yes they are genuinely independent; if B misses precisely what A misses, they share a blind spot regardless of who authored them. This repository currently asserts independence and has never measured it, and this quantity is the closest thing to a definition.

Pre-registered predictions

Frozen before any data. Ordered from the one I most expect to survive to the one I expect to be wrong.

If P1 fails — co-designed checkers detect and mis-certify at the same rates as independent ones — the asymmetry was an artifact of this repository's particular audit being weak, hypothesis C on the futures map loses its evidence, and the "instrument and benchmark" hypothesis loses its most interesting content. That is the outcome to hope for in the sense that matters: it is the one that would teach us the most about how wrong we were.

Cost and cheapest first step

The full factorial is weeks. The cheapest informative slice is days and does not need the factorial:

Take the four hollow batteries that survive the current audit. Have an independent party — a model that has seen neither the audit nor the batteries' authors' reasoning — attempt to identify which of six batteries measure nothing. Compare its detection rate against the audit's 2 of 6.

One number, one afternoon, and it discriminates P1 immediately. If the independent party also gets 2 of 6, independence is not the variable and this whole design is premature.

Relationship to the rest of the tree

This is meta-research, so it lives here rather than in docs/. It borrows the zeta department's and compiler department's batteries as arenas; per harness/README.md's rule, borrowing another department's battery means this is not a department and cannot become one by growing. Results, when they exist, get a docs/ number and a case-log-style disposition — including if the answer is that the asymmetry does not exist.