log_charge
plain-language theorem explainer
The log-charge assigns to each ledger configuration the sum of the logarithms of its entries, serving as the real-valued conserved quantity under the variational update rule. Researchers modeling neutral sectors or Noether charges in Recognition Science would cite it when proving that parameter-free observables must be neutral. The definition is realized directly as summation of the logarithm over the finite index set of configuration entries.
Claim. For a configuration $c$ of $N$ positive real entries $c_i$, the log-charge is defined by $Q(c) := sum_{i=1}^N log(c_i)$.
background
The Variational Dynamics module supplies the missing update rule for the Recognition Science ledger: each step selects the configuration that minimizes total defect subject to the feasible set reachable in one tick. A configuration is the structure of $N$ positive real ratios introduced in InitialCondition, with the J-cost function $J(x) = (x + x^{-1})/2 - 1$ supplying the defect measure. The module doc states that the ledger conserves total log-ratio because J-symmetry implies the system tracks both $x$ and $1/x$, so the sum of logs is invariant under the constrained minimization.
proof idea
This is a direct definition realized as the summation of Real.log applied entrywise to the configuration vector indexed by Fin N. No auxiliary lemmas are invoked beyond the standard summation and logarithm primitives.
why it matters
The definition supplies the conserved charge used downstream in NeutralSector to prove neutral_ratio_eq_one and parameter_free_observables_are_neutral, and is lifted to a Noether charge in TopologicalConservation to show that such charges need not be quantized. It closes the conservation law required by the variational update principle in F-008, linking the J-uniqueness result to the eight-tick evolution and the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.