ClausiusFiniteWitness · section of the QIQT-H book

QIQTH.ClausiusFiniteWitness

← all sections · ← ChristoffelSmooth · ClausiusToPernull →

ClausiusFiniteWitness · entries 11–11 of 1000

Lemma 11 (clausius_package_from_finite_model).  source ↗

The Clausius package from the finite QIQT entropy model. Given a finite record set R, a deformation-dependent record law p t (a probability distribution for every t, uniform at the reference t=0), and the holographic area-capacity identification η·Acap = log|R|, the constructed functionals

Sf t := Shannon (p t), KE t := Sf t + KL (p t ‖ p 0), A t := Acap

satisfy the four thermodynamic premises of the QIQT→GR area-law derivation: capacity bound, saturation, relative-entropy positivity, and its tightness at the reference. Each is a direct consequence of the axiom-free finite core (Gibbs/Jensen, uniform saturation, classical Klein).

(∀(t:R)(r:R),0≤p t r)→(∀(t:R),∑rp t r=1)→(p 0=λx↦((# R))−1)→η⋅Acap=log⁡ (# R)→(for t near 0,  S(p t)≤η⋅Acap)∧S(p 0)=η⋅Acap∧(∀(t:R),0≤S(p t)+DKL(p t ∥ p 0)−S(p t))∧S(p 0)+DKL(p 0 ∥ p 0)−S(p 0)=0(\forall (t : \mathbb{R}) (r : R), 0 \le p\,t\,r) \to (\forall (t : \mathbb{R}), \sum_{r} p\,t\,r = 1) \to (p\,0 = \lambda x \mapsto {((\#\,R))}^{-1}) \to \eta \cdot \mathrm{Acap} = \log\,(\#\,R) \to (\text{for }t\text{ near }0,\; \href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p\,t})} \le \eta \cdot \mathrm{Acap}) \wedge \href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p\,0})} = \eta \cdot \mathrm{Acap} \wedge (\forall (t : \mathbb{R}), 0 \le \href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p\,t})} + \href{/browser/qiqth-relentpositivity#d-qiqth-relentpositivity-kl}{D_{\mathrm{KL}}({p\,t}\,\|\,{p\,0})} - \href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p\,t})}) \wedge \href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p\,0})} + \href{/browser/qiqth-relentpositivity#d-qiqth-relentpositivity-kl}{D_{\mathrm{KL}}({p\,0}\,\|\,{p\,0})} - \href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p\,0})} = 0

Proof. By shannon_le_log_card, shannon_uniform_eq_log_card, KL_classical_nonneg. □\square

Used by qiqt_gr_freefield_thermo.

← all sections · ← ChristoffelSmooth · ClausiusToPernull →