zero_defect_iff_unity
plain-language theorem explainer
A configuration of N ledger entries has vanishing total defect precisely when every entry equals one. Cosmologists resolving the low-entropy initial condition cite this biconditional as the core of the Past Theorem. The proof splits into two directions: non-negative summands summing to zero must each vanish, then applies the zero-defect characterization at unity; the converse follows by direct summation.
Claim. For positive integer $N$ and configuration $c$ of $N$ positive real entries, the sum of defects equals zero if and only if every entry equals 1, where defect of an entry $x$ is the J-cost $J(x) = (x + x^{-1})/2 - 1$.
background
In the Initial Condition module a Configuration of $N$ entries is a structure whose entries map Fin $N$ to positive reals. Total defect is defined as the sum over all entries of the individual defect, where defect coincides with the J-cost from the Law of Existence. The module formalizes the low-entropy initial state: the only configuration with total defect zero is the all-unity one, turning the Past Hypothesis into a theorem.
proof idea
Constructor splits the biconditional. Forward: assume total defect zero; by contradiction obtain a positive defect term, apply single_le_sum together with defect_nonneg to reach a positive sum, contradicting zero; then invoke defect_zero_iff_one on each term. Reverse: rewrite total_defect, apply sum_eq_zero, and substitute defect_one for each entry.
why it matters
This equivalence supplies the core step of F-005, feeding directly into past_theorem (which asserts the unique zero-defect configuration is the low-entropy initial state) and unity_unique_minimizer. It is also invoked in static_ground_state_impossible and stillness_is_creative to derive that recognition cannot coexist with perfect uniformity. It closes the link from J-uniqueness (T5) to the forced initial condition with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.