unity_unique_minimizer
plain-language theorem explainer
The theorem shows that for any positive integer N and configuration c of N ledger entries, equality of total defect with the all-ones unity configuration forces every entry of c to equal 1. Cosmologists addressing the initial low-entropy state would cite it to close the uniqueness half of the Past Theorem. The proof is a term-mode reduction that rewrites the unity defect to zero then applies the forward direction of the zero-defect equivalence.
Claim. Let $N$ be a positive integer and let $c$ be a configuration of $N$ positive real ledger entries. If the total defect of $c$ equals the total defect of the configuration with every entry equal to 1, then every entry of $c$ equals 1.
background
The module F-005 formalizes the initial low-entropy state as the unique zero-cost configuration forced by the cost axioms. A Configuration is the structure with entries : Fin N → ℝ together with the positivity condition ∀ i, 0 < entries i. total_defect sums LawOfExistence.defect over the entries; entropy is defined to be identical to total_defect, so zero defect is minimum entropy. unity_config N hN is the all-ones configuration whose defect vanishes by the upstream lemma unity_defect_zero.
proof idea
The term proof first rewrites the right-hand side via unity_defect_zero hN to obtain total_defect c = 0, then applies the forward implication of zero_defect_iff_unity hN c.
why it matters
The result supplies the uniqueness direction required by the module doc-comment for F-005, turning the Past Hypothesis into the Past Theorem that the initial state is the unique zero-defect configuration. It sits downstream of unity_defect_zero and zero_defect_iff_unity and alongside unity_is_global_minimum in the same module. No further uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.