mismatch_to_operative
plain-language theorem explainer
A comparison operator read as magnitude of mismatch yields an operative positive-ratio comparison structure. Workers assembling the canonical encoding of logic in Recognition Science cite this result when constructing SatisfiesLawsOfLogic from the mismatch package. The proof is a direct term-mode construction that maps each field of the input mismatch structure onto the corresponding field of the operative structure.
Claim. Let $C : ℝ → ℝ → ℝ$ be a comparison operator. If $C$ satisfies the magnitude-of-mismatch conditions (trivial value at exact match, symmetry of unordered pairs, continuous determinability, scale-free comparison, and nontriviality), then $C$ satisfies the operative positive-ratio comparison axioms (identity at the unit, non-contradiction, continuity, scale invariance, and nontriviality).
background
The module formalizes the canonicality step for the logic encoding. A ComparisonOperator is an abbreviation for maps from positive reals to reals that return a comparison cost. MagnitudeOfMismatch packages five conditions on such an operator: trivial_at_match (identity), pair_symmetric (non-contradiction), determinate_continuous (excluded middle), scale_free (scale invariant), and nontrivial. These conditions are shown to imply the OperativePositiveRatioComparison structure, whose fields collect identity, non-contradiction, continuous, scale_invariant, and non_trivial. The local setting is the derivation of logical laws from functional equations on costs, with upstream results supplying the definitions of both structures.
proof idea
The proof constructs the OperativePositiveRatioComparison instance by direct field assignment from the input hypothesis. Identity is taken from trivial_at_match, non_contradiction from pair_symmetric, continuous from determinate_continuous, scale_invariant from scale_free, and non_trivial from nontrivial. No auxiliary lemmas are applied; the term is a pure renaming of the five fields.
why it matters
This theorem supplies the bridge from the magnitude-of-mismatch reading to the operative comparison structure required for the canonical encoding. It is invoked inside canonicality_of_encoding to obtain SatisfiesLawsOfLogic and inside rcl_from_canonical_mismatch_encoding to derive the Recognition Composition Law family. The step fills the canonicality claim at the level of the paper's LogicAsFunctionalEquation section, confirming that the mismatch interpretation supplies exactly the structural content needed for the logic laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.