theorem CommutingRepetition.TracialStrategy.history_relative_entropy {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (hw1 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), w xw yw zA zB ≤ 1) (hwD : ∀ (xw xw' : Fin n → X) (yw yw' : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), agreesOn D xw xw' → agreesOn D yw yw' → w xw yw zA zB = w xw' yw' zA zB) {p : ℝ} (hp : p = S.coreMass D μ w) (hppos : 0 < p) (hm : D.card < n) : Pinsker.finiteRelativeEntropy (S.flatQ R D μ w p) (S.flatJA R D μ w p) ≤ (3 * Real.log p⁻¹ + 2 * (↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B)))) / (↑n - ↑D.card) ∧ Pinsker.finiteRelativeEntropy (S.flatQ R D μ w p) (S.flatJB R D μ w p) ≤ (3 * Real.log p⁻¹ + 2 * (↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B)))) / (↑n - ↑D.card)

History closeness (node 1.2.10; 05_prerounding.tex, eq history-relative-entropy): D(ℚ ‖ J_A), D(ℚ ‖ J_B) ≤ (3t₀ + 2s₀)/m with t₀ = log(1/p), s₀ = |D|·log(|A||B|), m = n − |D|. The proof is the KL chain rule (eq JA-chain-rule), tensorization + data processing for the first term (eq first-history-chain-term), and the reverse-experiment chain rule with the uniform cut for the second (eqs bob-block-conditioning-budget through second-history-chain-term), using the conditioning budget eq question-answer-conditioning-budget (itself from D(ℚ‖ℙ) = t₀, eq conditioning-divergence, and the s₀-cost of adjoining the core word). Classical given the branch masses: no entropy budget is consumed.