uniform_is_variational_successor
plain-language theorem explainer
The theorem states that for any positive integer N and configuration c of N entries, the uniform configuration sharing the total log-charge of c is its variational successor. Researchers modeling the deterministic ledger evolution in Recognition Science would cite this as the explicit closed-form update rule. The proof is a term-mode verification that rewrites the uniform state to a constant configuration, confirms the log-charge match, and invokes the total defect lower bound to establish minimality.
Claim. Let $N$ be a positive integer and $c$ a configuration of $N$ positive real entries with log-charge $σ = ∑ log(c_i)$. The uniform configuration with every entry equal to $exp(σ/N)$ is the variational successor of $c$: it lies in the feasible set from $c$ and attains the minimal total defect among all configurations in that set.
background
The VariationalDynamics module supplies the missing update map for the Recognition Science ledger. IsVariationalSuccessor(current, next) holds when next is feasible from current and total_defect(next) is minimal over the feasible set. A Configuration N is a tuple of N positive reals; total defect sums the individual J-costs with J(x) = (x + x^{-1})/2 - 1. The module builds on LawOfExistence (J has unique minimum at 1) and Determinism (strict convexity forces unique minimizers). The conservation law states that ∑ log(entries) is invariant under feasible updates.
proof idea
The term proof applies simpa with the uniform_config and constant_config rewrites to reduce the claim to the two clauses of IsVariationalSuccessor. The log-charge clause follows by rewriting constant_config_log_charge and canceling the factor 1/N using hN. The minimality clause applies total_defect_lower_bound to an arbitrary feasible c' and substitutes the shared log-charge hypothesis.
why it matters
This supplies the concrete equation of motion state(t+1) = argmin {TotalDefect(s) : s feasible from state(t)}, completing the F-008 certificate on variational dynamics. It identifies uniform distributions as fixed points, consistent with the equilibrium property in the module summary. The result rests on J-uniqueness (T5) and the log-charge conservation from LawOfExistence; it closes the gap between the cost landscape and the explicit update rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.