Dual Repair Entropy Decomposition

Abstract

Canonical predictive-interior and forgetting-closure quotients split conditional entropy into the two repair costs.

Theorem 1.1 (Conditional entropy telescopes across both canonical repairs).

$$\begin{array}{c}\forall X:\mathrm{Type},F:X\to X,R:\mathrm{Setoid}(X),mu:X\to \mathbb{R},\\ \mathrm{Fintype}(X)\wedge (\forall x:X,0<mu(x))\wedge \sum _{x:X}mu(x)=1\Rightarrow \\ I:=\mathrm{congruenceInterior}(F,R),C:=\mathrm{congruenceClosure}(F,R),\\ Q_I:=\mathrm{Quotient}(\mathrm{congruenceInterior}(F,R)),Q_R:=\mathrm{Quotient}(R),\\ Q_C:=\mathrm{Quotient}(\mathrm{congruenceClosure}(F,R)),\\ f_I:=\mathrm{FintypeOfFinite}(Q_I),f_R:=\mathrm{FintypeOfFinite}(Q_R),\\ f_C:=\mathrm{FintypeOfFinite}(Q_C),\\ p{i}_{IR}:Q_I\to Q_R:=\mathrm{QuotientMap}(id,\mathrm{congruenceInterior}(F,R)\subseteq R),\\ p{i}_{RC}:Q_R\to Q_C:=\mathrm{QuotientMap}(id,R\subseteq \mathrm{congruenceClosure}(F,R)),\\ q_I:X\to Q_I:=(x\mapsto \mathrm{QuotientMk}(\mathrm{congruenceInterior}(F,R),x)),\\ m{u}_I:=\mathrm{pushforward}(q_I,mu),m{u}_R:=\mathrm{pushforward}(p{i}_{IR},m{u}_I),\\ \mathrm{Hcond}(\mathrm{pushforward}((i\mapsto (p{i}_{RC}(p{i}_{IR}(i)),i)),m{u}_I))=\mathrm{Hcond}(\mathrm{pushforward}((r\mapsto (p{i}_{RC}(r),r)),m{u}_R))+\mathrm{Hcond}(\mathrm{pushforward}((i\mapsto (p{i}_{IR}(i),i)),m{u}_I)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Observation/DualRepairEntropyDecomposition.dual_repair_entropy_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let X be finite, let F update X, let R be an equivalence relation, and let mu be a normalized law with positive mass at every state. The predictive interior and forgetting closure are the imported canonical congruence repairs.

Their inclusion proofs induce canonical quotient maps from X/I to X/R and from X/R to X/C. The displayed laws are deterministic pushforwards of mu along these quotient maps, so no entropy target is used to define a source object.

Applying the repository quotient-fiber entropy decomposition to I to C, I to R, and R to C gives three entropy balances. Pushforward composition identifies the two closure laws, and the balances telescope to the claimed equality.

Pinned Mathlib and installed-package searches found no finite real-valued conditional-entropy theorem with these canonical repair quotients.

References

• Truth anchor: D5/S3/Entropy/Observation/DualRepairEntropyDecomposition.dual_repair_entropy_decomposition
• Dependency: D5/S3/Entropy/Fusion/QuotientFiberDecomposition
• Dependency: D5/S3/Observer/Separation/CongruenceClosureDuality