weighted_Jlog_average
plain-language theorem explainer
The weighted average of Jlog applied to the log of each ledger entry equals total defect divided by N. Researchers deriving Jensen bounds for ledger evolution cite this identity to equate per-entry log costs with the global defect sum. The proof is a direct calc that substitutes the Jlog definition via exp_log and factors the sum.
Claim. For a configuration $c$ of $N$ positive entries, let $J$ denote the defect functional. Then $N^{-1} sum_i J_{log}(log c_i) = N^{-1} total_defect(c)$, where $J_{log}(t) := J(e^t)$.
background
The Variational Dynamics module supplies the missing update rule for the Recognition ledger: each step selects the feasible configuration minimizing total defect while preserving log-charge. A Configuration is a finite vector of positive reals; total_defect sums the individual defects. Jlog composes the defect functional with the exponential so that costs can be written directly in the log domain. This rests on LawOfExistence, which defines defect as the J function with unique minimum at unity, and on InitialCondition, which introduces the Configuration structure together with the total_defect sum.
proof idea
The proof uses a calc chain. The first equality applies Finset.sum_congr to replace each Jlog(Real.log(entry_i)) by defect(entry_i), unfolding Jlog and invoking Real.exp_log. The second step unfolds total_defect and rewrites the sum via mul_sum.
why it matters
This identity is invoked by total_defect_lower_bound and eq_constant_config_of_defect_eq inside the same module. It converts the average log-domain cost into the global defect measure, enabling the constrained minimization that defines the ledger time step. In the broader framework it links the J-cost functional to the log-charge conservation law that survives each tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.