constant_config_log_charge
plain-language theorem explainer
The constant configuration of N ledger entries each equal to exp(μ) has total log-charge exactly Nμ. Researchers constructing the explicit uniform minimizer for the constrained J-cost update in the Recognition ledger cite this identity to distribute conserved charge equally. The proof is a direct term-mode unfolding of log_charge and constant_config followed by simplification of the constant sum.
Claim. Let $c$ be the configuration of $N$ ledger entries where each entry equals $e^μ$. Then the log-charge of $c$, defined as the sum of the logarithms of its entries, satisfies $∑_{i=1}^N log(c_i) = Nμ$.
background
The Variational Dynamics module formalizes the ledger update as constrained global minimization of total defect subject to invariance of total log-ratio (the charge). A Configuration N is a structure whose entries field is a function Fin N → ℝ with all values positive. The constant configuration sets every entry to exp(μ). Log-charge is the sum of log(entries i), which the module documentation states is conserved because J-symmetry implies the ledger tracks both x and 1/x.
proof idea
The term proof unfolds the definitions of log_charge and constant_config, applies simp only [Real.log_exp] to replace each log(exp μ) by μ, then rewrites the sum of a constant value over the finite index set using Finset.sum_const, Finset.card_univ, Fintype.card_fin and nsmul_eq_mul to obtain the factor N.
why it matters
This identity supplies the charge value of the uniform configuration that is exhibited as the variational successor in variational_step_exists and uniform_is_variational_successor. It realizes the explicit solution for the update rule of F-008 by confirming that the AM-GM-optimal configuration preserves the total charge σ as N·(σ/N). In the Recognition framework it closes the step from conserved charge to the concrete minimizer of total defect, consistent with the eight-tick octave and the global consistency requirement of the ledger evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.