Holography Gibbs Casini Bound Gibbs Reference Pos

A positive reference state

In information theory, a probability distribution assigns a nonnegative number to each possible outcome, and those numbers sum to one. A distribution is called positive if every outcome gets a number strictly greater than zero. The declaration gibbsReference_pos establishes exactly this positivity for a specific kind of reference distribution: one built from a Gibbs state, which assigns probabilities according to the formula q(i) = exp(−β·En(i)). Here β is a positive inverse temperature and En(i) is the energy of record i.

The theorem states that if a reference distribution q has the Gibbs form, then every record i has q(i) > 0. This is a direct consequence of the exponential function always returning a positive number. The proof is immediate: the definition of the Gibbs form, combined with the fact that the exponential of any real number is positive, gives the result. No further assumptions are needed, and the argument works for any finite set of records.

Why does this matter? The Gibbs inequality, a separate theorem in the same framework, bounds the Shannon entropy of any delivered distribution p by the cross entropy against a reference q. That inequality requires the reference to be positive, so gibbsReference_pos supplies a necessary condition for the bound to apply. In the framework's account, the reference state models a thermal equilibrium at inverse temperature β, and the theorem confirms that such a state assigns nonzero weight to every possible record.

In Recognition Science, the framework treats a finite set of records as a ledger, a discrete record of events. The Gibbs reference is a model choice: it assumes the reference state has the thermal form. The theorem does not derive that form from anything more basic; it only states a property that follows once the form is assumed. The positivity result is unconditional mathematics, but the physical interpretation of the reference as a thermal state carries the status of a model premise.

The theorem does not claim that any actual physical system is in a Gibbs state, nor does it derive the Gibbs form from first principles. It also does not address the continuum case of quantum field theory, where the analogous argument requires operator algebra. The result is a small but necessary piece of a larger assembly that aims to prove a Bekenstein-type bound on entropy for all states, not just thermal ones.

/-- A Gibbs reference is automatically positive on every record. -/
theorem gibbsReference_pos {n : ℕ} {q : Fin n → ℝ} {beta : ℝ} {En : Fin n → ℝ}
    (h : GibbsReference q beta En) (i : Fin n) : 0 < q i := by
  rw [h i]
  exact Real.exp_pos _

/-- A Gibbs reference is automatically positive on every record. -/
theorem gibbsReference_pos {n : ℕ} {q : Fin n → ℝ} {beta : ℝ} {En : Fin n → ℝ}
    (h : GibbsReference q beta En) (i : Fin n) : 0 < q i := by
  rw [h i]
  exact Real.exp_pos _

/-- **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 Gibbs form of the reference state is derived from more basic principles. Any actual physical system is guaranteed to be in a Gibbs state. The result extends to the continuum case with operator algebras.

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: