unity_unique_minimizer
plain-language theorem explainer
Any configuration of N ledger entries whose total defect matches that of the unity configuration must have every entry equal to 1. Foundational work on the initial state in Recognition Science cites this to establish uniqueness of the zero-cost starting point. The proof rewrites the unity defect to zero then applies the zero-defect equivalence in one direction.
Claim. Let $N$ be a positive integer and let $c$ be a configuration of $N$ ledger entries. If the total defect of $c$ equals the total defect of the unity configuration on $N$, then every entry of $c$ equals 1.
background
A Configuration of $N$ ledger entries is a structure whose entries field maps each index in Fin $N$ to a positive real ratio, with the positivity condition enforced. Total defect sums the individual defects of these entries, where each defect is supplied by the LawOfExistence module. Entropy is defined directly as this total defect, so zero defect is the minimum-entropy state. The module F-005 formalizes the initial condition by showing that the only RSExists state is the ratio 1, that a ledger of all such entries has total defect zero, and that this zero is the unique minimum.
proof idea
The term proof first rewrites the right-hand side using unity_defect_zero to obtain total_defect c = 0. It then applies the forward direction of zero_defect_iff_unity to conclude that c must be the unity configuration, forcing every entry to equal 1.
why it matters
This theorem supplies the uniqueness step inside the F-005 argument that converts the Past Hypothesis into the Past Theorem. It closes the loop from the cost axioms to the claim that the initial state is the unique zero-defect configuration, directly supporting the low-entropy initial condition required by the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.