variational_step_unique
plain-language theorem explainer
The uniqueness theorem for variational steps asserts that any two configurations minimizing total defect subject to log-charge conservation from a given current state must have identical entries. Researchers deriving deterministic ledger evolution from the Recognition Science framework cite this to guarantee a single next state at each tick. The proof exhibits the constant configuration with preserved average log-charge as the unique minimizer and shows both candidates equal it by defect equality and charge preservation.
Claim. Let $N > 0$ be a natural number and let $c$ be a configuration of $N$ entries. Suppose next$_1$ and next$_2$ are both variational successors of $c$, i.e., each lies in the feasible set from $c$ and attains the minimal total defect among all feasible configurations from $c$. Then the entry vectors of next$_1$ and next$_2$ coincide.
background
The VariationalDynamics module supplies the explicit update rule for the Recognition Science ledger: the next state is the global minimizer of total defect over the feasible set defined by conservation of total log-charge. The predicate IsVariationalSuccessor c next holds precisely when next belongs to the feasible set from c and total_defect next equals the infimum of total_defect over that set. This construction rests on the J-cost Jlog(t) = ((e^t + e^{-t})/2) - 1 whose strict convexity, established in the upstream LawOfExistence and Determinism modules, forces uniqueness of minimizers. The module_doc states that prior results had shown defect is non-increasing but had left the concrete dynamics unspecified.
proof idea
The proof first constructs the uniform configuration u with every entry exp((log_charge c)/N) and verifies it is a variational successor by direct computation of its log_charge together with the total_defect_lower_bound. For each given successor next_i it obtains total_defect next_i = N * Jlog(avg) by applying the minimality property of next_i to u and the minimality property of u to next_i, then invoking le_antisymm. It next applies eq_constant_config_of_defect_eq to conclude that next_i must itself be the constant configuration carrying the preserved charge. The two charges are identical by the IsVariationalSuccessor hypotheses, so the constant configurations coincide and therefore the entry vectors are equal.
why it matters
This theorem supplies the uniqueness half of the variational update rule and is invoked directly by the downstream variational_dynamics_deterministic to conclude that entire trajectories are uniquely determined by the initial configuration. It realizes the determinism promised in the Determinism module and completes the equation-of-motion description in the module_doc. Within the Recognition Science chain it closes the gap between non-increasing defect (TimeEmergence) and the uniqueness required for a well-defined dynamics, thereby enabling the eight-tick octave and spatial-dimension derivations that rest on deterministic evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.