extension_to_consistent
plain-language theorem explainer
Two cost functions that share a calibration witness α with matching positive cost δ agree on the cost of joining α to any consistent Γ independent of α. Researchers deriving uniqueness for the recognition-work constraint would cite this when extending from a generator to composite configurations. The proof decomposes each join via independent additivity, equates the α contributions through the shared calibration value, sets both Γ contributions to zero, and reassembles the equality.
Claim. Let κ₁ and κ₂ be cost functions on a configuration space. Let cal₁ and cal₂ be calibrations for them that share the same distinguished inconsistent configuration α and the same positive cost value δ. Then for any consistent configuration Γ independent of α, κ₁.C(α ∨ Γ) = κ₂.C(α ∨ Γ).
background
A CostFunction on a ConfigSpace satisfies dichotomy (cost zero precisely when the configuration is consistent) and independent additivity (cost of a join equals the sum of costs when the summands share no predicates). A Calibration for such a function selects one inconsistent α together with a positive δ such that the cost at α equals δ. The module develops the recognition-work constraint by showing that these two axioms force the cost function to be uniquely determined by its values on a generating set of indecomposable inconsistent configurations. Upstream, cost_zero_of_consistent records that any consistent configuration contributes zero cost under either function.
proof idea
Apply the additivity field of the first CostFunction to split the join cost into the sum of the α term and the Γ term. Rewrite independence for the second function using the shared α. Equate the two α contributions by rewriting the calibration agreements and the shared δ. Equate the two Γ contributions by invoking cost_zero_of_consistent on both sides. Substitute back to obtain the desired equality.
why it matters
The lemma closes one step in the uniqueness argument of the recognition-work constraint theorem by extending agreement from the calibration witness to all independent consistent extensions. It relies only on the dichotomy and independent-additivity axioms already present in the CostFunction structure and on the zero-cost property for consistent configurations. In the T-1 to T0 bridge this supplies the quantitative extension property needed before the master constraint certificate can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.