Research note 001 / 18 September 2026
What does it take
to close a channel?
A small, exact experiment in making an untrusted worker’s choices invisible to a defined observer.
We combine five digital controls with a thermal model, search every configuration in the catalogue, and check the winning design. The failures are part of the result.
Illustrative model · Declared physical assumptions · No hardware validation
Beyond the thermal example
Air-gapped. Still observable.
Explore 21 channel families, a proposed configuration for nearby observers, and the evidence needed to establish an optimum.
Open the channel prevention field guide →The question that started this
Air gaps still leave physical observations.
“One of them is able to run their CPU really hot, and then the other one can actually detect the temperature change.”
01 / The model
Control what the receiver can observe.
Different authorized answers may still differ. The goal is to remove the worker’s freedom to encode an extra signal inside the same authorized result.
All five are necessary within this catalogue. A simulator switch is a contract to implement, not evidence of an enforced boundary. Read the assumptions ↗
02 / Configuration explorer
A whole search space.
One least-cost answer.
Choose a thermal design to inspect its exact certificate. This slice holds all five digital controls on: 11 attenuation settings × 5 regulation settings.
Numbers inside cells are modeled cost. “Certified” means the stipulated invariant and service floor hold.
Certified · minimum cost
s = 7 / r = 2
- Modeled cost
- 57
- Declared service score
- 90 / 100
- Invariant radius
- 1/20
- Sensor threshold
- 11/200
The radius stays strictly below the threshold. The all-time certificate holds under the declared envelope.
Every configuration, in JSON ↗Why this is optimal
9J = 2(2s + r)² + (s − 4r)² ≥ 512
Feasibility requires 2s + r ≥ 16. Integer cost therefore satisfies J ≥ 57, and the witness reaches 57. Follow the derivation ↗
03 / The instructive failure
Quiet for 23 steps.
Observable at step 24.
Reduce regulation by one unit and the near-miss looks safe until it crosses the sensor threshold. A finite quiet prefix is not an all-time certificate.
At step 24 the hot observation becomes 1; the quiet observation stays 0. The two runs use the same allowed disturbance.
Illustrative temperature deviation, zero initialization. Points are computed with exact fractions; their plotted positions are rounded for display. Raw temperatures also differ in the winning design.
04 / Negative knowledge
Keep the failures.
Make the next attempt better.
Nine replayable records preserve the rejected claims, decisive witnesses, and lessons. They are linked into the Research Kernel ledger.
NK-01A short quiet trace can hide a channel
Rejected claim: 23 equal observations imply all-time equality at s=7,r=1.
Use an all-time invariant. This near-miss first diverges at step 24.
python3 -m unittest -v test_lab.ThermalTests.test_near_miss_at_24_not_23NK-02Raw sensors defeat the observation restriction
Rejected claim: The winner makes raw hot and quiet temperatures indistinguishable.
The guarantee depends on a mediated quantized observer; raw trajectories differ.
python3 -m unittest -v test_lab.ThermalTests.test_quantization_is_essentialNK-03Removing canonical encoding
Rejected claim: Dropping canonical_encoding preserves observation equality.
Retain this control or discharge its exact observation obligation.
python3 -m unittest -v test_lab.DigitalTests.test_five_ablation_witnessesNK-04Removing fixed release slot
Rejected claim: Dropping fixed_release_slot preserves observation equality.
Retain this control or discharge its exact observation obligation.
python3 -m unittest -v test_lab.DigitalTests.test_five_ablation_witnessesNK-05Removing total fallback
Rejected claim: Dropping total_fallback preserves observation equality.
Retain this control or discharge its exact observation obligation.
python3 -m unittest -v test_lab.DigitalTests.test_five_ablation_witnessesNK-06Removing shared resource partition
Rejected claim: Dropping shared_resource_partition preserves observation equality.
Retain this control or discharge its exact observation obligation.
python3 -m unittest -v test_lab.DigitalTests.test_five_ablation_witnessesNK-07Removing mediated egress
Rejected claim: Dropping mediated_egress preserves observation equality.
Retain this control or discharge its exact observation obligation.
python3 -m unittest -v test_lab.DigitalTests.test_five_ablation_witnessesNK-08The certificate depends on the envelope
Rejected claim: The nominal winner remains certified under each tested perturbation.
Re-synthesize after changing bounds. Certificate failure alone is not a physical exploit.
python3 -m unittest -v test_lab.ThermalTests.test_uncertainty_invalidates_original_winnerNK-09Written proof source can fail to compile
Rejected claim: The unmodified archive compiles under Lean 4.19.0.
The base case needed exact Nat.zero_le 50. Statements were preserved; current source passes.
Extract the original archive to a temporary directory and run bash check_lean.sh with Lean 4.19.0.05 / Evidence & scope
Check the result. Know its boundary.
Reproduced and checked
- Exact search and independent optimality certificate
- 34 Python tests, including 65,792 sorting cases
- Lean 4.19.0 kernel check and 24 theorem axiom audits
- Five digital ablations and every default thermal pair
Still open
- Real-valued plant to integer envelope refinement
- Concrete gate, isolation and fallback deadline
- Measured hardware bounds and complete observer map
- Composition with aggregate colluding-worker loads
Reproduce locally
Python 3.10+ · Lean 4.19.0 · No Mathlib
python3 scripts/verify.py
python3 scripts/replay_negative.py --check