constant_config_total_defect
plain-language theorem explainer
The constant configuration with parameter μ across N ledger entries has total defect exactly N times Jlog μ. Variational dynamics proofs cite this to evaluate the cost of the uniform state that distributes conserved log-charge equally. The proof proceeds by direct unfolding of the definitions followed by simplification of the constant sum.
Claim. For any natural number $N$ and real number $μ$, the total defect of the constant configuration (all $N$ entries equal to $e^μ$) equals $N · Jlog(μ)$.
background
The module formalizes ledger evolution as constrained global minimization of total defect subject to fixed log-charge $σ = ∑ log(x_i)$. A Configuration N is a structure of N positive real entries. Total defect sums the individual J-costs of those entries. Jlog(t) is the log-domain cost Jcost(exp t) = ((exp t + exp(-t))/2) - 1. Upstream results include the Configuration definition and total_defect from InitialCondition, plus the Jlog definition from Cost.
proof idea
The term proof unfolds total_defect and constant_config, then applies simp on Finset.sum_const, Finset.card_univ, Fintype.card_fin and nsmul_eq_mul to reduce the sum of N identical terms, followed by rfl.
why it matters
This supplies the explicit defect value for the uniform configuration used to construct the variational successor in variational_step_exists and uniform_is_variational_successor. It confirms the AM-GM state achieves the minimal total defect under the conservation law, closing the step from the update principle to an explicit equation of motion in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.