total_defect_lower_bound
plain-language theorem explainer
The theorem proves that for any configuration of N positive entries with fixed log-charge σ, the total defect is bounded below by N times Jlog(σ/N). Researchers formalizing the ledger's variational update rule cite it to establish that the uniform configuration achieves minimal defect. The proof applies Jensen's inequality to the strictly convex Jlog function with uniform weights 1/N on the log-entries, followed by algebraic rearrangement.
Claim. Let $N$ be a positive integer and $c$ a configuration of $N$ positive real entries. Let $σ = ∑_{i=1}^N log(c_i)$ denote the conserved log-charge. Then $N · Jlog(σ/N) ≤ ∑_{i=1}^N Jlog(log c_i)$, where $Jlog(t) = (e^t + e^{-t})/2 - 1$.
background
In the VariationalDynamics module the ledger state evolves by constrained global minimization of total defect subject to conservation of log-charge. A Configuration N consists of N positive real entries; log_charge c is their sum of logarithms; total_defect c is the sum of Jlog(log entries_i). Jlog itself is defined by composing the base J-cost with the exponential, yielding the explicit form (cosh t - 1). The module builds directly on LawOfExistence (unique minimum of J at 1) and InitialCondition (zero-defect starting state), together with the strict-convexity result Jlog_strictConvexOn.
proof idea
The proof first records that the weights 1/N are nonnegative and sum to 1. It invokes Jlog_strictConvexOn.convexOn.map_sum_le on the logs of the entries. After rewriting the left-hand side via weighted_log_average and the right-hand side via weighted_Jlog_average, the resulting inequality is multiplied through by N to obtain the stated bound.
why it matters
This lower bound is the central inequality used to prove that the uniform configuration is the unique variational successor (see uniform_is_variational_successor, variational_step_exists and variational_step_unique). It supplies the concrete content of the update rule state(t+1) = argmin total_defect subject to fixed log-charge, closing the gap between the energy landscape and the explicit equation of motion. The result sits inside the Recognition Science forcing chain at the point where J-uniqueness and strict convexity determine the dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.