4.1. 1. Setting🔗

Units. Units and conventions are those of section 0 of the contact page: all entropies and mutual informations on this page are in nats, and every logarithm is natural. The race calculation concerns B,d,h,j(a); the optima used in the introductory assembly discussion are defined in section 0 of the contact page. Neither d nor j(a) is divided by \ln2 in its definition.

Notation. Let X,Y be finite alphabets and p a probability law on X\times Y. Let \mathcal I = \{1, \ldots, n\} with n \ge 1. A finite latent is a joint law of Z = (X,Y) and L \in \mathcal I. On the support of Z, write p(z) = \Pr(Z = z) > 0, r_z(i) = \Pr(L = i \mid Z = z) > 0 and \pi_i = \sum_z p(z)\, r_z(i) > 0. Each row and the prior sum to one. A seeded map is a deterministic map A_e : \mathrm{supp}\,p \to \mathcal I for each seed e, with the seed independent of Z. Calibration means \Pr_E(A_E(z) = i) = r_z(i). The entropy H, the relative entropy D(r\Vert\pi)=\sum_ir_i\ln(r_i/\pi_i), the budget B=I(L;X\mid Y)+I(L;Y\mid X) and the posterior mismatch d=\sum_zp(z)\left(1-\sum_ir_z(i)^2\right) are those of (D2) and (D3). Define

h=\mathbb E_E\left[H(A_E(Z)\mid X)+H(A_E(Z)\mid Y)\right],\qquad j(a)=a\ln\Gamma(1-1/a)-\gamma_E . \qquad \text{(R1)}

In the definition of h, entropy is taken over Z with E = e held fixed, then averaged over E. Equivalently the two terms are H(A_E(Z) \mid X, E) and H(A_E(Z) \mid Y, E) on the joint probability space. Here \gamma_E is Euler's constant. Some letters are reused locally and are unrelated to the notation T(p) and D_p(f) of section 0: in Lemma R4 the letter T is the minimal scaled clock time; in Lemma R1 the letters D_k and B_\ell are exponential variables and sets; from Lemma R5 on, J_i, S_i, S and Q are the reference masses and the reference of (R8), unrelated to the quartic moment J and the support S of the contact page; N is the Poisson process in Lemma R1 and the limit index in Lemma R3; M in the proof of Lemma R2 is an interval endpoint, not the budget M; b in Lemma R3 and \alpha=1/a in Lemmas R7 and R8 are scalars, not the quadratic b of (A2.1) or the coefficient \alpha of the pair-charge page; s, v, w and y are integration or transform variables, s not the separation; G=\Gamma(1-\alpha) in Lemma R8 and the Gumbel coordinates G_i are not the profile G(s) of the pair-charge page; and \Phi_a in (R12) is not the component functional of the setup page. The random map F, the posterior r_z, B, d, h and j(a) are the shared objects of section 0 of the contact page and of (R1).

Lean: gammaPrice (j), seedEntropy (h), mismatch (d) and CalibratedSeededFamily (NaturalLatents/General/Definitions.lean). A calibrated family is a probability law on complete maps from X\times Y to the labels, calibrated at every cell of the support, and seedEntropy is the seed average of the fixed-map conditional entropies, the form (L7) of the ledger, each the bit-valued conditional entropy converted by condHNat (NaturalLatents/General/Nats.lean). The function gammaPrice uses Mathlib's Real.Gamma and Real.eulerMascheroniConstant.