variational_step_unique
plain-language theorem explainer
If two configurations both minimize total defect over the feasible set from the same current configuration of length N, then they share identical entries. Researchers establishing deterministic ledger evolution in Recognition Science cite this to close the uniqueness gap in the variational update rule. The proof exhibits the uniform constant configuration as the shared minimizer, equates both successors to it via defect equality and the characterization of minimizers, then equates their log-charges.
Claim. Let $N$ be a positive integer and $c$ a configuration of length $N$. If $next_1$ and $next_2$ both minimize total defect over the feasible set from $c$ (i.e., each satisfies the log-charge conservation constraint and achieves the global minimum defect), then the entries of $next_1$ equal those of $next_2$.
background
The module formalizes the ledger update as state(t+1) equals the argmin of total defect over configurations reachable in one tick while conserving total log-charge. IsVariationalSuccessor encodes exactly this: the successor lies in the feasible set and attains the minimal defect value among all feasible states. Configuration N is the type of N-tuples of positive reals whose log-charge (sum of logs) is conserved; total_defect sums Jlog over the entries, where Jlog(t) = Jcost(exp t) and Jcost is the Recognition cost function with unique minimum at 1.
proof idea
The tactic proof first constructs the constant configuration whose every entry equals the average log-charge; this state is feasible and achieves the absolute minimal defect. Both successors are shown to match this minimal defect value by mutual comparison against the uniform state, using antisymmetry of ≤. Each successor is then identified with the uniform configuration by the characterization that any state attaining the minimal defect must be constant. The shared log-charge value then forces the two constant configurations to coincide.
why it matters
This uniqueness supplies the missing determinism step for the variational dynamics module, directly feeding the theorem that any two trajectories obeying the update rule from the same initial state remain identical for all time. It realizes the core claim in the module documentation that the next state is unique, closing the gap between the energy landscape (from LawOfExistence and Determinism) and an explicit equation of motion. The result sits inside the forcing chain that derives D=3 and the eight-tick octave from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.