OperativePositiveRatioComparison
plain-language theorem explainer
Operative positive-ratio comparison packages the five axioms (zero self-cost, reciprocal symmetry, continuity on the positive quadrant, scale invariance, and non-triviality) that any comparison operator on positive reals must obey. Workers on the direct Recognition Composition Law proof cite this wrapper to isolate the regularity conditions before adding finite pairwise polynomial closure. The declaration is a bare structure definition with no computational content or lemmas.
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 (continuous 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
The module supplies the paper-facing wrapper for the Level-1 logic-as-functional-equation setting. A ComparisonOperator is any map from pairs of positive reals to reals that returns a comparison cost. Identity requires zero self-cost. NonContradiction requires reciprocal symmetry. ExcludedMiddle encodes both totality and continuity on the positive domain. ScaleInvariant reduces the two-argument form to a function of the ratio alone. NonTrivial excludes the zero function. The module doc states that this wrapper isolates the finite pairwise polynomial closure hypothesis as the precise regularity condition needed to force the Recognition Composition Law family.
proof idea
This declaration is a structure definition that bundles the five named properties Identity, NonContradiction, ExcludedMiddle, ScaleInvariant and NonTrivial; no lemmas are applied and no tactics are used.
why it matters
OperativePositiveRatioComparison supplies the central hypothesis for the direct RCL theorems. It is instantiated by mismatch_to_operative from the MagnitudeOfMismatch interpretation and serves as input to counted_once_combiner_forces_rcl, operative_to_laws_of_logic, operative_descends_to_ratio and rcl_direct_theorem. The structure supplies the regularity conditions that, together with finite pairwise polynomial closure, recover the Recognition Composition Law on the derived cost. It corresponds to the Level-1 setting in the Recognition Science framework before the eight-tick octave and spatial dimension steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.