IndisputableMonolith.Foundation.CostFromDistinction
Abstract configuration spaces with empty config, commutative join, consistency, and independence, plus a nonnegative cost vanishing exactly on consistent configs and additive on independent joins. Supplies the algebraic floor for recognition cost before any forcing. Downstream foundation modules import it to pin T-1 through T1 and the unified T0-T8 chain. Content is definitional: ConfigSpace and CostFunction with elementary monoid and positivity lemmas.
claimA configuration space is a type $\Gamma$ with empty element $e$, commutative monoid join $\Gamma_1 * \Gamma_2$, consistency predicate $C$, and independence relation $I$, such that $e$ is the identity and is consistent, $I$ is symmetric with $I(e,\cdot)$, consistent independent configs join to a consistent config, and inconsistency is preserved under independent join. A cost $J:\Gamma\to\mathbb{R}_{\ge 0}$ satisfies $J(\gamma)=0$ iff $C(\gamma)$, and $J(\gamma_1*\gamma_2)=J(\gamma_1)+J(\gamma_2)$ whenever $I(\gamma_1,\gamma_2)$.
background
Recognition Science starts from distinguishability rather than a pre-chosen Lagrangian. This module axiomatizes that starting point as a configuration space: an empty configuration, a binary join, a consistency predicate, and an independence relation (no shared predicates).
The stated laws make join a commutative monoid with empty identity; independence is symmetric and empty is independent of everything; empty is consistent; consistent independent pieces join consistently; inconsistent pieces stay inconsistent under independent join. The axioms are thin enough to instantiate on predicate-constraint configs, sequent multisets, or typed assertions.
A cost function is then any nonnegative map that vanishes exactly on consistent configurations and is additive on independent joins. The module imports only Mathlib; the content is self-contained axiomatics for the ledger floor and the early forcing bridge.
proof idea
This is a definition module, not a deep proof development. It introduces the ConfigSpace structure (empty, join, consistency, independence, and the monoid/consistency laws) and the CostFunction interface (nonnegative cost zero exactly on consistent configs, additive on independent joins).
Elementary lemmas then record immediate consequences: empty has cost zero; cost is positive iff the config is inconsistent; cost vanishes on every consistent config; three-way additivity for mutually independent joins; and strict positivity of a join when both summands are inconsistent. No external lemmas beyond Mathlib arithmetic are required.
why it matters in Recognition Science
This module is the carrier for absolute distinguishability cost in the foundation layer. It is imported by RecognitionLedgerFloor, which closes the two genuine T-1/T0 audit gaps on the free additive cost floor; by TMinus1ToT1Bridge, which isolates T-1 (absolute floor of distinguishability), T0 (minimal recognition-work cost interface), and T1 (inconsistent floor states cannot be selected at zero cost); and by UnifiedForcingChain, which proves all of T0-T8 as inevitabilities from the cost foundation and the Recognition Composition Law.
Without this abstract cost-from-distinction layer, the forcing chain would lack a neutral interface on which the unique J-cost, phi, the eight-tick octave, and D=3 can later be forced.
scope and limits
- Does not force the unique J-cost form $(x+x^{-1})/2-1$; that is T5 in the forcing chain.
- Does not pin phi, the eight-tick octave, or D=3; those are later UnifiedForcingChain steps.
- Does not construct a concrete carrier (predicates, sequents, etc.); only the abstract interface.
- Does not prove existence of nontrivial costs beyond the stated axiomatic properties.
- Does not address the Recognition Composition Law or mass/ladder formulae.
used by (3)
declarations in this module (24)
-
class
ConfigSpace -
theorem
join_emp -
theorem
independent_emp -
theorem
inconsistent_of_join_indep_right -
structure
CostFunction -
theorem
emp_cost_zero -
theorem
cost_pos_iff_inconsistent -
theorem
cost_zero_of_consistent -
theorem
cost_pos_of_inconsistent -
theorem
cost_ne_zero_of_inconsistent -
theorem
additive_three -
theorem
additive_strict_of_both_inconsistent -
theorem
additive_emp_left -
theorem
additive_emp_right -
theorem
uniqueness_on_indep_decomposition -
theorem
uniqueness_three_indep -
theorem
then -
structure
Calibration -
theorem
calibration_pos -
theorem
extension_to_consistent -
theorem
with -
structure
RecognitionWorkConstraintCert -
def
recognition_work_constraint_cert -
theorem
recognition_work_constraint_theorem