with
open lean source
IndisputableMonolith.Foundation.CostFromDistinction on GitHub at line 350.
browse module
All declarations in this module, on Recognition.
plain-language theorem explainer
The recognition work constraint theorem establishes that cost on a configuration equals the sum of costs on its independent inconsistent components and is uniquely fixed by values on indecomposable inconsistencies. Researchers formalizing the T-1 to T0 bridge in Recognition Science cite it to justify quantitative structure beyond the mere consistency dichotomy. The argument combines the dichotomy axiom with independent additivity to reduce arbitrary configurations to base cases via finite decompositions.
Claim. Let $C$ be a cost function on a configuration space satisfying the dichotomy ($C=0$ precisely on consistent configurations) and independent additivity ($C$ of an independent join equals the sum of the $C$ values). Then for any finite collection of pairwise independent configurations, $C$ of their join equals the sum of the individual $C$ values, and $C$ is uniquely determined by its restriction to indecomposable inconsistent configurations.
background
The module formalizes the substantive content of the T-1 to T0 bridge paper RS_Cost_From_Distinction.tex by adding one operational primitive: recognition work as the unit cost of performing a single distinction. ConfigSpace is the typeclass abstracting configuration spaces equipped with consistency, joining, and independence. CostFunction is the structure satisfying the dichotomy axiom together with independent additivity over configurations that share no predicates. The local theoretical setting is that the recognition-work narrative supplies no formal content without this additivity constraint; the proofs then use only the satisfiability dichotomy plus the stipulation that cost vanishes on consistent configurations.
proof idea
The proof is a one-line wrapper that applies the independent-additivity axiom to finite pairwise-independent joins and invokes uniqueness on indecomposable decompositions. It first records that the empty configuration has cost zero, then shows that any configuration decomposes into independent inconsistent components whose costs sum, reducing the general case to the base inconsistent configurations.
why it matters
This is the main constraint result of the CostFromDistinction module and directly fills the gap identified in RS_Cost_From_Distinction.tex by enforcing independent additivity. It supplies the quantitative structure required for the cost framework in the Foundation layer and feeds into downstream derivations of the forcing chain. The result touches the open calibration question of assigning a specific positive cost to the base inconsistent configuration. In the Recognition Science framework it operationalizes the T-1 to T0 bridge by turning the recognition-work primitive into a genuine additive cost function.
depends on
formal source
347
348/--
349**Master certificate**: bundles the recognition-work constraint
350theorem with its immediate consequences.
351
352This certificate makes precise what the recognition-work primitive
353adds above the algebra of distinguishability. It is non-vacuous: the
354calibration component picks out a specific inconsistent
355configuration with a specific positive cost, and the additivity
356component constrains the cost on all independent extensions of that
357configuration.
358-/
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. -/
380def recognition_work_constraint_cert