pith. machine review for the scientific record. sign in
theorem proved tactic proof high

variational_step_unique

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

Lean usage

have h_eq : next₁.entries = next₂.entries := variational_step_unique hN c next₁ next₂ h₁ h₂

formal statement (Lean)

 290theorem variational_step_unique {N : ℕ} (hN : 0 < N)
 291    (c : Configuration N)
 292    (next₁ next₂ : Configuration N)
 293    (h₁ : IsVariationalSuccessor c next₁)
 294    (h₂ : IsVariationalSuccessor c next₂) :
 295    next₁.entries = next₂.entries := by

proof body

Tactic-mode proof.

 296  have h_uniform : IsVariationalSuccessor c (constant_config (log_charge c / N) : Configuration N) := by
 297    constructor
 298    · show log_charge (constant_config (log_charge c / N) : Configuration N) = log_charge c
 299      rw [constant_config_log_charge]
 300      exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN))
 301    · intro c' hc'
 302      rw [constant_config_total_defect]
 303      have hbound := total_defect_lower_bound hN c'
 304      rw [hc'] at hbound
 305      exact hbound
 306  have h1_eq_min : total_defect next₁ = (N : ℝ) * Jlog (log_charge c / N) := by
 307    have h1le := h₁.2 (constant_config (log_charge c / N) : Configuration N) h_uniform.1
 308    have h1ge := h_uniform.2 next₁ h₁.1
 309    rw [constant_config_total_defect] at h1le h1ge
 310    exact le_antisymm h1le h1ge
 311  have h2_eq_min : total_defect next₂ = (N : ℝ) * Jlog (log_charge c / N) := by
 312    have h2le := h₂.2 (constant_config (log_charge c / N) : Configuration N) h_uniform.1
 313    have h2ge := h_uniform.2 next₂ h₂.1
 314    rw [constant_config_total_defect] at h2le h2ge
 315    exact le_antisymm h2le h2ge
 316  have h1_const :
 317      next₁.entries = (constant_config (log_charge next₁ / N) : Configuration N).entries := by
 318    apply eq_constant_config_of_defect_eq hN next₁
 319    rw [← h₁.1] at h1_eq_min
 320    exact h1_eq_min
 321  have h2_const :
 322      next₂.entries = (constant_config (log_charge next₂ / N) : Configuration N).entries := by
 323    apply eq_constant_config_of_defect_eq hN next₂
 324    rw [← h₂.1] at h2_eq_min
 325    exact h2_eq_min
 326  have hcharge1 : log_charge next₁ = log_charge c := h₁.1
 327  have hcharge2 : log_charge next₂ = log_charge c := h₂.1
 328  calc
 329    next₁.entries = (constant_config (log_charge next₁ / N) : Configuration N).entries := h1_const
 330    _ = (constant_config (log_charge c / N) : Configuration N).entries := by rw [hcharge1]
 331    _ = (constant_config (log_charge next₂ / N) : Configuration N).entries := by rw [hcharge2]
 332    _ = next₂.entries := h2_const.symm
 333
 334/-! ## Defect Reduction -/
 335
 336/-- **Theorem (Variational Step Reduces Defect)**:
 337    The total defect of the successor is at most the total defect
 338    of the current state.
 339
 340    This follows immediately: the current state is feasible for itself,
 341    and the successor minimizes over the feasible set, so the successor's
 342    cost is at most the current state's cost. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (32)

Lean names referenced from this declaration's body.

… and 2 more