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

CostFunction

show as:
view Lean formalization →

CostFunction axiomatizes a non-negative map C on configurations that vanishes exactly on consistent ones and adds over independent joins. Researchers formalizing the recognition-work bridge cite it as the carrier of the T-1 to T0 constraint. The declaration is a direct structure bundling the three axioms with no derivation steps.

claimA cost function on a configuration space consists of a map $C : Cfg → ℝ$ such that $0 ≤ C(Γ)$ for every configuration $Γ$, $C(Γ) = 0$ if and only if $Γ$ is consistent, and $C(join(Γ₁, Γ₂)) = C(Γ₁) + C(Γ₂)$ whenever $Γ₁$ and $Γ₂$ are independent.

background

ConfigSpace is the typeclass supplying an empty configuration emp, a commutative join operation, a consistency predicate IsConsistent, and a symmetric independence relation Independent compatible with the monoid laws. The module develops the recognition-work constraint from the T-1 to T0 bridge paper by adding independent additivity to the dichotomy, which forces cost to equal the sum of costs on independent inconsistent components. Upstream results include the ConfigSpace class and related structures such as LedgerFactorization for later calibration.

proof idea

This is a structure definition with no proof body. It directly encodes the cost map C together with the nonnegativity, dichotomy equivalence, and independent-additivity fields as stated in the doc-comment.

why it matters in Recognition Science

CostFunction supplies the central definition feeding downstream results such as additive_three, Calibration, and the recognition_work_constraint_theorem. It realizes the independent-additivity constraint from the RS_Cost_From_Distinction paper, enabling uniqueness on indecomposable inconsistent configurations. In the Recognition Science framework it grounds the T0 cost structure that later connects to the phi-ladder and constants such as G = phi^5 / pi.

scope and limits

formal statement (Lean)

 147structure CostFunction (Config : Type u) [ConfigSpace Config] where
 148  /-- The cost function itself, taking values in the non-negative reals. -/
 149  C : Config → ℝ
 150  /-- Cost is non-negative. -/
 151  nonneg : ∀ Γ, 0 ≤ C Γ
 152  /-- (D) Dichotomy: zero cost characterises consistency. -/
 153  dichotomy : ∀ Γ, C Γ = 0 ↔ IsConsistent Γ
 154  /-- (A) Independent additivity: the recognition-work constraint. -/
 155  additivity : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ → C (join Γ₁ Γ₂) = C Γ₁ + C Γ₂
 156
 157namespace CostFunction
 158
 159variable {Config : Type u} [ConfigSpace Config]
 160
 161/-! ### Immediate consequences of the axioms -/
 162
 163/-- The empty configuration has zero cost. -/

used by (16)

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

depends on (23)

Lean names referenced from this declaration's body.