Cosmology Recognition Equilibrium Recognition Equilibrium

The equilibrium theorem

In the Recognition Science framework, a recognition event is a discrete record of one system component registering another. The framework models a collection of such components as points on a graph, each carrying a numerical level. The declaration recognitionEquilibrium is a machine-checked theorem about what happens when those components interact by a single forced rule: whenever two connected components meet, both adopt their average. This is the whole dynamics; there is no relaxation rate, no tuning parameter, no choice about how strongly they respond.

The theorem proves five facts about this rule, each with an exact statement. First, the sum of all levels is conserved: averaging two numbers leaves their total unchanged, so the overall amount is fixed. Second, the spread, measured as the sum of squared deviations from the mean, drops by exactly half the squared difference between the two averaged values. Third, that spread never increases under any resolution. Fourth, the total recognition cost, defined as a sum over every edge of a positive function of the level ratio, is always nonnegative. Fifth, and most importantly, that total cost is zero if and only if every connected pair has equal levels, meaning the system has reached consensus.

These five facts assemble into the central conclusion: the dynamics is a strict descent that provably relaxes to the ground state, and that ground state is exactly the configuration where all connected components agree. The theorem is not a numerical simulation or a heuristic argument; it is a formal proof in the framework's machine-checked library of formal theorems, with no unproved assumptions beyond the standard logical axioms. The variance acts as a Lyapunov function, a quantity that decreases with each step until it bottoms out, guaranteeing the descent cannot cycle or stall short of agreement.

The theorem also covers an open-system extension where new components are born in conjugate pairs, one at level +u and one at level -u. The declarations conjugateBirth_chargeSum and manyBirths_chargeSum prove that such births conserve the total level sum, so the conservation law holds through the entire driven evolution. This matters because it keeps non-homogenizing structure alive: the closed-system descent would flatten everything to a single value, but the conserved-sigma birth is the forced open input that prevents that flattening. The equilibrium theorem thus describes both the closed-system relaxation and the condition under which the open system maintains diversity.

What the theorem does not claim is as precise as what it proves. It does not claim that the total edge demand, a different measure of system activity, is monotone; the variance is the monotone quantity, and total edge demand is explicitly not claimed to be. It does not claim that the dynamics reaches consensus in finite time, only that the variance decreases by a definite amount per step and never grows. It does not claim that the consensus configuration is unique, since any constant field is a fixed point. And it does not claim anything about the physical interpretation of the levels or the graph; those are modeling choices, not consequences of the theorem.

/-- **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)

/-- **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)]

/-- **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]

/-- 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)]

/-- **A conjugate birth conserves sigma.** Inserting `+u` at the fine frontier and `-u` at
the coarse frontier leaves the total charge unchanged: the net of the born pair is zero. -/
theorem conjugateBirth_chargeSum (u : ℝ) (xs : List ℝ) :
    ((u :: xs) ++ [-u]).sum = xs.sum := by
  simp only [List.sum_append, List.sum_cons, List.sum_nil]
  ring

What this page does not claim

The theorem does not claim that total edge demand is monotone; only the variance is. The theorem does not claim finite-time convergence to consensus, only strict descent of the variance. The theorem does not claim that the consensus configuration is unique, since any constant field is a fixed point.

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: