CostFunction
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.