Cosmology Recognition Equilibrium Many Births Charge Sum

The conserved sum

In mathematics and physics, a conserved quantity is one that stays the same while a system changes. The Recognition Science framework models a universe as a discrete record of events, a ledger that tracks a set of numerical levels on a network of interacting sites. The framework's central cost function, derived from five plain conditions, forces a specific dynamics: each tick, one pair of linked sites is resolved by sending both to their average. That move provably conserves the sum of all levels, a quantity the framework calls the charge sum.

The theorem manyBirths_chargeSum extends this conservation to the driven case, where the system is not closed but grows. The framework's expanding dynamics adds, at each cadence cycle, a conjugate pair of new levels, one positive and one negative, at the horizon. The theorem states that adding any number of such pairs, in any order, leaves the total charge sum unchanged. In symbols, if the existing levels are a list xs, then adding k copies of u and k copies of -u gives (replicate k u ++ xs ++ replicate k (-u)).sum = xs.sum. The proof is a short algebraic identity: the positive and negative copies cancel exactly.

This result matters because the framework's closed-system dynamics provably relaxes to consensus, where every site has the same level and the recognition cost reaches its minimum of zero. Without an input, the universe would flatten into uniformity. The conserved-sigma birth is the forced open input that keeps non-homogenizing structure alive. The charge sum staying zero through both resolutions and births is what lets the framework describe a cosmos that maintains pockets of difference while obeying its own conservation law.

The theorem does not claim that the dynamics reaches equilibrium, that the charge sum is the only conserved quantity, or that the framework's model of cosmic expansion matches observation. It is a formal statement about a specific algebraic operation on lists of real numbers, proved in the machine-checked library of formal theorems.

/-- **Any number of conjugate births conserves sigma.** After `k` cadence cycles of
expansion the ladder carries `k` extra `+u` charges at the fine frontier and `k` extra `-u`
charges at the coarse frontier; the total charge is still the initial total. So sigma = 0 is
preserved through the entire driven run. -/
theorem manyBirths_chargeSum (k : ℕ) (u : ℝ) (xs : List ℝ) :
    (List.replicate k u ++ xs ++ List.replicate k (-u)).sum = xs.sum := by
  simp only [List.sum_append, List.sum_replicate, nsmul_eq_mul]
  ring

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

What this page does not claim

The theorem does not claim the driven dynamics reaches equilibrium or that the charge sum is the only conserved quantity. The theorem does not claim the framework's cosmic model matches any astronomical observation. The theorem does not claim the birth operation is derived from the cost function; it is a chosen input.

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: