calibration_pos
plain-language theorem explainer
A calibration of a cost function selects an inconsistent configuration α together with a positive real δ such that the cost equals δ at α. Researchers formalizing the recognition-work constraint would cite this to confirm positivity at the witness point before invoking uniqueness on independent decompositions. The proof is a one-line term wrapper that rewrites the agreement field and applies the δ_pos hypothesis directly.
Claim. Let $κ$ be a cost function on a configuration space and let $cal$ be a calibration of $κ$. Then $0 < κ.C(α)$, where $α$ is the distinguished inconsistent configuration of $cal$ and the calibration record ensures $κ.C(α) = δ$ for the chosen $δ > 0$.
background
The module CostFromDistinction formalizes the T-1 to T0 bridge by adding independent additivity to the cost dichotomy: cost is zero on consistent configurations and positive on inconsistent ones, with additivity over independent joins. The Calibration structure packages a distinguished inconsistent configuration α, a positive real δ, the assertion 0 < δ, the inconsistency of α, and the agreement clause that the cost function satisfies κ.C α = δ. This supplies the quantitative anchor needed for the recognition-work constraint theorem to determine cost functions from their values on indecomposable generators.
proof idea
The proof is a one-line term-mode wrapper. It rewrites the goal via the agrees field of the calibration record, which equates κ.C cal.α to δ, then applies the δ_pos field asserting 0 < δ.
why it matters
This result anchors positivity at the calibration witness, a prerequisite for the recognition_work_constraint_theorem that shows cost functions are uniquely determined by their restriction to indecomposable inconsistent configurations. It closes the basic consistency check required by the independent-additivity axiom in the CostFromDistinction module. In the Recognition Science chain it supports the passage from the distinguishability algebra to quantitative cost structure without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.