Foundation Variational Dynamics Constant Config Total Defect

The uniform configuration's cost

A ledger, a discrete record of entries, has a total cost, a single number that measures how far the whole record sits from its ideal state. The declaration constant_config_total_defect computes that cost for a special kind of ledger: one where every entry is the same positive number. If that common value is written as e^μ, and the ledger has N entries, the total cost is exactly N times J(μ), where J is the framework's fundamental cost function J(x) = ½(x + 1/x) − 1. The proof is a direct calculation, unfolding definitions and summing the identical terms.

The formula matters because it exposes the structure of the ledger's resting states. A configuration where all entries are equal is called uniform. The theorem shows that the cost of such a state depends only on the common value and the size of the ledger, not on any arrangement of entries. This is a consequence of the cost function's symmetry: J(x) = J(1/x), so a pair of reciprocal entries costs the same as a pair of equal ones. The uniform state is the one where that symmetry is expressed most simply.

In Recognition Science, the ledger evolves by choosing, at each tick, the reachable configuration with the lowest total cost. The uniform configuration is the unique minimizer among all states with the same conserved total log-ratio, a fact the framework proves separately. This theorem, constant_config_total_defect, is the arithmetic backbone of that result: it gives the exact cost of the candidate minimizer, which the uniqueness proof then compares against every other reachable state. Without this formula, the minimization argument would have no concrete value to aim at.

The declaration does not claim that uniform configurations are always reachable from any starting state, nor that they are the only equilibria. It is a statement about a specific family of configurations, not about the dynamics that lead to them. The theorem also does not say that the ledger must end in a uniform state; it only provides the cost of such a state, which the dynamics may or may not select depending on the conservation law and the set of feasible moves.

/-- The constant configuration has total defect `N * Jlog μ`. -/
private theorem constant_config_total_defect {N : ℕ} (μ : ℝ) :
    total_defect (constant_config μ : Configuration N) = (N : ℝ) * Jlog μ := by
  unfold total_defect constant_config
  simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  rfl

/-- Equality in the Jensen bound forces the configuration to be uniform. -/
private theorem eq_constant_config_of_defect_eq {N : ℕ} (hN : 0 < N) (c : Configuration N)
    (hEq : total_defect c = (N : ℝ) * Jlog (log_charge c / N)) :
    c.entries = (constant_config (log_charge c / N) : Configuration N).entries := by
  have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
  have hw_pos : ∀ i ∈ (Finset.univ : Finset (Fin N)), 0 < (1 / (N : ℝ)) := by
    intro _ _
    exact one_div_pos.mpr hN_pos
  have hw_sum : ∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) = 1 := by
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    field_simp [hN_pos.ne']
  have hmem : ∀ i ∈ (Finset.univ : Finset (Fin N)), Real.log (c.entries i) ∈ (Set.univ : Set ℝ) := by
    intro _ _
    simp
  have hEq' : Jlog (log_charge c / N) = (1 / (N : ℝ)) * total_defect c := by
    have hN_ne : (N : ℝ) ≠ 0 := hN_pos.ne'
    calc
      Jlog (log_charge c / N)
          = (1 / (N : ℝ)) * ((N : ℝ) * Jlog (log_charge c / N)) := by
              field_simp [hN_ne]
      _ = (1 / (N : ℝ)) * total_defect c := by rw [← hEq]
  have hMapEq :
      Jlog (∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) • Real.log (c.entries i)) =
        ∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) • Jlog (Real.log (c.entries i)) := by
    have hMapEq0 :
        Jlog (∑ i : Fin N, (1 / (N : ℝ)) * Real.log (c.entries i)) =
          ∑ i : Fin N, (1 / (N : ℝ)) * Jlog (Real.log (c.entries i)) := by
      rw [weighted_log_average hN c, weighted_Jlog_average c]
      exact hEq'
    simpa [smul_eq_mul] using hMapEq0
  have hall :=
    (Jlog_strictConvexOn.map_sum_eq_iff
      (t := (Finset.univ : Finset (Fin N)))
      (w := fun _ : Fin N => (1 / (N : ℝ)))
      (p := fun i : Fin N => Real.log (c.entries i))
      hw_pos hw_sum hmem).mp hMapEq
  funext i
  have hlog : Real.log (c.entries i) = log_charge c / N := by
    have hlog0 : Real.log (c.entries i) = ∑ i : Fin N, (1 / (N : ℝ)) * Real.log (c.entries i) := by
      simpa [smul_eq_mul] using hall i (by simp)
    rw [weighted_log_average hN c] at hlog0
    exact hlog0
  have hexp := congrArg Real.exp hlog
  simpa [constant_config, Real.exp_log (c.entries_pos i)] using hexp

What this page does not claim

The declaration does not claim that uniform configurations are always reachable from any starting state. It does not claim that the ledger must end in a uniform state under the variational dynamics. It does not assert that the uniform configuration is the only equilibrium of the ledger.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/VariationalDynamics.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: