unity_log_charge_zero
plain-language theorem explainer
The all-ones configuration of the Recognition ledger carries zero total log-ratio. Workers on the variational dynamics of the ledger cite this to confirm charge neutrality of the initial state. The proof reduces directly by unfolding the definitions of log_charge and unity_config, applying the identity log(1) = 0, and summing the resulting zeros.
Claim. For any positive integer $N$, if $c$ denotes the configuration with all $N$ entries equal to 1, then the total log-ratio satisfies $c = 0$.
background
In the Variational Dynamics module the ledger evolves by constrained global J-cost minimization, subject to the conservation law that the total log-ratio of a configuration remains invariant. The log-ratio of a configuration is the sum of the natural logarithms of its entries; this quantity is the conserved charge of the ledger. The all-ones configuration is the zero-defect initial state in which every entry equals 1, as supplied by the upstream unity_config definition.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definitions of log_charge and unity_config, simplifies via the identity log(1) = 0, and concludes by the finite-sum property that the sum of zeros is zero.
why it matters
This lemma supplies the zero-charge property required by the downstream theorem unity_is_optimal, which shows that the all-ones state is feasible and globally minimal when log-charge vanishes. It anchors the conservation-law step inside the F-008 update principle, ensuring the initial state starts with zero net charge so that defect evolves non-increasingly from the J-minimum at unity. The result is consistent with the J-symmetry that forces log-ratios to sum to zero in balanced pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.