# Researcher and mathematician handoff

This is an independent, bounded research benchmark inspired by Noam Brown of
OpenAI's discussion of air gaps and temperature sensors in the
[September 17, 2026 Dwarkesh interview](https://www.dwarkesh.com/p/noam-brown).
The results page carries the exact attributed quotation. The model's numbers
were chosen for this benchmark; they were not measured at OpenAI or fitted to
BitWhisper. No endorsement or unrestricted containment result is implied.

## Broader deployment continuation

The user-selected focus is **air-gapped computers with nearby observers**.
[CHANNELS.md](CHANNELS.md) defines the broader joint observation contract, a
21-family inventory, a proposed architecture and three new work packets for
researchers and mathematicians. Its deployment optimum is undetermined.
Run `python3 scripts/verify_coverage.py` for the eight new tests and four exact
counterexamples. These do not extend the scope of the original Lean theorems.

Continue run `covert-channel-lab-coverage-20260918` for this expansion. Its
[report](research/coverage/kernel-report.json),
[events](research/coverage/kernel-events.json), and
[frontier](research/coverage/kernel-frontier.json) are separate from the original
publication run. Both preserve negative and inconclusive knowledge.

## Start here

1. Read [CONTRACTS.md](CONTRACTS.md) before interpreting a result as security.
2. Read [MATH.md](MATH.md) for the model, quantifiers, invariant and cost identity.
3. Run `python3 scripts/verify.py`. Python 3.10+ and Lean 4.19.0 are required;
   there are no Python packages or Mathlib dependencies. `--python-only` leaves
   Lean explicitly unchecked. Receipts and logs go to `_verification/`.
4. Run `python3 scripts/replay_negative.py` to recover the negative witnesses.
5. Read [the kernel report](research/kernel-report.json),
   [negative knowledge](research/negative-knowledge.json), and the work packets below.
6. Record `git rev-parse HEAD`, environment, exact command, exit status, source
   hashes, assumptions and falsifier for every continuation. Use a new branch.

## What is established

The exact Python search enumerates 1,760 configurations and finds 19 feasible
ones in the declared model. The unique cost minimizer is `(s,r)=(7,2)`, cost 57,
declared service score 90. The identity
`9(s²+2r²) = 2(2s+r)² + (s−4r)²` gives an integer lower bound of 57;
the winner attains it. The all-natural-number lower bound, integer envelope,
abstract release and trace properties, digital negative controls, and exact
near-miss arithmetic kernel-check in Lean 4.19.0.

The original archive is immutable in `evidence/original/`. Its proposed Lean
source failed to compile. The publication changes one proof term, with no change
to its statement. Both the failure and successful axiom audit remain in
`evidence/publication/`. The archive's compiler-unavailable status is historical.

## Research Kernel protocol

Stable run ID: `covert-channel-lab-publication-20260918`.
`research/kernel-report.json` and `research/kernel-events.json` export the live
MCP run. Two scoped claims passed the SUPPORT gate; five shortcut hypotheses
passed the REFUTED gate using nine negative records. The raw report also lists
five COUNTEREXAMPLE atoms under REFUTED; these are witness records, not five
additional rejected hypotheses. Initial gate rejections are retained in the
event export, along with their later evidence-backed resolutions.

Researchers without that service can continue the portable
`research/continuations.jsonl` journal and submit it with their artifacts.

1. **Contract:** write one typed claim with explicit quantifiers, model/version,
   dependencies, observer map, authority impact, budget and a concrete falsifier.
2. **Retrieve:** search existing claims, failures and contradictions. Resume the
   stable run; reuse or supersede a claim instead of silently rewriting history.
3. **Propose:** add a QUESTION, CLAIM/HYPOTHESIS and RISK; link dependencies.
   Morph and theorem retrieval only suggest candidates. Record selected and
   rejected suggestions with reasons.
4. **Refute:** register a test before promotion. Save the smallest counterexample,
   exact parameters, both observations, and replay command. A timeout, missing
   tool or inconclusive search is UNKNOWN, not a counterexample or proof.
5. **Check:** run an independent deterministic checker appropriate to the claim.
   Attach source hashes, logs, exit codes and provenance. A benchmark can support
   a bounded claim; it cannot silently discharge a universal quantifier.
6. **Promote:** retrieve contradictions again. Call `rk_promote` only with support,
   reviewed dependencies, a refutation attempt, reproducible evidence and a
   concise rationale. Preserve rejections and missing gates. `SUPPORTED` is a
   local ledger status; the attached checker determines what was actually proved.
7. **Handoff:** export `rk_report` and `rk_frontier`, append a continuation record,
   and state the strongest supported claim, remaining gaps and next falsifier.

Do not overwrite a failed experiment to make a successful rerun look original.
Use `supersedes` to connect repaired results while retaining the failed artifact.
Do not promote physical security because Python or Lean passed.

## Negative knowledge worth reusing

| Rejected shortcut | Decisive observation | Consequence |
|---|---|---|
| 23 equal time steps establish safety | `(7,1)` diverges at step 24 | Use an all-time invariant; finite prefixes can hide leakage. |
| A safe quantized output protects raw sensors | `(7,2)` has distinct raw hot/quiet temperatures | Sensor mediation is a premise, not a cosmetic interface. |
| One digital control can be dropped | Each of five ablations changes an observable coordinate | Keep canonicalization, release slots, fallback, partition and egress together. |
| The nominal optimum survives changed bounds | Each tested perturbation invalidates its certificate | Re-synthesize under new conservative bounds. |
| Plausible Lean source is a checked proof | The original base case fails elaboration | Compile and audit the exact published source. |

These failures are scoped. Losing an invariant certificate under a changed model
is not automatically a demonstrated physical attack. The original Lean failure
refutes a compilation claim, not the mathematical theorem.

## Work packet M1: real-valued refinement (mathematician)

**Question:** under the stated signed bounds and `|theta[0]| <= 1/20`, construct
a generalized integer envelope `M` with `M[0]=50`,
`M[t+1]=ceil((9 M[t]+10(g+1))/10)`, and prove
`1000 |theta[t]| <= M[t] <= 50` for `g<=4`. The current concrete `envelope`
starts at zero: use it only with zero initialization. The existing generalized
invariant accepts any initial bound at most 50.

**Dependencies:** pinned Lean environment; a deliberate exact rational or real
representation; signed triangle inequality; ceiling monotonicity and scaling;
explicit observer threshold and initialization. If Mathlib is introduced, pin
the toolchain and dependency commit in a separate change and document the shift.

**Falsifiers first:** wrong rounding direction, `|theta[0]|>1/20`, threshold
equality, negative disturbances, time-varying cooling coefficients, and combined
load exceeding the bound. Do not strengthen premises invisibly to make the proof
pass. Separate `M<=50` from the strict observation conclusion `50<55`.

**Deliverable:** a named refinement theorem, assumption mapping to `Thermal`,
boundary counterexamples, axiom audit and independent replay. Success closes
only the mathematical refinement obligation; no hardware claim follows.

## Work packet R1: concrete release gate (researcher)

Specify a bounded plain-integer byte format, canonical answer, sound private
verifier and total fallback. The Python sorting function demonstrates the result
semantics; it is not an isolated or constant-time implementation.

**Attack cases:** withholding, malformed inputs, proof floods, worst-case fallback,
observable checking work, retries, output length and scheduler contention.
**Deliverable:** implementation-to-spec refinement, resource and deadline bounds,
and a complete observable-state test harness. A fast average-case benchmark does
not discharge worst-case fallback or persistent resource isolation.

## Work packet R2: physical and compositional scope (researcher)

Design a measurement protocol for conservative load, disturbance, cooling and
initialization bounds. List every receiver-visible path, including clocks,
fans, throttling, billing/logs, radio, acoustics and raw sensors. Combine colluding
workers under an aggregate actuation bound. No real-device experiments are
included in this publication.

**Falsifier:** one omitted observable or admitted state outside the envelope.
**Deliverable:** dated calibration data, uncertainty treatment, observer/actuator
inventory, multi-worker composition assumptions and re-optimized configurations.
Do not treat an absence of observed leakage as proof of absent channels.

## Work packet M2: generalized optimization (mathematician)

Generalize attenuation, regulation, utility floor or cost weights while preserving
the old benchmark as a regression case. State the new integer domain and which
properties are necessary, sufficient, or both. Derive an independently checkable
lower bound or return an explicit optimality gap. Inspect quantizer-boundary and
zero-gain cases. A best value in a finite search is insufficient unless the
outside-domain dominance argument is also supplied.

## Retrieval record

TheoremSearch supplied retrieval-only prior art. The promoted claim depends
only on the independently checked local evidence listed in the kernel report.
The two semantic searches are saved under `research/retrieval/`; results were
adjacent or low-signal and were not used as mathematical premises. The formal
graph request timed out; no formal-corpus coverage is claimed. Morph returned
generic contract and counterexample suggestions; neither is a new theorem.

## Contribution record

Append one JSON object per experiment to `research/continuations.jsonl` using
`research/continuation-template.json`. Include negative and inconclusive outcomes.
Use a stable unique ID and a prior ID in `supersedes` for corrections. Attach
artifacts to the commit and link them in the kernel. Keep hidden reasoning,
credentials and unrelated personal data out of the public ledger.