Natural latents: a bound below seven

12.1. 6. From latents to probability tables🔗

The frozen definitions. Let A,B be finite alphabets, N=\lvert A\times B\rvert, and [N]=\{0,\ldots,N-1\}. Statement.lean works with real tables and logarithms to base two. A table p is a probability law if it is nonnegative with total one (Probability). For tables of the appropriate shapes,

\begin{aligned} H(p)&=-\sum_ap(a)\log_2p(a),\qquad H(U\mid W)=H(p_{UW})-H(p_W),\qquad I(U;V\mid W)=H(p_{UW})+H(p_{VW})-H(p_{UVW})-H(p_W),\\ \mathrm{SE}(q)&=I(X;Y\mid V)+I(V;X\mid Y)+I(V;Y\mid X),\qquad \mathrm{DE}(t)=I(X;Y\mid\Gamma)+H(\Gamma\mid X)+H(\Gamma\mid Y),\\ t_{p,g}(x,y,\ell)&=p(x,y)\,\mathbf 1_{\{g(x,y)=\ell\}},\qquad T_\star(p)=\min_{g:A\times B\to[N]}\mathrm{DE}(t_{p,g}),\qquad \tau_\star(p)=\inf_{k,\,q}\mathrm{SE}(q), \end{aligned} \qquad \text{(T6.A)}

where every marginal is a table sum, \mathrm{SE} is StochasticError, \mathrm{DE} is DeterministicError, t_{p,g} is deterministicTable p g, and the infimum in \tau_\star is over k\in\mathbb N and probability laws q on A\times B\times[k] with (X,Y)-marginal p; call such q admissible. For a law r on K\times(A\times B), with K finite, \mathrm{SE}(r) is the same sum of three conditional mutual informations, with V in the first slot. TableClaim asks for one code g, depending on p only, with \mathrm{DE}(t_{p,g})\le c\,\mathrm{SE}(q) for every such q; ScoreClaim asks for T_\star(p)\le c\,\tau_\star(p). Inside the proof, T and \tau are the bit-valued stoch_to_det.T and stoch_to_det.tau (NaturalLatents/Upstream/Functionals.lean), that is, the optima of (D3) on the contact page divided by \ln2 (D1): \tau is an infimum over latents with any finite label type, and T an infimum over deterministic latents, those in which each cell has positive joint mass with at most one label. On this page \Gamma is a code, not the Gamma function of the race page; A,B are alphabets, not the budget B; and K is a finite label set, not the replica budget K.

Theorem12.1.1
Group: The table form. (5)
Group member previews
Preview
Theorem 12.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 10.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagskernel-verified

Lemma T6.1 (bits and nats). For every finite law p, T(p)\le c\,\tau(p) in bits.

Lean code for Theorem12.1.1●4 theorems
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.T_le_c_mul_tau {α β : Type} [Fintype α] [Fintype β]
  [DecidableEq α] [DecidableEq β] {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p) :
  stoch_to_det.T p ≤ NaturalLatents.c * stoch_to_det.tau p
    theorem NaturalLatents.T_le_c_mul_tau {α β : Type}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p) :
  stoch_to_det.T p ≤
    NaturalLatents.c * stoch_to_det.tau p
    The optimum form in bits, over bundled latents.
  • theoremdefined in NaturalLatents/General/Nats.lean
    complete
    theorem NaturalLatents.General.bits_of_nats {x y c : ℝ}
  (h :
    NaturalLatents.General.nats x ≤ c * NaturalLatents.General.nats y) :
  x ≤ c * y
    theorem NaturalLatents.General.bits_of_nats
  {x y c : ℝ}
  (h :
    NaturalLatents.General.nats x ≤
      c * NaturalLatents.General.nats y) :
  x ≤ c * y
  • theoremdefined in NaturalLatents/General/Nats.lean
    complete
    theorem NaturalLatents.General.nats_le_nats_iff {x y : ℝ} :
  NaturalLatents.General.nats x ≤ NaturalLatents.General.nats y ↔ x ≤ y
    theorem NaturalLatents.General.nats_le_nats_iff
  {x y : ℝ} :
  NaturalLatents.General.nats x ≤
      NaturalLatents.General.nats y ↔
    x ≤ y
  • theoremdefined in NaturalLatents/General/Extension.lean
    complete
    theorem NaturalLatents.General.extension_of_connected {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y] (C : ℝ) (hC : 0 ≤ C)
  (hconnected :
    ∀ (q : NaturalLatents.General.Law X Y),
      stoch_to_det.IsPMF q →
        stoch_to_det.IsConnected (stoch_to_det.support q) →
          stoch_to_det.T q ≤ C * stoch_to_det.tau q)
  {p : NaturalLatents.General.Law X Y} (hp : stoch_to_det.IsPMF p) :
  stoch_to_det.T p ≤ C * stoch_to_det.tau p
    theorem NaturalLatents.General.extension_of_connected
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y] (C : ℝ)
  (hC : 0 ≤ C)
  (hconnected :
    ∀
      (q :
        NaturalLatents.General.Law X Y),
      stoch_to_det.IsPMF q →
        stoch_to_det.IsConnected
            (stoch_to_det.support q) →
          stoch_to_det.T q ≤
            C * stoch_to_det.tau q)
  {p : NaturalLatents.General.Law X Y}
  (hp : stoch_to_det.IsPMF p) :
  stoch_to_det.T p ≤
    C * stoch_to_det.tau p
    For `0 ≤ C`, a connected optimum bound in bits extends to every probability law.
