pith. sign in
module module high

IndisputableMonolith.RRF.Core.Strain

show as:
view Lean formalization →

The Strain module defines a strain functional that maps states to non-negative reals, vanishing exactly at balanced equilibria. RRF core developers cite it to anchor cost-based ordering before scaling or categorical constructions. It is a pure definition module with class constraints and no proofs.

claimA strain functional is a map $J : X → ℝ$ satisfying $J(x) ≥ 0$ for every state $x$, with $J(x) = 0$ if and only if $x$ is balanced.

background

This module introduces the strain functional as the basic cost object in the Reality Recognition Framework. It equips an arbitrary state space with a non-negative real-valued map whose kernel marks equilibrium, using a type-class constraint for nonnegativity. Sibling definitions cover predicates for balance, equilibria, minimizers, and ordering relations such as strictlyBetter and weaklyBetter.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the core strain concept to the RRF.Core umbrella, Glossary, Octave, VantageCategory, and OrderPreservation theorems. It supplies the definitional base for cost ordering that later modules extend to scaling and categorical equivalence.

scope and limits

used by (5)

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

declarations in this module (16)