module module high

`IndisputableMonolith.Foundation.CostFromDistinction`

This module defines an abstract configuration space equipped with an empty element, commutative join, consistency predicate, and independence relation, together with their basic algebraic and preservation laws. Foundation researchers cite it when building concrete models such as predicate-constraint systems or sequent calculi before deriving cost from inconsistency. The module supplies the structure definitions and the elementary lemmas that establish the monoid and consistency axioms.

claimA configuration space is a set $C$ with distinguished element $e$, binary operation $*$ forming a commutative monoid with identity $e$, unary predicate $IsConsistent$, and binary relation $Independent$ such that $Independent$ is symmetric, $Independent(e,x)$ holds for all $x$, $IsConsistent(e)$ holds, $IsConsistent(x)$ and $IsConsistent(y)$ and $Independent(x,y)$ imply $IsConsistent(x*y)$, and $IsConsistent(x)$ and $Independent(x,y)$ imply that $IsConsistent(x*y)$ is equivalent to $IsConsistent(y)$.

background

The module opens the Foundation.CostFromDistinction section by introducing ConfigSpace as the minimal abstract carrier for configurations that can be joined and checked for consistency. The supplied doc-comment states that join is a commutative monoid with emp as identity, independence is symmetric with emp independent of everything, emp is consistent, and consistent independent configurations join to a consistent result while inconsistent configurations remain inconsistent under independent join. These axioms are deliberately weak so that the same interface can be realized by predicate-constraint configurations on a carrier K, multisets of formulas, or sets of typed assertions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the abstract ConfigSpace that all subsequent cost lemmas in the file (emp_cost_zero, cost_pos_iff_inconsistent, additive_three, additive_strict_of_both_inconsistent) instantiate. It therefore underpins the derivation of cost from distinction that later feeds the J-cost and defectDist constructions used in the forcing chain.

scope and limits

Does not instantiate ConfigSpace with any concrete carrier such as predicate sets.
Does not assign numerical cost values or connect to the J-function.
Does not reference the phi-ladder, eight-tick octave, or spatial dimension D=3.
Does not prove any global properties of cost beyond the listed local lemmas.

declarations in this module (24)

class ConfigSpace L77
theorem join_emp L112
theorem independent_emp L117
theorem inconsistent_of_join_indep_right L122
structure CostFunction L147
theorem emp_cost_zero L164
theorem cost_pos_iff_inconsistent L169
theorem cost_zero_of_consistent L180
theorem cost_pos_of_inconsistent L185
theorem cost_ne_zero_of_inconsistent L190
theorem additive_three L202
theorem additive_strict_of_both_inconsistent L216
theorem additive_emp_left L231
theorem additive_emp_right L235
theorem uniqueness_on_indep_decomposition L258
theorem uniqueness_three_indep L275
theorem then L294
structure Calibration L299
theorem calibration_pos L317
theorem extension_to_consistent L324
theorem with L350
structure RecognitionWorkConstraintCert L359
def recognition_work_constraint_cert L380
theorem recognition_work_constraint_theorem L409