Cosmology Recognition Equilibrium Variance Nonincreasing

The spread that only shrinks

A ledger, a discrete record of events, often has entries that differ. The declaration variance_nonincreasing states a precise fact about one way those differences can change: when two entries are resolved by replacing both with their average, the spread of all entries, measured as variance, never increases. The proof is exact, not approximate: the variance drops by exactly half the squared difference between the two resolved entries, (x i - x j)² / 2. Since a square is never negative, the variance after resolution is always less than or equal to the variance before it.

This is a theorem in the framework's machine-checked library of formal theorems. It is a corollary of a stronger statement, variance_pairResolve, which gives the exact decrement. The dynamics that this describes is a forced recognition event: each tick, a coupled pair is selected and both endpoints are sent to their mean. There is no relaxation rate, no adjustable knob. The sum of all entries is conserved by this move, so the average stays fixed while the spread contracts. The theorem holds for any pair of distinct indices in a finite field of recognition levels, with no further conditions.

The consequence is that the variance acts as a Lyapunov function, a quantity that strictly decreases until a stopping condition is met. That stopping condition is consensus: the recognition cost, which is nonnegative, reaches zero exactly when every coupled pair has equal values. The ground state of the system, the configuration of lowest cost, is precisely the consensus configuration. The descent is strict until that point, meaning the dynamics provably relaxes to agreement across every edge of the coupling graph.

In Recognition Science, this is the closed-system picture. The framework also models a driven extension where new pairs are born at the horizon in conjugate form, one positive and one negative, which conserves the charge sum. Those births keep non-homogenizing structure alive, but the variance result itself concerns only the resolution step. What the theorem does not claim is that the total edge demand is monotone; it is not, and no such claim is made. The variance is the quantity that never grows, not every measure of activity.

The plain takeaway is that a system following this rule cannot become more disordered in the variance sense. Differences shrink by a law-given amount each resolution, and the only resting point is full agreement. This gives a rigorous, machine-checked foundation for why recognition dynamics, left to itself, settles into uniformity.

/-- The spread never grows under a forced resolution. -/
theorem variance_nonincreasing {n : ℕ} (x : Fin n → ℝ) {i j : Fin n} (h : i ≠ j) :
    variance (pairResolve x i j) ≤ variance x := by
  rw [variance_pairResolve x h]
  nlinarith [sq_nonneg (x i - x j)]

/-- **The variance Lyapunov law.** Each forced resolution lowers the level variance by
exactly `(x i - x j)^2 / 2`. The decrement is the recognition gap that was resolved, so
the descent is strict until every coupled pair is equal. -/
theorem variance_pairResolve {n : ℕ} (x : Fin n → ℝ) {i j : Fin n} (h : i ≠ j) :
    variance (pairResolve x i j) = variance x - (x i - x j) ^ 2 / 2 := by
  unfold variance
  rw [meanLevel_pairResolve x h, varAround_pairResolve x h (meanLevel x)]

/-- **The recognition ground state is consensus.** The total recognition cost vanishes if
and only if the level field is constant on every coupled pair. So the zero-cost
configuration the descent converges to is exactly graph consensus. -/
theorem totalCost_eq_zero_iff {n : ℕ} (x : Fin n → ℝ) (edges : Finset (Fin n × Fin n)) :
    totalCost x edges = 0 ↔ ∀ e ∈ edges, x e.1 = x e.2 := by
  rw [totalCost, Finset.sum_eq_zero_iff_of_nonneg
        (fun _ _ => jcost_nonneg (Real.rpow_pos_of_pos Constants.phi_pos _))]
  constructor
  · intro h e he; exact (cost_phi_eq_zero_iff _ _).mp (h e he)
  · intro h e he; exact (cost_phi_eq_zero_iff _ _).mpr (h e he)

/-- **Sigma is conserved.** Resolving a pair leaves the total level unchanged. -/
theorem pairResolve_levelSum {n : ℕ} (x : Fin n → ℝ) {i j : Fin n} (h : i ≠ j) :
    levelSum (pairResolve x i j) = levelSum x := by
  unfold levelSum
  have hagree : ∀ k, k ≠ i → k ≠ j → pairResolve x i j k = x k :=
    fun k hi hj => pairResolve_other x hi hj
  have hsp := sum_split_pair (pairResolve x i j) x h hagree
  rw [pairResolve_at_i, pairResolve_at_j] at hsp
  -- hsp : (∑ resolved) - (∑ x) = ((xi+xj)/2 + (xi+xj)/2) - (x i + x j)
  have hzero : ((x i + x j) / 2 + (x i + x j) / 2) - (x i + x j) = 0 := by ring
  rw [hzero] at hsp
  linarith [hsp]

What this page does not claim

The total edge demand is monotone; it is not, and no such claim is made. The theorem applies to any dynamics with relaxation rates or adjustable parameters. The driven extension with conjugate births is proven to converge to consensus.

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/Cosmology/RecognitionEquilibrium.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: