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

ConfigSpace

show as:
view Lean formalization →

ConfigSpace defines the collection of admissible configurations in the modal setting as those with strictly positive value. Modal logicians and recognition theorists cite this when building cost functions or proving existence of consistent states. The definition is realized as a direct set comprehension over the Config structure.

claimLet $C$ be the structure of recognition configurations with value component in $ℝ$. Then ConfigSpace $:= { c : C | 0 < c.value }$.

background

The Modal.Possibility module develops modal logic over simplified configuration states for the Recognition Science framework. A configuration is a point in recognition state space, represented here by a structure with positive real value (generalizing bond multiplier), time coordinate in ticks, and log-bound constraint |log(value)| ≤ 16. This set definition extracts the well-formed configurations satisfying the positivity requirement.

proof idea

The declaration is a one-line definition using set comprehension to filter configurations by the positivity of their value field.

why it matters in Recognition Science

This supplies the concrete carrier set for the CostFunction and RecognitionWorkConstraintCert in the CostFromDistinction module. It is referenced by config_exists in RecogGeom.Core to witness nonempty configuration spaces. Within the framework it anchors the modal possibility space that supports the J-cost minimum at the identity configuration.

scope and limits

Lean usage

example : ∃ c, c ∈ ConfigSpace := by use ⟨1, by norm_num, 0, by norm_num⟩; simp [ConfigSpace]

formal statement (Lean)

  71def ConfigSpace : Set Config := {c | 0 < c.value}

proof body

Definition body.

  72
  73/-- The identity configuration (value = 1, minimal cost) -/

used by (25)

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

depends on (9)

Lean names referenced from this declaration's body.