canonicality_of_encoding
plain-language theorem explainer
A comparison operator equipped with the magnitude-of-mismatch interpretation and finite pairwise polynomial closure satisfies the full set of laws of logic. Researchers deriving logic from the Recognition functional equation would cite this result to close the encoding step. The proof is a one-line term that converts the mismatch structure and applies the operative-to-laws lemma.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ satisfies the magnitude-of-mismatch conditions (trivial value at match, pair symmetry, determinate continuity, scale freedom, nontriviality) together with finite pairwise polynomial closure, then $C$ satisfies the laws of logic: identity, non-contradiction, excluded middle, scale invariance, and route independence.
background
ComparisonOperator is an abbreviation for a map ℝ → ℝ → ℝ that assigns a real cost to any pair of positive reals. MagnitudeOfMismatch is the structure whose five fields are exactly the Aristotelian constraints read as mismatch magnitude: Identity (trivial at match), NonContradiction (pair symmetry), ExcludedMiddle (determinate continuity), ScaleInvariant (scale-free), and NonTrivial. SatisfiesLawsOfLogic is the target structure that adds route independence to the first four constraints plus scale invariance.
proof idea
The proof is the one-line term operative_to_laws_of_logic C (mismatch_to_operative C hM) hFinite. It first converts the MagnitudeOfMismatch hypothesis into an operative positive-ratio structure via the sibling lemma mismatch_to_operative, then feeds that structure together with the FinitePairwisePolynomialClosure assumption into operative_to_laws_of_logic.
why it matters
This theorem packages the canonicality step of the Recognition Science logic encoding. It shows that the magnitude-of-mismatch reading plus finite pairwise polynomial closure directly yields SatisfiesLawsOfLogic, which supplies the operator-level input to the Recognition Composition Law. The module doc-comment records that the philosophical claim of uniqueness is left to the paper; the Lean result only verifies the implication from the packaged reading to the formal laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.