Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

The two-clique quantum junction tree theorem (Lauritzen–Zwiernik, arXiv:2605.19453, Theorem 3.1): over the acyclic two-clique base, the base's compatibility datum decides base-side reconstruction. For strictly positive consistent marginals, a quantum Markov completion exists iff Tr T(R) = 1; the completion is then unique and equals the normalized logarithmic candidate σ(R) = T(R)/Tr T(R). Together with trC_le_one (the trace bound) this is the full theorem.

DeclHiddenChannelCapacity.lz_theorem_3_1

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [inst_5 : Nonempty c] [inst_6 : Fintype b] [inst_7 : DecidableEq b]
  [inst_8 : Nonempty b] {ρAC : MState (a × c)} {ρCB : MState (c × b)},
  ρAC.m.PosDef →
    ρCB.m.PosDef →
      ρAC.traceLeft = ρCB.traceRight →
        (HiddenChannelCapacity.trC ρAC ρCB = 1 ↔ ∃ ω, HiddenChannelCapacity.IsMarkovCompletion ρAC ρCB ω) ∧
          ∀ (ω : MState (a × c × b)),
            HiddenChannelCapacity.IsMarkovCompletion ρAC ρCB ω → ω = HiddenChannelCapacity.sigT ρAC ρCB

TopicGraphical models

ThesisStepHypothesisDefinition

DeclHiddenChannelCapacity.lz_theorem_3_1Declaration kindtheorem

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [inst_5 : Nonempty c] [inst_6 : Fintype b] [inst_7 : DecidableEq b]
  [inst_8 : Nonempty b] {ρAC : MState (a × c)} {ρCB : MState (c × b)},
  ρAC.m.PosDef →
    ρCB.m.PosDef →
      ρAC.traceLeft = ρCB.traceRight →
        (HiddenChannelCapacity.trC ρAC ρCB = 1 ↔ ∃ ω, HiddenChannelCapacity.IsMarkovCompletion ρAC ρCB ω) ∧
          ∀ (ω : MState (a × c × b)),
            HiddenChannelCapacity.IsMarkovCompletion ρAC ρCB ω → ω = HiddenChannelCapacity.sigT ρAC ρCB

HiddenChannelCapacity.IsMarkovCompletion HiddenChannelCapacity.sigT HiddenChannelCapacity.trC

Uses

HiddenChannelCapacity.markov_completion_eq_sigT
HiddenChannelCapacity.sigT_markov_of_trC_eq_one

DeclHiddenChannelCapacity.sigT_markov_of_trC_eq_oneDeclaration kindtheorem
LZ Theorem 3.1, existence direction: if Tr T(R) = 1 then the normalized candidate IS a quantum Markov completion (extraction of Δ_R = 0 via DPI and the faithfulness of relative entropy, in the order recorded in the QJT_URS front-load).
```
∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [inst_5 : Nonempty c] [inst_6 : Fintype b] [inst_7 : DecidableEq b]
  [inst_8 : Nonempty b] {ρAC : MState (a × c)} {ρCB : MState (c × b)},
  ρAC.m.PosDef →
    ρCB.m.PosDef →
      ρAC.traceLeft = ρCB.traceRight →
        HiddenChannelCapacity.trC ρAC ρCB = 1 →
          HiddenChannelCapacity.IsMarkovCompletion ρAC ρCB (HiddenChannelCapacity.sigT ρAC ρCB)
```
HiddenChannelCapacity.IsCompletion HiddenChannelCapacity.IsMarkovCompletion HiddenChannelCapacity.margAC HiddenChannelCapacity.margC HiddenChannelCapacity.margCB HiddenChannelCapacity.qDivR HiddenChannelCapacity.sigT HiddenChannelCapacity.trC
Uses
Used by
- HiddenChannelCapacity.lz_theorem_3_1
DeclHiddenChannelCapacity.markov_completion_eq_sigTDeclaration kindtheorem
LZ Theorem 3.1, uniqueness direction: any quantum Markov completion forces Tr T(R) = 1 and equals the normalized candidate σ(R).
```
∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [inst_5 : Nonempty c] [inst_6 : Fintype b] [inst_7 : DecidableEq b]
  [inst_8 : Nonempty b] {ρAC : MState (a × c)} {ρCB : MState (c × b)},
  ρAC.m.PosDef →
    ρCB.m.PosDef →
      ρAC.traceLeft = ρCB.traceRight →
        ∀ (ω : MState (a × c × b)),
          HiddenChannelCapacity.IsMarkovCompletion ρAC ρCB ω →
            HiddenChannelCapacity.trC ρAC ρCB = 1 ∧ ω = HiddenChannelCapacity.sigT ρAC ρCB
```
HiddenChannelCapacity.IsCompletion HiddenChannelCapacity.IsMarkovCompletion HiddenChannelCapacity.margAC HiddenChannelCapacity.margC HiddenChannelCapacity.margCB HiddenChannelCapacity.qDivR HiddenChannelCapacity.sigT HiddenChannelCapacity.trC
Uses
Used by
- HiddenChannelCapacity.lz_theorem_3_1
DeclHiddenChannelCapacity.trC_le_oneDeclaration kindtheorem
LZ Theorem 3.1, the trace bound: Tr T(R) ≤ 1. Proved WITHOUT Lieb's three-matrix inequality, by the eq. 13 route specialized to two cliques (Lemma 3.2 at ω = σ(R) plus SSA and DPI); see the QJT_URS L2a front-load.
```
∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [Nonempty c] [inst_6 : Fintype b] [inst_7 : DecidableEq b] [Nonempty b]
  {ρAC : MState (a × c)} {ρCB : MState (c × b)}, ρAC.m.PosDef → ρCB.m.PosDef → HiddenChannelCapacity.trC ρAC ρCB ≤ 1
```
HiddenChannelCapacity.margAC HiddenChannelCapacity.margC HiddenChannelCapacity.margCB HiddenChannelCapacity.qDivR HiddenChannelCapacity.sigT HiddenChannelCapacity.trC
Uses
Used by
- HiddenChannelCapacity.markov_completion_eq_sigT

