RecordContract · section of the QIQT-H book

QIQTH.RecordContract

← all sections · ← RaychaudhuriCongruence · RelEntPositivity →

RecordContract · entries 579–581 of 1000

Lemma 579 (shannon_eq_sum_negMulLog).  source ↗

Shannon entropy is a sum of negMulLog of the weights.

S(p)=∑is(p i).nml\href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p})} = \sum_{i s} (p\,i).\mathrm{nml}

Proof. Immediate from the definitions. □\square

Used by shannon_le_log_card, shannon_uniform_eq_log_card.

Lemma 580 (shannon_le_log_card).  source ↗

The information bound H(R) ≤ log|R| (Gibbs/Jensen), machine-checked. For any finite Born record law, the Shannon entropy is at most the log of the record count. This discharges the hinfo hypothesis of area_capacity_bridge concretely — the only genuinely-mathematical (still textbook) step in the contract.

(∀(i:ι),0≤p i)→∑ip i=1→S(p)≤log⁡ (# ι)(\forall (i : \iota), 0 \le p\,i) \to \sum_{i} p\,i = 1 \to \href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({p})} \le \log\,(\#\,\iota)

Proof. By shannon_eq_sum_negMulLog. □\square

Used by clausius_package_from_finite_model, qiqt_gr_ppwave_showcase.

Lemma 581 (shannon_uniform_eq_log_card).  source ↗

Capacity saturation H(R) = log|R| at the maximally-mixed (equilibrium) record. The Jensen/Gibbs bound shannon_le_log_card is an EQUALITY exactly at the uniform distribution p i = 1/|R| — the maximum-entropy state. There the record’s Shannon entropy SATURATES its capacity log|R|. This is the regime where a horizon is in local equilibrium, the state Jacobson assumes when positing the area law. Machine-checked: ∑_{i} negMulLog(1/n) = n·(1/n)·log n = log n.

(S(λx↦((# ι))−1))=log⁡ (# ι)(\href{/browser/qiqth-branchledger#d-qiqth-branchledger-shannon}{S({\lambda x \mapsto {((\#\,\iota))}^{-1}})}) = \log\,(\#\,\iota)

Proof. By shannon_eq_sum_negMulLog. □\square

Used by clausius_package_from_finite_model.

← all sections · ← RaychaudhuriCongruence · RelEntPositivity →