entropy_decomposition
plain-language theorem explainer
Total RS entropy of a configuration equals observer entropy plus system entropy for any subsystem partition. Thermodynamic arguments that treat the unseen ledger entries as a heat bath cite this identity. The proof is a short Finset sum split: unfold the four entropy defs and reassociate the sum over observer indices and their complement.
Claim. For any $N\in\mathbb{N}$, any subsystem partition $S$ of the $N$ ledger entries, and any configuration $c$, the total entropy equals the sum of the entropy on the observer indices and the entropy on the complementary system indices: $S_{\mathrm{RS}}(c)=S_{\mathrm{obs}}(S,c)+S_{\mathrm{sys}}(S,c)$.
background
Module F-011 builds temperature and the canonical ensemble from the ledger J-cost and a finite-resolution observer. Entropy is identified with total defect: for a configuration $c$ of $N$ positive ledger ratios, $S_{\mathrm{RS}}(c)=\sum_i J(x_i)$, where defect is the cost functional $J$ from LawOfExistence. That identification already lives in InitialCondition as total_defect.
A Subsystem (from MeasurementMechanism) partitions ${0,\ldots,N-1}$ into observer indices of cardinality $K$ and the complementary system indices of size $N-K$. Observer entropy and system entropy are the restrictions of the defect sum to those two index sets. The module's key physical claim is that the unseen complement acts as a heat bath for the coarse-grained observer; the present identity is the additive bookkeeping that makes that split legitimate.
Upstream, Configuration packages the $N$ positive entries, and defect is pointwise $J$. Commutativity of addition is used only to match the order of the two partial sums.
proof idea
Term-mode, three steps. Unfold rs_entropy, total_defect, observer_entropy, and system_entropy so both sides are Finset sums of defect over index sets. Rewrite the full sum as the sum over the observer indices plus the sum over the set difference (universe minus observer indices) via Finset.sum_sdiff and the fact that observer indices are a subset of the universe. Finish with simpa using the definition of system indices as that complement and add_comm to align summand order.
why it matters
This is Step-1 bookkeeping in the F-011 thermodynamic derivation: once total entropy is total defect, any observer/system cut must split that defect additively. Without the split, one cannot define observer entropy, system entropy, or the later equilibrium and temperature constructions that treat the complement as a bath (siblings such as equilibrium_entropy, rs_temperature, and the canonical-ensemble section that follows immediately in the file).
In the broader Recognition chain this sits after entropy-as-defect (InitialCondition), observers-as-subsystems (MeasurementMechanism), and variational dynamics; it does not itself invoke T5–T8 or the RCL, but it is the additive hinge that lets those ledger structures speak the language of $S=S_{\mathrm{obs}}+S_{\mathrm{sys}}$. No downstream theorems currently depend on it in the graph, so it is infrastructure awaiting the temperature and ensemble theorems in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.