DeclHiddenChannelCapacity.deltaR_nonnegDeclaration kindtheorem

Δ_R(ω) ≥ 0: one DPI application plus Klein nonnegativity (LZ Lem 3.2's nonnegativity clause, via Prop A.7 imported through the vendored channel DPI).

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [inst_5 : Fintype b] [inst_6 : DecidableEq b] {ρAC : MState (a × c)}
  {ρCB : MState (c × b)},
  ρAC.m.PosDef →
    ρCB.m.PosDef →
      ∀ (ω : MState (a × c × b)),
        0 ≤
          HiddenChannelCapacity.qDivR (HiddenChannelCapacity.margAC ω) ρAC +
              HiddenChannelCapacity.qDivR (HiddenChannelCapacity.margCB ω) ρCB -
            HiddenChannelCapacity.qDivR (HiddenChannelCapacity.margC ω) ρAC.traceLeft

HiddenChannelCapacity.margAC HiddenChannelCapacity.margC HiddenChannelCapacity.margCB HiddenChannelCapacity.qDivR

Uses

HiddenChannelCapacity.posDef_traceLeft
HiddenChannelCapacity.qDivR_dpi_traceLeft
HiddenChannelCapacity.qDivR_nonneg

Used by

HiddenChannelCapacity.sigT_markov_of_trC_eq_one
HiddenChannelCapacity.trC_le_one

DeclHiddenChannelCapacity.qDivR_dpi_traceLeftDeclaration kindtheorem
DPI for the real divergence under the left partial trace (monotonicity of relative entropy, LZ Prop A.7; imported from the vendored channel DPI sandwichedRenyiEntropy_DPI_eq_one at the partial-trace channel).
```
∀ {d₁ : Type u_5} {d₂ : Type u_6} [inst : Fintype d₁] [inst_1 : DecidableEq d₁] [inst_2 : Fintype d₂]
  [inst_3 : DecidableEq d₂] (ρ σ : MState (d₁ × d₂)),
  σ.m.PosDef →
    σ.traceLeft.m.PosDef → HiddenChannelCapacity.qDivR ρ.traceLeft σ.traceLeft ≤ HiddenChannelCapacity.qDivR ρ σ
```
HiddenChannelCapacity.qDivR
Uses
- HiddenChannelCapacity.qDivR_eq_toReal
Used by
- HiddenChannelCapacity.deltaR_nonneg
- HiddenChannelCapacity.sigT_markov_of_trC_eq_one
DeclHiddenChannelCapacity.qDivR_eq_toRealDeclaration kindtheorem
The single ENNReal-to-ℝ seam: qDivR equals the vendored relative entropy. (LZ p. 5; vendored qRelativeEnt_rank.)
```
∀ {d : Type u_4} [inst : Fintype d] [inst_1 : DecidableEq d] {ρ σ : MState d},
  σ.m.PosDef → HiddenChannelCapacity.qDivR ρ σ = 𝐃(ρ‖σ).toReal
```
HiddenChannelCapacity.qDivR
Uses
- HiddenChannelCapacity.toReal_bridge
Used by
- HiddenChannelCapacity.qDivR_dpi_traceLeft
DeclHiddenChannelCapacity.toReal_bridgeDeclaration kindtheorem
```
∀ {x : ENNReal} {r : ℝ}, x ≠ ⊤ → ↑x = ↑r → x.toReal = r
```
Used by
- HiddenChannelCapacity.qDivR_eq_toReal
DeclHiddenChannelCapacity.posDef_traceLeftDeclaration kindtheorem
The partial trace of a strictly positive state is strictly positive (marginals of elements of S₁⁺ stay in S₁⁺, LZ p. 4).
```
∀ {d₁ : Type u_1} {d₂ : Type u_2} [inst : Fintype d₁] [inst_1 : DecidableEq d₁] [Nonempty d₁] [inst_3 : Fintype d₂]
  [inst_4 : DecidableEq d₂] {σ : MState (d₁ × d₂)}, σ.m.PosDef → σ.traceLeft.m.PosDef
```
Used by
- HiddenChannelCapacity.deltaR_nonneg
- HiddenChannelCapacity.sigT_markov_of_trC_eq_one

DeclHiddenChannelCapacity.sigT_posDefDeclaration kindtheorem

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [inst_5 : Nonempty c] [inst_6 : Fintype b] [inst_7 : DecidableEq b]
  [inst_8 : Nonempty b] (ρAC : MState (a × c)) (ρCB : MState (c × b)), (HiddenChannelCapacity.sigT ρAC ρCB).m.PosDef

HiddenChannelCapacity.TR HiddenChannelCapacity.Tmat HiddenChannelCapacity.sigT HiddenChannelCapacity.trC

Uses

HiddenChannelCapacity.trC_pos

Used by

HiddenChannelCapacity.markov_completion_eq_sigT

DeclHiddenChannelCapacity.qDivR_selfDeclaration kindtheorem
```
∀ {d : Type u_4} [inst : Fintype d] [inst_1 : DecidableEq d] (ρ : MState d), HiddenChannelCapacity.qDivR ρ ρ = 0
```
HiddenChannelCapacity.qDivR
Used by
DeclHiddenChannelCapacity.qDivR_nonnegDeclaration kindtheorem
Klein nonnegativity in real form (vendored core: inner_log_sub_log_nonneg).
```
∀ {d : Type u_4} [inst : Fintype d] [inst_1 : DecidableEq d] {ρ σ : MState d},
  σ.m.PosDef → 0 ≤ HiddenChannelCapacity.qDivR ρ σ
```
HiddenChannelCapacity.qDivR
Uses
- HiddenChannelCapacity.ker_le_of_posDef
Used by

DeclHiddenChannelCapacity.ker_le_of_posDefDeclaration kindtheorem

∀ {d : Type u_4} [inst : Fintype d] [inst_1 : DecidableEq d] {ρ σ : MState d}, σ.m.PosDef → (↑σ).ker ≤ (↑ρ).ker

Used by

HiddenChannelCapacity.qDivR_nonneg

DeclHiddenChannelCapacity.lem_3_2Declaration kindtheorem
LZ Lemma 3.2, normalized form: for EVERY state ω, D(ω‖σ(R)) − log Tr T(R) = I(A:B|C)_ω + Δ_R(ω) with Δ_R(ω) := D(ω_AC‖ρ_AC) + D(ω_CB‖ρ_CB) − D(ω_C‖ρ_C). This is the paper's divergence identity (p. 8) restated against the NORMALIZED candidate via log T(R) = log Tr T(R) + log σ(R) (the presentation variant recorded in QJT_URS; pure real algebra over the duality, no positivity hypotheses).
```
∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [inst_5 : Nonempty c] [inst_6 : Fintype b] [inst_7 : DecidableEq b]
  [inst_8 : Nonempty b] (ρAC : MState (a × c)) (ρCB : MState (c × b)) (ω : MState (a × c × b)),
  HiddenChannelCapacity.qDivR ω (HiddenChannelCapacity.sigT ρAC ρCB) - Real.log (HiddenChannelCapacity.trC ρAC ρCB) =
    qcmi ω +
      (HiddenChannelCapacity.qDivR (HiddenChannelCapacity.margAC ω) ρAC +
          HiddenChannelCapacity.qDivR (HiddenChannelCapacity.margCB ω) ρCB -
        HiddenChannelCapacity.qDivR (HiddenChannelCapacity.margC ω) ρAC.traceLeft)
```
HiddenChannelCapacity.Tmat HiddenChannelCapacity.embedAC HiddenChannelCapacity.embedC HiddenChannelCapacity.embedCB HiddenChannelCapacity.margAC HiddenChannelCapacity.margC HiddenChannelCapacity.margCB HiddenChannelCapacity.qDivR HiddenChannelCapacity.sigT HiddenChannelCapacity.trC
Uses
Used by

DeclHiddenChannelCapacity.log_sigTDeclaration kindtheorem

The log of the normalized candidate splits into the trace constant and the embedded-log sum (log T(R) = log Tr T(R) + log σ(R), the normalization step of the LZ eq. 13 route).

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [inst_5 : Nonempty c] [inst_6 : Fintype b] [inst_7 : DecidableEq b]
  [inst_8 : Nonempty b] (ρAC : MState (a × c)) (ρCB : MState (c × b)),
  (↑(HiddenChannelCapacity.sigT ρAC ρCB)).log =
    Real.log (HiddenChannelCapacity.trC ρAC ρCB)⁻¹ • 1 + HiddenChannelCapacity.Tmat ρAC ρCB

HiddenChannelCapacity.TR HiddenChannelCapacity.Tmat HiddenChannelCapacity.sigT HiddenChannelCapacity.trC

Uses

HiddenChannelCapacity.exp_log_id
HiddenChannelCapacity.trC_pos

Used by

HiddenChannelCapacity.lem_3_2

DeclHiddenChannelCapacity.trC_posDeclaration kindtheorem

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [Nonempty c] [inst_6 : Fintype b] [inst_7 : DecidableEq b] [Nonempty b]
  (ρAC : MState (a × c)) (ρCB : MState (c × b)), 0 < HiddenChannelCapacity.trC ρAC ρCB

HiddenChannelCapacity.TR HiddenChannelCapacity.Tmat HiddenChannelCapacity.trC

Used by

HiddenChannelCapacity.log_sigT
HiddenChannelCapacity.markov_completion_eq_sigT
HiddenChannelCapacity.sigT_posDef

DeclHiddenChannelCapacity.exp_log_idDeclaration kindtheorem
exp then log is the identity on Hermitian matrices (unconditionally: both are cfc transports and Real.log ∘ Real.exp = id).
```
∀ {d : Type u_4} [inst : Fintype d] [inst_1 : DecidableEq d] (A : HermitianMat d ℂ), A.exp.log = A
```
Used by
- HiddenChannelCapacity.log_sigT
DeclHiddenChannelCapacity.inner_embedCDeclaration kindtheorem
Duality for the C-embedding (two-step pull-out; uses the marginal coherence margC_eq_CBright, LZ Lem 2.2).
```
∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Fintype c]
  [inst_3 : DecidableEq c] [inst_4 : Fintype b] [inst_5 : DecidableEq b] (ω : MState (a × c × b))
  (L : HermitianMat c ℂ), inner ℝ (↑ω) (HiddenChannelCapacity.embedC L) = inner ℝ (↑(HiddenChannelCapacity.margC ω)) L
```
HiddenChannelCapacity.embedC HiddenChannelCapacity.embedCB HiddenChannelCapacity.margC HiddenChannelCapacity.margCB
Uses
Used by
- HiddenChannelCapacity.lem_3_2
DeclHiddenChannelCapacity.margC_eq_CBrightDeclaration kindtheorem
Coherence of the two separator-marginal routes (iterated marginalization, LZ Lem 2.2): tracing a then b is tracing b then a.
```
∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Fintype c]
  [inst_3 : DecidableEq c] [inst_4 : Fintype b] [inst_5 : DecidableEq b] (ω : MState (a × c × b)),
  HiddenChannelCapacity.margC ω = (HiddenChannelCapacity.margCB ω).traceRight
```
HiddenChannelCapacity.margAC HiddenChannelCapacity.margC HiddenChannelCapacity.margCB
Uses
- HiddenChannelCapacity.assoc'_eq_relabel
Used by

DeclHiddenChannelCapacity.inner_kron_oneDeclaration kindtheorem

Duality for a right-identity Kronecker factor on any bipartite carrier.

∀ {d₁ : Type u_4} {d₂ : Type u_5} [inst : Fintype d₁] [inst_1 : DecidableEq d₁] [inst_2 : Fintype d₂]
  [inst_3 : DecidableEq d₂] (X : MState (d₁ × d₂)) (L : HermitianMat d₁ ℂ),
  inner ℝ (↑X) (L.kronecker 1) = inner ℝ (↑X.traceRight) L

Uses

Matrix.traceRight_mul_kron_one

Used by

HiddenChannelCapacity.inner_embedC

DeclMatrix.traceRight_mul_kron_oneDeclaration kindtheorem

Pull-out for the right partial trace, right-multiplication form: Tr_B(ρ (M ⊗ 1_B)) = Tr_B(ρ) · M.

∀ {R : Type u_1} [inst : NonAssocSemiring R] {d : Type u_2} {d₁ : Type u_3} {d₂ : Type u_4} {d₃ : Type u_5}
  [inst_1 : Fintype d] [inst_2 : Fintype d₂] [inst_3 : DecidableEq d] (ρ : Matrix (d₁ × d) (d₂ × d) R)
  (M : Matrix d₂ d₃ R), Matrix.traceRight (ρ * Matrix.kroneckerMap (fun x1 x2 => x1 * x2) M 1) = ρ.traceRight * M

Used by

HiddenChannelCapacity.inner_kron_one

DeclHiddenChannelCapacity.inner_embedCBDeclaration kindtheorem

Duality for the C∪B-embedding: testing the state against an embedded observable is testing the marginal (LZ eq. 2).

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Fintype c]
  [inst_3 : DecidableEq c] [inst_4 : Fintype b] [inst_5 : DecidableEq b] (ω : MState (a × c × b))
  (L : HermitianMat (c × b) ℂ),
  inner ℝ (↑ω) (HiddenChannelCapacity.embedCB L) = inner ℝ (↑(HiddenChannelCapacity.margCB ω)) L

