Pith. sign in
module module high

IndisputableMonolith.Cosmology.RecognitionEquilibrium

show as:
view Lean formalization →

Defines the forced recognition resolution of one coupled pair: both endpoints are sent to their arithmetic mean. That move is the unique sigma = 0, J-minimal update the forward cosmogenesis dynamics posts each tick. Cosmology workers cite it as the elementary active step behind mean-level and variance identities. The module is mostly definitions plus short algebraic lemmas on level sums and variance under the move.

claimOn a coupled pair of levels $(\ell_i,\ell_j)$, the recognition-equilibrium (pair-resolve) map sends both endpoints to their mean: $\ell_i'\,=\,\ell_j'\,=\,(\ell_i+\ell_j)/2$. This is the unique $\sigma=0$, $J$-minimal resolution posted by the forward dynamics each tick. The module records the induced identities for total level sum, mean level, and variance about the mean.

background

Recognition Science cosmology runs a discrete forward dynamics on rung levels. Each tick, coupled pairs that fire the refinement trigger are resolved by a forced local move. The module doc fixes that move: send both endpoints to their mean. In RS language this is the $\sigma=0$, $J$-minimal update (the cost $J$ is the unique symmetric convex cost from the forcing chain; the zero-spread choice is the unique minimizer once the pair is selected).

Upstream, Constants supplies the RS time quantum (one tick). RefineTrigger is the Lean form of theorem T-3 of the scale-adaptive cosmogenesis engine: the refinement threshold is law-derived and equals zero, with no free knob, building on the T-1 cell model (events, internal/cross cost).

Sibling definitions package the move (pairResolve and pointwise variants), the level sum and its split across a pair, mean level, variance about a reference, and the elementary identities relating those quantities before and after the resolve.

proof idea

This is primarily a definition module. The core object is the pair-resolve map (both indices written to the arithmetic mean). Surrounding lemmas are short algebraic identities: the total level sum is invariant under the move; the sum splits cleanly into the resolved pair plus the untouched complement; variance about the mean drops in the expected way when a pair is collapsed to its mean; mean level is likewise preserved. Proofs are direct rewriting and Finset sum splits, not deep analysis.

why it matters in Recognition Science

The module supplies the elementary active step of recognition dynamics used throughout the cosmogenesis spine. Downstream, RecognitionUnitStepPreservation imports it and records a negative fact: the tempting claim that active mean-move dynamics automatically preserves the graded-rung UnitStep invariant (adjacent rungs differ by at most one) is false. Phase 56 had proved the graded-rung cost law under UnitStep; Phase 57 wired that into the runtime cost meter; this module's pairResolve is exactly the dynamics those phases must confront. In the broader RS picture it is the local $\sigma\to 0$ projection that implements one tick of forced recognition equilibrium, sitting under the T-3 law-derived refinement trigger.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (25)