OperativePositiveRatioComparison
plain-language theorem explainer
OperativePositiveRatioComparison bundles five properties on a ComparisonOperator C into one Prop: identity, reciprocal symmetry, continuity on positives, scale invariance, and non-triviality. Direct RCL proofs and canonicality results cite this structure to assume an operative comparison without repeating the axioms. The declaration is a structure definition with no proof body.
Claim. A comparison operator $C: (0,∞)×(0,∞)→ℝ$ is operative when it satisfies identity ($C(x,x)=0$ for $x>0$), non-contradiction ($C(x,y)=C(y,x)$ for $x,y>0$), continuity on the positive quadrant, scale invariance ($C(λx,λy)=C(x,y)$ for $λ>0$), and non-triviality (derived cost nonzero for some positive ratio).
background
ComparisonOperator is the abbrev ℝ→ℝ→ℝ for the cost of comparing two positive quantities. Identity requires $C(x,x)=0$. NonContradiction requires reciprocal symmetry $C(x,y)=C(y,x)$. ExcludedMiddle here encodes continuity: ContinuousOn (uncurry C) on $(0,∞)×(0,∞)$. ScaleInvariant requires the cost to depend only on the ratio. NonTrivial requires the derived cost (cost with second argument fixed at 1) to be nonzero somewhere. The module isolates this structure as the wrapper for the direct RCL theorem, separating it from the finite pairwise polynomial closure hypothesis.
proof idea
Structure definition that simultaneously requires the five field properties Identity, NonContradiction, ExcludedMiddle, ScaleInvariant, and NonTrivial to hold for the given ComparisonOperator.
why it matters
Feeds mismatch_to_operative (constructs the structure from MagnitudeOfMismatch), counted_once_combiner_forces_rcl (derives RCLFamily from operative plus CountedOnceComposition), operative_to_laws_of_logic (packages into SatisfiesLawsOfLogic), and rcl_direct_theorem (direct counted-once algebra). It supplies the exact hypothesis set needed to reach the Recognition Composition Law family in the direct proof path while keeping finite pairwise closure separate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.