HiddenChannelCapacity.embedCB HiddenChannelCapacity.margCB

Uses

Matrix.traceLeft_mul_one_kron

Used by

HiddenChannelCapacity.inner_embedC
HiddenChannelCapacity.lem_3_2

DeclMatrix.traceLeft_mul_one_kronDeclaration kindtheorem

Pull-out, right-multiplication form: Tr_A(ρ (1_A ⊗ M)) = Tr_A(ρ) · M.

∀ {R : Type u_1} [inst : NonAssocSemiring R] {d : Type u_2} {d₁ : Type u_3} {d₂ : Type u_4} {d₃ : Type u_5}
  [inst_1 : Fintype d] [inst_2 : Fintype d₂] [inst_3 : DecidableEq d] (ρ : Matrix (d × d₁) (d × d₂) R)
  (M : Matrix d₂ d₃ R), Matrix.traceLeft (ρ * Matrix.kroneckerMap (fun x1 x2 => x1 * x2) 1 M) = ρ.traceLeft * M

Used by

HiddenChannelCapacity.inner_embedCB

DeclHiddenChannelCapacity.inner_embedACDeclaration kindtheorem

Duality for the A∪C-embedding (via the L0 primitive traceAlong_duality).

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Fintype c]
  [inst_3 : DecidableEq c] [inst_4 : Fintype b] [inst_5 : DecidableEq b] (ω : MState (a × c × b))
  (L : HermitianMat (a × c) ℂ),
  inner ℝ (↑ω) (HiddenChannelCapacity.embedAC L) = inner ℝ (↑(HiddenChannelCapacity.margAC ω)) L

