# Primary-source provenance

Retrieved September 18, 2026. The optimization parameters were chosen explicitly
for this benchmark; they were not fitted to the following papers or to OpenAI
infrastructure. No unpublished company information was used.

1. **Dwarkesh Podcast, September 17, 2026:** Noam Brown — Agent swarms,
   alignment, & recursive self-improvement.
   https://www.dwarkesh.com/p/noam-brown
   The relevant discussion is near the end of the 01:08:34 chapter, immediately
   before 01:14:12. Brown discusses strengthening sandboxes and says air-gapping
   may not suffice, giving thermal communication as an example. This is not a
   quoted claim that mathematics cannot address containment.

2. **Guri, Monitz, Mirski, and Elovici (2015):** BitWhisper: Covert Signaling
   Channel between Air-Gapped Computers using Thermal Manipulations.
   https://arxiv.org/abs/1503.07919
   The authors' abstract describes adjacent compromised computers, built-in
   thermal sensors, and their tested distance/rate limits. The citation supports
   the existence of that demonstrated thermal channel, not a universal physical
   impossibility theorem or the numerical plant model in this bundle.

3. **Ge, Yarom, Chothia, and Heiser:** Time Protection: the Missing OS Abstraction.
   https://arxiv.org/abs/1810.05345
   Primary research on OS-level time protection and information-flow isolation.

4. **seL4 official verification assumptions.**
   https://sel4.systems/Verification/assumptions.html
   Explicitly distinguishes verified model channels from unmodeled physical and
   timing channels and identifies hardware/boot/other trust assumptions.

5. **seL4 official proof statements.**
   https://sel4.systems/Verification/proofs.html
   Describes isolation, functional/binary correctness, access-control setup,
   and configuration-specific proof coverage.

6. **Lean official language reference: Validating a Lean Proof.**
   https://lean-lang.org/doc/reference/latest/ValidatingProofs/
   Relevant to type/theorem inspection, axiom audits, and kernel checking.
   The latest online manual is not a claim that this bundle uses the latest
   compiler; the source deliberately pins Lean 4.19.0.

7. **Lean official 4.19.0 release.**
   https://github.com/leanprover/lean4/releases/tag/v4.19.0
   Used to identify the pinned compiler distribution. Download attempts did not
   produce a working compiler in the originating environment.

The four supplied P33RL3SS X posts remained inaccessible through the available
retrieval path. Their contents were not inferred or quoted. The Brown passage was
verified through the interviewer's published transcript instead.

Publication update: Lean 4.19.0 was available on the publishing workstation.
The original elaboration failure, statement-preserving repair, and successful
kernel/axiom checks are preserved in `evidence/publication/`. The original
archive retains the compiler-unavailable report from its originating environment.