Proof for Theorem 12.1.1
uses 0

Cancel the positive bits-to-nats factor and extend the connected bound by the component split. See the page section.

Lean: NaturalLatents.T_le_c_mul_tau (NaturalLatents/Main.lean), which cancels by NaturalLatents.General.bits_of_nats (NaturalLatents/General/Nats.lean, through nats_le_nats_iff) and then applies extension_of_connected.

Theorem12.1.2
Group: The table form. (5)
Group member previews
Preview
Theorem 12.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
Tagskernel-verified

Lemma T6.2 (an optimal code with N labels). For every finite law p there is a code \Gamma:A\times B\to[N], depending on p only, with D(\Gamma)=T(p), where D(\Gamma) is the bit-valued error I(X;Y\mid\Gamma)+H(\Gamma\mid X)+H(\Gamma\mid Y).

Lean code for Theorem12.1.2●6 theorems
  • theoremdefined in NaturalLatents/Upstream/Envelope.lean
    complete
    theorem stoch_to_det.exists_T_optimal_code.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {p : α × β → ℝ} (hp : stoch_to_det.IsPMF p) :
  ∃ Γ, (stoch_to_det.Latent.ofFunction hp Γ).score = stoch_to_det.T p
    theorem stoch_to_det.exists_T_optimal_code.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p) :
  ∃ Γ,
    (stoch_to_det.Latent.ofFunction hp
          Γ).score =
      stoch_to_det.T p
    Function-level form of deterministic attainment.  The returned code has
the fixed alphabet `Fin (card (α × β))`, and depends only on `p`.
  • theoremdefined in NaturalLatents/Upstream/Envelope.lean
    complete
    theorem stoch_to_det.exists_T_optimal_latent.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {p : α × β → ℝ} (hp : stoch_to_det.IsPMF p) :
  ∃ V, V.IsDet ∧ V.score = stoch_to_det.T p
    theorem stoch_to_det.exists_T_optimal_latent.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p) :
  ∃ V,
    V.IsDet ∧ V.score = stoch_to_det.T p
    Deterministic partition form: the same statement for `T` over
deterministic latents.
  • theoremdefined in NaturalLatents/Upstream/Envelope.lean
    complete
    theorem stoch_to_det.Latent.ofFunction_score_eq_detScore.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ} {γ : Type} [Fintype γ] [DecidableEq γ]
  (hp : stoch_to_det.IsPMF p) (Γ : α × β → γ) :
  (stoch_to_det.Latent.ofFunction hp Γ).score =
    stoch_to_det.detScore p Γ
    theorem stoch_to_det.Latent.ofFunction_score_eq_detScore.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  {γ : Type} [Fintype γ] [DecidableEq γ]
  (hp : stoch_to_det.IsPMF p)
  (Γ : α × β → γ) :
  (stoch_to_det.Latent.ofFunction hp
        Γ).score =
    stoch_to_det.detScore p Γ
    The score of a function-induced latent is exactly the deterministic
LessWrong expression computed under `p`.
  • theoremdefined in NaturalLatents/Upstream/Functionals.lean
    complete
    theorem stoch_to_det.condMI_code_X_given_Y.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {γ : Type u_3} [Fintype γ] [DecidableEq γ] {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p) (Γ : α × β → γ) :
  stoch_to_det.condMI Γ (fun z => z.1) (fun z => z.2) p =
    stoch_to_det.condH Γ (fun z => z.2) p
    theorem stoch_to_det.condMI_code_X_given_Y.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {γ : Type u_3}
  [Fintype γ] [DecidableEq γ]
  {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p)
  (Γ : α × β → γ) :
  stoch_to_det.condMI Γ (fun z => z.1)
      (fun z => z.2) p =
    stoch_to_det.condH Γ (fun z => z.2) p
  • theoremdefined in NaturalLatents/Upstream/Functionals.lean
    complete
    theorem stoch_to_det.condMI_code_Y_given_X.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {γ : Type u_3} [Fintype γ] [DecidableEq γ] {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p) (Γ : α × β → γ) :
  stoch_to_det.condMI Γ (fun z => z.2) (fun z => z.1) p =
    stoch_to_det.condH Γ (fun z => z.1) p
    theorem stoch_to_det.condMI_code_Y_given_X.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {γ : Type u_3}
  [Fintype γ] [DecidableEq γ]
  {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p)
  (Γ : α × β → γ) :
  stoch_to_det.condMI Γ (fun z => z.2)
      (fun z => z.1) p =
    stoch_to_det.condH Γ (fun z => z.1) p
  • theoremdefined in NaturalLatents/Upstream/Envelope.lean
    complete
    theorem stoch_to_det.Latent.score_eq.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {p : α × β → ℝ} (hp : stoch_to_det.IsPMF p)
  (V : stoch_to_det.Latent p) :
  V.score =
    stoch_to_det.Psi p - ∑ v, V.prior v * stoch_to_det.Phi (V.comp v)
    theorem stoch_to_det.Latent.score_eq.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p)
  (V : stoch_to_det.Latent p) :
  V.score =
    stoch_to_det.Psi p -
      ∑ v,
        V.prior v *
          stoch_to_det.Phi (V.comp v)
    Decomposition identity.