HiddenChannelCapacity.embedAC HiddenChannelCapacity.margAC MState.traceAlong Matrix.embedAlong

Uses

HiddenChannelCapacity.margAC_eq_traceAlong
MState.traceAlong_duality

Used by

HiddenChannelCapacity.lem_3_2

DeclMState.traceAlong_dualityDeclaration kindtheorem
The partial-trace duality (LZ eq (2), the defining property of the partial trace, split-indexed): testing the marginal against an observable is testing the state against the embedded observable, Tr(embedAlong e M · ρ) = Tr(M · traceAlong e ρ).
```
∀ {d : Type u_1} {a : Type u_2} {b : Type u_3} [inst : Fintype d] [inst_1 : DecidableEq d] [inst_2 : Fintype a]
  [inst_3 : DecidableEq a] [inst_4 : Fintype b] [inst_5 : DecidableEq b] (ρ : MState d) (e : d ≃ a × b)
  (M : Matrix a a ℂ), (Matrix.embedAlong e M * ρ.m).trace = (M * (ρ.traceAlong e).m).trace
```
MState.traceAlong Matrix.embedAlong
Uses
- Matrix.traceRight_kron_one_mul
- Matrix.trace_submatrix_equiv
Used by
- HiddenChannelCapacity.inner_embedAC

