uniform_config_charge
plain-language theorem explainer
The theorem asserts that the uniform configuration of length N with parameter σ has log-charge exactly σ. Researchers deriving the explicit update rule for the Recognition Science ledger would cite it to confirm charge conservation under the variational successor. The proof is a direct term-mode calculation that unfolds the definitions and simplifies the finite sum of logarithms.
Claim. For positive integer $N$ and real number σ, let $c$ be the uniform configuration of length $N$ with charge σ. Then the log-charge of $c$ equals σ.
background
The Variational Dynamics module supplies the missing update rule for the ledger: state(t+1) is the argmin of total J-cost over configurations reachable in one tick while preserving the total log-ratio (the charge). log_charge sums the logarithms of the entries; uniform_config builds the constant vector whose entries are each exp(σ/N). This rests on the convexity of J established in LawOfExistence and the uniqueness of minimizers from Determinism.
proof idea
The term proof unfolds log_charge and uniform_config, applies simp to replace log(exp(·)) by the identity, then rewrites the sum of N identical terms via Finset.sum_const together with the cardinality of Fin n. The final exact step invokes Nat.cast_ne_zero on the positive integer N to clear the division.
why it matters
The result verifies that the explicit uniform solution satisfies the conservation law required by the equation of motion. It directly supports the module claim that the uniform distribution minimizes total J-cost subject to fixed log-sum (via Jensen). The declaration sits inside the F-008 chain that closes the gap between the energy landscape and the concrete dynamics; downstream results on constant_config and weighted averages rely on this charge preservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.