IndisputableMonolith.Foundation.MagnitudeOfMismatch
The MagnitudeOfMismatch module defines the single-valued-on-unordered-pair property for comparison operators C : K → K → Cost. Researchers formalizing symmetry in recognition costs within the forcing chain cite it when establishing order-independent mismatch. The module proceeds via a chain of lemmas that equate single-valuedness with symmetry and factoring through Sym2, then derive the forced magnitude of mismatch.
claimA comparison operator $C : K o K o \mathrm{Cost}$ is single-valued on the unordered pair when it factors through the type of unordered pairs $\mathrm{Sym2}\, K$, so that $C(x,y)$ equals $f(\{x,y\})$ for a single function $f$ independent of argument order.
background
The module imports PrimitiveDistinction to ground basic costs and distinctions. Its central object is the SingleValuedOnUnorderedPair predicate on operators C, which requires that C factors through Sym2 K. Sibling lemmas establish that this predicate is equivalent to symmetry of C and that symmetry implies the factoring property. The setting is the foundation layer that precedes the T0–T8 forcing chain and supplies consistent mismatch costs for later recognizer constructions.
proof idea
This is a definition module whose argument consists of a sequence of equivalences and implications: singleValued_implies_symmetric, symmetric_implies_factorsThrough, and singleValued_iff_symmetric, followed by the derivation that magnitude_of_mismatch_forced holds once single-valuedness is assumed.
why it matters in Recognition Science
The module supplies the mismatch-cost foundation required by the root IndisputableMonolith module and by RecognizerInducesLogic, which unifies Recognition Geometry with the Law of Logic. It thereby supports the J-uniqueness step (T5) and the self-similar fixed-point step (T6) of the forcing chain by guaranteeing order-independent costs on pairs.
scope and limits
- Does not treat ordered or directed comparisons.
- Does not extend to continuous or infinite K.
- Does not derive numerical values of physical constants.
- Does not close the full T0–T8 forcing chain.