DeclMatrix.trace_submatrix_equivDeclaration kindtheorem

The trace is invariant under simultaneous reindexing by an equivalence.

∀ {R : Type u_1} [inst : NonAssocSemiring R] {n : Type u_6} {m : Type u_7} [inst_1 : Fintype n] [inst_2 : Fintype m]
  (A : Matrix m m R) (e : n ≃ m), (A.submatrix ⇑e ⇑e).trace = A.trace

Used by

MState.traceAlong_duality

DeclMatrix.traceRight_kron_one_mulDeclaration kindtheorem

Pull-out for the right partial trace, left-multiplication form: Tr_B((M ⊗ 1_B) ρ) = M · Tr_B(ρ).

∀ {R : Type u_1} [inst : NonAssocSemiring R] {d : Type u_2} {d₁ : Type u_3} {d₂ : Type u_4} {d₃ : Type u_5}
  [inst_1 : Fintype d] [inst_2 : Fintype d₂] [inst_3 : DecidableEq d] (M : Matrix d₁ d₂ R)
  (ρ : Matrix (d₂ × d) (d₃ × d) R),
  Matrix.traceRight (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) M 1 * ρ) = M * ρ.traceRight

Used by

MState.traceAlong_duality

DeclHiddenChannelCapacity.margAC_eq_traceAlongDeclaration kindtheorem

