# Landauer Frontier — Lean formalization

Machine-checked core of *The Thermodynamic Cost of Answering* (draft v0.3).
Lean 4 (`v4.30.0`) + Mathlib `v4.30.0`.

## What this formalizes

The paper's main theorem is: a cyclic, steady-state agent answering queries
`Q ~ D` at accuracy `a`, through a one-way read-only query interface and a
copy-semantics output interface, dissipates at least `kT ln2 · R_D(a)` of heat
per query, where `R_D(a)` is the task's rate–distortion function.

This file (`LandauerFrontier.lean`) machine-checks the **algebraic and
information-theoretic skeleton** of that proof — precisely the parts three
human referees verified by hand:

| Result (Lean name)        | Statement                                                        |
|---------------------------|------------------------------------------------------------------|
| `definitional_converse`   | `R = sInf(feasible rates)`, all `≥ 0`, `IQY` feasible ⟹ `R ≤ IQY` |
| `landauer_general`        | general bound `Qdiss ≥ kT·ln2·(R − H(Ŷ|A₂))` (Remark, no A5)      |
| `landauer_main`           | main theorem `Qdiss ≥ kT·ln2·R` under copy-semantics (A5)         |
| `landauer_finite_time`    | `Qdiss ≥ kT·ln2·R + kT·excess` (Shiraishi–Funo–Saito term)        |
| `landauer_familiar`       | correlated queries: `Qdiss ≥ kT·ln2·(R − I(A₀;Q))`               |

The machine checks:
- the **telescoping cancellation** of the three phase inequalities (a hand
  sign-error would hide here) — verified by `ring`;
- the **boundary identities** (fresh queries, blank output register, chain
  rule, steady state) feeding that cancellation;
- the **data-processing + converse** chain `R ≤ I(Q;Ŷ) ≤ I(A₁;Q)`;
- the **definitional converse** `R ≤ I(Q;Ŷ)` proved outright from Mathlib's
  `csInf_le` — this is the paper's "no coding theorem is used" claim, reduced
  to the defining property of an infimum;
- all **sign conditions** (`kT > 0`, `ln 2 > 0`) needed to preserve the
  inequalities under multiplication.

## What is a HYPOTHESIS (not proved here)

Honesty about the boundary, following standard practice for formalizing
physics. Mathlib `v4.30` has no theory of Markov-jump entropy production, so:

- **The three per-phase second-law inequalities** `pM, pE, pR` are hypotheses.
  Their physical origin is Lemma 1 of the paper (Esposito–Van den Broeck;
  Parrondo–Horowitz–Sagawa). Formalizing them would require building
  stochastic thermodynamics in Lean — a separate, multi-month project.
- **The data-processing inequality** `hdpi : I(Q;Ŷ) ≤ I(A₁;Q)` is a
  hypothesis (standard; not cleanly available in Mathlib v4.30).
- The entropies, heats, and rate are abstract reals constrained by the stated
  identities; they are not built from a probability space.

So this is a *conditional* formalization: **given** the physical second law in
per-phase form and the standard DPI, the bookkeeping and the definitional
converse are correct, with certainty. That is exactly the layer where a
hand-proof could have erred — and now cannot.

## Build

The project pins the same toolchain/Mathlib as a sibling project on disk. The
fast path that avoids re-fetching or rebuilding Mathlib is to type-check the
file against an already-built Mathlib:

```
# inside a project whose Mathlib v4.30.0 is already built:
lake env lean LandauerFrontier.lean   # no output = success
```

For a standalone build, `lake exe cache get` (restores prebuilt oleans keyed
to the Mathlib rev) followed by `lake build` is far faster than a cold compile.
Do **not** populate `.lake/packages` by copying another project's tree: lake
re-verifies on changed mtimes and Windows Defender scans every olean.