unity_is_optimal
plain-language theorem explainer
When a configuration has zero total log-charge, the uniform all-ones state is feasible from it and achieves the global minimum total defect. Ledger-dynamics researchers cite this to anchor the variational update rule at the initial zero-charge state. The proof is a direct term-mode verification that unity preserves zero charge and that its zero defect bounds every other feasible configuration from below.
Claim. Let $c$ be a configuration of $N$ positive real entries with total log-charge zero. Then the uniform configuration $1$ (all entries equal to 1) lies in the feasible set of $c$ and satisfies total defect of $1$ less than or equal to total defect of every other feasible configuration from $c$.
background
The module formalizes the ledger update as the constrained global minimization of total defect subject to log-charge conservation. A Configuration is a tuple of $N$ positive real ratios. Total defect is the sum of individual defects, each given by the J-cost $J(x) = (x + x^{-1})/2 - 1$. The uniform configuration unity_config has every entry equal to 1. Upstream lemmas establish that total defect is nonnegative for any configuration and exactly zero for unity_config.
proof idea
The term-mode proof constructs the IsVariationalSuccessor predicate directly. It first rewrites the log-charge of unity_config to zero using the unity_log_charge_zero lemma together with the zero-charge hypothesis. It then rewrites the defect of unity_config to zero and applies total_defect_nonneg to an arbitrary feasible configuration.
why it matters
This result supplies the explicit minimizer for the zero-charge case of the variational update rule defined in the module. It instantiates the J-uniqueness property from LawOfExistence and the nonnegativity of defect from InitialCondition, confirming that the ledger begins at the global minimum when charge vanishes. The lemma therefore closes the base case needed to define the RecognitionStep evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.