RΛIN / ATO · Evidence Lab 01
When the relationship
does the work.
Two bits. Three possible repairs. A pair can remove dependence that every single repair leaves behind. Change the budget, inspect every candidate and verify the result yourself.
The declared model
History H is a pair of independent fair bits, a and b. The retained summary Z is constant. A mediator M can retain a subset of the three features below.
| H | a | b | Parity |
|---|---|---|---|
| 00 | 0 | 0 | 0 |
| 01 | 0 | 1 | 1 |
| 10 | 1 | 0 | 1 |
| 11 | 1 | 1 | 0 |
A repair passes when H and the future F are conditionally independent given M, for every selected intervention. Acquisition cost and information entropy are different quantities.
Between 0 and 3. Fractions work: try 3/2, then 8/5.
The calculation runs on this device. A pending run can resume after you reload this page.
Ready. Run all eight candidates to find the lowest-cost repair.
| Retained features | Cost | Worst residual (bits) | Exact decision |
|---|---|---|---|
| No run yet. | |||
Inspect the evidence record and failure witnesses
Run the search to create a record.
Local activity
Only these experiment actions are counted on this page. No analytics service receives them.
Formal verification / a separate research branch
A checked algebraic identity
The pointwise mixing identity underlying T8-02 has been checked with Lean 4.35.0 over a general commutative ring:
KV((1−e)v + ea) + KA((1−e)a + ev) − (KVv + KAa) = e(KV−KA)(a−v)
The proof also covers equal-kernel cancellation, equal-density cancellation and preservation of v+a. This certifies the algebraic statements; an integral formulation and physical interpretation require additional assumptions and evidence.
Evidence, scope and interpretation
SAT: a completed search found an allowed repair. UNSAT: a completed search found none in this grammar within the budget. UNKNOWN: the evaluation limit stopped the search before completion.
Decisions use integer cross-products of exact probability weights. The displayed mutual information uses floating-point logarithms and is descriptive. Hashes detect changes to records; they are not signatures or proof of who created a record.
The model’s intervention laws are supplied by construction. This is not identification of a causal effect from observational data, a physical validation or a novelty claim.
Explore context repair · Read the research boundaries · Research Atlas