/- The Thermodynamic Cost of Answering — machine-checked core. This file formalizes the ALGEBRAIC and INFORMATION-THEORETIC skeleton of the main theorem of `landauer_frontier.tex` (draft v0.3): the entropy bookkeeping, the phase telescoping, the data-processing step, and — proved outright from Mathlib — the *definitional* rate–distortion converse. WHAT IS A HYPOTHESIS vs WHAT IS PROVED -------------------------------------- The stochastic-thermodynamics content (the per-phase second law) is NOT formalized here; Mathlib has no theory of Markov-jump entropy production at v4.30. Following the standard practice for formalizing physics, the three per-phase second-law inequalities enter as HYPOTHESES `pM, pE, pR` (their physical origin is Lemma 1 of the paper). Likewise the data-processing inequality `hdpi` (standard; not cleanly in Mathlib v4.30) is a hypothesis. Everything else — the boundary identities, the telescoping cancellation (where a hand sign-error would hide), the sign conditions, and the converse `R ≤ I(Q;Ŷ)` from the DEFINITION of R as an infimum (the paper's "no coding theorem is used" claim) — is machine-checked below. Naming mirrors the paper: H0A,H1A,H2A,H3A H(A) at t0..t3 (marginal agent entropy) H0AgQ,H1AgQ H(A|Q) at t0,t1 (conditional) H1AO,H2AO H(A,O) at t1,t2 (joint with output register) Hcond H(Ŷ | A(t2)) (0 under copy-semantics, A5) IQY I(Q;Ŷ) kT = k_B T, L = ln 2 -/ import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Tactic.Linarith import Mathlib.Tactic.Ring import Mathlib.Tactic.NormNum set_option maxHeartbeats 400000 namespace LandauerFrontier /-- ln 2 is positive. Used to preserve inequalities under `· * ln 2`. -/ theorem log_two_pos : (0 : ℝ) < Real.log 2 := Real.log_pos (by norm_num) /-- **Definitional rate–distortion converse.** If `R` is the infimum of the set of mutual-information rates achievable by feasible channels (all nonnegative, so the set is bounded below), then any feasible channel's rate `IQY` is at least `R`. This is the paper's claim that the converse needs no coding theorem: it is `csInf_le`, the defining property of an infimum. -/ theorem definitional_converse (feasibleRates : Set ℝ) (R IQY : ℝ) (hR : R = sInf feasibleRates) (hlb : ∀ x ∈ feasibleRates, 0 ≤ x) (hmem : IQY ∈ feasibleRates) : R ≤ IQY := by have hbdd : BddBelow feasibleRates := ⟨0, fun a ha => hlb a ha⟩ rw [hR] exact csInf_le hbdd hmem /-- **General bound (Remark, without copy-semantics).** From the three per-phase second-law inequalities, the boundary identities (fresh queries `a1`, blank output register `blank`, chain rule `chain`, steady state `a4`), the data-processing inequality `hdpi`, and the converse `hRle`, the per-cycle heat obeys `Qdiss ≥ kT · ln2 · (R − H(Ŷ|A(t2)))`. The telescoping cancellation is checked by `ring`; the sign handling by `linarith` / `mul_le_mul_of_nonneg_left`. -/ theorem landauer_general (kT L Qdiss QM QE QR : ℝ) (H0A H1A H2A H3A H0AgQ H1AgQ H1AO H2AO Hcond IQY R : ℝ) (hkT : 0 < kT) (hL : L = Real.log 2) (hQdiss : Qdiss = QM + QE + QR) (pM : QM ≥ kT * L * (H0AgQ - H1AgQ)) (pE : QE ≥ kT * L * (H1AO - H2AO)) (pR : QR ≥ kT * L * (H2A - H3A)) (a1 : H0AgQ = H0A) -- (A1) fresh queries (blank : H1AO = H1A) -- blank output register at t1 (chain : H2AO = H2A + Hcond) -- chain rule; Hcond = H(Ŷ|A(t2)) (a4 : H3A = H0A) -- (A4) steady state (hdpi : IQY ≤ H1A - H1AgQ) -- data processing: I(Q;Ŷ) ≤ I(A₁;Q) (hRle : R ≤ IQY) -- definitional converse : Qdiss ≥ kT * L * (R - Hcond) := by have hc : 0 < kT * L := by rw [hL]; exact mul_pos hkT log_two_pos -- sum of the three phase inequalities (linear in the product atoms) have hsum : Qdiss ≥ kT * L * (H0AgQ - H1AgQ) + kT * L * (H1AO - H2AO) + kT * L * (H2A - H3A) := by rw [hQdiss]; linarith [pM, pE, pR] -- telescoping cancellation, verified by ring after substituting identities have hfac : kT * L * (H0AgQ - H1AgQ) + kT * L * (H1AO - H2AO) + kT * L * (H2A - H3A) = kT * L * ((H1A - H1AgQ) - Hcond) := by rw [a1, blank, chain, a4]; ring have hstep : Qdiss ≥ kT * L * ((H1A - H1AgQ) - Hcond) := by linarith [hsum, hfac] -- R ≤ I(Q;Ŷ) ≤ I(A₁;Q) = H1A - H1AgQ have hRfull : R ≤ H1A - H1AgQ := le_trans hRle hdpi have hmono : kT * L * (R - Hcond) ≤ kT * L * ((H1A - H1AgQ) - Hcond) := mul_le_mul_of_nonneg_left (by linarith) (le_of_lt hc) linarith [hstep, hmono] /-- **Main theorem (Landauer frontier for answering).** Under copy-semantics emission (A5: `Hcond = 0`), the per-cycle heat obeys `Qdiss ≥ kT · ln2 · R`. -/ theorem landauer_main (kT L Qdiss QM QE QR : ℝ) (H0A H1A H2A H3A H0AgQ H1AgQ H1AO H2AO IQY R : ℝ) (hkT : 0 < kT) (hL : L = Real.log 2) (hQdiss : Qdiss = QM + QE + QR) (pM : QM ≥ kT * L * (H0AgQ - H1AgQ)) (pE : QE ≥ kT * L * (H1AO - H2AO)) (pR : QR ≥ kT * L * (H2A - H3A)) (a1 : H0AgQ = H0A) (blank : H1AO = H1A) (chain : H2AO = H2A + 0) -- (A5) copy-semantics: H(Ŷ|A₂)=0 (a4 : H3A = H0A) (hdpi : IQY ≤ H1A - H1AgQ) (hRle : R ≤ IQY) : Qdiss ≥ kT * L * R := by have h := landauer_general kT L Qdiss QM QE QR H0A H1A H2A H3A H0AgQ H1AgQ H1AO H2AO 0 IQY R hkT hL hQdiss pM pE pR a1 blank chain a4 hdpi hRle simpa using h /-- **Finite-time frontier.** With the read-phase second law strengthened by a nonnegative excess term (the Shiraishi–Funo–Saito speed-limit contribution `kT · excess`, `excess = ℓ*²/(2N) ≥ 0`), the bound gains that term: `Qdiss ≥ kT · ln2 · R + kT · excess`. -/ theorem landauer_finite_time (kT L Qdiss QM QE QR excess : ℝ) (H0A H1A H2A H3A H0AgQ H1AgQ H1AO H2AO IQY R : ℝ) (hkT : 0 < kT) (hL : L = Real.log 2) (_hexc : 0 ≤ excess) -- SFS term is nonnegative; this makes the bound a -- STRENGTHENING of the main theorem, but the -- inequality below is valid for any `excess`. (hQdiss : Qdiss = QM + QE + QR) (pM : QM ≥ kT * L * (H0AgQ - H1AgQ) + kT * excess) -- strengthened read phase (pE : QE ≥ kT * L * (H1AO - H2AO)) (pR : QR ≥ kT * L * (H2A - H3A)) (a1 : H0AgQ = H0A) (blank : H1AO = H1A) (chain : H2AO = H2A + 0) (a4 : H3A = H0A) (hdpi : IQY ≤ H1A - H1AgQ) (hRle : R ≤ IQY) : Qdiss ≥ kT * L * R + kT * excess := by have hc : 0 < kT * L := by rw [hL]; exact mul_pos hkT log_two_pos have hsum : Qdiss ≥ kT * L * (H0AgQ - H1AgQ) + kT * excess + kT * L * (H1AO - H2AO) + kT * L * (H2A - H3A) := by rw [hQdiss]; linarith [pM, pE, pR] have hfac : kT * L * (H0AgQ - H1AgQ) + kT * L * (H1AO - H2AO) + kT * L * (H2A - H3A) = kT * L * (H1A - H1AgQ) := by rw [a1, blank, chain, a4]; ring have hRfull : R ≤ H1A - H1AgQ := le_trans hRle hdpi have hmono : kT * L * R ≤ kT * L * (H1A - H1AgQ) := mul_le_mul_of_nonneg_left hRfull (le_of_lt hc) linarith [hsum, hfac, hmono] /-- **Familiarity corollary.** When the agent already holds `I0 = I(A(t0);Q)` bits about the incoming query (fresh-query identity `a1` replaced by `a1' : H0AgQ = H0A - I0`), the floor drops by exactly `kT · ln2 · I0`: `Qdiss ≥ kT · ln2 · (R − I0)`. -/ theorem landauer_familiar (kT L Qdiss QM QE QR I0 : ℝ) (H0A H1A H2A H3A H0AgQ H1AgQ H1AO H2AO IQY R : ℝ) (hkT : 0 < kT) (hL : L = Real.log 2) (hQdiss : Qdiss = QM + QE + QR) (pM : QM ≥ kT * L * (H0AgQ - H1AgQ)) (pE : QE ≥ kT * L * (H1AO - H2AO)) (pR : QR ≥ kT * L * (H2A - H3A)) (a1' : H0AgQ = H0A - I0) -- agent holds I0 about Q (blank : H1AO = H1A) (chain : H2AO = H2A + 0) (a4 : H3A = H0A) (hdpi : IQY ≤ H1A - H1AgQ) (hRle : R ≤ IQY) : Qdiss ≥ kT * L * (R - I0) := by have hc : 0 < kT * L := by rw [hL]; exact mul_pos hkT log_two_pos have hsum : Qdiss ≥ kT * L * (H0AgQ - H1AgQ) + kT * L * (H1AO - H2AO) + kT * L * (H2A - H3A) := by rw [hQdiss]; linarith [pM, pE, pR] have hfac : kT * L * (H0AgQ - H1AgQ) + kT * L * (H1AO - H2AO) + kT * L * (H2A - H3A) = kT * L * ((H1A - H1AgQ) - I0) := by rw [a1', blank, chain, a4]; ring have hstep : Qdiss ≥ kT * L * ((H1A - H1AgQ) - I0) := by linarith [hsum, hfac] have hRfull : R ≤ H1A - H1AgQ := le_trans hRle hdpi have hmono : kT * L * (R - I0) ≤ kT * L * ((H1A - H1AgQ) - I0) := mul_le_mul_of_nonneg_left (by linarith) (le_of_lt hc) linarith [hstep, hmono] end LandauerFrontier