`S_p(V) = Ψ(p) − ∑ᵥ λᵥ Φ(qᵥ)`.
Proof for Theorem 12.1.2
uses 0

Relabel positive-prior deterministic labels injectively by source cells and minimize over the finite code space. See the page section.

Lean: stoch_to_det.exists_T_optimal_code (NaturalLatents/Upstream/Envelope.lean), through stoch_to_det.exists_T_optimal_latent, the private Latent.detLabel, Latent.detCode, Latent.detLabel_inj_of_prior_ne_zero and Latent.functionLatent_detCode_score_eq in the same file, and stoch_to_det.Latent.ofFunction_score_eq_detScore (same file), with stoch_to_det.condMI_code_X_given_Y and stoch_to_det.condMI_code_Y_given_X (NaturalLatents/Upstream/Functionals.lean). The score equality uses stoch_to_det.Latent.score_eq rather than the entropy expansion of Lemma S1.1.

Theorem12.1.3
Group: The table form. (5)
Group member previews
Preview
Theorem 12.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N
Tagskernel-verified

Lemma T6.3 (a joint table is a latent). For every finite label set K and every probability law r on K\times(A\times B) with (X,Y)-marginal p, there is a latent of p whose joint law is r; its error is the stochastic error of r.

Lean code for Theorem12.1.3●3 declarations
  • defdefined in NaturalLatents/Upstream/SourceCoarsening.lean
    complete
    def stoch_to_det.SourceCoarsening.ofJoint.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} {K : Type} [Fintype X] [Fintype Y] [Fintype K]
  [DecidableEq X] [DecidableEq Y] [DecidableEq K] {p : X × Y → ℝ}
  (hp : stoch_to_det.IsPMF p) (r : K × X × Y → ℝ)
  (hr : stoch_to_det.IsPMF r)
  (hsource : stoch_to_det.push Prod.snd r = p) : stoch_to_det.Latent p
    def stoch_to_det.SourceCoarsening.ofJoint.{u_1,
    u_2}
  {X : Type u_1} {Y : Type u_2} {K : Type}
  [Fintype X] [Fintype Y] [Fintype K]
  [DecidableEq X] [DecidableEq Y]
  [DecidableEq K] {p : X × Y → ℝ}
  (hp : stoch_to_det.IsPMF p)
  (r : K × X × Y → ℝ)
  (hr : stoch_to_det.IsPMF r)
  (hsource :
    stoch_to_det.push Prod.snd r = p) :
  stoch_to_det.Latent p
    A finite joint law with the specified source marginal defines a latent.
Zero-prior labels are filled with the source law.
  • theoremdefined in NaturalLatents/Upstream/SourceCoarsening.lean
    complete
    theorem stoch_to_det.SourceCoarsening.ofJoint_joint.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} {K : Type} [Fintype X] [Fintype Y] [Fintype K]
  [DecidableEq X] [DecidableEq Y] [DecidableEq K] {p : X × Y → ℝ}
  (hp : stoch_to_det.IsPMF p) (r : K × X × Y → ℝ)
  (hr : stoch_to_det.IsPMF r)
  (hsource : stoch_to_det.push Prod.snd r = p) :
  (stoch_to_det.SourceCoarsening.ofJoint hp r hr hsource).joint = r
    theorem stoch_to_det.SourceCoarsening.ofJoint_joint.{u_1,
    u_2}
  {X : Type u_1} {Y : Type u_2} {K : Type}
  [Fintype X] [Fintype Y] [Fintype K]
  [DecidableEq X] [DecidableEq Y]
  [DecidableEq K] {p : X × Y → ℝ}
  (hp : stoch_to_det.IsPMF p)
  (r : K × X × Y → ℝ)
  (hr : stoch_to_det.IsPMF r)
  (hsource :
    stoch_to_det.push Prod.snd r = p) :
  (stoch_to_det.SourceCoarsening.ofJoint
        hp r hr hsource).joint =
    r
  • theoremdefined in NaturalLatents/Upstream/SourceCoarsening.lean
    complete
    theorem stoch_to_det.SourceCoarsening.ofJoint_score.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} {K : Type} [Fintype X] [Fintype Y] [Fintype K]
  [DecidableEq X] [DecidableEq Y] [DecidableEq K] {p : X × Y → ℝ}
  (hp : stoch_to_det.IsPMF p) (r : K × X × Y → ℝ)
  (hr : stoch_to_det.IsPMF r)
  (hsource : stoch_to_det.push Prod.snd r = p) :
  (stoch_to_det.SourceCoarsening.ofJoint hp r hr hsource).score =
    stoch_to_det.condMI (fun v => v.2.1) (fun v => v.2.2) Prod.fst r +
        stoch_to_det.condMI Prod.fst (fun v => v.2.1) (fun v => v.2.2)
          r +
      stoch_to_det.condMI Prod.fst (fun v => v.2.2) (fun v => v.2.1) r
    theorem stoch_to_det.SourceCoarsening.ofJoint_score.{u_1,
    u_2}
  {X : Type u_1} {Y : Type u_2} {K : Type}
  [Fintype X] [Fintype Y] [Fintype K]
  [DecidableEq X] [DecidableEq Y]
  [DecidableEq K] {p : X × Y → ℝ}
  (hp : stoch_to_det.IsPMF p)
  (r : K × X × Y → ℝ)
  (hr : stoch_to_det.IsPMF r)
  (hsource :
    stoch_to_det.push Prod.snd r = p) :
  (stoch_to_det.SourceCoarsening.ofJoint
        hp r hr hsource).score =
    stoch_to_det.condMI (fun v => v.2.1)
          (fun v => v.2.2) Prod.fst r +
        stoch_to_det.condMI Prod.fst
          (fun v => v.2.1)
          (fun v => v.2.2) r +
      stoch_to_det.condMI Prod.fst
        (fun v => v.2.2) (fun v => v.2.1)
        r
