ComparisonOperatorL
plain-language theorem explainer
Type alias for binary maps on recovered reals: each argument and the value live in the Cauchy completion of the logic-derived rationals. Anyone stating Law-of-Logic axioms (identity, reciprocal symmetry, scale invariance, non-triviality) over that carrier cites it. The body is a pure abbreviation, no proof content.
Claim. A comparison operator on recovered reals is any binary map $C : \mathbb{R}_L \to \mathbb{R}_L \to \mathbb{R}_L$, where $\mathbb{R}_L$ is the Cauchy completion of the logic-recovered rationals.
background
The module is the recovered-real mirror of the real Law-of-Logic development. Structural fields (identity, symmetry, scale invariance, non-triviality) are written natively on the recovered carrier; analytic regularity is transported through the real embedding.
LogicReal is that carrier: the Cauchy completion of the recovered rationals, realized via Mathlib's completion of $\mathbb{Q}$ and the equivalence of logic-rationals with ordinary rationals, wrapped to avoid polluting global instances. A comparison operator is the two-argument cost surface against which those structural laws are stated.
Upstream cost notions (J-cost on recognition events, derived cost of a multiplicative recognizer, rung-coarsened multiset cost) all live on ordinary reals or specialized ratio types. This abbreviation supplies the matching binary type once the ambient field has been rebuilt from logic.
proof idea
Pure type abbreviation: no tactics, no lemmas. It names the function type LogicReal → LogicReal → LogicReal so downstream predicates and the one-argument derived cost can quantify over a single comparison-operator parameter.
why it matters
This is the carrier type for the entire recovered-real Law-of-Logic stack. Downstream, the one-argument derived cost is $C(r,1)$; identity, non-contradiction, scale invariance, and non-triviality are Props on this type; their bundle is the recovered-real satisfaction predicate. Transport theorems push each structural field, and the full bundle, to the already-verified real Law-of-Logic surface, so the Recognition Composition Law and J-uniqueness (forcing chain T5) become available over logic-recovered reals without re-proving analytic content. It is scaffolding for the claim that logic alone forces the same comparison geometry that ordinary reals already satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.