RecognitionWorkConstraintCert
The RecognitionWorkConstraintCert structure packages a cost function on a configuration space with the properties that the empty configuration has zero cost, positive cost precisely signals inconsistency, costs add over independent joins, and the function is uniquely determined by its values on independent components. Researchers studying the recognition-work bridge in Recognition Science would cite this certificate when invoking the quantitative structure forced by independent additivity. The definition is assembled directly from the CostFunc-
claimA recognition-work constraint certificate on a configuration space $Config$ consists of a cost function $κ:Config→ℝ_{≥0}$ such that $κ(∅)=0$, $0<κ(Γ)↔¬IsConsistent(Γ)$ for all $Γ$, $κ(Γ_1∨Γ_2)=κ(Γ_1)+κ(Γ_2)$ whenever $Γ_1,Γ_2$ are independent, and $κ$ is the unique cost function agreeing with any other on a set closed under independent joins.
background
The module formalizes the T-1 to T0 bridge by introducing recognition work as the unit cost of a single distinction above the algebra of distinguishability. A configuration space abstracts an empty element, a commutative join monoid, a consistency predicate, and an independence relation (no shared predicates). A cost function maps configurations to non-negative reals and obeys the dichotomy (zero cost exactly on consistent configurations) together with independent additivity (cost of join equals sum of costs).
proof idea
The structure is defined by direct bundling of the cost function field with four properties: empty cost zero from the emp_cost_zero lemma, positivity characterization from cost_pos_iff_inconsistent, additivity taken from the CostFunction additivity axiom, and uniqueness on independent decompositions. No tactics appear; it is a pure structure declaration packaging the axioms and immediate corollaries.
why it matters in Recognition Science
This certificate is the master packaging for the recognition-work constraint theorem, which asserts existence of such a certificate for any cost function obeying the bridge axioms. It fills the T-1 to T0 step in RS_Cost_From_Distinction.tex by making explicit that independent additivity constrains costs on all independent extensions. In the Recognition Science framework it supplies the cost structure that later feeds phi-ladder mass formulas and the eight-tick octave. The downstream recognition_work_constraint_theorem invokes it to prove nonemptiness of the certificate type.
scope and limits
- Does not establish existence of a cost function satisfying the axioms on a given configuration space.
- Does not derive the explicit form of the cost function from J-cost or other primitives.
- Does not address consistency with multiplicative recognizer or observer forcing costs.
- Does not prove uniqueness beyond independent decompositions.
formal statement (Lean)
359structure RecognitionWorkConstraintCert
360 (Config : Type u) [ConfigSpace Config] where
361 /-- A cost function on the configuration space. -/
362 κ : CostFunction Config
363 /-- Empty cost is zero (immediate from dichotomy + emp_consistent). -/
364 emp_zero : κ.C emp = 0
365 /-- Cost-positivity characterises inconsistency. -/
366 pos_iff_inconsistent : ∀ Γ, 0 < κ.C Γ ↔ ¬IsConsistent Γ
367 /-- Cost is additive over independent joins. -/
368 additive_indep : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ →
369 κ.C (join Γ₁ Γ₂) = κ.C Γ₁ + κ.C Γ₂
370 /-- Cost is uniquely determined on independent decompositions by
371 its values on the components. -/
372 uniqueness :
373 ∀ (κ₂ : CostFunction Config) (S : Set Config),
374 (∀ Γ ∈ S, κ.C Γ = κ₂.C Γ) →
375 ∀ Γ₁ Γ₂, Γ₁ ∈ S → Γ₂ ∈ S → Independent Γ₁ Γ₂ →
376 κ.C (join Γ₁ Γ₂) = κ₂.C (join Γ₁ Γ₂)
377
378/-- Construct the master constraint certificate from any cost function
379satisfying the dichotomy and independent-additivity axioms. -/