update_is_global
plain-language theorem explainer
The theorem establishes that the variational successor of a ledger configuration cannot always be realized by altering only one entry. Researchers modeling the non-local character of recognition dynamics would cite this result when arguing that global conservation constraints force simultaneous updates across multiple sites. The proof proceeds by direct construction of an explicit two-site example whose minimizer changes both entries while preserving log-charge and achieving zero total defect.
Claim. There exists a positive integer $N$, configurations $c$ and $next$ of $N$ positive real ratios, such that $next$ minimizes total defect among all configurations sharing the same log-charge as $c$, yet no single-entry modification (holding all other entries fixed) connects $c$ to $next$.
background
The module formalizes the ledger update rule as the global argmin of total defect subject to conservation of log-charge. A Configuration is a tuple of $N$ positive real ratios; total_defect sums the individual J-costs (where $J(x) = (x + x^{-1})/2 - 1$); log-charge is the sum of logarithms of the entries, which remains invariant under feasible updates. IsVariationalSuccessor holds when $next$ lies in the feasible set of $c$ and attains the minimal total defect among all such feasible states. LocalUpdate is the structure requiring that exactly one entry changes while all others remain identical.
proof idea
The tactic proof selects $N=2$ and the explicit pair $c = [2, 1/2]$, $next = [1, 1]$. It verifies the successor property by unfolding log_charge (both equal zero) and showing that any other feasible configuration has nonnegative total defect via defect_nonneg and sum_nonneg. It then rules out LocalUpdate by exhibiting that both entries differ and applying fin_cases on the changed_index to derive a contradiction in each case.
why it matters
This result supplies the concrete non-locality statement required by the variational dynamics module and directly supports the claim that every variational step yields a valid RecognitionStep in the TimeEmergence framework. It closes the gap between the abstract conservation law and an explicit equation of motion, confirming that the update depends on the entire configuration rather than isolated entries. The construction uses the same defect and log-charge primitives introduced in LawOfExistence and InitialCondition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.