pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.RRF.Theorems.OrderPreservation

show as:
view Lean formalization →

This module defines the rank function on finite state sets and proves order-preservation results for RRF structures under display channels and strain. Researchers building RRF equilibria or minimal-strain arguments would cite these lemmas to establish monotonicity and transitivity. The proofs consist of direct applications of finiteness, strict monotonicity, and basic order lemmas from the imported Core modules.

claimThe rank of a state $x$ in a finite set $S$ is the cardinality of states with strictly lower $J$-cost: $rank(x,S)=|y in S:J(y)<J(x)|$. The module proves that strict monotonicity preserves strict order, that rank is invariant under optimal transfers, and that strain orders are transitive.

background

RRF works with states observed through display channels, which project internal states into an observation space, and with strain, the fundamental deviation from equilibrium where strain approaches zero precisely when $J$ approaches zero. Lower strain corresponds to greater consistency. The module introduces rank as the counting measure of lower-$J$ states within any finite set $S$ and then derives preservation properties for the induced orders.

proof idea

The module opens with the definition of rank. It then applies order-theory facts to obtain strictMono_preserves_strict_order, proves rank_invariant and optimal_transfer, establishes channel_mono_transfer, and closes with the two strain transitivity lemmas plus equilibria_minimal. All steps are short algebraic or cardinality arguments that rely on the finiteness assumption and the imported Strain and DisplayChannel definitions.

why it matters in Recognition Science

These results supply the order-theoretic infrastructure required by the parent RRF.Theorems umbrella module. They deliver the pure-logic facts needed to reason about minimal-strain configurations and equilibrium ordering without invoking physical hypotheses. The downstream theorems directly import and apply the transitivity and invariance statements proved here.

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 (8)