Proof for Theorem 12.1.3
uses 0

Normalize each positive row of the joint table and assign the source law to zero-prior rows. See the page section.

Lean: stoch_to_det.SourceCoarsening.ofJoint, ofJoint_joint and ofJoint_score (NaturalLatents/Upstream/SourceCoarsening.lean).

Theorem12.1.4
Group: The table form. (5)
Group member previews
Preview
Theorem 12.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 12.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagskernel-verified

Lemma T6.4 (one code for every joint law). For every finite law p, there is a code \Gamma such that D(\Gamma)\le c\,\mathrm{SE}(r) for every finite K and every law r on K\times(A\times B) with marginal p.

Lean code for Theorem12.1.4●5 theorems
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.finite_bound {α β : Type} [Fintype α] [Fintype β]
  [DecidableEq α] [DecidableEq β] {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p) :
  ∃ Γ,
    ∀ {K : Type} [inst : Fintype K] [inst_1 : DecidableEq K]
      (q : K × α × β → ℝ),
      stoch_to_det.IsPMF q →
        (∀ (z : α × β), ∑ v, q (v, z) = p z) →
          stoch_to_det.condMI Prod.fst Prod.snd Γ p +
                stoch_to_det.condH Γ Prod.fst p +
              stoch_to_det.condH Γ Prod.snd p ≤
            NaturalLatents.c *
              (stoch_to_det.condMI (fun w => w.2.1) (fun w => w.2.2)
                    Prod.fst q +
                  stoch_to_det.condMI Prod.fst (fun w => w.2.1)
                    (fun w => w.2.2) q +
                stoch_to_det.condMI Prod.fst (fun w => w.2.2)
                  (fun w => w.2.1) q)
    theorem NaturalLatents.finite_bound {α β : Type}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p) :
  ∃ Γ,
    ∀ {K : Type} [inst : Fintype K]
      [inst_1 : DecidableEq K]
      (q : K × α × β → ℝ),
      stoch_to_det.IsPMF q →
        (∀ (z : α × β),
            ∑ v, q (v, z) = p z) →
          stoch_to_det.condMI Prod.fst
                  Prod.snd Γ p +
                stoch_to_det.condH Γ
                  Prod.fst p +
              stoch_to_det.condH Γ
                Prod.snd p ≤
            NaturalLatents.c *
              (stoch_to_det.condMI
                    (fun w => w.2.1)
                    (fun w => w.2.2)
                    Prod.fst q +
                  stoch_to_det.condMI
                    Prod.fst
                    (fun w => w.2.1)
                    (fun w => w.2.2) q +
                stoch_to_det.condMI
                  Prod.fst
                  (fun w => w.2.2)
                  (fun w => w.2.1) q)
    One optimal deterministic code bounds every finite joint latent law.
  • theoremdefined in NaturalLatents/Upstream/Envelope.lean
    complete
    theorem stoch_to_det.exists_T_optimal_code.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {p : α × β → ℝ} (hp : stoch_to_det.IsPMF p) :
  ∃ Γ, (stoch_to_det.Latent.ofFunction hp Γ).score = stoch_to_det.T p
    theorem stoch_to_det.exists_T_optimal_code.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  (hp : stoch_to_det.IsPMF p) :
  ∃ Γ,
    (stoch_to_det.Latent.ofFunction hp
          Γ).score =
      stoch_to_det.T p
    Function-level form of deterministic attainment.  The returned code has
the fixed alphabet `Fin (card (α × β))`, and depends only on `p`.
  • theoremdefined in NaturalLatents/Upstream/Envelope.lean
    complete
    theorem stoch_to_det.Latent.ofFunction_score_eq_detScore.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ} {γ : Type} [Fintype γ] [DecidableEq γ]
  (hp : stoch_to_det.IsPMF p) (Γ : α × β → γ) :
  (stoch_to_det.Latent.ofFunction hp Γ).score =
    stoch_to_det.detScore p Γ
    theorem stoch_to_det.Latent.ofFunction_score_eq_detScore.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  {γ : Type} [Fintype γ] [DecidableEq γ]
  (hp : stoch_to_det.IsPMF p)
  (Γ : α × β → γ) :
  (stoch_to_det.Latent.ofFunction hp
        Γ).score =
    stoch_to_det.detScore p Γ
    The score of a function-induced latent is exactly the deterministic
