ratioConfig_log_charge
plain-language theorem explainer
For a positive real ratio packaged as a one-channel ledger configuration, the conserved log-charge equals the ordinary logarithm of that ratio. Anyone working the neutral-sector ground-state argument cites this as the bridge from configuration data to the scalar charge. The proof is a two-step unfold-and-simp of the sum definition on a singleton index type.
Claim. Let $r > 0$. If $c_r$ is the one-channel configuration whose single positive entry equals $r$, then the total log-charge of $c_r$ equals $\log r$.
background
The module develops the B4-style ground-state claim from the variational ledger update: equilibria are variational minimizers; in a zero-charge sector the unique equilibrium is the unity configuration; stability of a one-channel ratio observable therefore forces that ratio to $1$.
A configuration of length $N$ is a positive $N$-tuple of ledger entries. The conserved charge is the total log-ratio
$$\mathrm{log_charge}(c)=\sum_{i}\log(c_i),$$
which the variational dynamics preserve under feasible one-tick updates. The helper ratioConfig packages a single positive real $r$ as a length-$1$ configuration with that sole entry, so the sum collapses to one term.
Upstream, the cost projector and $J$-structure fix the variational cost on positive reals; here only the charge bookkeeping is needed.
proof idea
Term-mode proof by definition chase. Unfold the charge sum and the one-channel packaging; the index type is Fin 1, so the sum is a single logarithm of the unique entry $r$. simp closes the equality. No external lemmas beyond the definitions are required.
why it matters
This simp lemma is the scalar identification step inside the ground-state chain: once charge is computed on ratio configurations, the zero-charge sector becomes the condition $\log r = 0$, hence $r = 1$ for stable one-channel ratios (the sibling claim that neutral stable ratios are forced to unity). That is exactly the module's third bullet: stability of a one-channel ratio observable forces $r = 1$.
In the broader Recognition framework the conserved log-charge is the ledger neutral-sector constraint that sits under the variational dynamics feeding the forcing chain (equilibria as minimizers, unique unity ground state). The declaration itself is local bookkeeping rather than a T0–T8 landmark, but without it the passage from configuration data to the scalar neutrality condition does not typecheck. No downstream edges are recorded yet; the natural consumer is the stable-unity theorem in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.