constant_config
plain-language theorem explainer
The constant_config definition supplies the uniform ledger state with every entry equal to exp(μ) for a given charge parameter μ. Researchers working on the variational update rule cite it when constructing the explicit minimizer of total defect under fixed log-charge. The definition is a direct record construction that satisfies the positivity requirement by the exponential function's range.
Claim. For each natural number $N$ and real number $μ$, the configuration $c$ of $N$ ledger entries is defined by $c_i = e^μ$ for all $i=1,…,N$.
background
Configuration N is the structure of N positive real numbers representing ledger entries, as defined in InitialCondition. The module VariationalDynamics formalizes the ledger's evolution by minimizing total J-cost subject to conserved log-charge. Upstream, LawOfExistence establishes J(x) = (x + 1/x)/2 - 1 with unique minimum at x=1, while Determinism ensures uniqueness of minimizers via strict convexity.
proof idea
Direct definition: the entries field is the constant function returning Real.exp μ, and positivity follows immediately from Real.exp_pos.
why it matters
This definition provides the explicit form of the uniform configuration that serves as the variational successor in uniform_is_variational_successor and variational_step_exists. It realizes the AM-GM optimal distribution of conserved charge, closing the gap between the energy landscape and the explicit equation of motion for the ledger. In the Recognition Science framework it instantiates the constrained global J-cost minimization principle of F-008.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.