weighted_log_average
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish conservation of log_charge under time evolution.
- Does not apply to non-uniform weights or configurations with non-positive entries.
- Does not invoke the J-cost or Jlog functions themselves.
- Does not depend on the specific value of phi or the alpha band.
Lean usage
have h_avg := weighted_log_average hN cformal statement (Lean)
137private theorem weighted_log_average {N : ℕ} (hN : 0 < N) (c : Configuration N) :
138 (∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) * Real.log (c.entries i)) =
139 log_charge c / N := by
proof body
Term-mode proof.
140 unfold log_charge
141 rw [← Finset.mul_sum]
142 ring
143
144/-- Weighted average of `Jlog(log x_i)` equals `total_defect / N`. -/