pith. machine review for the scientific record. sign in
def definition def or abbrev high

minimalImprovement

show as:
view Lean formalization →

minimalImprovement supplies the base generator for ethical action states as the pair with agent index zero and improvement rank one. Researchers modeling strict ethical realizations in the Recognition framework cite it as the minimal step that seeds the carrier type. The definition is a direct constructor application to the ActionState structure.

claimThe minimal improvement generator is the action state with agent coordinate $0$ and improvement rank $1$, written as the pair $(0,1)$ in the structure whose fields are agent index and improvement rank.

background

ActionState is the structure whose fields are an agent coordinate in the natural numbers and an improvement rank also in the natural numbers. The Strict/Ethics module uses this structure to realize ethical states over action coordinates, with the generator defined as the smallest recognized improvement step. Upstream, the 'as' structure from the SimplicialLedger.ContinuumBridge module identifies the Laplacian action via the identity (1/2) Σ w_ij (ε_i − ε_j)² = (1/κ) Σ δ_h A_h.

proof idea

This is a one-line definition that applies the ActionState constructor directly to the constants 0 and 1.

why it matters in Recognition Science

The definition supplies the generator for strictEthicsRealization, which assembles a StrictLogicRealization whose carrier is ActionState and whose cost function is the natural numbers. It occupies the role of the smallest improvement step inside the UniversalForcing.Strict.Ethics module and thereby anchors the ethical coordinate system that sits downstream of the forcing chain.

scope and limits

formal statement (Lean)

  39def minimalImprovement : ActionState := ⟨0, 1⟩

proof body

Definition body.

  40
  41/-- Strict ethical realization using minimal improvement as generator. -/

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.