01 / Reproduction
Start from a checked baseline.
Clone the repository, record its commit, and replay the results. Python 3.10+ and Lean 4.19.0 are sufficient; the lab uses no Python packages or Mathlib.
git clone https://github.com/TheDarkLightX/CovertChannelLab.git
cd CovertChannelLab
git rev-parse HEAD
python3 scripts/verify.py
python3 scripts/replay_negative.py --check
python3 scripts/verify_coverage.pyWithout Lean, use --python-only. Its receipt explicitly records Lean as NOT_RUN. Logs and fresh receipts go to _verification/.
The original archive is preserved. Its proposed Lean proof failed in one initial-state case. The publication repairs the proof term without changing its statement, and preserves both the failure and the successful check.
Inspect the publication receipt ↗02 / Research Kernel protocol
A failure is a result with a scope.
Use the stable run covert-channel-lab-publication-20260918, or continue the portable journal included in the repository. The export captures claims, dependencies, refutation attempts, witnesses and unresolved questions.
- State the contract. Specify quantifiers, assumptions, the observer, dependencies, a budget and an explicit falsifier.
- Retrieve before repeating. Search earlier failures and contradictions. Keep stable IDs and supersede corrected claims.
- Try to break it. Register the smallest decisive test. Save both observations and the exact replay command.
- Attach the checker. Preserve source hashes, environment, stdout and exit code. Retrieval and model suggestions are proposals.
- Promote only within scope. Recheck contradictions and dependencies. Keep any rejected gate and its missing evidence.
- Leave a handoff. Export the report and frontier, append an experiment record, and identify the next falsifier.
All nine negative records include lessons and replay instructions. The formal-corpus lookup timed out; semantic search hits were adjacent or low-signal and did not become premises.
03 / Open work
Choose a boundary to investigate.
covert-channel-lab-coverage-20260918. The deployment optimum remains undetermined.The original benchmark also retains the following open work:
M1 · Mathematician · First priority
Connect the real recurrence to the integer envelope.
Prove the signed real-valued dynamics refine an upward-rounded natural-number bound. Make initialization explicit: the existing concrete envelope starts at zero; a nonzero initial condition needs a generalized envelope.
Break it with: downward rounding, threshold equality, negative disturbances, time-varying cooling, or aggregate load outside the bound.
Done when: a named Lean refinement theorem, assumption map, boundary examples and axiom audit are independently replayable.
R1 · Researcher
Refine a concrete release gate.
Define the bounded byte format, canonical answer, private verifier, total fallback and public deadline. The Python sorting example establishes functional behavior only.
Break it with: withholding, malformed proposals, proof floods, variable checking work, retries or scheduler contention.
Done when: the implementation refines the abstract release theorem, including worst-case resources and every observable effect.
R2 · Researcher
Validate the physical observation contract.
Measure conservative envelope parameters and account for every receiver-visible path. Include raw sensors, clocks, fans, throttling, logs and colluding workers.
Break it with: a missing observable or a permitted state outside the assumed envelope.
Done when: calibration evidence, uncertainty bounds, observer inventory and multi-worker assumptions are explicit and reviewed.
M2 · Mathematician
Generalize the optimum.
Change cost weights, utility floors or control curves while retaining the original case as a regression. Distinguish necessary conditions from sufficient certificates.
Break it with: a cheaper feasible integer witness, an unhandled boundary, or an outside-catalogue design.
Done when: an independent certificate proves the new bound, or the result reports a remaining optimality gap.
04 / Interpretation
Let the evidence set the claim.
| Evidence | What it establishes |
|---|---|
| Exact Python replay | Reproducible outputs and bounded checks for the declared model. |
| Lean kernel check | The stated abstract theorems under their explicit premises. |
| Research Kernel SUPPORTED | A local ledger gate passed. Inspect its attached evidence and scope. |
| Physical containment | Not established. Refinement, complete observations and measured hardware contracts remain open. |
This independent lab is inspired by Noam Brown of OpenAI’s published remarks. It does not attribute an impossibility theorem to him or imply an endorsement.
Append a continuation record for positive, negative and inconclusive work. Preserve old evidence, link a correction through supersedes, and submit the artifacts with the source change.