Calibration
plain-language theorem explainer
A calibration of a cost function κ on configurations selects one inconsistent α and positive δ with κ.C α = δ. Researchers deriving the recognition-work constraint theorem cite this to normalize before proving uniqueness on independent decompositions. The declaration is a direct five-field structure encoding the witness, positivity, inconsistency, and agreement.
Claim. Let κ be a cost function on a configuration space. A calibration consists of an inconsistent configuration α and a positive real δ > 0 such that κ(α) = δ.
background
CostFunction is the structure requiring a map C : Config → ℝ that is nonnegative, obeys dichotomy (C Γ = 0 ↔ IsConsistent Γ), and satisfies independent additivity (C(join Γ₁ Γ₂) = C Γ₁ + C Γ₂ whenever Independent Γ₁ Γ₂). The module formalizes the T-1 → T0 bridge by adjoining independent additivity to the satisfiability dichotomy, so that cost equals the sum of costs of independent inconsistent components and is uniquely determined by its values on indecomposable generators. The sibling Calibration axiom from CostAxioms normalizes curvature via G''(0) = 1 where G(t) = F(exp t); the present structure supplies the concrete witness used to invoke that normalization.
proof idea
Direct structure definition. The five fields α, δ, δ_pos, α_inconsistent, and agrees are introduced with no lemmas, tactics, or reduction steps.
why it matters
This supplies the normalization witness required by the recognition-work constraint theorem. It is invoked by IsCalibrated, composition_law_equiv_coshAdd, and washburn_uniqueness to obtain uniqueness of cost functions agreeing on generators, and by mass_ratio_bounds, E_coh_rs_eq_E_coh, and Lambda_no_fine_tuning to anchor RS-native units and cosmological constants. It closes the T-1 → T0 bridge by fixing the scale for J-cost derivations that propagate into the phi-ladder and alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.