LessWrong expression computed under `p`.
  • theoremdefined in NaturalLatents/Upstream/Functionals.lean
    complete
    theorem stoch_to_det.tau_le_score.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {p : α × β → ℝ} (V : stoch_to_det.Latent p) :
  stoch_to_det.tau p ≤ V.score
    theorem stoch_to_det.tau_le_score.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  (V : stoch_to_det.Latent p) :
  stoch_to_det.tau p ≤ V.score
    The infimum `tau p` is below the score of every finite latent.
  • theoremdefined in NaturalLatents/Upstream/Functionals.lean
    complete
    theorem stoch_to_det.Latent.score_nonneg.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {p : α × β → ℝ} (V : stoch_to_det.Latent p) : 0 ≤ V.score
    theorem stoch_to_det.Latent.score_nonneg.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {p : α × β → ℝ}
  (V : stoch_to_det.Latent p) :
  0 ≤ V.score
Proof for Theorem 12.1.4
uses 0

Use the optimal code and the all-law bound, then compare the stochastic infimum with the joint table’s latent error. See the page section.

Lean: NaturalLatents.finite_bound (NaturalLatents/Main.lean), which takes \Gamma from stoch_to_det.exists_T_optimal_code and rewrites its error by stoch_to_det.Latent.ofFunction_score_eq_detScore, with stoch_to_det.tau_le_score (NaturalLatents/Upstream/Functionals.lean), whose lower bound is stoch_to_det.Latent.score_nonneg (same file).

Theorem12.1.5
Group: The table form. (5)
Group member previews
Preview
Theorem 12.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
Tagskernel-verified

Lemma T6.5 (the table form). For every finite law p, there is a code \Gamma such that \mathrm{DE}(t_{p,\Gamma})\le c\,\mathrm{SE}(q) for every k and every law q on A\times B\times[k] with marginal p; since 0\le c<7, TableClaim holds with c.

