update_is_global
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.
claimThere 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 in Recognition Science
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.
scope and limits
- Does not claim every variational update changes multiple entries.
- Does not provide a closed-form expression for the general minimizer.
- Does not address continuous-time limits or infinite $N$.
- Does not quantify how often non-local updates occur.
formal statement (Lean)
426theorem update_is_global :
427 ∃ (N : ℕ) (hN : 0 < N) (c next : Configuration N),
428 IsVariationalSuccessor c next ∧
429 ¬∃ lu : LocalUpdate c next, True := by
proof body
Tactic-mode proof.
430 use 2, (by norm_num : 0 < 2)
431 -- Consider c with entries [2, 1/2] (log-charge = 0).
432 -- The variational successor is [1, 1] (also log-charge = 0).
433 -- This changes BOTH entries, so no local update suffices.
434 let c : Configuration 2 := {
435 entries := fun i => if i.val = 0 then 2 else 1/2
436 entries_pos := fun i => by
437 fin_cases i <;> norm_num
438 }
439 let next : Configuration 2 := {
440 entries := fun _ => 1
441 entries_pos := fun _ => by norm_num
442 }
443 use c, next
444 constructor
445 · constructor
446 · -- Feasibility: log_charge [1,1] = log(1) + log(1) = 0
447 -- log_charge [2, 1/2] = log(2) + log(1/2) = log(2) - log(2) = 0
448 show log_charge next = log_charge c
449 unfold log_charge
450 simp [Fin.sum_univ_two, next, c]
451 · -- Minimality: [1,1] has zero total defect, which is minimal
452 intro c' _
453 unfold total_defect
454 have h_next : ∀ i : Fin 2, next.entries i = 1 := fun _ => rfl
455 simp only [h_next, defect_at_one, Finset.sum_const_zero]
456 exact Finset.sum_nonneg (fun i _ => defect_nonneg (c'.entries_pos i))
457 · -- No local update: both entries change (2 → 1 and 1/2 → 1)
458 intro ⟨lu, _⟩
459 have h0 : next.entries ⟨0, by norm_num⟩ ≠ c.entries ⟨0, by norm_num⟩ := by
460 show (1 : ℝ) ≠ 2
461 norm_num
462 have h1 : next.entries ⟨1, by norm_num⟩ ≠ c.entries ⟨1, by norm_num⟩ := by
463 show (1 : ℝ) ≠ 1 / 2
464 norm_num
465 cases lu with
466 | mk idx hfixed =>
467 fin_cases idx
468 · have := hfixed ⟨1, by norm_num⟩ (by decide)
469 exact h1 this
470 · have := hfixed ⟨0, by norm_num⟩ (by decide)
471 exact h0 this
472
473/-! ## Connection to Existing RecognitionStep -/
474
475/-- **Theorem (Variational Implies Recognition Step)**:
476 Every variational step produces a valid `RecognitionStep` in the
477 `TimeEmergence` framework.
478
479 The variational dynamics generates the defect-reducing steps that
480 TimeEmergence postulated but never constructed. -/