weighted_log_average
plain-language theorem explainer
The weighted log average theorem shows that for any configuration of N positive entries the uniform average of their logarithms equals the total log charge divided by N. Variational dynamics proofs cite this identity when deriving Jensen bounds on total defect from the conserved charge. The proof reduces directly to the definition of log_charge via summation rewriting and ring simplification.
Claim. For integer $N > 0$ and configuration $c$ with positive real entries $c_i$, the uniform average satisfies $N^{-1} sum_{i=1}^N log(c_i) = log_charge(c)/N$, where $log_charge(c)$ is the sum of the logarithms of the entries.
background
The VariationalDynamics module formalizes ledger evolution as constrained global minimization of total J-cost subject to invariance of the total log-ratio (the charge). A Configuration N is the structure of N positive real entries supplied by InitialCondition, with the positivity proof attached. log_charge is the sum of the natural logs of these entries; its conservation follows from J-symmetry J(x) = J(1/x) already established in LawOfExistence and InitialCondition.
proof idea
The proof unfolds the definition of log_charge, rewrites the sum via the Finset.mul_sum lemma to factor out the constant 1/N, and finishes with the ring tactic for algebraic cancellation. It is a direct one-line algebraic identity with no external lemmas beyond basic summation arithmetic.
why it matters
This identity is invoked by the Jensen lower bound total_defect_lower_bound and the equality-case theorem eq_constant_config_of_defect_eq, both in the same module. It encodes the conservation law of the ledger's total log-ratio that underpins the variational update rule stated in the module documentation. In the Recognition Science framework it supplies the averaging step needed to relate the phi-ladder mass formula and the eight-tick octave to the global J-cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.