rs_entropy_zero_iff_unity
plain-language theorem explainer
RS entropy of an N-entry ledger configuration vanishes if and only if every entry equals 1 (the unity configuration). Thermodynamic and equilibrium arguments in the foundation layer cite this as the unique zero-entropy state. The proof is a one-line transfer of the zero-total-defect uniqueness theorem, since entropy is defined as total defect.
Claim. For $N > 0$ and any configuration $c$ of $N$ positive real ledger entries, the RS entropy $S(c) := \sum_i J(x_i)$ satisfies $S(c) = 0$ if and only if $x_i = 1$ for every index $i$.
background
In the Foundation thermodynamics module (F-011), entropy and temperature are built from the ledger's J-cost structure rather than postulated. A configuration of $N$ entries is a map from $\mathrm{Fin}, N$ to positive reals: each entry is a ratio $x_i > 0$. The individual cost is the unique J-functional $J(x) = (x + x^{-1})/2 - 1$ forced earlier in the chain; total defect is the sum of these costs.
RS entropy is defined by identifying $S(c)$ with that total defect. The module doc records the standing facts: $S \ge 0$ always, and $S = 0$ precisely at unity. Energy is the separate conserved log-charge $\sum_i \log x_i$. Temperature later appears only at the observer level, as a Lagrange multiplier for a coarse-grained subsystem against an unseen heat bath.
The upstream theorem zero_defect_iff_unity (F-005 core) already states that total defect vanishes iff every entry is 1, using nonnegativity of each J-term and the fact that $J(x) = 0$ forces $x = 1$.
proof idea
One-line term wrapper. Because rs_entropy c is definitionally total_defect c, the claim is exactly zero_defect_iff_unity hN c. No extra algebra or case split is performed here; the uniqueness of the zero-defect (hence zero-entropy) configuration is inherited wholesale from InitialCondition.
why it matters
This is Step 1 of the F-011 thermodynamic derivation: entropy as defect count, with the unique zero at unity. It pins the ground state of the canonical picture before energy, equilibrium entries, and temperature are introduced in the same module (siblings include rs_entropy_nonneg, rs_energy_unity, equilibrium_entropy_zero_iff, rs_temperature).
In the broader Recognition framework it ties the thermodynamic ground state to the J-cost minimum forced by T5 (J-uniqueness) and to the law-of-existence defect calculus. Without a unique zero-entropy configuration, the later identification of equilibrium and the observer heat-bath construction would lack a reference state. No downstream dependents are recorded yet; the immediate consumers are the equilibrium and temperature definitions in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.