12.2. What the formal argument proves🔗

The optima. For the code \Gamma of Lemma T6.2 the Lean shows T_\star(p)\le D(\Gamma)=T(p), and D(\Gamma)\le c\,\mathrm{SE}(q) for every admissible q (Lemmas T6.4 and T6.5); the headline theorems need only these inequalities. Inside the proof of table_of_score, the error of that code is also identified with the frozen optimum, so T_\star(p)=T(p) holds there. No separate theorem states it, and none states \tau_\star=\tau.

The definitions. The frozen Probability, H, Hcond, CMI, StochasticError, DeterministicError and deterministicTable agree with the definitions of TableInformationProof.lean and TableBoundProof.lean definitionally, by unfolding. The kernel checks this when it checks table; no separate lemma states it.

The two claims. Both implications keep the supplied constant c: score_of_table proves TableClaim → ScoreClaim, and table_of_score proves the converse. The converse uses an optimal code (Lemma T6.2), so the attainment of the deterministic optimum and the relabelling of its labels into [N], and the lower bound 0 on every admissible \mathrm{SE}(q); it does not need the stochastic infimum to be attained. So the equivalence remarked in the docstring of ScoreClaim holds in Lean.

Remark (equality of the optima). In fact T_\star(p)=T(p) and \tau_\star(p)=\tau(p) for every finite law p, with T and \tau in bits. First, all four optima are finite and lie below each of their members. Every admissible \mathrm{SE}(q) is a sum of three conditional mutual informations of a probability law, hence nonnegative (stoch_to_det.condMI_nonneg, NaturalLatents/Upstream/Entropy.lean, after latentError_eq_core). Every latent error is nonnegative (stoch_to_det.Latent.score_nonneg, NaturalLatents/Upstream/Functionals.lean), and T_\star is an infimum over finitely many codes. Every code g into [N] defines a deterministic latent of error D(g), and D(g)=\mathrm{DE}(t_{p,g}) by the table identification in the description of Lemma T6.5, stated there for every code; so T(p)\le T_\star(p), and T_\star(p)\le T(p) by the first paragraph of this section. An admissible q, with its slots reordered, is the joint law of a latent of error \mathrm{SE}(q) by Lemmas T6.3 and T6.5, so \tau(p)\le\tau_\star(p). Conversely, a latent whose label set has k elements becomes an admissible table on A\times B\times[k] once its labels are numbered; a one-to-one renaming of labels changes no entropy, so its error is that table's \mathrm{SE}, and \tau_\star(p)\le\tau(p).