The AC-marginal in traceAlong form (the L0 primitive).

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Fintype c]
  [inst_3 : DecidableEq c] [inst_4 : Fintype b] [inst_5 : DecidableEq b] (ω : MState (a × c × b)),
  HiddenChannelCapacity.margAC ω = ω.traceAlong (Equiv.prodAssoc a c b).symm

HiddenChannelCapacity.margAC MState.traceAlong

Uses

HiddenChannelCapacity.assoc'_eq_relabel

Used by

HiddenChannelCapacity.inner_embedAC

DeclHiddenChannelCapacity.assoc'_eq_relabelDeclaration kindtheorem

The vendored associator is the plain prodAssoc relabel.

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Fintype c]
  [inst_3 : DecidableEq c] [inst_4 : Fintype b] [inst_5 : DecidableEq b] (ω : MState (a × c × b)),
  ω.assoc' = ω.relabel (Equiv.prodAssoc a c b)

Used by

HiddenChannelCapacity.margAC_eq_traceAlong
HiddenChannelCapacity.margC_eq_CBright

DeclHiddenChannelCapacity.inner_log_faithfulDeclaration kindtheorem
Faithfulness of quantum relative entropy (the equality case of Klein's inequality, LZ p. 5, Ruskai 2002 Thm 3; not present in the vendored corpus): for a state ρ and a STRICTLY POSITIVE state σ, Tr[ρ(log ρ − log σ)] = 0 forces ρ = σ.
```
∀ {d : Type u_1} [inst : Fintype d] [inst_1 : DecidableEq d] (ρ σ : MState d),
  σ.m.PosDef → inner ℝ (↑ρ) ((↑ρ).log - (↑σ).log) = 0 → ρ = σ
```
HiddenChannelCapacity.kleinTerm
Uses
Used by
- HiddenChannelCapacity.markov_completion_eq_sigT
- HiddenChannelCapacity.sigT_markov_of_trC_eq_one
DeclHiddenChannelCapacity.kleinTerm_nonnegDeclaration kindtheorem
```
∀ {x y : ℝ}, 0 ≤ x → 0 < y → 0 ≤ HiddenChannelCapacity.kleinTerm x y
```
HiddenChannelCapacity.kleinTerm
Used by
- HiddenChannelCapacity.inner_log_faithful
DeclHiddenChannelCapacity.kleinTerm_eq_zero_iffDeclaration kindtheorem
```
∀ {x y : ℝ}, 0 ≤ x → 0 < y → (HiddenChannelCapacity.kleinTerm x y = 0 ↔ x = y)
```
HiddenChannelCapacity.kleinTerm
Used by
- HiddenChannelCapacity.inner_log_faithful

DeclHermitianMat.overlap_row_sumDeclaration kindtheorem

Rows of the shared-basis kernel sum to one (C is unitary).

∀ {d : Type u_1} [inst : Fintype d] [inst_1 : DecidableEq d] (A B : HermitianMat d ℂ) (i : d),
  ∑ j, ‖((↑⋯.eigenvectorUnitary).conjTranspose * ↑⋯.eigenvectorUnitary) i j‖ ^ 2 = 1

Used by

HiddenChannelCapacity.inner_log_faithful

DeclHermitianMat.overlap_col_sumDeclaration kindtheorem

Columns of the shared-basis kernel sum to one.

∀ {d : Type u_1} [inst : Fintype d] [inst_1 : DecidableEq d] (A B : HermitianMat d ℂ) (j : d),
  ∑ i, ‖((↑⋯.eigenvectorUnitary).conjTranspose * ↑⋯.eigenvectorUnitary) i j‖ ^ 2 = 1

Used by

HiddenChannelCapacity.inner_log_faithful

DeclHermitianMat.log_eq_cfcDeclaration kindtheorem
A.log is cfc at Real.log, definitionally (QuantumInfo LogExp.lean).
```
∀ {d : Type u_1} [inst : Fintype d] [inst_1 : DecidableEq d] (A : HermitianMat d ℂ), A.log = A.cfc Real.log
```
Used by
- HiddenChannelCapacity.inner_log_faithful
DeclHermitianMat.inner_cfc_cfcDeclaration kindtheorem
The shared-basis double sum (generalizing the vendored inner_eq_doubly_stochastic_sum from (A, B) to (A.cfc f, B.cfc g) with the SAME overlap kernel): the inner product of two matrix functions expands over the pair of eigenbases with weights ‖C i j‖², C = U_A† U_B. All four divergence pairings of the faithfulness argument are instances of this one lemma at a single shared kernel.
```
∀ {d : Type u_1} [inst : Fintype d] [inst_1 : DecidableEq d] (A B : HermitianMat d ℂ) (f g : ℝ → ℝ),
  inner ℝ (A.cfc f) (B.cfc g) =
    ∑ i,
      ∑ j,
        f (⋯.eigenvalues i) * g (⋯.eigenvalues j) *
          ‖((↑⋯.eigenvectorUnitary).conjTranspose * ↑⋯.eigenvectorUnitary) i j‖ ^ 2
```
Uses
- HermitianMat.trace_single_conj
Used by
- HiddenChannelCapacity.inner_log_faithful

DeclHermitianMat.trace_single_conjDeclaration kindtheorem

∀ {d : Type u_1} [inst : Fintype d] [inst_1 : DecidableEq d] (C : Matrix d d ℂ) (i j : d),
  (Matrix.single i i 1 * C * Matrix.single j j 1 * C.conjTranspose).trace = C i j * star (C i j)

Uses

HermitianMat.trace_single_mul

Used by

HermitianMat.inner_cfc_cfc

DeclHermitianMat.trace_single_mulDeclaration kindtheorem

∀ {d : Type u_1} [inst : Fintype d] [inst_1 : DecidableEq d] (X : Matrix d d ℂ) (i : d),
  (Matrix.single i i 1 * X).trace = X i i

Used by

HermitianMat.trace_single_conj

HypothesishAC
```
ρAC.m.PosDef
```
HypothesishCB
```
ρCB.m.PosDef
```
Hypothesishcons
```
ρAC.traceLeft = ρCB.traceRight
```

DefinitionHiddenChannelCapacity.IsCompletiondef

A completion: a global state with the prescribed marginals (LZ M(R), p. 7).

{a : Type u_1} →
  {c : Type u_2} →
    {b : Type u_3} →
      [inst : Fintype a] →
        [inst_1 : DecidableEq a] →
          [inst_2 : Fintype c] →
            [inst_3 : DecidableEq c] →
              [inst_4 : Fintype b] →
                [inst_5 : DecidableEq b] → MState (a × c) → MState (c × b) → MState (a × c × b) → Prop

DefinitionHiddenChannelCapacity.IsMarkovCompletiondef

A quantum Markov completion: a completion with I(A:B|C) = 0 (LZ Def 2.4 quantum conditional independence + the Markov completion of p. 7).

{a : Type u_1} →
  {c : Type u_2} →
    {b : Type u_3} →
      [inst : Fintype a] →
        [inst_1 : DecidableEq a] →
          [inst_2 : Fintype c] →
            [inst_3 : DecidableEq c] →
              [inst_4 : Fintype b] →
                [inst_5 : DecidableEq b] → MState (a × c) → MState (c × b) → MState (a × c × b) → Prop

DefinitionHiddenChannelCapacity.TRdef

The logarithmic candidate T(R) = exp(log ρ_{AC} + log ρ_{CB} − log ρ_C) (LZ eq. 5). A Hermitian matrix, NOT a priori a state: its trace deficit is the subject of the theorem.

{a : Type u_1} →
  {c : Type u_2} →
    {b : Type u_3} →
      [inst : Fintype a] →
        [inst_1 : DecidableEq a] →
          [inst_2 : Fintype c] →
            [inst_3 : DecidableEq c] →
              [inst_4 : Fintype b] →
                [inst_5 : DecidableEq b] → MState (a × c) → MState (c × b) → HermitianMat (a × c × b) ℂ

DefinitionHiddenChannelCapacity.Tmatdef

The Hermitian exponent of the logarithmic candidate: the sum of the embedded logarithms of the marginals (log ρ_{AC} + log ρ_{CB} − log ρ_C, every operator embedded BEFORE exp; LZ eq. 5 with the p. 23 embedding convention; the separator marginal is taken from the AC side).

{a : Type u_1} →
  {c : Type u_2} →
    {b : Type u_3} →
      [inst : Fintype a] →
        [inst_1 : DecidableEq a] →
          [inst_2 : Fintype c] →
            [inst_3 : DecidableEq c] →
              [inst_4 : Fintype b] →
                [inst_5 : DecidableEq b] → MState (a × c) → MState (c × b) → HermitianMat (a × c × b) ℂ

DefinitionHiddenChannelCapacity.embedACdef

Embed an A∪C-local operator into the global system.

{a : Type u_1} → {c : Type u_2} → {b : Type u_3} → [DecidableEq b] → HermitianMat (a × c) ℂ → HermitianMat (a × c × b) ℂ

DefinitionHiddenChannelCapacity.embedCdef

Embed a C-local operator into the global system.

{a : Type u_1} →
  {c : Type u_2} → {b : Type u_3} → [DecidableEq a] → [DecidableEq b] → HermitianMat c ℂ → HermitianMat (a × c × b) ℂ

DefinitionHiddenChannelCapacity.embedCBdef

Embed a C∪B-local operator into the global system (tensoring with the identity, LZ p. 23).

{a : Type u_1} → {c : Type u_2} → {b : Type u_3} → [DecidableEq a] → HermitianMat (c × b) ℂ → HermitianMat (a × c × b) ℂ

DefinitionHiddenChannelCapacity.kleinTermdef
The scalar Klein term x log x − x log y − x + y (the integrand of Klein's inequality, LZ p. 5 / Ruskai 2002 Thm 3).
```
ℝ → ℝ → ℝ
```

DefinitionHiddenChannelCapacity.margACdef

The A∪C-marginal of a global state (LZ p. 4: reduced density operator).

{a : Type u_1} →
  {c : Type u_2} →
    {b : Type u_3} →
      [inst : Fintype a] →
        [inst_1 : DecidableEq a] →
          [inst_2 : Fintype c] →
            [inst_3 : DecidableEq c] →
              [inst_4 : Fintype b] → [inst_5 : DecidableEq b] → MState (a × c × b) → MState (a × c)

DefinitionHiddenChannelCapacity.margCdef

The C-marginal (the separator marginal), as the vendor composite the qcmi definition consumes.

{a : Type u_1} →
  {c : Type u_2} →
    {b : Type u_3} →
      [inst : Fintype a] →
        [inst_1 : DecidableEq a] →
          [inst_2 : Fintype c] →
            [inst_3 : DecidableEq c] → [inst_4 : Fintype b] → [inst_5 : DecidableEq b] → MState (a × c × b) → MState c

DefinitionHiddenChannelCapacity.margCBdef

The C∪B-marginal of a global state.

{a : Type u_1} →
  {c : Type u_2} →
    {b : Type u_3} →
      [inst : Fintype a] →
        [inst_1 : DecidableEq a] →
          [inst_2 : Fintype c] →
            [inst_3 : DecidableEq c] →
              [inst_4 : Fintype b] → [inst_5 : DecidableEq b] → MState (a × c × b) → MState (c × b)

DefinitionHiddenChannelCapacity.qDivRdef
The quantum relative entropy in real form, Tr[ρ (log ρ − log σ)] (LZ eq. 4 on density operators; equals the vendored qRelativeEnt by qRelativeEnt_rank when σ is nonsingular).
```
{d : Type u_4} → [inst : Fintype d] → [inst_1 : DecidableEq d] → MState d → MState d → ℝ
```

DefinitionHiddenChannelCapacity.sigTdef

The normalized candidate σ(R) = T(R)/Tr T(R): the state the equivalences of LZ Thm 3.1 are about.

{a : Type u_1} →
  {c : Type u_2} →
    {b : Type u_3} →
      [inst : Fintype a] →
        [inst_1 : DecidableEq a] →
          [Nonempty a] →
            [inst_3 : Fintype c] →
              [inst_4 : DecidableEq c] →
                [Nonempty c] →
                  [inst_6 : Fintype b] →
                    [inst_7 : DecidableEq b] → [Nonempty b] → MState (a × c) → MState (c × b) → MState (a × c × b)

DefinitionHiddenChannelCapacity.trCdef

The trace of the logarithmic candidate.

{a : Type u_1} →
  {c : Type u_2} →
    {b : Type u_3} →
      [inst : Fintype a] →
        [inst_1 : DecidableEq a] →
          [inst_2 : Fintype c] →
            [inst_3 : DecidableEq c] →
              [inst_4 : Fintype b] → [inst_5 : DecidableEq b] → MState (a × c) → MState (c × b) → ℝ

DefinitionMState.traceAlongdef

Trace out the second block of a coordinate split: the abstract partial-trace primitive of the L0 layer.

{d : Type u_1} →
  {a : Type u_2} →
    {b : Type u_3} →
      [inst : Fintype d] →
        [inst_1 : DecidableEq d] →
          [inst_2 : Fintype a] →
            [inst_3 : DecidableEq a] → [Fintype b] → [DecidableEq b] → MState d → d ≃ a × b → MState a

DefinitionMatrix.embedAlongdef
Embed an operator on one block of a coordinate split into the whole space (tensor with the identity, transported along the split): the dual of MState.traceAlong, and the paper's embedding convention ("tensoring with identities BEFORE logs") as a named primitive.
```
{R : Type u_1} →
  [NonAssocSemiring R] →
    {d : Type u_2} → {a : Type u_6} → {b : Type u_7} → [DecidableEq b] → d ≃ a × b → Matrix a a R → Matrix d d R
```

DOIMTH.R-2026-6021

Cite

Verification

Replay: accepted
Axioms: Classical.choiceQuot.soundpropext
Statement identity: not-applicable
Substrate: Lean 4 kernel v4.31.0
Dictionary pin: design-lab@5802df4 · initial
Frozen export: 90f091ee8510
Verified: 2026-09-24T00:00:00Z