canonical_excluded_middle
plain-language theorem explainer
The magnitude-of-mismatch reading of a comparison operator on positive reals encodes excluded middle directly as determinate continuity of the cost function on the open positive quadrant. Researchers closing the canonicality step in the Recognition Science derivation of logic from the J-functional equation cite this result. The proof is a one-line field projection from the MagnitudeOfMismatch structure.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ satisfies the magnitude-of-mismatch conditions (trivial value at exact match, symmetry of the unordered pair, determinate continuity, scale-free comparison, and nontriviality), then the uncurried map $C$ is continuous on $(0,∞) × (0,∞)$.
background
This module formalises the canonicality step of the logic encoding: once a comparison operator is read as a magnitude of mismatch, the operator-level conditions become the canonical structural content of that reading. A ComparisonOperator is an abbrev for ℝ → ℝ → ℝ, the cost of comparing two positive quantities. The MagnitudeOfMismatch structure packages five properties: trivial_at_match (Identity), pair_symmetric (NonContradiction), determinate_continuous (ExcludedMiddle), scale_free (ScaleInvariant), and nontrivial (NonTrivial). ExcludedMiddle itself is defined as ContinuousOn (Function.uncurry C) on the positive quadrant.
proof idea
The proof is the one-line term that projects the determinate_continuous field from the supplied MagnitudeOfMismatch hypothesis.
why it matters
This theorem supplies one direction of the canonicality argument inside LogicAsFunctionalEquation. It shows that the magnitude-of-mismatch interpretation canonically forces excluded middle, completing the bridge from the mismatch package to the Aristotelian conditions used in the functional-equation development. The module verifies the implication; the paper supplies the philosophical claim that this package is the right reading of Aristotle. It sits in the foundation layer that derives logic from the J-cost and Recognition Composition Law before the forcing chain reaches T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.