operative_descends_to_ratio
plain-language theorem explainer
Operative positive-ratio comparisons reduce their two-argument form to a single-argument derived cost via scale invariance. Researchers formalizing the Recognition Composition Law would cite this reduction when translating between comparison operators and cost functions on ratios. The proof applies the scale-invariance hypothesis to rescale arguments by the inverse of the second variable, then rewrites using multiplication and inversion identities to reach the derived cost at the ratio.
Claim. Let $C$ be a comparison operator satisfying the operative positive-ratio conditions (identity, non-contradiction, continuity, scale invariance, and non-triviality). Then for all positive real numbers $x,y$, $C(x,y) = $ derivedCost$_C(x/y)$, where derivedCost$_C(r) := C(r,1)$.
background
The module isolates the direct RCL theorem for operative positive-ratio comparison. A ComparisonOperator is a map from pairs of positive reals to reals. derivedCost of $C$ is the map $r mapsto C(r,1)$, well-defined on positive ratios under scale invariance. OperativePositiveRatioComparison $C$ is the structure requiring identity, non-contradiction, continuity (via ExcludedMiddle), scale invariance, and non-triviality on positive arguments.
proof idea
The tactic proof introduces positive $x,y$, unfolds derivedCost, obtains inverse positivity, applies the scale_invariant field to equate $C x y$ with $C(y^{-1}x)(y^{-1}y)$, then rewrites the arguments via mul_comm and inv_mul_cancel to obtain $C(x/y)1$.
why it matters
This reduction supplies the scale-invariance step needed for the direct RCL theorem in the same module. It connects to the Recognition Composition Law functional equation and the T5 J-uniqueness landmark in the forcing chain. The result prepares the ground for siblings such as rcl_direct_theorem by isolating the descent to ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.