/-
  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