Lean code for Theorem12.1.5●14 theorems
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.table_bound {A B : Type} [Fintype A] [Fintype B]
  [DecidableEq A] [DecidableEq B] {p : A × B → ℝ}
  (hp : TableInformationProof.probability p) :
  ∃ Γ,
    ∀ (k : ℕ) (q : A × B × Fin k → ℝ),
      TableInformationProof.probability q →
        (∀ (a : A) (b : B), ∑ v, q (a, b, v) = p (a, b)) →
          TableInformationProof.latentError
              (TableBoundProof.deterministicTable p Γ) ≤
            NaturalLatents.c * TableInformationProof.latentError q
    theorem NaturalLatents.table_bound {A B : Type}
  [Fintype A] [Fintype B] [DecidableEq A]
  [DecidableEq B] {p : A × B → ℝ}
  (hp :
    TableInformationProof.probability p) :
  ∃ Γ,
    ∀ (k : ℕ) (q : A × B × Fin k → ℝ),
      TableInformationProof.probability
          q →
        (∀ (a : A) (b : B),
            ∑ v, q (a, b, v) = p (a, b)) →
          TableInformationProof.latentError
              (TableBoundProof.deterministicTable
                p Γ) ≤
            NaturalLatents.c *
              TableInformationProof.latentError
                q
    The bound on probability tables, with the core-library error on both sides.
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.table_bound_entropy {A B : Type} [Fintype A] [Fintype B]
  [DecidableEq A] [DecidableEq B] {p : A × B → ℝ}
  (hp : TableInformationProof.probability p) :
  ∃ Γ,
    ∀ (k : ℕ) (q : A × B × Fin k → ℝ),
      TableInformationProof.probability q →
        (∀ (a : A) (b : B), ∑ v, q (a, b, v) = p (a, b)) →
          TableBoundProof.deterministicError
              (TableBoundProof.deterministicTable p Γ) ≤
            NaturalLatents.c * TableInformationProof.latentError q
    theorem NaturalLatents.table_bound_entropy
  {A B : Type} [Fintype A] [Fintype B]
  [DecidableEq A] [DecidableEq B]
  {p : A × B → ℝ}
  (hp :
    TableInformationProof.probability p) :
  ∃ Γ,
    ∀ (k : ℕ) (q : A × B × Fin k → ℝ),
      TableInformationProof.probability
          q →
        (∀ (a : A) (b : B),
            ∑ v, q (a, b, v) = p (a, b)) →
          TableBoundProof.deterministicError
              (TableBoundProof.deterministicTable
                p Γ) ≤
            NaturalLatents.c *
              TableInformationProof.latentError
                q
    The bound on probability tables, with conditional entropies on the deterministic side.
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.table : NaturalLatents.TableClaim
    theorem NaturalLatents.table :
  NaturalLatents.TableClaim
    **The finite natural-latent theorem, table form.**
  • theoremdefined in NaturalLatents/Upstream/TableBoundProof.lean
    complete
    theorem TableBoundProof.deterministicTable_eq_push {A B C : Type} [Fintype A]
  [Fintype B] [DecidableEq A] [DecidableEq B] [DecidableEq C]
  (p : A × B → ℝ) (Γ : A × B → C) :
  TableBoundProof.deterministicTable p Γ =
    stoch_to_det.push (fun ab => (ab.1, ab.2, Γ ab)) p
    theorem TableBoundProof.deterministicTable_eq_push
  {A B C : Type} [Fintype A] [Fintype B]
  [DecidableEq A] [DecidableEq B]
  [DecidableEq C] (p : A × B → ℝ)
  (Γ : A × B → C) :
  TableBoundProof.deterministicTable p Γ =
    stoch_to_det.push
      (fun ab => (ab.1, ab.2, Γ ab)) p
  • theoremdefined in NaturalLatents/Upstream/TableBoundProof.lean
    complete
    theorem TableBoundProof.deterministicTable_error {A B C : Type} [Fintype A]
  [Fintype B] [Fintype C] [DecidableEq A] [DecidableEq B]
  [DecidableEq C] {p : A × B → ℝ} (hp : stoch_to_det.IsPMF p)
  (Γ : A × B → C) :
  TableInformationProof.latentError
      (TableBoundProof.deterministicTable p Γ) =
    stoch_to_det.detScore p Γ
    theorem TableBoundProof.deterministicTable_error
  {A B C : Type} [Fintype A] [Fintype B]
  [Fintype C] [DecidableEq A]
  [DecidableEq B] [DecidableEq C]
  {p : A × B → ℝ}
  (hp : stoch_to_det.IsPMF p)
  (Γ : A × B → C) :
  TableInformationProof.latentError
      (TableBoundProof.deterministicTable
        p Γ) =
    stoch_to_det.detScore p Γ
  • theoremdefined in NaturalLatents/Upstream/TableBoundProof.lean
    complete
    theorem TableBoundProof.deterministicTable_entropy_error {A B C : Type}
  [Fintype A] [Fintype B] [Fintype C] [DecidableEq A] [DecidableEq B]
  [DecidableEq C] {p : A × B → ℝ} (hp : stoch_to_det.IsPMF p)
  (Γ : A × B → C) :
  TableBoundProof.deterministicError
      (TableBoundProof.deterministicTable p Γ) =
    stoch_to_det.detScore p Γ
    theorem TableBoundProof.deterministicTable_entropy_error
  {A B C : Type} [Fintype A] [Fintype B]
  [Fintype C] [DecidableEq A]
  [DecidableEq B] [DecidableEq C]
  {p : A × B → ℝ}
  (hp : stoch_to_det.IsPMF p)
  (Γ : A × B → C) :
  TableBoundProof.deterministicError
      (TableBoundProof.deterministicTable
        p Γ) =
    stoch_to_det.detScore p Γ
  • theoremdefined in NaturalLatents/Upstream/TableBoundProof.lean
    complete
    theorem TableBoundProof.deterministicTable_errors_equal {A B C : Type}
  [Fintype A] [Fintype B] [Fintype C] [DecidableEq A] [DecidableEq B]
  [DecidableEq C] {p : A × B → ℝ} (hp : stoch_to_det.IsPMF p)
  (Γ : A × B → C) :
  TableBoundProof.deterministicError
      (TableBoundProof.deterministicTable p Γ) =
    TableInformationProof.latentError
      (TableBoundProof.deterministicTable p Γ)
    theorem TableBoundProof.deterministicTable_errors_equal
  {A B C : Type} [Fintype A] [Fintype B]
  [Fintype C] [DecidableEq A]
  [DecidableEq B] [DecidableEq C]
  {p : A × B → ℝ}
  (hp : stoch_to_det.IsPMF p)
  (Γ : A × B → C) :
  TableBoundProof.deterministicError
      (TableBoundProof.deterministicTable
        p Γ) =
    TableInformationProof.latentError
      (TableBoundProof.deterministicTable
        p Γ)
  • theoremdefined in NaturalLatents/Upstream/TableBoundProof.lean
    complete
    theorem TableBoundProof.transpose_eq_push {A B C : Type} [Fintype A] [Fintype B]
  [Fintype C] [DecidableEq A] [DecidableEq B] [DecidableEq C]
  (q : A × B × C → ℝ) :
  (fun v => q (v.2.1, v.2.2, v.1)) =
    stoch_to_det.push (fun abc => (abc.2.2, abc.1, abc.2.1)) q
    theorem TableBoundProof.transpose_eq_push
  {A B C : Type} [Fintype A] [Fintype B]
  [Fintype C] [DecidableEq A]
  [DecidableEq B] [DecidableEq C]
  (q : A × B × C → ℝ) :
  (fun v => q (v.2.1, v.2.2, v.1)) =
    stoch_to_det.push
      (fun abc =>
        (abc.2.2, abc.1, abc.2.1))
      q
  • theoremdefined in NaturalLatents/Upstream/TableInformationProof.lean
    complete
    theorem TableInformationProof.entropy_eq_H.{u_1} {A : Type u_1} [Fintype A]
  {p : A → ℝ} (hp : stoch_to_det.IsPMF p) :
  TableInformationProof.entropy p = stoch_to_det.H p
    theorem TableInformationProof.entropy_eq_H.{u_1}
  {A : Type u_1} [Fintype A] {p : A → ℝ}
  (hp : stoch_to_det.IsPMF p) :
  TableInformationProof.entropy p =
    stoch_to_det.H p
  • theoremdefined in NaturalLatents/Upstream/TableInformationProof.lean
    complete
    theorem TableInformationProof.conditionalMutualInformation_push.{u_1, u_2, u_3,
    u_4}
  {A : Type u_1} {B : Type u_2} {C : Type u_3} {Ω : Type u_4}
  [Fintype A] [Fintype B] [Fintype C] [Fintype Ω] [DecidableEq A]
  [DecidableEq B] [DecidableEq C] {p : Ω → ℝ}
  (hp : stoch_to_det.IsPMF p) (x : Ω → A) (y : Ω → B) (v : Ω → C) :
  TableInformationProof.conditionalMutualInformation
      (stoch_to_det.push (fun w => (x w, y w, v w)) p) =
    stoch_to_det.condMI x y v p
    theorem TableInformationProof.conditionalMutualInformation_push.{u_1,
    u_2, u_3, u_4}
  {A : Type u_1} {B : Type u_2}
  {C : Type u_3} {Ω : Type u_4}
  [Fintype A] [Fintype B] [Fintype C]
  [Fintype Ω] [DecidableEq A]
  [DecidableEq B] [DecidableEq C]
  {p : Ω → ℝ} (hp : stoch_to_det.IsPMF p)
  (x : Ω → A) (y : Ω → B) (v : Ω → C) :
  TableInformationProof.conditionalMutualInformation
      (stoch_to_det.push
        (fun w => (x w, y w, v w)) p) =
    stoch_to_det.condMI x y v p
  • theoremdefined in NaturalLatents/Upstream/TableInformationProof.lean
    complete
    theorem TableInformationProof.latentError_eq_core.{u_1, u_2, u_3} {A : Type u_1}
  {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C]
  [DecidableEq A] [DecidableEq B] [DecidableEq C] {p : A × B × C → ℝ}
  (hp : stoch_to_det.IsPMF p) :
  TableInformationProof.latentError p =
    stoch_to_det.condMI (fun w => w.1) (fun w => w.2.1) (fun w => w.2.2)
          p +
        stoch_to_det.condMI (fun w => w.2.2) (fun w => w.1)
          (fun w => w.2.1) p +
      stoch_to_det.condMI (fun w => w.2.2) (fun w => w.2.1)
        (fun w => w.1) p
    theorem TableInformationProof.latentError_eq_core.{u_1,
    u_2, u_3}
  {A : Type u_1} {B : Type u_2}
  {C : Type u_3} [Fintype A] [Fintype B]
  [Fintype C] [DecidableEq A]
  [DecidableEq B] [DecidableEq C]
  {p : A × B × C → ℝ}
  (hp : stoch_to_det.IsPMF p) :
  TableInformationProof.latentError p =
    stoch_to_det.condMI (fun w => w.1)
          (fun w => w.2.1)
          (fun w => w.2.2) p +
        stoch_to_det.condMI
          (fun w => w.2.2) (fun w => w.1)
          (fun w => w.2.1) p +
      stoch_to_det.condMI (fun w => w.2.2)
        (fun w => w.2.1) (fun w => w.1) p
  • theoremdefined in NaturalLatents/Upstream/Entropy.lean
    complete
    theorem stoch_to_det.condMI_push_source.{u_6, u_7, u_8, u_9, u_10}
  {Ω : Type u_6} {Ω' : Type u_7} {K : Type u_8} {D : Type u_9}
  {E : Type u_10} [Fintype Ω] [Fintype Ω'] [DecidableEq Ω'] [Fintype K]
  [DecidableEq K] [Fintype D] [DecidableEq D] [Fintype E]
  [DecidableEq E] (e : Ω → Ω') (a : Ω' → K) (b : Ω' → D) (c : Ω' → E)
  (m : Ω → ℝ) :
  stoch_to_det.condMI a b c (stoch_to_det.push e m) =
    stoch_to_det.condMI (a ∘ e) (b ∘ e) (c ∘ e) m
    theorem stoch_to_det.condMI_push_source.{u_6, u_7,
    u_8, u_9, u_10}
  {Ω : Type u_6} {Ω' : Type u_7}
  {K : Type u_8} {D : Type u_9}
  {E : Type u_10} [Fintype Ω] [Fintype Ω']
  [DecidableEq Ω'] [Fintype K]
  [DecidableEq K] [Fintype D]
  [DecidableEq D] [Fintype E]
  [DecidableEq E] (e : Ω → Ω')
  (a : Ω' → K) (b : Ω' → D) (c : Ω' → E)
  (m : Ω → ℝ) :
  stoch_to_det.condMI a b c
      (stoch_to_det.push e m) =
    stoch_to_det.condMI (a ∘ e) (b ∘ e)
      (c ∘ e) m
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.c_nonneg : 0 ≤ NaturalLatents.c
    theorem NaturalLatents.c_nonneg :
  0 ≤ NaturalLatents.c
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.c_lt_seven : NaturalLatents.c < 7
    theorem NaturalLatents.c_lt_seven :
  NaturalLatents.c < 7
Proof for Theorem 12.1.5
uses 0

Transpose the table slots and identify table entropies with pushforward entropies to apply the finite-law code bound. See the page section.

Lean: NaturalLatents.table_bound (stochastic form on both sides), NaturalLatents.table_bound_entropy (conditional entropies on the deterministic side) and NaturalLatents.table (NaturalLatents/Main.lean), through TableBoundProof.deterministicTable_eq_push, deterministicTable_error, deterministicTable_entropy_error, deterministicTable_errors_equal and transpose_eq_push, and TableInformationProof.entropy_eq_H, conditionalMutualInformation_push and latentError_eq_core, with stoch_to_det.condMI_push_source (NaturalLatents/Upstream/Entropy.lean). The identification lemmas hold for every code. The bound 0\le c<7 is NaturalLatents.c_nonneg and NaturalLatents.c_lt_seven (NaturalLatents/Main.lean). The frozen definitions agree with these bridge definitions definitionally, by unfolding; the kernel checks this when it checks table, and no separate lemma states it.

Theorem12.1.6
Group: The table form. (5)
Group member previews
Preview
Theorem 12.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
Tagskernel-verified

Lemma T6.6 (the optimum form). Let p be a probability law on A\times B. If a code g and a constant c\ge0 satisfy \mathrm{DE}(t_{p,g})\le c\,\mathrm{SE}(q) for every admissible q, then T_\star(p)\le c\,\tau_\star(p). Hence TableClaim implies ScoreClaim.

Lean code for Theorem12.1.6●4 theorems
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.T_le_mul_tau_of_code {A B : Type} [Fintype A] [Fintype B]
  [DecidableEq A] [DecidableEq B] {p : A × B → ℝ}
  (hp : NaturalLatents.Probability p) (c : ℝ) (hc0 : 0 ≤ c)
  (g : A × B → Fin (Fintype.card (A × B)))
  (hg :
    ∀ (k : ℕ) (q : A × B × Fin k → ℝ),
      NaturalLatents.Probability q →
        (∀ (x : A) (y : B), ∑ v, q (x, y, v) = p (x, y)) →
          NaturalLatents.DeterministicError
              (NaturalLatents.deterministicTable p g) ≤
            c * NaturalLatents.StochasticError q) :
  NaturalLatents.T p ≤ c * NaturalLatents.tau p
    theorem NaturalLatents.T_le_mul_tau_of_code
  {A B : Type} [Fintype A] [Fintype B]
  [DecidableEq A] [DecidableEq B]
  {p : A × B → ℝ}
  (hp : NaturalLatents.Probability p)
  (c : ℝ) (hc0 : 0 ≤ c)
  (g : A × B → Fin (Fintype.card (A × B)))
  (hg :
    ∀ (k : ℕ) (q : A × B × Fin k → ℝ),
      NaturalLatents.Probability q →
        (∀ (x : A) (y : B),
            ∑ v, q (x, y, v) = p (x, y)) →
          NaturalLatents.DeterministicError
              (NaturalLatents.deterministicTable
                p g) ≤
            c *
              NaturalLatents.StochasticError
                q) :
  NaturalLatents.T p ≤
    c * NaturalLatents.tau p
    A code bound implies the optimum bound: `T p` is at most the error of any one code,
and the stochastic feasible set is nonempty (the constant latent).
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.score_of_table (h : NaturalLatents.TableClaim) :
  NaturalLatents.ScoreClaim
    theorem NaturalLatents.score_of_table
  (h : NaturalLatents.TableClaim) :
  NaturalLatents.ScoreClaim
    The table form implies the optimum form.
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.T_le_mul_tau (A B : Type) [Fintype A] [Fintype B]
  [DecidableEq A] [DecidableEq B] (p : A × B → ℝ)
  (hp : NaturalLatents.Probability p) :
  NaturalLatents.T p ≤ 13999 / 2000 * NaturalLatents.tau p
    theorem NaturalLatents.T_le_mul_tau (A B : Type)
  [Fintype A] [Fintype B] [DecidableEq A]
  [DecidableEq B] (p : A × B → ℝ)
  (hp : NaturalLatents.Probability p) :
  NaturalLatents.T p ≤
    13999 / 2000 * NaturalLatents.tau p
    The exact optimum bound in the frozen statement's vocabulary.
  • theoremdefined in NaturalLatents/Main.lean
    complete
    theorem NaturalLatents.score : NaturalLatents.ScoreClaim
    theorem NaturalLatents.score :
  NaturalLatents.ScoreClaim
    **The finite natural-latent theorem, optimum form.**
Proof for Theorem 12.1.6
uses 0

Compare the deterministic minimum with the supplied code, then take the stochastic infimum, treating a zero constant separately. See the page section.

Lean: NaturalLatents.T_le_mul_tau_of_code, score_of_table, T_le_mul_tau and score (NaturalLatents/Main.lean). score is proved from T_le_mul_tau, which applies T_le_mul_tau_of_code to the code of table_bound_entropy, not through score_of_table. NaturalLatents.T_le_mul_tau states the constant as the literal 13999 / 2000, as does its pinned example in Verify.lean.