Holography Gibbs Casini Bound Relative Entropy Nonneg

Relative entropy and its positivity

In probability and information theory, relative entropy, also known as Kullback-Leibler divergence, measures the inefficiency of assuming one probability distribution when the true distribution is another. It is always nonnegative, and it is zero exactly when the two distributions are identical. This is a foundational fact in statistics, machine learning, and physics, where it quantifies the cost of using an approximate model.

The Recognition Science framework, through its machine-checked library of formal theorems, proves this nonnegativity in a finite setting. The declaration relativeEntropy_nonneg establishes that for any two probability distributions over a finite set of possible outcomes, the relative entropy is greater than or equal to zero. The proof is simple: it reduces to the tangent-line bound on the logarithm, log x ≤ x − 1, applied to each outcome and then summed. This is the finite form of the Gibbs inequality, which states that the Shannon entropy of a distribution is at most its cross-entropy with respect to a reference distribution.

This mathematical result is unconditional. It requires only that the first distribution sums to one, that the reference distribution is positive and sums to at most one, and that the number of outcomes is finite. No measure theory, no operator algebra, and no physical assumptions are needed. The framework's library proves it directly from the tangent-line bound, making it a theorem in the strongest sense: axiom-clean and machine-checked.

In the framework's physical application, this inequality becomes a stepping stone. The framework models a physical system as a finite ledger of discrete records, and it uses relative entropy to compare a delivered state against a thermal reference state. The nonnegativity of relative entropy is then the engine behind a conditional derivation of the Bekenstein bound, a limit on the entropy of a physical system. However, that physical assembly carries named model premises: the reference state must be of Gibbs form, the horizon rate must be normalized, and the delivered state's mean energy must be within budget. The positivity of relative entropy itself is unconditional; the physical bound is not.

What this declaration does not claim is equally important. It does not claim that any physical system is thermal, nor does it derive the Gibbs form of the reference state from first principles. It does not extend to continuous systems or to the operator-algebraic setting of Casini's original argument. It proves a purely mathematical inequality about finite probability distributions, and nothing more.

/-- Relative-entropy positivity: the Casini form of the Gibbs inequality. -/
theorem relativeEntropy_nonneg {n : ℕ} (p q : Fin n → ℝ)
    (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 < q i)
    (hp1 : ∑ i, p i = 1) (hq1 : ∑ i, q i ≤ 1) :
    0 ≤ relativeEntropy p q := by
  unfold relativeEntropy
  linarith [gibbs_inequality p q hp hq hp1 hq1]

/-- **Gibbs inequality.** For a probability vector `p` and a positive reference `q`
with `∑ q ≤ 1` (subnormalized allowed): `S(p) ≤ ⟨K_q⟩_p`. This is relative-entropy
positivity, the finite form of Casini's bound. The entire proof reduces to the
tangent-line bound `log x ≤ x − 1` applied per record at `x = q i / p i`. -/
theorem gibbs_inequality {n : ℕ} (p q : Fin n → ℝ)
    (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 < q i)
    (hp1 : ∑ i, p i = 1) (hq1 : ∑ i, q i ≤ 1) :
    shannonEntropy p ≤ crossEntropy p q := by
  -- Per-record tangent bound: p·(log q − log p) ≤ q − p.
  have key : ∀ i : Fin n, p i * (Real.log (q i) - Real.log (p i)) ≤ q i - p i := by
    intro i
    rcases eq_or_lt_of_le (hp i) with h0 | hpi
    · rw [← h0]
      simpa using (hq i).le
    · have hdiv : 0 < q i / p i := div_pos (hq i) hpi
      have hlog : Real.log (q i / p i) ≤ q i / p i - 1 :=
        Real.log_le_sub_one_of_pos hdiv
      have hlogdiv : Real.log (q i / p i) = Real.log (q i) - Real.log (p i) :=
        Real.log_div (ne_of_gt (hq i)) (ne_of_gt hpi)
      have hmul : p i * Real.log (q i / p i) ≤ p i * (q i / p i - 1) :=
        mul_le_mul_of_nonneg_left hlog hpi.le
      have hpne : p i ≠ 0 := ne_of_gt hpi
      have hpq : p i * (q i / p i) = q i := by
        field_simp
      have hcancel : p i * (q i / p i - 1) = q i - p i := by
        calc p i * (q i / p i - 1) = p i * (q i / p i) - p i := by ring
          _ = q i - p i := by rw [hpq]
      calc p i * (Real.log (q i) - Real.log (p i))
          = p i * Real.log (q i / p i) := by rw [hlogdiv]
        _ ≤ p i * (q i / p i - 1) := hmul
        _ = q i - p i := hcancel
  -- Sum the per-record bounds; the mass difference is ≤ 0.
  have hsum : ∑ i, p i * (Real.log (q i) - Real.log (p i)) ≤ ∑ i, (q i - p i) :=
    Finset.sum_le_sum fun i _ => key i
  have hmass : ∑ i, (q i - p i) ≤ 0 := by
    rw [Finset.sum_sub_distrib, hp1]
    linarith
  have hexpand : ∑ i, p i * (Real.log (q i) - Real.log (p i))
      = (∑ i, p i * Real.log (q i)) - ∑ i, p i * Real.log (p i) := by
    rw [← Finset.sum_sub_distrib]
    exact Finset.sum_congr rfl fun i _ => by ring
  have hdiff : (∑ i, p i * Real.log (q i)) - (∑ i, p i * Real.log (p i)) ≤ 0 := by
    rw [← hexpand]
    linarith
  simp only [shannonEntropy, crossEntropy, modularHamiltonian]
  have hneg : (∑ i, p i * -Real.log (q i)) = -(∑ i, p i * Real.log (q i)) := by
    simp [mul_neg]
  rw [hneg]
  linarith

What this page does not claim

The theorem does not claim that any physical system is thermal. The theorem does not derive the Gibbs form of the reference state from first principles. The theorem does not extend to continuous systems or to the operator-algebraic setting of Casini's original argument.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Holography/GibbsCasiniBound.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: