uniform_config
plain-language theorem explainer
uniform_config constructs the ledger state in which all N entries equal exp(σ/N). Researchers formalizing the variational update rule cite it as the explicit candidate that preserves total log-charge σ under the constrained J-minimization. The definition directly populates the Configuration structure with the constant exponential value and invokes the positivity of the exponential.
Claim. For positive integer $N$ and real charge parameter $σ$, the uniform configuration is the $N$-tuple of positive reals in which every entry equals $e^{σ/N}$.
background
The module formalizes the ledger update as the global argmin of TotalDefect subject to the Feasible set, with the conservation law that the sum of log-entries (the charge) is invariant. Configuration, imported from InitialCondition, is the structure whose entries field is a map from Fin N to positive reals. The uniform construction mirrors the uniform distribution from ShannonEntropy but applied to the ledger ratios rather than probabilities.
proof idea
Direct definition that sets entries to the constant function returning Real.exp(σ/N) and supplies the positivity witness via Real.exp_pos. No upstream lemmas are invoked beyond the standard library facts on the exponential.
why it matters
The definition supplies the explicit form required by the downstream theorems uniform_config_charge and uniform_is_variational_successor. The latter states that this configuration is the variational successor for any input with the same charge, thereby giving the concrete equation of motion for the ledger. It realizes the conservation law described in the module documentation and supplies the constant-charge case needed for the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.